Skip to content

Commit 61fd24d

Browse files
feliperodrifeliperodri
authored
Merge pull request #6277 from feliperodri/struct-members-history
Adds support for struct members in history variables
2 parents 25ed175 + 21622a9 commit 61fd24d

File tree

10 files changed

+195
-12
lines changed

10 files changed

+195
-12
lines changed

‎doc/cprover-manual/contracts-history-variables.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ _ensures_ clause.
1313
1414
### Parameters
1515
16-
`__CPROVER_old` takes a single argument, which is the identifier corresponding to
17-
a parameter of the function. For now, only scalar or pointer types are supported.
16+
`__CPROVER_old` takes a single argument, which is the identifier
17+
corresponding to a parameter of the function. For now, only scalars,
18+
pointers, and struct members are supported.
1819
1920
### Semantics
2021

‎regression/contracts/history-pointer-enforce-09/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <stdlib.h>
2+
3+
struct pair
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
void foo(struct pair *p) __CPROVER_assigns(p->y)
10+
__CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
11+
{
12+
p->y = p->y + 5;
13+
}
14+
15+
int main()
16+
{
17+
struct pair *p = malloc(sizeof(*p));
18+
p->x = 2;
19+
p->y = 2;
20+
foo(p);
21+
22+
return 0;
23+
}

‎regression/contracts/history-pointer-enforce-09/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
7+
^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
8+
^VERIFICATION SUCCESSFUL$
9+
--
10+
--
11+
This test checks that history variables are supported for struct members.
12+
By using the --enforce-all-contracts flag, the post-condition (which contains
13+
the history variable) is asserted. In this case, this assertion should pass.

‎regression/contracts/history-pointer-enforce-10/main.c

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
struct pair
5+
{
6+
int x;
7+
int *y;
8+
};
9+
10+
int z = 5;
11+
int w[10] = {0};
12+
13+
void foo(struct pair *p) __CPROVER_assigns(*(p->y), z)
14+
__CPROVER_ensures(*(p->y) == __CPROVER_old(*(p->y)) + __CPROVER_old(z))
15+
{
16+
*(p->y) = *(p->y) + z;
17+
z = 10;
18+
}
19+
20+
void bar(struct pair *p) __CPROVER_assigns(p->y)
21+
__CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
22+
{
23+
p->y = (p->y + 5);
24+
}
25+
26+
void baz(struct pair p) __CPROVER_assigns(p)
27+
__CPROVER_ensures(p == __CPROVER_old(p))
28+
{
29+
struct pair pp = p;
30+
struct pair empty = {0};
31+
p = empty;
32+
p = pp;
33+
}
34+
35+
int main()
36+
{
37+
struct pair *p = malloc(sizeof(*p));
38+
p->y = malloc(sizeof(*(p->y)));
39+
p->x = 2;
40+
*(p->y) = 2;
41+
foo(p);
42+
assert(*(p->y) == 7);
43+
p->y = w;
44+
w[5] = -1;
45+
bar(p);
46+
assert(*(p->y) == -1);
47+
baz(*p);
48+
49+
return 0;
50+
}

‎regression/contracts/history-pointer-enforce-10/test.desc

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
7+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
8+
^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
9+
^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
10+
^\[baz.\d+\] line \d+ Check that pp is assignable\: SUCCESS$
11+
^\[baz.\d+\] line \d+ Check that empty is assignable\: SUCCESS$
12+
^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
13+
^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
14+
^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$
15+
^\[foo.\d+\] line \d+ Check that z is assignable\: SUCCESS$
16+
^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == 7\: SUCCESS$
17+
^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == -1\: SUCCESS$
18+
^VERIFICATION SUCCESSFUL$
19+
--
20+
--
21+
This test checks that history variables are supported for structs, symbols, and
22+
struct members. By using the --enforce-all-contracts flag, the postcondition
23+
(with history variable) is asserted. In this case, this assertion should pass.

‎regression/contracts/history-pointer-enforce-11/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <stdlib.h>
2+
3+
struct pair
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
void foo(struct pair *p) __CPROVER_assigns(p->y)
10+
__CPROVER_ensures((p != NULL) == > (p->y == __CPROVER_old(p->y) + 5))
11+
__CPROVER_ensures((p == NULL) == > (p->y == __CPROVER_old(p->y)))
12+
{
13+
if(p != NULL)
14+
p->y = p->y + 5;
15+
}
16+
17+
int main()
18+
{
19+
struct pair *p = NULL;
20+
foo(p);
21+
22+
return 0;
23+
}

‎regression/contracts/history-pointer-enforce-11/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[postcondition.\d+\] Check ensures clause\: SUCCESS$
7+
^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
8+
^VERIFICATION SUCCESSFUL$
9+
--
10+
--
11+
This test checks that history variables handle NULL pointers.
12+
History variables currently do not check for nullness while
13+
storing values of objects, which may lead to NULL pointer dereferences.

‎regression/contracts/history-pointer-replace-04/main.c

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <stdlib.h>
2+
3+
struct pair
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
void foo(struct pair *p) __CPROVER_requires(p != NULL) __CPROVER_assigns(p->y)
10+
__CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
11+
{
12+
p->y = p->y + 5;
13+
}
14+
15+
int main()
16+
{
17+
struct pair *p = malloc(sizeof(*p));
18+
p->x = 2;
19+
p->y = 2;
20+
foo(p);
21+
assert(p->y != 7);
22+
23+
return 0;
24+
}

‎regression/contracts/history-pointer-replace-04/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[precondition.\d+\] file main.c line \d+ Check requires clause\: SUCCESS$
7+
^\[main.assertion.\d+\] line \d+ assertion p\-\>y \!\= 7\: FAILURE$
8+
^VERIFICATION FAILED$
9+
--
10+
--
11+
This test checks that history variables are supported for struct members.
12+
By using the --replace-all-calls-with-contracts flag, the assertion in
13+
main should consider the ensures clause (with old value). In this case,
14+
this assertion should fail.

‎src/goto-instrument/contracts/contracts.cpp

+9-10
Original file line numberDiff line numberDiff line change
@@ -394,23 +394,22 @@ void code_contractst::replace_old_parameter(
394394

395395
const auto &parameter = to_old_expr(expr).expression();
396396

397-
// TODO: generalize below
398-
if(parameter.id() == ID_dereference)
397+
if(
398+
parameter.id() == ID_dereference || parameter.id() == ID_member ||
399+
parameter.id() == ID_symbol)
399400
{
400-
const auto &dereference_expr = to_dereference_expr(parameter);
401-
402-
auto it = parameter2history.find(dereference_expr);
401+
auto it = parameter2history.find(parameter);
403402

404403
if(it == parameter2history.end())
405404
{
406405
// 1. Create a temporary symbol expression that represents the
407406
// history variable
408407
symbol_exprt tmp_symbol =
409-
new_tmp_symbol(dereference_expr.type(), location, mode).symbol_expr();
408+
new_tmp_symbol(parameter.type(), location, mode).symbol_expr();
410409

411410
// 2. Associate the above temporary variable to it's corresponding
412411
// expression
413-
parameter2history[dereference_expr] = tmp_symbol;
412+
parameter2history[parameter] = tmp_symbol;
414413

415414
// 3. Add the required instructions to the instructions list
416415
// 3.1 Declare the newly created temporary variable
@@ -419,11 +418,11 @@ void code_contractst::replace_old_parameter(
419418
// 3.2 Add an assignment such that the value pointed to by the new
420419
// temporary variable is equal to the value of the corresponding
421420
// parameter
422-
history.add(goto_programt::make_assignment(
423-
tmp_symbol, dereference_expr, location));
421+
history.add(
422+
goto_programt::make_assignment(tmp_symbol, parameter, location));
424423
}
425424

426-
expr = parameter2history[dereference_expr];
425+
expr = parameter2history[parameter];
427426
}
428427
else
429428
{

0 commit comments

Comments
 (0)