Skip to content

Commit 147a1e3

Browse files
tautschnigtautschnig
authored
Merge pull request #8579 from tautschnig/bugfixes/field-sensitivity-union
Field sensitivity: account for array size in all index expressions
2 parents 9d14448 + bf5d793 commit 147a1e3

File tree

4 files changed

+121
-49
lines changed

4 files changed

+121
-49
lines changed

‎regression/cbmc/field-sensitivity17/main.c‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
union U
2+
{
3+
unsigned char buf[2];
4+
} s;
5+
6+
int main()
7+
{
8+
__CPROVER_assert(s.buf[0] == 0, "");
9+
}

‎regression/cbmc/field-sensitivity17/test.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--max-field-sensitivity-array-size 1
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--
9+
The test is a minimized version of code generated using Kani. It should pass
10+
irrespective of whether field sensitivity is applied to the array or not. (The
11+
original example was unexpectedly failing with an array size of 65, but passed
12+
with an array size of 64 or less.)

‎src/goto-symex/field_sensitivity.cpp‎

Lines changed: 92 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,97 @@ exprt field_sensitivityt::apply(
3131
return get_fields(ns, state, ssa_expr, true);
3232
}
3333

34+
exprt field_sensitivityt::apply_byte_extract(
35+
const namespacet &ns,
36+
goto_symex_statet &state,
37+
const byte_extract_exprt &be,
38+
bool write) const
39+
{
40+
if(
41+
(be.op().type().id() != ID_union && be.op().type().id() != ID_union_tag) ||
42+
!is_ssa_expr(be.op()) || !be.offset().is_constant())
43+
{
44+
return be;
45+
}
46+
47+
const union_typet &type = be.op().type().id() == ID_union_tag
48+
? ns.follow_tag(to_union_tag_type(be.op().type()))
49+
: to_union_type(be.op().type());
50+
for(const auto &comp : type.components())
51+
{
52+
ssa_exprt tmp = to_ssa_expr(be.op());
53+
bool was_l2 = !tmp.get_level_2().empty();
54+
tmp.remove_level_2();
55+
const member_exprt member{tmp.get_original_expr(), comp};
56+
auto recursive_member =
57+
get_subexpression_at_offset(member, be.offset(), be.type(), ns);
58+
if(!recursive_member.has_value())
59+
continue;
60+
61+
// We need to inspect the access path as the resulting expression may
62+
// involve index expressions. When array field sensitivity is disabled
63+
// or the size of the array that is indexed into is larger than
64+
// max_field_sensitivity_array_size then only the expression up to (but
65+
// excluding) said index expression can be turned into an ssa_exprt.
66+
exprt full_exprt = *recursive_member;
67+
exprt *for_ssa = &full_exprt;
68+
exprt *parent = for_ssa;
69+
while(parent->id() == ID_typecast)
70+
parent = &to_typecast_expr(*parent).op();
71+
while(parent->id() == ID_member || parent->id() == ID_index)
72+
{
73+
if(parent->id() == ID_member)
74+
{
75+
parent = &to_member_expr(*parent).compound();
76+
}
77+
else
78+
{
79+
parent = &to_index_expr(*parent).array();
80+
#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
81+
if(
82+
!to_array_type(parent->type()).size().is_constant() ||
83+
numeric_cast_v<mp_integer>(
84+
to_constant_expr(to_array_type(parent->type()).size())) >
85+
max_field_sensitivity_array_size)
86+
{
87+
for_ssa = parent;
88+
}
89+
#else
90+
for_ssa = parent;
91+
#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
92+
}
93+
}
94+
95+
if(for_ssa->id() == ID_index || for_ssa->id() == ID_member)
96+
{
97+
tmp.type() = for_ssa->type();
98+
tmp.set_expression(*for_ssa);
99+
if(was_l2)
100+
{
101+
*for_ssa =
102+
apply(ns, state, state.rename(std::move(tmp), ns).get(), write);
103+
}
104+
else
105+
*for_ssa = apply(ns, state, std::move(tmp), write);
106+
107+
return full_exprt;
108+
}
109+
else if(for_ssa->id() == ID_typecast)
110+
{
111+
if(was_l2)
112+
{
113+
*for_ssa = apply(ns, state, state.rename(*for_ssa, ns).get(), write);
114+
}
115+
else
116+
*for_ssa = apply(ns, state, std::move(*for_ssa), write);
117+
118+
return full_exprt;
119+
}
120+
}
121+
122+
return be;
123+
}
124+
34125
exprt field_sensitivityt::apply(
35126
const namespacet &ns,
36127
goto_symex_statet &state,
@@ -93,55 +184,7 @@ exprt field_sensitivityt::apply(
93184
!write && (expr.id() == ID_byte_extract_little_endian ||
94185
expr.id() == ID_byte_extract_big_endian))
95186
{
96-
const byte_extract_exprt &be = to_byte_extract_expr(expr);
97-
if(
98-
(be.op().type().id() == ID_union ||
99-
be.op().type().id() == ID_union_tag) &&
100-
is_ssa_expr(be.op()) && be.offset().is_constant())
101-
{
102-
const union_typet &type =
103-
be.op().type().id() == ID_union_tag
104-
? ns.follow_tag(to_union_tag_type(be.op().type()))
105-
: to_union_type(be.op().type());
106-
for(const auto &comp : type.components())
107-
{
108-
ssa_exprt tmp = to_ssa_expr(be.op());
109-
bool was_l2 = !tmp.get_level_2().empty();
110-
tmp.remove_level_2();
111-
const member_exprt member{tmp.get_original_expr(), comp};
112-
auto recursive_member =
113-
get_subexpression_at_offset(member, be.offset(), be.type(), ns);
114-
if(
115-
recursive_member.has_value() &&
116-
(recursive_member->id() == ID_member ||
117-
recursive_member->id() == ID_index))
118-
{
119-
tmp.type() = be.type();
120-
tmp.set_expression(*recursive_member);
121-
if(was_l2)
122-
{
123-
return apply(
124-
ns, state, state.rename(std::move(tmp), ns).get(), write);
125-
}
126-
else
127-
return apply(ns, state, std::move(tmp), write);
128-
}
129-
else if(
130-
recursive_member.has_value() && recursive_member->id() == ID_typecast)
131-
{
132-
if(was_l2)
133-
{
134-
return apply(
135-
ns,
136-
state,
137-
state.rename(std::move(*recursive_member), ns).get(),
138-
write);
139-
}
140-
else
141-
return apply(ns, state, std::move(*recursive_member), write);
142-
}
143-
}
144-
}
187+
return apply_byte_extract(ns, state, to_byte_extract_expr(expr), write);
145188
}
146189
#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
147190
else if(expr.id() == ID_index)

‎src/goto-symex/field_sensitivity.h‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Michael Tautschnig
1111

1212
#include <util/ssa_expr.h>
1313

14+
class byte_extract_exprt;
1415
class namespacet;
1516
class goto_symex_statet;
1617
class symex_targett;
@@ -221,6 +222,13 @@ class field_sensitivityt
221222
exprt e,
222223
const value_sett &value_set,
223224
const namespacet &ns) const;
225+
226+
/// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
227+
[[nodiscard]] exprt apply_byte_extract(
228+
const namespacet &ns,
229+
goto_symex_statet &state,
230+
const byte_extract_exprt &expr,
231+
bool write) const;
224232
};
225233

226234
#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

0 commit comments

Comments
 (0)