From 3756baea7ea8bfa3251354866672a98286b9ea53 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 19 Jun 2021 14:00:29 +0100 Subject: [PATCH 1/5] widening interval_abstract_value upper_bound can hit maximum If new upper bound is already at maximum, or overflows, then explicitly set to max_exprt(type) --- .../interval_abstract_value.cpp | 32 +++++++++++++++---- .../widening_merge.cpp | 30 ++++++++++++++++- 2 files changed, 54 insertions(+), 8 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index c7b63956eca..0151c1ac832 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -346,6 +346,8 @@ void interval_abstract_valuet::output( } } +exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns); + abstract_object_pointert widening_merge( const constant_interval_exprt &lhs, const constant_interval_exprt &rhs) @@ -354,26 +356,42 @@ abstract_object_pointert widening_merge( constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower()); auto upper_bound = constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper()); - auto range = plus_exprt( - minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); auto dummy_symbol_table = symbol_tablet{}; auto dummy_namespace = namespacet{dummy_symbol_table}; + auto range = plus_exprt( + minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); + // should extend lower bound? - if(rhs.get_lower() < lhs.get_lower()) - lower_bound = - simplify_expr(minus_exprt(lower_bound, range), dummy_namespace); + if(rhs.get_lower() < lhs.get_lower()) lower_bound = + simplify_expr(minus_exprt(lower_bound, range), dummy_namespace); // should extend upper bound? if(lhs.get_upper() < rhs.get_upper()) - upper_bound = - simplify_expr(plus_exprt(upper_bound, range), dummy_namespace); + upper_bound = extend_upper_bound(upper_bound, range, dummy_namespace); // new interval ... auto new_interval = constant_interval_exprt(lower_bound, upper_bound); return interval_abstract_valuet::make_interval(new_interval); } +bool has_overflowed(const exprt& value) +{ + return constant_interval_exprt::less_than(value, from_integer(0, value.type())); +} + +exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns) +{ + auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range), ns); + + if (constant_interval_exprt::contains_extreme(new_upper_bound) || + has_overflowed(new_upper_bound)) + return max_exprt(upper_bound.type()); + + return new_upper_bound; +} + + abstract_object_pointert interval_abstract_valuet::merge_with_value( const abstract_value_pointert &other, const widen_modet &widen_mode) const diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index 110a7b46a42..cce21152b49 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -14,7 +14,7 @@ #include static merge_result -widening_merge(abstract_object_pointert op1, abstract_object_pointert op2) +widening_merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2) { auto result = abstract_objectt::merge(op1, op2, widen_modet::could_widen); @@ -41,6 +41,8 @@ SCENARIO( const exprt val5minus = from_integer(-5, type); const exprt val8minus = from_integer(-8, type); const exprt val10minus = from_integer(-10, type); + auto valMax = max_exprt(type); + auto valMin = min_exprt(type); auto config = vsd_configt::constant_domain(); config.context_tracking.data_dependency_context = false; @@ -302,5 +304,31 @@ SCENARIO( EXPECT_MODIFIED(merged, val10minus, val4); } } + + WHEN("merging [1, 10] with [1, MAX]") + { + auto op1 = make_interval(val1, val10, environment, ns); + auto op2 = make_interval(val1, valMax, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [1, MAX]") + { + EXPECT_MODIFIED(merged, val1, valMax); + } + } + WHEN("merging [0, 1] with [1, very_large]") + { + auto veryLarge = from_integer(2<<29, type); + auto op1 = make_interval(val0, val1, environment, ns); + auto op2 = make_interval(val1, veryLarge, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [0, MAX]") + { + EXPECT_MODIFIED(merged, val0, valMax); + } + } } } From 9bfa965c41ad8f07854e67d7b19f015c7d2139e4 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 19 Jun 2021 14:47:58 +0100 Subject: [PATCH 2/5] widening interval_abstract_value lower_bound can be minimum If new lower bound is already at minimum, or underflows, then explicitly set to min_exprt(type) --- .../interval_abstract_value.cpp | 53 ++++++-- .../widening_merge.cpp | 115 +++++++++++++++++- 2 files changed, 154 insertions(+), 14 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 0151c1ac832..caa82156e3c 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -346,7 +346,14 @@ void interval_abstract_valuet::output( } } -exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns); +exprt extend_lower_bound( + const exprt &lower_bound, + const exprt &range, + const namespacet &ns); +exprt extend_upper_bound( + const exprt &upper_bound, + const exprt &range, + const namespacet &ns); abstract_object_pointert widening_merge( const constant_interval_exprt &lhs, @@ -361,13 +368,13 @@ abstract_object_pointert widening_merge( auto dummy_namespace = namespacet{dummy_symbol_table}; auto range = plus_exprt( - minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); + minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); // should extend lower bound? - if(rhs.get_lower() < lhs.get_lower()) lower_bound = - simplify_expr(minus_exprt(lower_bound, range), dummy_namespace); + if(constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())) + lower_bound = extend_lower_bound(lower_bound, range, dummy_namespace); // should extend upper bound? - if(lhs.get_upper() < rhs.get_upper()) + if(constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())) upper_bound = extend_upper_bound(upper_bound, range, dummy_namespace); // new interval ... @@ -375,23 +382,47 @@ abstract_object_pointert widening_merge( return interval_abstract_valuet::make_interval(new_interval); } -bool has_overflowed(const exprt& value) +bool has_underflowed(const exprt &value) { - return constant_interval_exprt::less_than(value, from_integer(0, value.type())); + return constant_interval_exprt::greater_than( + value, from_integer(0, value.type())); } +bool has_overflowed(const exprt &value) +{ + return constant_interval_exprt::less_than( + value, from_integer(0, value.type())); +} + +exprt extend_lower_bound( + const exprt &lower_bound, + const exprt &range, + const namespacet &ns) +{ + auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range), ns); -exprt extend_upper_bound(const exprt &upper_bound, const exprt& range, const namespacet& ns) + if( + constant_interval_exprt::contains_extreme(new_lower_bound) || + has_underflowed(new_lower_bound)) + return min_exprt(lower_bound.type()); + + return new_lower_bound; +} + +exprt extend_upper_bound( + const exprt &upper_bound, + const exprt &range, + const namespacet &ns) { auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range), ns); - if (constant_interval_exprt::contains_extreme(new_upper_bound) || - has_overflowed(new_upper_bound)) + if( + constant_interval_exprt::contains_extreme(new_upper_bound) || + has_overflowed(new_upper_bound)) return max_exprt(upper_bound.type()); return new_upper_bound; } - abstract_object_pointert interval_abstract_valuet::merge_with_value( const abstract_value_pointert &other, const widen_modet &widen_mode) const diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index cce21152b49..3699a6b1c61 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -13,8 +13,9 @@ #include #include -static merge_result -widening_merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2) +static merge_result widening_merge( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2) { auto result = abstract_objectt::merge(op1, op2, widen_modet::could_widen); @@ -319,7 +320,7 @@ SCENARIO( } WHEN("merging [0, 1] with [1, very_large]") { - auto veryLarge = from_integer(2<<29, type); + auto veryLarge = from_integer(2 << 29, type); auto op1 = make_interval(val0, val1, environment, ns); auto op2 = make_interval(val1, veryLarge, environment, ns); @@ -330,5 +331,113 @@ SCENARIO( EXPECT_MODIFIED(merged, val0, valMax); } } + + WHEN("merging [1, 10] with [MIN, 1]") + { + auto op1 = make_interval(val1, val10, environment, ns); + auto op2 = make_interval(valMin, val1, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [MIN, 10]") + { + EXPECT_MODIFIED(merged, valMin, val10); + } + } + WHEN("merging [0, 1] with [-very_large, 1]") + { + auto veryLargeMinus = from_integer(-(2 << 29), type); + auto op1 = make_interval(val0, val1, environment, ns); + auto op2 = make_interval(veryLargeMinus, val1, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [MIN, 1]") + { + EXPECT_MODIFIED(merged, valMin, val1); + } + } + + WHEN("merging [1, MAX] with [MIN, 1]") + { + auto op1 = make_interval(val1, valMax, environment, ns); + auto op2 = make_interval(valMin, val1, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is TOP - ie [MIN, MAX]") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging [MIN, 1] with [1, MAX]") + { + auto op1 = make_interval(valMin, val1, environment, ns); + auto op2 = make_interval(val1, valMax, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is TOP - ie [MIN, MAX]") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging [0, very_large] with [-very_large, 0]") + { + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); + auto op1 = make_interval(val0, veryLarge, environment, ns); + auto op2 = make_interval(veryLargeMinus, val0, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [MIN, very_large]") + { + EXPECT_MODIFIED(merged, valMin, veryLarge); + } + } + WHEN("merging [-very_large, 0] with [0, very_large]") + { + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); + auto op1 = make_interval(veryLargeMinus, val0, environment, ns); + auto op2 = make_interval(val0, veryLarge, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [-very_large, MAX]") + { + EXPECT_MODIFIED(merged, veryLargeMinus, valMax); + } + } + + WHEN("merging [-very_large, very_large] with [0, 1]") + { + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); + auto op1 = make_interval(veryLargeMinus, veryLarge, environment, ns); + auto op2 = make_interval(val0, val1, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [-very_large, very_large]") + { + EXPECT_UNMODIFIED(merged, veryLargeMinus, veryLarge); + } + } + WHEN("merging [0, 1] with [-very_large, very_large]") + { + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); + auto op1 = make_interval(val0, val1, environment, ns); + auto op2 = make_interval(veryLargeMinus, veryLarge, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is TOP, ie [MIN, MAX]") + { + EXPECT_MODIFIED_TOP(merged); + } + } } } From 5efbdcd22165bf5832d7a4b44b8b3536634cc207 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 19 Jun 2021 15:40:30 +0100 Subject: [PATCH 3/5] Gather interval widening out into a little helper class of its own --- src/analyses/Makefile | 1 + .../interval_abstract_value.cpp | 72 ++----------------- .../variable-sensitivity/widened_range.cpp | 51 +++++++++++++ .../variable-sensitivity/widened_range.h | 57 +++++++++++++++ 4 files changed, 113 insertions(+), 68 deletions(-) create mode 100644 src/analyses/variable-sensitivity/widened_range.cpp create mode 100644 src/analyses/variable-sensitivity/widened_range.h diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 9637db57551..c9ed0299bf1 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -52,6 +52,7 @@ SRC = ai.cpp \ variable-sensitivity/variable_sensitivity_dependence_graph.cpp \ variable-sensitivity/variable_sensitivity_domain.cpp \ variable-sensitivity/variable_sensitivity_object_factory.cpp \ + variable-sensitivity/widened_range.cpp \ variable-sensitivity/write_location_context.cpp \ variable-sensitivity/write_stack.cpp \ variable-sensitivity/write_stack_entry.cpp \ diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index caa82156e3c..93e05bec769 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -17,6 +17,7 @@ #include "abstract_environment.h" #include "abstract_object_statistics.h" #include "interval_abstract_value.h" +#include "widened_range.h" static index_range_implementation_ptrt make_interval_index_range( const constant_interval_exprt &interval, @@ -346,83 +347,18 @@ void interval_abstract_valuet::output( } } -exprt extend_lower_bound( - const exprt &lower_bound, - const exprt &range, - const namespacet &ns); -exprt extend_upper_bound( - const exprt &upper_bound, - const exprt &range, - const namespacet &ns); - abstract_object_pointert widening_merge( const constant_interval_exprt &lhs, const constant_interval_exprt &rhs) { - auto lower_bound = - constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower()); - auto upper_bound = - constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper()); - - auto dummy_symbol_table = symbol_tablet{}; - auto dummy_namespace = namespacet{dummy_symbol_table}; - - auto range = plus_exprt( - minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); - - // should extend lower bound? - if(constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())) - lower_bound = extend_lower_bound(lower_bound, range, dummy_namespace); - // should extend upper bound? - if(constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())) - upper_bound = extend_upper_bound(upper_bound, range, dummy_namespace); + auto widened = widened_ranget(lhs, rhs); // new interval ... - auto new_interval = constant_interval_exprt(lower_bound, upper_bound); + auto new_interval = + constant_interval_exprt(widened.lower_bound, widened.upper_bound); return interval_abstract_valuet::make_interval(new_interval); } -bool has_underflowed(const exprt &value) -{ - return constant_interval_exprt::greater_than( - value, from_integer(0, value.type())); -} -bool has_overflowed(const exprt &value) -{ - return constant_interval_exprt::less_than( - value, from_integer(0, value.type())); -} - -exprt extend_lower_bound( - const exprt &lower_bound, - const exprt &range, - const namespacet &ns) -{ - auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range), ns); - - if( - constant_interval_exprt::contains_extreme(new_lower_bound) || - has_underflowed(new_lower_bound)) - return min_exprt(lower_bound.type()); - - return new_lower_bound; -} - -exprt extend_upper_bound( - const exprt &upper_bound, - const exprt &range, - const namespacet &ns) -{ - auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range), ns); - - if( - constant_interval_exprt::contains_extreme(new_upper_bound) || - has_overflowed(new_upper_bound)) - return max_exprt(upper_bound.type()); - - return new_upper_bound; -} - abstract_object_pointert interval_abstract_valuet::merge_with_value( const abstract_value_pointert &other, const widen_modet &widen_mode) const diff --git a/src/analyses/variable-sensitivity/widened_range.cpp b/src/analyses/variable-sensitivity/widened_range.cpp new file mode 100644 index 00000000000..5a8cf88bb48 --- /dev/null +++ b/src/analyses/variable-sensitivity/widened_range.cpp @@ -0,0 +1,51 @@ +/*******************************************************************\ + + Module: helper for extending intervals during widening merges + + Author: Jez Higgins + +\*******************************************************************/ + +#include "widened_range.h" +#include + +static bool has_underflowed(const exprt &value) +{ + return constant_interval_exprt::greater_than( + value, from_integer(0, value.type())); +} +static bool has_overflowed(const exprt &value) +{ + return constant_interval_exprt::less_than( + value, from_integer(0, value.type())); +} + +exprt widened_ranget::make_lower_bound() const +{ + if(!lower_extended) + return lower_; + + auto new_lower_bound = simplify_expr(minus_exprt(lower_, range_), ns_); + + if( + constant_interval_exprt::contains_extreme(new_lower_bound) || + has_underflowed(new_lower_bound)) + return min_exprt(lower_.type()); + + return new_lower_bound; +} + +exprt widened_ranget::make_upper_bound() const +{ + if(!upper_extended) + return upper_; + + auto new_upper_bound = simplify_expr(plus_exprt(upper_, range_), ns_); + + if( + constant_interval_exprt::contains_extreme(new_upper_bound) || + has_overflowed(new_upper_bound)) + return max_exprt(upper_.type()); + + return new_upper_bound; +} diff --git a/src/analyses/variable-sensitivity/widened_range.h b/src/analyses/variable-sensitivity/widened_range.h new file mode 100644 index 00000000000..57c16add92f --- /dev/null +++ b/src/analyses/variable-sensitivity/widened_range.h @@ -0,0 +1,57 @@ +/*******************************************************************\ + + Module: helper for extending intervals during widening merges + + Author: Jez Higgins + +\*******************************************************************/ + +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H + +#include +#include +#include +#include + +class widened_ranget +{ +public: + widened_ranget( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) + : lower_extended( + constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())), + upper_extended( + constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())), + ns_(symbol_tablet{}), + lower_( + constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())), + upper_( + constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())), + range_( + plus_exprt(minus_exprt(upper_, lower_), from_integer(1, lhs.type()))), + lower_bound(make_lower_bound()), + upper_bound(make_upper_bound()) + { + } + + const bool lower_extended; + const bool upper_extended; + +private: + namespacet ns_; + exprt lower_; + exprt upper_; + exprt range_; + +public: + const exprt lower_bound; + const exprt upper_bound; + +private: + exprt make_lower_bound() const; + exprt make_upper_bound() const; +}; + +#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H From 5cd42eb7c5557d45abb17711828fda084fa304e7 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 19 Jun 2021 16:26:49 +0100 Subject: [PATCH 4/5] Use widening_range in value_set_abstract_object widening merge Means widened ranges are calculated in the same way for both intervals and value sets, both now handling max & min appropriately. --- .../interval_abstract_value.cpp | 4 +- .../value_set_abstract_object.cpp | 43 ++++++------- .../variable-sensitivity/widened_range.cpp | 20 +++--- .../variable-sensitivity/widened_range.h | 35 ++++++----- .../widening_merge.cpp | 12 +--- .../widening_merge.cpp | 63 +++++++++++++++++++ 6 files changed, 117 insertions(+), 60 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 93e05bec769..d4610f47087 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -354,8 +354,8 @@ abstract_object_pointert widening_merge( auto widened = widened_ranget(lhs, rhs); // new interval ... - auto new_interval = - constant_interval_exprt(widened.lower_bound, widened.upper_bound); + auto new_interval = constant_interval_exprt( + widened.widened_lower_bound, widened.widened_upper_bound); return interval_abstract_valuet::make_interval(new_interval); } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 5f157851458..f451040cd92 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -14,6 +14,7 @@ #include #include #include +#include #include #include @@ -414,6 +415,7 @@ static abstract_object_sett compact_values(const abstract_object_sett &values) } static exprt eval_expr(const exprt &e); +static bool is_eq(const exprt &lhs, const exprt &rhs); static bool is_le(const exprt &lhs, const exprt &rhs); static abstract_object_sett collapse_values_in_intervals( const abstract_object_sett &values, @@ -446,6 +448,8 @@ void collapse_overlapping_intervals( intervals.begin(), intervals.end(), [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) { + if(is_eq(lhs.get_lower(), rhs.get_lower())) + return is_le(lhs.get_upper(), rhs.get_upper()); return is_le(lhs.get_lower(), rhs.get_lower()); }); @@ -556,10 +560,14 @@ static exprt eval_expr(const exprt &e) return simplify_expr(e, ns); } +static bool is_eq(const exprt &lhs, const exprt &rhs) +{ + return constant_interval_exprt::equal(lhs, rhs); +} + static bool is_le(const exprt &lhs, const exprt &rhs) { - auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs); - return eval_expr(is_le_expr).is_true(); + return constant_interval_exprt::less_than_or_equal(lhs, rhs); } static abstract_object_sett widen_value_set( @@ -572,41 +580,34 @@ static abstract_object_sett widen_value_set( auto widened_ends = std::vector{}; - auto lower_bound = - constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower()); - auto upper_bound = - constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper()); - auto range = plus_exprt( - minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); - - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto range = widened_ranget(lhs, rhs); // should extend lower bound? - if(rhs.get_lower() < lhs.get_lower()) + if(range.is_lower_widened) { - auto widened_lower_bound = constant_interval_exprt( - simplify_expr(minus_exprt(lower_bound, range), ns), lower_bound); - widened_ends.push_back(widened_lower_bound); + auto extended_lower_bound = + constant_interval_exprt(range.widened_lower_bound, range.lower_bound); + + widened_ends.push_back(extended_lower_bound); for(auto &obj : values) { auto value = std::dynamic_pointer_cast(obj); auto as_expr = value->to_interval(); - if(is_le(as_expr.get_lower(), lower_bound)) + if(is_le(as_expr.get_lower(), range.lower_bound)) widened_ends.push_back(as_expr); } } // should extend upper bound? - if(lhs.get_upper() < rhs.get_upper()) + if(range.is_upper_widened) { - auto widened_upper_bound = constant_interval_exprt( - upper_bound, simplify_expr(plus_exprt(upper_bound, range), ns)); - widened_ends.push_back(widened_upper_bound); + auto extended_upper_bound = + constant_interval_exprt(range.upper_bound, range.widened_upper_bound); + widened_ends.push_back(extended_upper_bound); for(auto &obj : values) { auto value = std::dynamic_pointer_cast(obj); auto as_expr = value->to_interval(); - if(is_le(upper_bound, as_expr.get_upper())) + if(is_le(range.upper_bound, as_expr.get_upper())) widened_ends.push_back(as_expr); } } diff --git a/src/analyses/variable-sensitivity/widened_range.cpp b/src/analyses/variable-sensitivity/widened_range.cpp index 5a8cf88bb48..cc59c08c0f4 100644 --- a/src/analyses/variable-sensitivity/widened_range.cpp +++ b/src/analyses/variable-sensitivity/widened_range.cpp @@ -20,32 +20,32 @@ static bool has_overflowed(const exprt &value) value, from_integer(0, value.type())); } -exprt widened_ranget::make_lower_bound() const +exprt widened_ranget::widen_lower_bound() const { - if(!lower_extended) - return lower_; + if(!is_lower_widened) + return lower_bound; - auto new_lower_bound = simplify_expr(minus_exprt(lower_, range_), ns_); + auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range_), ns_); if( constant_interval_exprt::contains_extreme(new_lower_bound) || has_underflowed(new_lower_bound)) - return min_exprt(lower_.type()); + return min_exprt(lower_bound.type()); return new_lower_bound; } -exprt widened_ranget::make_upper_bound() const +exprt widened_ranget::widen_upper_bound() const { - if(!upper_extended) - return upper_; + if(!is_upper_widened) + return upper_bound; - auto new_upper_bound = simplify_expr(plus_exprt(upper_, range_), ns_); + auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range_), ns_); if( constant_interval_exprt::contains_extreme(new_upper_bound) || has_overflowed(new_upper_bound)) - return max_exprt(upper_.type()); + return max_exprt(upper_bound.type()); return new_upper_bound; } diff --git a/src/analyses/variable-sensitivity/widened_range.h b/src/analyses/variable-sensitivity/widened_range.h index 57c16add92f..3b0eb68dec4 100644 --- a/src/analyses/variable-sensitivity/widened_range.h +++ b/src/analyses/variable-sensitivity/widened_range.h @@ -20,38 +20,39 @@ class widened_ranget widened_ranget( const constant_interval_exprt &lhs, const constant_interval_exprt &rhs) - : lower_extended( + : is_lower_widened( constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())), - upper_extended( + is_upper_widened( constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())), - ns_(symbol_tablet{}), - lower_( + lower_bound( constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())), - upper_( + upper_bound( constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())), - range_( - plus_exprt(minus_exprt(upper_, lower_), from_integer(1, lhs.type()))), - lower_bound(make_lower_bound()), - upper_bound(make_upper_bound()) + ns_(symbol_tablet{}), + range_(plus_exprt( + minus_exprt(upper_bound, lower_bound), + from_integer(1, lhs.type()))), + widened_lower_bound(widen_lower_bound()), + widened_upper_bound(widen_upper_bound()) { } - const bool lower_extended; - const bool upper_extended; + const bool is_lower_widened; + const bool is_upper_widened; + const exprt lower_bound; + const exprt upper_bound; private: namespacet ns_; - exprt lower_; - exprt upper_; exprt range_; public: - const exprt lower_bound; - const exprt upper_bound; + const exprt widened_lower_bound; + const exprt widened_upper_bound; private: - exprt make_lower_bound() const; - exprt make_upper_bound() const; + exprt widen_lower_bound() const; + exprt widen_upper_bound() const; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index 3699a6b1c61..5213ca4592b 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -44,6 +44,8 @@ SCENARIO( const exprt val10minus = from_integer(-10, type); auto valMax = max_exprt(type); auto valMin = min_exprt(type); + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); auto config = vsd_configt::constant_domain(); config.context_tracking.data_dependency_context = false; @@ -320,7 +322,6 @@ SCENARIO( } WHEN("merging [0, 1] with [1, very_large]") { - auto veryLarge = from_integer(2 << 29, type); auto op1 = make_interval(val0, val1, environment, ns); auto op2 = make_interval(val1, veryLarge, environment, ns); @@ -346,7 +347,6 @@ SCENARIO( } WHEN("merging [0, 1] with [-very_large, 1]") { - auto veryLargeMinus = from_integer(-(2 << 29), type); auto op1 = make_interval(val0, val1, environment, ns); auto op2 = make_interval(veryLargeMinus, val1, environment, ns); @@ -384,8 +384,6 @@ SCENARIO( } WHEN("merging [0, very_large] with [-very_large, 0]") { - auto veryLarge = from_integer(2 << 29, type); - auto veryLargeMinus = from_integer(-(2 << 29), type); auto op1 = make_interval(val0, veryLarge, environment, ns); auto op2 = make_interval(veryLargeMinus, val0, environment, ns); @@ -398,8 +396,6 @@ SCENARIO( } WHEN("merging [-very_large, 0] with [0, very_large]") { - auto veryLarge = from_integer(2 << 29, type); - auto veryLargeMinus = from_integer(-(2 << 29), type); auto op1 = make_interval(veryLargeMinus, val0, environment, ns); auto op2 = make_interval(val0, veryLarge, environment, ns); @@ -413,8 +409,6 @@ SCENARIO( WHEN("merging [-very_large, very_large] with [0, 1]") { - auto veryLarge = from_integer(2 << 29, type); - auto veryLargeMinus = from_integer(-(2 << 29), type); auto op1 = make_interval(veryLargeMinus, veryLarge, environment, ns); auto op2 = make_interval(val0, val1, environment, ns); @@ -427,8 +421,6 @@ SCENARIO( } WHEN("merging [0, 1] with [-very_large, very_large]") { - auto veryLarge = from_integer(2 << 29, type); - auto veryLargeMinus = from_integer(-(2 << 29), type); auto op1 = make_interval(val0, val1, environment, ns); auto op2 = make_interval(veryLargeMinus, veryLarge, environment, ns); diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp index 42b526f2759..c23c4e13c6e 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp @@ -47,6 +47,10 @@ SCENARIO( auto val5minus = from_integer(-5, type); auto val8minus = from_integer(-8, type); auto val10minus = from_integer(-10, type); + auto valMax = max_exprt(type); + auto valMin = min_exprt(type); + auto veryLarge = from_integer(2 << 29, type); + auto veryLargeMinus = from_integer(-(2 << 29), type); auto config = vsd_configt::constant_domain(); config.context_tracking.data_dependency_context = false; @@ -382,5 +386,64 @@ SCENARIO( val2minus}); } } + + WHEN("merging {0, very_large} with {-very_large, 0}") + { + auto op1 = make_value_set({val0, veryLarge}, environment, ns); + auto op2 = make_value_set({veryLargeMinus, val0}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is {[MIN, -very_large], 0, very_large]") + { + EXPECT_MODIFIED( + merged, + {constant_interval_exprt(valMin, veryLargeMinus), val0, veryLarge}); + } + } + WHEN("merging {-very_large, 0} with {0, very_large}") + { + auto op1 = make_value_set({veryLargeMinus, val0}, environment, ns); + auto op2 = make_value_set({val0, veryLarge}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is {-very_large, 0, [very_large, MAX]}") + { + EXPECT_MODIFIED( + merged, + {veryLargeMinus, val0, constant_interval_exprt(veryLarge, valMax)}); + } + } + + WHEN("merging {-very_large, very_large } with {0, 1}") + { + auto op1 = make_value_set({veryLargeMinus, veryLarge}, environment, ns); + auto op2 = make_value_set({val0, val1}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is {-very_large, val0, val1, very_large}") + { + EXPECT_MODIFIED(merged, {veryLargeMinus, val0, val1, veryLarge}); + } + } + WHEN("merging {0, 1} with {-very_large, very_large}") + { + auto op1 = make_value_set({val0, val1}, environment, ns); + auto op2 = make_value_set({veryLargeMinus, veryLarge}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is {[MIN, 0}, [1, MAX]}") + { + EXPECT_MODIFIED( + merged, + {constant_interval_exprt(valMin, veryLargeMinus), + val0, + val1, + constant_interval_exprt(veryLarge, valMax)}); + } + } } } From 9815a7b0b5959f5cb37e87383907186c2fa3e410 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sun, 20 Jun 2021 13:08:11 +0100 Subject: [PATCH 5/5] Correct widening overflow detection for unsigned types --- .../variable-sensitivity/widened_range.cpp | 7 ++-- .../widening_merge.cpp | 37 +++++++++++++++++++ 2 files changed, 40 insertions(+), 4 deletions(-) diff --git a/src/analyses/variable-sensitivity/widened_range.cpp b/src/analyses/variable-sensitivity/widened_range.cpp index cc59c08c0f4..a98504b3131 100644 --- a/src/analyses/variable-sensitivity/widened_range.cpp +++ b/src/analyses/variable-sensitivity/widened_range.cpp @@ -14,10 +14,9 @@ static bool has_underflowed(const exprt &value) return constant_interval_exprt::greater_than( value, from_integer(0, value.type())); } -static bool has_overflowed(const exprt &value) +static bool has_overflowed(const exprt &value, const exprt &initial_value) { - return constant_interval_exprt::less_than( - value, from_integer(0, value.type())); + return constant_interval_exprt::less_than(value, initial_value); } exprt widened_ranget::widen_lower_bound() const @@ -44,7 +43,7 @@ exprt widened_ranget::widen_upper_bound() const if( constant_interval_exprt::contains_extreme(new_upper_bound) || - has_overflowed(new_upper_bound)) + has_overflowed(new_upper_bound, upper_bound)) return max_exprt(upper_bound.type()); return new_upper_bound; diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index 5213ca4592b..8a9641aa729 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -332,6 +332,43 @@ SCENARIO( EXPECT_MODIFIED(merged, val0, valMax); } } + WHEN("merging [0, 1] with [1, unsigned_very_large]") + { + auto utype = unsignedbv_typet(32); + auto uval0 = from_integer(0, utype); + auto uval1 = from_integer(1, utype); + auto uVeryLarge = from_integer(2 << 30, utype); + + auto op1 = make_interval(uval0, uval1, environment, ns); + auto op2 = make_interval(uval1, uVeryLarge, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [0, MAX]") + { + auto uvalMax = max_exprt(utype); + EXPECT_MODIFIED(merged, uval0, uvalMax); + } + } + WHEN("merging unsigned [7, 9] with [3, 6]") + { + auto utype = unsignedbv_typet(32); + auto uval0 = from_integer(0, utype); + auto uval3 = from_integer(3, utype); + auto uval6 = from_integer(6, utype); + auto uval7 = from_integer(7, utype); + auto uval9 = from_integer(9, utype); + + auto op1 = make_interval(uval7, uval9, environment, ns); + auto op2 = make_interval(uval3, uval6, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is [0, 9]") + { + EXPECT_MODIFIED(merged, uval0, uval9); + } + } WHEN("merging [1, 10] with [MIN, 1]") {