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 "config.h"
15#include "invariant.h"
16#include "namespace.h"
17#include "pointer_offset_size.h"
18#include "simplify_utils.h"
19#include "std_expr.h"
20
23{
24 const irep_idt &component_name=
25 to_member_expr(expr).get_component_name();
26
27 const exprt &op = expr.compound();
28 const typet &op_type=ns.follow(op.type());
29
30 if(op.id()==ID_with)
31 {
32 // the following optimization only works on structs,
33 // and not on unions
34
35 if(op.operands().size()>=3 &&
36 op_type.id()==ID_struct)
37 {
39
40 while(new_operands.size() > 1)
41 {
42 exprt &op1 = new_operands[new_operands.size() - 2];
43 exprt &op2 = new_operands[new_operands.size() - 1];
44
45 if(op1.get(ID_component_name)==component_name)
46 {
47 // found it!
49 op2.type() == expr.type(),
50 "member expression type must match component type");
51
52 return op2;
53 }
54 else // something else, get rid of it
55 new_operands.resize(new_operands.size() - 2);
56 }
57
58 DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
59
60 auto new_member_expr = expr;
61 new_member_expr.struct_op() = new_operands.front();
62 // do this recursively
64 }
65 else if(op_type.id()==ID_union)
66 {
68
69 if(with_expr.where().get(ID_component_name)==component_name)
70 {
71 // WITH(s, .m, v).m -> v
72 return with_expr.new_value();
73 }
74 }
75 }
76 else if(op.id()==ID_update)
77 {
78 if(op.operands().size()==3 &&
79 op_type.id()==ID_struct)
80 {
82 const exprt::operandst &designator=update_expr.designator();
83
84 // look at very first designator
85 if(designator.size()==1 &&
86 designator.front().id()==ID_member_designator)
87 {
88 if(designator.front().get(ID_component_name)==component_name)
89 {
90 // UPDATE(s, .m, v).m -> v
91 return update_expr.new_value();
92 }
93 // the following optimization only works on structs,
94 // and not on unions
95 else if(op_type.id()==ID_struct)
96 {
97 // UPDATE(s, .m1, v).m2 -> s.m2
98 auto new_expr = expr;
99 new_expr.struct_op() = update_expr.old();
100
101 // do this recursively
103 }
104 }
105 }
106 }
107 else if(op.id() == ID_struct)
108 {
109 // pull out the right member
111 if(struct_type.has_component(component_name))
112 {
113 std::size_t number = struct_type.component_number(component_name);
115 op.operands().size() > number,
116 "struct expression must have sufficiently many operands");
118 op.operands()[number].type() == expr.type(),
119 "member expression type must match component type");
120 return op.operands()[number];
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.is_boolean())
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(),
158 byte_extract_expr.get_bits_per_byte(),
159 expr.type());
160
161 return changed(simplify_byte_extract(result)); // recursive call
162 }
163 else if(op_type.id() == ID_union)
164 {
165 // rewrite byte_extract(X, 0).member to X
166 // if the type of X is that of the member
167 if(byte_extract_expr.offset().is_zero())
168 {
170 const typet &subtype = union_type.component_type(component_name);
171
172 if(subtype == byte_extract_expr.op().type())
173 return byte_extract_expr.op();
174 }
175 }
176 }
177 else if(op.id()==ID_union && op_type.id()==ID_union)
178 {
179 // trivial?
180 if(to_union_expr(op).op().type() == expr.type())
181 return to_union_expr(op).op();
182
183 // need to convert!
184 auto target_size = pointer_offset_size(expr.type(), ns);
185
186 if(target_size.has_value())
187 {
188 mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
189 const auto bits = expr2bits(op, true, ns);
190
191 if(bits.has_value() &&
192 mp_integer(bits->size())>=target_bits)
193 {
194 std::string bits_cut =
195 std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
196
197 auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
198
199 if(tmp.has_value())
200 return std::move(*tmp);
201 }
202 }
203 }
204 else if(op.id() == ID_typecast)
205 {
206 const auto &typecast_expr = to_typecast_expr(op);
207
208 // Try to look through member(cast(x)) if the cast is between structurally
209 // identical types:
210 if(op_type == typecast_expr.op().type())
211 {
212 auto new_expr = expr;
213 new_expr.struct_op() = typecast_expr.op();
215 }
216
217 // Try to translate into an equivalent member (perhaps nested) of the type
218 // being cast (for example, this might turn ((struct A)x).field1 into
219 // x.substruct.othersubstruct.field2, if field1 and field2 have the same
220 // type and offset with respect to x.
221 if(op_type.id() == ID_struct)
222 {
224 member_offset(to_struct_type(op_type), component_name, ns);
225 if(requested_offset.has_value())
226 {
228 typecast_expr.op(), *requested_offset, expr.type(), ns);
229
230 // Guess: turning this into a byte-extract operation is not really an
231 // optimisation.
232 if(
233 equivalent_member.has_value() &&
236 {
237 auto tmp = equivalent_member.value();
238 return changed(simplify_rec(tmp));
239 }
240 }
241 }
242 }
243 else if(op.id()==ID_if)
244 {
245 const if_exprt &if_expr=to_if_expr(op);
246 exprt cond=if_expr.cond();
247
249 member_false.compound()=if_expr.false_case();
250
252 member_true.compound() = if_expr.true_case();
253
254 auto tmp = if_exprt(cond, member_true, member_false, expr.type());
255 return changed(simplify_rec(tmp));
256 }
257 else if(op.id() == ID_let)
258 {
259 // Push a member operator inside a let binding, to avoid the let bisecting
260 // structures we otherwise know how to analyse, such as
261 // (let x = 1 in ({x, x})).field1 --> let x = 1 in ({x, x}.field1) -->
262 // let x = 1 in x
264 pushed_in_member.op() = to_let_expr(op).where();
265 auto new_expr = op;
267 to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
268
270 }
271
272 return unchanged(expr);
273}
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2323
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
const exprt & compound() const
Definition std_expr.h:2843
The plus expression Associativity is not specified.
Definition std_expr.h:947
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
The union type.
Definition c_types.h:147
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
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:534
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:77
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3273
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1754
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2486
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2688
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308