From 0f53d144f246407bc61a78a7fcaa4c0921caf239 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 28 Oct 2016 16:15:54 +0100 Subject: [PATCH 1/3] Check static array bounds of dynamic objects Previously checking against malloc bounds and against statically-bounded arrays (e.g. int[2]) were mutually exclusive. This enables the static array bounds check even for dynamic objects. Fixes #239. --- regression/cbmc/Pointer_byte_extract5/test.desc | 4 ++-- src/analyses/goto_check.cpp | 13 ++++++++++--- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 5c5241acf14..ffd4b6e5750 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -3,7 +3,7 @@ main.c --bounds-check --32 ^EXIT=10$ ^SIGNAL=0$ -^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILURE$ -^\*\* 1 of 9 failed (2 iterations)$ +array\.List dynamic object upper bound in p->List\[2\]: FAILURE +\*\* 1 of 11 failed (2 iterations) -- ^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index aa22aa72563..a3f83a80422 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1193,6 +1193,8 @@ void goto_checkt::bounds_check( } } + exprt type_matches_size=true_exprt(); + if(ode.root_object().id()==ID_dereference) { const exprt &pointer= @@ -1218,13 +1220,18 @@ void goto_checkt::bounds_check( add_guarded_claim( precond, - name+" upper bound", + name+" dynamic object upper bound", "array bounds", expr.find_source_location(), expr, guard); - return; + exprt type_size=size_of_expr(ode.root_object().type(), ns); + if(type_size.is_not_nil()) + type_matches_size= + equal_exprt( + size, + typecast_exprt(type_size, size.type())); } const exprt &size=array_type.id()==ID_array ? @@ -1257,7 +1264,7 @@ void goto_checkt::bounds_check( inequality.op1().make_typecast(inequality.op0().type()); add_guarded_claim( - inequality, + implies_exprt(type_matches_size, inequality), name+" upper bound", "array bounds", expr.find_source_location(), From f41505b71fc63db13e206557a63dd75ee17cd553 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 1 Jan 2017 22:40:04 +0000 Subject: [PATCH 2/3] mode!=ID_java is trivially true in this branch This is part of the else { ... } in if(mode==ID_java) { ... } else { ... } --- src/analyses/goto_check.cpp | 35 ++++++++++++++++------------------- 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index a3f83a80422..2f7e4160d71 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1029,26 +1029,23 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(mode != ID_java) - { - if(flags.is_unknown() || flags.is_dynamic_heap()) - add_guarded_claim( - not_exprt(deallocated(pointer, ns)), - "dereference failure: deallocated dynamic object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); + if(flags.is_unknown() || flags.is_dynamic_heap()) + add_guarded_claim( + not_exprt(deallocated(pointer, ns)), + "dereference failure: deallocated dynamic object", + "pointer dereference", + expr.find_source_location(), + expr, + guard); - if(flags.is_unknown() || flags.is_dynamic_local()) - add_guarded_claim( - not_exprt(dead_object(pointer, ns)), - "dereference failure: dead object", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } + if(flags.is_unknown() || flags.is_dynamic_local()) + add_guarded_claim( + not_exprt(dead_object(pointer, ns)), + "dereference failure: dead object", + "pointer dereference", + expr.find_source_location(), + expr, + guard); if(enable_bounds_check) { From 867f748b13148f75f94b107ee1a741a83f46878d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 2 Jan 2017 09:56:32 +0000 Subject: [PATCH 3/3] Limit dereferencing checks to actual access size For member accesses, access to other components need not be valid as shown in the included regression test Malloc23. Also do not require --bounds-check for full dereferencing checks. Fixes #219. --- regression/cbmc/Function5/test.desc | 2 +- regression/cbmc/Malloc23/main.c | 25 +++++ regression/cbmc/Malloc23/test.desc | 12 +++ src/analyses/goto_check.cpp | 102 ++++++++++++------ .../value_set_dereference.cpp | 13 ++- src/util/pointer_predicates.cpp | 83 ++++++++++---- src/util/pointer_predicates.h | 22 +++- 7 files changed, 196 insertions(+), 63 deletions(-) create mode 100644 regression/cbmc/Malloc23/main.c create mode 100644 regression/cbmc/Malloc23/test.desc diff --git a/regression/cbmc/Function5/test.desc b/regression/cbmc/Function5/test.desc index 239e8494e54..3dada8790af 100644 --- a/regression/cbmc/Function5/test.desc +++ b/regression/cbmc/Function5/test.desc @@ -3,6 +3,6 @@ main.c --pointer-check --bounds-check ^SIGNAL=0$ ^EXIT=10$ -^\[.*\] dereference failure: object bounds in \*p: FAILURE$ +^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$ -- ^warning: ignoring diff --git a/regression/cbmc/Malloc23/main.c b/regression/cbmc/Malloc23/main.c new file mode 100644 index 00000000000..e6e192b51ba --- /dev/null +++ b/regression/cbmc/Malloc23/main.c @@ -0,0 +1,25 @@ +#include + +struct A +{ + int x; + int y; +}; + +int main() +{ + struct A *p=malloc(sizeof(int)); + p->x=0; // OK + p->y=0; // out of bounds + + struct A o=*p; // out of bounds + + int *p2=malloc(sizeof(int)); + p2[0]=0; // OK + p2[1]=0; // out of bounds + + ++p2; + p2[0]=0; // out of bounds + + return 0; +} diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc new file mode 100644 index 00000000000..6271e2d1865 --- /dev/null +++ b/regression/cbmc/Malloc23/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check +^EXIT=10$ +^SIGNAL=0$ +pointer outside dynamic object bounds in \*p: FAILURE +pointer outside dynamic object bounds in \*p: FAILURE +pointer outside dynamic object bounds in p2\[(signed long int)1\]: FAILURE +pointer outside dynamic object bounds in p2\[(signed long int)0\]: FAILURE +\*\* 4 of 36 failed (3 iterations) +-- +^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 2f7e4160d71..038e7152230 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -73,7 +74,11 @@ class goto_checkt void undefined_shift_check(const shift_exprt &expr, const guardt &guard); void pointer_rel_check(const exprt &expr, const guardt &guard); void pointer_overflow_check(const exprt &expr, const guardt &guard); - void pointer_validity_check(const dereference_exprt &expr, const guardt &guard); + void pointer_validity_check( + const dereference_exprt &expr, + const guardt &guard, + const exprt &access_lb, + const exprt &access_ub); void integer_overflow_check(const exprt &expr, const guardt &guard); void conversion_check(const exprt &expr, const guardt &guard); void float_overflow_check(const exprt &expr, const guardt &guard); @@ -966,7 +971,9 @@ Function: goto_checkt::pointer_validity_check void goto_checkt::pointer_validity_check( const dereference_exprt &expr, - const guardt &guard) + const guardt &guard, + const exprt &access_lb, + const exprt &access_ub) { if(!enable_pointer_check) return; @@ -1047,42 +1054,44 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(enable_bounds_check) + if(flags.is_unknown() || flags.is_dynamic_heap()) { - if(flags.is_unknown() || flags.is_dynamic_heap()) - { - exprt dynamic_bounds= - or_exprt(dynamic_object_lower_bound(pointer), - dynamic_object_upper_bound(pointer, dereference_type, ns)); + exprt dynamic_bounds= + or_exprt(dynamic_object_lower_bound(pointer, ns, access_lb), + dynamic_object_upper_bound( + pointer, + dereference_type, + ns, + access_ub)); - add_guarded_claim( - implies_exprt(malloc_object(pointer, ns), not_exprt(dynamic_bounds)), - "dereference failure: dynamic object bounds", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } + add_guarded_claim( + implies_exprt(malloc_object(pointer, ns), not_exprt(dynamic_bounds)), + "dereference failure: pointer outside dynamic object bounds", + "pointer dereference", + expr.find_source_location(), + expr, + guard); } - if(enable_bounds_check) + if(flags.is_unknown() || + flags.is_dynamic_local() || + flags.is_static_lifetime()) { - if(flags.is_unknown() || - flags.is_dynamic_local() || - flags.is_static_lifetime()) - { - exprt object_bounds= - or_exprt(object_lower_bound(pointer), - object_upper_bound(pointer, dereference_type, ns)); + exprt object_bounds= + or_exprt(object_lower_bound(pointer, ns, access_lb), + object_upper_bound( + pointer, + dereference_type, + ns, + access_ub)); - add_guarded_claim( - or_exprt(dynamic_object(pointer), not_exprt(object_bounds)), - "dereference failure: object bounds", - "pointer dereference", - expr.find_source_location(), - expr, - guard); - } + add_guarded_claim( + or_exprt(dynamic_object(pointer), not_exprt(object_bounds)), + "dereference failure: pointer outside object bounds", + "pointer dereference", + expr.find_source_location(), + expr, + guard); } } } @@ -1130,7 +1139,7 @@ void goto_checkt::bounds_check( typet array_type=ns.follow(expr.array().type()); if(array_type.id()==ID_pointer) - return; // done by the pointer code + throw "index got pointer as array type"; else if(array_type.id()==ID_incomplete_array) throw "index got incomplete array"; else if(array_type.id()!=ID_array && array_type.id()!=ID_vector) @@ -1434,6 +1443,27 @@ void goto_checkt::check_rec( return; } + else if(expr.id()==ID_member && + to_member_expr(expr).struct_op().id()==ID_dereference) + { + const member_exprt &member=to_member_expr(expr); + const dereference_exprt &deref= + to_dereference_expr(member.struct_op()); + + check_rec(deref.op0(), guard, false); + + exprt access_ub=nil_exprt(); + + exprt member_offset=member_offset_expr(member, ns); + exprt size=size_of_expr(expr.type(), ns); + + if(member_offset.is_not_nil() && size.is_not_nil()) + access_ub=plus_exprt(member_offset, size); + + pointer_validity_check(deref, guard, member_offset, access_ub); + + return; + } forall_operands(it, expr) check_rec(*it, guard, false); @@ -1491,7 +1521,11 @@ void goto_checkt::check_rec( expr.id()==ID_ge || expr.id()==ID_gt) pointer_rel_check(expr, guard); else if(expr.id()==ID_dereference) - pointer_validity_check(to_dereference_expr(expr), guard); + pointer_validity_check( + to_dereference_expr(expr), + guard, + nil_exprt(), + size_of_expr(expr.type(), ns)); } /*******************************************************************\ diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index c69e6feda73..c1913567448 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -425,7 +425,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // check lower bound guardt tmp_guard(guard); tmp_guard.add(is_malloc_object); - tmp_guard.add(dynamic_object_lower_bound(pointer_expr)); + tmp_guard.add( + dynamic_object_lower_bound( + pointer_expr, + ns, + nil_exprt())); dereference_callback.dereference_failure( "pointer dereference", "dynamic object lower bound", tmp_guard); @@ -439,7 +443,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( guardt tmp_guard(guard); tmp_guard.add(is_malloc_object); - tmp_guard.add(dynamic_object_upper_bound(pointer_expr, dereference_type, ns)); + tmp_guard.add( + dynamic_object_upper_bound( + pointer_expr, + dereference_type, + ns, + size_of_expr(dereference_type, ns))); dereference_callback.dereference_failure( "pointer dereference", "dynamic object upper bound", tmp_guard); diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 1e1e285e01c..dcbf813ae48 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -241,8 +241,15 @@ exprt good_pointer_def( exprt good_dynamic_tmp1= or_exprt( not_exprt(malloc_object(pointer, ns)), - and_exprt(not_exprt(dynamic_object_lower_bound(pointer)), - not_exprt(dynamic_object_upper_bound(pointer, dereference_type, ns)))); + and_exprt(not_exprt(dynamic_object_lower_bound( + pointer, + ns, + nil_exprt())), + not_exprt(dynamic_object_upper_bound( + pointer, + dereference_type, + ns, + size_of_expr(dereference_type, ns))))); exprt good_dynamic_tmp2= and_exprt(not_exprt(deallocated(pointer, ns)), @@ -259,8 +266,12 @@ exprt good_pointer_def( not_exprt(invalid_pointer(pointer)); exprt bad_other= - or_exprt(object_lower_bound(pointer), - object_upper_bound(pointer, dereference_type, ns)); + or_exprt(object_lower_bound(pointer, ns, nil_exprt()), + object_upper_bound( + pointer, + dereference_type, + ns, + size_of_expr(dereference_type, ns))); exprt good_other= or_exprt(dynamic_object(pointer), @@ -357,9 +368,12 @@ Function: dynamic_object_lower_bound \*******************************************************************/ -exprt dynamic_object_lower_bound(const exprt &pointer) +exprt dynamic_object_lower_bound( + const exprt &pointer, + const namespacet &ns, + const exprt &offset) { - return object_lower_bound(pointer); + return object_lower_bound(pointer, ns, offset); } /*******************************************************************\ @@ -377,25 +391,31 @@ Function: dynamic_object_upper_bound exprt dynamic_object_upper_bound( const exprt &pointer, const typet &dereference_type, - const namespacet &ns) + const namespacet &ns, + const exprt &access_size) { // this is - // POINTER_OFFSET(p)+size>__CPROVER_malloc_size + // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size exprt malloc_size=dynamic_size(ns); exprt object_offset=pointer_offset(pointer); - exprt size=size_of_expr(dereference_type, ns); - // need to add size - exprt sum=plus_exprt(object_offset, size); + irep_idt op=ID_ge; + exprt sum=object_offset; + + if(access_size.is_not_nil()) + { + op=ID_gt; + sum=plus_exprt(object_offset, access_size); + } if(ns.follow(sum.type())!= ns.follow(malloc_size.type())) sum.make_typecast(malloc_size.type()); - return binary_relation_exprt(sum, ID_gt, malloc_size); + return binary_relation_exprt(sum, op, malloc_size); } /*******************************************************************\ @@ -413,25 +433,32 @@ Function: object_upper_bound exprt object_upper_bound( const exprt &pointer, const typet &dereference_type, - const namespacet &ns) + const namespacet &ns, + const exprt &access_size) { // this is - // POINTER_OFFSET(p)+size>OBJECT_SIZE(pointer) + // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer) exprt object_size_expr=object_size(pointer); exprt object_offset=pointer_offset(pointer); - exprt size=size_of_expr(dereference_type, ns); - // need to add size - exprt sum=plus_exprt(object_offset, size); + irep_idt op=ID_ge; + exprt sum=object_offset; + + if(access_size.is_not_nil()) + { + op=ID_gt; + sum=plus_exprt(object_offset, access_size); + } + if(ns.follow(sum.type())!= ns.follow(object_size_expr.type())) sum.make_typecast(object_size_expr.type()); - return binary_relation_exprt(sum, ID_gt, object_size_expr); + return binary_relation_exprt(sum, op, object_size_expr); } /*******************************************************************\ @@ -446,12 +473,24 @@ Function: object_lower_bound \*******************************************************************/ -exprt object_lower_bound(const exprt &pointer) +exprt object_lower_bound( + const exprt &pointer, + const namespacet &ns, + const exprt &offset) { - exprt offset=pointer_offset(pointer); + exprt p_offset=pointer_offset(pointer); - exprt zero=from_integer(0, offset.type()); + exprt zero=from_integer(0, p_offset.type()); assert(zero.is_not_nil()); - return binary_relation_exprt(offset, ID_lt, zero); + if(offset.is_not_nil()) + { + if(ns.follow(p_offset.type())!=ns.follow(offset.type())) + p_offset= + plus_exprt(p_offset, typecast_exprt(offset, p_offset.type())); + else + p_offset=plus_exprt(p_offset, offset); + } + + return binary_relation_exprt(p_offset, ID_lt, zero); } diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index a3b88e80cc6..354c110f3e2 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -28,9 +28,23 @@ exprt null_object(const exprt &pointer); exprt null_pointer(const exprt &pointer); exprt integer_address(const exprt &pointer); exprt invalid_pointer(const exprt &pointer); -exprt dynamic_object_lower_bound(const exprt &pointer); -exprt dynamic_object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns); -exprt object_lower_bound(const exprt &pointer); -exprt object_upper_bound(const exprt &pointer, const typet &dereference_type, const namespacet &ns); +exprt dynamic_object_lower_bound( + const exprt &pointer, + const namespacet &ns, + const exprt &offset); +exprt dynamic_object_upper_bound( + const exprt &pointer, + const typet &dereference_type, + const namespacet &ns, + const exprt &access_size); +exprt object_lower_bound( + const exprt &pointer, + const namespacet &ns, + const exprt &offset); +exprt object_upper_bound( + const exprt &pointer, + const typet &dereference_type, + const namespacet &ns, + const exprt &access_size); #endif // CPROVER_UTIL_POINTER_PREDICATES_H