cprover
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
10
11#include "arith_tools.h"
12#include "byte_operators.h"
13#include "c_types.h"
14#include "invariant.h"
15#include "namespace.h"
16#include "pointer_offset_size.h"
17#include "simplify_utils.h"
18#include "std_expr.h"
19
22{
23 const irep_idt &component_name=
25
26 const exprt &op = expr.compound();
27 const typet &op_type=ns.follow(op.type());
28
29 if(op.id()==ID_with)
30 {
31 // the following optimization only works on structs,
32 // and not on unions
33
34 if(op.operands().size()>=3 &&
35 op_type.id()==ID_struct)
36 {
38
39 while(new_operands.size() > 1)
40 {
41 exprt &op1 = new_operands[new_operands.size() - 2];
42 exprt &op2 = new_operands[new_operands.size() - 1];
43
44 if(op1.get(ID_component_name)==component_name)
45 {
46 // found it!
48 op2.type() == expr.type(),
49 "member expression type must match component type");
50
51 return op2;
52 }
53 else // something else, get rid of it
54 new_operands.resize(new_operands.size() - 2);
55 }
56
57 DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
58
59 auto new_member_expr = expr;
60 new_member_expr.struct_op() = new_operands.front();
61 // do this recursively
63 }
64 else if(op_type.id()==ID_union)
65 {
67
68 if(with_expr.where().get(ID_component_name)==component_name)
69 {
70 // WITH(s, .m, v).m -> v
71 return with_expr.new_value();
72 }
73 }
74 }
75 else if(op.id()==ID_update)
76 {
77 if(op.operands().size()==3 &&
78 op_type.id()==ID_struct)
79 {
81 const exprt::operandst &designator=update_expr.designator();
82
83 // look at very first designator
84 if(designator.size()==1 &&
85 designator.front().id()==ID_member_designator)
86 {
87 if(designator.front().get(ID_component_name)==component_name)
88 {
89 // UPDATE(s, .m, v).m -> v
90 return update_expr.new_value();
91 }
92 // the following optimization only works on structs,
93 // and not on unions
94 else if(op_type.id()==ID_struct)
95 {
96 // UPDATE(s, .m1, v).m2 -> s.m2
97 auto new_expr = expr;
98 new_expr.struct_op() = update_expr.old();
99
100 // do this recursively
102 }
103 }
104 }
105 }
106 else if(op.id()==ID_struct ||
107 op.id()==ID_constant)
108 {
109 if(op_type.id()==ID_struct)
110 {
111 // pull out the right member
113 if(struct_type.has_component(component_name))
114 {
115 std::size_t number=struct_type.component_number(component_name);
117 op.operands()[number].type() == expr.type(),
118 "member expression type must match component type");
119 return op.operands()[number];
120 }
121 }
122 }
123 else if(op.id()==ID_byte_extract_little_endian ||
125 {
126 const auto &byte_extract_expr = to_byte_extract_expr(op);
127
128 if(op_type.id()==ID_struct)
129 {
130 // This rewrites byte_extract(s, o, struct_type).member
131 // to byte_extract(s, o+member_offset, member_type)
132
135 struct_type.get_component(component_name);
136
137 if(
138 component.is_nil() || component.type().id() == ID_c_bit_field ||
139 component.type().id() == ID_bool)
140 {
141 return unchanged(expr);
142 }
143
144 // add member offset to index
145 auto offset_int = member_offset(struct_type, component_name, ns);
146 if(!offset_int.has_value())
147 return unchanged(expr);
148
149 const exprt &struct_offset = byte_extract_expr.offset();
153
154 byte_extract_exprt result(
155 op.id(), byte_extract_expr.op(), final_offset, expr.type());
156
157 return changed(simplify_byte_extract(result)); // recursive call
158 }
159 else if(op_type.id() == ID_union)
160 {
161 // rewrite byte_extract(X, 0).member to X
162 // if the type of X is that of the member
163 if(byte_extract_expr.offset().is_zero())
164 {
166 const typet &subtype = union_type.component_type(component_name);
167
168 if(subtype == byte_extract_expr.op().type())
169 return byte_extract_expr.op();
170 }
171 }
172 }
173 else if(op.id()==ID_union && op_type.id()==ID_union)
174 {
175 // trivial?
176 if(to_union_expr(op).op().type() == expr.type())
177 return to_union_expr(op).op();
178
179 // need to convert!
180 auto target_size = pointer_offset_size(expr.type(), ns);
181
182 if(target_size.has_value())
183 {
184 mp_integer target_bits = target_size.value() * 8;
185 const auto bits = expr2bits(op, true, ns);
186
187 if(bits.has_value() &&
188 mp_integer(bits->size())>=target_bits)
189 {
190 std::string bits_cut =
191 std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
192
193 auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
194
195 if(tmp.has_value())
196 return std::move(*tmp);
197 }
198 }
199 }
200 else if(op.id() == ID_typecast)
201 {
202 const auto &typecast_expr = to_typecast_expr(op);
203
204 // Try to look through member(cast(x)) if the cast is between structurally
205 // identical types:
206 if(op_type == typecast_expr.op().type())
207 {
208 auto new_expr = expr;
209 new_expr.struct_op() = typecast_expr.op();
211 }
212
213 // Try to translate into an equivalent member (perhaps nested) of the type
214 // being cast (for example, this might turn ((struct A)x).field1 into
215 // x.substruct.othersubstruct.field2, if field1 and field2 have the same
216 // type and offset with respect to x.
217 if(op_type.id() == ID_struct)
218 {
220 member_offset(to_struct_type(op_type), component_name, ns);
221 if(requested_offset.has_value())
222 {
224 typecast_expr.op(), *requested_offset, expr.type(), ns);
225
226 // Guess: turning this into a byte-extract operation is not really an
227 // optimisation.
228 if(
229 equivalent_member.has_value() &&
232 {
233 auto tmp = equivalent_member.value();
234 return changed(simplify_rec(tmp));
235 }
236 }
237 }
238 }
239 else if(op.id()==ID_if)
240 {
241 const if_exprt &if_expr=to_if_expr(op);
242 exprt cond=if_expr.cond();
243
245 member_false.compound()=if_expr.false_case();
246
248 member_true.compound() = if_expr.true_case();
249
250 auto tmp = if_exprt(cond, member_true, member_false, expr.type());
251 return changed(simplify_rec(tmp));
252 }
253 else if(op.id() == ID_let)
254 {
255 // Push a member operator inside a let binding, to avoid the let bisecting
256 // structures we otherwise know how to analyse, such as
257 // (let x = 1 in ({x, x})).field1 --> let x = 1 in ({x, x}.field1) -->
258 // let x = 1 in x
261 auto new_expr = op;
264
266 }
267
268 return unchanged(expr);
269}
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:162
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Expression of type type extracted from some object op starting at position offset (given in number of...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
The trinary if-then-else operator.
Definition std_expr.h:2226
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
const irep_idt & id() const
Definition irep.h:396
exprt & where()
convenience accessor for binding().where()
Definition std_expr.h:3066
Extract member of struct or union.
Definition std_expr.h:2667
const exprt & compound() const
Definition std_expr.h:2708
irep_idt get_component_name() const
Definition std_expr.h:2681
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
The plus expression Associativity is not specified.
Definition std_expr.h:914
const namespacet & ns
resultt simplify_byte_extract(const byte_extract_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 &)
Structure type, corresponds to C style structs.
Definition std_types.h:231
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:293
The union type.
Definition c_types.h:125
Operator to update elements in structs and arrays.
Definition std_expr.h:2496
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Pointer Logic.
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< 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:510
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3097
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1657
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2374
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2561
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308