Skip to content

Commit 9629f3c

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #150 from tautschnig/efficient-rewrites
Expression transformations for symbolic execution need only be done once
2 parents 972c4c7 + 979d120 commit 9629f3c

File tree

10 files changed

+455
-40
lines changed

10 files changed

+455
-40
lines changed

‎src/cbmc/cbmc_parse_options.cpp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,9 @@ Author: Daniel Kroening, [email protected]
3939
#include <goto-programs/remove_skip.h>
4040
#include <goto-programs/show_goto_functions.h>
4141

42+
#include <goto-symex/rewrite_union.h>
43+
#include <goto-symex/adjust_float_expressions.h>
44+
4245
#include <goto-instrument/full_slicer.h>
4346
#include <goto-instrument/nondet_static.h>
4447
#include <goto-instrument/cover.h>
@@ -898,10 +901,13 @@ bool cbmc_parse_optionst::process_goto_program(
898901
remove_returns(symbol_table, goto_functions);
899902
remove_vector(symbol_table, goto_functions);
900903
remove_complex(symbol_table, goto_functions);
904+
rewrite_union(goto_functions, ns);
901905

902906
// add generic checks
903907
status() << "Generic Property Instrumentation" << eom;
904908
goto_check(ns, options, goto_functions);
909+
// checks don't know about adjusted float expressions
910+
adjust_float_expressions(goto_functions, ns);
905911

906912
// ignore default/user-specified initialization
907913
// of variables with static lifetime

‎src/goto-programs/remove_complex.cpp‎

Lines changed: 99 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,6 @@ Date: September 2014
1212

1313
#include "remove_complex.h"
1414

15-
void remove_complex(typet &);
16-
void remove_complex(exprt &);
17-
1815
/*******************************************************************\
1916
2017
Function: complex_member
@@ -27,7 +24,7 @@ Function: complex_member
2724
2825
\*******************************************************************/
2926

30-
exprt complex_member(const exprt &expr, irep_idt id)
27+
static exprt complex_member(const exprt &expr, irep_idt id)
3128
{
3229
if(expr.id()==ID_struct && expr.operands().size()==2)
3330
{
@@ -50,6 +47,90 @@ exprt complex_member(const exprt &expr, irep_idt id)
5047

5148
/*******************************************************************\
5249
50+
Function: have_to_remove_complex
51+
52+
Inputs:
53+
54+
Outputs:
55+
56+
Purpose:
57+
58+
\*******************************************************************/
59+
60+
static bool have_to_remove_complex(const typet &type);
61+
62+
static bool have_to_remove_complex(const exprt &expr)
63+
{
64+
if(expr.id()==ID_typecast &&
65+
to_typecast_expr(expr).op().type().id()==ID_complex &&
66+
expr.type().id()!=ID_complex)
67+
return true;
68+
69+
if(expr.type().id()==ID_complex)
70+
{
71+
if(expr.id()==ID_plus || expr.id()==ID_minus ||
72+
expr.id()==ID_mult || expr.id()==ID_div)
73+
return true;
74+
else if(expr.id()==ID_unary_minus)
75+
return true;
76+
else if(expr.id()==ID_complex)
77+
return true;
78+
else if(expr.id()==ID_typecast)
79+
return true;
80+
}
81+
82+
if(expr.id()==ID_complex_real)
83+
return true;
84+
else if(expr.id()==ID_complex_imag)
85+
return true;
86+
87+
if(have_to_remove_complex(expr.type()))
88+
return true;
89+
90+
forall_operands(it, expr)
91+
if(have_to_remove_complex(*it))
92+
return true;
93+
94+
return false;
95+
}
96+
97+
/*******************************************************************\
98+
99+
Function: have_to_remove_complex
100+
101+
Inputs:
102+
103+
Outputs:
104+
105+
Purpose:
106+
107+
\*******************************************************************/
108+
109+
static bool have_to_remove_complex(const typet &type)
110+
{
111+
if(type.id()==ID_struct || type.id()==ID_union)
112+
{
113+
const struct_union_typet &struct_union_type=
114+
to_struct_union_type(type);
115+
for(struct_union_typet::componentst::const_iterator
116+
it=struct_union_type.components().begin();
117+
it!=struct_union_type.components().end();
118+
it++)
119+
if(have_to_remove_complex(it->type()))
120+
return true;
121+
}
122+
else if(type.id()==ID_pointer ||
123+
type.id()==ID_vector ||
124+
type.id()==ID_array)
125+
return have_to_remove_complex(type.subtype());
126+
else if(type.id()==ID_complex)
127+
return true;
128+
129+
return false;
130+
}
131+
132+
/*******************************************************************\
133+
53134
Function: remove_complex
54135
55136
Inputs:
@@ -60,8 +141,13 @@ Purpose: removes complex data type
60141
61142
\*******************************************************************/
62143

63-
void remove_complex(exprt &expr)
144+
static void remove_complex(typet &);
145+
146+
static void remove_complex(exprt &expr)
64147
{
148+
if(!have_to_remove_complex(expr))
149+
return;
150+
65151
if(expr.id()==ID_typecast)
66152
{
67153
assert(expr.operands().size()==1);
@@ -200,8 +286,11 @@ Purpose: removes complex data type
200286
201287
\*******************************************************************/
202288

203-
void remove_complex(typet &type)
289+
static void remove_complex(typet &type)
204290
{
291+
if(!have_to_remove_complex(type))
292+
return;
293+
205294
if(type.id()==ID_struct || type.id()==ID_union)
206295
{
207296
struct_union_typet &struct_union_type=
@@ -250,7 +339,7 @@ Purpose: removes complex data type
250339
251340
\*******************************************************************/
252341

253-
void remove_complex(symbolt &symbol)
342+
static void remove_complex(symbolt &symbol)
254343
{
255344
remove_complex(symbol.value);
256345
remove_complex(symbol.type);
@@ -286,7 +375,8 @@ Purpose: removes complex data type
286375
287376
\*******************************************************************/
288377

289-
void remove_complex(goto_functionst::goto_functiont &goto_function)
378+
static void remove_complex(
379+
goto_functionst::goto_functiont &goto_function)
290380
{
291381
remove_complex(goto_function.type);
292382

@@ -309,7 +399,7 @@ Purpose: removes complex data type
309399
310400
\*******************************************************************/
311401

312-
void remove_complex(goto_functionst &goto_functions)
402+
static void remove_complex(goto_functionst &goto_functions)
313403
{
314404
Forall_goto_functions(it, goto_functions)
315405
remove_complex(it->second);

‎src/goto-programs/remove_vector.cpp‎

Lines changed: 87 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,80 @@ Date: September 2014
1212

1313
#include "remove_vector.h"
1414

15-
void remove_vector(typet &);
16-
void remove_vector(exprt &);
15+
/*******************************************************************\
16+
17+
Function: have_to_remove_vector
18+
19+
Inputs:
20+
21+
Outputs:
22+
23+
Purpose:
24+
25+
\*******************************************************************/
26+
27+
static bool have_to_remove_vector(const typet &type);
28+
29+
static bool have_to_remove_vector(const exprt &expr)
30+
{
31+
if(expr.type().id()==ID_vector)
32+
{
33+
if(expr.id()==ID_plus || expr.id()==ID_minus ||
34+
expr.id()==ID_mult || expr.id()==ID_div ||
35+
expr.id()==ID_mod || expr.id()==ID_bitxor ||
36+
expr.id()==ID_bitand || expr.id()==ID_bitor)
37+
return true;
38+
else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
39+
return true;
40+
else if(expr.id()==ID_vector)
41+
return true;
42+
}
43+
44+
if(have_to_remove_vector(expr.type()))
45+
return true;
46+
47+
forall_operands(it, expr)
48+
if(have_to_remove_vector(*it))
49+
return true;
50+
51+
return false;
52+
}
53+
54+
/*******************************************************************\
55+
56+
Function: have_to_remove_vector
57+
58+
Inputs:
59+
60+
Outputs:
61+
62+
Purpose:
63+
64+
\*******************************************************************/
65+
66+
static bool have_to_remove_vector(const typet &type)
67+
{
68+
if(type.id()==ID_struct || type.id()==ID_union)
69+
{
70+
const struct_union_typet &struct_union_type=
71+
to_struct_union_type(type);
72+
73+
for(struct_union_typet::componentst::const_iterator
74+
it=struct_union_type.components().begin();
75+
it!=struct_union_type.components().end();
76+
it++)
77+
if(have_to_remove_vector(it->type()))
78+
return true;
79+
}
80+
else if(type.id()==ID_pointer ||
81+
type.id()==ID_complex ||
82+
type.id()==ID_array)
83+
return have_to_remove_vector(type.subtype());
84+
else if(type.id()==ID_vector)
85+
return true;
86+
87+
return false;
88+
}
1789

1890
/*******************************************************************\
1991
@@ -27,8 +99,13 @@ Purpose: removes vector data type
2799
28100
\*******************************************************************/
29101

30-
void remove_vector(exprt &expr)
102+
static void remove_vector(typet &);
103+
104+
static void remove_vector(exprt &expr)
31105
{
106+
if(!have_to_remove_vector(expr))
107+
return;
108+
32109
Forall_operands(it, expr)
33110
remove_vector(*it);
34111

@@ -109,8 +186,11 @@ Purpose: removes vector data type
109186
110187
\*******************************************************************/
111188

112-
void remove_vector(typet &type)
189+
static void remove_vector(typet &type)
113190
{
191+
if(!have_to_remove_vector(type))
192+
return;
193+
114194
if(type.id()==ID_struct || type.id()==ID_union)
115195
{
116196
struct_union_typet &struct_union_type=
@@ -155,7 +235,7 @@ Purpose: removes vector data type
155235
156236
\*******************************************************************/
157237

158-
void remove_vector(symbolt &symbol)
238+
static void remove_vector(symbolt &symbol)
159239
{
160240
remove_vector(symbol.value);
161241
remove_vector(symbol.type);
@@ -173,7 +253,7 @@ Purpose: removes vector data type
173253
174254
\*******************************************************************/
175255

176-
void remove_vector(symbol_tablet &symbol_table)
256+
static void remove_vector(symbol_tablet &symbol_table)
177257
{
178258
Forall_symbols(it, symbol_table.symbols)
179259
remove_vector(it->second);
@@ -214,7 +294,7 @@ Purpose: removes vector data type
214294
215295
\*******************************************************************/
216296

217-
void remove_vector(goto_functionst &goto_functions)
297+
static void remove_vector(goto_functionst &goto_functions)
218298
{
219299
Forall_goto_functions(it, goto_functions)
220300
remove_vector(it->second);

0 commit comments

Comments
 (0)