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 
18 static bool have_to_remove_vector(const typet &type);
19 
20 static bool have_to_remove_vector(const exprt &expr)
21 {
22  if(expr.type().id()==ID_vector)
23  {
24  if(expr.id()==ID_plus || expr.id()==ID_minus ||
25  expr.id()==ID_mult || expr.id()==ID_div ||
26  expr.id()==ID_mod || expr.id()==ID_bitxor ||
27  expr.id()==ID_bitand || expr.id()==ID_bitor)
28  return true;
29  else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
30  return true;
31  else if(expr.id()==ID_vector)
32  return true;
33  }
34 
35  if(have_to_remove_vector(expr.type()))
36  return true;
37 
38  forall_operands(it, expr)
39  if(have_to_remove_vector(*it))
40  return true;
41 
42  return false;
43 }
44 
45 static bool have_to_remove_vector(const typet &type)
46 {
47  if(type.id()==ID_struct || type.id()==ID_union)
48  {
49  const struct_union_typet &struct_union_type=
51 
52  for(struct_union_typet::componentst::const_iterator
53  it=struct_union_type.components().begin();
54  it!=struct_union_type.components().end();
55  it++)
56  if(have_to_remove_vector(it->type()))
57  return true;
58  }
59  else if(type.id()==ID_pointer ||
60  type.id()==ID_complex ||
61  type.id()==ID_array)
62  return have_to_remove_vector(type.subtype());
63  else if(type.id()==ID_vector)
64  return true;
65 
66  return false;
67 }
68 
70 static void remove_vector(typet &);
71 
72 static void remove_vector(exprt &expr)
73 {
74  if(!have_to_remove_vector(expr))
75  return;
76 
77  Forall_operands(it, expr)
78  remove_vector(*it);
79 
80  if(expr.type().id()==ID_vector)
81  {
82  if(expr.id()==ID_plus || expr.id()==ID_minus ||
83  expr.id()==ID_mult || expr.id()==ID_div ||
84  expr.id()==ID_mod || expr.id()==ID_bitxor ||
85  expr.id()==ID_bitand || expr.id()==ID_bitor)
86  {
87  remove_vector(expr.type());
88  array_typet array_type=to_array_type(expr.type());
89 
90  mp_integer dimension;
91  to_integer(array_type.size(), dimension);
92 
93  assert(expr.operands().size()==2);
94  const typet subtype=array_type.subtype();
95  // do component-wise:
96  // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
97  array_exprt array_expr(array_type);
98  array_expr.operands().resize(integer2size_t(dimension));
99 
100  for(unsigned i=0; i<array_expr.operands().size(); i++)
101  {
102  exprt index=from_integer(i, array_type.size().type());
103 
104  array_expr.operands()[i]=
105  binary_exprt(index_exprt(expr.op0(), index, subtype), expr.id(),
106  index_exprt(expr.op1(), index, subtype));
107  }
108 
109  expr=array_expr;
110  }
111  else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
112  {
113  remove_vector(expr.type());
114  array_typet array_type=to_array_type(expr.type());
115 
116  mp_integer dimension;
117  to_integer(array_type.size(), dimension);
118 
119  assert(expr.operands().size()==1);
120  const typet subtype=array_type.subtype();
121  // do component-wise:
122  // -x -> vector(-x[0],-x[1],...)
123  array_exprt array_expr(array_type);
124  array_expr.operands().resize(integer2size_t(dimension));
125 
126  for(unsigned 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]=
131  unary_exprt(expr.id(), index_exprt(expr.op0(), index, subtype));
132  }
133 
134  expr=array_expr;
135  }
136  else if(expr.id()==ID_vector)
137  {
138  expr.id(ID_array);
139  }
140  }
141 
142  remove_vector(expr.type());
143 }
144 
146 static void remove_vector(typet &type)
147 {
148  if(!have_to_remove_vector(type))
149  return;
150 
151  if(type.id()==ID_struct || type.id()==ID_union)
152  {
153  struct_union_typet &struct_union_type=
154  to_struct_union_type(type);
155 
156  for(struct_union_typet::componentst::iterator
157  it=struct_union_type.components().begin();
158  it!=struct_union_type.components().end();
159  it++)
160  {
161  remove_vector(it->type());
162  }
163  }
164  else if(type.id()==ID_pointer ||
165  type.id()==ID_complex ||
166  type.id()==ID_array)
167  {
168  remove_vector(type.subtype());
169  }
170  else if(type.id()==ID_vector)
171  {
172  vector_typet &vector_type=to_vector_type(type);
173 
174  remove_vector(type.subtype());
175 
176  // Replace by an array with appropriate number of members.
177  array_typet array_type(vector_type.subtype(), vector_type.size());
178  array_type.add_source_location()=type.source_location();
179  type=array_type;
180  }
181 }
182 
184 static void remove_vector(symbolt &symbol)
185 {
186  remove_vector(symbol.value);
187  remove_vector(symbol.type);
188 }
189 
191 static void remove_vector(symbol_tablet &symbol_table)
192 {
193  Forall_symbols(it, symbol_table.symbols)
194  remove_vector(it->second);
195 }
196 
199 {
200  remove_vector(goto_function.type);
201 
202  Forall_goto_program_instructions(it, goto_function.body)
203  {
204  remove_vector(it->code);
205  remove_vector(it->guard);
206  }
207 }
208 
210 static void remove_vector(goto_functionst &goto_functions)
211 {
212  Forall_goto_functions(it, goto_functions)
213  remove_vector(it->second);
214 }
215 
218  symbol_tablet &symbol_table,
219  goto_functionst &goto_functions)
220 {
221  remove_vector(symbol_table);
222  remove_vector(goto_functions);
223 }
224 
226 void remove_vector(goto_modelt &goto_model)
227 {
228  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
229 }
The type of an expression.
Definition: type.h:20
BigInt mp_integer
Definition: mp_arith.h:19
exprt & op0()
Definition: expr.h:84
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
symbolst symbols
Definition: symbol_table.h:57
A generic base class for binary expressions.
Definition: std_expr.h:471
static bool have_to_remove_vector(const typet &type)
A constant-size array type.
Definition: std_types.h:1554
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
Generic base class for unary expressions.
Definition: std_expr.h:221
const exprt & size() const
Definition: std_types.h:1568
#define forall_operands(it, expr)
Definition: expr.h:17
goto_function_templatet< goto_programt > goto_functiont
const source_locationt & source_location() const
Definition: type.h:95
typet type
Type of symbol.
Definition: symbol.h:37
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
Base class for all expressions.
Definition: expr.h:46
source_locationt & add_source_location()
Definition: type.h:100
#define Forall_goto_functions(it, functions)
#define Forall_operands(it, expr)
Definition: expr.h:23
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
arrays with given size
Definition: std_types.h:901
Remove the &#39;vector&#39; data type by compilation into arrays.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
goto_functionst goto_functions
Definition: goto_model.h:26
static void remove_vector(typet &)
removes vector data type
array constructor from list of elements
Definition: std_expr.h:1309
array index operator
Definition: std_expr.h:1170