cprover
simplify_expr_array.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 "replace_expr.h"
17 #include "arith_tools.h"
18 #include "pointer_offset_size.h"
19 
21 {
22  bool result=true;
23 
24  // extra arithmetic optimizations
25  const exprt &index=to_index_expr(expr).index();
26  const exprt &array=to_index_expr(expr).array();
27 
28  if(index.id()==ID_div &&
29  index.operands().size()==2)
30  {
31  if(index.op0().id()==ID_mult &&
32  index.op0().operands().size()==2 &&
33  index.op0().op1()==index.op1())
34  {
35  exprt tmp=index.op0().op0();
36  expr.op1()=tmp;
37  result=false;
38  }
39  else if(index.op0().id()==ID_mult &&
40  index.op0().operands().size()==2 &&
41  index.op0().op0()==index.op1())
42  {
43  exprt tmp=index.op0().op1();
44  expr.op1()=tmp;
45  result=false;
46  }
47  }
48 
49  if(array.id()==ID_lambda)
50  {
51  // simplify (lambda i: e)(x) to e[i/x]
52 
53  const exprt &lambda_expr=array;
54 
55  if(lambda_expr.operands().size()!=2)
56  return true;
57 
58  if(expr.op1().type()==lambda_expr.op0().type())
59  {
60  exprt tmp=lambda_expr.op1();
61  replace_expr(lambda_expr.op0(), expr.op1(), tmp);
62  expr.swap(tmp);
63  return false;
64  }
65  }
66  else if(array.id()==ID_with)
67  {
68  // we have (a WITH [i:=e])[j]
69 
70  const exprt &with_expr=array;
71 
72  if(with_expr.operands().size()!=3)
73  return true;
74 
75  if(with_expr.op1()==expr.op1())
76  {
77  // simplify (e with [i:=v])[i] to v
78  exprt tmp=with_expr.op2();
79  expr.swap(tmp);
80  return false;
81  }
82  else
83  {
84  // Turn (a with i:=x)[j] into (i==j)?x:a[j].
85  // watch out that the type of i and j might be different.
86  equal_exprt equality_expr(expr.op1(), with_expr.op1());
87 
88  if(equality_expr.lhs().type()!=equality_expr.rhs().type())
89  equality_expr.rhs().make_typecast(equality_expr.lhs().type());
90 
91  simplify_inequality(equality_expr);
92 
93  index_exprt new_index_expr;
94  new_index_expr.type()=expr.type();
95  new_index_expr.array()=with_expr.op0();
96  new_index_expr.index()=expr.op1();
97 
98  simplify_index(new_index_expr); // recursive call
99 
100  if(equality_expr.is_true())
101  {
102  expr=with_expr.op2();
103  return false;
104  }
105  else if(equality_expr.is_false())
106  {
107  expr.swap(new_index_expr);
108  return false;
109  }
110 
111  if_exprt if_expr(equality_expr, with_expr.op2(), new_index_expr);
112  simplify_if(if_expr);
113 
114  expr.swap(if_expr);
115 
116  return false;
117  }
118  }
119  else if(array.id()==ID_constant ||
120  array.id()==ID_array)
121  {
122  mp_integer i;
123 
124  if(to_integer(expr.op1(), i))
125  {
126  }
127  else if(i<0 || i>=array.operands().size())
128  {
129  // out of bounds
130  }
131  else
132  {
133  // ok
134  exprt tmp=array.operands()[integer2size_t(i)];
135  expr.swap(tmp);
136  return false;
137  }
138  }
139  else if(array.id()==ID_string_constant)
140  {
141  mp_integer i;
142 
143  const irep_idt &value=array.get(ID_value);
144 
145  if(to_integer(expr.op1(), i))
146  {
147  }
148  else if(i<0 || i>value.size())
149  {
150  // out of bounds
151  }
152  else
153  {
154  // terminating zero?
155  char v=(i==value.size())?0:value[integer2size_t(i)];
156  exprt tmp=from_integer(v, expr.type());
157  expr.swap(tmp);
158  return false;
159  }
160  }
161  else if(array.id()==ID_array_of)
162  {
163  if(array.operands().size()==1)
164  {
165  exprt tmp=array.op0();
166  expr.swap(tmp);
167  return false;
168  }
169  }
170  else if(array.id()=="array-list")
171  {
172  // These are index/value pairs, alternating.
173  for(size_t i=0; i<array.operands().size()/2; i++)
174  {
175  exprt tmp_index=array.operands()[i*2];
176  tmp_index.make_typecast(index.type());
177  simplify(tmp_index);
178  if(tmp_index==index)
179  {
180  exprt tmp=array.operands()[i*2+1];
181  expr.swap(tmp);
182  return false;
183  }
184  }
185  }
186  else if(array.id()==ID_byte_extract_little_endian ||
187  array.id()==ID_byte_extract_big_endian)
188  {
189  const typet &array_type=ns.follow(array.type());
190 
191  if(array_type.id()==ID_array)
192  {
193  // This rewrites byte_extract(s, o, array_type)[i]
194  // to byte_extract(s, o+offset, sub_type)
195 
196  mp_integer sub_size=pointer_offset_size(array_type.subtype(), ns);
197  if(sub_size==-1)
198  return true;
199 
200  // add offset to index
201  mult_exprt offset(from_integer(sub_size, array.op1().type()), index);
202  plus_exprt final_offset(array.op1(), offset);
203  simplify_node(final_offset);
204 
205  exprt result(array.id(), expr.type());
206  result.copy_to_operands(array.op0(), final_offset);
207  expr.swap(result);
208 
209  simplify_rec(expr);
210 
211  return false;
212  }
213  }
214  else if(array.id()==ID_if)
215  {
216  const if_exprt &if_expr=to_if_expr(array);
217  exprt cond=if_expr.cond();
218 
219  index_exprt idx_false=to_index_expr(expr);
220  idx_false.array()=if_expr.false_case();
221 
222  to_index_expr(expr).array()=if_expr.true_case();
223 
224  expr=if_exprt(cond, expr, idx_false, expr.type());
225  simplify_rec(expr);
226 
227  return false;
228  }
229 
230  return result;
231 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
BigInt mp_integer
Definition: mp_arith.h:19
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
bool simplify_index(exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
typet & type()
Definition: expr.h:60
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
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
size_t size() const
Definition: dstring.h:77
exprt & false_case()
Definition: std_expr.h:2815
binary multiplication
Definition: std_expr.h:806
Pointer Logic.
bool simplify_rec(exprt &expr)
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
const namespacet & ns
void swap(irept &irep)
Definition: irep.h:231
virtual bool simplify(exprt &expr)
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
array index operator
Definition: std_expr.h:1170