cprover
remove_vector.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove 'vector' data type
4
5Author: Daniel Kroening
6
7Date: September 2014
8
9\*******************************************************************/
10
13
14#include "remove_vector.h"
15
16#include <util/arith_tools.h>
17#include <util/std_expr.h>
18
19#include "goto_model.h"
20
21static bool have_to_remove_vector(const typet &type);
22
23static bool have_to_remove_vector(const exprt &expr)
24{
25 if(expr.type().id()==ID_vector)
26 {
27 if(
28 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
29 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
30 expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
31 expr.id() == ID_lshr || expr.id() == ID_ashr)
32 {
33 return true;
34 }
35 else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
36 return true;
37 else if(
38 expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
39 expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
40 expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
41 {
42 return true;
43 }
44 else if(expr.id()==ID_vector)
45 return true;
46 }
47
48 if(have_to_remove_vector(expr.type()))
49 return true;
50
51 forall_operands(it, expr)
53 return true;
54
55 return false;
56}
57
58static bool have_to_remove_vector(const typet &type)
59{
60 if(type.id()==ID_struct || type.id()==ID_union)
61 {
62 for(const auto &c : to_struct_union_type(type).components())
63 if(have_to_remove_vector(c.type()))
64 return true;
65 }
66 else if(type.id() == ID_code)
67 {
68 const code_typet &code_type = to_code_type(type);
69
70 if(have_to_remove_vector(code_type.return_type()))
71 return true;
72 for(auto &parameter : code_type.parameters())
73 {
74 if(have_to_remove_vector(parameter.type()))
75 return true;
76 }
77 }
78 else if(type.id()==ID_pointer ||
79 type.id()==ID_complex ||
80 type.id()==ID_array)
81 return have_to_remove_vector(to_type_with_subtype(type).subtype());
82 else if(type.id()==ID_vector)
83 return true;
84
85 return false;
86}
87
89static void remove_vector(typet &);
90
91static void remove_vector(exprt &expr)
92{
93 if(!have_to_remove_vector(expr))
94 return;
95
96 Forall_operands(it, expr)
97 remove_vector(*it);
98
99 if(expr.type().id()==ID_vector)
100 {
101 if(
102 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
103 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
104 expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
105 expr.id() == ID_lshr || expr.id() == ID_ashr)
106 {
107 // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
108 // operations rather than binary. This code assumes that they
109 // can only have exactly 2 operands, and it is not clear
110 // that it is safe to do so in this context
111 PRECONDITION(expr.operands().size() == 2);
112 auto const &binary_expr = to_binary_expr(expr);
113 remove_vector(expr.type());
114 array_typet array_type=to_array_type(expr.type());
115
116 const mp_integer dimension =
117 numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
118
119 const typet subtype = array_type.element_type();
120 // do component-wise:
121 // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
122 array_exprt array_expr({}, array_type);
123 array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
124 array_expr.add_source_location() = expr.source_location();
125
126 for(std::size_t i=0; i<array_expr.operands().size(); i++)
127 {
128 exprt index=from_integer(i, array_type.size().type());
129
130 array_expr.operands()[i] = binary_exprt(
131 index_exprt(binary_expr.op0(), index, subtype),
132 binary_expr.id(),
133 index_exprt(binary_expr.op1(), index, subtype));
134 }
135
136 expr=array_expr;
137 }
138 else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
139 {
140 auto const &unary_expr = to_unary_expr(expr);
141 remove_vector(expr.type());
142 array_typet array_type=to_array_type(expr.type());
143
144 const mp_integer dimension =
145 numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
146
147 const typet subtype = array_type.element_type();
148 // do component-wise:
149 // -x -> vector(-x[0],-x[1],...)
150 array_exprt array_expr({}, array_type);
151 array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
152 array_expr.add_source_location() = expr.source_location();
153
154 for(std::size_t i=0; i<array_expr.operands().size(); i++)
155 {
156 exprt index=from_integer(i, array_type.size().type());
157
158 array_expr.operands()[i] = unary_exprt(
159 unary_expr.id(), index_exprt(unary_expr.op(), index, subtype));
160 }
161
162 expr=array_expr;
163 }
164 else if(
165 expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
166 expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
167 expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
168 {
169 // component-wise and generate 0 (false) or -1 (true)
170 // x ~ y -> vector(x[0] ~ y[0] ? -1 : 0, x[1] ~ y[1] ? -1 : 0, ...)
171
172 auto const &binary_expr = to_binary_expr(expr);
173 const vector_typet &vector_type = to_vector_type(expr.type());
174 const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
175
176 const typet &subtype = vector_type.element_type();
177 PRECONDITION(subtype.id() == ID_signedbv);
178 exprt minus_one = from_integer(-1, subtype);
179 exprt zero = from_integer(0, subtype);
180
181 exprt::operandst operands;
182 operands.reserve(dimension);
183
184 const bool is_float =
185 to_array_type(binary_expr.lhs().type()).element_type().id() ==
186 ID_floatbv;
187 irep_idt new_id;
188 if(binary_expr.id() == ID_vector_notequal)
189 {
190 if(is_float)
191 new_id = ID_ieee_float_notequal;
192 else
193 new_id = ID_notequal;
194 }
195 else if(binary_expr.id() == ID_vector_equal)
196 {
197 if(is_float)
198 new_id = ID_ieee_float_equal;
199 else
200 new_id = ID_equal;
201 }
202 else
203 {
204 // just strip the "vector-" prefix
205 new_id = id2string(binary_expr.id()).substr(7);
206 }
207
208 for(std::size_t i = 0; i < dimension; ++i)
209 {
210 exprt index = from_integer(i, vector_type.size().type());
211
212 operands.push_back(
213 if_exprt{binary_relation_exprt{index_exprt{binary_expr.lhs(), index},
214 new_id,
215 index_exprt{binary_expr.rhs(), index}},
216 minus_one,
217 zero});
218 }
219
220 source_locationt source_location = expr.source_location();
221 expr = array_exprt{std::move(operands),
222 array_typet{subtype, vector_type.size()}};
223 expr.add_source_location() = std::move(source_location);
224 }
225 else if(expr.id()==ID_vector)
226 {
227 expr.id(ID_array);
228 }
229 else if(expr.id() == ID_typecast)
230 {
231 const auto &op = to_typecast_expr(expr).op();
232
233 if(op.type().id() != ID_array)
234 {
235 // (vector-type) x ==> { x, x, ..., x }
236 remove_vector(expr.type());
237 array_typet array_type = to_array_type(expr.type());
238 const auto dimension =
239 numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
240 exprt casted_op =
242 source_locationt source_location = expr.source_location();
243 expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
244 expr.add_source_location() = std::move(source_location);
245 }
246 }
247 }
248
249 remove_vector(expr.type());
250}
251
253static void remove_vector(typet &type)
254{
255 if(!have_to_remove_vector(type))
256 return;
257
258 if(type.id()==ID_struct || type.id()==ID_union)
259 {
260 struct_union_typet &struct_union_type=
262
263 for(struct_union_typet::componentst::iterator
264 it=struct_union_type.components().begin();
265 it!=struct_union_type.components().end();
266 it++)
267 {
268 remove_vector(it->type());
269 }
270 }
271 else if(type.id() == ID_code)
272 {
273 code_typet &code_type = to_code_type(type);
274
275 remove_vector(code_type.return_type());
276 for(auto &parameter : code_type.parameters())
277 remove_vector(parameter.type());
278 }
279 else if(type.id()==ID_pointer ||
280 type.id()==ID_complex ||
281 type.id()==ID_array)
282 {
283 remove_vector(type.subtype());
284 }
285 else if(type.id()==ID_vector)
286 {
287 vector_typet &vector_type=to_vector_type(type);
288
289 remove_vector(vector_type.element_type());
290
291 // Replace by an array with appropriate number of members.
292 array_typet array_type(vector_type.element_type(), vector_type.size());
293 array_type.add_source_location()=type.source_location();
294 type=array_type;
295 }
296}
297
299static void remove_vector(symbolt &symbol)
300{
301 remove_vector(symbol.value);
302 remove_vector(symbol.type);
303}
304
306static void remove_vector(symbol_tablet &symbol_table)
307{
308 for(const auto &named_symbol : symbol_table.symbols)
309 remove_vector(symbol_table.get_writeable_ref(named_symbol.first));
310}
311
314{
315 for(auto &i : goto_function.body.instructions)
316 i.transform([](exprt e) -> optionalt<exprt> {
318 {
319 remove_vector(e);
320 return e;
321 }
322 else
323 return {};
324 });
325}
326
328static void remove_vector(goto_functionst &goto_functions)
329{
330 for(auto &gf_entry : goto_functions.function_map)
331 remove_vector(gf_entry.second);
332}
333
336 symbol_tablet &symbol_table,
337 goto_functionst &goto_functions)
338{
339 remove_vector(symbol_table);
340 remove_vector(goto_functions);
341}
342
344void remove_vector(goto_modelt &goto_model)
345{
346 remove_vector(goto_model.symbol_table, goto_model.goto_functions);
347}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A base class for binary expressions.
Definition: std_expr.h:550
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
The trinary if-then-else operator.
Definition: std_expr.h:2226
Array index operator.
Definition: std_expr.h:1328
const irep_idt & id() const
Definition: irep.h:396
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
static void remove_vector(typet &)
removes vector data type
static bool have_to_remove_vector(const typet &type)
Remove the 'vector' data type by compilation into arrays.
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177