CBMC
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 "config.h"
15 #include "expr_util.h"
16 #include "invariant.h"
17 #include "namespace.h"
18 #include "pointer_offset_size.h"
19 #include "simplify_utils.h"
20 #include "std_expr.h"
21 
24 {
25  const irep_idt &component_name=
27 
28  const exprt &op = expr.compound();
29 
30  if(op.id()==ID_with)
31  {
32  // the following optimization only works on structs,
33  // and not on unions
34 
35  if(
36  op.operands().size() >= 3 &&
37  (op.type().id() == ID_struct || op.type().id() == ID_struct_tag))
38  {
39  exprt::operandst new_operands = op.operands();
40 
41  while(new_operands.size() > 1)
42  {
43  exprt &op1 = new_operands[new_operands.size() - 2];
44  exprt &op2 = new_operands[new_operands.size() - 1];
45 
46  if(op1.get(ID_component_name)==component_name)
47  {
48  // found it!
50  op2.type() == expr.type(),
51  "member expression type must match component type");
52 
53  return op2;
54  }
55  else // something else, get rid of it
56  new_operands.resize(new_operands.size() - 2);
57  }
58 
59  DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
60 
61  auto new_member_expr = expr;
62  new_member_expr.struct_op() = new_operands.front();
63  // do this recursively
64  return changed(simplify_member(new_member_expr));
65  }
66  else if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
67  {
68  const with_exprt &with_expr=to_with_expr(op);
69 
70  if(with_expr.where().get(ID_component_name)==component_name)
71  {
72  // WITH(s, .m, v).m -> v
73  return with_expr.new_value();
74  }
75  }
76  }
77  else if(op.id()==ID_update)
78  {
79  if(
80  op.operands().size() == 3 &&
81  (op.type().id() == ID_struct || op.type().id() == ID_struct_tag))
82  {
83  const update_exprt &update_expr=to_update_expr(op);
84  const exprt::operandst &designator=update_expr.designator();
85 
86  // look at very first designator
87  if(designator.size()==1 &&
88  designator.front().id()==ID_member_designator)
89  {
90  if(designator.front().get(ID_component_name)==component_name)
91  {
92  // UPDATE(s, .m, v).m -> v
93  return update_expr.new_value();
94  }
95  // the following optimization only works on structs,
96  // and not on unions
97  else if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
98  {
99  // UPDATE(s, .m1, v).m2 -> s.m2
100  auto new_expr = expr;
101  new_expr.struct_op() = update_expr.old();
102 
103  // do this recursively
104  return changed(simplify_member(new_expr));
105  }
106  }
107  }
108  }
109  else if(op.id() == ID_struct)
110  {
111  // pull out the right member
112  const struct_typet &struct_type =
113  op.type().id() == ID_struct_tag
115  : to_struct_type(op.type());
116  if(struct_type.has_component(component_name))
117  {
118  std::size_t number = struct_type.component_number(component_name);
120  op.operands().size() > number,
121  "struct expression must have sufficiently many operands");
123  op.operands()[number].type() == expr.type(),
124  "member expression type must match component type");
125  return op.operands()[number];
126  }
127  }
128  else if(op.id()==ID_byte_extract_little_endian ||
129  op.id()==ID_byte_extract_big_endian)
130  {
131  const auto &byte_extract_expr = to_byte_extract_expr(op);
132 
133  if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
134  {
135  // This rewrites byte_extract(s, o, struct_type).member
136  // to byte_extract(s, o+member_offset, member_type)
137 
138  const struct_typet &struct_type =
139  op.type().id() == ID_struct_tag
141  : to_struct_type(op.type());
143  struct_type.get_component(component_name);
144 
145  if(
146  component.is_nil() || component.type().id() == ID_c_bit_field ||
147  component.is_boolean())
148  {
149  return unchanged(expr);
150  }
151 
152  // add member offset to index
153  auto offset_int = member_offset(struct_type, component_name, ns);
154  if(!offset_int.has_value())
155  return unchanged(expr);
156 
157  const exprt &struct_offset = byte_extract_expr.offset();
158  exprt member_offset = from_integer(*offset_int, struct_offset.type());
159  exprt final_offset =
160  simplify_plus(plus_exprt(struct_offset, member_offset));
161 
162  byte_extract_exprt result(
163  op.id(),
164  byte_extract_expr.op(),
165  final_offset,
166  byte_extract_expr.get_bits_per_byte(),
167  expr.type());
168 
169  return changed(simplify_byte_extract(result)); // recursive call
170  }
171  else if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
172  {
173  // rewrite byte_extract(X, 0).member to X
174  // if the type of X is that of the member
175  if(byte_extract_expr.offset().is_zero())
176  {
177  const union_typet &union_type =
178  op.type().id() == ID_union_tag
180  : to_union_type(op.type());
181  const typet &subtype = union_type.component_type(component_name);
182 
183  if(subtype == byte_extract_expr.op().type())
184  return byte_extract_expr.op();
185  }
186  }
187  }
188  else if(
189  op.id() == ID_union &&
190  (op.type().id() == ID_union || op.type().id() == ID_union_tag))
191  {
192  // trivial?
193  if(to_union_expr(op).op().type() == expr.type())
194  return to_union_expr(op).op();
195 
196  // need to convert!
197  auto target_size = pointer_offset_size(expr.type(), ns);
198 
199  if(target_size.has_value())
200  {
201  mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
202  const auto bits = expr2bits(op, true, ns);
203 
204  if(bits.has_value() &&
205  mp_integer(bits->size())>=target_bits)
206  {
207  std::string bits_cut =
208  std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
209 
210  auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
211 
212  if(tmp.has_value())
213  return std::move(*tmp);
214  }
215  }
216  }
217  else if(op.id() == ID_typecast)
218  {
219  const auto &typecast_expr = to_typecast_expr(op);
220 
221  // Try to look through member(cast(x)) if the cast is between structurally
222  // identical types:
223  if(op.type() == typecast_expr.op().type())
224  {
225  auto new_expr = expr;
226  new_expr.struct_op() = typecast_expr.op();
227  return changed(simplify_member(new_expr));
228  }
229 
230  // Try to translate into an equivalent member (perhaps nested) of the type
231  // being cast (for example, this might turn ((struct A)x).field1 into
232  // x.substruct.othersubstruct.field2, if field1 and field2 have the same
233  // type and offset with respect to x.
234  if(op.type().id() == ID_struct || op.type().id() == ID_struct_tag)
235  {
236  const struct_typet &struct_type =
237  op.type().id() == ID_struct_tag
239  : to_struct_type(op.type());
240  std::optional<mp_integer> requested_offset =
241  member_offset(struct_type, component_name, ns);
242  if(requested_offset.has_value())
243  {
244  auto equivalent_member = get_subexpression_at_offset(
245  typecast_expr.op(), *requested_offset, expr.type(), ns);
246 
247  // Guess: turning this into a byte-extract operation is not really an
248  // optimisation.
249  if(
250  equivalent_member.has_value() &&
251  equivalent_member.value().id() != ID_byte_extract_little_endian &&
252  equivalent_member.value().id() != ID_byte_extract_big_endian)
253  {
254  auto tmp = equivalent_member.value();
255  return changed(simplify_rec(tmp));
256  }
257  }
258  }
259  }
260  else if(op.id() == ID_let)
261  {
262  // Push a member operator inside a let binding, to avoid the let bisecting
263  // structures we otherwise know how to analyse, such as
264  // (let x = 1 in ({x, x})).field1 --> let x = 1 in ({x, x}.field1) -->
265  // let x = 1 in x
266  member_exprt pushed_in_member = to_member_expr(expr);
267  pushed_in_member.op() = to_let_expr(op).where();
268  auto new_expr = op;
269  to_let_expr(new_expr).where() = pushed_in_member;
270  to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
271 
272  return changed(simplify_rec(new_expr));
273  }
274 
275  return unchanged(expr);
276 }
277 
280 {
281  const exprt &compound = expr.compound();
282 
283  if(compound.id() == ID_if)
284  {
285  if_exprt if_expr = lift_if(expr, 0);
286  return changed(simplify_if_preorder(if_expr));
287  }
288  else
289  {
290  auto r_it = simplify_rec(compound); // recursive call
291  if(r_it.has_changed())
292  {
293  auto tmp = expr;
294  tmp.compound() = r_it.expr;
295  return tmp;
296  }
297  }
298 
299  return unchanged(expr);
300 }
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_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
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:38
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:2370
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:384
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3289
Extract member of struct or union.
Definition: std_expr.h:2841
const exprt & compound() const
Definition: std_expr.h:2890
const exprt & struct_op() const
Definition: std_expr.h:2879
irep_idt get_component_name() const
Definition: std_expr.h:2863
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
const namespacet & ns
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_member_preorder(const member_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 &)
resultt simplify_if_preorder(const if_exprt &expr)
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:76
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:63
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:46
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
The union type.
Definition: c_types.h:147
Operator to update elements in structs and arrays.
Definition: std_expr.h:2655
exprt::operandst & designator()
Definition: std_expr.h:2681
exprt & old()
Definition: std_expr.h:2667
exprt & new_value()
Definition: std_expr.h:2691
Operator to update elements in structs and arrays.
Definition: std_expr.h:2471
exprt & new_value()
Definition: std_expr.h:2501
exprt & where()
Definition: std_expr.h:2491
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
Deprecated expression utility functions.
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#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:80
API to expression classes.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2735
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3320
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1811
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2533
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
std::size_t char_width
Definition: config.h:140