Skip to content

Commit f9ca353

Browse files
author
martin
committed
Add is_bottom() and is_top() to ai_domain_baset and derived domains.
1 parent 88d8673 commit f9ca353

11 files changed

+218
-60
lines changed

‎src/analyses/ai.h

+4
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,10 @@ class ai_domain_baset
8080
// a reasonable entry-point state
8181
virtual void make_entry()=0;
8282

83+
virtual bool is_bottom() const=0;
84+
85+
virtual bool is_top() const=0;
86+
8387
// also add
8488
//
8589
// bool merge(const T &b, locationt from, locationt to);

‎src/analyses/constant_propagator.h

+29-9
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
2525
locationt from,
2626
locationt to,
2727
ai_baset &ai_base,
28-
const namespacet &ns) override;
28+
const namespacet &ns) final override;
2929

3030
virtual void output(
3131
std::ostream &out,
@@ -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() override
44+
virtual void make_bottom() final override
4545
{
4646
values.set_to_bottom();
4747
}
4848

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

54-
virtual void make_entry() override
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
}

‎src/analyses/custom_bitvector_analysis.h

+21-5
Original file line numberDiff line numberDiff line change
@@ -27,32 +27,48 @@ 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+
DATA_INVARIANT(!has_values.is_false() ||
59+
(may_bits.empty() && must_bits.empty()),
60+
"If the domain is bottom, it must have no bits set");
61+
return has_values.is_false();
62+
}
63+
64+
bool is_top() const final override
65+
{
66+
DATA_INVARIANT(!has_values.is_true() ||
67+
(may_bits.empty() && must_bits.empty()),
68+
"If the domain is top, it must have no bits set");
69+
return has_values.is_true();
70+
}
71+
5672
bool merge(
5773
const custom_bitvector_domaint &b,
5874
locationt from,

‎src/analyses/dependence_graph.h

+32-6
Original file line numberDiff line numberDiff line change
@@ -83,40 +83,66 @@ 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,
9595
const namespacet &ns) const override;
9696

9797
void make_top() final override
9898
{
99-
assert(node_id!=std::numeric_limits<node_indext>::max());
99+
DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
100+
"node_id must not be valid");
100101

101102
has_values=tvt(true);
102103
control_deps.clear();
103104
data_deps.clear();
104105
}
105106

106-
void make_bottom() final
107+
void make_bottom() final override
107108
{
108-
assert(node_id!=std::numeric_limits<node_indext>::max());
109+
DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
110+
"node_id must be valid");
109111

110112
has_values=tvt(false);
111113
control_deps.clear();
112114
data_deps.clear();
113115
}
114116

115-
void make_entry() final
117+
void make_entry() final override
116118
{
117119
make_top();
118120
}
119121

122+
bool is_top() const final override
123+
{
124+
DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
125+
"node_id must be valid");
126+
127+
DATA_INVARIANT(!has_values.is_true() ||
128+
(control_deps.empty() && data_deps.empty()),
129+
"If the domain is top, it must have no dependencies");
130+
131+
return has_values.is_true();
132+
}
133+
134+
bool is_bottom() const final override
135+
{
136+
DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
137+
"node_id must be valid");
138+
139+
DATA_INVARIANT(!has_values.is_false() ||
140+
(control_deps.empty() && data_deps.empty()),
141+
"If the domain is bottom, it must have no dependencies");
142+
143+
return has_values.is_false();
144+
}
145+
120146
void set_node_id(node_indext id)
121147
{
122148
node_id=id;

‎src/analyses/escape_analysis.h

+21-5
Original file line numberDiff line numberDiff line change
@@ -32,33 +32,49 @@ 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+
DATA_INVARIANT(!has_values.is_false() ||
64+
(cleanup_map.empty() && (aliases.size()==0)),
65+
"If the domain is bottom, all maps must be empty");
66+
return has_values.is_false();
67+
}
68+
69+
bool is_top() const override final
70+
{
71+
DATA_INVARIANT(!has_values.is_true() ||
72+
(cleanup_map.empty() && (aliases.size()==0)),
73+
"If the domain is top, all maps must be empty");
74+
return has_values.is_true();
75+
}
76+
77+
void make_entry() override final
6278
{
6379
make_top();
6480
}

‎src/analyses/global_may_alias.h

+19-5
Original file line numberDiff line numberDiff line change
@@ -32,35 +32,49 @@ 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+
DATA_INVARIANT(!has_values.is_false() || (aliases.size()==0),
67+
"If the domain is bottom, there must be no aliases");
68+
return has_values.is_false();
69+
}
70+
71+
bool is_top() const final override
72+
{
73+
DATA_INVARIANT(!has_values.is_true() || (aliases.size()==0),
74+
"If the domain is top, there must be no aliases");
75+
return has_values.is_true();
76+
}
77+
6478
typedef union_find<irep_idt> aliasest;
6579
aliasest aliases;
6680

0 commit comments

Comments
 (0)