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  assert(expr.type().id()==ID_struct);
36  const struct_typet &struct_type=
37  to_struct_type(expr.type());
38  assert(struct_type.components().size()==2);
39  return member_exprt(expr, id, struct_type.components().front().type());
40  }
41 }
42 
43 static bool have_to_remove_complex(const typet &type);
44 
45 static bool have_to_remove_complex(const exprt &expr)
46 {
47  if(expr.id()==ID_typecast &&
48  to_typecast_expr(expr).op().type().id()==ID_complex &&
49  expr.type().id()!=ID_complex)
50  return true;
51 
52  if(expr.type().id()==ID_complex)
53  {
54  if(expr.id()==ID_plus || expr.id()==ID_minus ||
55  expr.id()==ID_mult || expr.id()==ID_div)
56  return true;
57  else if(expr.id()==ID_unary_minus)
58  return true;
59  else if(expr.id()==ID_complex)
60  return true;
61  else if(expr.id()==ID_typecast)
62  return true;
63  }
64 
65  if(expr.id()==ID_complex_real)
66  return true;
67  else if(expr.id()==ID_complex_imag)
68  return true;
69 
70  if(have_to_remove_complex(expr.type()))
71  return true;
72 
73  forall_operands(it, expr)
74  if(have_to_remove_complex(*it))
75  return true;
76 
77  return false;
78 }
79 
80 static bool have_to_remove_complex(const typet &type)
81 {
82  if(type.id()==ID_struct || type.id()==ID_union)
83  {
84  const struct_union_typet &struct_union_type=
86  for(struct_union_typet::componentst::const_iterator
87  it=struct_union_type.components().begin();
88  it!=struct_union_type.components().end();
89  it++)
90  if(have_to_remove_complex(it->type()))
91  return true;
92  }
93  else if(type.id()==ID_pointer ||
94  type.id()==ID_vector ||
95  type.id()==ID_array)
96  return have_to_remove_complex(type.subtype());
97  else if(type.id()==ID_complex)
98  return true;
99 
100  return false;
101 }
102 
104 static void remove_complex(typet &);
105 
106 static void remove_complex(exprt &expr)
107 {
108  if(!have_to_remove_complex(expr))
109  return;
110 
111  if(expr.id()==ID_typecast)
112  {
113  assert(expr.operands().size()==1);
114  if(expr.op0().type().id()==ID_complex)
115  {
116  if(expr.type().id()==ID_complex)
117  {
118  // complex to complex
119  }
120  else
121  {
122  // cast complex to non-complex is (T)__real__ x
123  unary_exprt tmp(
124  ID_complex_real, expr.op0(), expr.op0().type().subtype());
125 
126  expr=typecast_exprt(tmp, expr.type());
127  }
128  }
129  }
130 
131  Forall_operands(it, expr)
132  remove_complex(*it);
133 
134  if(expr.type().id()==ID_complex)
135  {
136  if(expr.id()==ID_plus || expr.id()==ID_minus ||
137  expr.id()==ID_mult || expr.id()==ID_div)
138  {
139  assert(expr.operands().size()==2);
140  // do component-wise:
141  // x+y -> complex(x.r+y.r,x.i+y.i)
142  struct_exprt struct_expr(expr.type());
143  struct_expr.operands().resize(2);
144 
145  struct_expr.op0()=
146  binary_exprt(complex_member(expr.op0(), ID_real), expr.id(),
147  complex_member(expr.op1(), ID_real));
148 
149  struct_expr.op0().add_source_location()=expr.source_location();
150 
151  struct_expr.op1()=
152  binary_exprt(complex_member(expr.op0(), ID_imag), expr.id(),
153  complex_member(expr.op1(), ID_imag));
154 
155  struct_expr.op1().add_source_location()=expr.source_location();
156 
157  expr=struct_expr;
158  }
159  else if(expr.id()==ID_unary_minus)
160  {
161  assert(expr.operands().size()==1);
162  // do component-wise:
163  // -x -> complex(-x.r,-x.i)
164  struct_exprt struct_expr(expr.type());
165  struct_expr.operands().resize(2);
166 
167  struct_expr.op0()=
168  unary_minus_exprt(complex_member(expr.op0(), ID_real));
169 
170  struct_expr.op0().add_source_location()=expr.source_location();
171 
172  struct_expr.op1()=
173  unary_minus_exprt(complex_member(expr.op0(), ID_imag));
174 
175  struct_expr.op1().add_source_location()=expr.source_location();
176 
177  expr=struct_expr;
178  }
179  else if(expr.id()==ID_complex)
180  {
181  assert(expr.operands().size()==2);
182  expr.id(ID_struct);
183  }
184  else if(expr.id()==ID_typecast)
185  {
186  assert(expr.operands().size()==1);
187  typet subtype=expr.type().subtype();
188 
189  if(expr.op0().type().id()==ID_struct)
190  {
191  // complex to complex -- do typecast per component
192 
193  struct_exprt struct_expr(expr.type());
194  struct_expr.operands().resize(2);
195 
196  struct_expr.op0()=
197  typecast_exprt(complex_member(expr.op0(), ID_real), subtype);
198 
199  struct_expr.op0().add_source_location()=expr.source_location();
200 
201  struct_expr.op1()=
202  typecast_exprt(complex_member(expr.op0(), ID_imag), subtype);
203 
204  struct_expr.op1().add_source_location()=expr.source_location();
205 
206  expr=struct_expr;
207  }
208  else
209  {
210  // non-complex to complex
211  struct_exprt struct_expr(expr.type());
212  struct_expr.operands().resize(2);
213 
214  struct_expr.op0()=typecast_exprt(expr.op0(), subtype);
215  struct_expr.op1()=from_integer(0, subtype);
216  struct_expr.add_source_location()=expr.source_location();
217 
218  expr=struct_expr;
219  }
220  }
221  }
222 
223  if(expr.id()==ID_complex_real)
224  {
225  assert(expr.operands().size()==1);
226  expr=complex_member(expr.op0(), ID_real);
227  }
228  else if(expr.id()==ID_complex_imag)
229  {
230  assert(expr.operands().size()==1);
231  expr=complex_member(expr.op0(), ID_imag);
232  }
233 
234  remove_complex(expr.type());
235 }
236 
238 static void remove_complex(typet &type)
239 {
240  if(!have_to_remove_complex(type))
241  return;
242 
243  if(type.id()==ID_struct || type.id()==ID_union)
244  {
245  struct_union_typet &struct_union_type=
246  to_struct_union_type(type);
247  for(struct_union_typet::componentst::iterator
248  it=struct_union_type.components().begin();
249  it!=struct_union_type.components().end();
250  it++)
251  {
252  remove_complex(it->type());
253  }
254  }
255  else if(type.id()==ID_pointer ||
256  type.id()==ID_vector ||
257  type.id()==ID_array)
258  {
259  remove_complex(type.subtype());
260  }
261  else if(type.id()==ID_complex)
262  {
263  remove_complex(type.subtype());
264 
265  // Replace by a struct with two members.
266  // The real part goes first.
267  struct_typet struct_type;
268  struct_type.add_source_location()=type.source_location();
269  struct_type.components().resize(2);
270  struct_type.components()[0].type()=type.subtype();
271  struct_type.components()[0].set_name(ID_real);
272  struct_type.components()[1].type()=type.subtype();
273  struct_type.components()[1].set_name(ID_imag);
274 
275  type=struct_type;
276  }
277 }
278 
280 static void remove_complex(symbolt &symbol)
281 {
282  remove_complex(symbol.value);
283  remove_complex(symbol.type);
284 }
285 
287 void remove_complex(symbol_tablet &symbol_table)
288 {
289  for(const auto &named_symbol : symbol_table.symbols)
290  remove_complex(*symbol_table.get_writeable(named_symbol.first));
291 }
292 
294 static void remove_complex(
295  goto_functionst::goto_functiont &goto_function)
296 {
297  remove_complex(goto_function.type);
298 
299  Forall_goto_program_instructions(it, goto_function.body)
300  {
301  remove_complex(it->code);
302  remove_complex(it->guard);
303  }
304 }
305 
307 static void remove_complex(goto_functionst &goto_functions)
308 {
309  Forall_goto_functions(it, goto_functions)
310  remove_complex(it->second);
311 }
312 
315  symbol_tablet &symbol_table,
316  goto_functionst &goto_functions)
317 {
318  remove_complex(symbol_table);
319  remove_complex(goto_functions);
320 }
321 
323 void remove_complex(goto_modelt &goto_model)
324 {
325  remove_complex(goto_model.symbol_table, goto_model.goto_functions);
326 }
The type of an expression.
Definition: type.h:22
semantic type conversion
Definition: std_expr.h:2111
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
Remove the &#39;complex&#39; data type by compilation into structs.
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
static exprt complex_member(const exprt &expr, irep_idt id)
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
Structure type.
Definition: std_types.h:297
Extract member of struct or union.
Definition: std_expr.h:3871
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
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
#define forall_operands(it, expr)
Definition: expr.h:17
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
The unary minus expression.
Definition: std_expr.h:444
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
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)
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
static bool have_to_remove_complex(const typet &type)
#define Forall_operands(it, expr)
Definition: expr.h:23
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
static void remove_complex(typet &)
removes complex data type
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)
struct constructor from list of elements
Definition: std_expr.h:1815
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32