CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <ansi-c/c_expr.h>
20
21#include "goto_model.h"
22
23static bool have_to_remove_vector(const typet &type);
24
25static bool have_to_remove_vector(const exprt &expr)
26{
27 if(expr.type().id()==ID_vector)
28 {
29 if(
30 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
31 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
32 expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
33 expr.id() == ID_lshr || expr.id() == ID_ashr ||
34 expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
35 {
36 return true;
37 }
38 else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
39 return true;
40 else if(
41 expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
42 expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
43 expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
44 {
45 return true;
46 }
47 else if(expr.id() == ID_shuffle_vector)
48 return true;
49 else if(expr.id()==ID_vector)
50 return true;
51 }
52
53 if(have_to_remove_vector(expr.type()))
54 return true;
55
56 for(const auto &op : expr.operands())
57 {
59 return true;
60 }
61
62 return false;
63}
64
65static bool have_to_remove_vector(const typet &type)
66{
67 if(type.id()==ID_struct || type.id()==ID_union)
68 {
69 for(const auto &c : to_struct_union_type(type).components())
70 if(have_to_remove_vector(c.type()))
71 return true;
72 }
73 else if(type.id() == ID_code)
74 {
75 const code_typet &code_type = to_code_type(type);
76
77 if(have_to_remove_vector(code_type.return_type()))
78 return true;
79 for(auto &parameter : code_type.parameters())
80 {
82 return true;
83 }
84 }
85 else if(type.id()==ID_pointer ||
86 type.id()==ID_complex ||
87 type.id()==ID_array)
88 return have_to_remove_vector(to_type_with_subtype(type).subtype());
89 else if(type.id()==ID_vector)
90 return true;
91
92 return false;
93}
94
96static void remove_vector(typet &);
97
98static void remove_vector(exprt &expr)
99{
100 if(!have_to_remove_vector(expr))
101 return;
102
103 if(expr.id() == ID_shuffle_vector)
104 {
105 exprt result = to_shuffle_vector_expr(expr).lower();
106 remove_vector(result);
107 expr.swap(result);
108 return;
109 }
110
111 Forall_operands(it, expr)
112 remove_vector(*it);
113
114 if(expr.type().id()==ID_vector)
115 {
116 if(
117 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
118 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
119 expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
120 expr.id() == ID_lshr || expr.id() == ID_ashr ||
121 expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
122 {
123 // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
124 // operations rather than binary. This code assumes that they
125 // can only have exactly 2 operands, and it is not clear
126 // that it is safe to do so in this context
127 PRECONDITION(expr.operands().size() == 2);
128 auto const &binary_expr = to_binary_expr(expr);
129 remove_vector(expr.type());
131
132 const mp_integer dimension =
134
135 const typet subtype = array_type.element_type();
136 // do component-wise:
137 // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
140 array_expr.add_source_location() = expr.source_location();
141
142 for(std::size_t i=0; i<array_expr.operands().size(); i++)
143 {
144 exprt index=from_integer(i, array_type.size().type());
145
146 array_expr.operands()[i] = binary_exprt(
147 index_exprt(binary_expr.op0(), index, subtype),
148 binary_expr.id(),
149 index_exprt(binary_expr.op1(), index, subtype));
150 }
151
152 expr=array_expr;
153 }
154 else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
155 {
156 auto const &unary_expr = to_unary_expr(expr);
157 remove_vector(expr.type());
159
160 const mp_integer dimension =
162
163 const typet subtype = array_type.element_type();
164 // do component-wise:
165 // -x -> vector(-x[0],-x[1],...)
168 array_expr.add_source_location() = expr.source_location();
169
170 for(std::size_t i=0; i<array_expr.operands().size(); i++)
171 {
172 exprt index=from_integer(i, array_type.size().type());
173
174 array_expr.operands()[i] = unary_exprt(
175 unary_expr.id(), index_exprt(unary_expr.op(), index, subtype));
176 }
177
178 expr=array_expr;
179 }
180 else if(
181 expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
182 expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
183 expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
184 {
185 // component-wise and generate 0 (false) or -1 (true)
186 // x ~ y -> vector(x[0] ~ y[0] ? -1 : 0, x[1] ~ y[1] ? -1 : 0, ...)
187
188 auto const &binary_expr = to_binary_expr(expr);
191
192 const typet &subtype = vector_type.element_type();
193 exprt minus_one = from_integer(-1, subtype);
194 exprt zero = from_integer(0, subtype);
195
196 exprt::operandst operands;
197 operands.reserve(dimension);
198
199 const bool is_float =
200 to_array_type(binary_expr.lhs().type()).element_type().id() ==
204 {
205 if(is_float)
207 else
209 }
210 else if(binary_expr.id() == ID_vector_equal)
211 {
212 if(is_float)
214 else
216 }
217 else
218 {
219 // just strip the "vector-" prefix
220 new_id = id2string(binary_expr.id()).substr(7);
221 }
222
223 for(std::size_t i = 0; i < dimension; ++i)
224 {
225 exprt index = from_integer(i, vector_type.size().type());
226
227 operands.push_back(
229 new_id,
230 index_exprt{binary_expr.rhs(), index}},
231 minus_one,
232 zero});
233 }
234
235 source_locationt source_location = expr.source_location();
236 expr = array_exprt{std::move(operands),
237 array_typet{subtype, vector_type.size()}};
238 expr.add_source_location() = std::move(source_location);
239 }
240 else if(expr.id()==ID_vector)
241 {
242 expr.id(ID_array);
243 }
244 else if(expr.id() == ID_typecast)
245 {
246 const auto &op = to_typecast_expr(expr).op();
247
248 if(op.type().id() != ID_array)
249 {
250 // (vector-type) x ==> { x, x, ..., x }
251 remove_vector(expr.type());
253 const auto dimension =
257 source_locationt source_location = expr.source_location();
259 expr.add_source_location() = std::move(source_location);
260 }
261 else if(
262 expr.type().id() == ID_vector &&
263 to_vector_type(expr.type()).size() == to_array_type(op.type()).size())
264 {
265 // do component-wise typecast:
266 // (vector-type) x -> array((vector-sub-type)x[0], ...)
267 remove_vector(expr.type());
268 const array_typet &array_type = to_array_type(expr.type());
269 const std::size_t dimension =
271 const typet subtype = array_type.element_type();
272
273 exprt::operandst elements;
274 elements.reserve(dimension);
275
276 for(std::size_t i = 0; i < dimension; i++)
277 {
278 exprt index = from_integer(i, array_type.size().type());
279 elements.push_back(
280 typecast_exprt{index_exprt{op, std::move(index)}, subtype});
281 }
282
283 array_exprt array_expr(std::move(elements), array_type);
284 array_expr.add_source_location() = expr.source_location();
285 expr.swap(array_expr);
286 }
287 }
288 }
289
290 remove_vector(expr.type());
291}
292
294static void remove_vector(typet &type)
295{
296 if(!have_to_remove_vector(type))
297 return;
298
299 if(type.id()==ID_struct || type.id()==ID_union)
300 {
303
304 for(struct_union_typet::componentst::iterator
305 it=struct_union_type.components().begin();
306 it!=struct_union_type.components().end();
307 it++)
308 {
309 remove_vector(it->type());
310 }
311 }
312 else if(type.id() == ID_code)
313 {
315
316 remove_vector(code_type.return_type());
317 for(auto &parameter : code_type.parameters())
318 remove_vector(parameter.type());
319 }
320 else if(type.id()==ID_pointer ||
321 type.id()==ID_complex ||
322 type.id()==ID_array)
323 {
324 remove_vector(to_type_with_subtype(type).subtype());
325 }
326 else if(type.id()==ID_vector)
327 {
329
330 remove_vector(vector_type.element_type());
331
332 // Replace by an array with appropriate number of members.
333 array_typet array_type(vector_type.element_type(), vector_type.size());
334 array_type.add_source_location()=type.source_location();
335 type=array_type;
336 }
337}
338
340static void remove_vector(symbolt &symbol)
341{
342 remove_vector(symbol.value);
343 remove_vector(symbol.type);
344}
345
347static void remove_vector(symbol_table_baset &symbol_table)
348{
349 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
350 remove_vector(it.get_writeable_symbol());
351}
352
355{
356 for(auto &i : goto_function.body.instructions)
357 i.transform([](exprt e) -> std::optional<exprt> {
359 {
360 remove_vector(e);
361 return e;
362 }
363 else
364 return {};
365 });
366}
367
369static void remove_vector(goto_functionst &goto_functions)
370{
371 for(auto &gf_entry : goto_functions.function_map)
372 remove_vector(gf_entry.second);
373}
374
377 symbol_table_baset &symbol_table,
378 goto_functionst &goto_functions)
379{
380 remove_vector(symbol_table);
381 remove_vector(goto_functions);
382}
383
385void remove_vector(goto_modelt &goto_model)
386{
387 remove_vector(goto_model.symbol_table, goto_model.goto_functions);
388}
389
390bool has_vector(const goto_functionst &goto_functions)
391{
392 for(auto &function_it : goto_functions.function_map)
393 for(auto &instruction : function_it.second.body.instructions)
394 {
395 bool has_vector = false;
396 instruction.apply([&has_vector](const exprt &expr) {
397 if(have_to_remove_vector(expr))
398 has_vector = true;
399 });
400 if(has_vector)
401 return true;
402 }
403
404 return false;
405}
406
407bool has_vector(const goto_modelt &goto_model)
408{
409 return has_vector(goto_model.goto_functions);
410}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes that are internal to the C frontend.
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
Definition c_expr.h:93
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Base type of functions.
Definition std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
Base type for structs and unions.
Definition std_types.h:62
The symbol table base class interface.
virtual iteratort begin()=0
virtual iteratort end()=0
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
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
Generic base class for unary expressions.
Definition std_expr.h:361
The vector type.
Definition std_types.h:1064
#define Forall_operands(it, expr)
Definition expr.h:27
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static void remove_vector(typet &)
removes vector data type
static bool have_to_remove_vector(const typet &type)
bool has_vector(const goto_functionst &goto_functions)
returns true iff any of the given goto functions has instructions that use the vector type
Remove the 'vector' data type by compilation into arrays.
BigInt mp_integer
Definition smt_terms.h:17
#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:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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:208