Skip to content

Commit a7d4c3d

Browse files
martin-csmartin-cs
authored
Merge pull request #6209 from jezhiggins/vsd-bool-intervals-go-top
VSD - bool intervals go top
2 parents b69a629 + 0a0a862 commit a7d4c3d

File tree

12 files changed

+257
-4
lines changed

12 files changed

+257
-4
lines changed

‎regression/goto-analyzer/nondet-bool/main.c

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

‎regression/goto-analyzer/nondet-bool/test-constants.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+
--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
7+
--

‎regression/goto-analyzer/nondet-bool/test-intervals.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+
--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values intervals --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
7+
--

‎regression/goto-analyzer/nondet-bool/test-value-sets.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+
--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values set-of-constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
7+
--

‎regression/goto-analyzer/ternary-operator/test-intervals.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
main::1::b1 \(\) -> \[1, 1\] @ \[2\]
77
main::1::b2 \(\) -> \[0, 0\] @ \[3\]
8-
main::1::b3 \(\) -> \[0, 1\] @ \[5\]
8+
main::1::b3 \(\) -> TOP @ \[5\]
99
main::1::i \(\) -> \[A, A\] @ \[7\]
1010
main::1::j \(\) -> \[14, 14\] @ \[9\]
1111
main::1::k \(\) -> \[A, 14\] @ \[11\]

‎regression/goto-analyzer/ternary-operator/test-value-sets.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end
77
main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end
8-
main::1::b3 \(\) -> value-set-begin: TRUE, FALSE :value-set-end
8+
main::1::b3 \(\) -> TOP @ \[5\]
99
main::1::i \(\) -> value-set-begin: 10 :value-set-end
1010
main::1::j \(\) -> value-set-begin: 20 :value-set-end
1111
main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end

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

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -244,9 +244,25 @@ interval_abstract_valuet::interval_abstract_valuet(
244244
{
245245
}
246246

247+
bool new_interval_is_top(const constant_interval_exprt &e)
248+
{
249+
if(e.is_top())
250+
return true;
251+
252+
if(e.get_lower().is_false() && e.get_upper().is_true())
253+
return true;
254+
if(
255+
e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
256+
e.get_upper().is_one())
257+
return true;
258+
259+
return false;
260+
}
261+
247262
interval_abstract_valuet::interval_abstract_valuet(
248263
const constant_interval_exprt &e)
249-
: abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e)
264+
: abstract_value_objectt(e.type(), new_interval_is_top(e), e.is_bottom()),
265+
interval(e)
250266
{
251267
}
252268

@@ -290,6 +306,11 @@ exprt interval_abstract_valuet::to_constant() const
290306
#endif
291307
}
292308

309+
void interval_abstract_valuet::set_top_internal()
310+
{
311+
interval = constant_interval_exprt(type());
312+
}
313+
293314
size_t interval_abstract_valuet::internal_hash() const
294315
{
295316
return std::hash<std::string>{}(interval.pretty());

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,8 @@ class interval_abstract_valuet : public abstract_value_objectt
9696

9797
private:
9898
constant_interval_exprt interval;
99+
100+
void set_top_internal() override;
99101
};
100102

101103
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H

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

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,7 @@ static abstract_object_pointert
116116
maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
117117

118118
static bool are_any_top(const abstract_object_sett &set);
119+
static bool is_set_extreme(const typet &type, const abstract_object_sett &set);
119120

120121
static abstract_object_sett compact_values(const abstract_object_sett &values);
121122
static abstract_object_sett widen_value_set(
@@ -296,7 +297,7 @@ void value_set_abstract_objectt::set_values(
296297
const abstract_object_sett &other_values)
297298
{
298299
PRECONDITION(!other_values.empty());
299-
if(are_any_top(other_values))
300+
if(are_any_top(other_values) || is_set_extreme(type(), other_values))
300301
{
301302
set_top();
302303
}
@@ -391,6 +392,65 @@ static bool are_any_top(const abstract_object_sett &set)
391392
}) != set.end();
392393
}
393394

395+
using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
396+
static bool set_contains(const abstract_object_sett &set, set_predicate_fn pred)
397+
{
398+
return std::find_if(
399+
set.begin(),
400+
set.end(),
401+
[&pred](const abstract_object_pointert &obj) {
402+
const auto &value =
403+
std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
404+
return pred(*value);
405+
}) != set.end();
406+
}
407+
408+
static bool set_has_extremes(
409+
const abstract_object_sett &set,
410+
set_predicate_fn lower_fn,
411+
set_predicate_fn upper_fn)
412+
{
413+
bool has_lower = set_contains(set, lower_fn);
414+
if(!has_lower)
415+
return false;
416+
417+
bool has_upper = set_contains(set, upper_fn);
418+
return has_upper;
419+
}
420+
421+
static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
422+
{
423+
if(type.id() == ID_bool)
424+
{
425+
return set_has_extremes(
426+
set,
427+
[](const abstract_value_objectt &value) {
428+
auto c = value.to_constant();
429+
return c.is_false() || (c.id() == ID_min);
430+
},
431+
[](const abstract_value_objectt &value) {
432+
auto c = value.to_constant();
433+
return c.is_true() || (c.id() == ID_max);
434+
});
435+
}
436+
437+
if(type.id() == ID_c_bool)
438+
{
439+
return set_has_extremes(
440+
set,
441+
[](const abstract_value_objectt &value) {
442+
auto c = value.to_constant();
443+
return c.is_zero() || (c.id() == ID_min);
444+
},
445+
[](const abstract_value_objectt &value) {
446+
auto c = value.to_constant();
447+
return c.is_one() || (c.id() == ID_max);
448+
});
449+
}
450+
451+
return false;
452+
}
453+
394454
/////////////////
395455
static abstract_object_sett
396456
non_destructive_compact(const abstract_object_sett &values);

‎unit/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ SRC += analyses/ai/ai.cpp \
2121
analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
2222
analyses/variable-sensitivity/eval.cpp \
2323
analyses/variable-sensitivity/eval-member-access.cpp \
24+
analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp \
2425
analyses/variable-sensitivity/interval_abstract_value/meet.cpp \
2526
analyses/variable-sensitivity/interval_abstract_value/merge.cpp \
2627
analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \
@@ -29,6 +30,7 @@ SRC += analyses/ai/ai.cpp \
2930
analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \
3031
analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \
3132
analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \
33+
analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp \
3234
analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp \
3335
analyses/variable-sensitivity/value_set_abstract_object/meet.cpp \
3436
analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \

0 commit comments

Comments
 (0)