Skip to content

Commit 0f8ac07

Browse files
hannes-steffenhagen-diffbluehannes-steffenhagen-diffblue
committed
Split up pointer-primitive-checks
These were previously checking if the pointer being validated is either null or a valid pointer, because primitives like r_ok don't work on invalid pointers. However, grouping them all together like that makes it hard to see which exact condition failed. This just adds each of these checks individually instead, which is more verbose but therefore also more useful when diagnosing problems. Some of the tests are marked as broken-smt-backend because the SMT backend gives different results for these checks for some reason.
1 parent cfd387d commit 0f8ac07

File tree

4 files changed

+91
-34
lines changed

4 files changed

+91
-34
lines changed

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

Lines changed: 36 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,43 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
7-
\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OFFSET.*: FAILURE
8-
\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
9-
\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in OBJECT_SIZE.*: FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
11-
\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in W_OK.*: FAILURE
12-
\*\* 7 of \d+ failed
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 dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
10+
\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
11+
\[main.pointer_primitives.6\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
12+
\[main.pointer_primitives.7\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
13+
\[main.pointer_primitives.8\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
14+
\[main.pointer_primitives.9\] line \d+ pointer outside dynamic object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
15+
\[main.pointer_primitives.10\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
16+
\[main.pointer_primitives.11\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
17+
\[main.pointer_primitives.12\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
18+
\[main.pointer_primitives.13\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
19+
\[main.pointer_primitives.14\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
20+
\[main.pointer_primitives.15\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
21+
\[main.pointer_primitives.16\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
22+
\[main.pointer_primitives.17\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
23+
\[main.pointer_primitives.18\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
24+
\[main.pointer_primitives.19\] line \d+ pointer outside dynamic object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
25+
\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
26+
\[main.pointer_primitives.21\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
27+
\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
28+
\[main.pointer_primitives.23\] line \d+ dead object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
29+
\[main.pointer_primitives.24\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
30+
\[main.pointer_primitives.25\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
31+
\[main.pointer_primitives.26\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
32+
\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
33+
\[main.pointer_primitives.28\] line \d+ dead object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
34+
\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
35+
\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
36+
\[main.pointer_primitives.31\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
37+
\[main.pointer_primitives.32\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
38+
\[main.pointer_primitives.33\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
39+
\[main.pointer_primitives.34\] line \d+ pointer outside dynamic object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
40+
\[main.pointer_primitives.35\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
1341
--
1442
^warning: ignoring
1543
--

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

Lines changed: 38 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,45 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
7-
\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
8-
\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
9-
\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
11-
\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
12-
\[main.pointer_primitives.7\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
13-
\*\* 7 of \d+ failed
146
--
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
1545
^warning: ignoring
1646
--
1747
Verifies that the pointer primitives check fails for the various forms of

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
7-
\*\* 1 of \d+ failed
6+
\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
7+
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
8+
\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
9+
\[main.pointer_primitives.4\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
10+
\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
811
--
912
^warning: ignoring
1013
--

‎src/analyses/goto_check.cpp

Lines changed: 11 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1236,22 +1236,18 @@ void goto_checkt::pointer_primitive_check(
12361236
? from_integer(1, size_type())
12371237
: size_of_expr_opt.value();
12381238

1239-
const conditionst &conditions = get_pointer_dereferenceable_conditions(pointer, size);
1240-
1241-
exprt::operandst conjuncts;
1242-
1239+
const conditionst &conditions =
1240+
get_pointer_points_to_valid_memory_conditions(pointer, size);
12431241
for(const auto &c : conditions)
1244-
conjuncts.push_back(c.assertion);
1245-
1246-
const or_exprt or_expr(null_object(pointer), conjunction(conjuncts));
1247-
1248-
add_guarded_property(
1249-
or_expr,
1250-
"pointer in pointer primitive is neither null nor valid",
1251-
"pointer primitives",
1252-
expr.source_location(),
1253-
expr,
1254-
guard);
1242+
{
1243+
add_guarded_property(
1244+
or_exprt{null_object(pointer), c.assertion},
1245+
c.description,
1246+
"pointer primitives",
1247+
expr.source_location(),
1248+
expr,
1249+
guard);
1250+
}
12551251
}
12561252

12571253
bool goto_checkt::is_pointer_primitive(const exprt &expr)

0 commit comments

Comments
 (0)