Skip to content

Commit 3178f1b

Browse files
author
martin
committed
Add is_bottom() and is_top() to ai_domain_baset and derived domains.
1 parent e2fdcbf commit 3178f1b

11 files changed

+192
-63
lines changed

‎src/analyses/ai.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,10 @@ class ai_domain_baset
7878
// a reasonable entry-point state
7979
virtual void make_entry()=0;
8080

81+
virtual bool is_bottom() const=0;
82+
83+
virtual bool is_top() const=0;
84+
8185
// also add
8286
//
8387
// bool merge(const T &b, locationt from, locationt to);

‎src/analyses/constant_propagator.h

Lines changed: 30 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,12 @@ class constant_propagator_domaint:public ai_domain_baset
2525
locationt from,
2626
locationt to,
2727
ai_baset &ai_base,
28-
const namespacet &ns);
28+
const namespacet &ns) final override;
2929

3030
virtual void output(
3131
std::ostream &out,
3232
const ai_baset &ai_base,
33-
const namespacet &ns) const;
33+
const namespacet &ns) const override;
3434

3535
bool merge(
3636
const constant_propagator_domaint &other,
@@ -39,23 +39,33 @@ class constant_propagator_domaint:public ai_domain_baset
3939

4040
virtual bool ai_simplify(
4141
exprt &condition,
42-
const namespacet &ns) const override;
42+
const namespacet &ns) const final override;
4343

44-
virtual void make_bottom()
44+
virtual void make_bottom() final override
4545
{
4646
values.set_to_bottom();
4747
}
4848

49-
virtual void make_top()
49+
virtual void make_top() final override
5050
{
5151
values.set_to_top();
5252
}
5353

54-
virtual void make_entry()
54+
virtual void make_entry() final override
5555
{
5656
make_top();
5757
}
5858

59+
virtual bool is_bottom() const final override
60+
{
61+
return values.is_bot();
62+
}
63+
64+
virtual bool is_top() const final override
65+
{
66+
return values.is_top();
67+
}
68+
5969
struct valuest
6070
{
6171
public:
@@ -70,27 +80,37 @@ class constant_propagator_domaint:public ai_domain_baset
7080

7181
// set whole state
7282

73-
inline void set_to_bottom()
83+
void set_to_bottom()
7484
{
7585
replace_const.clear();
7686
is_bottom=true;
7787
}
7888

79-
inline void set_to_top()
89+
void set_to_top()
8090
{
8191
replace_const.clear();
8292
is_bottom=false;
8393
}
8494

95+
bool is_bot() const
96+
{
97+
return is_bottom && replace_const.empty();
98+
}
99+
100+
bool is_top() const
101+
{
102+
return !is_bottom && replace_const.empty();
103+
}
104+
85105
// set single identifier
86106

87-
inline void set_to(const irep_idt &lhs, const exprt &rhs)
107+
void set_to(const irep_idt &lhs, const exprt &rhs)
88108
{
89109
replace_const.expr_map[lhs]=rhs;
90110
is_bottom=false;
91111
}
92112

93-
inline void set_to(const symbol_exprt &lhs, const exprt &rhs)
113+
void set_to(const symbol_exprt &lhs, const exprt &rhs)
94114
{
95115
set_to(lhs.get_identifier(), rhs);
96116
}
@@ -142,8 +162,6 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
142162
goto_functionst &goto_functions,
143163
const namespacet &ns):dirty(goto_functions)
144164
{
145-
assert(false);
146-
147165
operator()(goto_functions, ns);
148166
replace(goto_functions, ns);
149167
}
@@ -152,8 +170,6 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
152170
goto_functionst::goto_functiont &goto_function,
153171
const namespacet &ns):dirty(goto_function)
154172
{
155-
assert(false);
156-
157173
operator()(goto_function, ns);
158174
replace(goto_function, ns);
159175
}

‎src/analyses/custom_bitvector_analysis.h

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,32 +27,44 @@ class custom_bitvector_domaint:public ai_domain_baset
2727
locationt from,
2828
locationt to,
2929
ai_baset &ai,
30-
const namespacet &ns) final;
30+
const namespacet &ns) final override;
3131

3232
void output(
3333
std::ostream &out,
3434
const ai_baset &ai,
35-
const namespacet &ns) const final;
35+
const namespacet &ns) const final override;
3636

37-
void make_bottom() final
37+
void make_bottom() final override
3838
{
3939
may_bits.clear();
4040
must_bits.clear();
4141
has_values=tvt(false);
4242
}
4343

44-
void make_top() final
44+
void make_top() final override
4545
{
4646
may_bits.clear();
4747
must_bits.clear();
4848
has_values=tvt(true);
4949
}
5050

51-
void make_entry() final
51+
void make_entry() final override
5252
{
5353
make_top();
5454
}
5555

56+
bool is_bottom() const final override
57+
{
58+
assert(!has_values.is_false() || (may_bits.empty() && must_bits.empty()));
59+
return has_values.is_false();
60+
}
61+
62+
bool is_top() const final override
63+
{
64+
assert(!has_values.is_true() || (may_bits.empty() && must_bits.empty()));
65+
return has_values.is_true();
66+
}
67+
5668
bool merge(
5769
const custom_bitvector_domaint &b,
5870
locationt from,

‎src/analyses/dependence_graph.h

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,12 +83,12 @@ class dep_graph_domaint:public ai_domain_baset
8383
goto_programt::const_targett from,
8484
goto_programt::const_targett to,
8585
ai_baset &ai,
86-
const namespacet &ns) final;
86+
const namespacet &ns) final override;
8787

8888
void output(
8989
std::ostream &out,
9090
const ai_baset &ai,
91-
const namespacet &ns) const final;
91+
const namespacet &ns) const final override;
9292

9393
jsont output_json(
9494
const ai_baset &ai,
@@ -103,7 +103,7 @@ class dep_graph_domaint:public ai_domain_baset
103103
data_deps.clear();
104104
}
105105

106-
void make_bottom() final
106+
void make_bottom() final override
107107
{
108108
assert(node_id!=std::numeric_limits<node_indext>::max());
109109

@@ -112,11 +112,31 @@ class dep_graph_domaint:public ai_domain_baset
112112
data_deps.clear();
113113
}
114114

115-
void make_entry() final
115+
void make_entry() final override
116116
{
117117
make_top();
118118
}
119119

120+
bool is_top() const final override
121+
{
122+
assert(node_id!=std::numeric_limits<node_indext>::max());
123+
124+
assert(!has_values.is_true() ||
125+
(control_deps.empty() && data_deps.empty()));
126+
127+
return has_values.is_true();
128+
}
129+
130+
bool is_bottom() const final override
131+
{
132+
assert(node_id!=std::numeric_limits<node_indext>::max());
133+
134+
assert(!has_values.is_false() ||
135+
(control_deps.empty() && data_deps.empty()));
136+
137+
return has_values.is_false();
138+
}
139+
120140
void set_node_id(node_indext id)
121141
{
122142
node_id=id;

‎src/analyses/escape_analysis.h

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -32,33 +32,45 @@ class escape_domaint:public ai_domain_baset
3232
locationt from,
3333
locationt to,
3434
ai_baset &ai,
35-
const namespacet &ns) final;
35+
const namespacet &ns) final override;
3636

3737
void output(
3838
std::ostream &out,
3939
const ai_baset &ai,
40-
const namespacet &ns) const final;
40+
const namespacet &ns) const final override;
4141

4242
bool merge(
4343
const escape_domaint &b,
4444
locationt from,
4545
locationt to);
4646

47-
void make_bottom() final
47+
void make_bottom() final override
4848
{
4949
cleanup_map.clear();
5050
aliases.clear();
5151
has_values=tvt(false);
5252
}
5353

54-
void make_top() final
54+
void make_top() final override
5555
{
5656
cleanup_map.clear();
5757
aliases.clear();
5858
has_values=tvt(true);
5959
}
6060

61-
void make_entry() final
61+
bool is_bottom() const override final
62+
{
63+
assert(!has_values.is_false() || (cleanup_map.empty() && aliases.empty()));
64+
return has_values.is_false();
65+
}
66+
67+
bool is_top() const override final
68+
{
69+
assert(!has_values.is_true() || (cleanup_map.empty() && aliases.empty()));
70+
return has_values.is_true();
71+
}
72+
73+
void make_entry() override final
6274
{
6375
make_top();
6476
}

‎src/analyses/global_may_alias.h

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -32,35 +32,47 @@ class global_may_alias_domaint:public ai_domain_baset
3232
locationt from,
3333
locationt to,
3434
ai_baset &ai,
35-
const namespacet &ns) final;
35+
const namespacet &ns) final override;
3636

3737
void output(
3838
std::ostream &out,
3939
const ai_baset &ai,
40-
const namespacet &ns) const final;
40+
const namespacet &ns) const final override;
4141

4242
bool merge(
4343
const global_may_alias_domaint &b,
4444
locationt from,
4545
locationt to);
4646

47-
void make_bottom() final
47+
void make_bottom() final override
4848
{
4949
aliases.clear();
5050
has_values=tvt(false);
5151
}
5252

53-
void make_top() final
53+
void make_top() final override
5454
{
5555
aliases.clear();
5656
has_values=tvt(true);
5757
}
5858

59-
void make_entry() final
59+
void make_entry() final override
6060
{
6161
make_top();
6262
}
6363

64+
bool is_bottom() const final override
65+
{
66+
assert(!has_values.is_false() || aliases.empty());
67+
return has_values.is_false();
68+
}
69+
70+
bool is_top() const final override
71+
{
72+
assert(!has_values.is_true() || aliases.empty());
73+
return has_values.is_true();
74+
}
75+
6476
typedef union_find<irep_idt> aliasest;
6577
aliasest aliases;
6678

0 commit comments

Comments
 (0)