couldn't verify series of struct member initializations
ID0001119: This issue was created automatically from Mantis Issue 1119. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0001119 | Frama-C | Plug-in > wp | public | 2012-03-13 | 2013-04-23 |
Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
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.