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