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>(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>(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.op0(), 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 = numeric_cast_v<std::size_t>(array_type.size());
154  exprt casted_op =
155  typecast_exprt::conditional_cast(op, array_type.subtype());
156  array_exprt array_expr(array_type);
157  array_expr.operands().resize(dimension, op);
158  expr = array_expr;
159  }
160  }
161  }
162 
163  remove_vector(expr.type());
164 }
165 
167 static void remove_vector(typet &type)
168 {
169  if(!have_to_remove_vector(type))
170  return;
171 
172  if(type.id()==ID_struct || type.id()==ID_union)
173  {
174  struct_union_typet &struct_union_type=
175  to_struct_union_type(type);
176 
177  for(struct_union_typet::componentst::iterator
178  it=struct_union_type.components().begin();
179  it!=struct_union_type.components().end();
180  it++)
181  {
182  remove_vector(it->type());
183  }
184  }
185  else if(type.id()==ID_pointer ||
186  type.id()==ID_complex ||
187  type.id()==ID_array)
188  {
189  remove_vector(type.subtype());
190  }
191  else if(type.id()==ID_vector)
192  {
193  vector_typet &vector_type=to_vector_type(type);
194 
195  remove_vector(type.subtype());
196 
197  // Replace by an array with appropriate number of members.
198  array_typet array_type(vector_type.subtype(), vector_type.size());
199  array_type.add_source_location()=type.source_location();
200  type=array_type;
201  }
202 }
203 
205 static void remove_vector(symbolt &symbol)
206 {
207  remove_vector(symbol.value);
208  remove_vector(symbol.type);
209 }
210 
212 static void remove_vector(symbol_tablet &symbol_table)
213 {
214  for(const auto &named_symbol : symbol_table.symbols)
215  remove_vector(*symbol_table.get_writeable(named_symbol.first));
216 }
217 
220 {
221  remove_vector(goto_function.type);
222 
223  Forall_goto_program_instructions(it, goto_function.body)
224  {
225  remove_vector(it->code);
226  remove_vector(it->guard);
227  }
228 }
229 
231 static void remove_vector(goto_functionst &goto_functions)
232 {
233  Forall_goto_functions(it, goto_functions)
234  remove_vector(it->second);
235 }
236 
239  symbol_tablet &symbol_table,
240  goto_functionst &goto_functions)
241 {
242  remove_vector(symbol_table);
243  remove_vector(goto_functions);
244 }
245 
247 void remove_vector(goto_modelt &goto_model)
248 {
249  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
250 }
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
const exprt & op() const
Definition: std_expr.h:371
exprt value
Initial value of symbol.
Definition: symbol.h:34
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:93
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
A base class for binary expressions.
Definition: std_expr.h:738
static bool have_to_remove_vector(const typet &type)
The vector type.
Definition: std_types.h:1755
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
Generic base class for unary expressions.
Definition: std_expr.h:331
::goto_functiont goto_functiont
const exprt & size() const
Definition: std_types.h:1765
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
#define forall_operands(it, expr)
Definition: expr.h:20
A collection of goto functions.
const symbolst & symbols
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
const source_locationt & source_location() const
Definition: type.h:62
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
Base type for structs and unions.
Definition: std_types.h:114
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
source_locationt & add_source_location()
Definition: type.h:67
#define Forall_goto_functions(it, functions)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
#define Forall_operands(it, expr)
Definition: expr.h:26
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Arrays with given size.
Definition: std_types.h:1000
Remove the &#39;vector&#39; data type by compilation into arrays.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:810
const typet & subtype() const
Definition: type.h:38
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:395
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static void remove_vector(typet &)
removes vector data type
Array constructor from list of elements.
Definition: std_expr.h:1739
Array index operator.
Definition: std_expr.h:1595