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 #include <util/std_types.h>
19 
20 #include "goto_model.h"
21 
22 static bool have_to_remove_vector(const typet &type);
23 
24 static bool have_to_remove_vector(const exprt &expr)
25 {
26  if(expr.type().id()==ID_vector)
27  {
28  if(
29  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
30  expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
31  expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
32  expr.id() == ID_lshr || expr.id() == ID_ashr)
33  {
34  return true;
35  }
36  else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
37  return true;
38  else if(
39  expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
40  expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
41  expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
42  {
43  return true;
44  }
45  else if(expr.id()==ID_vector)
46  return true;
47  }
48 
49  if(have_to_remove_vector(expr.type()))
50  return true;
51 
52  forall_operands(it, expr)
53  if(have_to_remove_vector(*it))
54  return true;
55 
56  return false;
57 }
58 
59 static bool have_to_remove_vector(const typet &type)
60 {
61  if(type.id()==ID_struct || type.id()==ID_union)
62  {
63  for(const auto &c : to_struct_union_type(type).components())
64  if(have_to_remove_vector(c.type()))
65  return true;
66  }
67  else if(type.id() == ID_code)
68  {
69  const code_typet &code_type = to_code_type(type);
70 
71  if(have_to_remove_vector(code_type.return_type()))
72  return true;
73  for(auto &parameter : code_type.parameters())
74  {
75  if(have_to_remove_vector(parameter.type()))
76  return true;
77  }
78  }
79  else if(type.id()==ID_pointer ||
80  type.id()==ID_complex ||
81  type.id()==ID_array)
82  return have_to_remove_vector(type.subtype());
83  else if(type.id()==ID_vector)
84  return true;
85 
86  return false;
87 }
88 
90 static void remove_vector(typet &);
91 
92 static void remove_vector(exprt &expr)
93 {
94  if(!have_to_remove_vector(expr))
95  return;
96 
97  Forall_operands(it, expr)
98  remove_vector(*it);
99 
100  if(expr.type().id()==ID_vector)
101  {
102  if(
103  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
104  expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
105  expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
106  expr.id() == ID_lshr || expr.id() == ID_ashr)
107  {
108  // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
109  // operations rather than binary. This code assumes that they
110  // can only have exactly 2 operands, and it is not clear
111  // that it is safe to do so in this context
112  PRECONDITION(expr.operands().size() == 2);
113  auto const &binary_expr = to_binary_expr(expr);
114  remove_vector(expr.type());
115  array_typet array_type=to_array_type(expr.type());
116 
117  const mp_integer dimension =
118  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
119 
120  const typet subtype=array_type.subtype();
121  // do component-wise:
122  // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
123  array_exprt array_expr({}, array_type);
124  array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
125  array_expr.add_source_location() = expr.source_location();
126 
127  for(std::size_t i=0; i<array_expr.operands().size(); i++)
128  {
129  exprt index=from_integer(i, array_type.size().type());
130 
131  array_expr.operands()[i] = binary_exprt(
132  index_exprt(binary_expr.op0(), index, subtype),
133  binary_expr.id(),
134  index_exprt(binary_expr.op1(), index, subtype));
135  }
136 
137  expr=array_expr;
138  }
139  else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
140  {
141  auto const &unary_expr = to_unary_expr(expr);
142  remove_vector(expr.type());
143  array_typet array_type=to_array_type(expr.type());
144 
145  const mp_integer dimension =
146  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
147 
148  const typet subtype=array_type.subtype();
149  // do component-wise:
150  // -x -> vector(-x[0],-x[1],...)
151  array_exprt array_expr({}, array_type);
152  array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
153  array_expr.add_source_location() = expr.source_location();
154 
155  for(std::size_t i=0; i<array_expr.operands().size(); i++)
156  {
157  exprt index=from_integer(i, array_type.size().type());
158 
159  array_expr.operands()[i] = unary_exprt(
160  unary_expr.id(), index_exprt(unary_expr.op(), index, subtype));
161  }
162 
163  expr=array_expr;
164  }
165  else if(
166  expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
167  expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
168  expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
169  {
170  // component-wise and generate 0 (false) or -1 (true)
171  // x ~ y -> vector(x[0] ~ y[0] ? -1 : 0, x[1] ~ y[1] ? -1 : 0, ...)
172 
173  auto const &binary_expr = to_binary_expr(expr);
174  const vector_typet &vector_type = to_vector_type(expr.type());
175  const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
176 
177  const typet &subtype = vector_type.subtype();
178  PRECONDITION(subtype.id() == ID_signedbv);
179  exprt minus_one = from_integer(-1, subtype);
180  exprt zero = from_integer(0, subtype);
181 
182  exprt::operandst operands;
183  operands.reserve(dimension);
184 
185  const bool is_float =
186  binary_expr.lhs().type().subtype().id() == 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 =
241  typecast_exprt::conditional_cast(op, array_type.subtype());
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 
253 static 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=
261  to_struct_union_type(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(type.subtype());
290 
291  // Replace by an array with appropriate number of members.
292  array_typet array_type(vector_type.subtype(), vector_type.size());
293  array_type.add_source_location()=type.source_location();
294  type=array_type;
295  }
296 }
297 
299 static void remove_vector(symbolt &symbol)
300 {
301  remove_vector(symbol.value);
302  remove_vector(symbol.type);
303 }
304 
306 static 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> {
317  if(have_to_remove_vector(e))
318  {
319  remove_vector(e);
320  return e;
321  }
322  else
323  return {};
324  });
325 }
326 
328 static 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 
344 void remove_vector(goto_modelt &goto_model)
345 {
346  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
347 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
typet::subtype
const typet & subtype() const
Definition: type.h:47
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
arith_tools.h
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:208
typet
The type of an expression, extends irept.
Definition: type.h:28
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:56
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:580
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
vector_typet
The vector type.
Definition: std_types.h:969
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:253
array_typet::size
const exprt & size() const
Definition: std_types.h:765
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
std_types.h
Pre-defined types.
code_typet
Base type of functions.
Definition: std_types.h:533
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:243
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
array_typet
Arrays with given size.
Definition: std_types.h:757
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1242
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
have_to_remove_vector
static bool have_to_remove_vector(const typet &type)
Definition: remove_vector.cpp:59
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700