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  exprt tmp;
51  tmp.swap(op2);
52 
53  // do this recursively
54  return changed(simplify_rec(tmp));
55  }
56  else // something else, get rid of it
57  new_operands.resize(new_operands.size() - 2);
58  }
59 
60  DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
61 
62  auto new_member_expr = expr;
63  new_member_expr.struct_op() = new_operands.front();
64  // do this recursively
65  return changed(simplify_member(new_member_expr));
66  }
67  else if(op_type.id()==ID_union)
68  {
69  const with_exprt &with_expr=to_with_expr(op);
70 
71  if(with_expr.where().get(ID_component_name)==component_name)
72  {
73  // WITH(s, .m, v).m -> v
74  auto tmp = with_expr.new_value();
75 
76  // do this recursively
77  return changed(simplify_rec(tmp));
78  }
79  }
80  }
81  else if(op.id()==ID_update)
82  {
83  if(op.operands().size()==3 &&
84  op_type.id()==ID_struct)
85  {
86  const update_exprt &update_expr=to_update_expr(op);
87  const exprt::operandst &designator=update_expr.designator();
88 
89  // look at very first designator
90  if(designator.size()==1 &&
91  designator.front().id()==ID_member_designator)
92  {
93  if(designator.front().get(ID_component_name)==component_name)
94  {
95  // UPDATE(s, .m, v).m -> v
96  exprt tmp=update_expr.new_value();
97 
98  // do this recursively
99  return changed(simplify_rec(tmp));
100  }
101  // the following optimization only works on structs,
102  // and not on unions
103  else if(op_type.id()==ID_struct)
104  {
105  // UPDATE(s, .m1, v).m2 -> s.m2
106  auto new_expr = expr;
107  new_expr.struct_op() = update_expr.old();
108 
109  // do this recursively
110  return changed(simplify_rec(new_expr));
111  }
112  }
113  }
114  }
115  else if(op.id()==ID_struct ||
116  op.id()==ID_constant)
117  {
118  if(op_type.id()==ID_struct)
119  {
120  // pull out the right member
121  const struct_typet &struct_type=to_struct_type(op_type);
122  if(struct_type.has_component(component_name))
123  {
124  std::size_t number=struct_type.component_number(component_name);
126  op.operands()[number].type() == expr.type(),
127  "member expression type must match component type");
128  return op.operands()[number];
129  }
130  }
131  }
132  else if(op.id()==ID_byte_extract_little_endian ||
133  op.id()==ID_byte_extract_big_endian)
134  {
135  const auto &byte_extract_expr = to_byte_extract_expr(op);
136 
137  if(op_type.id()==ID_struct)
138  {
139  // This rewrites byte_extract(s, o, struct_type).member
140  // to byte_extract(s, o+member_offset, member_type)
141 
142  const struct_typet &struct_type=to_struct_type(op_type);
144  struct_type.get_component(component_name);
145 
146  if(
147  component.is_nil() || component.type().id() == ID_c_bit_field ||
148  component.type().id() == ID_bool)
149  {
150  return unchanged(expr);
151  }
152 
153  // add member offset to index
154  auto offset_int = member_offset(struct_type, component_name, ns);
155  if(!offset_int.has_value())
156  return unchanged(expr);
157 
158  const exprt &struct_offset = byte_extract_expr.offset();
159  exprt member_offset = from_integer(*offset_int, struct_offset.type());
160  exprt final_offset =
161  simplify_node(plus_exprt(struct_offset, member_offset));
162 
163  byte_extract_exprt result(
164  op.id(), byte_extract_expr.op(), final_offset, expr.type());
165 
166  return changed(simplify_rec(result)); // recursive call
167  }
168  else if(op_type.id() == ID_union)
169  {
170  // rewrite byte_extract(X, 0).member to X
171  // if the type of X is that of the member
172  if(byte_extract_expr.offset().is_zero())
173  {
174  const union_typet &union_type = to_union_type(op_type);
175  const typet &subtype = union_type.component_type(component_name);
176 
177  if(subtype == byte_extract_expr.op().type())
178  return byte_extract_expr.op();
179  }
180  }
181  }
182  else if(op.id()==ID_union && op_type.id()==ID_union)
183  {
184  // trivial?
185  if(to_union_expr(op).op().type() == expr.type())
186  return to_union_expr(op).op();
187 
188  // need to convert!
189  auto target_size = pointer_offset_size(expr.type(), ns);
190 
191  if(target_size.has_value())
192  {
193  mp_integer target_bits = target_size.value() * 8;
194  const auto bits = expr2bits(op, true, ns);
195 
196  if(bits.has_value() &&
197  mp_integer(bits->size())>=target_bits)
198  {
199  std::string bits_cut =
200  std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
201 
202  auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
203 
204  if(tmp.has_value())
205  return std::move(*tmp);
206  }
207  }
208  }
209  else if(op.id() == ID_typecast)
210  {
211  const auto &typecast_expr = to_typecast_expr(op);
212 
213  // Try to look through member(cast(x)) if the cast is between structurally
214  // identical types:
215  if(op_type == typecast_expr.op().type())
216  {
217  auto new_expr = expr;
218  new_expr.struct_op() = typecast_expr.op();
219  return changed(simplify_member(new_expr));
220  }
221 
222  // Try to translate into an equivalent member (perhaps nested) of the type
223  // being cast (for example, this might turn ((struct A)x).field1 into
224  // x.substruct.othersubstruct.field2, if field1 and field2 have the same
225  // type and offset with respect to x.
226  if(op_type.id() == ID_struct)
227  {
228  optionalt<mp_integer> requested_offset =
229  member_offset(to_struct_type(op_type), component_name, ns);
230  if(requested_offset.has_value())
231  {
232  auto equivalent_member = get_subexpression_at_offset(
233  typecast_expr.op(), *requested_offset, expr.type(), ns);
234 
235  // Guess: turning this into a byte-extract operation is not really an
236  // optimisation.
237  if(
238  equivalent_member.has_value() &&
239  equivalent_member.value().id() != ID_byte_extract_little_endian &&
240  equivalent_member.value().id() != ID_byte_extract_big_endian)
241  {
242  auto tmp = equivalent_member.value();
243  return changed(simplify_rec(tmp));
244  }
245  }
246  }
247  }
248  else if(op.id()==ID_if)
249  {
250  const if_exprt &if_expr=to_if_expr(op);
251  exprt cond=if_expr.cond();
252 
253  member_exprt member_false=to_member_expr(expr);
254  member_false.compound()=if_expr.false_case();
255 
256  member_exprt member_true = to_member_expr(expr);
257  member_true.compound() = if_expr.true_case();
258 
259  auto tmp = if_exprt(cond, member_true, member_false, expr.type());
260  return changed(simplify_rec(tmp));
261  }
262  else if(op.id() == ID_let)
263  {
264  // Push a member operator inside a let binding, to avoid the let bisecting
265  // structures we otherwise know how to analyse, such as
266  // (let x = 1 in ({x, x})).field1 --> let x = 1 in ({x, x}.field1) -->
267  // let x = 1 in x
268  member_exprt pushed_in_member = to_member_expr(expr);
269  pushed_in_member.op() = to_let_expr(op).where();
270  auto new_expr = op;
271  to_let_expr(new_expr).where() = pushed_in_member;
272  to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
273 
274  return changed(simplify_rec(new_expr));
275  }
276 
277  return unchanged(expr);
278 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2462
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2421
simplify_expr_class.h
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2368
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:194
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2202
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
struct_union_typet::component_type
const typet & component_type(const irep_idt &component_name) const
Definition: std_types.cpp:66
exprt
Base class for all expressions.
Definition: expr.h:54
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1562
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
namespace.h
struct_union_typet::component_number
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:36
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:129
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2216
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2568
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2557
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:134
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2928
irept::swap
void swap(irept &irep)
Definition: irep.h:453
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:151
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
union_typet
The union type.
Definition: c_types.h:112
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
simplify_exprt::resultt
Definition: simplify_expr_class.h:96
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2234
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2356
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2382
expr2bits
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:406
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
struct_union_typet::componentt
Definition: std_types.h:63
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:21
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2392
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:605
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
invariant.h
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:244
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
exprt::operands
operandst & operands()
Definition: expr.h:96
simplify_utils.h
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:2897
std_expr.h
API to expression classes.
with_exprt::where
exprt & where()
Definition: std_expr.h:2192
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
c_types.h