diff --git a/regression/goto-analyzer/nondet-bool/main.c b/regression/goto-analyzer/nondet-bool/main.c new file mode 100644 index 00000000000..0883611af6a --- /dev/null +++ b/regression/goto-analyzer/nondet-bool/main.c @@ -0,0 +1,11 @@ +_Bool nondet_bool(); +int main() +{ + int x = 0; + while(1) + { + if(nondet_bool()) + x = x + 1; + assert(x != 1000); + } +} diff --git a/regression/goto-analyzer/nondet-bool/test-constants.desc b/regression/goto-analyzer/nondet-bool/test-constants.desc new file mode 100644 index 00000000000..929a27ee26f --- /dev/null +++ b/regression/goto-analyzer/nondet-bool/test-constants.desc @@ -0,0 +1,7 @@ +CORE +main.c +--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --verify +^EXIT=0$ +^SIGNAL=0$ +\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN +-- diff --git a/regression/goto-analyzer/nondet-bool/test-intervals.desc b/regression/goto-analyzer/nondet-bool/test-intervals.desc new file mode 100644 index 00000000000..c7d2f0156e6 --- /dev/null +++ b/regression/goto-analyzer/nondet-bool/test-intervals.desc @@ -0,0 +1,7 @@ +CORE +main.c +--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values intervals --verify +^EXIT=0$ +^SIGNAL=0$ +\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN +-- diff --git a/regression/goto-analyzer/nondet-bool/test-value-sets.desc b/regression/goto-analyzer/nondet-bool/test-value-sets.desc new file mode 100644 index 00000000000..fbb287e2d1b --- /dev/null +++ b/regression/goto-analyzer/nondet-bool/test-value-sets.desc @@ -0,0 +1,7 @@ +CORE +main.c +--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values set-of-constants --verify +^EXIT=0$ +^SIGNAL=0$ +\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN +-- diff --git a/regression/goto-analyzer/ternary-operator/test-intervals.desc b/regression/goto-analyzer/ternary-operator/test-intervals.desc index 12fbe2f8c13..03e52dd051d 100644 --- a/regression/goto-analyzer/ternary-operator/test-intervals.desc +++ b/regression/goto-analyzer/ternary-operator/test-intervals.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ main::1::b1 \(\) -> \[1, 1\] @ \[2\] main::1::b2 \(\) -> \[0, 0\] @ \[3\] -main::1::b3 \(\) -> \[0, 1\] @ \[5\] +main::1::b3 \(\) -> TOP @ \[5\] main::1::i \(\) -> \[A, A\] @ \[7\] main::1::j \(\) -> \[14, 14\] @ \[9\] main::1::k \(\) -> \[A, 14\] @ \[11\] diff --git a/regression/goto-analyzer/ternary-operator/test-value-sets.desc b/regression/goto-analyzer/ternary-operator/test-value-sets.desc index 12aee4014f7..be593b76d7e 100644 --- a/regression/goto-analyzer/ternary-operator/test-value-sets.desc +++ b/regression/goto-analyzer/ternary-operator/test-value-sets.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end -main::1::b3 \(\) -> value-set-begin: TRUE, FALSE :value-set-end +main::1::b3 \(\) -> TOP @ \[5\] main::1::i \(\) -> value-set-begin: 10 :value-set-end main::1::j \(\) -> value-set-begin: 20 :value-set-end main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index d4610f47087..449b8d942a4 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -244,9 +244,25 @@ interval_abstract_valuet::interval_abstract_valuet( { } +bool new_interval_is_top(const constant_interval_exprt &e) +{ + if(e.is_top()) + return true; + + if(e.get_lower().is_false() && e.get_upper().is_true()) + return true; + if( + e.type().id() == ID_c_bool && e.get_lower().is_zero() && + e.get_upper().is_one()) + return true; + + return false; +} + interval_abstract_valuet::interval_abstract_valuet( const constant_interval_exprt &e) - : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e) + : abstract_value_objectt(e.type(), new_interval_is_top(e), e.is_bottom()), + interval(e) { } @@ -290,6 +306,11 @@ exprt interval_abstract_valuet::to_constant() const #endif } +void interval_abstract_valuet::set_top_internal() +{ + interval = constant_interval_exprt(type()); +} + size_t interval_abstract_valuet::internal_hash() const { return std::hash{}(interval.pretty()); diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 4a02192c4a5..45c04cbb3ef 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -96,6 +96,8 @@ class interval_abstract_valuet : public abstract_value_objectt private: constant_interval_exprt interval; + + void set_top_internal() override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index f451040cd92..43a27ea1d64 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -116,6 +116,7 @@ static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); static bool are_any_top(const abstract_object_sett &set); +static bool is_set_extreme(const typet &type, const abstract_object_sett &set); static abstract_object_sett compact_values(const abstract_object_sett &values); static abstract_object_sett widen_value_set( @@ -296,7 +297,7 @@ void value_set_abstract_objectt::set_values( const abstract_object_sett &other_values) { PRECONDITION(!other_values.empty()); - if(are_any_top(other_values)) + if(are_any_top(other_values) || is_set_extreme(type(), other_values)) { set_top(); } @@ -391,6 +392,65 @@ static bool are_any_top(const abstract_object_sett &set) }) != set.end(); } +using set_predicate_fn = std::function; +static bool set_contains(const abstract_object_sett &set, set_predicate_fn pred) +{ + return std::find_if( + set.begin(), + set.end(), + [&pred](const abstract_object_pointert &obj) { + const auto &value = + std::dynamic_pointer_cast(obj); + return pred(*value); + }) != set.end(); +} + +static bool set_has_extremes( + const abstract_object_sett &set, + set_predicate_fn lower_fn, + set_predicate_fn upper_fn) +{ + bool has_lower = set_contains(set, lower_fn); + if(!has_lower) + return false; + + bool has_upper = set_contains(set, upper_fn); + return has_upper; +} + +static bool is_set_extreme(const typet &type, const abstract_object_sett &set) +{ + if(type.id() == ID_bool) + { + return set_has_extremes( + set, + [](const abstract_value_objectt &value) { + auto c = value.to_constant(); + return c.is_false() || (c.id() == ID_min); + }, + [](const abstract_value_objectt &value) { + auto c = value.to_constant(); + return c.is_true() || (c.id() == ID_max); + }); + } + + if(type.id() == ID_c_bool) + { + return set_has_extremes( + set, + [](const abstract_value_objectt &value) { + auto c = value.to_constant(); + return c.is_zero() || (c.id() == ID_min); + }, + [](const abstract_value_objectt &value) { + auto c = value.to_constant(); + return c.is_one() || (c.id() == ID_max); + }); + } + + return false; +} + ///////////////// static abstract_object_sett non_destructive_compact(const abstract_object_sett &values); diff --git a/unit/Makefile b/unit/Makefile index 88d7c054396..60357218fcf 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -21,6 +21,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/eval.cpp \ analyses/variable-sensitivity/eval-member-access.cpp \ + analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp \ analyses/variable-sensitivity/interval_abstract_value/meet.cpp \ analyses/variable-sensitivity/interval_abstract_value/merge.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ @@ -29,6 +30,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \ analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \ + analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp \ analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp \ analyses/variable-sensitivity/value_set_abstract_object/meet.cpp \ analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \ diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp new file mode 100644 index 00000000000..0a188e78314 --- /dev/null +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + + Module: Unit tests for interval_abstract_valuet + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +#include +#include +#include + +static void +verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns) +{ + auto interval = make_interval(min_exprt(type), max_exprt(type), env, ns); + + EXPECT_TOP(interval); +} + +SCENARIO( + "extreme intervals go TOP", + "[core][analyses][variable-sensitivity][interval_abstract_value][extreme]") +{ + auto object_factory = variable_sensitivity_object_factoryt::configured_with( + vsd_configt::intervals()); + + auto environment = abstract_environmentt{object_factory}; + environment.make_top(); + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + GIVEN("[min-max] signed goes TOP") + { + verify_extreme_interval(signedbv_typet(32), environment, ns); + } + GIVEN("[min-max] unsigned goes TOP") + { + verify_extreme_interval(unsignedbv_typet(32), environment, ns); + } + GIVEN("[min-max] bool goes TOP") + { + verify_extreme_interval(bool_typet(), environment, ns); + } + GIVEN("[min-max] c_bool goes TOP") + { + verify_extreme_interval(bitvector_typet(ID_c_bool, 8), environment, ns); + } + GIVEN("[FALSE, TRUE] goes TOP") + { + auto boolInterval = + make_interval(false_exprt(), true_exprt(), environment, ns); + + EXPECT_TOP(boolInterval); + } + GIVEN("[0, 1] c_bool goes TOP") + { + auto c_bool_type = bitvector_typet(ID_c_bool, 8); + auto boolInterval = make_interval( + from_integer(0, c_bool_type), + from_integer(1, c_bool_type), + environment, + ns); + + EXPECT_TOP(boolInterval); + } +} diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp new file mode 100644 index 00000000000..2b18b941ffa --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp @@ -0,0 +1,63 @@ +/*******************************************************************\ + + Module: Unit tests for value_set_abstract_valuet + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +#include +#include +#include + +SCENARIO( + "value-sets spanning min-max go TOP", + "[core][analyses][variable-sensitivity][value_set_abstract_object][extreme]") +{ + auto object_factory = variable_sensitivity_object_factoryt::configured_with( + vsd_configt::intervals()); + + auto environment = abstract_environmentt{object_factory}; + environment.make_top(); + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + GIVEN("{FALSE, TRUE} goes TOP") + { + auto boolInterval = + make_value_set({false_exprt(), true_exprt()}, environment, ns); + + EXPECT_TOP(boolInterval); + } + GIVEN("{min(bool), max(bool)} goes TOP") + { + auto boolInterval = make_value_set( + {min_exprt(bool_typet()), max_exprt(bool_typet())}, environment, ns); + + EXPECT_TOP(boolInterval); + } + GIVEN("{0, 1} c_bool goes TOP") + { + auto c_bool_type = bitvector_typet(ID_c_bool, 8); + auto boolInterval = make_value_set( + {from_integer(0, c_bool_type), from_integer(1, c_bool_type)}, + environment, + ns); + + EXPECT_TOP(boolInterval); + } + GIVEN("{min(c_bool), max(c_bool)} goes TOP") + { + auto c_bool_type = bitvector_typet(ID_c_bool, 8); + auto boolInterval = make_value_set( + {min_exprt(c_bool_type), max_exprt(c_bool_type)}, environment, ns); + + EXPECT_TOP(boolInterval); + } +}