Skip to content

Commit 5c0408c

Browse files
committed
Simplify multiple-of-element size access to arrays
Array operations may fall back to byte_extract or byte_update expressions in parts of the code base. Simplify this to index or WITH expressions, respectively, when the offset is known to be a multiple of the array-element size, or a constant offset plus a multiple of the array-element size. Fixes: #8617
1 parent d251345 commit 5c0408c

File tree

9 files changed

+319
-22
lines changed

9 files changed

+319
-22
lines changed
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int main()
2+
{
3+
char source[8];
4+
int int_source[2];
5+
int target[4];
6+
int n;
7+
if(n >= 0 && n < 3)
8+
{
9+
__CPROVER_array_replace(&target[n], source);
10+
__CPROVER_array_replace(&target[n], int_source);
11+
__CPROVER_assert(target[n] == int_source[0], "");
12+
__CPROVER_assert(target[n + 1] == int_source[1], "");
13+
}
14+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE paths-lifo-expected-failure
2+
main.c
3+
--program-only
4+
target!0@1#2 ==
5+
target!0@1#3 ==
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
byte_update_
10+
--
11+
This test demonstrates that we can simplify byte_update expressions to, e.g.,
12+
WITH expressions.
13+
Disabled for paths-lifo mode, which does not support --program-only.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

regression/cbmc/havoc_slice/functional_assign.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
functional.c
33
-DN=4 -DASSIGN --program-only
44
^EXIT=0$

regression/cbmc/havoc_slice/functional_slice_bytes.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
functional.c
33
-DN=4 -DSLICE_BYTES --program-only
44
^EXIT=0$

regression/cbmc/havoc_slice/functional_slice_typed.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
functional.c
33
-DN=4 -DSLICE_TYPED --program-only
44
^EXIT=0$

regression/validate-trace-xml-schema/check.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@
3535
['show_properties1', 'test.desc'],
3636
# program-only instead of trace
3737
['vla1', 'program-only.desc'],
38+
['Array_operations4', 'program-only.desc'],
3839
['Pointer_Arithmetic19', 'test.desc'],
3940
['Quantifiers-simplify', 'simplify_not_forall.desc'],
4041
['array-cell-sensitivity15', 'test.desc'],

src/util/pointer_offset_size.cpp

Lines changed: 137 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -687,7 +687,143 @@ std::optional<exprt> get_subexpression_at_offset(
687687
const auto offset_bytes = numeric_cast<mp_integer>(offset);
688688

689689
if(!offset_bytes.has_value())
690-
return {};
690+
{
691+
// offset is not a constant; try to see whether it is a multiple of a
692+
// constant, or a sum that involves a multiple of a constant
693+
if(auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
694+
{
695+
const auto target_size_bits = pointer_offset_bits(target_type, ns);
696+
const auto elem_size_bits =
697+
pointer_offset_bits(array_type->element_type(), ns);
698+
699+
// no arrays of zero-, or unknown-sized elements, or ones where elements
700+
// have a bit-width that isn't a multiple of bytes
701+
if(
702+
!target_size_bits.has_value() || !elem_size_bits.has_value() ||
703+
*elem_size_bits <= 0 ||
704+
*elem_size_bits % config.ansi_c.char_width != 0 ||
705+
*target_size_bits != *elem_size_bits)
706+
{
707+
return {};
708+
}
709+
710+
// if we have an offset C + x (where C is a constant) we can try to
711+
// recurse by first looking at the member at offset C
712+
if(
713+
offset.id() == ID_plus && offset.operands().size() == 2 &&
714+
(to_multi_ary_expr(offset).op0().is_constant() ||
715+
to_multi_ary_expr(offset).op1().is_constant()))
716+
{
717+
const plus_exprt &offset_plus = to_plus_expr(offset);
718+
const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
719+
offset_plus.op0().is_constant() ? offset_plus.op0()
720+
: offset_plus.op1()));
721+
const exprt &other_factor = offset_plus.op0().is_constant()
722+
? offset_plus.op1()
723+
: offset_plus.op0();
724+
725+
auto expr_at_offset_C =
726+
get_subexpression_at_offset(expr, const_factor, target_type, ns);
727+
728+
if(
729+
expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
730+
to_index_expr(*expr_at_offset_C).index().is_zero())
731+
{
732+
return get_subexpression_at_offset(
733+
to_index_expr(*expr_at_offset_C).array(),
734+
other_factor,
735+
target_type,
736+
ns);
737+
}
738+
}
739+
740+
// give up if the offset expression isn't of the form K * i or i * K
741+
// (where K is a constant)
742+
if(
743+
offset.id() != ID_mult || offset.operands().size() != 2 ||
744+
(!to_multi_ary_expr(offset).op0().is_constant() &&
745+
!to_multi_ary_expr(offset).op1().is_constant()))
746+
{
747+
return {};
748+
}
749+
750+
const mult_exprt &offset_mult = to_mult_expr(offset);
751+
const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
752+
offset_mult.op0().is_constant() ? offset_mult.op0()
753+
: offset_mult.op1()));
754+
const exprt &other_factor =
755+
offset_mult.op0().is_constant() ? offset_mult.op1() : offset_mult.op0();
756+
757+
if(const_factor % (*elem_size_bits / config.ansi_c.char_width) != 0)
758+
return {};
759+
760+
exprt index = mult_exprt{
761+
other_factor,
762+
from_integer(
763+
const_factor / (*elem_size_bits / config.ansi_c.char_width),
764+
other_factor.type())};
765+
766+
return get_subexpression_at_offset(
767+
index_exprt{
768+
expr,
769+
typecast_exprt::conditional_cast(index, array_type->index_type())},
770+
0,
771+
target_type,
772+
ns);
773+
}
774+
else if(
775+
auto struct_tag_type =
776+
type_try_dynamic_cast<struct_tag_typet>(expr.type()))
777+
{
778+
// If the offset expression is of the form K * i or i * K (where K is a
779+
// constant) and the first component of the struct is an array we will
780+
// recurse on that member.
781+
const auto &components = ns.follow_tag(*struct_tag_type).components();
782+
if(
783+
!components.empty() &&
784+
can_cast_type<array_typet>(components.front().type()) &&
785+
offset.id() == ID_mult && offset.operands().size() == 2 &&
786+
(to_multi_ary_expr(offset).op0().is_constant() ||
787+
to_multi_ary_expr(offset).op1().is_constant()))
788+
{
789+
return get_subexpression_at_offset(
790+
member_exprt{expr, components.front()}, offset, target_type, ns);
791+
}
792+
// if we have an offset C + x (where C is a constant) we can try to
793+
// recurse by first looking at the member at offset C
794+
else if(
795+
offset.id() == ID_plus && offset.operands().size() == 2 &&
796+
(to_multi_ary_expr(offset).op0().is_constant() ||
797+
to_multi_ary_expr(offset).op1().is_constant()))
798+
{
799+
const plus_exprt &offset_plus = to_plus_expr(offset);
800+
const auto &const_factor = numeric_cast_v<mp_integer>(to_constant_expr(
801+
offset_plus.op0().is_constant() ? offset_plus.op0()
802+
: offset_plus.op1()));
803+
const exprt &other_factor = offset_plus.op0().is_constant()
804+
? offset_plus.op1()
805+
: offset_plus.op0();
806+
807+
auto expr_at_offset_C =
808+
get_subexpression_at_offset(expr, const_factor, target_type, ns);
809+
810+
if(
811+
expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
812+
to_index_expr(*expr_at_offset_C).index().is_zero())
813+
{
814+
return get_subexpression_at_offset(
815+
to_index_expr(*expr_at_offset_C).array(),
816+
other_factor,
817+
target_type,
818+
ns);
819+
}
820+
}
821+
822+
return {};
823+
}
824+
else
825+
return {};
826+
}
691827
else
692828
return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
693829
}

0 commit comments

Comments
 (0)