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