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 expr.op0();
28  else if(id==ID_imag)
29  return 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(expr.type());
140  struct_expr.operands().resize(2);
141 
142  struct_expr.op0()=
143  binary_exprt(complex_member(expr.op0(), ID_real), expr.id(),
144  complex_member(expr.op1(), ID_real));
145 
146  struct_expr.op0().add_source_location()=expr.source_location();
147 
148  struct_expr.op1()=
149  binary_exprt(complex_member(expr.op0(), ID_imag), expr.id(),
150  complex_member(expr.op1(), ID_imag));
151 
152  struct_expr.op1().add_source_location()=expr.source_location();
153 
154  expr=struct_expr;
155  }
156  else if(expr.id()==ID_unary_minus)
157  {
158  auto const &unary_minus_expr = to_unary_minus_expr(expr);
159  // do component-wise:
160  // -x -> complex(-x.r,-x.i)
161  struct_exprt struct_expr(unary_minus_expr.type());
162  struct_expr.operands().resize(2);
163 
164  struct_expr.op0() =
165  unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real));
166 
167  struct_expr.op0().add_source_location() =
168  unary_minus_expr.source_location();
169 
170  struct_expr.op1() =
171  unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag));
172 
173  struct_expr.op1().add_source_location() =
174  unary_minus_expr.source_location();
175 
176  expr=struct_expr;
177  }
178  else if(expr.id()==ID_complex)
179  {
180  auto const &complex_expr = to_complex_expr(expr);
181  auto struct_expr = struct_exprt(complex_expr.type());
182  struct_expr.add_source_location() = complex_expr.source_location();
183  struct_expr.copy_to_operands(complex_expr.real(), complex_expr.imag());
184  expr.swap(struct_expr);
185  }
186  else if(expr.id()==ID_typecast)
187  {
188  auto const &typecast_expr = to_typecast_expr(expr);
189  typet subtype = typecast_expr.type().subtype();
190 
191  if(typecast_expr.op().type().id() == ID_struct)
192  {
193  // complex to complex -- do typecast per component
194 
195  struct_exprt struct_expr(typecast_expr.type());
196  struct_expr.operands().resize(2);
197 
198  struct_expr.op0() =
199  typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype);
200 
201  struct_expr.op0().add_source_location() =
202  typecast_expr.source_location();
203 
204  struct_expr.op1() =
205  typecast_exprt(complex_member(typecast_expr.op(), ID_imag), subtype);
206 
207  struct_expr.op1().add_source_location() =
208  typecast_expr.source_location();
209 
210  expr=struct_expr;
211  }
212  else
213  {
214  // non-complex to complex
215  struct_exprt struct_expr(typecast_expr.type());
216  struct_expr.operands().resize(2);
217 
218  struct_expr.op0() = typecast_exprt(typecast_expr.op(), subtype);
219  struct_expr.op1()=from_integer(0, subtype);
220  struct_expr.add_source_location() = typecast_expr.source_location();
221 
222  expr=struct_expr;
223  }
224  }
225  }
226 
227  if(expr.id()==ID_complex_real)
228  {
229  expr = complex_member(to_complex_real_expr(expr).op0(), ID_real);
230  }
231  else if(expr.id()==ID_complex_imag)
232  {
233  expr = complex_member(to_complex_imag_expr(expr).op0(), ID_imag);
234  }
235 
236  remove_complex(expr.type());
237 }
238 
240 static void remove_complex(typet &type)
241 {
242  if(!have_to_remove_complex(type))
243  return;
244 
245  if(type.id()==ID_struct || type.id()==ID_union)
246  {
247  struct_union_typet &struct_union_type=
248  to_struct_union_type(type);
249  for(struct_union_typet::componentst::iterator
250  it=struct_union_type.components().begin();
251  it!=struct_union_type.components().end();
252  it++)
253  {
254  remove_complex(it->type());
255  }
256  }
257  else if(type.id()==ID_pointer ||
258  type.id()==ID_vector ||
259  type.id()==ID_array)
260  {
261  remove_complex(type.subtype());
262  }
263  else if(type.id()==ID_complex)
264  {
265  remove_complex(type.subtype());
266 
267  // Replace by a struct with two members.
268  // The real part goes first.
269  struct_typet struct_type;
270  struct_type.add_source_location()=type.source_location();
271  struct_type.components().resize(2);
272  struct_type.components()[0].type()=type.subtype();
273  struct_type.components()[0].set_name(ID_real);
274  struct_type.components()[1].type()=type.subtype();
275  struct_type.components()[1].set_name(ID_imag);
276 
277  type=struct_type;
278  }
279 }
280 
282 static void remove_complex(symbolt &symbol)
283 {
284  remove_complex(symbol.value);
285  remove_complex(symbol.type);
286 }
287 
289 void remove_complex(symbol_tablet &symbol_table)
290 {
291  for(const auto &named_symbol : symbol_table.symbols)
292  remove_complex(*symbol_table.get_writeable(named_symbol.first));
293 }
294 
296 static void remove_complex(
297  goto_functionst::goto_functiont &goto_function)
298 {
299  remove_complex(goto_function.type);
300 
301  Forall_goto_program_instructions(it, goto_function.body)
302  {
303  remove_complex(it->code);
304  remove_complex(it->guard);
305  }
306 }
307 
309 static void remove_complex(goto_functionst &goto_functions)
310 {
311  Forall_goto_functions(it, goto_functions)
312  remove_complex(it->second);
313 }
314 
317  symbol_tablet &symbol_table,
318  goto_functionst &goto_functions)
319 {
320  remove_complex(symbol_table);
321  remove_complex(goto_functions);
322 }
323 
325 void remove_complex(goto_modelt &goto_model)
326 {
327  remove_complex(goto_model.symbol_table, goto_model.goto_functions);
328 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
typet::subtype
const typet & subtype() const
Definition: type.h:38
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
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:349
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:260
typet
The type of an expression, extends irept.
Definition: type.h:27
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:114
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:2040
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt::op1
const exprt & op1() const =delete
goto_modelt
Definition: goto_model.h:24
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:2011
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:738
exprt::op0
exprt & op0()
Definition: expr.h:84
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
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:2055
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
remove_complex.h
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
std_types.h
exprt::op1
exprt & op1()
Definition: expr.h:87
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:496
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:469
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:67
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:2102
remove_complex
static void remove_complex(typet &)
removes complex data type
Definition: remove_complex.cpp:240
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
symbol_tablet::get_writeable
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
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
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:276
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
symbolt
Symbol table entry.
Definition: symbol.h:27
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
exprt::operands
operandst & operands()
Definition: expr.h:78
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
std_expr.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29