Search code examples
frama-c

Eva method to compute intervals [frama-c]

My goal is to understand how Eva shrinks the intervals for a variable. for example:

unsigned int nondet_uint(void);
int main()
{
  unsigned int x=nondet_uint();
  unsigned int y=nondet_uint();
  //@ assert x >= 20 && x <= 30;
  //@ assert y <= 60;
  //@ assert(x>=y);
  return 0;
}

So, we have x=[20,30] and y=[0,60]. However, the results from Eva shrinks y to [0,30] which is where the domain may be valid.

[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  x ∈ [20..30]
  y ∈ [0..30]
  __retres ∈ {0}

I tried some options for the Eva plugin, but none showed the steps for it. May I ask you to provide the method or publication on how to compute these values?

Solution

  • Showing values during abstract interpretation

    I tried some options for the Eva plugin, but none showed the steps for it.

    The most efficient way to follow the evaluation is not via command-line options, but by adding Frama_C_show_each(exp) statements in the code. These are special function calls which, during the analysis, emit the values of the expression contained in them. They are especially useful in loops, for instance to see when a widening is triggered, what happens to the loop counter values.

    Note that displaying all of the intermediary evaluation and reduction steps would be very verbose, even for very small programs. By default, this information is not exposed, since it is too dense and rarely useful.

    For starters, try adding Frama_C_show_each statements, and use the Frama-C GUI to see the result. It allows focusing on any expression in the code and, in the Values tab, shows the values for the given expression, at the selected statement, for each callstack. You can also press Ctrl+E and type an arbitrary expression to have its value evaluated at that statement.

    If you want more details about the values, their reductions, and the overall mechanism, see the section below.

    Detailed information about values in Eva

    Your question is related to the values used by the abstract interpretation engine in Eva.

    Chapter 3 of the Eva User Manual describes the abstractions used by the engine, which are, succinctly:

    • sets of integers, which are maximally precise but limited to a number of elements (modified by option -eva-ilevel, which on Frama-C 22 is set to 8 by default);
    • integer intervals with periodicity information (also called modulo, or congruence), e.g. [2..42],2%10 being the set containing {2, 12, 22, 32, 42}. In the simple case, e.g. [2..42], all integers between 2 and 42 are included;
    • sets of addresses (for pointers), with offsets represented using the above values (sets of integers or intervals);
    • intervals of floating-point variables (unlike integers, there are no small sets of floating-point values).

    Why is all of this necessary? Because without knowing some of these details, you'll have a hard time understanding why the analysis is sometimes precise, sometimes imprecise.

    Note that the term reduction is used in the documentation, instead of shrinkage. So look for words related to reduce in the Eva manual when searching for clues.

    For instance, in the following code:

    int a = Frama_C_interval(-5, 5);
if (a != 0) {
  //@ assert a != 0;
  int b = 5 / a;
}

    By default, the analysis will not be able to remove the 0 from the interval inside the if, because [-5..-1];[1..5] is not an interval, but a disjoint union of intervals. However, if the number of elements drops below -eva-ilevel, then the analysis will convert it into a small set, and get a precise result. Therefore, changing some analysis options will result in different ranges, and different results.

    In some cases, you can force Eva to compute using disjunctions, for instance by adding the split ACSL annotation, e.g. //@ split a < b || a >= b;. But you still need the give the analysis some "fuel" for it to evaluate both branches separately. The easiest way to do so is to use -eva-precision N, with N being an integer between 0 and 11. The higher N is, the more splitting is allowed to happen, but the longer the analysis may take.

    Note that, to ensure termination of the analysis, some mechanisms such as widening are used. Without it, a simple loop might require billions of evaluation steps to terminate. This mechanism may introduce extra values which lead to a less precise analysis.

    Finally, there are also some abstract domains (option -eva-domains) which allow other kinds of values besides the default ones mentioned above. For instance, the sign domain allows splitting values between negative, zero and positive, and would avoid the imprecision in the above example. The Eva user manual contains examples of usage of each of the domains, indicating when they are useful.