Helping the value analysis — part 3

Sven Mattsen is working at CEA until the summer. He is the author of this post. The post continues the series explaining how to guide the value analysis towards more precise conclusions. It starts where that one and that other left off.

Problem

This article is concerned with the Value Analysis plug-in of Frama-C which implements an automatic approach towards verifying C programs. The Value Analysis provides an overapproximated set of possible values for each occurence of each variable of a C program. I will describe how to guide the value analysis in the example below:

int main(int argc  char* argv[]) { 
      int x = argc % 11; 
      return 100 / x; 
} 

We can call the value analysis on this program by issuing frama-c -val smallcprogram.c on the shell. Among other things the plug-in tells us that x is always in the range from -10 to 10 at the point of the division. Frama-C also warns of a possible division by zero in the argument to return. Great we had overlooked that. Let us insert a check for this and return 0 in this case.

int main(int argc  char* argv[]) { 
       int x = argc % 11; 
       if(x != 0) 
               return 100 / x; 
       else 
               return 0; 
} 

When we call Frama-C again it gives the same result including the warning for a possible division by zero. This is despite the division being guarded by the if(x != 0). This time the alarm is a false alarm.

Explanation

What happened? The Value Analysis plug-in performs an abstract interpretation of the program with the abstract domain being ranges of integers (the actual abstract domain is more complex but for this example it is enough to consider this much simpler domain). Apart from the type the value analysis does not know anything about the variable argc and therefore sets the range of possible values for it to [MININT MAXINT]. When x is initialized the set of possible values of the expression argc % 11 is computed which is [-10 10]. Now it gets interesting. Inside the then block of the if condition we know that x can have every possible value within [-10 10] except 0. However in our simplified version of the value analysis it cannot represent [-10 10] \ 0 and therefore overapproximates to [-10 10]. This is precisely the reason why we still get this warning.

Solution

One way to get around this issue is to split the range of possible values of x right before the if condition into two sub-ranges. Luckily the Value Analysis plug-in allows us to do just that by inserting an assertion:

int main(int argc  char* argv[]) { 
       int x = argc % 11; 
       /*@ assert x < 0 || x >= 0;*/ 
       if(x != 0) 
               return 100 / x; 
       else 
               return 0; 
} 

The plug-in now splits the state propagated through the assert annotation continues with two independent analyses and later merges the results. To allow this the parameter -slevel N with N at least two must be passed to Frama-C. With these changes the range of possible values for the first analysis is [-10 -1] and the second is [0 10]. The first range is not interesting since there is no zero in there and the abstract interpretation will therefore not enter the then block of the if condition. However it will do this for the second range but now it can compute a range that includes all of the original elements without zero ([1 10]). Therefore it can now detect that x can not be zero inside the division expression. Everything is fine...

Final thoughts

If you want to track the states of the Value Analysis plug-in I recommend the special Frama-C functions Frama_C_dump_each() and Frama_C_show_each(). Just insert them in the C file at the position you are interested in.