Skip to content

Commit 42afd18

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 c8a7e27 commit 42afd18

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
@@ -355,15 +355,29 @@ SCENARIO("Constructing write stacks",
355355
}
356356
WHEN("Constructing from &s")
357357
{
358-
// fiddly as it depends on the type to some degree
359-
// if we want to make a (struct str *) then we want to make a pointer to
360-
// &s
361-
// If it is a pointer to the type of the first component then we really
362-
// want &(s.comp)
363-
// for now we just reject and create a junk stack
364358
exprt in_expr=to_expr("&s", ns);
365359
CAPTURE(expr2c(in_expr, ns));
366360

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

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

0 commit comments

Comments
 (0)