cprover
Loading...
Searching...
No Matches
simplify_expr_array.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include "arith_tools.h"
12#include "byte_operators.h"
13#include "pointer_offset_size.h"
14#include "replace_expr.h"
15#include "std_expr.h"
16#include "string_constant.h"
17
20{
21 bool no_change = true;
22
23 // copy
24 auto new_expr = expr;
25
26 // references
27 auto &index = new_expr.index();
28 auto &array = new_expr.array();
29
30 // extra arithmetic optimizations
31
32 if(index.id() == ID_div)
33 {
34 const auto &index_div_expr = to_div_expr(index);
35
36 if(
37 index_div_expr.dividend().id() == ID_mult &&
38 index_div_expr.dividend().operands().size() == 2 &&
39 to_mult_expr(index_div_expr.dividend()).op1() == index_div_expr.divisor())
40 {
41 // this rewrites (a*b)/b to a
42 index = to_mult_expr(index_div_expr.dividend()).op0();
43 no_change = false;
44 }
45 else if(
46 index_div_expr.dividend().id() == ID_mult &&
47 index_div_expr.dividend().operands().size() == 2 &&
48 to_mult_expr(index_div_expr.dividend()).op0() == index_div_expr.divisor())
49 {
50 // this rewrites (a*b)/a to b
51 index = to_mult_expr(index_div_expr.dividend()).op1();
52 no_change = false;
53 }
54 }
55
56 if(array.id() == ID_array_comprehension)
57 {
58 // simplify (lambda i: e)(x) to e[i/x]
59
60 const auto &comprehension = to_array_comprehension_expr(array);
61
62 if(index.type() == comprehension.arg().type())
63 {
64 exprt tmp = comprehension.body();
65 replace_expr(comprehension.arg(), index, tmp);
66 return changed(simplify_rec(tmp));
67 }
68 }
69 else if(array.id()==ID_with)
70 {
71 // we have (a WITH [i:=e])[j]
72
73 if(array.operands().size() != 3)
74 return unchanged(expr);
75
76 const auto &with_expr = to_with_expr(array);
77
78 if(with_expr.where() == index)
79 {
80 // simplify (e with [i:=v])[i] to v
81 return with_expr.new_value();
82 }
83 else
84 {
85 // Turn (a with i:=x)[j] into (i==j)?x:a[j].
86 // watch out that the type of i and j might be different.
87 const exprt rhs_casted =
88 typecast_exprt::conditional_cast(with_expr.where(), index.type());
89
91
93 index_exprt(with_expr.old(), index, new_expr.type())); // recursive call
94
95 if(equality_expr.is_true())
96 {
97 return with_expr.new_value();
98 }
99 else if(equality_expr.is_false())
100 {
101 return new_index_expr;
102 }
103
105 return changed(simplify_if(if_expr));
106 }
107 }
108 else if(
109 array.is_constant() || array.id() == ID_array || array.id() == ID_vector)
110 {
111 const auto i = numeric_cast<mp_integer>(index);
112
113 if(!i.has_value())
114 {
115 }
116 else if(*i < 0 || *i >= array.operands().size())
117 {
118 // out of bounds
119 }
120 else
121 {
122 // ok
123 return array.operands()[numeric_cast_v<std::size_t>(*i)];
124 }
125 }
126 else if(array.id()==ID_string_constant)
127 {
128 const auto i = numeric_cast<mp_integer>(index);
129
130 const std::string &value = id2string(to_string_constant(array).get_value());
131
132 if(!i.has_value())
133 {
134 }
135 else if(*i < 0 || *i > value.size())
136 {
137 // out of bounds
138 }
139 else
140 {
141 // terminating zero?
142 const char v =
143 (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
144 return from_integer(v, new_expr.type());
145 }
146 }
147 else if(array.id()==ID_array_of)
148 {
149 return to_array_of_expr(array).what();
150 }
151 else if(array.id() == ID_array_list)
152 {
153 // These are index/value pairs, alternating.
154 for(size_t i=0; i<array.operands().size()/2; i++)
155 {
156 exprt tmp_index = typecast_exprt(array.operands()[i * 2], index.type());
158 if(tmp_index==index)
159 {
160 return array.operands()[i * 2 + 1];
161 }
162 }
163 }
164 else if(array.id()==ID_byte_extract_little_endian ||
165 array.id()==ID_byte_extract_big_endian)
166 {
167 const auto &byte_extract_expr = to_byte_extract_expr(array);
168
169 if(array.type().id() == ID_array || array.type().id() == ID_vector)
170 {
171 optionalt<typet> subtype;
172 if(array.type().id() == ID_array)
173 subtype = to_array_type(array.type()).element_type();
174 else
175 subtype = to_vector_type(array.type()).element_type();
176
177 // This rewrites byte_extract(s, o, array_type)[i]
178 // to byte_extract(s, o+offset, sub_type)
179
180 auto sub_size = pointer_offset_size(*subtype, ns);
181 if(!sub_size.has_value())
182 return unchanged(expr);
183
184 // add offset to index
186 from_integer(*sub_size, byte_extract_expr.offset().type()),
188 index, byte_extract_expr.offset().type())});
190 simplify_plus(plus_exprt(byte_extract_expr.offset(), offset));
191
193 result_expr.type() = expr.type();
194 result_expr.offset() = final_offset;
195
197 }
198 }
199 else if(array.id()==ID_if)
200 {
201 const if_exprt &if_expr=to_if_expr(array);
202 exprt cond=if_expr.cond();
203
205 idx_false.array()=if_expr.false_case();
206
207 new_expr.array() = if_expr.true_case();
208
209 exprt result = if_exprt(cond, new_expr, idx_false, expr.type());
210 return changed(simplify_rec(result));
211 }
212
213 if(no_change)
214 return unchanged(expr);
215 else
216 return std::move(new_expr);
217}
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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
The plus expression Associativity is not specified.
Definition std_expr.h:947
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_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)
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
Pointer Logic.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
API to expression classes.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1543
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1077
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3425
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1146
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2486
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
const string_constantt & to_string_constant(const exprt &expr)