Notes 

(0006043)

kroeckx

20150918 09:13
(edited on: 20150920 23:42) 

So my explanation was a little wrong. First both len and n are size_t, so unsigned, and so the 62 doesn't make sense.
Next, the real code is:
if (len + n >= 64) {
[...]
n = 64 n
len = n;
WP let's me proof that len >= n, but then I'm unsure how it helps the value analyses.




Thanks for the example. The analysis domains of Value are nonrelational, which is a known source of imprecision. This is the case here, because the analysis must keep track of the relation between len and n.
We are currently implementing a massive overhaul of the plugin. Hopefully, this example should ultimately be proven automatically. (Not before FramaC Silicon, though.) 



As a workaround this seems to work:
/*@ assert len ≡ \at(len,Pre)n; */ ; 



Can you post a selfcontained example, with assertions or postconditions for what you want to prove? I'm not quite following what works, what does not, and which plugin is doing what. You can constrain your function arguments (len, n, ...) using 'requires' clauses to build a suitable initial state. 



So an example showing the problem:
#include
/*@ requires len > 0 && len <= 1024;
@ requires n < 64;
*/
void main(size_t len, size_t n)
{
if (n != 0)
{
if (len >= 64  len + n >= 64)
{
n = 64  n;
len = n;
}
}
}
At the len = n line Value will show you:
Before this statement:
len ∈ [1..1024]
After this statement:
len ∈ [..]
n is:
n ∈ [1..63]
It's possible to prove that it should be:
len ∈ [0..1023] 



Thanks for the additional information. Your ACSL assertion len ≡ \at(len,Pre)n does something I did not expect.
 On the C side, the computation len  n is detected as potentially overflowing (in the negative). The possible range [62 .. 1023] % 2^32 yields [0..2^321] hence [..] for the possible values of len. ([62 .. 1023] is not an acceptable range for an unsigned variable)
 In the logic world, len  n is computed as belonging to [62 .. 1023], because all computations take place on mathematical integers
 taking into account the assertion after the assignment means that len can only contain the values common to [0..2^321] and [62 .. 1023], which is exactly [0..1023]
A slightly more involved version of Value could symbolically prove that len ≡ (size_t)(\at(len,Pre)n) (although this is currently not implemented). However, the crux of the proof is to show that len  n >=0, which only the WP is able to do for now. 



I tried the len  n >= 0 (and len >= n) before but that didn't do anything Value.
Looking at why my current assert works I should probably change it to just len < \at(len, Pre). 



In this example, nothing you can write will be able to help Value used alone, in the sense that you would get a precise state with all assertions proven. (Except a full disjunction on all possibles values for n, but let's not go there.)
The best you can do is to write some assertions that will have an effect, but won't be proven by Value itself. Those assertions may later be proven by WP, though.
Also, as you noticed, some assertions won't have any effect for Value. As a rule of thumb, for the arithmetic fragment, limit yourself to the language "assert lv {=, <=, >=, <, >} e", where lv is a leftvalue, and e an arbitrary expression. This will usually have some effect on lv, except if the possible values for e are too imprecise. 
