Skip to content

Commit 43c7f71

Browse files
martin-csmartin-cs
authored
Merge pull request #6271 from jezhiggins/vsd-region-context
VSD - liveness context
2 parents a508bca + c311ad1 commit 43c7f71

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+837
-235
lines changed

‎regression/goto-analyzer/liveness-array/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x[2] = {0, 1};
5+
6+
if(non_det)
7+
x[0] = 2;
8+
else
9+
x[0] = 3;
10+
}

‎regression/goto-analyzer/liveness-array/test-liveness.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
8+
^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\]
9+
--

‎regression/goto-analyzer/liveness-array/test-write-location.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
8+
^main::1::x .* \{\[0\] = \[2, 3\] @ \[4, 6\]
9+
--

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int globalX;
2+
3+
void f00()
4+
{
5+
}
6+
7+
int main()
8+
{
9+
globalX = 1;
10+
11+
f00();
12+
13+
assert(globalX == 1);
14+
15+
globalX = 2;
16+
17+
f00();
18+
19+
assert(globalX == 2);
20+
21+
return 0;
22+
}

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

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

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

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

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-liveness --three-way-merge --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] .* globalX == 1: SUCCESS
7+
\[main.assertion.2\] .* globalX == 2: SUCCESS
8+
--

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-liveness --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] .* globalX == 1: SUCCESS
7+
\[main.assertion.2\] .* globalX == 2: UNKNOWN
8+
--

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

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

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

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

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --three-way-merge --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] .* globalX == 1: SUCCESS
7+
\[main.assertion.2\] .* globalX == 2: SUCCESS
8+
--

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] .* globalX == 1: SUCCESS
7+
\[main.assertion.2\] .* globalX == 2: UNKNOWN
8+
--

‎regression/goto-analyzer/liveness-loop/main.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x = 0;
5+
6+
for(int i = 0; i != 5; ++i)
7+
{
8+
int y = 0;
9+
x++;
10+
y = 1;
11+
}
12+
}

‎regression/goto-analyzer/liveness-loop/test-liveness.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[9\]
9+
^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[5\]
10+
--

‎regression/goto-analyzer/liveness-loop/test-write-location.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[8\]
9+
^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[2, 8\]
10+
--

‎regression/goto-analyzer/liveness-pointer-write-through/main.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x = 0;
5+
int *p = &x;
6+
7+
if(non_det)
8+
*p = 2;
9+
else
10+
*p = 3;
11+
}

‎regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[9\]
9+
^main::1::p .* TOP @ \[3\]
10+
^main::1::p .*\(main::1::x\) @ \[4\]
11+
--

‎regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[6, 8\]
9+
^main::1::p .* TOP @ \[3\]
10+
^main::1::p .*\(main::1::x\) @ \[4\]
11+
--

‎regression/goto-analyzer/liveness-struct/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
struct S
2+
{
3+
int x;
4+
int y;
5+
};
6+
7+
int main()
8+
{
9+
int non_det;
10+
struct S s = {1, 3};
11+
12+
if(non_det)
13+
s.x = 2;
14+
else
15+
s.x = 3;
16+
}

‎regression/goto-analyzer/liveness-struct/test-liveness.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::s .* \{\} @ \[1\]
7+
^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\]
8+
^main::1::s .* \{.x=\[2, 3\] @ \[7\], .y=\[3, 3\] @ \[2\]\} @ \[7\]
9+
--

‎regression/goto-analyzer/liveness-struct/test-write-location.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-structs every-field --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::s .* \{\} @ \[1\]
7+
^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\]
8+
^main::1::s .* \{.x=\[2, 3\] @ \[4, 6\], .y=\[3, 3\] @ \[2\]\} @ \[4, 6\]
9+
--

‎regression/goto-analyzer/liveness/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int main()
2+
{
3+
int non_det;
4+
int x = 0;
5+
6+
if(non_det)
7+
x = 2;
8+
else
9+
x = 3;
10+
}

‎regression/goto-analyzer/liveness/test-liveness.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\]
9+
--

‎regression/goto-analyzer/liveness/test-write-location.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* TOP @ \[1\]
7+
^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\]
8+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[4, 6\]
9+
--

‎src/analyses/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ SRC = ai.cpp \
4545
variable-sensitivity/full_array_abstract_object.cpp \
4646
variable-sensitivity/full_struct_abstract_object.cpp \
4747
variable-sensitivity/interval_abstract_value.cpp \
48+
variable-sensitivity/liveness_context.cpp \
4849
variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
4950
variable-sensitivity/two_value_pointer_abstract_object.cpp \
5051
variable-sensitivity/value_set_abstract_object.cpp \

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -345,6 +345,7 @@ abstract_object_pointert abstract_environmentt::add_object_context(
345345

346346
bool abstract_environmentt::merge(
347347
const abstract_environmentt &env,
348+
const goto_programt::const_targett &merge_location,
348349
widen_modet widen_mode)
349350
{
350351
// for each entry in the incoming environment we need to either add it
@@ -363,8 +364,9 @@ bool abstract_environmentt::merge(
363364
bool modified = false;
364365
for(const auto &entry : env.map.get_delta_view(map))
365366
{
366-
auto merge_result =
367-
abstract_objectt::merge(entry.get_other_map_value(), entry.m, widen_mode);
367+
auto merge_result = abstract_objectt::merge(
368+
entry.get_other_map_value(), entry.m, merge_location, widen_mode);
369+
368370
modified |= merge_result.modified;
369371
map.replace(entry.k, merge_result.object);
370372
}

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,10 +190,14 @@ class abstract_environmentt
190190
/// Computes the join between "this" and "b"
191191
///
192192
/// \param env: the other environment
193+
/// \param merge_location: when the merge is happening
193194
/// \param widen_mode: indicates if this is a widening merge
194195
///
195196
/// \return A Boolean, true when the merge has changed something
196-
virtual bool merge(const abstract_environmentt &env, widen_modet widen_mode);
197+
virtual bool merge(
198+
const abstract_environmentt &env,
199+
const goto_programt::const_targett &merge_location,
200+
widen_modet widen_mode);
197201

198202
/// This should be used as a default case / everything else has failed
199203
/// The string is so that I can easily find and diagnose cases where this

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

Lines changed: 22 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -206,6 +206,19 @@ void abstract_objectt::output(
206206
}
207207
}
208208

209+
abstract_objectt::combine_result abstract_objectt::merge(
210+
const abstract_object_pointert &op1,
211+
const abstract_object_pointert &op2,
212+
const locationt &merge_location,
213+
const widen_modet &widen_mode)
214+
{
215+
abstract_object_pointert result = merge(op1, op2, widen_mode).object;
216+
result = result->merge_location_context(merge_location);
217+
218+
// If no modifications, we will return the original pointer
219+
return {result, result != op1};
220+
}
221+
209222
abstract_objectt::combine_result abstract_objectt::merge(
210223
const abstract_object_pointert &op1,
211224
const abstract_object_pointert &op2,
@@ -214,6 +227,7 @@ abstract_objectt::combine_result abstract_objectt::merge(
214227
abstract_object_pointert result = op1->should_use_base_merge(op2)
215228
? op1->abstract_object_merge(op2)
216229
: op1->merge(op2, widen_mode);
230+
217231
// If no modifications, we will return the original pointer
218232
return {result, result != op1};
219233
}
@@ -241,9 +255,14 @@ bool abstract_objectt::should_use_base_meet(
241255
return is_bottom() || is_top() || other->is_bottom() || other->is_top();
242256
}
243257

244-
abstract_object_pointert abstract_objectt::update_location_context(
245-
const locationst &locations,
246-
const bool update_sub_elements) const
258+
abstract_object_pointert
259+
abstract_objectt::write_location_context(const locationt &location) const
260+
{
261+
return shared_from_this();
262+
}
263+
264+
abstract_object_pointert
265+
abstract_objectt::merge_location_context(const locationt &location) const
247266
{
248267
return shared_from_this();
249268
}

0 commit comments

Comments
 (0)