New loop unroll annotation in Frama-C 18

One of the new features in Frama-C 18 (Argon) is the annotation @loop unroll, used by the Eva plug-in to replace and improve upon the usage of slevel for semantically unrolling loops. This new annotation is more stable, predictable, and overall more efficient. In this post we present the annotation with some examples where it outperforms previous mechanisms.

Loop unrolling mechanisms in Frama-C/Eva

Frama-C has two ways to unroll loops syntactically: either via option -ulevel N (which unrolls all loops in the program N times), or via the loop pragma UNROLL annotation, placed before a loop, which unrolls only that loop. Both have their uses, especially for plug-ins other than Eva; however, Eva has specific mechanisms which are almost always better suited to deal with loops.

When using the Eva plug-in, syntactic loop unrolling is is not recommended: it is more costly than semantic unrolling, and it makes the code harder to read in the GUI.

In Eva, the slevel mechanism is used to improve precision of the analysis inside loops: as long as there is enough slevel to be consumed, each loop iteration will keep consuming it before performing a widening and merging states, which might lead to loss of precision.

This works fine for simple loops, but as soon as there are branches or nested loops, slevel consumption is hard to control: each branch will also consume some slevel, and there is no way to ensure that only outer loop iterations will consume the remaining slevel.

To mitigate the effects of unwanted slevel consumption, options such as -eva-slevel-merge-after-loop force the merging of states at the end of each loop iteration, which minimizes the issue with loops containing branches. However, this option operates at the function level, so nested loops are still an issue.

Plug-ins such as Loop Analysis perform complex estimations to try and indicate values of slevel for each function, accounting for the fact that nested loops and branches require extra slevel. In realistic code bases, this often leads to functions having excessively large values of slevel (in the worst case, such overflows lead to 0, that is, giving up unrolling).

In the end, existing solutions had drawbacks which imposed an extra burden on the parameter refinement process. This motivated the development of the new @loop unroll annotation.

The new loop unroll mechanism

@loop unroll N is a code annotation, to be placed just before a loop in the program (as is the case with all @loop ACSL annotations). It will instruct Eva to avoid merging states after each loop iteration, until either:

• there are no more states to unroll (i.e. the loop has been completely unrolled), or
• N unrollings have been performed.

Just like with slevel, a value for N larger than the required to completely unroll the loop will not lead to wasted time.

The annotation currently accepts only constant expressions, that is, those involving literal constants or #define macros. This limitation may be removed in the future.

Nested loops and slevel usage

The main advantage of using @loop unroll is in the presence of nested loops. Consider the following example:

void main() {
  int a[10][10] = {0};
  for (int i = 0; i < 10; i++) {
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;
    }
  }
}

In this program, one might naively think that using -eva-slevel 100 would be enough to unroll the loops. This will however result in:

[eva] example1.c:4: starting to merge loop iterations
[eva:alarm] example1.c:5: Warning:
  signed overflow. assert a[i][j] + (int)(i + j) ≤ 2147483647;
...
[eva:final-states] Values at end of function main:
...
   [8][9] ∈ {17}
   [9][0] ∈ {9}
   [9][1..9] ∈ [0..2147483647]

The first message indicates that there was not enough slevel to consume during the analysis, and thus a merge between different loop iterations happened, resulting in loss of precision. Widening causes the last cells of the matrix to contain over-approximated intervals, leading to an alarm.

The reason why 100 is not enough is due to the fact that an extra slevel is consumed for each iteration of the outer loop; for instance, you can try using -eva-slevel 10 and then -eva-slevel 11 and checking the displayed final states: in the first case, the result remains imprecise for the entire matrix:

[eva:final-states] Values at end of function main:
  a[0..9][0..9] ∈ [0..2147483647]

While in the second case (-eva-slevel 11), we have:

[eva:final-states] Values at end of function main:
  a[0][0] ∈ {0}
   [0][1] ∈ {1}
   [0][2] ∈ {2}
   [0][3] ∈ {3}
   [0][4] ∈ {4}
   [0][5] ∈ {5}
   [0][6] ∈ {6}
   [0][7] ∈ {7}
   [0][8] ∈ {8}
   [0][9] ∈ {9}
   [1..9][0..9] ∈ [0..2147483647]

Thus, the actual slevel required to completely unroll both loops is 109 (the last iteration does not require extra slevel). Computing this exact value is not straightforward, and it gets even more complicated when there are branches in the loop.

Using @loop unroll in nested loops

The @loop unroll annotation is local to a loop, and thus completely independent of whether the loop contains or is contained by other loops. Therefore, we can perform simple calculations to obtain the bounds: (max - min) / step in the general case, which here results in (10 - 0) / 1 = 10.

void main() {
  int a[10][10] = {0};
  //@ loop unroll 10;
  for (int i = 0; i < 10; i++) {
    //@ loop unroll 10;
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;
    }
  }
}

With the above annotations, simply running Eva, without any slevel required, will result in no alarms at all. The bounds are much simpler to compute. In future Frama-C releases, we hope to obtain this information automatically whenever possible, so the user will not have to add them in simple cases.

There is currently (in Frama-C 18 - Argon) an option to set a minimum value for @loop unroll for all loops in the program: -eva-min-loop-unroll. This may be unwise for realistic case studies with several loops, but in many cases this saves time by not having to add annotations to each loop in the program. In our first example, adding -eva-min-loop-unroll 10 has the same effect as adding the two //@ loop unroll 10; annotations.

Loops with branches and slevel usage

The previous example was comprised of two very simple nested loops. In reality, many loops contain branches and conditional exits. In such cases, slevel usage becomes exponential. For instance, consider this variant of the previous example, with a non-deterministic increment:

void main(int nondet) {
  int a[10][10] = {0};
  for (int i = 0; i < 10; i++) {
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;
      if (nondet) a[i][j]++;
    }
  }
}

In this example, instead of 109 as minimum slevel to avoid any warnings, Eva needs 5509. On my machine, the analysis goes from nearly instantaneous (about 0.3s) to visibly perceptible (about 1.7s). And all this for a very modestly-sized loop, with a single branching point.

Eva has an option to help mitigate the issue with slevel: -eva-slevel-merge-after-loop <functions>. This option ensures that, at the end of each loop iteration, all states from different branches in the current iteration will be merged. This avoids the exponential explosion, but still requires extra slevel, in a non-intuitive manner; for instance, the minimum slevel value required to avoid warnings in the above example is 208. Simply trying to understand precisely why this value is necessary and sufficient requires deep understanding of the evaluation mechanism inside Eva.

Again, if we add the same @loop unroll annotations as before, we do not need anything else: the analysis will not generate any warnings, it will run almost as fast as before (with a barely perceptible increase in time due to the branching), and it will be robust to changes: the introduction of extra branches or nested loops will not affect the existing annotations.

Warnings to help the user

The message starting to merge loop iterations is used to indicate insufficient slevel during the analysis of loops. A more specific warning is now available for loop unroll annotations. For instance, suppose we used 9 instead of 10 in our previous annotations. Eva would then report:

[eva:loop-unrolling] example2.c:6: loop not completely unrolled

This warning appears when there is an annotation that is insufficient to completely unroll the loop, which is often a sign that the annotation should contain a larger value. It can be disabled or even turned into an error, to make sure the user will not miss it.

Upgrading to the new mechanism

Existing case studies may benefit from the new annotation without requiring changes to existing parametrization; in most cases, keeping current slevel values (which are still necessary for dealing with branches) while adding such annotations should give results at least as precise, possibly improving the efficiency of the analysis. Then, slevel values can be lowered on a second stage.

The analysis scripts and sources in the Github open-source-case-studies repository have been updated to include several loop unroll annotations throughout the code, to serve as usage examples. During the process, we could confirm their improved reliability, predictability and ease of use. Their only downsides are that some oracles change due to different line numbers after they are introduced, and the fact that some (if not most) of these annotations could be automatically generated.

Conclusion

The slevel mechanism is very generic, but not appropriate in all situations, especially because it does not allow fine-grained control, and is context-dependent. Having a specific mechanism for handling loops, which is the majority of practical use cases, improves reliability and predictability of the analysis. It also prevents exponential blowup of states in more complex loops.

loop unroll annotations are very useful and likely to be present in every meaningful case study. Their usage is straightforward, and future Frama-C versions may end up incorporating more flexible annotations (e.g. using non-constant expressions). The slevel mechanism is still used in some cases, especially for branching, but its usage is likely to diminish over time, replaced with more specialized and expressive mechanisms.