From 0a61fbdce380d5f8f66b1ec8de8f60cbd2c1f8cf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 6 May 2021 10:41:43 +0000 Subject: [PATCH] Remove unnecessary use of dynamic_size goto_check still used dynamic_size, even though it was safe to consistently use object_size as of 11431ea8. The use of dynamic_size resulted in redundant, and at times unnecessarily complex assertions, as witnessed by the changes to regression tests. --- .../Pointer_byte_extract5/no-simplify.desc | 2 +- regression/cbmc/bounds_check1/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 2 +- src/analyses/goto_check.cpp | 62 ++++++------------- 4 files changed, 21 insertions(+), 47 deletions(-) diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index a0cd2a4ed2e..31b58b17b85 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 16 failed +\*\* 1 of 11 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc index 28805d2437b..f9a7242a358 100644 --- a/regression/cbmc/bounds_check1/test.desc +++ b/regression/cbmc/bounds_check1/test.desc @@ -6,7 +6,7 @@ main.c \[\(.*\)i2\]: FAILURE dest\[\(.*\)j2\]: FAILURE payload\[\(.*\)[kl]2\]: FAILURE -\*\* 10 of [0-9]+ failed +\*\* 7 of [0-9]+ failed -- ^warning: ignoring \[\(.*\)i\]: FAILURE diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index ff8497a9af5..c88637311c2 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ ^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ -^\*\* 2 of 7 failed +^\*\* 1 of 6 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 42d302cf5ab..c3f7b4129bb 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1347,7 +1347,7 @@ void goto_checkt::bounds_check_index( const index_exprt &expr, const guardt &guard) { - typet array_type = expr.array().type(); + const typet &array_type = expr.array().type(); if(array_type.id()==ID_pointer) throw "index got pointer as array type"; @@ -1382,9 +1382,10 @@ void goto_checkt::bounds_check_index( { exprt p_offset=pointer_offset( to_dereference_expr(ode.root_object()).pointer()); - assert(p_offset.type()==effective_offset.type()); - effective_offset=plus_exprt(p_offset, effective_offset); + effective_offset = plus_exprt{p_offset, + typecast_exprt::conditional_cast( + effective_offset, p_offset.type())}; } exprt zero=from_integer(0, ode.offset().type()); @@ -1404,26 +1405,21 @@ void goto_checkt::bounds_check_index( } } - exprt type_matches_size=true_exprt(); - if(ode.root_object().id()==ID_dereference) { const exprt &pointer= to_dereference_expr(ode.root_object()).pointer(); - const if_exprt size( - dynamic_object(pointer), - typecast_exprt(dynamic_size(ns), object_size(pointer).type()), - object_size(pointer)); - - const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer)); - - assert(effective_offset.op0().type()==effective_offset.op1().type()); - - const auto size_casted = - typecast_exprt::conditional_cast(size, effective_offset.type()); + const plus_exprt effective_offset{ + ode.offset(), + typecast_exprt::conditional_cast( + pointer_offset(pointer), ode.offset().type())}; - binary_relation_exprt inequality(effective_offset, ID_lt, size_casted); + binary_relation_exprt inequality{ + effective_offset, + ID_lt, + typecast_exprt::conditional_cast( + object_size(pointer), effective_offset.type())}; exprt in_bounds_of_some_explicit_allocation = is_in_bounds_of_some_explicit_allocation( @@ -1432,7 +1428,6 @@ void goto_checkt::bounds_check_index( or_exprt precond( std::move(in_bounds_of_some_explicit_allocation), - and_exprt(dynamic_object(pointer), not_exprt(malloc_object(pointer, ns))), inequality); add_guarded_property( @@ -1443,25 +1438,7 @@ void goto_checkt::bounds_check_index( expr, guard); - auto type_size_opt = size_of_expr(ode.root_object().type(), ns); - - if(type_size_opt.has_value()) - { - // Build a predicate that evaluates to true iff the size reported by - // sizeof (i.e., compile-time size) matches the actual run-time size. The - // run-time size for a dynamic (i.e., heap-allocated) object is determined - // by the dynamic_size(ns) expression, which can only be used when - // malloc_object(pointer, ns) evaluates to true for a given pointer. - type_matches_size = if_exprt{ - dynamic_object(pointer), - and_exprt{malloc_object(pointer, ns), - equal_exprt{typecast_exprt::conditional_cast( - dynamic_size(ns), type_size_opt->type()), - *type_size_opt}}, - equal_exprt{typecast_exprt::conditional_cast( - object_size(pointer), type_size_opt->type()), - *type_size_opt}}; - } + return; } const exprt &size=array_type.id()==ID_array ? @@ -1497,7 +1474,7 @@ void goto_checkt::bounds_check_index( type_size_opt.value()); add_guarded_property( - implies_exprt(type_matches_size, inequality), + inequality, name + " upper bound", "array bounds", expr.find_source_location(), @@ -1506,14 +1483,11 @@ void goto_checkt::bounds_check_index( } else { - binary_relation_exprt inequality(index, ID_lt, size); - - // typecast size - inequality.op1() = typecast_exprt::conditional_cast( - inequality.op1(), inequality.op0().type()); + binary_relation_exprt inequality{ + typecast_exprt::conditional_cast(index, size.type()), ID_lt, size}; add_guarded_property( - implies_exprt(type_matches_size, inequality), + inequality, name + " upper bound", "array bounds", expr.find_source_location(),