cprover
simplify_expr_struct.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
10 
11 #include "arith_tools.h"
12 #include "base_type.h"
13 #include "byte_operators.h"
14 #include "namespace.h"
15 #include "pointer_offset_size.h"
16 #include "std_expr.h"
17 #include "type_eq.h"
18 
20 {
21  if(expr.operands().size()!=1)
22  return true;
23 
24  const irep_idt &component_name=
26 
27  exprt &op=expr.op0();
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  {
38  exprt::operandst &operands=op.operands();
39 
40  while(operands.size()>1)
41  {
42  exprt &op1=operands[operands.size()-2];
43  exprt &op2=operands[operands.size()-1];
44 
45  if(op1.get(ID_component_name)==component_name)
46  {
47  // found it!
48  exprt tmp;
49  tmp.swap(op2);
50  expr.swap(tmp);
51 
52  // do this recursively
53  simplify_rec(expr);
54 
55  return false;
56  }
57  else // something else, get rid of it
58  operands.resize(operands.size()-2);
59  }
60 
61  if(op.operands().size()==1)
62  {
63  exprt tmp;
64  tmp.swap(op.op0());
65  op.swap(tmp);
66  // do this recursively
67  simplify_member(expr);
68  }
69 
70  return false;
71  }
72  else if(op_type.id()==ID_union)
73  {
74  const with_exprt &with_expr=to_with_expr(op);
75 
76  if(with_expr.where().get(ID_component_name)==component_name)
77  {
78  // WITH(s, .m, v).m -> v
79  expr=with_expr.new_value();
80 
81  // do this recursively
82  simplify_rec(expr);
83 
84  return false;
85  }
86  }
87  }
88  else if(op.id()==ID_update)
89  {
90  if(op.operands().size()==3 &&
91  op_type.id()==ID_struct)
92  {
93  const update_exprt &update_expr=to_update_expr(op);
94  const exprt::operandst &designator=update_expr.designator();
95 
96  // look at very first designator
97  if(designator.size()==1 &&
98  designator.front().id()==ID_member_designator)
99  {
100  if(designator.front().get(ID_component_name)==component_name)
101  {
102  // UPDATE(s, .m, v).m -> v
103  exprt tmp=update_expr.new_value();
104  expr.swap(tmp);
105 
106  // do this recursively
107  simplify_rec(expr);
108 
109  return false;
110  }
111  // the following optimization only works on structs,
112  // and not on unions
113  else if(op_type.id()==ID_struct)
114  {
115  // UPDATE(s, .m1, v).m2 -> s.m2
116  exprt tmp=update_expr.old();
117  op.swap(tmp);
118 
119  // do this recursively
120  simplify_rec(expr);
121 
122  return false;
123  }
124  }
125  }
126  }
127  else if(op.id()==ID_struct ||
128  op.id()==ID_constant)
129  {
130  if(op_type.id()==ID_struct)
131  {
132  // pull out the right member
133  const struct_typet &struct_type=to_struct_type(op_type);
134  if(struct_type.has_component(component_name))
135  {
136  std::size_t number=struct_type.component_number(component_name);
137  exprt tmp;
138  tmp.swap(op.operands()[number]);
139  expr.swap(tmp);
140  return false;
141  }
142  }
143  }
144  else if(op.id()==ID_byte_extract_little_endian ||
145  op.id()==ID_byte_extract_big_endian)
146  {
147  if(op_type.id()==ID_struct)
148  {
149  // This rewrites byte_extract(s, o, struct_type).member
150  // to byte_extract(s, o+member_offset, member_type)
151 
152  const struct_typet &struct_type=to_struct_type(op_type);
154  struct_type.get_component(component_name);
155 
156  if(
157  component.is_nil() || component.type().id() == ID_c_bit_field ||
158  component.type().id() == ID_bool)
159  {
160  return true;
161  }
162 
163  // add member offset to index
164  auto offset_int = member_offset(struct_type, component_name, ns);
165  if(!offset_int.has_value())
166  return true;
167 
168  const exprt &struct_offset=op.op1();
169  exprt member_offset = from_integer(*offset_int, struct_offset.type());
170  plus_exprt final_offset(struct_offset, member_offset);
171  simplify_node(final_offset);
172 
173  byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type());
174  expr.swap(result);
175 
176  simplify_rec(expr);
177 
178  return false;
179  }
180  else if(op_type.id() == ID_union)
181  {
182  // rewrite byte_extract(X, 0).member to X
183  // if the type of X is that of the member
184  const auto &byte_extract_expr = to_byte_extract_expr(op);
185  if(byte_extract_expr.offset().is_zero())
186  {
187  const union_typet &union_type = to_union_type(op_type);
188  const typet &subtype = union_type.component_type(component_name);
189 
190  if(subtype == byte_extract_expr.op().type())
191  {
192  exprt tmp = byte_extract_expr.op();
193  expr.swap(tmp);
194 
195  return false;
196  }
197  }
198  }
199  }
200  else if(op.id()==ID_union && op_type.id()==ID_union)
201  {
202  // trivial?
203  if(ns.follow(to_union_expr(op).op().type())==ns.follow(expr.type()))
204  {
205  exprt tmp=to_union_expr(op).op();
206  expr.swap(tmp);
207  return false;
208  }
209 
210  // need to convert!
211  auto target_size = pointer_offset_size(expr.type(), ns);
212 
213  if(target_size.has_value())
214  {
215  mp_integer target_bits = target_size.value() * 8;
216  const auto bits=expr2bits(op, true);
217 
218  if(bits.has_value() &&
219  mp_integer(bits->size())>=target_bits)
220  {
221  std::string bits_cut =
222  std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
223 
224  exprt tmp=bits2expr(bits_cut, expr.type(), true);
225 
226  if(tmp.is_not_nil())
227  {
228  expr=tmp;
229  return false;
230  }
231  }
232  }
233  }
234  else if(op.id() == ID_typecast)
235  {
236  // Try to look through member(cast(x)) if the cast is between structurally
237  // identical types:
238  if(base_type_eq(op_type, op.op0().type(), ns))
239  {
240  expr.op0() = op.op0();
241  simplify_member(expr);
242  return false;
243  }
244 
245  // Try to translate into an equivalent member (perhaps nested) of the type
246  // being cast (for example, this might turn ((struct A)x).field1 into
247  // x.substruct.othersubstruct.field2, if field1 and field2 have the same
248  // type and offset with respect to x.
249  if(op_type.id() == ID_struct)
250  {
251  optionalt<mp_integer> requested_offset =
252  member_offset(to_struct_type(op_type), component_name, ns);
253  if(requested_offset.has_value())
254  {
255  exprt equivalent_member = get_subexpression_at_offset(
256  op.op0(), *requested_offset, expr.type(), ns);
257 
258  // Guess: turning this into a byte-extract operation is not really an
259  // optimisation.
260  // The type_eq check is because get_subexpression_at_offset uses
261  // base_type_eq, whereas in the context of a simplifier we should not
262  // change the type of the expression.
263  if(
264  equivalent_member.is_not_nil() &&
265  equivalent_member.id() != ID_byte_extract_little_endian &&
266  equivalent_member.id() != ID_byte_extract_big_endian &&
267  type_eq(equivalent_member.type(), expr.type(), ns))
268  {
269  expr = equivalent_member;
270  simplify_rec(expr);
271  return false;
272  }
273  }
274  }
275  }
276  else if(op.id()==ID_if)
277  {
278  const if_exprt &if_expr=to_if_expr(op);
279  exprt cond=if_expr.cond();
280 
281  member_exprt member_false=to_member_expr(expr);
282  member_false.compound()=if_expr.false_case();
283 
284  to_member_expr(expr).compound()=if_expr.true_case();
285 
286  expr=if_exprt(cond, expr, member_false, expr.type());
287  simplify_rec(expr);
288 
289  return false;
290  }
291 
292  return true;
293 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
Definition: type_eq.cpp:31
The type of an expression, extends irept.
Definition: type.h:27
bool simplify_member(exprt &expr)
exprt & true_case()
Definition: std_expr.h:3455
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
BigInt mp_integer
Definition: mp_arith.h:22
bool is_not_nil() const
Definition: irep.h:173
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
const exprt & op() const
Definition: std_expr.h:371
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
Type equality.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
exprt::operandst & designator()
Definition: std_expr.h:3743
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
exprt & new_value()
Definition: std_expr.h:3552
typet & type()
Return the type of the expression.
Definition: expr.h:68
Structure type, corresponds to C style structs.
Definition: std_types.h:276
Extract member of struct or union.
Definition: std_expr.h:3890
const exprt & compound() const
Definition: std_expr.h:3942
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
exprt & old()
Definition: std_expr.h:3729
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3770
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
exprt & false_case()
Definition: std_expr.h:3465
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
std::vector< exprt > operandst
Definition: expr.h:57
Pointer Logic.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3569
bool simplify_rec(exprt &expr)
Base class for all expressions.
Definition: expr.h:54
The union type.
Definition: std_types.h:425
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:35
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
const namespacet & ns
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
irep_idt get_component_name() const
Definition: std_expr.h:3915
void swap(irept &irep)
Definition: irep.h:303
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
exprt & new_value()
Definition: std_expr.h:3753
exprt & where()
Definition: std_expr.h:3542
Base Type Computation.
operandst & operands()
Definition: expr.h:78
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53