cprover
Loading...
Searching...
No Matches
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 expr.id()==ID_mult || expr.id()==ID_div)
132 {
133 // FIXME plus and mult are defined as n-ary operations
134 // rather than binary. This code assumes that they
135 // can only have exactly 2 operands, and it is not clear
136 // that it is safe to do so in this context
137 PRECONDITION(expr.operands().size() == 2);
138 // do component-wise:
139 // x+y -> complex(x.r+y.r,x.i+y.i)
143 expr.id(),
147 expr.id(),
148 complex_member(to_binary_expr(expr).op1(), ID_imag))},
149 expr.type());
150
151 struct_expr.op0().add_source_location() = expr.source_location();
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)
164 unary_minus_expr.type());
165
166 struct_expr.op0().add_source_location() =
167 unary_minus_expr.source_location();
168
169 struct_expr.op1().add_source_location() =
170 unary_minus_expr.source_location();
171
172 expr=struct_expr;
173 }
174 else if(expr.id()==ID_complex)
175 {
176 auto const &complex_expr = to_complex_expr(expr);
178 {complex_expr.real(), complex_expr.imag()}, complex_expr.type());
179 struct_expr.add_source_location() = complex_expr.source_location();
180 expr.swap(struct_expr);
181 }
182 else if(expr.id()==ID_typecast)
183 {
184 auto const &typecast_expr = to_typecast_expr(expr);
185 typet subtype = to_complex_type(typecast_expr.type()).subtype();
186
187 if(typecast_expr.op().type().id() == ID_struct)
188 {
189 // complex to complex -- do typecast per component
190
194 complex_member(typecast_expr.op(), ID_imag), subtype)},
195 typecast_expr.type());
196
197 struct_expr.op0().add_source_location() =
198 typecast_expr.source_location();
199
200 struct_expr.op1().add_source_location() =
201 typecast_expr.source_location();
202
203 expr=struct_expr;
204 }
205 else
206 {
207 // non-complex to complex
209 {typecast_exprt(typecast_expr.op(), subtype),
210 from_integer(0, subtype)},
211 typecast_expr.type());
212 struct_expr.add_source_location() = typecast_expr.source_location();
213
214 expr=struct_expr;
215 }
216 }
217 }
218
219 if(expr.id()==ID_complex_real)
220 {
221 expr = complex_member(to_complex_real_expr(expr).op(), ID_real);
222 }
223 else if(expr.id()==ID_complex_imag)
224 {
225 expr = complex_member(to_complex_imag_expr(expr).op(), ID_imag);
226 }
227
228 remove_complex(expr.type());
229}
230
232static void remove_complex(typet &type)
233{
234 if(!have_to_remove_complex(type))
235 return;
236
237 if(type.id()==ID_struct || type.id()==ID_union)
238 {
241 for(struct_union_typet::componentst::iterator
242 it=struct_union_type.components().begin();
243 it!=struct_union_type.components().end();
244 it++)
245 {
246 remove_complex(it->type());
247 }
248 }
249 else if(type.id()==ID_pointer ||
250 type.id()==ID_vector ||
251 type.id()==ID_array)
252 {
253 remove_complex(to_type_with_subtype(type).subtype());
254 }
255 else if(type.id()==ID_complex)
256 {
257 remove_complex(to_complex_type(type).subtype());
258
259 // Replace by a struct with two members.
260 // The real part goes first.
262 {{ID_real, to_complex_type(type).subtype()},
263 {ID_imag, to_complex_type(type).subtype()}});
264 struct_type.add_source_location()=type.source_location();
265
266 type = std::move(struct_type);
267 }
268}
269
271static void remove_complex(symbolt &symbol)
272{
273 remove_complex(symbol.value);
274 remove_complex(symbol.type);
275}
276
278static void remove_complex(symbol_table_baset &symbol_table)
279{
280 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
281 remove_complex(it.get_writeable_symbol());
282}
283
285static void remove_complex(
286 goto_functionst::goto_functiont &goto_function)
287{
288 for(auto &i : goto_function.body.instructions)
289 i.transform([](exprt e) -> optionalt<exprt> {
291 {
293 return e;
294 }
295 else
296 return {};
297 });
298}
299
301static void remove_complex(goto_functionst &goto_functions)
302{
303 for(auto &gf_entry : goto_functions.function_map)
304 remove_complex(gf_entry.second);
305}
306
309 symbol_table_baset &symbol_table,
310 goto_functionst &goto_functions)
311{
312 remove_complex(symbol_table);
313 remove_complex(goto_functions);
314}
315
318{
319 remove_complex(goto_model.symbol_table, goto_model.goto_functions);
320}
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:563
A base class for binary expressions.
Definition std_expr.h:583
Real part of the expression describing a complex number.
Definition std_expr.h:1926
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:223
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:442
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
Struct constructor from list of elements.
Definition std_expr.h:1819
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:2017
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:423
#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:2051
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:1997
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:1952
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1907
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:453
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:1102
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:175