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  const struct_union_typet &struct_union_type=
55 
56  for(struct_union_typet::componentst::const_iterator
57  it=struct_union_type.components().begin();
58  it!=struct_union_type.components().end();
59  it++)
60  if(have_to_remove_vector(it->type()))
61  return true;
62  }
63  else if(type.id()==ID_pointer ||
64  type.id()==ID_complex ||
65  type.id()==ID_array)
66  return have_to_remove_vector(type.subtype());
67  else if(type.id()==ID_vector)
68  return true;
69 
70  return false;
71 }
72 
74 static void remove_vector(typet &);
75 
76 static void remove_vector(exprt &expr)
77 {
78  if(!have_to_remove_vector(expr))
79  return;
80 
81  Forall_operands(it, expr)
82  remove_vector(*it);
83 
84  if(expr.type().id()==ID_vector)
85  {
86  if(expr.id()==ID_plus || expr.id()==ID_minus ||
87  expr.id()==ID_mult || expr.id()==ID_div ||
88  expr.id()==ID_mod || expr.id()==ID_bitxor ||
89  expr.id()==ID_bitand || expr.id()==ID_bitor)
90  {
91  remove_vector(expr.type());
92  array_typet array_type=to_array_type(expr.type());
93 
94  mp_integer dimension;
95  to_integer(array_type.size(), dimension);
96 
97  assert(expr.operands().size()==2);
98  const typet subtype=array_type.subtype();
99  // do component-wise:
100  // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
101  array_exprt array_expr(array_type);
102  array_expr.operands().resize(integer2size_t(dimension));
103 
104  for(std::size_t i=0; i<array_expr.operands().size(); i++)
105  {
106  exprt index=from_integer(i, array_type.size().type());
107 
108  array_expr.operands()[i]=
109  binary_exprt(index_exprt(expr.op0(), index, subtype), expr.id(),
110  index_exprt(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  remove_vector(expr.type());
118  array_typet array_type=to_array_type(expr.type());
119 
120  mp_integer dimension;
121  to_integer(array_type.size(), dimension);
122 
123  assert(expr.operands().size()==1);
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(integer2size_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]=
135  unary_exprt(expr.id(), index_exprt(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  }
145 
146  remove_vector(expr.type());
147 }
148 
150 static void remove_vector(typet &type)
151 {
152  if(!have_to_remove_vector(type))
153  return;
154 
155  if(type.id()==ID_struct || type.id()==ID_union)
156  {
157  struct_union_typet &struct_union_type=
158  to_struct_union_type(type);
159 
160  for(struct_union_typet::componentst::iterator
161  it=struct_union_type.components().begin();
162  it!=struct_union_type.components().end();
163  it++)
164  {
165  remove_vector(it->type());
166  }
167  }
168  else if(type.id()==ID_pointer ||
169  type.id()==ID_complex ||
170  type.id()==ID_array)
171  {
172  remove_vector(type.subtype());
173  }
174  else if(type.id()==ID_vector)
175  {
176  vector_typet &vector_type=to_vector_type(type);
177 
178  remove_vector(type.subtype());
179 
180  // Replace by an array with appropriate number of members.
181  array_typet array_type(vector_type.subtype(), vector_type.size());
182  array_type.add_source_location()=type.source_location();
183  type=array_type;
184  }
185 }
186 
188 static void remove_vector(symbolt &symbol)
189 {
190  remove_vector(symbol.value);
191  remove_vector(symbol.type);
192 }
193 
195 static void remove_vector(symbol_tablet &symbol_table)
196 {
197  for(const auto &named_symbol : symbol_table.symbols)
198  remove_vector(*symbol_table.get_writeable(named_symbol.first));
199 }
200 
203 {
204  remove_vector(goto_function.type);
205 
206  Forall_goto_program_instructions(it, goto_function.body)
207  {
208  remove_vector(it->code);
209  remove_vector(it->guard);
210  }
211 }
212 
214 static void remove_vector(goto_functionst &goto_functions)
215 {
216  Forall_goto_functions(it, goto_functions)
217  remove_vector(it->second);
218 }
219 
222  symbol_tablet &symbol_table,
223  goto_functionst &goto_functions)
224 {
225  remove_vector(symbol_table);
226  remove_vector(goto_functions);
227 }
228 
230 void remove_vector(goto_modelt &goto_model)
231 {
232  remove_vector(goto_model.symbol_table, goto_model.goto_functions);
233 }
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:72
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:87
const irep_idt & id() const
Definition: irep.h:189
Symbol Table + CFG.
A generic base class for binary expressions.
Definition: std_expr.h:649
static bool have_to_remove_vector(const typet &type)
A constant-size array type.
Definition: std_types.h:1629
API to expression classes.
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
Generic base class for unary expressions.
Definition: std_expr.h:303
::goto_functiont goto_functiont
const exprt & size() const
Definition: std_types.h:1639
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
#define forall_operands(it, expr)
Definition: expr.h:17
const symbolst & symbols
const source_locationt & source_location() const
Definition: type.h:97
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
source_locationt & add_source_location()
Definition: type.h:102
#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:740
arrays with given size
Definition: std_types.h:1004
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:17
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
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:1617
array index operator
Definition: std_expr.h:1462