CBMC: /home/runner/work/cbmc/cbmc/src/util/simplify_expr_struct.cpp Source File

CBMC
Loading...
Searching...
No Matches
simplify_expr_struct.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "simplify_expr_class.h"
10
11#include "arith_tools.h"
12#include "byte_operators.h"
13#include "c_types.h"
14#include "config.h"
15#include "expr_util.h"
16#include "invariant.h"
17#include "namespace.h"
18#include "pointer_offset_size.h"
19#include "simplify_utils.h"
20#include "std_expr.h"
21
22simplify_exprt::resultt<>
24{
25 const irep_idt &component_name=
26 to_member_expr(expr).get_component_name();
27
28 const exprt &op = expr.compound();
29
30 if(op.id()==ID_with)
31 {
32 // the following optimization only works on structs,
33 // and not on unions
34
35 if(
36 op.operands().size() >= 3 &&
37 (op.type().id() == ID_struct || op.type().id() == ID_struct_tag))
38 {
40
41 while(new_operands.size() > 1)
42 {
43 exprt &op1 = new_operands[new_operands.size() - 2];
44 exprt &op2 = new_operands[new_operands.size() - 1];
45
46 if(op1.get(ID_component_name)==component_name)
47 {
48 // found it!
50 op2.type() == expr.type(),
51 "member expression type must match component type");
52
53 return op2;
54 }
55 else // something else, get rid of it
56 new_operands.resize(new_operands.size() - 2);
57 }
58
59 DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
60
61 auto new_member_expr = expr;
62 new_member_expr.struct_op() = new_operands.front();
63 // do this recursively
65 }
66 else if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
67 {
69
70 if(with_expr.where().get(ID_component_name)==component_name)
71 {
72 // WITH(s, .m, v).m -> v
73 return with_expr.new_value();
74 }
75 }
76 }
77 else if(op.id()==ID_update)
78 {
79 if(
80 op.operands().size() == 3 &&
81 (op.type().id() == ID_struct || op.type().id() == ID_struct_tag))
82 {
84 const exprt::operandst &designator=update_expr.designator();
85
86 // look at very first designator
87 if(designator.size()==1 &&
88 designator.front().id()==ID_member_designator)
89 {
90 if(designator.front().get(ID_component_name)==component_name)
91 {
92 // UPDATE(s, .m, v).m -> v
93 return update_expr.new_value();
94 }
95 // the following optimization only works on structs,
96 // and not on unions
97 else if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
98 {
99 // UPDATE(s, .m1, v).m2 -> s.m2
100 auto new_expr = expr;
101 new_expr.struct_op() = update_expr.old();
102
103 // do this recursively
105 }
106 }
107 }
108 }
109 else if(op.id() == ID_struct)
110 {
111 // pull out the right member
113 op.type().id() == ID_struct_tag
114 ? ns.follow_tag(to_struct_tag_type(op.type()))
115 : to_struct_type(op.type());
116 if(struct_type.has_component(component_name))
117 {
118 std::size_t number = struct_type.component_number(component_name);
120 op.operands().size() > number,
121 "struct expression must have sufficiently many operands");
123 op.operands()[number].type() == expr.type(),
124 "member expression type must match component type");
125 return op.operands()[number];
126 }
127 }
128 else if(op.id()==ID_byte_extract_little_endian ||
130 {
131 const auto &byte_extract_expr = to_byte_extract_expr(op);
132
133 if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
134 {
135 // This rewrites byte_extract(s, o, struct_type).member
136 // to byte_extract(s, o+member_offset, member_type)
137
139 op.type().id() == ID_struct_tag
140 ? ns.follow_tag(to_struct_tag_type(op.type()))
141 : to_struct_type(op.type());
143 struct_type.get_component(component_name);
144
145 if(
146 component.is_nil() || component.type().id() == ID_c_bit_field ||
147 component.is_boolean())
148 {
149 return unchanged(expr);
150 }
151
152 // add member offset to index
153 auto offset_int = member_offset(struct_type, component_name, ns);
154 if(!offset_int.has_value())
155 return unchanged(expr);
156
157 const exprt &struct_offset = byte_extract_expr.offset();
161
162 byte_extract_exprt result(
163 op.id(),
166 byte_extract_expr.get_bits_per_byte(),
167 expr.type());
168
169 return changed(simplify_byte_extract(result)); // recursive call
170 }
171 else if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
172 {
173 // rewrite byte_extract(X, 0).member to X
174 // if the type of X is that of the member
175 if(byte_extract_expr.offset() == 0)
176 {
177 const union_typet &union_type =
178 op.type().id() == ID_union_tag
179 ? ns.follow_tag(to_union_tag_type(op.type()))
180 : to_union_type(op.type());
181 const typet &subtype = union_type.component_type(component_name);
182
183 if(subtype == byte_extract_expr.op().type())
184 return byte_extract_expr.op();
185 }
186 }
187 }
188 else if(
189 op.id() == ID_union &&
190 (op.type().id() == ID_union || op.type().id() == ID_union_tag))
191 {
192 // trivial?
193 if(to_union_expr(op).op().type() == expr.type())
194 return to_union_expr(op).op();
195
196 // need to convert!
197 auto target_size = pointer_offset_size(expr.type(), ns);
198
199 if(target_size.has_value())
200 {
201 mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
202 const auto bits = expr2bits(op, true, ns);
203
204 if(bits.has_value() &&
205 mp_integer(bits->size())>=target_bits)
206 {
207 std::string bits_cut =
208 std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
209
210 auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
211
212 if(tmp.has_value())
213 return std::move(*tmp);
214 }
215 }
216 }
217 else if(op.id() == ID_typecast)
218 {
219 const auto &typecast_expr = to_typecast_expr(op);
220
221 // Try to look through member(cast(x)) if the cast is between structurally
222 // identical types:
223 if(op.type() == typecast_expr.op().type())
224 {
225 auto new_expr = expr;
226 new_expr.struct_op() = typecast_expr.op();
228 }
229
230 // Try to translate into an equivalent member (perhaps nested) of the type
231 // being cast (for example, this might turn ((struct A)x).field1 into
232 // x.substruct.othersubstruct.field2, if field1 and field2 have the same
233 // type and offset with respect to x.
234 if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
235 {
237 op.type().id() == ID_struct_tag
238 ? ns.follow_tag(to_struct_tag_type(op.type()))
239 : to_struct_type(op.type());
240 std::optional<mp_integer> requested_offset =
241 member_offset(struct_type, component_name, ns);
242 if(requested_offset.has_value())
243 {
245 typecast_expr.op(), *requested_offset, expr.type(), ns);
246
247 // Guess: turning this into a byte-extract operation is not really an
248 // optimisation.
249 if(
250 equivalent_member.has_value() &&
253 {
254 auto tmp = equivalent_member.value();
255 return changed(simplify_rec(tmp));
256 }
257 }
258 }
259 }
260 else if(op.id() == ID_let)
261 {
262 // Push a member operator inside a let binding, to avoid the let bisecting
263 // structures we otherwise know how to analyse, such as
264 // (let x = 1 in ({x, x})).field1 --> let x = 1 in ({x, x}.field1) -->
265 // let x = 1 in x
267 pushed_in_member.op() = to_let_expr(op).where();
268 auto new_expr = op;
270 to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
271
273 }
274
275 return unchanged(expr);
276}
277
278simplify_exprt::resultt<>
280{
281 const exprt &compound = expr.compound();
282
283 if(compound.id() == ID_if)
284 {
285 if_exprt if_expr = lift_if(expr, 0);
287 }
288 else
289 {
290 auto r_it = simplify_rec(compound); // recursive call
291 if(r_it.has_changed())
292 {
293 auto tmp = expr;
294 tmp.compound() = r_it.expr;
295 return tmp;
296 }
297 }
298
299 return unchanged(expr);
300}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Expression of type type extracted from some object op starting at position offset (given in number of...
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
The trinary if-then-else operator.
Definition std_expr.h:2426
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2866
const exprt & compound() const
Definition std_expr.h:2915
The plus expression Associativity is not specified.
Definition std_expr.h:1006
const namespacet & ns
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_member_preorder(const member_exprt &)
static resultt changed(resultt<> result)
resultt simplify_rec(const exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_plus(const plus_exprt &)
resultt simplify_if_preorder(const if_exprt &expr)
Structure type, corresponds to C style structs.
Definition std_types.h:230
Definition std_types.h:68
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:147
Operator to update elements in structs and arrays.
Definition std_expr.h:2679
Operator to update elements in structs and arrays.
Definition std_expr.h:2520
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition expr_util.cpp:172
Deprecated expression utility functions.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:291
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3383
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2953
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1765
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2573
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2762
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:307
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517

AltStyle によって変換されたページ (->オリジナル) /