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 
19 {
20  if(expr.operands().size()!=1)
21  return true;
22 
23  const irep_idt &component_name=
25 
26  exprt &op=expr.op0();
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 &operands=op.operands();
38 
39  while(operands.size()>1)
40  {
41  exprt &op1=operands[operands.size()-2];
42  exprt &op2=operands[operands.size()-1];
43 
44  if(op1.get(ID_component_name)==component_name)
45  {
46  // found it!
47  exprt tmp;
48  tmp.swap(op2);
49  expr.swap(tmp);
50 
51  // do this recursively
52  simplify_rec(expr);
53 
54  return false;
55  }
56  else // something else, get rid of it
57  operands.resize(operands.size()-2);
58  }
59 
60  if(op.operands().size()==1)
61  {
62  exprt tmp;
63  tmp.swap(op.op0());
64  op.swap(tmp);
65  // do this recursively
66  simplify_member(expr);
67  }
68 
69  return false;
70  }
71  else if(op_type.id()==ID_union)
72  {
73  const with_exprt &with_expr=to_with_expr(op);
74 
75  if(with_expr.where().get(ID_component_name)==component_name)
76  {
77  // WITH(s, .m, v).m -> v
78  expr=with_expr.new_value();
79 
80  // do this recursively
81  simplify_rec(expr);
82 
83  return false;
84  }
85  }
86  }
87  else if(op.id()==ID_update)
88  {
89  if(op.operands().size()==3 &&
90  op_type.id()==ID_struct)
91  {
92  const update_exprt &update_expr=to_update_expr(op);
93  const exprt::operandst &designator=update_expr.designator();
94 
95  // look at very first designator
96  if(designator.size()==1 &&
97  designator.front().id()==ID_member_designator)
98  {
99  if(designator.front().get(ID_component_name)==component_name)
100  {
101  // UPDATE(s, .m, v).m -> v
102  exprt tmp=update_expr.new_value();
103  expr.swap(tmp);
104 
105  // do this recursively
106  simplify_rec(expr);
107 
108  return false;
109  }
110  // the following optimization only works on structs,
111  // and not on unions
112  else if(op_type.id()==ID_struct)
113  {
114  // UPDATE(s, .m1, v).m2 -> s.m2
115  exprt tmp=update_expr.old();
116  op.swap(tmp);
117 
118  // do this recursively
119  simplify_rec(expr);
120 
121  return false;
122  }
123  }
124  }
125  }
126  else if(op.id()==ID_struct ||
127  op.id()==ID_constant)
128  {
129  if(op_type.id()==ID_struct)
130  {
131  // pull out the right member
132  const struct_typet &struct_type=to_struct_type(op_type);
133  if(struct_type.has_component(component_name))
134  {
135  std::size_t number=struct_type.component_number(component_name);
136  exprt tmp;
137  tmp.swap(op.operands()[number]);
138  expr.swap(tmp);
139  return false;
140  }
141  }
142  }
143  else if(op.id()==ID_byte_extract_little_endian ||
144  op.id()==ID_byte_extract_big_endian)
145  {
146  if(op_type.id()==ID_struct)
147  {
148  // This rewrites byte_extract(s, o, struct_type).member
149  // to byte_extract(s, o+member_offset, member_type)
150 
151  const struct_typet &struct_type=to_struct_type(op_type);
152  const struct_typet::componentt &component=
153  struct_type.get_component(component_name);
154 
155  if(component.is_nil() || component.type().id()==ID_c_bit_field)
156  return true;
157 
158  // add member offset to index
159  mp_integer offset_int=member_offset(struct_type, component_name, ns);
160  if(offset_int==-1)
161  return true;
162 
163  const exprt &struct_offset=op.op1();
164  exprt member_offset=from_integer(offset_int, struct_offset.type());
165  plus_exprt final_offset(struct_offset, member_offset);
166  simplify_node(final_offset);
167 
168  byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type());
169  expr.swap(result);
170 
171  simplify_rec(expr);
172 
173  return false;
174  }
175  }
176  else if(op.id()==ID_union && op_type.id()==ID_union)
177  {
178  // trivial?
179  if(ns.follow(to_union_expr(op).op().type())==ns.follow(expr.type()))
180  {
181  exprt tmp=to_union_expr(op).op();
182  expr.swap(tmp);
183  return false;
184  }
185 
186  // need to convert!
187  mp_integer target_size=
188  pointer_offset_size(expr.type(), ns);
189 
190  if(target_size!=-1)
191  {
192  mp_integer target_bits=target_size*8;
193  const auto bits=expr2bits(op, true);
194 
195  if(bits.has_value() &&
196  mp_integer(bits->size())>=target_bits)
197  {
198  std::string bits_cut=std::string(*bits, 0, integer2size_t(target_bits));
199 
200  exprt tmp=bits2expr(bits_cut, expr.type(), true);
201 
202  if(tmp.is_not_nil())
203  {
204  expr=tmp;
205  return false;
206  }
207  }
208  }
209  }
210  else if(op.id() == ID_typecast)
211  {
212  // Try to look through member(cast(x)) if the cast is between structurally
213  // identical types:
214  if(base_type_eq(op_type, op.op0().type(), ns))
215  {
216  expr.op0() = op.op0();
217  simplify_member(expr);
218  return false;
219  }
220  }
221  else if(op.id()==ID_if)
222  {
223  const if_exprt &if_expr=to_if_expr(op);
224  exprt cond=if_expr.cond();
225 
226  member_exprt member_false=to_member_expr(expr);
227  member_false.compound()=if_expr.false_case();
228 
229  to_member_expr(expr).compound()=if_expr.true_case();
230 
231  expr=if_exprt(cond, expr, member_false, expr.type());
232  simplify_rec(expr);
233 
234  return false;
235  }
236 
237  return true;
238 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
bool simplify_member(exprt &expr)
exprt & true_case()
Definition: std_expr.h:3393
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:72
Operator to update elements in structs and arrays.
Definition: std_expr.h:3670
const exprt & op() const
Definition: std_expr.h:340
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
exprt::operandst & designator()
Definition: std_expr.h:3708
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
exprt & new_value()
Definition: std_expr.h:3496
typet & type()
Definition: expr.h:56
Structure type.
Definition: std_types.h:297
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
Definition: std_expr.h:3869
const exprt & compound() const
Definition: std_expr.h:3920
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
exprt & old()
Definition: std_expr.h:3694
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3739
API to expression classes.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
The plus expression.
Definition: std_expr.h:893
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
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:33
exprt & false_case()
Definition: std_expr.h:3403
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:255
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3517
bool simplify_rec(exprt &expr)
Base class for all expressions.
Definition: expr.h:42
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1782
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
const namespacet & ns
irep_idt get_component_name() const
Definition: std_expr.h:3893
void swap(irept &irep)
Definition: irep.h:303
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
exprt & new_value()
Definition: std_expr.h:3718
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
exprt & where()
Definition: std_expr.h:3486
Base Type Computation.
operandst & operands()
Definition: expr.h:66
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const componentt & get_component(const irep_idt &component_name) const
Definition: std_types.cpp:51