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  const auto i = numeric_cast<mp_integer>(expr.op1());
120 
121  if(!i.has_value())
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()[numeric_cast_v<std::size_t>(*i)];
132  expr.swap(tmp);
133  return false;
134  }
135  }
136  else if(array.id()==ID_string_constant)
137  {
138  const auto i = numeric_cast<mp_integer>(expr.op1());
139 
140  const irep_idt &value=array.get(ID_value);
141 
142  if(!i.has_value())
143  {
144  }
145  else if(*i < 0 || *i > value.size())
146  {
147  // out of bounds
148  }
149  else
150  {
151  // terminating zero?
152  const char v =
153  (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
154  exprt tmp=from_integer(v, expr.type());
155  expr.swap(tmp);
156  return false;
157  }
158  }
159  else if(array.id()==ID_array_of)
160  {
161  if(array.operands().size()==1)
162  {
163  exprt tmp=array.op0();
164  expr.swap(tmp);
165  return false;
166  }
167  }
168  else if(array.id() == ID_array_list)
169  {
170  // These are index/value pairs, alternating.
171  for(size_t i=0; i<array.operands().size()/2; i++)
172  {
173  exprt tmp_index=array.operands()[i*2];
174  tmp_index.make_typecast(index.type());
175  simplify(tmp_index);
176  if(tmp_index==index)
177  {
178  exprt tmp=array.operands()[i*2+1];
179  expr.swap(tmp);
180  return false;
181  }
182  }
183  }
184  else if(array.id()==ID_byte_extract_little_endian ||
185  array.id()==ID_byte_extract_big_endian)
186  {
187  if(array.type().id() == ID_array)
188  {
189  const auto &array_type = to_array_type(array.type());
190 
191  // This rewrites byte_extract(s, o, array_type)[i]
192  // to byte_extract(s, o+offset, sub_type)
193 
194  auto sub_size = pointer_offset_size(array_type.subtype(), ns);
195  if(!sub_size.has_value())
196  return true;
197 
198  // add offset to index
199  mult_exprt offset(from_integer(*sub_size, array.op1().type()), index);
200  plus_exprt final_offset(array.op1(), offset);
201  simplify_node(final_offset);
202 
203  exprt result_expr(array.id(), expr.type());
204  result_expr.add_to_operands(array.op0(), final_offset);
205  expr.swap(result_expr);
206 
207  simplify_rec(expr);
208 
209  return false;
210  }
211  }
212  else if(array.id()==ID_if)
213  {
214  const if_exprt &if_expr=to_if_expr(array);
215  exprt cond=if_expr.cond();
216 
217  index_exprt idx_false=to_index_expr(expr);
218  idx_false.array()=if_expr.false_case();
219 
220  to_index_expr(expr).array()=if_expr.true_case();
221 
222  expr=if_exprt(cond, expr, idx_false, expr.type());
223  simplify_rec(expr);
224 
225  return false;
226  }
227 
228  return result;
229 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
exprt & true_case()
Definition: std_expr.h:3455
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
bool simplify_index(exprt &expr)
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
typet & type()
Return the type of the expression.
Definition: expr.h:68
Equality.
Definition: std_expr.h:1484
bool simplify_if(if_exprt &expr)
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
exprt & false_case()
Definition: std_expr.h:3465
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
Pointer Logic.
bool simplify_rec(exprt &expr)
exprt & index()
Definition: std_expr.h:1631
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const namespacet & ns
void swap(irept &irep)
Definition: irep.h:303
virtual bool simplify(exprt &expr)
exprt & op2()
Definition: expr.h:90
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1621
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:130
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
Array index operator.
Definition: std_expr.h:1595