--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



Hello Boris,

2012/4/28 Boris Yakobowski <boris at yakobowski.org>:
> Here are a few complements to the answer that was given on the blog.

For the record:
  http://blog.frama-c.com/index.php?post/2012/04/28/The-value-analysis-propagation-order-is-inscrutable

> I think there exists a very common misunderstanding concerning the
> action of option -slevel k. What it does _not_ do is unroll loops k
> times. In many cases, this is what seems to happen. However, the real
> effect is to allow the independent propagation of k different states,
> for each statement.

This is clearly my understanding of -slevel.

> For simple loops, this is equivalent, as you need
> one state per value of the loop index. In other cases, it is clearly
> not:
>
> #define N 10
> int t[N];
> volatile int v;
>
> void main() {
> ?for (int i=0;i<N;i++) {
> ? ?if (v) t[i] = i;
> ?}
> }
>
> This example needs an slevel of 256 to be unrolled completely, because
> Value ultimately propagates all (t[1] ? {0, 1}) x ... x (t[9] ? {0,
> 9}) combinations. This is not useful here (the values of t[i-m] are
> not useful to compute t[i]), but this fact is not obvious without some
> prior analysis, which would have to influence the propagation strategy
> of Value.

OK. 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.

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. The more t[] I have, the more states I need for a precise
analysis. That's not a very good news. :-)

> As an additional example, your code within ?#ifdef ADDITIONAL_IF
> double the number of slevel required, because two states for 'a' are
> propagated separately.

Yes, that was my understanding.

> Does this explain your last interrogation (more
> than 10000 slevel required)?

I think so, thanks!

> Next, once you have more than one loop, things get much more
> complicated. With your nested loops, the -slevel 100 you chose is
> insufficient to propagate all possible states. So a question of
> fairness appears: should some fraction of the slevel be used for the
> inner loop, and the remainder for the outer one? Or should all the
> slevel be consumed by one of the two loops? But this is in fact a
> rhetorical question. As Pascal wrote, Value has a low-level view of
> the control-flow-graph, in which notions of inner and outer loops are
> almost meaningless. The order in which Value propagates states is thus
> entirely unspecified.

OK.

> For code such as yours, the "good" solution is
> to use enough slevel to entirely unroll the loops, or almost none at
> all. In your example, using a slevel of 2 or of 100 does little
> difference.

OK, I'll try to remember that.

> I can however shed another light on why adding some statements degrade
> the precision on k. In your example, the new statement changes not
> only the propagation strategy, but also increases the number of
> widening steps that are performed. Here, more widening are performed
> on the inner loop, and j ends up being widened there [1]. This can for
> example be observed in the gui [2]. This is turn degrades the
> precision on k, but the real cause is the loss of precision on j. My
> suggestion to avoid this would be to add another loop invariant on j,
> this time to the inner loop.
> ? ?/*@ loop invariant min <= j < max;
> ? ? ? ?loop invariant j - 31/2 <= k && k <= j+31/2+1; ?*/

OK. I tested it and indeed it helps Value analysis.

> [2] [...]
> Notice that, with
> the additional loop invariant on j, both invariant related to j get
> status Valid.

Yes with -slevel 620 and 600. With -slevel 100, 200, 400 and 500, only
the second instance of "loop invariant min <= j <= max;" (that you
could indeed write "loop invariant min <= j < max;") gets status
valid.


My question would be now: how can I control and help the Value
analysis on a given code?

Currently, on my test code at hand, I have two objectives:
  1. Verify some safety properties, like no out-of-bound array access
or integer overflow;

  2. Get some information on floating point computations, e.g. the
precision of those computations.

For 1., I am considering using WP plugin (Jessie crashes on this code).

>From you explanation, invariants gathered in step 1 could also help
step 2. Overall, the lack of predictability is very disturbing.

Best regards,
david