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

  • Subject: [Frama-c-discuss] Issue understanding Value analysis approximation on loop bounds
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 2 May 2012 09:15:07 +0200
  • In-reply-to: <CABbVA-D-3_LpyiFQSuW2Qrs+rzZ33h+019UORdbT4nAq6W97eA@mail.gmail.com>
  • References: <CAC3Lx=YsN9UReq035Y93i0pyo0TGYWmV4uK+u+wccvN-thDVLg@mail.gmail.com> <CABbVA-D-3_LpyiFQSuW2Qrs+rzZ33h+019UORdbT4nAq6W97eA@mail.gmail.com>
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