Skip to content

Commit 6d3c463

Browse files
jezhigginsjezhiggins
committed
Extend constant_abstract_valuet to merge with other value representations
Can successfully merge with matching intervals and value sets, including from bottom. Goes TOP otherwise.
1 parent c9abd82 commit 6d3c463

File tree

4 files changed

+253
-33
lines changed

4 files changed

+253
-33
lines changed

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -291,4 +291,6 @@ class abstract_value_objectt : public abstract_objectt,
291291
value_range_implementation() const = 0;
292292
};
293293

294+
using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;
295+
294296
#endif

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

Lines changed: 18 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,11 @@ constant_abstract_valuet::constant_abstract_valuet(const typet &t)
4242
{
4343
}
4444

45+
constant_abstract_valuet::constant_abstract_valuet(const exprt &e)
46+
: abstract_value_objectt(e.type(), false, false), value(e)
47+
{
48+
}
49+
4550
constant_abstract_valuet::constant_abstract_valuet(
4651
const typet &t,
4752
bool tp,
@@ -104,38 +109,25 @@ void constant_abstract_valuet::output(
104109
abstract_object_pointert
105110
constant_abstract_valuet::merge(abstract_object_pointert other) const
106111
{
107-
constant_abstract_value_pointert cast_other =
108-
std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
112+
auto cast_other =
113+
std::dynamic_pointer_cast<const abstract_value_objectt>(other);
109114
if(cast_other)
110-
{
111115
return merge_constant_constant(cast_other);
112-
}
113-
else
114-
{
115-
// TODO(tkiley): How do we set the result to be toppish? Does it matter?
116-
return abstract_objectt::merge(other);
117-
}
116+
117+
return abstract_objectt::merge(other);
118118
}
119119

120120
abstract_object_pointert constant_abstract_valuet::merge_constant_constant(
121-
const constant_abstract_value_pointert &other) const
121+
const abstract_value_pointert &other) const
122122
{
123-
if(is_bottom())
124-
{
125-
return std::make_shared<constant_abstract_valuet>(*other);
126-
}
127-
else
128-
{
129-
// Can we actually merge these value
130-
if(value == other->value)
131-
{
132-
return shared_from_this();
133-
}
134-
else
135-
{
136-
return abstract_objectt::merge(other);
137-
}
138-
}
123+
auto other_expr = other->to_constant();
124+
if(is_bottom() && other_expr.is_constant())
125+
return std::make_shared<constant_abstract_valuet>(other_expr);
126+
127+
if(value == other_expr) // Can we actually merge these value
128+
return shared_from_this();
129+
130+
return abstract_objectt::merge(other);
139131
}
140132

141133
void constant_abstract_valuet::get_statistics(

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

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,9 @@
1919

2020
class constant_abstract_valuet : public abstract_value_objectt
2121
{
22-
private:
23-
typedef sharing_ptrt<constant_abstract_valuet>
24-
constant_abstract_value_pointert;
25-
2622
public:
2723
explicit constant_abstract_valuet(const typet &t);
24+
explicit constant_abstract_valuet(const exprt &t);
2825
constant_abstract_valuet(const typet &t, bool tp, bool bttm);
2926
constant_abstract_valuet(
3027
const exprt &e,
@@ -75,15 +72,15 @@ class constant_abstract_valuet : public abstract_value_objectt
7572
abstract_object_pointert merge(abstract_object_pointert other) const override;
7673

7774
private:
78-
/// Merges another constant abstract value into this one
75+
/// Merges another abstract value into this one
7976
///
8077
/// \param other: the abstract object to merge with
8178
///
8279
/// \return Returns a new abstract object that is the result of the merge
8380
/// unless the merge is the same as this abstract object, in which
8481
/// case it returns this.
8582
abstract_object_pointert
86-
merge_constant_constant(const constant_abstract_value_pointert &other) const;
83+
merge_constant_constant(const abstract_value_pointert &other) const;
8784

8885
exprt value;
8986
};

‎unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp‎

Lines changed: 230 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -250,5 +250,234 @@ SCENARIO(
250250
}
251251
}
252252
}
253-
}
254253

254+
GIVEN("merging a constant and an interval")
255+
{
256+
WHEN("merging 1 with [1, 1]")
257+
{
258+
auto op1 = make_constant(val1, environment, ns);
259+
auto op2 = make_interval(val1, val1, environment, ns);
260+
261+
auto merged = merge(op1, op2);
262+
263+
THEN("result is unmodified 1")
264+
{
265+
EXPECT_UNMODIFIED(merged, val1);
266+
}
267+
}
268+
WHEN("merging 1 with [1, 2]")
269+
{
270+
auto op1 = make_constant(val1, environment, ns);
271+
auto op2 = make_interval(val1, val2, environment, ns);
272+
273+
auto merged = merge(op1, op2);
274+
275+
THEN("result is modified TOP")
276+
{
277+
EXPECT_MODIFIED(merged);
278+
EXPECT_TOP(merged.result);
279+
}
280+
}
281+
WHEN("merging 1 with [2, 2]")
282+
{
283+
auto op1 = make_constant(val1, environment, ns);
284+
auto op2 = make_interval(val2, val2, environment, ns);
285+
286+
auto merged = merge(op1, op2);
287+
288+
THEN("result is modified TOP")
289+
{
290+
EXPECT_MODIFIED(merged);
291+
EXPECT_TOP(merged.result);
292+
}
293+
}
294+
WHEN("merging BOTTOM with [1, 1]")
295+
{
296+
auto op1 = make_bottom_constant();
297+
auto op2 = make_interval(val1, val1, environment, ns);
298+
299+
auto merged = merge(op1, op2);
300+
301+
THEN("result is modified 1")
302+
{
303+
EXPECT_MODIFIED(merged, val1);
304+
}
305+
}
306+
WHEN("merging BOTTOM with [1, 2]")
307+
{
308+
auto op1 = make_bottom_constant();
309+
auto op2 = make_interval(val1, val2, environment, ns);
310+
311+
auto merged = merge(op1, op2);
312+
313+
THEN("result is modified TOP")
314+
{
315+
EXPECT_MODIFIED(merged);
316+
EXPECT_TOP(merged.result);
317+
}
318+
}
319+
}
320+
321+
GIVEN("merging a constant and a value set")
322+
{
323+
WHEN("merging 1 with { 1 }")
324+
{
325+
auto op1 = make_constant(val1, environment, ns);
326+
auto op2 = make_value_set(val1, environment, ns);
327+
328+
auto merged = merge(op1, op2);
329+
330+
THEN("result is unmodified 1")
331+
{
332+
EXPECT_UNMODIFIED(merged, val1);
333+
}
334+
}
335+
WHEN("merging 1 with { 2 }")
336+
{
337+
auto op1 = make_constant(val1, environment, ns);
338+
auto op2 = make_value_set(val2, environment, ns);
339+
340+
auto merged = merge(op1, op2);
341+
342+
THEN("result is modified TOP")
343+
{
344+
EXPECT_MODIFIED(merged);
345+
EXPECT_TOP(merged.result);
346+
}
347+
}
348+
WHEN("merging 1 with { 1, 2 }")
349+
{
350+
auto op1 = make_constant(val1, environment, ns);
351+
auto op2 = make_value_set({val1, val2}, environment, ns);
352+
353+
auto merged = merge(op1, op2);
354+
355+
THEN("result is modified TOP")
356+
{
357+
EXPECT_MODIFIED(merged);
358+
EXPECT_TOP(merged.result);
359+
}
360+
}
361+
WHEN("merging 1 with { [ 1, 1 ] }")
362+
{
363+
auto op1 = make_constant(val1, environment, ns);
364+
auto op2 =
365+
make_value_set(constant_interval_exprt(val1, val1), environment, ns);
366+
367+
auto merged = merge(op1, op2);
368+
369+
THEN("result is unmodified 1")
370+
{
371+
EXPECT_UNMODIFIED(merged, val1);
372+
}
373+
}
374+
WHEN("merging 1 with { [ 2, 2 ] }")
375+
{
376+
auto op1 = make_constant(val1, environment, ns);
377+
auto op2 =
378+
make_value_set(constant_interval_exprt(val2, val2), environment, ns);
379+
380+
auto merged = merge(op1, op2);
381+
382+
THEN("result is modified TOP")
383+
{
384+
EXPECT_MODIFIED(merged);
385+
EXPECT_TOP(merged.result);
386+
}
387+
}
388+
WHEN("merging 1 with { [ 1, 2 ] }")
389+
{
390+
auto op1 = make_constant(val1, environment, ns);
391+
auto op2 =
392+
make_value_set(constant_interval_exprt(val1, val2), environment, ns);
393+
394+
auto merged = merge(op1, op2);
395+
396+
THEN("result is modified TOP")
397+
{
398+
EXPECT_MODIFIED(merged);
399+
EXPECT_TOP(merged.result);
400+
}
401+
}
402+
WHEN("merging 1 with { 1, [ 1, 2 ] }")
403+
{
404+
auto op1 = make_constant(val1, environment, ns);
405+
auto op2 = make_value_set(
406+
{val1, constant_interval_exprt(val1, val2)}, environment, ns);
407+
408+
auto merged = merge(op1, op2);
409+
410+
THEN("result is modified TOP")
411+
{
412+
EXPECT_MODIFIED(merged);
413+
EXPECT_TOP(merged.result);
414+
}
415+
}
416+
WHEN("merging BOTTOM with { 1 }")
417+
{
418+
auto op1 = make_bottom_constant();
419+
auto op2 = make_value_set(val1, environment, ns);
420+
421+
auto merged = merge(op1, op2);
422+
423+
THEN("result is modified 1")
424+
{
425+
EXPECT_MODIFIED(merged, val1);
426+
}
427+
}
428+
WHEN("merging BOTTOM with { 1, 2 }")
429+
{
430+
auto op1 = make_bottom_constant();
431+
auto op2 = make_value_set({val1, val2}, environment, ns);
432+
433+
auto merged = merge(op1, op2);
434+
435+
THEN("result is modified TOP")
436+
{
437+
EXPECT_MODIFIED(merged);
438+
EXPECT_TOP(merged.result);
439+
}
440+
}
441+
WHEN("merging BOTTOM with { [ 1, 1 ] }")
442+
{
443+
auto op1 = make_bottom_constant();
444+
auto op2 =
445+
make_value_set(constant_interval_exprt(val1, val1), environment, ns);
446+
447+
auto merged = merge(op1, op2);
448+
449+
THEN("result is modified 1")
450+
{
451+
EXPECT_MODIFIED(merged, val1);
452+
}
453+
}
454+
WHEN("merging BOTTOM with { [ 1, 2 ] }")
455+
{
456+
auto op1 = make_bottom_constant();
457+
auto op2 =
458+
make_value_set(constant_interval_exprt(val1, val2), environment, ns);
459+
460+
auto merged = merge(op1, op2);
461+
462+
THEN("result is modified TOP")
463+
{
464+
EXPECT_MODIFIED(merged);
465+
EXPECT_TOP(merged.result);
466+
}
467+
}
468+
WHEN("merging BOTTOM with { 1, [ 1, 2 ] }")
469+
{
470+
auto op1 = make_bottom_constant();
471+
auto op2 = make_value_set(
472+
{val1, constant_interval_exprt(val1, val2)}, environment, ns);
473+
474+
auto merged = merge(op1, op2);
475+
476+
THEN("result is modified TOP")
477+
{
478+
EXPECT_MODIFIED(merged);
479+
EXPECT_TOP(merged.result);
480+
}
481+
}
482+
}
483+
}

0 commit comments

Comments
 (0)