View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001119 | Frama-C | Plug-in > wp | public | 2012-03-13 13:36 | 2013-04-23 15:13 | ||||
Reporter | Jochen | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Nitrogen-20111001 | ||||||||
Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
Summary | 0001119: couldn't verify series of struct member initializations | ||||||||
Description | Our students Kerstin Hartig and Kim Völlinger observed problems to verify a series of assignments to struct members. Their extensive investigations of code variants and workaround possibilities is the basis for the following issue description. Running "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof alt-ergo -wp-timeout 99999999 -no-unicode -wp-warnings 001.c", Alt-Ergo's proof attempt for line 25 didn't terminate within reasonable time, although only the effect of a trivial series of 16 initializing assignments was to be verified. That series wasn't unusually long; e.g. the most popular struct _IO_FILE has 21 members (in /usr/include/libio.h on my linux) that all need to be initialized. In contrast to Alt-Ergo, the Simplify prover found a proof within the default time-limit of 10 secs. Timing the proof attempts for shorter assignment series, we observed the figures in file 001times.gpdat (elapsed time on a 1GHz machine). Plotting them by gnuplot exhibits their super-exponential growth (file 001times.gif). This behavior is reported separately to the Alt-Ergo bts. Suggestion (A): In file 00b.c, we omitted encapsulating variables a,...,p into a struct and defined each of them as an own global variable. In that case, Wp optimizes the assignment series such that no proof obligation at all needs to be given to Alt-Ergo. I suggest to consider performing the same optimization for struct fields; I guess this should be admitted by the default Store memory model. For example, in file 00bC.c, only the contents of the ->a fields need to be considered to verify the ensures clauses in lines 45-47. Suggestion (B): Trying to find out the reason for Alt-Ergo's runtimes, I found that a proof of non-interference of different struct fields needs the property x<>y==>addr_shift(s,x)<>addr_shift(s,y), which can be proven from the right-injectivity of +, the axiom addr_inj2, and the definition of addr_shift: x <> y ==> offset(s)+x <> offset(s)+y ==> addr(base(s),offset(s)+x) <> addr(base(s),offset(s)+y) ==> addr_shift(s,x) <> addr_shift(s,y) However, Alt-ergo seems to have problems to draw that conclusion. When I provide it as an additional axiom axiom a2 : (forall s:int.(forall x:int.(forall y:int. addr_shift(s,x)=addr_shift(s,y) -> x=y))) Alt-Ergo verifies 001.c about as fast as Simplify. Hence, as a backup suggestion for those cases where (A) doesn't work or isn't sufficient, that additional axiom could be included in the .why files given to Alt-Ergo. (However, I'm not sure that this won't cause problems in other contexts.) Alternatively, and as a workaround, that axiom can be user-provided as Acsl: /*@ axiomatic a1 { axiom a2: \forall int* s; \forall integer x,y; (int)(&s[x]) == (int)(&s[y]) ==> x == y; } */ This works also with heterogeneous struct field types as e.g. in file ftest.c. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
correnson (manager) 2012-03-14 09:27 |
Hi Jochen, Your are perfectly right in your analyzes and, indeed, we already observed similar behaviors in our own experiments. We are currently working on these topics in the following way: A) Your proposed optimizations for top-level struct globals is very interesting. In some sense, it is a generalization of our new algorithm for detecting variables-or-array passed-by-reference, which is not yet fully deploied in current version. For sure, I will try to take your idea into account. B) Using built-in record types of Alt-Ergo 0.94 to encode pointers in Store model will tackle the exponential proof search involving injectivity inversions such as shift(s,i) <> shift(s,j) whenever i<>j. More generally, we are refactoring all the models for maximal usage of build-in theories in alt-ergo. The combination of records and arrays theories are especially powerfull at propagating equalities and disequalities, such that reasoning with separation and memory becomes painless. |
correnson (manager) 2012-03-14 09:30 |
Should be solved by refactoring of models and usage of alt-ergo 0.94 planned for future release. |
yakobowski (manager) 2013-03-09 23:35 |
With alt-ergo 0.94 and current WP, the properties of files 00bC.c (without axiom) are proved in 5s. This bug can probably be closed. |
correnson (manager) 2013-04-23 15:12 |
Fluorine : 001.c : 1 po, Alt-Ergo 255ms 00b.c : no po, Qed < 1ms 00bC.c : requires \separated(s,t) to be proved. 3 pos, Alt-Ergo timeout 30s required for 2. ftest.c : 1 po, Alt-Ergo 60ms |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2012-03-13 13:36 | Jochen | New Issue | |
2012-03-13 13:36 | Jochen | Status | new => assigned |
2012-03-13 13:36 | Jochen | Assigned To | => correnson |
2012-03-13 13:36 | Jochen | File Added: 001.c | |
2012-03-13 13:36 | Jochen | File Added: 001times.gpdat | |
2012-03-13 13:37 | Jochen | File Added: 001times.gif | |
2012-03-13 13:37 | Jochen | File Added: 00b.c | |
2012-03-13 13:37 | Jochen | File Added: 00bC.c | |
2012-03-13 13:37 | Jochen | File Added: ftest.c | |
2012-03-14 09:27 | correnson | Note Added: 0002764 | |
2012-03-14 09:30 | correnson | Note Added: 0002765 | |
2012-03-14 09:30 | correnson | Status | assigned => acknowledged |
2012-03-14 10:09 | correnson | Status | acknowledged => assigned |
2012-03-14 10:09 | correnson | Assigned To | correnson => pherrmann |
2012-06-13 10:05 | signoles | Assigned To | pherrmann => correnson |
2013-03-09 23:35 | yakobowski | Note Added: 0003738 | |
2013-04-23 15:12 | correnson | Note Added: 0003825 | |
2013-04-23 15:13 | correnson | Status | assigned => closed |
2013-04-23 15:13 | correnson | Resolution | open => fixed |
2013-04-23 15:13 | correnson | Fixed in Version | => Frama-C Fluorine |