Skip to content

Commit f786079

Browse files
committed
Pass merge_location to newly merged object
Extend region-contextt to pick this up if it needs to use it. Ever other object just ignores it.
1 parent 6835fb0 commit f786079

File tree

8 files changed

+78
-3
lines changed

8 files changed

+78
-3
lines changed
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+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --vsd-region-tracking --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\]
7+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[4, 6\]
7+
--

src/analyses/variable-sensitivity/abstract_environment.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -364,8 +364,9 @@ bool abstract_environmentt::merge(
364364
bool modified = false;
365365
for(const auto &entry : env.map.get_delta_view(map))
366366
{
367-
auto merge_result =
368-
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+
369370
modified |= merge_result.modified;
370371
map.replace(entry.k, merge_result.object);
371372
}

src/analyses/variable-sensitivity/abstract_object.cpp

Lines changed: 20 additions & 0 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
}
@@ -247,6 +261,12 @@ abstract_objectt::write_location_context(const locationt &location) const
247261
return shared_from_this();
248262
}
249263

264+
abstract_object_pointert
265+
abstract_objectt::merge_location_context(const locationt &location) const
266+
{
267+
return shared_from_this();
268+
}
269+
250270
void abstract_objectt::dump_map(
251271
std::ostream out,
252272
const abstract_objectt::shared_mapt &m)

src/analyses/variable-sensitivity/abstract_object.h

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -264,6 +264,11 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
264264
abstract_object_pointert object;
265265
bool modified;
266266
};
267+
static combine_result merge(
268+
const abstract_object_pointert &op1,
269+
const abstract_object_pointert &op2,
270+
const locationt &merge_location,
271+
const widen_modet &widen_mode);
267272
static combine_result merge(
268273
const abstract_object_pointert &op1,
269274
const abstract_object_pointert &op2,
@@ -289,7 +294,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
289294
meet(const abstract_object_pointert &other) const;
290295

291296
/**
292-
* Update the location context for an abstract object.
297+
* Update the write location context for an abstract object.
293298
*
294299
* \param location the location to be updated
295300
*
@@ -299,6 +304,17 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
299304
virtual abstract_object_pointert
300305
write_location_context(const locationt &location) const;
301306

307+
/**
308+
* Update the merge location context for an abstract object.
309+
*
310+
* \param location the location to be updated
311+
*
312+
* \return a clone of this abstract object with its location context
313+
* updated
314+
*/
315+
virtual abstract_object_pointert
316+
merge_location_context(const locationt &location) const;
317+
302318
// Const versions must perform copy-on-write
303319
abstract_object_pointert make_top() const
304320
{

src/analyses/variable-sensitivity/region_context.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,3 +202,14 @@ bool region_contextt::has_been_modified(
202202
// in the other, since a set can assume at most one match
203203
return before_context->get_location() != get_location();
204204
}
205+
206+
abstract_object_pointert
207+
region_contextt::merge_location_context(const locationt &location) const
208+
{
209+
if(assign_location.has_value())
210+
return shared_from_this();
211+
212+
auto update = std::dynamic_pointer_cast<region_contextt>(mutable_clone());
213+
update->assign_location = location;
214+
return update;
215+
}

src/analyses/variable-sensitivity/region_context.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,9 @@ class region_contextt : public context_abstract_objectt
6464

6565
bool has_been_modified(const abstract_object_pointert &before) const override;
6666

67+
abstract_object_pointert
68+
merge_location_context(const locationt &location) const override;
69+
6770
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
6871
const override;
6972

0 commit comments

Comments
 (0)