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 {
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
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 forall_operands(it, expr)
73 return true;
74
75 return false;
76}
77
78static 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(to_type_with_subtype(type).subtype());
90 else if(type.id()==ID_complex)
91 return true;
92
93 return false;
94}
95
97static void remove_complex(typet &);
98
99static 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(
140 complex_member(to_binary_expr(expr).op0(), ID_real),
141 expr.id(),
142 complex_member(to_binary_expr(expr).op1(), ID_real)),
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 = to_complex_type(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
230static 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=
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
268static void remove_complex(symbolt &symbol)
269{
270 remove_complex(symbol.value);
271 remove_complex(symbol.type);
272}
273
275void 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
282static 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 {
290 return e;
291 }
292 else
293 return {};
294 });
295}
296
298static 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
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 & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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
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:2667
exprt & op0()
Definition: std_expr.h:844
Struct constructor from list of elements.
Definition: std_expr.h:1722
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
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
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:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_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:1855
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1810
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 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:1082
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:177