Frama-C Bug Tracking System - Frama-C
View Issue Details
0002166Frama-CPlug-in > Evapublic2015-09-17 23:342017-12-17 20:50
kroeckx 
buhler 
normalminoralways
assignedopen 
Frama-C Sodium 
 
0002166: Substraction results in unknown values
This line of code has: if (len + n >= 64) len -= n; For callstack [SHA256_Update :: frama-test.c:19 <- main] Before this statement / after this statement: n ∈ [1..63] and: For callstack [SHA256_Update :: frama-test.c:19 <- main] Before this statement: len ∈ [1..1024] After this statement: len ∈ [--..--] I was expecting len after this to be: len ∈ [0..1023] It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in: len ∈ [-62..1023] Kurt
No tags attached.
Issue History
2015-09-17 23:34kroeckxNew Issue
2015-09-17 23:34kroeckxStatusnew => assigned
2015-09-17 23:34kroeckxAssigned To => yakobowski
2015-09-18 09:13kroeckxNote Added: 0006043
2015-09-20 23:30kroeckxNote Edited: 0006043View Revisions
2015-09-20 23:42yakobowskiNote Added: 0006044
2015-09-20 23:42kroeckxNote Edited: 0006043View Revisions
2015-09-29 23:18kroeckxNote Added: 0006048
2015-09-30 10:18yakobowskiNote Added: 0006049
2015-09-30 19:01kroeckxNote Added: 0006050
2015-09-30 19:47yakobowskiNote Added: 0006051
2015-09-30 20:15kroeckxNote Added: 0006052
2015-09-30 20:22yakobowskiNote Added: 0006053
2017-12-17 20:50yakobowskiAssigned Toyakobowski => buhler
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006043)
kroeckx   
2015-09-18 09:13   
(edited on: 2015-09-20 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.
(0006044)
yakobowski   
2015-09-20 23:42   
Thanks for the example. The analysis domains of Value are non-relational, 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 Frama-C Silicon, though.)
(0006048)
kroeckx   
2015-09-29 23:18   
As a workaround this seems to work: /*@ assert len ≡ \at(len,Pre)-n; */ ;
(0006049)
yakobowski   
2015-09-30 10:18   
Can you post a self-contained example, with assertions or post-conditions 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.
(0006050)
kroeckx   
2015-09-30 19:01   
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]
(0006051)
yakobowski   
2015-09-30 19:47   
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^32-1] 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^32-1] 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.
(0006052)
kroeckx   
2015-09-30 20:15   
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).
(0006053)
yakobowski   
2015-09-30 20:22   
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 left-value, and e an arbitrary expression. This will usually have some effect on lv, except if the possible values for e are too imprecise.