Skip to content

Commit db48f03

Browse files
author
thk123
committed
Enable the write stack for pointers to structs
This works correctly so we don't need to cautiously throw away stacks of pointers to structs. The original concern was pointers to structs being used as pointers to the first component, but the goto program introduces a cast which means we don't create the pointer. Added a unit test to document this behavior.
1 parent 02e4655 commit db48f03

File tree

6 files changed

+104
-25
lines changed

6 files changed

+104
-25
lines changed

‎regression/goto-analyzer/sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,5 +24,30 @@ int main(int argc, char *argv[])
2424
__CPROVER_assert(p->b==2.0, "p->b==2.0");
2525
__CPROVER_assert(p->b==1.0, "p->b==1.0");
2626

27+
// pointers to components
28+
int * comp_p = &x.a;
29+
__CPROVER_assert(comp_p==&x.a, "comp_p==&x.a");
30+
__CPROVER_assert(comp_p==&x.b, "comp_p==&x.b");
31+
__CPROVER_assert(*comp_p==0, "*comp_p==0");
32+
__CPROVER_assert(*comp_p==1, "*comp_p==1");
33+
34+
float * compb_p = &x.b;
35+
__CPROVER_assert(compb_p==&x.a, "compb_p==&x.a");
36+
__CPROVER_assert(compb_p==&x.b, "compb_p==&x.b");
37+
__CPROVER_assert(*compb_p==2.0, "*compb_p==2.0");
38+
__CPROVER_assert(*compb_p==1.0, "*compb_p==1.0");
39+
40+
// Use pointer implicitly pointing at the first component
41+
int * implicit_p = &x;
42+
__CPROVER_assert(implicit_p==&x.a, "implicit_p==&x.a");
43+
__CPROVER_assert(implicit_p==&x, "implicit_p==&x");
44+
__CPROVER_assert(*implicit_p==0, "*implicit_p==0");
45+
__CPROVER_assert(*implicit_p==1, "*implicit_p==1");
46+
47+
// Write through pointer implicitly pointing at the first component
48+
*implicit_p=5;
49+
__CPROVER_assert(x.a==5, "x.a==5");
50+
__CPROVER_assert(x.a==1, "x.a==1");
51+
2752
return 0;
2853
}

‎regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc

Lines changed: 23 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,30 @@
1-
KNOWNBUG
1+
CORE
22
sensitivity_test_constants_pointer_to_constants_struct.c
33
--variable --pointers --structs --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] .* \(\*p\).a==0: Success$
7-
^\[main.assertion.2\] .* \(\*p\).a==1: Failure \(if reachable\)$
8-
^\[main.assertion.3\] .* p->a==0: Success$
9-
^\[main.assertion.4\] .* p->a==1: Failure \(if reachable\)$
10-
^\[main.assertion.5\] .* p->b==2.0: Success$
11-
^\[main.assertion.6\] .* p->b==1.0: Failure \(if reachable\)$
6+
^\[main\.assertion\.1\] .* \(\*p\).a==0: Success$
7+
^\[main\.assertion\.2\] .* \(\*p\).a==1: Failure \(if reachable\)$
8+
^\[main\.assertion\.3\] .* p->a==0: Success$
9+
^\[main\.assertion\.4\] .* p->a==1: Failure \(if reachable\)$
10+
^\[main\.assertion\.5\] .* p->b==2.0: Success$
11+
^\[main\.assertion\.6\] .* p->b==1.0: Failure \(if reachable\)$
12+
^\[main\.assertion\.9\] .* \*comp_p==0: Success$
13+
^\[main\.assertion\.10\] .* \*comp_p==1: Failure \(if reachable\)$
14+
^\[main\.assertion\.13\] .* \*compb_p==2.0: Success$
15+
^\[main\.assertion\.14\] .* \*compb_p==1.0: Failure \(if reachable\)$
16+
^\[main\.assertion\.17\] .* \*implicit_p==0: Unknown$
17+
^\[main\.assertion\.18\] .* \*implicit_p==1: Unknown$
18+
^\[main\.assertion\.19\] .* x.a==5: Unknown$
19+
^\[main\.assertion\.20\] .* x.a==1: Unknown$
1220
--
1321
^warning: ignoring
1422
--
15-
The final two assertions are the wrong way round as modifying the pointer
16-
does not seem to be propogating through. See #96
23+
The following assertions are not checked since simplify_expr doesn't handle
24+
them. See issue diffblue/cbmc-toyota#145
25+
^\[main\.assertion\.7\] .* comp_p==&x.a: Success
26+
^\[main\.assertion\.8\] .* comp_p==&x.b: Failure \(if reachable\)$
27+
^\[main\.assertion\.11\] .* compb_p==&x.a: Failure \(if reachable\)$
28+
^\[main\.assertion\.12\] .* compb_p==&x.b: Success
29+
^\[main\.assertion\.15\] .* implicit_p==&x.a: Success
30+
^\[main\.assertion\.16\] .* implicit_p==&x: Success

‎regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,19 @@ sensitivity_test_constants_pointer_to_two_value_struct.c
99
^\[main.assertion.4\] .* p->a==1: Unknown$
1010
^\[main.assertion.5\] .* p->b==2.0: Unknown$
1111
^\[main.assertion.6\] .* p->b==1.0: Unknown$
12+
\[main\.assertion\.7\] .* comp_p==&x\.a: Unknown$
13+
\[main\.assertion\.8\] .* comp_p==&x\.b: Unknown$
14+
\[main\.assertion\.9\] .* \*comp_p==0: Unknown$
15+
\[main\.assertion\.10\] .* \*comp_p==1: Unknown$
16+
\[main\.assertion\.11\] .* compb_p==&x\.a: Unknown$
17+
\[main\.assertion\.12\] .* compb_p==&x\.b: Unknown$
18+
\[main\.assertion\.13\] .* \*compb_p==2\.0: Unknown$
19+
\[main\.assertion\.14\] .* \*compb_p==1\.0: Unknown$
20+
\[main\.assertion\.15\] .* implicit_p==&x\.a: Unknown$
21+
\[main\.assertion\.16\] .* implicit_p==&x: Unknown$
22+
\[main\.assertion\.17\] .* \*implicit_p==0: Unknown$
23+
\[main\.assertion\.18\] .* \*implicit_p==1: Unknown$
24+
\[main\.assertion\.19\] .* x\.a==5: Unknown$
25+
\[main\.assertion\.20\] .* x\.a==1: Unknown$
1226
--
1327
^warning: ignoring

‎regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,18 @@ sensitivity_test_two_value_pointer_to_two_value_struct.c
99
^\[main.assertion.4\] .* p->a==1: Unknown$
1010
^\[main.assertion.5\] .* p->b==2.0: Unknown$
1111
^\[main.assertion.6\] .* p->b==1.0: Unknown$
12+
^\[main.assertion.8\] .* comp_p==&x.b: Unknown$
13+
^\[main.assertion.9\] .* \*comp_p==0: Unknown$
14+
^\[main.assertion.10\] .* \*comp_p==1: Unknown$
15+
^\[main.assertion.11\] .* compb_p==&x.a: Unknown$
16+
^\[main.assertion.12\] .* compb_p==&x.b: Unknown$
17+
^\[main.assertion.13\] .* \*compb_p==2.0: Unknown$
18+
^\[main.assertion.14\] .* \*compb_p==1.0: Unknown$
19+
^\[main.assertion.15\] .* implicit_p==&x.a: Unknown$
20+
^\[main.assertion.16\] .* implicit_p==&x: Unknown$
21+
^\[main.assertion.17\] .* \*implicit_p==0: Unknown$
22+
^\[main.assertion.18\] .* \*implicit_p==1: Unknown$
23+
^\[main.assertion.19\] .* x.a==5: Unknown$
24+
^\[main.assertion.20\] .* x.a==1: Unknown$
1225
--
1326
^warning: ignoring

‎src/analyses/variable-sensitivity/write_stack.cpp

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -60,14 +60,6 @@ void write_stackt::construct_stack_to_pointer(
6060
{
6161
PRECONDITION(expr.type().id()==ID_pointer);
6262

63-
// If we are a pointer to a struct, we do not currently support reading
64-
// writing directly to it so just create a top stack
65-
if(ns.follow(expr.type().subtype()).id()==ID_struct)
66-
{
67-
top_stack=true;
68-
return;
69-
}
70-
7163
if(expr.id()==ID_address_of)
7264
{
7365
// resovle reminder, can either be a symbol, member or index of

‎unit/analyses/variable-sensitivity/write_stack.cpp

Lines changed: 29 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -353,15 +353,29 @@ SCENARIO("Constructing write stacks",
353353
}
354354
WHEN("Constructing from &s")
355355
{
356-
// fiddly as it depends on the type to some degree
357-
// if we want to make a (struct str *) then we want to make a pointer to
358-
// &s
359-
// If it is a pointer to the type of the first component then we really
360-
// want &(s.comp)
361-
// for now we just reject and create a junk stack
362356
exprt in_expr=to_expr("&s", ns);
363357
CAPTURE(expr2c(in_expr, ns));
364358

359+
THEN("Then should get a write stack representing &s")
360+
{
361+
auto stack=write_stackt(in_expr, environment, ns);
362+
REQUIRE_FALSE(stack.is_top_value());
363+
const exprt &out_expr=stack.to_expression();
364+
365+
CAPTURE(expr2c(out_expr, ns));
366+
367+
REQUIRE(out_expr.id()==ID_address_of);
368+
const exprt &object=out_expr.op0();
369+
require_exprt::require_symbol(object, "s");
370+
}
371+
}
372+
WHEN("Constructing from (int *)&s")
373+
{
374+
// TODO: we could in theory analyse the struct and offset the pointer
375+
// but not yet
376+
exprt in_expr=to_expr("(int *)&s", ns);
377+
CAPTURE(expr2c(in_expr, ns));
378+
365379
THEN("Then should get a top stack")
366380
{
367381
auto stack=write_stackt(in_expr, environment, ns);
@@ -419,9 +433,16 @@ SCENARIO("Constructing write stacks",
419433

420434
THEN("The constructed stack should be TOP")
421435
{
422-
// Since we don't allow constructing a pointer to a struct yet
423436
auto stack=write_stackt(in_expr, environment, ns);
424-
REQUIRE(stack.is_top_value());
437+
REQUIRE_FALSE(stack.is_top_value());
438+
const exprt &out_expr=stack.to_expression();
439+
440+
CAPTURE(expr2c(out_expr, ns));
441+
442+
REQUIRE(out_expr.id()==ID_address_of);
443+
const exprt &object=out_expr.op0();
444+
const index_exprt &index_expr=require_exprt::require_index(object, 1);
445+
require_exprt::require_symbol(index_expr.array(), "arr_s");
425446
}
426447
}
427448
GIVEN("A symbol int x")

0 commit comments

Comments
 (0)