Anonymous | Login | Signup for a new account | 2019-08-25 21:09 CEST |

Main | My View | View Issues | Change Log | Roadmap | Repositories |

View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||

ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||

0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 23:34 | 2017-12-17 20:50 | ||||||||

Reporter | kroeckx | ||||||||||||

Assigned To | buhler | ||||||||||||

Priority | normal | Severity | minor | Reproducibility | always | ||||||||

Status | assigned | Resolution | open | ||||||||||

Platform | OS | OS Version | |||||||||||

Product Version | Frama-C Sodium | ||||||||||||

Target Version | Fixed in Version | ||||||||||||

Summary | 0002166: Substraction results in unknown values | ||||||||||||

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

Tags | No tags attached. | ||||||||||||

Attached Files | |||||||||||||

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 <stdlib.h> /*@ 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 |