0001119: couldn't verify series of struct member initializations

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

001.c (513 bytes) 2012-03-13 13:36

struct _str {
    int a;
    int b;
    int c;
    int d;
    int e;
    int f;
    int g;
    int h;
    int i;
    int j;
    int k;
    int l;
    int m;
    int n;
    int o;
    int p;
};

struct _str *s;

/*@ 
    requires \valid(s);
    ensures s->a == 0;
*/
void ftest(void) {
    s->a = 0;
    s->b = 0;
    s->c = 0;
    s->d = 0;
    s->e = 0;
    s->f = 0;
    s->g = 0;
    s->h = 0;
    s->i = 0;
    s->j = 0;
    s->k = 0;
    s->l = 0;
    s->m = 0;
    s->n = 0;
    s->o = 0;
    s->p = 0;
}

001.c (513 bytes) 2012-03-13 13:36

001times.gpdat (709 bytes) 2012-03-13 13:36
001times.gif (22,024 bytes) 2012-03-13 13:37

001times.gif (22,024 bytes) 2012-03-13 13:37

00b.c (341 bytes) 2012-03-13 13:37

int a;
int b;
int c;
int d;
int e;
int f;
int g;
int h;
int i;
int j;
int k;
int l;
int m;
int n;
int o;
int p;


/*@ 
    ensures a == 0;
*/
void ftest(void) {
    a = 0;
    b = 0;
    c = 0;
    d = 0;
    e = 0;
    f = 0;
    g = 0;
    h = 0;
    i = 0;
    j = 0;
    k = 0;
    l = 0;
    m = 0;
    n = 0;
    o = 0;
    p = 0;
}

00b.c (341 bytes) 2012-03-13 13:37

00bC.c (1,161 bytes) 2012-03-13 13:37

struct _str {
    int a;
    int b;
    int c;
    int d;
    int e;
    int f;
    int g;
    int h;
    int i;
    int j;
    int k;
    int l;
    int m;
    int n;
    int o;
    int p;
};

struct _str *s;
struct _str *t;

int a;
int b;
int c;
int d;
int e;
int f;
int g;
int h;
int i;
int j;
int k;
int l;
int m;
int n;
int o;
int p;


/*@ 
    requires \valid(s);
    requires \valid(t);
    ensures    a == 0;
    ensures s->a == 0;
    ensures t->a == 0;
*/
void ftest(void) {
       a = 0;
    s->a = 0;
    t->a = 0;
       b = 0;
    s->b = 0;
    t->b = 0;
       c = 0;
    s->c = 0;
    t->c = 0;
       d = 0;
    s->d = 0;
    t->d = 0;
       e = 0;
    s->e = 0;
    t->e = 0;
       f = 0;
    s->f = 0;
    t->f = 0;
       g = 0;
    s->g = 0;
    t->g = 0;
       h = 0;
    s->h = 0;
    t->h = 0;
       i = 0;
    s->i = 0;
    t->i = 0;
       j = 0;
    s->j = 0;
    t->j = 0;
       k = 0;
    s->k = 0;
    t->k = 0;
       l = 0;
    s->l = 0;
    t->l = 0;
       m = 0;
    s->m = 0;
    t->m = 0;
       n = 0;
    s->n = 0;
    t->n = 0;
       o = 0;
    s->o = 0;
    t->o = 0;
       p = 0;
    s->p = 0;
    t->p = 0;
}

00bC.c (1,161 bytes) 2012-03-13 13:37

ftest.c (698 bytes) 2012-03-13 13:37

/*@ axiomatic a1 {
    axiom a2:
    \forall int* s; \forall integer x,y;
	(int)(&s[x]) == (int)(&s[y]) ==> x == y;
    }
*/

struct _str {
    int    a;
    char   b;
    short  c;
    int    d;
    double e;
    char   f;
    short  g;
    int    h;
    double i;
    char   j;
    short  k;
    int    l;
    double m;
    char   n;
    short  o;
    int    p;
};

/*@ 
    requires \valid(s);
    ensures s->a == 0;
*/
void ftest(struct _str *s) {
    s->a = 0;
    s->b = '\0';
    s->c = 0;
    s->d = 0;
    s->e = 0.0;
    s->f = '\0';
    s->g = 0;
    s->h = 0;
    s->i = 0.0;
    s->j = '\0';
    s->k = 0;
    s->l = 0;
    s->m = 0.0;
    s->n = '\0';
    s->o = 0;
    s->p = 0;
}

ftest.c (698 bytes) 2012-03-13 13:37

Relationships

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

Notes

Date Modified	Username	Field	Change
Issue History
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

Issue History