Skip to content

Commit c311ad1

Browse files
committed
Rework liveness_contextt on top of write_location_contextt
Maintains existing three-way-merge behaviour, which otherwise was lost because we'd discarded too much context information to be able to merge precisely.
1 parent 1354ef3 commit c311ad1

File tree

8 files changed

+41
-149
lines changed

8 files changed

+41
-149
lines changed

regression/goto-analyzer/liveness-function-call/main.c

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
#include <assert.h>
2-
31
int globalX;
42

53
void f00()
@@ -21,4 +19,4 @@ int main()
2119
assert(globalX == 2);
2220

2321
return 0;
24-
}
22+
}

regression/goto-analyzer/liveness-function-call/test-liveness-show.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ main.c
33
--variable-sensitivity --vsd-liveness --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[30\]
6+
globalX .* 0 @ \[28\]
77
globalX .* 1 @ \[0\]
8-
globalX .* TOP @ \[33\]
8+
globalX .* 2 @ \[3\]
9+
globalX .* TOP @ \[31\]
910
--

regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@ main.c
33
--variable-sensitivity --vsd-liveness --three-way-merge --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[30\]
6+
globalX .* 0 @ \[28\]
77
globalX .* 1 @ \[0\]
8-
globalX .* TOP @ \[33\]
8+
globalX .* 2 @ \[3\]
9+
globalX .* TOP @ \[31\]
910
--

regression/goto-analyzer/liveness-function-call/test-liveness-three-way.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main.assertion.1\] .* globalX == 1: SUCCESS
7-
\[main.assertion.2\] .* globalX == 2: UNKNOWN
7+
\[main.assertion.2\] .* globalX == 2: SUCCESS
88
--

regression/goto-analyzer/liveness-function-call/test-write-location-show.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[30\]
6+
globalX .* 0 @ \[28\]
77
globalX .* 1 @ \[0\]
8-
globalX .* TOP @ \[0, 4\]
8+
globalX .* TOP @ \[0, 3\]
99
--

regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --three-way-merge --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[30\]
6+
globalX .* 0 @ \[28\]
77
globalX .* 1 @ \[0\]
8-
globalX .* 2 @ \[4\]
8+
globalX .* 2 @ \[3\]
99
--

src/analyses/variable-sensitivity/liveness_context.cpp

Lines changed: 23 additions & 118 deletions
Original file line numberDiff line numberDiff line change
@@ -42,21 +42,15 @@ abstract_object_pointert liveness_contextt::write(
4242
const abstract_object_pointert &value,
4343
bool merging_write) const
4444
{
45-
abstract_object_pointert updated_child = child_abstract_object->write(
46-
environment, ns, stack, specifier, value, merging_write);
47-
48-
// Only perform an update if the write to the child has in fact changed it...
49-
if(updated_child == child_abstract_object)
45+
auto updated = std::dynamic_pointer_cast<const liveness_contextt>(
46+
write_location_contextt::write(
47+
environment, ns, stack, specifier, value, merging_write));
48+
if(updated == shared_from_this())
5049
return shared_from_this();
5150

52-
// Need to ensure the result of the write is still wrapped in a dependency
53-
// context
54-
const auto &result =
55-
std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
56-
57-
result->set_child(updated_child);
58-
59-
// Update the child and record the updated write locations
51+
// record the updated write locations
52+
auto result =
53+
std::dynamic_pointer_cast<liveness_contextt>(updated->mutable_clone());
6054
auto value_context =
6155
std::dynamic_pointer_cast<const liveness_contextt>(value);
6256
if(value_context)
@@ -83,91 +77,40 @@ abstract_object_pointert liveness_contextt::merge(
8377

8478
if(cast_other)
8579
{
86-
auto merge_fn = [&widen_mode](
87-
const abstract_object_pointert &op1,
88-
const abstract_object_pointert &op2) {
89-
return abstract_objectt::merge(op1, op2, widen_mode);
90-
};
91-
return combine(cast_other, merge_fn);
80+
auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
81+
write_location_contextt::merge(other, widen_mode));
82+
return reset_location_on_merge(merged);
9283
}
9384

9485
return abstract_objectt::merge(other, widen_mode);
9586
}
9687

97-
// need wrapper function here to disambiguate meet overload
98-
abstract_objectt::combine_result object_meet(
99-
const abstract_object_pointert &op1,
100-
const abstract_object_pointert &op2)
101-
{
102-
return abstract_objectt::meet(op1, op2);
103-
}
104-
105-
abstract_object_pointert
106-
liveness_contextt::meet(const abstract_object_pointert &other) const
107-
{
108-
auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
109-
110-
if(cast_other)
111-
return combine(cast_other, object_meet);
112-
113-
return abstract_objectt::meet(other);
114-
}
115-
116-
bool liveness_contextt::at_same_location(const liveness_context_ptrt &rhs) const
117-
{
118-
return has_location() && rhs->has_location() &&
119-
(get_location()->location_number ==
120-
rhs->get_location()->location_number);
121-
}
122-
123-
abstract_object_pointert liveness_contextt::combine(
124-
const liveness_context_ptrt &other,
125-
combine_fn fn) const
126-
{
127-
auto combined_child = fn(child_abstract_object, other->child_abstract_object);
128-
auto location_match = at_same_location(other);
129-
130-
if(combined_child.modified || !location_match)
131-
{
132-
const auto &result =
133-
std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
134-
result->set_child(combined_child.object);
135-
result->reset_location();
136-
return result;
137-
}
138-
139-
return shared_from_this();
140-
}
141-
14288
abstract_object_pointert liveness_contextt::abstract_object_merge_internal(
14389
const abstract_object_pointert &other) const
14490
{
145-
auto other_context =
146-
std::dynamic_pointer_cast<const liveness_contextt>(other);
147-
148-
if(!other_context)
149-
return shared_from_this();
150-
151-
if(other_context && !at_same_location(other_context))
152-
{
153-
auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
154-
result->reset_location();
155-
return result;
156-
}
157-
158-
return shared_from_this();
91+
auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
92+
write_location_contextt::abstract_object_merge_internal(other));
93+
return reset_location_on_merge(merged);
15994
}
16095

161-
void liveness_contextt::reset_location()
96+
abstract_object_pointert liveness_contextt::reset_location_on_merge(
97+
const liveness_context_ptrt &merged) const
16298
{
163-
assign_location.reset();
99+
if(merged == shared_from_this())
100+
return shared_from_this();
101+
102+
auto updated =
103+
std::dynamic_pointer_cast<liveness_contextt>(merged->mutable_clone());
104+
updated->assign_location.reset();
105+
return updated;
164106
}
165107

166108
context_abstract_objectt::context_abstract_object_ptrt
167109
liveness_contextt::update_location_context_internal(
168110
const locationst &locations) const
169111
{
170112
auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
113+
result->set_last_written_locations(locations);
171114
result->set_location(*locations.cbegin());
172115
return result;
173116
}
@@ -198,44 +141,6 @@ void liveness_contextt::output(
198141
out << " @ [undefined]";
199142
}
200143

201-
/**
202-
* Determine whether 'this' abstract_object has been modified in comparison
203-
* to a previous 'before' state.
204-
*
205-
* \param before the abstract_object_pointert to use as a reference to
206-
* compare against
207-
*
208-
* \return true if 'this' is considered to have been modified in comparison
209-
* to 'before', false otherwise.
210-
*/
211-
bool liveness_contextt::has_been_modified(
212-
const abstract_object_pointert &before) const
213-
{
214-
if(this == before.get())
215-
return false;
216-
217-
auto before_context =
218-
std::dynamic_pointer_cast<const liveness_contextt>(before);
219-
220-
if(!before_context)
221-
{
222-
// The other context is not something we understand, so must assume
223-
// that the abstract_object has been modified
224-
return true;
225-
}
226-
227-
// Even if the pointers are different, it maybe that it has changed only
228-
// because of a merge operation, rather than an actual write. Given that
229-
// this class has knowledge of where writes have occured, use that
230-
// information to determine if any writes have happened and use that as the
231-
// proxy for whether the value has changed or not.
232-
//
233-
// For two sets of last written locations to match,
234-
// each location in one set must be equal to precisely one location
235-
// in the other, since a set can assume at most one match
236-
return !at_same_location(before_context);
237-
}
238-
239144
abstract_object_pointert
240145
liveness_contextt::merge_location_context(const locationt &location) const
241146
{

src/analyses/variable-sensitivity/liveness_context.h

Lines changed: 6 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
1616
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LIVENESS_CONTEXT_H
1717

18-
#include <analyses/variable-sensitivity/context_abstract_object.h>
18+
#include <analyses/variable-sensitivity/write_location_context.h>
1919
#include <iostream>
2020
#include <stack>
2121

@@ -30,13 +30,13 @@
3030
* of this, 'context_abstract_objectt<T>' which provides the same
3131
* constructors as the standard 'abstract_objectt' class.
3232
*/
33-
class liveness_contextt : public context_abstract_objectt
33+
class liveness_contextt : public write_location_contextt
3434
{
3535
public:
3636
explicit liveness_contextt(
3737
const abstract_object_pointert child,
3838
const typet &type)
39-
: context_abstract_objectt(child, type)
39+
: write_location_contextt(child, type)
4040
{
4141
}
4242

@@ -45,7 +45,7 @@ class liveness_contextt : public context_abstract_objectt
4545
const typet &type,
4646
bool top,
4747
bool bottom)
48-
: context_abstract_objectt(child, type, top, bottom)
48+
: write_location_contextt(child, type, top, bottom)
4949
{
5050
}
5151

@@ -54,16 +54,10 @@ class liveness_contextt : public context_abstract_objectt
5454
const exprt &expr,
5555
const abstract_environmentt &environment,
5656
const namespacet &ns)
57-
: context_abstract_objectt(child, expr, environment, ns)
57+
: write_location_contextt(child, expr, environment, ns)
5858
{
5959
}
6060

61-
virtual ~liveness_contextt()
62-
{
63-
}
64-
65-
bool has_been_modified(const abstract_object_pointert &before) const override;
66-
6761
abstract_object_pointert
6862
merge_location_context(const locationt &location) const override;
6963

@@ -76,8 +70,6 @@ class liveness_contextt : public context_abstract_objectt
7670
abstract_object_pointert merge(
7771
const abstract_object_pointert &other,
7872
const widen_modet &widen_mode) const override;
79-
abstract_object_pointert
80-
meet(const abstract_object_pointert &other) const override;
8173

8274
abstract_object_pointert abstract_object_merge_internal(
8375
const abstract_object_pointert &other) const override;
@@ -91,24 +83,19 @@ class liveness_contextt : public context_abstract_objectt
9183
bool merging_write) const override;
9284

9385
locationt get_location() const;
94-
void reset_location();
9586

9687
private:
97-
using combine_fn = std::function<abstract_objectt::combine_result(
98-
const abstract_object_pointert &op1,
99-
const abstract_object_pointert &op2)>;
10088
using liveness_context_ptrt = std::shared_ptr<const liveness_contextt>;
10189

10290
abstract_object_pointert
103-
combine(const liveness_context_ptrt &other, combine_fn fn) const;
91+
reset_location_on_merge(const liveness_context_ptrt &merged) const;
10492

10593
optionalt<locationt> assign_location;
10694

10795
context_abstract_object_ptrt
10896
update_location_context_internal(const locationst &locations) const override;
10997

11098
bool has_location() const;
111-
bool at_same_location(const liveness_context_ptrt &rhs) const;
11299

113100
void set_location(const locationt &location);
114101
};

0 commit comments

Comments
 (0)