Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002166Frama-CPlug-in > Evapublic2015-09-17 23:342017-12-17 20:50
Reporterkroeckx 
Assigned Tobuhler 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002166: Substraction results in unknown values
DescriptionThis 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006043)
kroeckx (reporter)
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 (manager)
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 (reporter)
2015-09-29 23:18

As a workaround this seems to work: /*@ assert len ≡ \at(len,Pre)-n; */ ;
(0006049)
yakobowski (manager)
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 (reporter)
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 (manager)
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 (reporter)
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 (manager)
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.

- Issue History
Date Modified Username Field Change
2015-09-17 23:34 kroeckx New Issue
2015-09-17 23:34 kroeckx Status new => assigned
2015-09-17 23:34 kroeckx Assigned To => yakobowski
2015-09-18 09:13 kroeckx Note Added: 0006043
2015-09-20 23:30 kroeckx Note Edited: 0006043 View Revisions
2015-09-20 23:42 yakobowski Note Added: 0006044
2015-09-20 23:42 kroeckx Note Edited: 0006043 View Revisions
2015-09-29 23:18 kroeckx Note Added: 0006048
2015-09-30 10:18 yakobowski Note Added: 0006049
2015-09-30 19:01 kroeckx Note Added: 0006050
2015-09-30 19:47 yakobowski Note Added: 0006051
2015-09-30 20:15 kroeckx Note Added: 0006052
2015-09-30 20:22 yakobowski Note Added: 0006053
2017-12-17 20:50 yakobowski Assigned To yakobowski => buhler
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker