CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
remove_complex.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove 'complex' data type
4
5Author: Daniel Kroening
6
7Date: 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
21static 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 {
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
41static bool have_to_remove_complex(const typet &type);
42
43static 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
69 return true;
70
71 for(const auto &op : expr.operands())
72 {
74 return true;
75 }
76
77 return false;
78}
79
80static bool have_to_remove_complex(const typet &type)
81{
82 if(type.id()==ID_struct || type.id()==ID_union)
83 {
84 for(const auto &c : to_struct_union_type(type).components())
85 if(have_to_remove_complex(c.type()))
86 return true;
87 }
88 else if(type.id()==ID_pointer ||
89 type.id()==ID_vector ||
90 type.id()==ID_array)
91 return have_to_remove_complex(to_type_with_subtype(type).subtype());
92 else if(type.id()==ID_complex)
93 return true;
94
95 return false;
96}
97
99static void remove_complex(typet &);
100
101static void remove_complex(exprt &expr)
102{
103 if(!have_to_remove_complex(expr))
104 return;
105
106 if(expr.id()==ID_typecast)
107 {
108 auto const &typecast_expr = to_typecast_expr(expr);
109 if(typecast_expr.op().type().id() == ID_complex)
110 {
111 if(typecast_expr.type().id() == ID_complex)
112 {
113 // complex to complex
114 }
115 else
116 {
117 // cast complex to non-complex is (T)__real__ x
119
121 }
122 }
123 }
124
125 Forall_operands(it, expr)
126 remove_complex(*it);
127
128 if(expr.type().id()==ID_complex)
129 {
130 if(expr.id() == ID_plus || expr.id() == ID_minus)
131 {
132 // plus and mult are n-ary expressions, but front-ends currently ensure
133 // that we only see them as binary ones
134 PRECONDITION(expr.operands().size() == 2);
135 // do component-wise:
136 // x+y -> complex(x.r+y.r,x.i+y.i)
140 expr.id(),
144 expr.id(),
145 complex_member(to_binary_expr(expr).op1(), ID_imag))},
146 expr.type());
147
148 struct_expr.op0().add_source_location() = expr.source_location();
149 struct_expr.op1().add_source_location()=expr.source_location();
150
151 expr=struct_expr;
152 }
153 else if(expr.id() == ID_mult)
154 {
155 // plus and mult are n-ary expressions, but front-ends currently ensure
156 // that we only see them as binary ones
157 PRECONDITION(expr.operands().size() == 2);
162
168 expr.type()};
169
170 struct_expr.op0().add_source_location() = expr.source_location();
171 struct_expr.op1().add_source_location() = expr.source_location();
172
173 expr = struct_expr;
174 }
175 else if(expr.id() == ID_div)
176 {
181
186
187 plus_exprt denominator{
189
191 {div_exprt{numerator_real, denominator},
192 div_exprt{numerator_imag, denominator}},
193 expr.type()};
194
195 struct_expr.op0().add_source_location() = expr.source_location();
196 struct_expr.op1().add_source_location() = expr.source_location();
197
198 expr = struct_expr;
199 }
200 else if(expr.id()==ID_unary_minus)
201 {
202 auto const &unary_minus_expr = to_unary_minus_expr(expr);
203 // do component-wise:
204 // -x -> complex(-x.r,-x.i)
208 unary_minus_expr.type());
209
210 struct_expr.op0().add_source_location() =
211 unary_minus_expr.source_location();
212
213 struct_expr.op1().add_source_location() =
214 unary_minus_expr.source_location();
215
216 expr=struct_expr;
217 }
218 else if(expr.id()==ID_complex)
219 {
220 auto const &complex_expr = to_complex_expr(expr);
222 {complex_expr.real(), complex_expr.imag()}, complex_expr.type());
223 struct_expr.add_source_location() = complex_expr.source_location();
224 expr.swap(struct_expr);
225 }
226 else if(expr.id()==ID_typecast)
227 {
228 auto const &typecast_expr = to_typecast_expr(expr);
229 typet subtype = to_complex_type(typecast_expr.type()).subtype();
230
231 if(typecast_expr.op().type().id() == ID_struct)
232 {
233 // complex to complex -- do typecast per component
234
238 complex_member(typecast_expr.op(), ID_imag), subtype)},
239 typecast_expr.type());
240
241 struct_expr.op0().add_source_location() =
242 typecast_expr.source_location();
243
244 struct_expr.op1().add_source_location() =
245 typecast_expr.source_location();
246
247 expr=struct_expr;
248 }
249 else
250 {
251 // non-complex to complex
253 {typecast_exprt(typecast_expr.op(), subtype),
254 from_integer(0, subtype)},
255 typecast_expr.type());
256 struct_expr.add_source_location() = typecast_expr.source_location();
257
258 expr=struct_expr;
259 }
260 }
261 }
262
263 if(expr.id()==ID_complex_real)
264 {
265 expr = complex_member(to_complex_real_expr(expr).op(), ID_real);
266 }
267 else if(expr.id()==ID_complex_imag)
268 {
269 expr = complex_member(to_complex_imag_expr(expr).op(), ID_imag);
270 }
271
272 remove_complex(expr.type());
273}
274
276static void remove_complex(typet &type)
277{
278 if(!have_to_remove_complex(type))
279 return;
280
281 if(type.id()==ID_struct || type.id()==ID_union)
282 {
285 for(struct_union_typet::componentst::iterator
286 it=struct_union_type.components().begin();
287 it!=struct_union_type.components().end();
288 it++)
289 {
290 remove_complex(it->type());
291 }
292 }
293 else if(type.id()==ID_pointer ||
294 type.id()==ID_vector ||
295 type.id()==ID_array)
296 {
297 remove_complex(to_type_with_subtype(type).subtype());
298 }
299 else if(type.id()==ID_complex)
300 {
301 remove_complex(to_complex_type(type).subtype());
302
303 // Replace by a struct with two members.
304 // The real part goes first.
306 {{ID_real, to_complex_type(type).subtype()},
307 {ID_imag, to_complex_type(type).subtype()}});
308 struct_type.add_source_location()=type.source_location();
309
310 type = std::move(struct_type);
311 }
312}
313
315static void remove_complex(symbolt &symbol)
316{
317 remove_complex(symbol.value);
318 remove_complex(symbol.type);
319}
320
322static void remove_complex(symbol_table_baset &symbol_table)
323{
324 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
325 remove_complex(it.get_writeable_symbol());
326}
327
329static void remove_complex(
330 goto_functionst::goto_functiont &goto_function)
331{
332 for(auto &i : goto_function.body.instructions)
333 i.transform([](exprt e) -> std::optional<exprt> {
335 {
337 return e;
338 }
339 else
340 return {};
341 });
342}
343
345static void remove_complex(goto_functionst &goto_functions)
346{
347 for(auto &gf_entry : goto_functions.function_map)
348 remove_complex(gf_entry.second);
349}
350
353 symbol_table_baset &symbol_table,
354 goto_functionst &goto_functions)
355{
356 remove_complex(symbol_table);
357 remove_complex(goto_functions);
358}
359
362{
363 remove_complex(goto_model.symbol_table, goto_model.goto_functions);
364}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for binary expressions.
Definition std_expr.h:638
Real part of the expression describing a complex number.
Definition std_expr.h:1984
Division.
Definition std_expr.h:1157
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2971
Binary minus.
Definition std_expr.h:1061
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
The plus expression Associativity is not specified.
Definition std_expr.h:1002
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
The symbol table base class interface.
virtual iteratort begin()=0
virtual iteratort end()=0
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:2073
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:72
The unary minus expression.
Definition std_expr.h:484
#define Forall_operands(it, expr)
Definition expr.h:27
Symbol Table + CFG.
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:525
#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:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1965
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208