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: boris at yakobowski.org (Boris Yakobowski)
  • Date: Sat, 28 Apr 2012 13:45:20 +0200
  • In-reply-to: <CAC3Lx=YsN9UReq035Y93i0pyo0TGYWmV4uK+u+wccvN-thDVLg@mail.gmail.com>
  • References: <CAC3Lx=YsN9UReq035Y93i0pyo0TGYWmV4uK+u+wccvN-thDVLg@mail.gmail.com>
Hi David,

Here are a few complements to the answer that was given on the blog.

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

As an additional example, your code within  #ifdef ADDITIONAL_IF
double the number of slevel required, because two states for 'a' are
propagated separately. Does this explain your last interrogation (more
than 10000 slevel required)?


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

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;  */

Hope this clear things up,

[1] The current approach for finding which variables should be widened
could be made a bit smarter. For example, there is no real reason to
widen j in the inner loop, as it is not increased within. Conversely,
k should not be widened in the outer loop. The second possibility does
not occur here (I think), but the first one does. However, this is
complicated to get right without endangering the convergence of the
analysis in corner cases.

[2] The loss of precision on j is not visible in the synthetic text
results. The possible values for j are constrained by your loop
invariant each time the outer "loop" statement is analyzed. At some
point, when j is widened to 127 by the inner loop, the loop invariant
gets status unknown. However, the range of j keeps getting constrained
at the beginning of the loop body. You may have detected this by using
Frama_C_show_each_k_j(k, k); in your inner loop, but sing the GUI to
see the possible ranges of important variables at various statements
is complementary to the use of Frama_C_show_each(). Notice that, with
the additional loop invariant on j, both invariant related to j get
status Valid.

-- 
Boris