Skip to content

Commit 5167ef5

Browse files
martin-csmartin-cs
authored
Merge pull request #5640 from jezhiggins/immutable-abstract-objectt
abstract_objectt interface
2 parents cf788d7 + 168bf86 commit 5167ef5

30 files changed

+139
-154
lines changed

‎src/analyses/variable-sensitivity/abstract_object.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ abstract_object_pointert abstract_objectt::abstract_object_merge(
6868
return this->abstract_object_merge_internal(other);
6969

7070
internal_abstract_object_pointert merged = mutable_clone();
71-
merged->make_top();
71+
merged->set_top();
7272
merged->bottom = false;
7373
return merged->abstract_object_merge_internal(other);
7474
}
@@ -147,9 +147,9 @@ abstract_object_pointert abstract_objectt::read(
147147
abstract_object_pointert abstract_objectt::write(
148148
abstract_environmentt &environment,
149149
const namespacet &ns,
150-
const std::stack<exprt> stack,
150+
const std::stack<exprt> &stack,
151151
const exprt &specifier,
152-
const abstract_object_pointert value,
152+
const abstract_object_pointert &value,
153153
bool merging_write) const
154154
{
155155
return environment.abstract_object_factory(type(), ns, true);

‎src/analyses/variable-sensitivity/abstract_object.h

Lines changed: 11 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
121121
/// Get the real type of the variable this abstract object is representing.
122122
///
123123
/// \return The program type this abstract object represents
124-
const typet &type() const;
124+
virtual const typet &type() const;
125125

126126
/// Find out if the abstract object is top
127127
///
@@ -213,9 +213,9 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
213213
virtual abstract_object_pointert write(
214214
abstract_environmentt &environment,
215215
const namespacet &ns,
216-
const std::stack<exprt> stack,
216+
const std::stack<exprt> &stack,
217217
const exprt &specifier,
218-
const abstract_object_pointert value,
218+
const abstract_object_pointert &value,
219219
bool merging_write) const;
220220

221221
/// Print the value of the abstract object
@@ -244,11 +244,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
244244
static void
245245
dump_map_diff(std::ostream out, const shared_mapt &m1, const shared_mapt &m2);
246246

247-
abstract_object_pointert clone() const
248-
{
249-
return abstract_object_pointert(mutable_clone());
250-
}
251-
252247
/**
253248
* Determine whether 'this' abstract_object has been modified in comparison
254249
* to a previous 'before' state.
@@ -323,7 +318,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
323318
return shared_from_this();
324319

325320
internal_abstract_object_pointert clone = mutable_clone();
326-
clone->make_top();
321+
clone->set_top();
327322
return clone;
328323
}
329324

@@ -333,7 +328,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
333328
return shared_from_this();
334329

335330
internal_abstract_object_pointert clone = mutable_clone();
336-
clone->clear_top();
331+
clone->set_not_top();
337332
return clone;
338333
}
339334

@@ -384,10 +379,10 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
384379

385380
// Hooks to allow a sub-class to perform its own operations on
386381
// setting/clearing top
387-
virtual void make_top_internal()
382+
virtual void set_top_internal()
388383
{
389384
}
390-
virtual void clear_top_internal()
385+
virtual void set_not_top_internal()
391386
{
392387
}
393388

@@ -478,15 +473,15 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
478473
sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map);
479474

480475
// The one exception is merge in descendant classes, which needs this
481-
void make_top()
476+
void set_top()
482477
{
483478
top = true;
484-
this->make_top_internal();
479+
this->set_top_internal();
485480
}
486-
void clear_top()
481+
void set_not_top()
487482
{
488483
top = false;
489-
this->clear_top_internal();
484+
this->set_not_top_internal();
490485
}
491486
};
492487

‎src/analyses/variable-sensitivity/array_abstract_object.cpp

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -46,9 +46,9 @@ abstract_object_pointert array_abstract_objectt::read(
4646
abstract_object_pointert array_abstract_objectt::write(
4747
abstract_environmentt &environment,
4848
const namespacet &ns,
49-
const std::stack<exprt> stack,
49+
const std::stack<exprt> &stack,
5050
const exprt &specifier,
51-
const abstract_object_pointert value,
51+
const abstract_object_pointert &value,
5252
bool merging_write) const
5353
{
5454
return this->write_index(
@@ -68,12 +68,12 @@ abstract_object_pointert array_abstract_objectt::read_index(
6868
return env.abstract_object_factory(subtype, ns, !is_bottom(), is_bottom());
6969
}
7070

71-
sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
71+
abstract_object_pointert array_abstract_objectt::write_index(
7272
abstract_environmentt &environment,
7373
const namespacet &ns,
74-
const std::stack<exprt> stack,
74+
const std::stack<exprt> &stack,
7575
const index_exprt &index_expr,
76-
const abstract_object_pointert value,
76+
const abstract_object_pointert &value,
7777
bool merging_write) const
7878
{
7979
// TODO(tkiley): Should this in fact havoc since we can't verify
@@ -82,12 +82,11 @@ sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
8282
// havoc and the default should derive from this.
8383
if(is_top() || is_bottom())
8484
{
85-
return std::dynamic_pointer_cast<const array_abstract_objectt>(clone());
85+
return shared_from_this();
8686
}
8787
else
8888
{
89-
return sharing_ptrt<array_abstract_objectt>(
90-
new array_abstract_objectt(type(), true, false));
89+
return std::make_shared<array_abstract_objectt>(type(), true, false);
9190
}
9291
}
9392

‎src/analyses/variable-sensitivity/array_abstract_object.h

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -78,9 +78,9 @@ class array_abstract_objectt : public abstract_objectt
7878
abstract_object_pointert write(
7979
abstract_environmentt &environment,
8080
const namespacet &ns,
81-
const std::stack<exprt> stack,
81+
const std::stack<exprt> &stack,
8282
const exprt &specifier,
83-
const abstract_object_pointert value,
83+
const abstract_object_pointert &value,
8484
bool merging_write) const override;
8585

8686
void get_statistics(
@@ -117,15 +117,15 @@ class array_abstract_objectt : public abstract_objectt
117117
/// \param value: the value we are trying to assign to that value in the array
118118
/// \param merging_write: ?
119119
///
120-
/// \return The array_abstract_objectt representing the result of writing
120+
/// \return The abstract_object_pointert representing the result of writing
121121
/// to a specific component. In this case this will always be top
122122
/// as we are not tracking the value in the array.
123-
virtual sharing_ptrt<array_abstract_objectt> write_index(
123+
virtual abstract_object_pointert write_index(
124124
abstract_environmentt &environment,
125125
const namespacet &ns,
126-
const std::stack<exprt> stack,
126+
const std::stack<exprt> &stack,
127127
const index_exprt &index_expr,
128-
const abstract_object_pointert value,
128+
const abstract_object_pointert &value,
129129
bool merging_write) const;
130130
};
131131

‎src/analyses/variable-sensitivity/constant_array_abstract_object.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ constant_array_abstract_objectt::constant_array_abstract_objectt(
4343
map.insert(mp_integer(index), environment.eval(entry, ns));
4444
++index;
4545
}
46-
clear_top();
46+
set_not_top();
4747
}
4848
DATA_INVARIANT(verify(), "Structural invariants maintained");
4949
}
@@ -56,7 +56,7 @@ bool constant_array_abstract_objectt::verify() const
5656
(is_top() || is_bottom()) == map.empty();
5757
}
5858

59-
void constant_array_abstract_objectt::make_top_internal()
59+
void constant_array_abstract_objectt::set_top_internal()
6060
{
6161
// A structural invariant of constant_array_abstract_objectt is that
6262
// (is_top() || is_bottom()) => map.empty()
@@ -189,13 +189,12 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
189189
}
190190
}
191191

192-
sharing_ptrt<array_abstract_objectt>
193-
constant_array_abstract_objectt::write_index(
192+
abstract_object_pointert constant_array_abstract_objectt::write_index(
194193
abstract_environmentt &environment,
195194
const namespacet &ns,
196-
const std::stack<exprt> stack,
195+
const std::stack<exprt> &stack,
197196
const index_exprt &index_expr,
198-
const abstract_object_pointert value,
197+
const abstract_object_pointert &value,
199198
bool merging_write) const
200199
{
201200
if(is_bottom())
@@ -231,7 +230,7 @@ constant_array_abstract_objectt::write_index(
231230
old_value.value(), value, stack, ns, merging_write));
232231
}
233232

234-
result->clear_top();
233+
result->set_not_top();
235234
DATA_INVARIANT(result->verify(), "Structural invariants maintained");
236235
return result;
237236
}
@@ -248,7 +247,7 @@ constant_array_abstract_objectt::write_index(
248247
starting_value.first,
249248
environment.write(starting_value.second, value, stack, ns, true));
250249

251-
result->clear_top();
250+
result->set_not_top();
252251
}
253252

254253
DATA_INVARIANT(result->verify(), "Structural invariants maintained");
@@ -303,7 +302,7 @@ constant_array_abstract_objectt::write_index(
303302
{
304303
result->map.insert(index_value, value);
305304
}
306-
result->clear_top();
305+
result->set_not_top();
307306
DATA_INVARIANT(result->verify(), "Structural invariants maintained");
308307
return result;
309308
}

‎src/analyses/variable-sensitivity/constant_array_abstract_object.h

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -110,14 +110,14 @@ class constant_array_abstract_objectt : public array_abstract_objectt
110110
/// \param value: the value we are trying to assign to that value in the array
111111
/// \param merging_write: Should this and all future writes be merged with the
112112
/// current value
113-
/// \return The array_abstract_objectt representing the result of writing
113+
/// \return The abstract_object_pointert representing the result of writing
114114
/// to a specific index.
115-
sharing_ptrt<array_abstract_objectt> write_index(
115+
abstract_object_pointert write_index(
116116
abstract_environmentt &environment,
117117
const namespacet &ns,
118-
const std::stack<exprt> stack,
118+
const std::stack<exprt> &stack,
119119
const index_exprt &index_expr,
120-
const abstract_object_pointert value,
120+
const abstract_object_pointert &value,
121121
bool merging_write) const override;
122122

123123
/// Tries to do an array/array merge if merging with a constant array
@@ -138,7 +138,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
138138

139139
/// \brief Perform any additional structural modifications when setting this
140140
/// object to TOP
141-
void make_top_internal() override;
141+
void set_top_internal() override;
142142

143143
/// Evaluates the index and tries to convert it to a constant integer
144144
///

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,11 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
4646
PRECONDITION(expr.type().id() == ID_pointer);
4747
if(value_stack.is_top_value())
4848
{
49-
make_top();
49+
set_top();
5050
}
5151
else
5252
{
53-
clear_top();
53+
set_not_top();
5454
}
5555
}
5656

@@ -169,12 +169,11 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
169169
}
170170
}
171171

172-
sharing_ptrt<pointer_abstract_objectt>
173-
constant_pointer_abstract_objectt::write_dereference(
172+
abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
174173
abstract_environmentt &environment,
175174
const namespacet &ns,
176-
const std::stack<exprt> stack,
177-
const abstract_object_pointert new_value,
175+
const std::stack<exprt> &stack,
176+
const abstract_object_pointert &new_value,
178177
bool merging_write) const
179178
{
180179
if(is_top() || is_bottom() || value_stack.is_top_value())

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -99,11 +99,11 @@ class constant_pointer_abstract_objectt : public pointer_abstract_objectt
9999
///
100100
/// \return A modified abstract object representing this pointer after it
101101
/// has been written to.
102-
sharing_ptrt<pointer_abstract_objectt> write_dereference(
102+
abstract_object_pointert write_dereference(
103103
abstract_environmentt &environment,
104104
const namespacet &ns,
105-
const std::stack<exprt> stack,
106-
const abstract_object_pointert value,
105+
const std::stack<exprt> &stack,
106+
const abstract_object_pointert &value,
107107
bool merging_write) const override;
108108

109109
void get_statistics(

‎src/analyses/variable-sensitivity/context_abstract_object.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,13 +18,13 @@ void context_abstract_objectt::set_child(const abstract_object_pointert &child)
1818
child_abstract_object = child;
1919
}
2020

21-
void context_abstract_objectt::make_top_internal()
21+
void context_abstract_objectt::set_top_internal()
2222
{
2323
if(!child_abstract_object->is_top())
2424
set_child(child_abstract_object->make_top());
2525
}
2626

27-
void context_abstract_objectt::clear_top_internal()
27+
void context_abstract_objectt::set_not_top_internal()
2828
{
2929
if(child_abstract_object->is_top())
3030
set_child(child_abstract_object->clear_top());
@@ -71,9 +71,9 @@ abstract_object_pointert context_abstract_objectt::read(
7171
abstract_object_pointert context_abstract_objectt::write(
7272
abstract_environmentt &environment,
7373
const namespacet &ns,
74-
const std::stack<exprt> stack,
74+
const std::stack<exprt> &stack,
7575
const exprt &specifier,
76-
const abstract_object_pointert value,
76+
const abstract_object_pointert &value,
7777
bool merging_write) const
7878
{
7979
abstract_object_pointert updated_child = child_abstract_object->write(

‎src/analyses/variable-sensitivity/context_abstract_object.h

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ class context_abstract_objectt : public abstract_objectt
5555
{
5656
}
5757

58-
virtual const typet &type() const
58+
const typet &type() const override
5959
{
6060
return child_abstract_object->type();
6161
}
@@ -104,8 +104,8 @@ class context_abstract_objectt : public abstract_objectt
104104

105105
// These are internal hooks that allow sub-classes to perform additional
106106
// actions when an abstract_object is set/unset to TOP
107-
void make_top_internal() override;
108-
void clear_top_internal() override;
107+
void set_top_internal() override;
108+
void set_not_top_internal() override;
109109

110110
abstract_object_pointert read(
111111
const abstract_environmentt &env,
@@ -115,9 +115,9 @@ class context_abstract_objectt : public abstract_objectt
115115
abstract_object_pointert write(
116116
abstract_environmentt &environment,
117117
const namespacet &ns,
118-
const std::stack<exprt> stack,
118+
const std::stack<exprt> &stack,
119119
const exprt &specifier,
120-
const abstract_object_pointert value,
120+
const abstract_object_pointert &value,
121121
bool merging_write) const override;
122122

123123
bool has_been_modified(const abstract_object_pointert before) const override;

‎src/analyses/variable-sensitivity/data_dependency_context.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -186,9 +186,9 @@ data_dependency_contextt::set_data_deps(const dependencest &dependencies) const
186186
abstract_object_pointert data_dependency_contextt::write(
187187
abstract_environmentt &environment,
188188
const namespacet &ns,
189-
const std::stack<exprt> stack,
189+
const std::stack<exprt> &stack,
190190
const exprt &specifier,
191-
const abstract_object_pointert value,
191+
const abstract_object_pointert &value,
192192
bool merging_write) const
193193
{
194194
const auto updated_parent =

‎src/analyses/variable-sensitivity/data_dependency_context.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,9 +50,9 @@ class data_dependency_contextt : public write_location_contextt
5050
abstract_object_pointert write(
5151
abstract_environmentt &environment,
5252
const namespacet &ns,
53-
const std::stack<exprt> stack,
53+
const std::stack<exprt> &stack,
5454
const exprt &specifier,
55-
const abstract_object_pointert value,
55+
const abstract_object_pointert &value,
5656
bool merging_write) const override;
5757

5858
abstract_object_pointert update_location_context(

0 commit comments

Comments
 (0)