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 "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:149
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:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3012
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & compound() const
Definition: std_expr.h:2654
const exprt & struct_op() const
Definition: std_expr.h:2643
irep_idt get_component_name() const
Definition: std_expr.h:2627
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:62
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:49
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:32
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:293
The union type.
Definition: c_types.h:112
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
exprt::operandst & designator()
Definition: std_expr.h:2468
exprt & old()
Definition: std_expr.h:2454
exprt & new_value()
Definition: std_expr.h:2478
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
exprt & new_value()
Definition: std_expr.h:2288
exprt & where()
Definition: std_expr.h:2278
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, 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< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, 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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2507
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3043
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2320
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308