Skip to content

Commit 913fbd9

Browse files
smowtonsmowton
committed
Templatize and virtualize value-set analysis
This templates value-set-analysis, so that it can be subclassed providing a value-set extension, and virtualizes value-set so it can similarly be extended.
1 parent 1a314e3 commit 913fbd9

File tree

7 files changed

+125
-192
lines changed

7 files changed

+125
-192
lines changed

‎src/pointer-analysis/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
SRC = value_set.cpp goto_program_dereference.cpp value_set_analysis.cpp \
22
dereference.cpp pointer_offset_sum.cpp add_failed_symbols.cpp \
3-
show_value_sets.cpp value_set_domain.cpp rewrite_index.cpp \
3+
show_value_sets.cpp rewrite_index.cpp \
44
value_set_analysis_fi.cpp value_set_fi.cpp value_set_domain_fi.cpp \
55
value_set_analysis_fivr.cpp value_set_fivr.cpp value_set_domain_fivr.cpp \
66
value_set_analysis_fivrns.cpp value_set_fivrns.cpp \

‎src/pointer-analysis/show_value_sets.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
1111

1212
#include <util/ui_message.h>
13+
#include "value_set_analysis.h"
1314

1415
class goto_functionst;
1516
class goto_programt;
16-
class value_set_analysist;
1717

1818
void show_value_sets(
1919
ui_message_handlert::uit ui,

‎src/pointer-analysis/value_set.h

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -174,11 +174,11 @@ class value_sett
174174
const exprt &expr,
175175
const namespacet &ns);
176176

177-
void apply_code(
177+
virtual void apply_code(
178178
const codet &code,
179179
const namespacet &ns);
180180

181-
void assign(
181+
virtual void assign(
182182
const exprt &lhs,
183183
const exprt &rhs,
184184
const namespacet &ns,
@@ -205,37 +205,37 @@ class value_sett
205205
const namespacet &ns) const;
206206

207207
protected:
208-
void get_value_set_rec(
208+
virtual void get_value_set_rec(
209209
const exprt &expr,
210210
object_mapt &dest,
211211
const std::string &suffix,
212212
const typet &original_type,
213213
const namespacet &ns) const;
214214

215-
void get_value_set(
215+
virtual void get_value_set(
216216
const exprt &expr,
217217
object_mapt &dest,
218218
const namespacet &ns,
219219
bool is_simplified) const;
220220

221-
void get_reference_set(
221+
virtual void get_reference_set(
222222
const exprt &expr,
223223
object_mapt &dest,
224224
const namespacet &ns) const
225225
{
226226
get_reference_set_rec(expr, dest, ns);
227227
}
228228

229-
void get_reference_set_rec(
229+
virtual void get_reference_set_rec(
230230
const exprt &expr,
231231
object_mapt &dest,
232232
const namespacet &ns) const;
233233

234-
void dereference_rec(
234+
virtual void dereference_rec(
235235
const exprt &src,
236236
exprt &dest) const;
237237

238-
void assign_rec(
238+
virtual void assign_rec(
239239
const exprt &lhs,
240240
const object_mapt &values_rhs,
241241
const std::string &suffix,

‎src/pointer-analysis/value_set_analysis.cpp

Lines changed: 0 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -8,114 +8,13 @@ Author: Daniel Kroening, [email protected]
88

99
#include <util/prefix.h>
1010
#include <util/cprover_prefix.h>
11-
#include <util/xml_expr.h>
12-
#include <util/xml.h>
1311

1412
#include <langapi/language_util.h>
1513

1614
#include "value_set_analysis.h"
1715

1816
/*******************************************************************\
1917
20-
Function: value_set_analysist::initialize
21-
22-
Inputs:
23-
24-
Outputs:
25-
26-
Purpose:
27-
28-
\*******************************************************************/
29-
30-
void value_set_analysist::initialize(
31-
const goto_programt &goto_program)
32-
{
33-
baset::initialize(goto_program);
34-
}
35-
36-
/*******************************************************************\
37-
38-
Function: value_set_analysist::initialize
39-
40-
Inputs:
41-
42-
Outputs:
43-
44-
Purpose:
45-
46-
\*******************************************************************/
47-
48-
void value_set_analysist::initialize(
49-
const goto_functionst &goto_functions)
50-
{
51-
baset::initialize(goto_functions);
52-
}
53-
54-
/*******************************************************************\
55-
56-
Function: value_set_analysist::convert
57-
58-
Inputs:
59-
60-
Outputs:
61-
62-
Purpose:
63-
64-
\*******************************************************************/
65-
66-
void value_set_analysist::convert(
67-
const goto_programt &goto_program,
68-
const irep_idt &identifier,
69-
xmlt &dest) const
70-
{
71-
source_locationt previous_location;
72-
73-
forall_goto_program_instructions(i_it, goto_program)
74-
{
75-
const source_locationt &location=i_it->source_location;
76-
77-
if(location==previous_location)
78-
continue;
79-
80-
if(location.is_nil() || location.get_file()==irep_idt())
81-
continue;
82-
83-
// find value set
84-
const value_sett &value_set=(*this)[i_it].value_set;
85-
86-
xmlt &i=dest.new_element("instruction");
87-
i.new_element()=::xml(location);
88-
89-
for(value_sett::valuest::const_iterator
90-
v_it=value_set.values.begin();
91-
v_it!=value_set.values.end();
92-
v_it++)
93-
{
94-
xmlt &var=i.new_element("variable");
95-
var.new_element("identifier").data=
96-
id2string(v_it->first);
97-
98-
#if 0
99-
const value_sett::expr_sett &expr_set=
100-
v_it->second.expr_set();
101-
102-
for(value_sett::expr_sett::const_iterator
103-
e_it=expr_set.begin();
104-
e_it!=expr_set.end();
105-
e_it++)
106-
{
107-
std::string value_str=
108-
from_expr(ns, identifier, *e_it);
109-
110-
var.new_element("value").data=
111-
xmlt::escape(value_str);
112-
}
113-
#endif
114-
}
115-
}
116-
}
117-
/*******************************************************************\
118-
11918
Function: convert
12019
12120
Inputs:

‎src/pointer-analysis/value_set_analysis.h

Lines changed: 70 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -11,32 +11,90 @@ Author: Daniel Kroening, [email protected]
1111

1212
#define USE_DEPRECATED_STATIC_ANALYSIS_H
1313
#include <analyses/static_analysis.h>
14+
#include <util/xml_expr.h>
15+
#include <util/xml.h>
1416

1517
#include "value_set_domain.h"
1618
#include "value_sets.h"
19+
#include "value_set.h"
1720

1821
class xmlt;
1922

20-
class value_set_analysist:
23+
template<class Value_Sett>
24+
class value_set_analysis_baset:
2125
public value_setst,
22-
public static_analysist<value_set_domaint>
26+
public static_analysist<value_set_domaint<Value_Sett> >
2327
{
2428
public:
25-
explicit value_set_analysist(const namespacet &_ns):
26-
static_analysist<value_set_domaint>(_ns)
29+
typedef value_set_domaint<Value_Sett> domaint;
30+
typedef static_analysist<domaint> baset;
31+
typedef typename baset::locationt locationt;
32+
33+
explicit value_set_analysis_baset(const namespacet &_ns):baset(_ns)
2734
{
2835
}
2936

30-
typedef static_analysist<value_set_domaint> baset;
31-
3237
// overloading
33-
virtual void initialize(const goto_programt &goto_program);
34-
virtual void initialize(const goto_functionst &goto_functions);
38+
void initialize(const goto_programt &goto_program)
39+
{
40+
baset::initialize(goto_program);
41+
}
42+
void initialize(const goto_functionst &goto_functions)
43+
{
44+
baset::initialize(goto_functions);
45+
}
3546

3647
void convert(
3748
const goto_programt &goto_program,
3849
const irep_idt &identifier,
39-
xmlt &dest) const;
50+
xmlt &dest) const
51+
{
52+
source_locationt previous_location;
53+
54+
forall_goto_program_instructions(i_it, goto_program)
55+
{
56+
const source_locationt &location=i_it->source_location;
57+
58+
if(location==previous_location)
59+
continue;
60+
61+
if(location.is_nil() || location.get_file()==irep_idt())
62+
continue;
63+
64+
// find value set
65+
const value_sett &value_set=(*this)[i_it].value_set;
66+
67+
xmlt &i=dest.new_element("instruction");
68+
i.new_element()=::xml(location);
69+
70+
for(value_sett::valuest::const_iterator
71+
v_it=value_set.values.begin();
72+
v_it!=value_set.values.end();
73+
v_it++)
74+
{
75+
xmlt &var=i.new_element("variable");
76+
var.new_element("identifier").data=
77+
id2string(v_it->first);
78+
79+
#if 0
80+
const value_sett::expr_sett &expr_set=
81+
v_it->second.expr_set();
82+
83+
for(value_sett::expr_sett::const_iterator
84+
e_it=expr_set.begin();
85+
e_it!=expr_set.end();
86+
e_it++)
87+
{
88+
std::string value_str=
89+
from_expr(ns, identifier, *e_it);
90+
91+
var.new_element("value").data=
92+
xmlt::escape(value_str);
93+
}
94+
#endif
95+
}
96+
}
97+
}
4098

4199
public:
42100
// interface value_sets
@@ -45,10 +103,12 @@ class value_set_analysist:
45103
const exprt &expr,
46104
value_setst::valuest &dest)
47105
{
48-
(*this)[l].value_set.get_value_set(expr, dest, ns);
106+
(*this)[l].value_set.get_value_set(expr, dest, baset::ns);
49107
}
50108
};
51109

110+
typedef value_set_analysis_baset<value_sett> value_set_analysist;
111+
52112
void convert(
53113
const goto_functionst &goto_functions,
54114
const value_set_analysist &value_set_analysis,

‎src/pointer-analysis/value_set_domain.cpp

Lines changed: 0 additions & 65 deletions
This file was deleted.

0 commit comments

Comments
 (0)