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 <cassert>
12 
13 #include "expr.h"
14 #include "namespace.h"
15 #include "std_expr.h"
16 #include "pointer_offset_size.h"
17 #include "arith_tools.h"
18 
20 {
21  if(expr.operands().size()!=1)
22  return true;
23 
24  const irep_idt &component_name=
26 
27  exprt &op=expr.op0();
28  const typet &op_type=ns.follow(op.type());
29 
30  if(op.id()==ID_with)
31  {
32  // the following optimization only works on structs,
33  // and not on unions
34 
35  if(op.operands().size()>=3 &&
36  op_type.id()==ID_struct)
37  {
38  exprt::operandst &operands=op.operands();
39 
40  while(operands.size()>1)
41  {
42  exprt &op1=operands[operands.size()-2];
43  exprt &op2=operands[operands.size()-1];
44 
45  if(op1.get(ID_component_name)==component_name)
46  {
47  // found it!
48  exprt tmp;
49  tmp.swap(op2);
50  expr.swap(tmp);
51 
52  // do this recursively
53  simplify_rec(expr);
54 
55  return false;
56  }
57  else // something else, get rid of it
58  operands.resize(operands.size()-2);
59  }
60 
61  if(op.operands().size()==1)
62  {
63  exprt tmp;
64  tmp.swap(op.op0());
65  op.swap(tmp);
66  // do this recursively
67  simplify_member(expr);
68  }
69 
70  return false;
71  }
72  else if(op_type.id()==ID_union)
73  {
74  const with_exprt &with_expr=to_with_expr(op);
75 
76  if(with_expr.where().get(ID_component_name)==component_name)
77  {
78  // WITH(s, .m, v).m -> v
79  expr=with_expr.new_value();
80 
81  // do this recursively
82  simplify_rec(expr);
83 
84  return false;
85  }
86  }
87  }
88  else if(op.id()==ID_update)
89  {
90  if(op.operands().size()==3 &&
91  op_type.id()==ID_struct)
92  {
93  const update_exprt &update_expr=to_update_expr(op);
94  const exprt::operandst &designator=update_expr.designator();
95 
96  // look at very first designator
97  if(designator.size()==1 &&
98  designator.front().id()==ID_member_designator)
99  {
100  if(designator.front().get(ID_component_name)==component_name)
101  {
102  // UPDATE(s, .m, v).m -> v
103  exprt tmp=update_expr.new_value();
104  expr.swap(tmp);
105 
106  // do this recursively
107  simplify_rec(expr);
108 
109  return false;
110  }
111  // the following optimization only works on structs,
112  // and not on unions
113  else if(op_type.id()==ID_struct)
114  {
115  // UPDATE(s, .m1, v).m2 -> s.m2
116  exprt tmp=update_expr.old();
117  op.swap(tmp);
118 
119  // do this recursively
120  simplify_rec(expr);
121 
122  return false;
123  }
124  }
125  }
126  }
127  else if(op.id()==ID_struct ||
128  op.id()==ID_constant)
129  {
130  if(op_type.id()==ID_struct)
131  {
132  // pull out the right member
133  const struct_typet &struct_type=to_struct_type(op_type);
134  if(struct_type.has_component(component_name))
135  {
136  std::size_t number=struct_type.component_number(component_name);
137  exprt tmp;
138  tmp.swap(op.operands()[number]);
139  expr.swap(tmp);
140  return false;
141  }
142  }
143  }
144  else if(op.id()==ID_byte_extract_little_endian ||
145  op.id()==ID_byte_extract_big_endian)
146  {
147  if(op_type.id()==ID_struct)
148  {
149  // This rewrites byte_extract(s, o, struct_type).member
150  // to byte_extract(s, o+member_offset, member_type)
151 
152  const struct_typet &struct_type=to_struct_type(op_type);
153  const struct_typet::componentt &component=
154  struct_type.get_component(component_name);
155 
156  if(component.is_nil() || component.type().id()==ID_c_bit_field)
157  return true;
158 
159  // add member offset to index
160  mp_integer offset_int=member_offset(struct_type, component_name, ns);
161  if(offset_int==-1)
162  return true;
163 
164  const exprt &struct_offset=op.op1();
165  exprt member_offset=from_integer(offset_int, struct_offset.type());
166  plus_exprt final_offset(struct_offset, member_offset);
167  simplify_node(final_offset);
168 
169  exprt result(op.id(), expr.type());
170  result.copy_to_operands(op.op0(), final_offset);
171  expr.swap(result);
172 
173  simplify_rec(expr);
174 
175  return false;
176  }
177  }
178  else if(op.id()==ID_union && op_type.id()==ID_union)
179  {
180  // trivial?
181  if(ns.follow(to_union_expr(op).op().type())==ns.follow(expr.type()))
182  {
183  exprt tmp=to_union_expr(op).op();
184  expr.swap(tmp);
185  return false;
186  }
187 
188  // need to convert!
189  mp_integer target_size=
190  pointer_offset_size(expr.type(), ns);
191 
192  if(target_size!=-1)
193  {
194  mp_integer target_bits=target_size*8;
195  std::string bits=expr2bits(op, true);
196 
197  if(mp_integer(bits.size())>=target_bits)
198  {
199  std::string bits_cut=std::string(bits, 0, integer2size_t(target_bits));
200 
201  exprt tmp=bits2expr(bits_cut, expr.type(), true);
202 
203  if(tmp.is_not_nil())
204  {
205  expr=tmp;
206  return false;
207  }
208  }
209  }
210  }
211  else if(op.id()==ID_if)
212  {
213  const if_exprt &if_expr=to_if_expr(op);
214  exprt cond=if_expr.cond();
215 
216  member_exprt member_false=to_member_expr(expr);
217  member_false.compound()=if_expr.false_case();
218 
219  to_member_expr(expr).compound()=if_expr.true_case();
220 
221  expr=if_exprt(cond, expr, member_false, expr.type());
222  simplify_rec(expr);
223 
224  return false;
225  }
226 
227  return true;
228 }
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:2919
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
bool simplify_member(exprt &expr)
exprt & true_case()
Definition: std_expr.h:2805
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
Operator to update elements in structs and arrays.
Definition: std_expr.h:3039
const exprt & op() const
Definition: std_expr.h:258
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
exprt::operandst & designator()
Definition: std_expr.h:3077
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
std::string expr2bits(const exprt &expr, bool little_endian)
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
exprt & new_value()
Definition: std_expr.h:2898
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Extract member of struct or union.
Definition: std_expr.h:3214
const exprt & compound() const
Definition: std_expr.h:3281
const irep_idt & id() const
Definition: irep.h:189
exprt & old()
Definition: std_expr.h:3063
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3108
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
The plus expression.
Definition: std_expr.h:702
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
exprt & false_case()
Definition: std_expr.h:2815
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:252
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
bool simplify_rec(exprt &expr)
Base class for all expressions.
Definition: expr.h:46
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
const namespacet & ns
irep_idt get_component_name() const
Definition: std_expr.h:3249
void swap(irept &irep)
Definition: irep.h:231
exprt & new_value()
Definition: std_expr.h:3087
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
exprt & where()
Definition: std_expr.h:2888
operandst & operands()
Definition: expr.h:70
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