Skip to content

Commit abd4412

Browse files
martin-csmartin-cs
authored
Merge pull request #6046 from jezhiggins/vsd-widening-in-merge
Vsd - widening during abstract object merge
2 parents 6397c1e + 48146e0 commit abd4412

File tree

60 files changed

+2081
-1649
lines changed

Some content is hidden

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

60 files changed

+2081
-1649
lines changed

‎regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.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::1::1::i .* \[5, 5\] @ \[6\]
7-
^main::1::p .* \[2, 20\] @ \[5\]
7+
^main::1::p .* \[2, 1F9\] @ \[5\]
88
--

‎regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.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::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\]
7-
^main::1::p .* value-set-begin: 2, 17, 32 :value-set-end @ \[5\]
7+
^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\]
88
--

‎regression/goto-analyzer/value-set-convert-to-interval/main.c renamed to ‎regression/goto-analyzer/value-set-compact-01/main.c

File renamed without changes.

‎regression/goto-analyzer/value-set-convert-to-interval/test.desc renamed to ‎regression/goto-analyzer/value-set-compact-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ main.c
55
^SIGNAL=0$
66
main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\]
77
main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\]
8-
main::1::c .* \[14, 1E\] @ \[30\]
8+
main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\]
99
--

‎regression/goto-analyzer/value-set-compact-02/main.c

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
#include <stdbool.h>
2+
3+
extern int x;
4+
5+
int main(void)
6+
{
7+
int a[1] = {0};
8+
switch(x)
9+
{
10+
case 1:
11+
a[0] = 1;
12+
break;
13+
case 2:
14+
a[0] = 2;
15+
break;
16+
case 3:
17+
a[0] = 3;
18+
break;
19+
case 4:
20+
a[0] = 4;
21+
break;
22+
case 5:
23+
a[0] = 5;
24+
break;
25+
case 6:
26+
a[0] = 6;
27+
break;
28+
case 7:
29+
a[0] = 7;
30+
break;
31+
case 8:
32+
a[0] = 8;
33+
break;
34+
case 9:
35+
a[0] = 9;
36+
break;
37+
case 10:
38+
a[0] = 10;
39+
break;
40+
case 11:
41+
a[0] = 11;
42+
break;
43+
case 12:
44+
a[0] = 12;
45+
break;
46+
}
47+
48+
return 0;
49+
}

‎regression/goto-analyzer/value-set-compact-02/test.desc

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-arrays every-element --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]
7+
--

‎regression/goto-analyzer/value-set-compact-03/main.c

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
#include <stdbool.h>
2+
3+
extern int x;
4+
5+
struct S
6+
{
7+
int a;
8+
};
9+
10+
int main(void)
11+
{
12+
struct S a;
13+
a.a = 0;
14+
switch(x)
15+
{
16+
case 1:
17+
a.a = 1;
18+
break;
19+
case 2:
20+
a.a = 2;
21+
break;
22+
case 3:
23+
a.a = 3;
24+
break;
25+
case 4:
26+
a.a = 4;
27+
break;
28+
case 5:
29+
a.a = 5;
30+
break;
31+
case 6:
32+
a.a = 6;
33+
break;
34+
case 7:
35+
a.a = 7;
36+
break;
37+
case 8:
38+
a.a = 8;
39+
break;
40+
case 9:
41+
a.a = 9;
42+
break;
43+
case 10:
44+
a.a = 10;
45+
break;
46+
case 11:
47+
a.a = 11;
48+
break;
49+
case 12:
50+
a.a = 12;
51+
break;
52+
}
53+
54+
return 0;
55+
}

‎regression/goto-analyzer/value-set-compact-03/test.desc

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-structs every-field --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .*
7+
--

‎src/analyses/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,6 @@ SRC = ai.cpp \
4747
variable-sensitivity/interval_abstract_value.cpp \
4848
variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
4949
variable-sensitivity/value_set_abstract_object.cpp \
50-
variable-sensitivity/value_set_abstract_value.cpp \
5150
variable-sensitivity/value_set_pointer_abstract_object.cpp \
5251
variable-sensitivity/variable_sensitivity_configuration.cpp \
5352
variable-sensitivity/variable_sensitivity_dependence_graph.cpp \

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,8 @@ class abstract_aggregate_objectt : public abstract_objectt,
127127
static bool merge_shared_maps(
128128
const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map1,
129129
const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map2,
130-
sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map)
130+
sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map,
131+
const widen_modet &widen_mode)
131132
{
132133
bool modified = false;
133134

@@ -137,13 +138,12 @@ class abstract_aggregate_objectt : public abstract_objectt,
137138

138139
for(auto &item : delta_view)
139140
{
140-
bool changes = false;
141-
abstract_object_pointert v_new =
142-
abstract_objectt::merge(item.m, item.get_other_map_value(), changes);
143-
if(changes)
141+
auto v_new =
142+
abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode);
143+
if(v_new.modified)
144144
{
145145
modified = true;
146-
out_map.replace(item.k, v_new);
146+
out_map.replace(item.k, v_new.object);
147147
}
148148
}
149149

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

Lines changed: 18 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -312,38 +312,33 @@ abstract_object_pointert abstract_environmentt::add_object_context(
312312
return object_factory->wrap_with_context(abstract_object);
313313
}
314314

315-
bool abstract_environmentt::merge(const abstract_environmentt &env)
315+
bool abstract_environmentt::merge(
316+
const abstract_environmentt &env,
317+
widen_modet widen_mode)
316318
{
317319
// for each entry in the incoming environment we need to either add it
318320
// if it is new, or merge with the existing key if it is not present
319-
320321
if(bottom)
321322
{
322323
*this = env;
323324
return !env.bottom;
324325
}
325-
else if(env.bottom)
326-
{
326+
327+
if(env.bottom)
327328
return false;
328-
}
329-
else
330-
{
331-
// For each element in the intersection of map and env.map merge
332-
// If the result of the merge is top, remove from the map
333-
bool modified = false;
334-
decltype(env.map)::delta_viewt delta_view;
335-
env.map.get_delta_view(map, delta_view);
336-
for(const auto &entry : delta_view)
337-
{
338-
bool object_modified = false;
339-
abstract_object_pointert new_object = abstract_objectt::merge(
340-
entry.get_other_map_value(), entry.m, object_modified);
341-
modified |= object_modified;
342-
map.replace(entry.k, new_object);
343-
}
344329

345-
return modified;
330+
// For each element in the intersection of map and env.map merge
331+
// If the result of the merge is top, remove from the map
332+
bool modified = false;
333+
for(const auto &entry : env.map.get_delta_view(map))
334+
{
335+
auto merge_result =
336+
abstract_objectt::merge(entry.get_other_map_value(), entry.m, widen_mode);
337+
modified |= merge_result.modified;
338+
map.replace(entry.k, merge_result.object);
346339
}
340+
341+
return modified;
347342
}
348343

349344
void abstract_environmentt::havoc(const std::string &havoc_string)
@@ -508,12 +503,8 @@ std::vector<abstract_object_pointert> eval_operands(
508503
///////////
509504
abstract_value_pointert as_value(const abstract_object_pointert &obj)
510505
{
511-
auto context_value =
512-
std::dynamic_pointer_cast<const context_abstract_objectt>(obj);
513-
514-
return context_value
515-
? as_value(context_value->unwrap_context())
516-
: std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
506+
return std::dynamic_pointer_cast<const abstract_value_objectt>(
507+
obj->unwrap_context());
517508
}
518509

519510
bool is_value(const abstract_object_pointert &obj)

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,12 @@ class variable_sensitivity_object_factoryt;
2525
using variable_sensitivity_object_factory_ptrt =
2626
std::shared_ptr<variable_sensitivity_object_factoryt>;
2727

28+
enum class widen_modet
29+
{
30+
no,
31+
could_widen
32+
};
33+
2834
class abstract_environmentt
2935
{
3036
public:
@@ -180,9 +186,10 @@ class abstract_environmentt
180186
/// Computes the join between "this" and "b"
181187
///
182188
/// \param env: the other environment
189+
/// \param widen_mode: indicates if this is a widening merge
183190
///
184191
/// \return A Boolean, true when the merge has changed something
185-
virtual bool merge(const abstract_environmentt &env);
192+
virtual bool merge(const abstract_environmentt &env, widen_modet widen_mode);
186193

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

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

Lines changed: 10 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,9 @@ const typet &abstract_objectt::type() const
4848
return t;
4949
}
5050

51-
abstract_object_pointert
52-
abstract_objectt::merge(const abstract_object_pointert &other) const
51+
abstract_object_pointert abstract_objectt::merge(
52+
const abstract_object_pointert &other,
53+
const widen_modet &widen_mode) const
5354
{
5455
return abstract_object_merge(other);
5556
}
@@ -182,26 +183,16 @@ void abstract_objectt::output(
182183
}
183184
}
184185

185-
abstract_object_pointert abstract_objectt::merge(
186+
abstract_objectt::combine_result abstract_objectt::merge(
186187
const abstract_object_pointert &op1,
187188
const abstract_object_pointert &op2,
188-
bool &out_modifications)
189+
const widen_modet &widen_mode)
189190
{
190191
abstract_object_pointert result = op1->should_use_base_merge(op2)
191192
? op1->abstract_object_merge(op2)
192-
: op1->merge(op2);
193+
: op1->merge(op2, widen_mode);
193194
// If no modifications, we will return the original pointer
194-
out_modifications = result != op1;
195-
196-
return result;
197-
}
198-
199-
abstract_object_pointert abstract_objectt::merge(
200-
const abstract_object_pointert &op1,
201-
const abstract_object_pointert &op2)
202-
{
203-
bool dummy;
204-
return merge(op1, op2, dummy);
195+
return {result, result != op1};
205196
}
206197

207198
bool abstract_objectt::should_use_base_merge(
@@ -210,18 +201,15 @@ bool abstract_objectt::should_use_base_merge(
210201
return is_top() || other->is_bottom() || other->is_top();
211202
}
212203

213-
abstract_object_pointert abstract_objectt::meet(
204+
abstract_objectt::combine_result abstract_objectt::meet(
214205
const abstract_object_pointert &op1,
215-
const abstract_object_pointert &op2,
216-
bool &out_modifications)
206+
const abstract_object_pointert &op2)
217207
{
218208
abstract_object_pointert result = op1->should_use_base_meet(op2)
219209
? op1->abstract_object_meet(op2)
220210
: op1->meet(op2);
221211
// If no modifications, we will return the original pointer
222-
out_modifications = result != op1;
223-
224-
return result;
212+
return {result, result != op1};
225213
}
226214

227215
bool abstract_objectt::should_use_base_meet(

0 commit comments

Comments
 (0)