Frama-C Bug Tracking System - Frama-C
View Issue Details
0001119Frama-CPlug-in > wppublic2012-03-13 13:362013-04-23 15:13
Jochen 
correnson 
normalminoralways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Fluorine-20130401 
0001119: couldn't verify series of struct member initializations
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.
No tags attached.
c 001.c (513) 2012-03-13 13:36
https://bts.frama-c.com/file_download.php?file_id=352&type=bug
? 001times.gpdat (709) 2012-03-13 13:36
https://bts.frama-c.com/file_download.php?file_id=353&type=bug
gif 001times.gif (22,024) 2012-03-13 13:37
https://bts.frama-c.com/file_download.php?file_id=354&type=bug
gif

c 00b.c (341) 2012-03-13 13:37
https://bts.frama-c.com/file_download.php?file_id=355&type=bug
c 00bC.c (1,161) 2012-03-13 13:37
https://bts.frama-c.com/file_download.php?file_id=356&type=bug
c ftest.c (698) 2012-03-13 13:37
https://bts.frama-c.com/file_download.php?file_id=357&type=bug
Issue History
2012-03-13 13:36JochenNew Issue
2012-03-13 13:36JochenStatusnew => assigned
2012-03-13 13:36JochenAssigned To => correnson
2012-03-13 13:36JochenFile Added: 001.c
2012-03-13 13:36JochenFile Added: 001times.gpdat
2012-03-13 13:37JochenFile Added: 001times.gif
2012-03-13 13:37JochenFile Added: 00b.c
2012-03-13 13:37JochenFile Added: 00bC.c
2012-03-13 13:37JochenFile Added: ftest.c
2012-03-14 09:27corrensonNote Added: 0002764
2012-03-14 09:30corrensonNote Added: 0002765
2012-03-14 09:30corrensonStatusassigned => acknowledged
2012-03-14 10:09corrensonStatusacknowledged => assigned
2012-03-14 10:09corrensonAssigned Tocorrenson => pherrmann
2012-06-13 10:05signolesAssigned Topherrmann => correnson
2013-03-09 23:35yakobowskiNote Added: 0003738
2013-04-23 15:12corrensonNote Added: 0003825
2013-04-23 15:13corrensonStatusassigned => closed
2013-04-23 15:13corrensonResolutionopen => fixed
2013-04-23 15:13corrensonFixed in Version => Frama-C Fluorine

Notes
(0002764)
correnson   
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.
(0002765)
correnson   
2012-03-14 09:30   
Should be solved by refactoring of models and usage of alt-ergo 0.94 planned for future release.
(0003738)
yakobowski   
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.
(0003825)
correnson   
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