Skip to content

Commit 1f2a160

Browse files
tautschnigtautschnig
committed
Make pointer-primitive-check a no-op when behaviour is always defined
pointer_object, pointer_offset have well-defined behaviour even when the input is an unconstrained pointer: the result is equally unconstrained. Regression tests are updated to reflect the reduced number of checks generated by --pointer-primitive-check. Note that the patterns in pointer-primitive-check-03 never were effective as they were placed in the patterns-not-to-seen section of test.desc while also missing proper parenthesis escaping (making the patterns trivially non-matching).
1 parent 7eceeb5 commit 1f2a160

File tree

7 files changed

+74
-94
lines changed

7 files changed

+74
-94
lines changed

‎regression/cbmc/pointer-primitive-check-01/test.desc

Lines changed: 30 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -3,35 +3,36 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
7-
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
8-
\[main.pointer_primitives.3\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
9-
\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
11-
\[main.pointer_primitives.6\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
12-
\[main.pointer_primitives.7\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
13-
\[main.pointer_primitives.8\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
14-
\[main.pointer_primitives.9\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
15-
\[main.pointer_primitives.10\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
16-
\[main.pointer_primitives.11\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
17-
\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
18-
\[main.pointer_primitives.13\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
19-
\[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
20-
\[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
21-
\[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
22-
\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
23-
\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
24-
\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
25-
\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
26-
\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
27-
\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
28-
\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
29-
\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
30-
\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
31-
\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
32-
\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
33-
\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
6+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
7+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
8+
\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
9+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
10+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
11+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
12+
\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
13+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
3414
--
3515
^warning: ignoring
16+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
17+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
18+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
19+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
20+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
21+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
22+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
23+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
24+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
25+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
26+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
27+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
28+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
29+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
30+
\[main.pointer_primitives\.\d+\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
31+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
32+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
33+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
34+
\[main.pointer_primitives\.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
35+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
3636
--
37-
Verifies that checks are added for all pointer primitives
37+
Verifies that checks are added for exactly those pointer primitives that are not
38+
universally well defined.

‎regression/cbmc/pointer-primitive-check-02/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ char *p1;
44

55
void main()
66
{
7-
__CPROVER_POINTER_OBJECT(p1);
7+
__CPROVER_r_ok(p1, 1);
88

99
char *p2 = NULL;
10-
__CPROVER_POINTER_OBJECT(p2);
10+
__CPROVER_r_ok(p2, 1);
1111
}

‎regression/cbmc/pointer-primitive-check-03/main.c

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,37 +4,37 @@ void main()
44
{
55
// uninitialized pointer
66
char *p1;
7-
__CPROVER_POINTER_OBJECT(p1);
7+
__CPROVER_r_ok(p1, 1);
88

99
// special value of invalid pointer
1010
char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8);
11-
__CPROVER_POINTER_OBJECT(p2);
11+
__CPROVER_r_ok(p2, 1);
1212

1313
// pointer object 123, offset 123, not pointing to valid memory
1414
char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123;
15-
__CPROVER_POINTER_OBJECT(p3);
15+
__CPROVER_r_ok(p3, 1);
1616

1717
// negative offset
1818
char *p4 = malloc(1);
1919
p4 -= 1;
20-
__CPROVER_POINTER_OBJECT(p4);
20+
__CPROVER_r_ok(p4, 1);
2121

2222
// offset out of bounds
2323
char *p5 = malloc(10);
2424
p5 += 10;
25-
__CPROVER_POINTER_OBJECT(p5);
25+
__CPROVER_r_ok(p5, 1);
2626

2727
// dead
2828
char *p6;
2929
{
3030
char c;
3131
p6 = &c;
3232
}
33-
__CPROVER_POINTER_OBJECT(p6);
33+
__CPROVER_r_ok(p6, 1);
3434
*p6;
3535

3636
// deallocated
3737
char *p7 = malloc(1);
3838
free(p7);
39-
__CPROVER_POINTER_OBJECT(p7);
39+
__CPROVER_r_ok(p7, 1);
4040
}

‎regression/cbmc/pointer-primitive-check-03/test.desc

Lines changed: 7 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -3,45 +3,14 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6+
^\[main.pointer_primitives.\d+\] line 7 .* in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
7+
^\[main.pointer_primitives.\d+\] line 11 .* in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
8+
^\[main.pointer_primitives.\d+\] line 15 .* in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$
9+
^\[main.pointer_primitives.\d+\] line 20 .* in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$
10+
^\[main.pointer_primitives.\d+\] line 25 .* in R_OK\(p5, \(unsigned (long (long )?)?int\)1\): FAILURE$
11+
^\[main.pointer_primitives.\d+\] line 33 .* in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$
12+
^\[main.pointer_primitives.\d+\] line 39 .* in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$
613
--
7-
\[main.pointer_primitives.1\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p1): SUCCESS
8-
\[main.pointer_primitives.2\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p1): FAILURE
9-
\[main.pointer_primitives.3\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p1): SUCCESS
10-
\[main.pointer_primitives.4\] line \d+ dead object in POINTER_OBJECT((const void \*)p1): SUCCESS
11-
\[main.pointer_primitives.5\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
12-
\[main.pointer_primitives.6\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
13-
\[main.pointer_primitives.7\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p2): SUCCESS
14-
\[main.pointer_primitives.8\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p2): FAILURE
15-
\[main.pointer_primitives.9\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p2): SUCCESS
16-
\[main.pointer_primitives.10\] line \d+ dead object in POINTER_OBJECT((const void \*)p2): SUCCESS
17-
\[main.pointer_primitives.11\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p2): SUCCESS
18-
\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p2): FAILURE
19-
\[main.pointer_primitives.13\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p3): SUCCESS
20-
\[main.pointer_primitives.14\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p3): SUCCESS
21-
\[main.pointer_primitives.15\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p3): SUCCESS
22-
\[main.pointer_primitives.16\] line \d+ dead object in POINTER_OBJECT((const void \*)p3): SUCCESS
23-
\[main.pointer_primitives.17\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
24-
\[main.pointer_primitives.18\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
25-
\[main.pointer_primitives.19\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p4): SUCCESS
26-
\[main.pointer_primitives.20\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p4): SUCCESS
27-
\[main.pointer_primitives.21\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p4): SUCCESS
28-
\[main.pointer_primitives.22\] line \d+ dead object in POINTER_OBJECT((const void \*)p4): SUCCESS
29-
\[main.pointer_primitives.23\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p4): FAILURE
30-
\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p4): SUCCESS
31-
\[main.pointer_primitives.25\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p5): SUCCESS
32-
\[main.pointer_primitives.26\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p5): SUCCESS
33-
\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p5): SUCCESS
34-
\[main.pointer_primitives.28\] line \d+ dead object in POINTER_OBJECT((const void \*)p5): SUCCESS
35-
\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p5): FAILURE
36-
\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p5): SUCCESS
37-
\[main.pointer_primitives.31\] line \d+ dead object in POINTER_OBJECT((const void \*)p6): FAILURE
38-
\[main.pointer_primitives.32\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p6): SUCCESS
39-
\[main.pointer_primitives.33\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p7): SUCCESS
40-
\[main.pointer_primitives.34\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p7): SUCCESS
41-
\[main.pointer_primitives.35\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p7): FAILURE
42-
\[main.pointer_primitives.36\] line \d+ dead object in POINTER_OBJECT((const void \*)p7): SUCCESS
43-
\[main.pointer_primitives.37\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
44-
\[main.pointer_primitives.38\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
4514
^warning: ignoring
4615
--
4716
Verifies that the pointer primitives check fails for the various forms of

‎regression/cbmc/pragma_cprover3/main.c

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,19 @@ int main()
88
#pragma CPROVER check push
99
#pragma CPROVER check disable "pointer-primitive"
1010
// do not generate checks for the following statements
11-
if(__CPROVER_same_object(p, q))
11+
if(__CPROVER_r_ok(p, sizeof(*p) + 2))
1212
{
1313
}
1414
#pragma CPROVER check pop
1515

16-
// generate check and fail on the following statements
16+
// no checks are generated for the following statement as the behaviour is
17+
// always defined
1718
if(__CPROVER_same_object(p, q))
1819
{
1920
}
21+
22+
// generate check and fail on the following statements
23+
if(__CPROVER_r_ok(q, 1))
24+
{
25+
}
2026
}

‎regression/cbmc/pragma_cprover3/test.desc

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,12 @@ CORE
22
main.c
33
--pointer-primitive-check
44
^main.c function main$
5-
^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
6-
^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
7-
^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
8-
^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
9-
^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
11-
^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
12-
^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
5+
^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
137
^VERIFICATION FAILED$
148
^EXIT=10$
159
^SIGNAL=0$
1610
--
11+
^\[main.pointer_primitives.\d+\] line 11
12+
^\[main.pointer_primitives.\d+\] line 18
13+
--

‎src/analyses/goto_check.cpp

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -204,12 +204,13 @@ class goto_checkt
204204
/// \param guard: the condition under which the operation happens
205205
void pointer_primitive_check(const exprt &expr, const guardt &guard);
206206

207-
/// Returns true if the given expression is a pointer primitive such as
208-
/// __CPROVER_r_ok()
207+
/// Returns true if the given expression is a pointer primitive
208+
/// that requires validation of the operand to guard against misuse
209209
///
210210
/// \param expr expression
211-
/// \return true if the given expression is a pointer primitive
212-
bool is_pointer_primitive(const exprt &expr);
211+
/// \return true if the given expression is a pointer primitive that requires
212+
/// checking
213+
bool requires_pointer_primitive_check(const exprt &expr);
213214

214215
optionalt<goto_checkt::conditiont>
215216
get_pointer_is_null_condition(const exprt &address, const exprt &size);
@@ -1314,13 +1315,19 @@ void goto_checkt::pointer_primitive_check(
13141315
}
13151316
}
13161317

1317-
bool goto_checkt::is_pointer_primitive(const exprt &expr)
1318+
bool goto_checkt::requires_pointer_primitive_check(const exprt &expr)
13181319
{
13191320
// we don't need to include the __CPROVER_same_object primitive here as it
13201321
// is replaced by lower level primitives in the special function handling
13211322
// during typechecking (see c_typecheck_expr.cpp)
1322-
return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
1323-
expr.id() == ID_object_size || expr.id() == ID_r_ok ||
1323+
1324+
// pointer_object and pointer_offset are well-defined for an arbitrary
1325+
// pointer-typed operand (and the operands themselves have been checked
1326+
// separately for, e.g., invalid pointer dereferencing via check_rec):
1327+
// pointer_object and pointer_offset just extract a subset of bits from the
1328+
// pointer. If that pointer was unconstrained (non-deterministic), the result
1329+
// will equally be non-deterministic.
1330+
return expr.id() == ID_object_size || expr.id() == ID_r_ok ||
13241331
expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
13251332
expr.id() == ID_is_dynamic_object;
13261333
}
@@ -1794,7 +1801,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
17941801
{
17951802
pointer_validity_check(to_dereference_expr(expr), expr, guard);
17961803
}
1797-
else if(is_pointer_primitive(expr))
1804+
else if(requires_pointer_primitive_check(expr))
17981805
{
17991806
pointer_primitive_check(expr, guard);
18001807
}

0 commit comments

Comments
 (0)