cprover
remove_complex.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove 'complex' data type
4 
5 Author: Daniel Kroening
6 
7 Date: September 2014
8 
9 \*******************************************************************/
10 
13 
14 #include "remove_complex.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 exprt complex_member(const exprt &expr, irep_idt id)
23 {
24  if(expr.id()==ID_struct && expr.operands().size()==2)
25  {
26  if(id==ID_real)
27  return to_binary_expr(expr).op0();
28  else if(id==ID_imag)
29  return to_binary_expr(expr).op1();
30  else
32  }
33  else
34  {
35  const struct_typet &struct_type=
36  to_struct_type(expr.type());
37  PRECONDITION(struct_type.components().size() == 2);
38  return member_exprt(expr, id, struct_type.components().front().type());
39  }
40 }
41 
42 static bool have_to_remove_complex(const typet &type);
43 
44 static bool have_to_remove_complex(const exprt &expr)
45 {
46  if(expr.id()==ID_typecast &&
47  to_typecast_expr(expr).op().type().id()==ID_complex &&
48  expr.type().id()!=ID_complex)
49  return true;
50 
51  if(expr.type().id()==ID_complex)
52  {
53  if(expr.id()==ID_plus || expr.id()==ID_minus ||
54  expr.id()==ID_mult || expr.id()==ID_div)
55  return true;
56  else if(expr.id()==ID_unary_minus)
57  return true;
58  else if(expr.id()==ID_complex)
59  return true;
60  else if(expr.id()==ID_typecast)
61  return true;
62  }
63 
64  if(expr.id()==ID_complex_real)
65  return true;
66  else if(expr.id()==ID_complex_imag)
67  return true;
68 
69  if(have_to_remove_complex(expr.type()))
70  return true;
71 
72  forall_operands(it, expr)
73  if(have_to_remove_complex(*it))
74  return true;
75 
76  return false;
77 }
78 
79 static bool have_to_remove_complex(const typet &type)
80 {
81  if(type.id()==ID_struct || type.id()==ID_union)
82  {
83  for(const auto &c : to_struct_union_type(type).components())
84  if(have_to_remove_complex(c.type()))
85  return true;
86  }
87  else if(type.id()==ID_pointer ||
88  type.id()==ID_vector ||
89  type.id()==ID_array)
90  return have_to_remove_complex(type.subtype());
91  else if(type.id()==ID_complex)
92  return true;
93 
94  return false;
95 }
96 
98 static void remove_complex(typet &);
99 
100 static void remove_complex(exprt &expr)
101 {
102  if(!have_to_remove_complex(expr))
103  return;
104 
105  if(expr.id()==ID_typecast)
106  {
107  auto const &typecast_expr = to_typecast_expr(expr);
108  if(typecast_expr.op().type().id() == ID_complex)
109  {
110  if(typecast_expr.type().id() == ID_complex)
111  {
112  // complex to complex
113  }
114  else
115  {
116  // cast complex to non-complex is (T)__real__ x
117  complex_real_exprt complex_real_expr(typecast_expr.op());
118 
119  expr = typecast_exprt(complex_real_expr, typecast_expr.type());
120  }
121  }
122  }
123 
124  Forall_operands(it, expr)
125  remove_complex(*it);
126 
127  if(expr.type().id()==ID_complex)
128  {
129  if(expr.id()==ID_plus || expr.id()==ID_minus ||
130  expr.id()==ID_mult || expr.id()==ID_div)
131  {
132  // FIXME plus and mult are defined as n-ary operations
133  // rather than binary. This code assumes that they
134  // can only have exactly 2 operands, and it is not clear
135  // that it is safe to do so in this context
136  PRECONDITION(expr.operands().size() == 2);
137  // do component-wise:
138  // x+y -> complex(x.r+y.r,x.i+y.i)
139  struct_exprt struct_expr(
140  {binary_exprt(
141  complex_member(to_binary_expr(expr).op0(), ID_real),
142  expr.id(),
143  complex_member(to_binary_expr(expr).op1(), ID_real)),
144  binary_exprt(
145  complex_member(to_binary_expr(expr).op0(), ID_imag),
146  expr.id(),
147  complex_member(to_binary_expr(expr).op1(), ID_imag))},
148  expr.type());
149 
150  struct_expr.op0().add_source_location() = expr.source_location();
151  struct_expr.op1().add_source_location()=expr.source_location();
152 
153  expr=struct_expr;
154  }
155  else if(expr.id()==ID_unary_minus)
156  {
157  auto const &unary_minus_expr = to_unary_minus_expr(expr);
158  // do component-wise:
159  // -x -> complex(-x.r,-x.i)
160  struct_exprt struct_expr(
161  {unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real)),
162  unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag))},
163  unary_minus_expr.type());
164 
165  struct_expr.op0().add_source_location() =
166  unary_minus_expr.source_location();
167 
168  struct_expr.op1().add_source_location() =
169  unary_minus_expr.source_location();
170 
171  expr=struct_expr;
172  }
173  else if(expr.id()==ID_complex)
174  {
175  auto const &complex_expr = to_complex_expr(expr);
176  auto struct_expr = struct_exprt(
177  {complex_expr.real(), complex_expr.imag()}, complex_expr.type());
178  struct_expr.add_source_location() = complex_expr.source_location();
179  expr.swap(struct_expr);
180  }
181  else if(expr.id()==ID_typecast)
182  {
183  auto const &typecast_expr = to_typecast_expr(expr);
184  typet subtype = typecast_expr.type().subtype();
185 
186  if(typecast_expr.op().type().id() == ID_struct)
187  {
188  // complex to complex -- do typecast per component
189 
190  struct_exprt struct_expr(
191  {typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype),
193  complex_member(typecast_expr.op(), ID_imag), subtype)},
194  typecast_expr.type());
195 
196  struct_expr.op0().add_source_location() =
197  typecast_expr.source_location();
198 
199  struct_expr.op1().add_source_location() =
200  typecast_expr.source_location();
201 
202  expr=struct_expr;
203  }
204  else
205  {
206  // non-complex to complex
207  struct_exprt struct_expr(
208  {typecast_exprt(typecast_expr.op(), subtype),
209  from_integer(0, subtype)},
210  typecast_expr.type());
211  struct_expr.add_source_location() = typecast_expr.source_location();
212 
213  expr=struct_expr;
214  }
215  }
216  }
217 
218  if(expr.id()==ID_complex_real)
219  {
220  expr = complex_member(to_complex_real_expr(expr).op(), ID_real);
221  }
222  else if(expr.id()==ID_complex_imag)
223  {
224  expr = complex_member(to_complex_imag_expr(expr).op(), ID_imag);
225  }
226 
227  remove_complex(expr.type());
228 }
229 
231 static void remove_complex(typet &type)
232 {
233  if(!have_to_remove_complex(type))
234  return;
235 
236  if(type.id()==ID_struct || type.id()==ID_union)
237  {
238  struct_union_typet &struct_union_type=
239  to_struct_union_type(type);
240  for(struct_union_typet::componentst::iterator
241  it=struct_union_type.components().begin();
242  it!=struct_union_type.components().end();
243  it++)
244  {
245  remove_complex(it->type());
246  }
247  }
248  else if(type.id()==ID_pointer ||
249  type.id()==ID_vector ||
250  type.id()==ID_array)
251  {
252  remove_complex(type.subtype());
253  }
254  else if(type.id()==ID_complex)
255  {
256  remove_complex(type.subtype());
257 
258  // Replace by a struct with two members.
259  // The real part goes first.
260  struct_typet struct_type(
261  {{ID_real, type.subtype()}, {ID_imag, type.subtype()}});
262  struct_type.add_source_location()=type.source_location();
263 
264  type = std::move(struct_type);
265  }
266 }
267 
269 static void remove_complex(symbolt &symbol)
270 {
271  remove_complex(symbol.value);
272  remove_complex(symbol.type);
273 }
274 
276 void remove_complex(symbol_tablet &symbol_table)
277 {
278  for(const auto &named_symbol : symbol_table.symbols)
279  remove_complex(symbol_table.get_writeable_ref(named_symbol.first));
280 }
281 
283 static void remove_complex(
284  goto_functionst::goto_functiont &goto_function)
285 {
286  remove_complex(goto_function.type);
287 
288  for(auto &i : goto_function.body.instructions)
289  i.transform([](exprt e) -> optionalt<exprt> {
291  {
292  remove_complex(e);
293  return e;
294  }
295  else
296  return {};
297  });
298 }
299 
301 static void remove_complex(goto_functionst &goto_functions)
302 {
303  Forall_goto_functions(it, goto_functions)
304  remove_complex(it->second);
305 }
306 
309  symbol_tablet &symbol_table,
310  goto_functionst &goto_functions)
311 {
312  remove_complex(symbol_table);
313  remove_complex(goto_functions);
314 }
315 
317 void remove_complex(goto_modelt &goto_model)
318 {
319  remove_complex(goto_model.symbol_table, goto_model.goto_functions);
320 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
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
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1740
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1721
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1766
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
remove_complex.h
Remove the 'complex' data type by compilation into structs.
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.
complex_member
static exprt complex_member(const exprt &expr, irep_idt id)
Definition: remove_complex.cpp:22
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
have_to_remove_complex
static bool have_to_remove_complex(const typet &type)
Definition: remove_complex.cpp:79
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1811
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:231
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
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
binary_exprt::op0
exprt & op0()
Definition: expr.h:102