diff --git a/doc/architectural/memory-primitives.md b/doc/architectural/memory-primitives.md index 7ce7dbcf3d8..8b20f18ceb0 100644 --- a/doc/architectural/memory-primitives.md +++ b/doc/architectural/memory-primitives.md @@ -199,17 +199,21 @@ CBMC has the option `--pointer-primitive-check` to detect potential misuses of the memory primitives. It checks that the pointers that appear in the following primitives are either null or valid: -- `__CPROVER_POINTER_OBJECT` -- `__CPROVER_POINTER_OFFSET` -- `__CPROVER_same_object` - `__CPROVER_OBJECT_SIZE` - `__CPROVER_DYNAMIC_OBJECT` - `__CPROVER_r_ok` - `__CPROVER_w_ok` -While the first three primitives have well-defined semantics even on invalid -pointers, using them on invalid pointers is usually unintended in user programs. -Thus, they have been included in the `--pointer-primitive-check` option. +The following three primitives have well-defined semantics even on invalid +pointers. Thus, they have been excluded from the `--pointer-primitive-check` +option. + +- `__CPROVER_POINTER_OBJECT` +- `__CPROVER_POINTER_OFFSET` +- `__CPROVER_same_object` + +Using them on invalid pointers, however, may still be unintended in user +programs. 1 Pointers with negative offsets never point to memory objects. Negative values are used internally to detect pointer underflows. diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index c1130edfcff..112f69b7437 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -3,35 +3,36 @@ main.c --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -\[main.pointer_primitives.1\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE -\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS -\[main.pointer_primitives.3\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS -\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE -\[main.pointer_primitives.5\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE -\[main.pointer_primitives.6\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS -\[main.pointer_primitives.7\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS -\[main.pointer_primitives.8\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE -\[main.pointer_primitives.9\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE -\[main.pointer_primitives.10\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS -\[main.pointer_primitives.11\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS -\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE -\[main.pointer_primitives.13\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE -\[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS -\[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS -\[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE -\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE -\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS -\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS -\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE -\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE -\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS -\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS -\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE -\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE -\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS -\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS -\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE +\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS +\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE -- ^warning: ignoring +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE +\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS +\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE -- -Verifies that checks are added for all pointer primitives +Verifies that checks are added for exactly those pointer primitives that are not +universally well defined. diff --git a/regression/cbmc/pointer-primitive-check-02/main.c b/regression/cbmc/pointer-primitive-check-02/main.c index dfe35182bed..abd0c7415dc 100644 --- a/regression/cbmc/pointer-primitive-check-02/main.c +++ b/regression/cbmc/pointer-primitive-check-02/main.c @@ -4,8 +4,8 @@ char *p1; void main() { - __CPROVER_POINTER_OBJECT(p1); + __CPROVER_r_ok(p1, 1); char *p2 = NULL; - __CPROVER_POINTER_OBJECT(p2); + __CPROVER_r_ok(p2, 1); } diff --git a/regression/cbmc/pointer-primitive-check-03/main.c b/regression/cbmc/pointer-primitive-check-03/main.c index 54d135047da..0e7744e3182 100644 --- a/regression/cbmc/pointer-primitive-check-03/main.c +++ b/regression/cbmc/pointer-primitive-check-03/main.c @@ -4,25 +4,25 @@ void main() { // uninitialized pointer char *p1; - __CPROVER_POINTER_OBJECT(p1); + __CPROVER_r_ok(p1, 1); // special value of invalid pointer char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8); - __CPROVER_POINTER_OBJECT(p2); + __CPROVER_r_ok(p2, 1); // pointer object 123, offset 123, not pointing to valid memory char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123; - __CPROVER_POINTER_OBJECT(p3); + __CPROVER_r_ok(p3, 1); // negative offset char *p4 = malloc(1); p4 -= 1; - __CPROVER_POINTER_OBJECT(p4); + __CPROVER_r_ok(p4, 1); // offset out of bounds char *p5 = malloc(10); p5 += 10; - __CPROVER_POINTER_OBJECT(p5); + __CPROVER_r_ok(p5, 1); // dead char *p6; @@ -30,11 +30,11 @@ void main() char c; p6 = &c; } - __CPROVER_POINTER_OBJECT(p6); + __CPROVER_r_ok(p6, 1); *p6; // deallocated char *p7 = malloc(1); free(p7); - __CPROVER_POINTER_OBJECT(p7); + __CPROVER_r_ok(p7, 1); } diff --git a/regression/cbmc/pointer-primitive-check-03/test.desc b/regression/cbmc/pointer-primitive-check-03/test.desc index 6326d737232..4d529706266 100644 --- a/regression/cbmc/pointer-primitive-check-03/test.desc +++ b/regression/cbmc/pointer-primitive-check-03/test.desc @@ -3,45 +3,14 @@ main.c --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ +^\[main.pointer_primitives.\d+\] line 7 .* in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 11 .* in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 15 .* in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 20 .* in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 25 .* in R_OK\(p5, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 33 .* in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 39 .* in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$ -- -\[main.pointer_primitives.1\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p1): SUCCESS -\[main.pointer_primitives.2\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p1): FAILURE -\[main.pointer_primitives.3\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p1): SUCCESS -\[main.pointer_primitives.4\] line \d+ dead object in POINTER_OBJECT((const void \*)p1): SUCCESS -\[main.pointer_primitives.5\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p1): FAILURE -\[main.pointer_primitives.6\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p1): FAILURE -\[main.pointer_primitives.7\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p2): SUCCESS -\[main.pointer_primitives.8\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p2): FAILURE -\[main.pointer_primitives.9\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p2): SUCCESS -\[main.pointer_primitives.10\] line \d+ dead object in POINTER_OBJECT((const void \*)p2): SUCCESS -\[main.pointer_primitives.11\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p2): SUCCESS -\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p2): FAILURE -\[main.pointer_primitives.13\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p3): SUCCESS -\[main.pointer_primitives.14\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p3): SUCCESS -\[main.pointer_primitives.15\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p3): SUCCESS -\[main.pointer_primitives.16\] line \d+ dead object in POINTER_OBJECT((const void \*)p3): SUCCESS -\[main.pointer_primitives.17\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p3): FAILURE -\[main.pointer_primitives.18\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p3): FAILURE -\[main.pointer_primitives.19\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p4): SUCCESS -\[main.pointer_primitives.20\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p4): SUCCESS -\[main.pointer_primitives.21\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p4): SUCCESS -\[main.pointer_primitives.22\] line \d+ dead object in POINTER_OBJECT((const void \*)p4): SUCCESS -\[main.pointer_primitives.23\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p4): FAILURE -\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p4): SUCCESS -\[main.pointer_primitives.25\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p5): SUCCESS -\[main.pointer_primitives.26\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p5): SUCCESS -\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p5): SUCCESS -\[main.pointer_primitives.28\] line \d+ dead object in POINTER_OBJECT((const void \*)p5): SUCCESS -\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p5): FAILURE -\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p5): SUCCESS -\[main.pointer_primitives.31\] line \d+ dead object in POINTER_OBJECT((const void \*)p6): FAILURE -\[main.pointer_primitives.32\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p6): SUCCESS -\[main.pointer_primitives.33\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p7): SUCCESS -\[main.pointer_primitives.34\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p7): SUCCESS -\[main.pointer_primitives.35\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p7): FAILURE -\[main.pointer_primitives.36\] line \d+ dead object in POINTER_OBJECT((const void \*)p7): SUCCESS -\[main.pointer_primitives.37\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS -\[main.pointer_primitives.38\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS ^warning: ignoring -- Verifies that the pointer primitives check fails for the various forms of diff --git a/regression/cbmc/pragma_cprover3/main.c b/regression/cbmc/pragma_cprover3/main.c index f4dab2f722c..462fb376db2 100644 --- a/regression/cbmc/pragma_cprover3/main.c +++ b/regression/cbmc/pragma_cprover3/main.c @@ -8,13 +8,19 @@ int main() #pragma CPROVER check push #pragma CPROVER check disable "pointer-primitive" // do not generate checks for the following statements - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(p, sizeof(*p) + 2)) { } #pragma CPROVER check pop - // generate check and fail on the following statements + // no checks are generated for the following statement as the behaviour is + // always defined if(__CPROVER_same_object(p, q)) { } + + // generate check and fail on the following statements + if(__CPROVER_r_ok(q, 1)) + { + } } diff --git a/regression/cbmc/pragma_cprover3/test.desc b/regression/cbmc/pragma_cprover3/test.desc index a6ef5f1dbb8..c7e1faaa966 100644 --- a/regression/cbmc/pragma_cprover3/test.desc +++ b/regression/cbmc/pragma_cprover3/test.desc @@ -2,15 +2,12 @@ CORE main.c --pointer-primitive-check ^main.c function main$ -^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- +^\[main.pointer_primitives.\d+\] line 11 +^\[main.pointer_primitives.\d+\] line 18 +-- diff --git a/regression/cbmc/pragma_cprover_enable3/main.c b/regression/cbmc/pragma_cprover_enable3/main.c index b58963e731c..69cc46779a4 100644 --- a/regression/cbmc/pragma_cprover_enable3/main.c +++ b/regression/cbmc/pragma_cprover_enable3/main.c @@ -1,20 +1,17 @@ -#include - int main() { - char *p = malloc(sizeof(*p)); - char *q; + char *p, *q; #pragma CPROVER check push #pragma CPROVER check enable "pointer-primitive" // generate checks for the following statements and fail - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(p, 1)) { } #pragma CPROVER check pop // but do not generate checks on the following statements - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(q, 1)) { } } diff --git a/regression/cbmc/pragma_cprover_enable3/test.desc b/regression/cbmc/pragma_cprover_enable3/test.desc index 32e6a926064..951dc2c266d 100644 --- a/regression/cbmc/pragma_cprover_enable3/test.desc +++ b/regression/cbmc/pragma_cprover_enable3/test.desc @@ -2,17 +2,11 @@ CORE main.c ^main.c function main$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- -^\[main.pointer_primitives.\d+\] line 17 +^\[main.pointer_primitives.\d+\] line 14 -- diff --git a/regression/cbmc/pragma_cprover_enable_all/main.c b/regression/cbmc/pragma_cprover_enable_all/main.c index 626f6388a01..329b30f3a53 100644 --- a/regression/cbmc/pragma_cprover_enable_all/main.c +++ b/regression/cbmc/pragma_cprover_enable_all/main.c @@ -34,10 +34,10 @@ int main() float x; float y; ABC e; - bool same; + bool readable; char i; signed int j; - same = __CPROVER_same_object(p, q); + readable = __CPROVER_r_ok(q, 1); q = p + 2000000000000; q = r; if(nondet_bool()) @@ -71,10 +71,10 @@ int main() float x; float y; ABC e; - bool same; + bool readable; char i; signed int j; - same = __CPROVER_same_object(p, q); + readable = __CPROVER_r_ok(q, 1); q = p + 2000000000000; q = r; if(nondet_bool()) diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc index ae18f942e09..510113a342c 100644 --- a/regression/cbmc/pragma_cprover_enable_all/test.desc +++ b/regression/cbmc/pragma_cprover_enable_all/test.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend main.c --object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check -^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE -^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE +^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE ^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE ^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE @@ -14,8 +14,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ -- -^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in POINTER_OBJECT\(const void \*\)q\): FAILURE -^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in POINTER_OBJECT\(const void \*\)q\): FAILURE +^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE ^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE ^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE @@ -24,4 +24,4 @@ main.c ^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE ^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE -- -This test uses all possible named-checks to maximize coverage. \ No newline at end of file +This test uses all possible named-checks to maximize coverage. diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c index 31c7360121e..1e8a2a13077 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/main.c @@ -1,41 +1,38 @@ -#include - int main() { - char *p = malloc(sizeof(*p)); - char *q; + char *p, *q, *r, *s, *t, *v; #pragma CPROVER check push #pragma CPROVER check enable "pointer-primitive" // must generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(p, 1)) { } #pragma CPROVER check push #pragma CPROVER check disable "pointer-primitive" // must not generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(q, 1)) { } #pragma CPROVER check push #pragma CPROVER check enable "pointer-primitive" // must generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(r, 1)) { } #pragma CPROVER check pop // must not generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(s, 1)) { } #pragma CPROVER check pop // must generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(t, 1)) { } #pragma CPROVER check pop // must not generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(v, 1)) { } return 0; diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc index d438774aaa4..c9e8430a6b4 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc @@ -2,35 +2,17 @@ CORE main.c ^main.c function main$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- -^\[main.pointer_primitives.\d+\] line 17 -^\[main.pointer_primitives.\d+\] line 28 -^\[main.pointer_primitives.\d+\] line 38 +^\[main.pointer_primitives.\d+\] line 14 +^\[main.pointer_primitives.\d+\] line 25 +^\[main.pointer_primitives.\d+\] line 35 -- diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c index c4ad7887ccb..e78426c471c 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/main.c @@ -1,41 +1,38 @@ -#include - int main() { - char *p = malloc(sizeof(*p)); - char *q; + char *p, *q, *r, *s, *t, *v; #pragma CPROVER check push #pragma CPROVER check enable "pointer-primitive" // must generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(p, 1)) { } #pragma CPROVER check push #pragma CPROVER check disable "pointer-primitive" // must not generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(q, 1)) { } #pragma CPROVER check push #pragma CPROVER check enable "pointer-primitive" // must generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(r, 1)) { } #pragma CPROVER check pop // must not generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(s, 1)) { } #pragma CPROVER check pop // must generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(t, 1)) { } #pragma CPROVER check pop // must generate generate checks - if(__CPROVER_same_object(p, q)) + if(__CPROVER_r_ok(v, 1)) { } return 0; diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc index ccc772d828e..9e72ed21ec6 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc @@ -2,42 +2,18 @@ CORE main.c --pointer-primitive-check ^main.c function main$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 23 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 33 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 33 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ -^\[main.pointer_primitives.\d+\] line 38 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$ -^\[main.pointer_primitives.\d+\] line 38 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 35 pointer invalid in R_OK\(v, \(unsigned (long (long )?)?int\)1\): FAILURE$ +^\[main.pointer_primitives.\d+\] line 35 pointer outside object bounds in R_OK\(v, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ -- -^\[main.pointer_primitives.\d+\] line 17 -^\[main.pointer_primitives.\d+\] line 28 +^\[main.pointer_primitives.\d+\] line 14 +^\[main.pointer_primitives.\d+\] line 25 -- diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index 522dc53dac8..b95872368b3 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -206,12 +206,13 @@ class goto_check_ct /// \param guard: the condition under which the operation happens void pointer_primitive_check(const exprt &expr, const guardt &guard); - /// Returns true if the given expression is a pointer primitive such as - /// __CPROVER_r_ok() + /// Returns true if the given expression is a pointer primitive + /// that requires validation of the operand to guard against misuse /// /// \param expr expression - /// \return true if the given expression is a pointer primitive - bool is_pointer_primitive(const exprt &expr); + /// \return true if the given expression is a pointer primitive that requires + /// checking + bool requires_pointer_primitive_check(const exprt &expr); optionalt get_pointer_is_null_condition(const exprt &address, const exprt &size); @@ -1354,13 +1355,19 @@ void goto_check_ct::pointer_primitive_check( } } -bool goto_check_ct::is_pointer_primitive(const exprt &expr) +bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr) { // we don't need to include the __CPROVER_same_object primitive here as it // is replaced by lower level primitives in the special function handling // during typechecking (see c_typecheck_expr.cpp) - return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset || - expr.id() == ID_object_size || expr.id() == ID_r_ok || + + // pointer_object and pointer_offset are well-defined for an arbitrary + // pointer-typed operand (and the operands themselves have been checked + // separately for, e.g., invalid pointer dereferencing via check_rec): + // pointer_object and pointer_offset just extract a subset of bits from the + // pointer. If that pointer was unconstrained (non-deterministic), the result + // will equally be non-deterministic. + return expr.id() == ID_object_size || expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok || expr.id() == ID_is_dynamic_object; } @@ -1835,7 +1842,7 @@ void goto_check_ct::check_rec(const exprt &expr, guardt &guard) { pointer_validity_check(to_dereference_expr(expr), expr, guard); } - else if(is_pointer_primitive(expr)) + else if(requires_pointer_primitive_check(expr)) { pointer_primitive_check(expr, guard); }