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(expr.id()==ID_vector)
39  return true;
40  }
41 
42  if(have_to_remove_vector(expr.type()))
43  return true;
44 
45  forall_operands(it, expr)
46  if(have_to_remove_vector(*it))
47  return true;
48 
49  return false;
50 }
51 
52 static bool have_to_remove_vector(const typet &type)
53 {
54  if(type.id()==ID_struct || type.id()==ID_union)
55  {
56  for(const auto &c : to_struct_union_type(type).components())
57  if(have_to_remove_vector(c.type()))
58  return true;
59  }
60  else if(type.id()==ID_pointer ||
61  type.id()==ID_complex ||
62  type.id()==ID_array)
63  return have_to_remove_vector(type.subtype());
64  else if(type.id()==ID_vector)
65  return true;
66 
67  return false;
68 }
69 
71 static void remove_vector(typet &);
72 
73 static void remove_vector(exprt &expr)
74 {
75  if(!have_to_remove_vector(expr))
76  return;
77 
78  Forall_operands(it, expr)
79  remove_vector(*it);
80 
81  if(expr.type().id()==ID_vector)
82  {
83  if(
84  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
85  expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
86  expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
87  expr.id() == ID_lshr || expr.id() == ID_ashr)
88  {
89  // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
90  // operations rather than binary. This code assumes that they
91  // can only have exactly 2 operands, and it is not clear
92  // that it is safe to do so in this context
93  PRECONDITION(expr.operands().size() == 2);
94  auto const &binary_expr = to_binary_expr(expr);
95  remove_vector(expr.type());
96  array_typet array_type=to_array_type(expr.type());
97 
98  const mp_integer dimension =
99  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
100 
101  const typet subtype=array_type.subtype();
102  // do component-wise:
103  // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
104  array_exprt array_expr({}, array_type);
105  array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
106 
107  for(std::size_t i=0; i<array_expr.operands().size(); i++)
108  {
109  exprt index=from_integer(i, array_type.size().type());
110 
111  array_expr.operands()[i] = binary_exprt(
112  index_exprt(binary_expr.op0(), index, subtype),
113  binary_expr.id(),
114  index_exprt(binary_expr.op1(), index, subtype));
115  }
116 
117  expr=array_expr;
118  }
119  else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
120  {
121  auto const &unary_expr = to_unary_expr(expr);
122  remove_vector(expr.type());
123  array_typet array_type=to_array_type(expr.type());
124 
125  const mp_integer dimension =
126  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
127 
128  const typet subtype=array_type.subtype();
129  // do component-wise:
130  // -x -> vector(-x[0],-x[1],...)
131  array_exprt array_expr({}, array_type);
132  array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
133 
134  for(std::size_t i=0; i<array_expr.operands().size(); i++)
135  {
136  exprt index=from_integer(i, array_type.size().type());
137 
138  array_expr.operands()[i] = unary_exprt(
139  unary_expr.id(), index_exprt(unary_expr.op(), index, subtype));
140  }
141 
142  expr=array_expr;
143  }
144  else if(expr.id()==ID_vector)
145  {
146  expr.id(ID_array);
147  }
148  else if(expr.id() == ID_typecast)
149  {
150  const auto &op = to_typecast_expr(expr).op();
151 
152  if(op.type().id() != ID_array)
153  {
154  // (vector-type) x ==> { x, x, ..., x }
155  remove_vector(expr.type());
156  array_typet array_type = to_array_type(expr.type());
157  const auto dimension =
158  numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
159  exprt casted_op =
160  typecast_exprt::conditional_cast(op, array_type.subtype());
161  expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
162  }
163  }
164  }
165 
166  remove_vector(expr.type());
167 }
168 
170 static void remove_vector(typet &type)
171 {
172  if(!have_to_remove_vector(type))
173  return;
174 
175  if(type.id()==ID_struct || type.id()==ID_union)
176  {
177  struct_union_typet &struct_union_type=
178  to_struct_union_type(type);
179 
180  for(struct_union_typet::componentst::iterator
181  it=struct_union_type.components().begin();
182  it!=struct_union_type.components().end();
183  it++)
184  {
185  remove_vector(it->type());
186  }
187  }
188  else if(type.id()==ID_pointer ||
189  type.id()==ID_complex ||
190  type.id()==ID_array)
191  {
192  remove_vector(type.subtype());
193  }
194  else if(type.id()==ID_vector)
195  {
196  vector_typet &vector_type=to_vector_type(type);
197 
198  remove_vector(type.subtype());
199 
200  // Replace by an array with appropriate number of members.
201  array_typet array_type(vector_type.subtype(), vector_type.size());
202  array_type.add_source_location()=type.source_location();
203  type=array_type;
204  }
205 }
206 
208 static void remove_vector(symbolt &symbol)
209 {
210  remove_vector(symbol.value);
211  remove_vector(symbol.type);
212 }
213 
215 static void remove_vector(symbol_tablet &symbol_table)
216 {
217  for(const auto &named_symbol : symbol_table.symbols)
218  remove_vector(symbol_table.get_writeable_ref(named_symbol.first));
219 }
220 
223 {
224  for(auto &i : goto_function.body.instructions)
225  i.transform([](exprt e) -> optionalt<exprt> {
226  if(have_to_remove_vector(e))
227  {
228  remove_vector(e);
229  return e;
230  }
231  else
232  return {};
233  });
234 }
235 
237 static void remove_vector(goto_functionst &goto_functions)
238 {
239  for(auto &gf_entry : goto_functions.function_map)
240  remove_vector(gf_entry.second);
241 }
242 
245  symbol_tablet &symbol_table,
246  goto_functionst &goto_functions)
247 {
248  remove_vector(symbol_table);
249  remove_vector(goto_functions);
250 }
251 
253 void remove_vector(goto_modelt &goto_model)
254 {
255  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
256 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
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:329
typet::subtype
const typet & subtype() const
Definition: type.h:47
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:209
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:57
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
vector_typet
The vector type.
Definition: std_types.h:1764
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:628
remove_vector
static void remove_vector(typet &)
removes vector data type
Definition: remove_vector.cpp:170
array_typet::size
const exprt & size() const
Definition: std_types.h:976
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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
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.
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:294
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:282
remove_vector.h
Remove the 'vector' data type by compilation into arrays.
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:968
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:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1243
std_expr.h
API to expression classes.
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:1382
have_to_remove_vector
static bool have_to_remove_vector(const typet &type)
Definition: remove_vector.cpp:52
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701