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