From e05d8139363442ab0d81bd294608ab94ece15e09 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 26 Feb 2020 13:15:55 +0000 Subject: [PATCH] Change goto_checkt::address_check() dynamic memory bounds checking This changes the dynamic memory bounds checking predicate in address_check(). It now uses OBJECT_SIZE() instead of the variables __CPROVER_malloc_size and __CPROVER_malloc_object that are set in the malloc() model. This also means that the predicates __CPROVER_r_ok()/__CPROVER_w_ok() will be more precise. In the previous approach, the following assertion could not be proven for example: void main() { char *c = malloc(1); assert(!__CPROVER_r_ok(c, 2)); } --- regression/cbmc/r_w_ok5/main.c | 17 +++++++++++++++++ regression/cbmc/r_w_ok5/test.desc | 15 +++++++++++++++ regression/cbmc/r_w_ok6/main.c | 26 ++++++++++++++++++++++++++ regression/cbmc/r_w_ok6/test.desc | 16 ++++++++++++++++ regression/cbmc/r_w_ok7/main.c | 18 ++++++++++++++++++ regression/cbmc/r_w_ok7/test.desc | 12 ++++++++++++ regression/cbmc/r_w_ok8/main.c | 10 ++++++++++ regression/cbmc/r_w_ok8/test.desc | 16 ++++++++++++++++ src/analyses/goto_check.cpp | 8 ++++---- 9 files changed, 134 insertions(+), 4 deletions(-) create mode 100644 regression/cbmc/r_w_ok5/main.c create mode 100644 regression/cbmc/r_w_ok5/test.desc create mode 100644 regression/cbmc/r_w_ok6/main.c create mode 100644 regression/cbmc/r_w_ok6/test.desc create mode 100644 regression/cbmc/r_w_ok7/main.c create mode 100644 regression/cbmc/r_w_ok7/test.desc create mode 100644 regression/cbmc/r_w_ok8/main.c create mode 100644 regression/cbmc/r_w_ok8/test.desc diff --git a/regression/cbmc/r_w_ok5/main.c b/regression/cbmc/r_w_ok5/main.c new file mode 100644 index 00000000000..1b4884e09bb --- /dev/null +++ b/regression/cbmc/r_w_ok5/main.c @@ -0,0 +1,17 @@ +#include +#include + +void main() +{ + char c[2]; + assert(__CPROVER_r_ok(c, 2)); + assert(!__CPROVER_r_ok(c, 2)); + assert(__CPROVER_r_ok(c, 3)); + assert(!__CPROVER_r_ok(c, 3)); + + char *p = malloc(2); + assert(__CPROVER_r_ok(c, 2)); + assert(!__CPROVER_r_ok(c, 2)); + assert(__CPROVER_r_ok(p, 3)); + assert(!__CPROVER_r_ok(p, 3)); +} diff --git a/regression/cbmc/r_w_ok5/test.desc b/regression/cbmc/r_w_ok5/test.desc new file mode 100644 index 00000000000..a39b6d1bf4b --- /dev/null +++ b/regression/cbmc/r_w_ok5/test.desc @@ -0,0 +1,15 @@ +CORE +main.c + +\[main.assertion.1\] .*: SUCCESS +\[main.assertion.2\] .*: FAILURE +\[main.assertion.3\] .*: FAILURE +\[main.assertion.4\] .*: SUCCESS +\[main.assertion.5\] .*: SUCCESS +\[main.assertion.6\] .*: FAILURE +\[main.assertion.7\] .*: FAILURE +\[main.assertion.8\] .*: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc/r_w_ok6/main.c b/regression/cbmc/r_w_ok6/main.c new file mode 100644 index 00000000000..a1c2855f011 --- /dev/null +++ b/regression/cbmc/r_w_ok6/main.c @@ -0,0 +1,26 @@ +#include +#include + +void main() +{ + char *p; + int choice; + + if(choice) + { + p = malloc(2); + } + else + { + p = malloc(3); + } + + assert(__CPROVER_r_ok(p, 2)); + assert(!__CPROVER_r_ok(p, 2)); + + assert(__CPROVER_r_ok(p, 3)); + assert(!__CPROVER_r_ok(p, 3)); + + assert(__CPROVER_r_ok(p, 4)); + assert(!__CPROVER_r_ok(p, 4)); +} diff --git a/regression/cbmc/r_w_ok6/test.desc b/regression/cbmc/r_w_ok6/test.desc new file mode 100644 index 00000000000..0dd6251c978 --- /dev/null +++ b/regression/cbmc/r_w_ok6/test.desc @@ -0,0 +1,16 @@ +CORE broken-smt-backend +main.c + +\[main.assertion.1\] .*: SUCCESS +\[main.assertion.2\] .*: FAILURE +\[main.assertion.3\] .*: FAILURE +\[main.assertion.4\] .*: FAILURE +\[main.assertion.5\] .*: FAILURE +\[main.assertion.6\] .*: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test checks that __CPROVER_r_ok() gives the correct result when the given +pointer can point to different memory segments of different sizes diff --git a/regression/cbmc/r_w_ok7/main.c b/regression/cbmc/r_w_ok7/main.c new file mode 100644 index 00000000000..96e53444967 --- /dev/null +++ b/regression/cbmc/r_w_ok7/main.c @@ -0,0 +1,18 @@ +#include +#include +#include + +int main() +{ + size_t x; + size_t y; + uint8_t *a; + + __CPROVER_assume(x > 0); + __CPROVER_assume(y > x); + + a = malloc(sizeof(uint8_t) * x); + + assert(__CPROVER_w_ok(a, x)); + assert(!__CPROVER_w_ok(a, y)); +} diff --git a/regression/cbmc/r_w_ok7/test.desc b/regression/cbmc/r_w_ok7/test.desc new file mode 100644 index 00000000000..a5d7e85c7dc --- /dev/null +++ b/regression/cbmc/r_w_ok7/test.desc @@ -0,0 +1,12 @@ +CORE +main.c + +\[main.assertion.1\] .*: SUCCESS +\[main.assertion.2\] .*: SUCCESS +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test checks that __CPROVER_r_ok() works with nondet sizes diff --git a/regression/cbmc/r_w_ok8/main.c b/regression/cbmc/r_w_ok8/main.c new file mode 100644 index 00000000000..2f9052d2b44 --- /dev/null +++ b/regression/cbmc/r_w_ok8/main.c @@ -0,0 +1,10 @@ +#include +#include + +int main() +{ + int *x = malloc(2); + int *y = malloc(2); + assert(!__CPROVER_r_ok(x, 3)); + assert(__CPROVER_r_ok(x, 3) == __CPROVER_r_ok(y, 3)); +} diff --git a/regression/cbmc/r_w_ok8/test.desc b/regression/cbmc/r_w_ok8/test.desc new file mode 100644 index 00000000000..4102d81cb91 --- /dev/null +++ b/regression/cbmc/r_w_ok8/test.desc @@ -0,0 +1,16 @@ +CORE +main.c + +\[main.assertion.1\] .*: SUCCESS +\[main.assertion.2\] .*: SUCCESS +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test checks that two usages of the primitive __CPROVER_r_ok() can be false +simultaneously in the encoding of the program. Previously, at most one call +could be false at a time. This was imprecise, however, it was sufficient to +guarantee soundness when the __CPROVER_r_ok() primitive was used directly in an +assertion (i.e., as assert(__CPROVER_r_ok(p, size)). See issue #5194. diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index df62b9a7a53..4fff0ca80dd 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1249,15 +1249,15 @@ goto_checkt::address_check(const exprt &address, const exprt &size) if(flags.is_unknown() || flags.is_dynamic_heap()) { - const or_exprt dynamic_bounds_violation( - dynamic_object_lower_bound(address, nil_exprt()), - dynamic_object_upper_bound(address, ns, size)); + const or_exprt object_bounds_violation( + object_lower_bound(address, nil_exprt()), + object_upper_bound(address, size)); conditions.push_back(conditiont( or_exprt( in_bounds_of_some_explicit_allocation, implies_exprt( - malloc_object(address, ns), not_exprt(dynamic_bounds_violation))), + dynamic_object(address), not_exprt(object_bounds_violation))), "pointer outside dynamic object bounds")); }