Skip to content

Commit 0968c54

Browse files
jezhigginsjezhiggins
committed
Consolidate write_location_context, eliminate update_location_context
1 parent add7137 commit 0968c54

14 files changed

+62
-71
lines changed

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

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -243,12 +243,6 @@ bool abstract_objectt::should_use_base_meet(
243243

244244
abstract_object_pointert
245245
abstract_objectt::write_location_context(const locationt &location) const
246-
{
247-
return update_location_context({location});
248-
}
249-
250-
abstract_object_pointert
251-
abstract_objectt::update_location_context(const locationst &locations) const
252246
{
253247
return shared_from_this();
254248
}

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

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
218218
const namespacet &ns) const;
219219

220220
typedef goto_programt::const_targett locationt;
221-
typedef std::set<locationt> locationst;
222221
typedef sharing_mapt<irep_idt, abstract_object_pointert, false, irep_id_hash>
223222
shared_mapt;
224223

@@ -289,20 +288,16 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
289288
virtual abstract_object_pointert
290289
meet(const abstract_object_pointert &other) const;
291290

292-
virtual abstract_object_pointert
293-
write_location_context(const locationt &location) const;
294-
295291
/**
296-
* Update the location context for an abstract object, potentially
297-
* propogating the update to any children of this abstract object.
292+
* Update the location context for an abstract object.
298293
*
299-
* \param locations the set of locations to be updated
294+
* \param location the location to be updated
300295
*
301-
* \return a clone of this abstract object with it's location context
296+
* \return a clone of this abstract object with its location context
302297
* updated
303298
*/
304299
virtual abstract_object_pointert
305-
update_location_context(const locationst &locations) const;
300+
write_location_context(const locationt &location) const;
306301

307302
// Const versions must perform copy-on-write
308303
abstract_object_pointert make_top() const

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -105,13 +105,12 @@ abstract_object_pointert context_abstract_objectt::expression_transform(
105105
return envelop(result);
106106
}
107107

108-
abstract_object_pointert context_abstract_objectt::update_location_context(
109-
const abstract_objectt::locationst &locations) const
108+
abstract_object_pointert context_abstract_objectt::write_location_context(
109+
const locationt &location) const
110110
{
111-
auto result = update_location_context_internal(locations);
111+
auto result = update_location_context_internal({location});
112112

113-
abstract_object_pointert visited_child =
114-
child_abstract_object->update_location_context(locations);
113+
auto visited_child = child_abstract_object->write_location_context(location);
115114
result->set_child(visited_child);
116115

117116
return result;

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

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -81,8 +81,16 @@ class context_abstract_objectt : public abstract_objectt
8181
const abstract_environmentt &environment,
8282
const namespacet &ns) const override;
8383

84+
/**
85+
* Update the location context for an abstract object.
86+
*
87+
* \param location the location to be updated
88+
*
89+
* \return a clone of this abstract object with its location context
90+
* updated
91+
*/
8492
abstract_object_pointert
85-
update_location_context(const locationst &locations) const override;
93+
write_location_context(const locationt &location) const override;
8694

8795
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
8896
const override;
@@ -124,8 +132,10 @@ class context_abstract_objectt : public abstract_objectt
124132

125133
exprt to_predicate_internal(const exprt &name) const override;
126134

127-
virtual context_abstract_object_ptrt update_location_context_internal(
128-
const abstract_objectt::locationst &locations) const = 0;
135+
typedef std::set<locationt> locationst;
136+
137+
virtual context_abstract_object_ptrt
138+
update_location_context_internal(const locationst &locations) const = 0;
129139
};
130140

131141
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ bool data_dependency_contextt::has_been_modified(
4242
}
4343

4444
// Check whether the data dependencies have changed as well
45-
abstract_objectt::locationst intersection;
45+
locationst intersection;
4646
std::set_intersection(
4747
data_deps.cbegin(),
4848
data_deps.cend(),
@@ -129,7 +129,7 @@ abstract_object_pointert data_dependency_contextt::insert_data_deps(
129129

130130
context_abstract_objectt::context_abstract_object_ptrt
131131
data_dependency_contextt::update_location_context_internal(
132-
const abstract_objectt::locationst &locations) const
132+
const locationst &locations) const
133133
{
134134
auto result =
135135
std::dynamic_pointer_cast<data_dependency_contextt>(mutable_clone());
@@ -158,7 +158,7 @@ void data_dependency_contextt::set_data_deps(const locationst &locations)
158158
*/
159159
void data_dependency_contextt::set_data_deps(const dependenciest &dependencies)
160160
{
161-
abstract_objectt::locationst intersection;
161+
locationst intersection;
162162
std::set_intersection(
163163
data_deps.cbegin(),
164164
data_deps.cend(),

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -377,10 +377,10 @@ abstract_object_pointert full_array_abstract_objectt::get_top_entry(
377377
return env.abstract_object_factory(type().subtype(), ns, true, false);
378378
}
379379

380-
abstract_object_pointert full_array_abstract_objectt::update_location_context(
381-
const locationst &locations) const
380+
abstract_object_pointert full_array_abstract_objectt::write_location_context(
381+
const locationt &location) const
382382
{
383-
return visit_sub_elements(location_update_visitort(locations));
383+
return visit_sub_elements(location_update_visitort(location));
384384
}
385385

386386
abstract_object_pointert full_array_abstract_objectt::visit_sub_elements(

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -61,16 +61,15 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
6161
const override;
6262

6363
/**
64-
* Update the location context for an abstract object, potentially
65-
* propogating the update to any children of this abstract object.
64+
* Update the location context for an abstract object.
6665
*
67-
* \param locations the set of locations to be updated
66+
* \param location the location to be updated
6867
*
69-
* \return a clone of this abstract object with it's location context
68+
* \return a clone of this abstract object with its location context
7069
* updated
7170
*/
7271
abstract_object_pointert
73-
update_location_context(const locationst &locations) const override;
72+
write_location_context(const locationt &location) const override;
7473

7574
/**
7675
* Apply a visitor operation to all sub elements of this abstract_object.

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -278,10 +278,10 @@ abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs(
278278
}
279279
}
280280

281-
abstract_object_pointert full_struct_abstract_objectt::update_location_context(
282-
const locationst &locations) const
281+
abstract_object_pointert full_struct_abstract_objectt::write_location_context(
282+
const locationt &location) const
283283
{
284-
return visit_sub_elements(location_update_visitort(locations));
284+
return visit_sub_elements(location_update_visitort(location));
285285
}
286286

287287
abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements(

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -67,16 +67,15 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt<
6767
const class namespacet &ns) const override;
6868

6969
/**
70-
* Update the location context for an abstract object, potentially
71-
* propogating the update to any children of this abstract object.
70+
* Update the location context for an abstract object.
7271
*
73-
* \param locations the set of locations to be updated
72+
* \param location the location to be updated
7473
*
75-
* \return a clone of this abstract object with it's location context
74+
* \return a clone of this abstract object with its location context
7675
* updated
7776
*/
7877
abstract_object_pointert
79-
update_location_context(const locationst &locations) const override;
78+
write_location_context(const locationt &location) const override;
8079

8180
/**
8281
* Apply a visitor operation to all sub elements of this abstract_object.

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,20 +15,19 @@ class location_update_visitort
1515
: public abstract_objectt::abstract_object_visitort
1616
{
1717
public:
18-
explicit location_update_visitort(
19-
const abstract_objectt::locationst &locations)
20-
: locations(locations)
18+
explicit location_update_visitort(const abstract_objectt::locationt &location)
19+
: location(location)
2120
{
2221
}
2322

2423
abstract_object_pointert
2524
visit(const abstract_object_pointert &element) const override
2625
{
27-
return element->update_location_context(locations);
26+
return element->write_location_context(location);
2827
}
2928

3029
private:
31-
const abstract_objectt::locationst &locations;
30+
const abstract_objectt::locationt &location;
3231
};
3332

3433
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LOCATION_UPDATE_VISITOR_H

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ void region_contextt::reset_location()
132132

133133
context_abstract_objectt::context_abstract_object_ptrt
134134
region_contextt::update_location_context_internal(
135-
const abstract_objectt::locationst &locations) const
135+
const locationst &locations) const
136136
{
137137
auto result = std::dynamic_pointer_cast<region_contextt>(mutable_clone());
138138
result->set_location(*locations.cbegin());

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,8 +98,8 @@ class region_contextt : public context_abstract_objectt
9898

9999
optionalt<locationt> assign_location;
100100

101-
context_abstract_object_ptrt update_location_context_internal(
102-
const abstract_objectt::locationst &locations) const override;
101+
context_abstract_object_ptrt
102+
update_location_context_internal(const locationst &locations) const override;
103103

104104
void set_location(const locationt &location);
105105
};

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

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

1111
#include <algorithm>
1212

13-
abstract_objectt::locationst
13+
context_abstract_objectt::locationst
1414
write_location_contextt::get_last_written_locations() const
1515
{
1616
return last_written_locations;
@@ -122,8 +122,7 @@ abstract_object_pointert write_location_contextt::combine(
122122
{
123123
auto combined_child = fn(child_abstract_object, other->child_abstract_object);
124124

125-
abstract_objectt::locationst location_union =
126-
get_location_union(other->get_last_written_locations());
125+
auto location_union = get_location_union(other->get_last_written_locations());
127126
// If the union is larger than the initial set, then update.
128127
bool merge_locations =
129128
location_union.size() > get_last_written_locations().size();
@@ -169,7 +168,7 @@ write_location_contextt::abstract_object_merge_internal(
169168

170169
if(other_context)
171170
{
172-
abstract_objectt::locationst location_union =
171+
auto location_union =
173172
get_location_union(other_context->get_last_written_locations());
174173

175174
// If the union is larger than the initial set, then update.
@@ -185,7 +184,7 @@ write_location_contextt::abstract_object_merge_internal(
185184

186185
context_abstract_objectt::context_abstract_object_ptrt
187186
write_location_contextt::update_location_context_internal(
188-
const abstract_objectt::locationst &locations) const
187+
const locationst &locations) const
189188
{
190189
auto result =
191190
std::dynamic_pointer_cast<write_location_contextt>(mutable_clone());
@@ -199,7 +198,7 @@ write_location_contextt::update_location_context_internal(
199198
* \param locations the locations to set
200199
*/
201200
void write_location_contextt::set_last_written_locations(
202-
const abstract_objectt::locationst &locations)
201+
const locationst &locations)
203202
{
204203
last_written_locations = locations;
205204
}
@@ -232,7 +231,7 @@ void write_location_contextt::output(
232231
*
233232
* \return the union of this objects location set, and 'locations'
234233
*/
235-
abstract_objectt::locationst
234+
context_abstract_objectt::locationst
236235
write_location_contextt::get_location_union(const locationst &locations) const
237236
{
238237
locationst existing_locations = get_last_written_locations();
@@ -279,10 +278,9 @@ bool write_location_contextt::has_been_modified(
279278
// For two sets of last written locations to match,
280279
// each location in one set must be equal to precisely one location
281280
// in the other, since a set can assume at most one match
282-
const abstract_objectt::locationst &first_write_locations =
281+
const locationst &first_write_locations =
283282
before_context->get_last_written_locations();
284-
const abstract_objectt::locationst &second_write_locations =
285-
get_last_written_locations();
283+
const locationst &second_write_locations = get_last_written_locations();
286284

287285
class location_ordert
288286
{
@@ -310,7 +308,7 @@ bool write_location_contextt::has_been_modified(
310308
rhs_location.insert(entry);
311309
}
312310

313-
abstract_objectt::locationst intersection;
311+
locationst intersection;
314312
std::set_intersection(
315313
lhs_location.cbegin(),
316314
lhs_location.cend(),
@@ -332,7 +330,7 @@ bool write_location_contextt::has_been_modified(
332330
*/
333331
void write_location_contextt::output_last_written_locations(
334332
std::ostream &out,
335-
const abstract_objectt::locationst &locations)
333+
const locationst &locations)
336334
{
337335
out << "[";
338336
bool comma = false;

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

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -92,13 +92,11 @@ class write_location_contextt : public context_abstract_objectt
9292
const abstract_object_pointert &value,
9393
bool merging_write) const override;
9494

95-
static void output_last_written_locations(
96-
std::ostream &out,
97-
const abstract_objectt::locationst &locations);
95+
static void
96+
output_last_written_locations(std::ostream &out, const locationst &locations);
9897

99-
virtual abstract_objectt::locationst get_last_written_locations() const;
100-
void
101-
set_last_written_locations(const abstract_objectt::locationst &locations);
98+
virtual locationst get_last_written_locations() const;
99+
void set_last_written_locations(const locationst &locations);
102100

103101
private:
104102
using combine_fn = std::function<abstract_objectt::combine_result(
@@ -111,10 +109,10 @@ class write_location_contextt : public context_abstract_objectt
111109
combine(const write_location_context_ptrt &other, combine_fn fn) const;
112110

113111
// To enforce copy-on-write these are private and have read-only accessors
114-
abstract_objectt::locationst last_written_locations;
112+
locationst last_written_locations;
115113

116-
context_abstract_object_ptrt update_location_context_internal(
117-
const abstract_objectt::locationst &locations) const override;
114+
context_abstract_object_ptrt
115+
update_location_context_internal(const locationst &locations) const override;
118116
};
119117

120118
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H

0 commit comments

Comments
 (0)