CBMC
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 "byte_operators.h"
13 #include "expr_util.h"
14 #include "pointer_offset_size.h"
15 #include "replace_expr.h"
16 #include "std_expr.h"
17 #include "string_constant.h"
18 
21 {
22  bool no_change = true;
23 
24  // copy
25  auto new_expr = expr;
26 
27  // references
28  auto &index = new_expr.index();
29  auto &array = new_expr.array();
30 
31  // extra arithmetic optimizations
32 
33  if(index.id() == ID_div)
34  {
35  const auto &index_div_expr = to_div_expr(index);
36 
37  if(
38  index_div_expr.dividend().id() == ID_mult &&
39  index_div_expr.dividend().operands().size() == 2 &&
40  to_mult_expr(index_div_expr.dividend()).op1() == index_div_expr.divisor())
41  {
42  // this rewrites (a*b)/b to a
43  index = to_mult_expr(index_div_expr.dividend()).op0();
44  no_change = false;
45  }
46  else if(
47  index_div_expr.dividend().id() == ID_mult &&
48  index_div_expr.dividend().operands().size() == 2 &&
49  to_mult_expr(index_div_expr.dividend()).op0() == index_div_expr.divisor())
50  {
51  // this rewrites (a*b)/a to b
52  index = to_mult_expr(index_div_expr.dividend()).op1();
53  no_change = false;
54  }
55  }
56 
57  if(array.id() == ID_array_comprehension)
58  {
59  // simplify (lambda i: e)(x) to e[i/x]
60 
61  const auto &comprehension = to_array_comprehension_expr(array);
62 
63  if(index.type() == comprehension.arg().type())
64  {
65  exprt tmp = comprehension.body();
66  replace_expr(comprehension.arg(), index, tmp);
67  return changed(simplify_rec(tmp));
68  }
69  }
70  else if(array.id()==ID_with)
71  {
72  // we have (a WITH [i:=e])[j]
73 
74  if(array.operands().size() != 3)
75  return unchanged(expr);
76 
77  const auto &with_expr = to_with_expr(array);
78 
79  if(with_expr.where() == index)
80  {
81  // simplify (e with [i:=v])[i] to v
82  return with_expr.new_value();
83  }
84  else
85  {
86  // Turn (a with i:=x)[j] into (i==j)?x:a[j].
87  // watch out that the type of i and j might be different.
88  const exprt rhs_casted =
89  typecast_exprt::conditional_cast(with_expr.where(), index.type());
90 
91  exprt equality_expr = simplify_inequality(equal_exprt(index, rhs_casted));
92 
93  exprt new_index_expr = simplify_index(
94  index_exprt(with_expr.old(), index, new_expr.type())); // recursive call
95 
96  if(equality_expr.is_true())
97  {
98  return with_expr.new_value();
99  }
100  else if(equality_expr.is_false())
101  {
102  return new_index_expr;
103  }
104 
105  if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
106  return changed(simplify_if(if_expr));
107  }
108  }
109  else if(
110  array.is_constant() || array.id() == ID_array || array.id() == ID_vector)
111  {
112  const auto i = numeric_cast<mp_integer>(index);
113 
114  if(!i.has_value())
115  {
116  }
117  else if(*i < 0 || *i >= array.operands().size())
118  {
119  // out of bounds
120  }
121  else
122  {
123  // ok
124  return array.operands()[numeric_cast_v<std::size_t>(*i)];
125  }
126  }
127  else if(array.id()==ID_string_constant)
128  {
129  const auto i = numeric_cast<mp_integer>(index);
130 
131  const std::string &value = id2string(to_string_constant(array).value());
132 
133  if(!i.has_value())
134  {
135  }
136  else if(*i < 0 || *i > value.size())
137  {
138  // out of bounds
139  }
140  else
141  {
142  // terminating zero?
143  const char v =
144  (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
145  return from_integer(v, new_expr.type());
146  }
147  }
148  else if(array.id()==ID_array_of)
149  {
150  return to_array_of_expr(array).what();
151  }
152  else if(array.id() == ID_array_list)
153  {
154  // These are index/value pairs, alternating.
155  for(size_t i=0; i<array.operands().size()/2; i++)
156  {
157  exprt tmp_index = typecast_exprt(array.operands()[i * 2], index.type());
158  simplify(tmp_index);
159  if(tmp_index==index)
160  {
161  return array.operands()[i * 2 + 1];
162  }
163  }
164  }
165  else if(array.id()==ID_byte_extract_little_endian ||
166  array.id()==ID_byte_extract_big_endian)
167  {
168  const auto &byte_extract_expr = to_byte_extract_expr(array);
169 
170  if(array.type().id() == ID_array || array.type().id() == ID_vector)
171  {
172  std::optional<typet> subtype;
173  if(array.type().id() == ID_array)
174  subtype = to_array_type(array.type()).element_type();
175  else
176  subtype = to_vector_type(array.type()).element_type();
177 
178  // This rewrites byte_extract(s, o, array_type)[i]
179  // to byte_extract(s, o+offset, sub_type)
180 
181  auto sub_size = pointer_offset_size(*subtype, ns);
182  if(!sub_size.has_value())
183  return unchanged(expr);
184 
185  // add offset to index
186  exprt offset = simplify_rec(mult_exprt{
187  from_integer(*sub_size, byte_extract_expr.offset().type()),
189  index, byte_extract_expr.offset().type())});
190  exprt final_offset =
191  simplify_plus(plus_exprt(byte_extract_expr.offset(), offset));
192 
193  auto result_expr = byte_extract_expr;
194  result_expr.type() = expr.type();
195  result_expr.offset() = final_offset;
196 
197  return changed(simplify_byte_extract(result_expr));
198  }
199  }
200 
201  if(no_change)
202  return unchanged(expr);
203  else
204  return std::move(new_expr);
205 }
206 
209 {
210  // lift up any ID_if on the array
211  if(expr.array().id() == ID_if)
212  {
213  if_exprt if_expr = lift_if(expr, 0);
214  return changed(simplify_if_preorder(if_expr));
215  }
216  else
217  {
218  std::optional<exprt::operandst> new_operands;
219 
220  for(std::size_t i = 0; i < expr.operands().size(); ++i)
221  {
222  auto r_it = simplify_rec(expr.operands()[i]); // recursive call
223  if(r_it.has_changed())
224  {
225  if(!new_operands.has_value())
226  new_operands = expr.operands();
227  (*new_operands)[i] = std::move(r_it.expr);
228  }
229  }
230 
231  if(new_operands.has_value())
232  {
233  exprt result = expr;
234  std::swap(result.operands(), *new_operands);
235  return result;
236  }
237  }
238 
239  return unchanged(expr);
240 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt & what()
Definition: std_expr.h:1570
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
The trinary if-then-else operator.
Definition: std_expr.h:2370
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const irep_idt & id() const
Definition: irep.h:384
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
exprt & op1()
Definition: std_expr.h:938
exprt & op0()
Definition: std_expr.h:932
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
const namespacet & ns
resultt simplify_byte_extract(const byte_extract_exprt &)
static resultt changed(resultt<> result)
resultt simplify_if(const if_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_index_preorder(const index_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_index(const index_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_if_preorder(const if_exprt &expr)
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1068
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
API to expression classes.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3472
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1201
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2533
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1598
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1132
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1104
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const string_constantt & to_string_constant(const exprt &expr)