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 c7b63956eca..d4610f47087 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, @@ -350,27 +351,11 @@ 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 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}; - - // should extend lower bound? - 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); + 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.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 new file mode 100644 index 00000000000..a98504b3131 --- /dev/null +++ b/src/analyses/variable-sensitivity/widened_range.cpp @@ -0,0 +1,50 @@ +/*******************************************************************\ + + 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, const exprt &initial_value) +{ + return constant_interval_exprt::less_than(value, initial_value); +} + +exprt widened_ranget::widen_lower_bound() const +{ + if(!is_lower_widened) + return lower_bound; + + 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 widened_ranget::widen_upper_bound() const +{ + if(!is_upper_widened) + return upper_bound; + + 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, upper_bound)) + 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 new file mode 100644 index 00000000000..3b0eb68dec4 --- /dev/null +++ b/src/analyses/variable-sensitivity/widened_range.h @@ -0,0 +1,58 @@ +/*******************************************************************\ + + 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) + : is_lower_widened( + constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())), + is_upper_widened( + constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())), + lower_bound( + constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())), + upper_bound( + constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())), + 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 is_lower_widened; + const bool is_upper_widened; + const exprt lower_bound; + const exprt upper_bound; + +private: + namespacet ns_; + exprt range_; + +public: + const exprt widened_lower_bound; + const exprt widened_upper_bound; + +private: + 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 110a7b46a42..8a9641aa729 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(abstract_object_pointert op1, 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); @@ -41,6 +42,10 @@ 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 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; @@ -302,5 +307,166 @@ 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 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); + } + } + 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]") + { + 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 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 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 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 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 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); + } + } } } 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)}); + } + } } }