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