Skip to content

Commit e17d28e

Browse files
tautschnigtautschnig
committed
Refactor field_sensitivityt::apply
The function already was very long, and the preceding commit added yet more nested branches.
1 parent 99cb87c commit e17d28e

File tree

2 files changed

+99
-83
lines changed

2 files changed

+99
-83
lines changed

‎src/goto-symex/field_sensitivity.cpp‎

Lines changed: 92 additions & 83 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,89 +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(!recursive_member.has_value())
115-
continue;
116-
117-
// We need to inspect the access path as the resulting expression may
118-
// involve index expressions. When array field sensitivity is disabled
119-
// or the size of the array that is indexed into is larger than
120-
// max_field_sensitivity_array_size then only the expression up to (but
121-
// excluding) said index expression can be turned into an ssa_exprt.
122-
exprt full_exprt = *recursive_member;
123-
exprt *for_ssa = &full_exprt;
124-
exprt *parent = for_ssa;
125-
while(parent->id() == ID_typecast)
126-
parent = &to_typecast_expr(*parent).op();
127-
while(parent->id() == ID_member || parent->id() == ID_index)
128-
{
129-
if(parent->id() == ID_member)
130-
{
131-
parent = &to_member_expr(*parent).compound();
132-
}
133-
else
134-
{
135-
parent = &to_index_expr(*parent).array();
136-
#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
137-
if(
138-
!to_array_type(parent->type()).size().is_constant() ||
139-
numeric_cast_v<mp_integer>(
140-
to_constant_expr(to_array_type(parent->type()).size())) >
141-
max_field_sensitivity_array_size)
142-
{
143-
for_ssa = parent;
144-
}
145-
#else
146-
for_ssa = parent;
147-
#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
148-
}
149-
}
150-
151-
if(for_ssa->id() == ID_index || for_ssa->id() == ID_member)
152-
{
153-
tmp.type() = for_ssa->type();
154-
tmp.set_expression(*for_ssa);
155-
if(was_l2)
156-
{
157-
*for_ssa =
158-
apply(ns, state, state.rename(std::move(tmp), ns).get(), write);
159-
}
160-
else
161-
*for_ssa = apply(ns, state, std::move(tmp), write);
162-
163-
return full_exprt;
164-
}
165-
else if(for_ssa->id() == ID_typecast)
166-
{
167-
if(was_l2)
168-
{
169-
*for_ssa =
170-
apply(ns, state, state.rename(*for_ssa, ns).get(), write);
171-
}
172-
else
173-
*for_ssa = apply(ns, state, std::move(*for_ssa), write);
174-
175-
return full_exprt;
176-
}
177-
}
178-
}
187+
return apply_byte_extract(ns, state, to_byte_extract_expr(expr));
179188
}
180189
#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
181190
else if(expr.id() == ID_index)

‎src/goto-symex/field_sensitivity.h‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -221,6 +221,13 @@ class field_sensitivityt
221221
exprt e,
222222
const value_sett &value_set,
223223
const namespacet &ns) const;
224+
225+
/// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
226+
[[nodiscard]] exprt apply_byte_extract(
227+
const namespacet &ns,
228+
goto_symex_statet &state,
229+
const byte_extract_exprt &be,
230+
bool write) const;
224231
};
225232

226233
#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

0 commit comments

Comments
 (0)