From 3acdb52dd6e07f345dbce21ad8cac826b310580d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 19 Feb 2021 10:34:34 +0000 Subject: [PATCH] Perform pointer validity checks when doing pointer arithmetic Arithmetic over pointers requires that they point to valid objects (or one past the end of an object). The test uncovered two further problems: 1) there was a typo in subtraction handling in bv_pointerst; 2) redundant assertions are removed, even when they refer to different expressions. Fixes: #5426 --- regression/cbmc/pointer-overflow1/main.c | 4 ++-- regression/cbmc/pointer-overflow1/test.desc | 9 ++++++--- regression/cbmc/pointer-overflow2/main.c | 5 +++-- regression/cbmc/pointer-overflow3/main.c | 13 +++++++++++++ regression/cbmc/pointer-overflow3/test.desc | 16 ++++++++++++++++ src/analyses/goto_check.cpp | 21 ++++++++++++++++++++- src/solvers/flattening/bv_pointers.cpp | 2 +- 7 files changed, 61 insertions(+), 9 deletions(-) create mode 100644 regression/cbmc/pointer-overflow3/main.c create mode 100644 regression/cbmc/pointer-overflow3/test.desc diff --git a/regression/cbmc/pointer-overflow1/main.c b/regression/cbmc/pointer-overflow1/main.c index eecb5222a40..062a1819ec5 100644 --- a/regression/cbmc/pointer-overflow1/main.c +++ b/regression/cbmc/pointer-overflow1/main.c @@ -11,8 +11,8 @@ int main() p2 = p - other1; p2 = p - other2 - other1; - p2 = p + sizeof(int); - p2 = p + sizeof(int) + sizeof(int); + p2 = (char *)p + sizeof(int); + p2 = (char *)p + sizeof(int) + sizeof(int); return 0; } diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index c0f0033f690..fedee95fa1a 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/regression/cbmc/pointer-overflow1/test.desc @@ -3,9 +3,12 @@ main.c --pointer-overflow-check --unsigned-overflow-check ^EXIT=10$ ^SIGNAL=0$ -^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS +^\[main\.overflow\.\d+\] line 8 (pointer )?arithmetic overflow on .*: FAILURE +^\[main\.overflow\.\d+\] line 9 (pointer )?arithmetic overflow on .*: FAILURE +^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE +^\[main\.overflow\.\d+\] line 11 (pointer )?arithmetic overflow on .*: FAILURE +^\[main\.overflow\.\d+\] line 12 (pointer )?arithmetic overflow on .*: FAILURE ^VERIFICATION FAILED$ -^\*\* 8 of 13 failed -- -^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE +^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE ^warning: ignoring diff --git a/regression/cbmc/pointer-overflow2/main.c b/regression/cbmc/pointer-overflow2/main.c index e73ba1eb115..442e002ae79 100644 --- a/regression/cbmc/pointer-overflow2/main.c +++ b/regression/cbmc/pointer-overflow2/main.c @@ -2,9 +2,10 @@ void main() { + __CPROVER_allocated_memory(9, sizeof(char)); char *p = (char *)10; p -= 1; p += 1; - p += -1; // spurious pointer overflow report - p -= -1; // spurious pointer overflow report + p += -1; // previously: spurious pointer overflow report + p -= -1; // previously: spurious pointer overflow report } diff --git a/regression/cbmc/pointer-overflow3/main.c b/regression/cbmc/pointer-overflow3/main.c new file mode 100644 index 00000000000..a3a8c803f69 --- /dev/null +++ b/regression/cbmc/pointer-overflow3/main.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int *p = malloc(sizeof(int) * 5); + int *p2 = p + 10; // undefined behavior for indexing out of bounds + int *p3 = p - 10; // undefined behavior for indexing out of bounds + + int arr[5]; + int *p4 = arr + 10; // undefined behavior for indexing out of bounds + int *p5 = arr - 10; // undefined behavior for indexing out of bounds + return 0; +} diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc new file mode 100644 index 00000000000..7a98821d501 --- /dev/null +++ b/regression/cbmc/pointer-overflow3/test.desc @@ -0,0 +1,16 @@ +CORE broken-smt-backend +main.c +--pointer-overflow-check --no-simplify +^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE +^\*\* 4 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +Invariant check failed +-- +Uses --no-simplify to avoid removing repeated ASSERT FALSE statements. diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 594fab39fc6..76ffb0505f1 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -286,8 +286,12 @@ class goto_checkt void goto_checkt::collect_allocations( const goto_functionst &goto_functions) { - if(!enable_pointer_check && !enable_bounds_check) + if( + !enable_pointer_check && !enable_bounds_check && + !enable_pointer_overflow_check) + { return; + } for(const auto &gf_entry : goto_functions.function_map) { @@ -1172,6 +1176,21 @@ void goto_checkt::pointer_overflow_check( expr.find_source_location(), expr, guard); + + // the result must be within object bounds or one past the end + const auto size = from_integer(0, size_type()); + auto conditions = get_pointer_dereferenceable_conditions(expr, size); + + for(const auto &c : conditions) + { + add_guarded_property( + c.assertion, + "pointer arithmetic: " + c.description, + "pointer arithmetic", + expr.find_source_location(), + expr, + guard); + } } void goto_checkt::pointer_validity_check( diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index a841f026004..368d4e20c9f 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -506,7 +506,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) const bvt &bv = convert_bv(minus_expr.lhs()); - typet pointer_sub_type = minus_expr.rhs().type().subtype(); + typet pointer_sub_type = minus_expr.lhs().type().subtype(); mp_integer element_size; if(pointer_sub_type.id()==ID_empty)