--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on May 2012 ---
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