From 131e525b6ec185ba9d6886a8881430ae5f43dfc4 Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 27 Jul 2018 12:44:57 -0400 Subject: [PATCH 1/2] Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID. cr https://code.amazon.com/reviews/CR-2723653 --- src/analyses/local_bitvector_analysis.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 97caad53429..f307ba0f834 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -62,7 +62,7 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier) { localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier); if(it==locals.locals_map.end() || - it->second.id()!=ID_pointer || + it->second.type().id()!=ID_pointer || dirty(identifier)) return false; From 1e075465f3706f818adc1d34cbd91305d60f3147 Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 27 Jul 2018 16:21:20 -0400 Subject: [PATCH 2/2] Fixed secondary issues arising from local_bitvector_analysis fix. In particular, goto_check did not properly handle pointers whose value was an integer address (such as int *p = 0x10 in the test case memory_allocation1). This commit adds in pointer checks on pointers which are integer addresses, treating them essentially the same as pointers which are unknown (and could therefore point to any of the more well-defined types of memory objects), except that they are known not to be null, so no check for NULL is needed. --- regression/cbmc/memory_allocation1/test.desc | 6 +++--- src/analyses/goto_check.cpp | 21 ++++++++++++++------ 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index f45db0953f4..a4e17791c30 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -3,10 +3,10 @@ main.c --pointer-check ^EXIT=10$ ^SIGNAL=0$ -\[main.pointer_dereference.2\] dereference failure: pointer invalid in \*p: SUCCESS +\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in \*p: SUCCESS \[main.assertion.1\] assertion \*p==42: SUCCESS -\[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE +\[main.pointer_dereference.[0-9]+\] dereference failure: pointer invalid in p\[.*1\]: FAILURE \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS -\*\* 12 of 26 failed +^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index b294efafa29..c447e0de8ed 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -991,7 +991,8 @@ void goto_checkt::pointer_validity_check( allocs=disjunction(disjuncts); } - if(flags.is_unknown() || flags.is_null()) + if(flags.is_unknown() || + flags.is_null()) { add_guarded_claim( or_exprt(allocs, not_exprt(null_pointer(pointer))), @@ -1002,7 +1003,8 @@ void goto_checkt::pointer_validity_check( guard); } - if(flags.is_unknown()) + if(flags.is_unknown() || + flags.is_integer_address()) add_guarded_claim( or_exprt(allocs, not_exprt(invalid_pointer(pointer))), "dereference failure: pointer invalid", @@ -1020,7 +1022,9 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(flags.is_unknown() || flags.is_dynamic_heap()) + if(flags.is_unknown() || + flags.is_dynamic_heap() || + flags.is_integer_address()) add_guarded_claim( or_exprt(allocs, not_exprt(deallocated(pointer, ns))), "dereference failure: deallocated dynamic object", @@ -1029,7 +1033,9 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(flags.is_unknown() || flags.is_dynamic_local()) + if(flags.is_unknown() || + flags.is_dynamic_local() || + flags.is_integer_address()) add_guarded_claim( or_exprt(allocs, not_exprt(dead_object(pointer, ns))), "dereference failure: dead object", @@ -1038,7 +1044,9 @@ void goto_checkt::pointer_validity_check( expr, guard); - if(flags.is_unknown() || flags.is_dynamic_heap()) + if(flags.is_unknown() || + flags.is_dynamic_heap() || + flags.is_integer_address()) { const or_exprt dynamic_bounds( dynamic_object_lower_bound(pointer, ns, access_lb), @@ -1059,7 +1067,8 @@ void goto_checkt::pointer_validity_check( if(flags.is_unknown() || flags.is_dynamic_local() || - flags.is_static_lifetime()) + flags.is_static_lifetime() || + flags.is_integer_address()) { const or_exprt object_bounds( object_lower_bound(pointer, ns, access_lb),