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 {
37 exprt::operandst new_operands = op.operands();
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
62 return changed(simplify_member(new_member_expr));
63 }
64 else if(op_type.id()==ID_union)
65 {
66 const with_exprt &with_expr=to_with_expr(op);
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 {
80 const update_exprt &update_expr=to_update_expr(op);
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
101 return changed(simplify_member(new_expr));
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
112 const struct_typet &struct_type=to_struct_type(op_type);
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 ||
124 op.id()==ID_byte_extract_big_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
133 const struct_typet &struct_type=to_struct_type(op_type);
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();
150 exprt member_offset = from_integer(*offset_int, struct_offset.type());
151 exprt final_offset =
152 simplify_plus(plus_exprt(struct_offset, member_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 {
165 const union_typet &union_type = to_union_type(op_type);
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();
210 return changed(simplify_member(new_expr));
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 {
219 optionalt<mp_integer> requested_offset =
220 member_offset(to_struct_type(op_type), component_name, ns);
221 if(requested_offset.has_value())
222 {
223 auto equivalent_member = get_subexpression_at_offset(
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() &&
230 equivalent_member.value().id() != ID_byte_extract_little_endian &&
231 equivalent_member.value().id() != ID_byte_extract_big_endian)
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
244 member_exprt member_false=to_member_expr(expr);
245 member_false.compound()=if_expr.false_case();
246
247 member_exprt member_true = to_member_expr(expr);
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
259 member_exprt pushed_in_member = to_member_expr(expr);
260 pushed_in_member.op() = to_let_expr(op).where();
261 auto new_expr = op;
262 to_let_expr(new_expr).where() = pushed_in_member;
263 to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
264
265 return changed(simplify_rec(new_expr));
266 }
267
268 return unchanged(expr);
269}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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
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
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
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
const exprt & struct_op() const
Definition: std_expr.h:2697
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
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:70
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:40
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
exprt & old()
Definition: std_expr.h:2508
exprt::operandst & designator()
Definition: std_expr.h:2522
exprt & new_value()
Definition: std_expr.h:2532
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & new_value()
Definition: std_expr.h:2342
exprt & where()
Definition: std_expr.h:2332
nonstd::optional< T > optionalt
Definition: optional.h:35
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)
BigInt mp_integer
Definition: smt_terms.h:12
#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