Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001119Frama-CPlug-in > wppublic2012-03-13 13:362013-04-23 15:13
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001119: couldn't verify series of struct member initializations
DescriptionOur 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.
TagsNo tags attached.
Attached Filesc file icon 001.c [^] (513 bytes) 2012-03-13 13:36 [Show Content]
? file icon 001times.gpdat [^] (709 bytes) 2012-03-13 13:36
gif file icon 001times.gif [^] (22,024 bytes) 2012-03-13 13:37


c file icon 00b.c [^] (341 bytes) 2012-03-13 13:37 [Show Content]
c file icon 00bC.c [^] (1,161 bytes) 2012-03-13 13:37 [Show Content]
c file icon ftest.c [^] (698 bytes) 2012-03-13 13:37 [Show Content]

- Relationships

-  Notes
(0002764)
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.
(0002765)
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.
(0003738)
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.
(0003825)
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

- Issue History
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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker