cprover
remove_vector.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove 'vector' data type
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
21 static bool have_to_remove_vector(const typet &type);
22 
23 static 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)
52  if(have_to_remove_vector(*it))
53  return true;
54 
55  return false;
56 }
57 
58 static 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(type.subtype());
82  else if(type.id()==ID_vector)
83  return true;
84 
85  return false;
86 }
87 
89 static void remove_vector(typet &);
90 
91 static 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.subtype();
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.subtype();
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.subtype();
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  binary_expr.lhs().type().subtype().id() == ID_floatbv;
186  irep_idt new_id;
187  if(binary_expr.id() == ID_vector_notequal)
188  {
189  if(is_float)
190  new_id = ID_ieee_float_notequal;
191  else
192  new_id = ID_notequal;
193  }
194  else if(binary_expr.id() == ID_vector_equal)
195  {
196  if(is_float)
197  new_id = ID_ieee_float_equal;
198  else
199  new_id = ID_equal;
200  }
201  else
202  {
203  // just strip the "vector-" prefix
204  new_id = id2string(binary_expr.id()).substr(7);
205  }
206 
207  for(std::size_t i = 0; i < dimension; ++i)
208  {
209  exprt index = from_integer(i, vector_type.size().type());
210 
211  operands.push_back(
212  if_exprt{binary_relation_exprt{index_exprt{binary_expr.lhs(), index},
213  new_id,
214  index_exprt{binary_expr.rhs(), index}},
215  minus_one,
216  zero});
217  }
218 
219  source_locationt source_location = expr.source_location();
220  expr = array_exprt{std::move(operands),
221  array_typet{subtype, vector_type.size()}};
222  expr.add_source_location() = std::move(source_location);
223  }
224  else if(expr.id()==ID_vector)
225  {
226  expr.id(ID_array);
227  }
228  else if(expr.id() == ID_typecast)
229  {
230  const auto &op = to_typecast_expr(expr).op();
231 
232  if(op.type().id() != ID_array)
233  {
234  // (vector-type) x ==> { x, x, ..., x }
235  remove_vector(expr.type());
236  array_typet array_type = to_array_type(expr.type());
237  const auto dimension =
238  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
239  exprt casted_op =
240  typecast_exprt::conditional_cast(op, array_type.subtype());
241  source_locationt source_location = expr.source_location();
242  expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
243  expr.add_source_location() = std::move(source_location);
244  }
245  }
246  }
247 
248  remove_vector(expr.type());
249 }
250 
252 static void remove_vector(typet &type)
253 {
254  if(!have_to_remove_vector(type))
255  return;
256 
257  if(type.id()==ID_struct || type.id()==ID_union)
258  {
259  struct_union_typet &struct_union_type=
260  to_struct_union_type(type);
261 
262  for(struct_union_typet::componentst::iterator
263  it=struct_union_type.components().begin();
264  it!=struct_union_type.components().end();
265  it++)
266  {
267  remove_vector(it->type());
268  }
269  }
270  else if(type.id() == ID_code)
271  {
272  code_typet &code_type = to_code_type(type);
273 
274  remove_vector(code_type.return_type());
275  for(auto &parameter : code_type.parameters())
276  remove_vector(parameter.type());
277  }
278  else if(type.id()==ID_pointer ||
279  type.id()==ID_complex ||
280  type.id()==ID_array)
281  {
282  remove_vector(type.subtype());
283  }
284  else if(type.id()==ID_vector)
285  {
286  vector_typet &vector_type=to_vector_type(type);
287 
288  remove_vector(type.subtype());
289 
290  // Replace by an array with appropriate number of members.
291  array_typet array_type(vector_type.subtype(), vector_type.size());
292  array_type.add_source_location()=type.source_location();
293  type=array_type;
294  }
295 }
296 
298 static void remove_vector(symbolt &symbol)
299 {
300  remove_vector(symbol.value);
301  remove_vector(symbol.type);
302 }
303 
305 static void remove_vector(symbol_tablet &symbol_table)
306 {
307  for(const auto &named_symbol : symbol_table.symbols)
308  remove_vector(symbol_table.get_writeable_ref(named_symbol.first));
309 }
310 
313 {
314  for(auto &i : goto_function.body.instructions)
315  i.transform([](exprt e) -> optionalt<exprt> {
316  if(have_to_remove_vector(e))
317  {
318  remove_vector(e);
319  return e;
320  }
321  else
322  return {};
323  });
324 }
325 
327 static void remove_vector(goto_functionst &goto_functions)
328 {
329  for(auto &gf_entry : goto_functions.function_map)
330  remove_vector(gf_entry.second);
331 }
332 
335  symbol_tablet &symbol_table,
336  goto_functionst &goto_functions)
337 {
338  remove_vector(symbol_table);
339  remove_vector(goto_functions);
340 }
341 
343 void remove_vector(goto_modelt &goto_model)
344 {
345  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
346 }
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:1467
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
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 typet & return_type() const
Definition: std_types.h:645
const parameterst & parameters() const
Definition: std_types.h:655
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
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
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:2172
Array index operator.
Definition: std_expr.h:1328
const irep_idt & id() const
Definition: irep.h:407
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:1874
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
const typet & subtype() const
Definition: type.h:47
source_locationt & add_source_location()
Definition: type.h:76
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:975
const constant_exprt & size() const
Definition: std_types.cpp:239
#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:49
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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
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:813
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214