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 "byte_operators.h"
13 #include "namespace.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.id() == ID_constant || array.id() == ID_array ||
111  array.id() == ID_vector)
112  {
113  const auto i = numeric_cast<mp_integer>(index);
114 
115  if(!i.has_value())
116  {
117  }
118  else if(*i < 0 || *i >= array.operands().size())
119  {
120  // out of bounds
121  }
122  else
123  {
124  // ok
125  return array.operands()[numeric_cast_v<std::size_t>(*i)];
126  }
127  }
128  else if(array.id()==ID_string_constant)
129  {
130  const auto i = numeric_cast<mp_integer>(index);
131 
132  const std::string &value = id2string(to_string_constant(array).get_value());
133 
134  if(!i.has_value())
135  {
136  }
137  else if(*i < 0 || *i > value.size())
138  {
139  // out of bounds
140  }
141  else
142  {
143  // terminating zero?
144  const char v =
145  (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
146  return from_integer(v, new_expr.type());
147  }
148  }
149  else if(array.id()==ID_array_of)
150  {
151  return to_array_of_expr(array).what();
152  }
153  else if(array.id() == ID_array_list)
154  {
155  // These are index/value pairs, alternating.
156  for(size_t i=0; i<array.operands().size()/2; i++)
157  {
158  exprt tmp_index = typecast_exprt(array.operands()[i * 2], index.type());
159  simplify(tmp_index);
160  if(tmp_index==index)
161  {
162  return array.operands()[i * 2 + 1];
163  }
164  }
165  }
166  else if(array.id()==ID_byte_extract_little_endian ||
167  array.id()==ID_byte_extract_big_endian)
168  {
169  const auto &byte_extract_expr = to_byte_extract_expr(array);
170 
171  if(array.type().id() == ID_array || array.type().id() == ID_vector)
172  {
173  optionalt<typet> subtype;
174  if(array.type().id() == ID_array)
175  subtype = to_array_type(array.type()).subtype();
176  else
177  subtype = to_vector_type(array.type()).subtype();
178 
179  // This rewrites byte_extract(s, o, array_type)[i]
180  // to byte_extract(s, o+offset, sub_type)
181 
182  auto sub_size = pointer_offset_size(*subtype, ns);
183  if(!sub_size.has_value())
184  return unchanged(expr);
185 
186  // add offset to index
187  mult_exprt offset(
188  from_integer(*sub_size, byte_extract_expr.offset().type()), index);
189  exprt final_offset =
190  simplify_node(plus_exprt(byte_extract_expr.offset(), offset));
191 
192  exprt result_expr(array.id(), expr.type());
193  result_expr.add_to_operands(byte_extract_expr.op(), final_offset);
194 
195  return changed(simplify_rec(result_expr));
196  }
197  }
198  else if(array.id()==ID_if)
199  {
200  const if_exprt &if_expr=to_if_expr(array);
201  exprt cond=if_expr.cond();
202 
203  index_exprt idx_false=to_index_expr(expr);
204  idx_false.array()=if_expr.false_case();
205 
206  new_expr.array() = if_expr.true_case();
207 
208  exprt result = if_exprt(cond, new_expr, idx_false, expr.type());
209  return changed(simplify_rec(result));
210  }
211 
212  if(no_change)
213  return unchanged(expr);
214  else
215  return std::move(new_expr);
216 }
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2603
pointer_offset_size.h
Pointer Logic.
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:4485
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
simplify_expr_class.h
arith_tools.h
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1384
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2672
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1412
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1190
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2371
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:331
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
byte_operators.h
Expression classes for byte-level operators.
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1011
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1202
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
simplify_exprt::simplify_index
resultt simplify_index(const index_exprt &)
Definition: simplify_expr_array.cpp:20
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1775
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:246
replace_expr.h
index_exprt
Array index operator.
Definition: std_expr.h:1293
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
std_expr.h
API to expression classes.