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  std::string bits=expr2bits(op, true);
194 
195  if(mp_integer(bits.size())>=target_bits)
196  {
197  std::string bits_cut=std::string(bits, 0, integer2size_t(target_bits));
198 
199  exprt tmp=bits2expr(bits_cut, expr.type(), true);
200 
201  if(tmp.is_not_nil())
202  {
203  expr=tmp;
204  return false;
205  }
206  }
207  }
208  }
209  else if(op.id() == ID_typecast)
210  {
211  // Try to look through member(cast(x)) if the cast is between structurally
212  // identical types:
213  if(base_type_eq(op_type, op.op0().type(), ns))
214  {
215  expr.op0() = op.op0();
216  simplify_member(expr);
217  return false;
218  }
219  }
220  else if(op.id()==ID_if)
221  {
222  const if_exprt &if_expr=to_if_expr(op);
223  exprt cond=if_expr.cond();
224 
225  member_exprt member_false=to_member_expr(expr);
226  member_false.compound()=if_expr.false_case();
227 
228  to_member_expr(expr).compound()=if_expr.true_case();
229 
230  expr=if_exprt(cond, expr, member_false, expr.type());
231  simplify_rec(expr);
232 
233  return false;
234  }
235 
236  return true;
237 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
bool simplify_member(exprt &expr)
exprt & true_case()
Definition: std_expr.h:3395
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:72
Operator to update elements in structs and arrays.
Definition: std_expr.h:3672
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:3710
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::string expr2bits(const exprt &expr, bool little_endian)
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
exprt & new_value()
Definition: std_expr.h:3498
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:3871
const exprt & compound() const
Definition: std_expr.h:3922
const irep_idt & id() const
Definition: irep.h:189
Expression classes for byte-level operators.
exprt & old()
Definition: std_expr.h:3696
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3741
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:3955
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)
exprt & false_case()
Definition: std_expr.h:3405
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:3519
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:3461
const namespacet & ns
irep_idt get_component_name() const
Definition: std_expr.h:3895
void swap(irept &irep)
Definition: irep.h:231
exprt & new_value()
Definition: std_expr.h:3720
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
exprt & where()
Definition: std_expr.h:3488
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