Skip to content

Remove unnecessary use of dynamic_size #6082

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 6, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/cbmc/Pointer_byte_extract5/no-simplify.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
--
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/bounds_check1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc/memory_allocation2/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -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
62 changes: 18 additions & 44 deletions src/analyses/goto_check.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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());
Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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 ?
Expand Down Expand Up @@ -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(),
Expand All @@ -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(),
Expand Down