Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds

On 05/05/2012 12:24 AM, Pascal Cuoq wrote:
> David Mentr? wrote:
>
>> So, if I understand correctly, using an array t[] in a code will
>> multiply the number of propagated states, because the possible values
>> for the array are taken into account.
> No.
>
> You have seen a few examples where the presence of an array t[]
> was a catalyst in multiplying the number of propagated states. One
> was your original example with nested loops. Another was specially
> crafted by my facetious colleague Boris to illustrate one other particularity.
> Your statement above, as a general statement about Frama-C's
> value analysis, is extremely misleading and is a bad way to
> summarize or remember how it works. The slevel option separates
> abstract paths, and optionally user-provided ACSL disjuncts,
> not ?possible values for the array?.

Hi David and Pascal,

At the risk of saying something wrong, I'll try to explain what I think 
-slevel does. Abstract interpretation works by abstracting state. In 
Frama-C, state is abstracted at each program point using the value 
abstract domain, which, for integer values, is the same as the widely 
used interval abstract domain. So every integer value X in your code is 
abstracted as a range min..max at every program point. So, without 
slevel, the analysis of the following program only knows that i and j 
are in 0..1 after the if-statement, not that they are equal:

//@ requires 0 <= i <= 1;
void main(int i) {
   int j;
   if (i == 0) {
     j = 0;
   }
   else {
     j = 1;
   }
   //@ assert i == j;
   return;
}

This is because, at the join point after the if-statement, the analyzer 
"joins" (this is the abstract join operator of abstract interpretation) 
two states, one where i = j = 0 and one where i = j = 1. Now, if you set 
-slevel to 1, then the analyzer keeps these two states separate instead 
of merging them, so that it now knows that the assertion holds.

The explanation of -slevel in Frama-C manual says this in a slightly 
more abstract way, and it also says that it has a similar effect as 
unrolling loops. Indeed, join points are everywhere the flow of control 
encounters another path, which occurs at the start of loops.


>
>> So if I have code linear like:
>> """
>> ... = ... t1[i] ....
>> ...
>> t2[j] = ...
>> """
>> then all possible values for t1[] and t2[] arrays will be taken into
>> account, thus increasing the need for a high -slevel for a precise
>> analysis.
> No. Unlike the previous statement which, despite being generally false,
> is true about some particular examples, this statement is simply
> always false. The -slevel option has no effects at all on the analysis
> of a linear code without ACSL disjunctions. If you identify a piece of
> linear code on which the option -slevel has an effect, feel free
> to report it as a bug.

I believe that it is clear once you understand that -slevel has only an 
effect on the number of states that are kept separate at join points. On 
your example, David, there are no join points at all, so no effect of 
-slevel.


> I do not think that the Q&A format is going to work to transmit the
> fundamentals. My case rests on recent discussions on this list
> (including this thread).

One thing I found quite effective at conveying how the tool works, 
without going into the details of how it is implemented, is to 
show/discuss the detailed results on small examples. I have done it for 
our static analyzer CodePeer, and this works very well in trainings. 
Here is the online version if you want to have a look at it: 
http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html

(And it is quite fast to do for someone very familiar with the tool, it 
took me just one week. One thing you'd like though is that the document 
is generated from actual runs of the tool on the examples, so that it is 
kept up-to-date easily, which is what we did.)

> I would recommend that anyone interested in the subject reads up
> on abstract interpretation, the technique on which the value analysis
> is loosely based (as I think the manual mentions).

I don't think you need to read highly mathematical descriptions of 
abstract domains to understand what -slevel does. And I believe David 
knows much more than what is needed already. I agree with you that a 
tool has many tradeoffs that cannot be all documented (except in the 
code!), but surely that question of David can be answered simply like I 
just did.

-- 
Yannick Moy, Senior Software Engineer, AdaCore