diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 13000ce979b..5144e5b2e89 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -456,6 +456,10 @@ class abstract_objectt : public std::enable_shared_from_this top = false; this->set_not_top_internal(); } + void set_not_bottom() + { + bottom = false; + } }; struct abstract_hashert diff --git a/src/analyses/variable-sensitivity/abstract_object_set.cpp b/src/analyses/variable-sensitivity/abstract_object_set.cpp index 9336b6e560b..92a2a96437b 100644 --- a/src/analyses/variable-sensitivity/abstract_object_set.cpp +++ b/src/analyses/variable-sensitivity/abstract_object_set.cpp @@ -37,18 +37,24 @@ void abstract_object_sett::output( join_strings(out, output_values.begin(), output_values.end(), ", "); } -abstract_object_pointert abstract_object_sett::to_interval() +constant_interval_exprt abstract_object_sett::to_interval() const { PRECONDITION(!values.empty()); - exprt lower_expr = first()->to_constant(); - exprt upper_expr = first()->to_constant(); + const auto &initial = + std::dynamic_pointer_cast(first()); + + exprt lower_expr = initial->to_interval().get_lower(); + exprt upper_expr = initial->to_interval().get_upper(); for(const auto &value : values) { - const auto &value_expr = value->to_constant(); - lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr); - upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr); + const auto &v = + std::dynamic_pointer_cast(value); + const auto &value_expr = v->to_interval(); + lower_expr = + constant_interval_exprt::get_min(lower_expr, value_expr.get_lower()); + upper_expr = + constant_interval_exprt::get_max(upper_expr, value_expr.get_upper()); } - return std::make_shared( - constant_interval_exprt(lower_expr, upper_expr)); + return constant_interval_exprt(lower_expr, upper_expr); } diff --git a/src/analyses/variable-sensitivity/abstract_object_set.h b/src/analyses/variable-sensitivity/abstract_object_set.h index 8d05ae405ea..300704f8006 100644 --- a/src/analyses/variable-sensitivity/abstract_object_set.h +++ b/src/analyses/variable-sensitivity/abstract_object_set.h @@ -80,10 +80,9 @@ class abstract_object_sett void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const; - /// Cast the set of values \p other_values to an interval. - /// \param other_values: the value-set to be abstracted into an interval - /// \return the interval-abstract-object containing \p other_values - abstract_object_pointert to_interval(); + /// Calculate the set of values as an interval. + /// \return the constant_interval_exprt bounding the values + constant_interval_exprt to_interval() const; private: value_sett values; diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index 0ca0e314e8a..a1221f6648b 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -631,11 +631,17 @@ class value_set_evaluator auto unwrapped_values = unwrap_and_extract_values(new_values); if(unwrapped_values.size() > value_set_abstract_objectt::max_value_set_size) - return unwrapped_values.to_interval(); + return make_interval(unwrapped_values); return make_value_set(unwrapped_values); } + static abstract_object_pointert + make_interval(const abstract_object_sett &values) + { + return std::make_shared(values.to_interval()); + } + static abstract_object_pointert make_value_set(const abstract_object_sett &values) { diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 65f9ca690e2..989e536ba1f 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -13,6 +13,7 @@ #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H #include +#include class abstract_value_tag { @@ -265,6 +266,8 @@ class abstract_value_objectt : public abstract_objectt, return value_ranget(value_range_implementation()); } + virtual constant_interval_exprt to_interval() const = 0; + /// Interface for transforms /// /// \param expr: the expression to evaluate and find the result of it. @@ -291,4 +294,6 @@ class abstract_value_objectt : public abstract_objectt, value_range_implementation() const = 0; }; -#endif \ No newline at end of file +using abstract_value_pointert = sharing_ptrt; + +#endif diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index a5d490c3aec..ae3f9462195 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -42,6 +42,11 @@ constant_abstract_valuet::constant_abstract_valuet(const typet &t) { } +constant_abstract_valuet::constant_abstract_valuet(const exprt &e) + : abstract_value_objectt(e.type(), false, false), value(e) +{ +} + constant_abstract_valuet::constant_abstract_valuet( const typet &t, bool tp, @@ -86,6 +91,11 @@ exprt constant_abstract_valuet::to_constant() const } } +constant_interval_exprt constant_abstract_valuet::to_interval() const +{ + return constant_interval_exprt(value, value); +} + void constant_abstract_valuet::output( std::ostream &out, const ai_baset &ai, @@ -104,38 +114,25 @@ void constant_abstract_valuet::output( abstract_object_pointert constant_abstract_valuet::merge(abstract_object_pointert other) const { - constant_abstract_value_pointert cast_other = - std::dynamic_pointer_cast(other); + auto cast_other = + std::dynamic_pointer_cast(other); if(cast_other) - { return merge_constant_constant(cast_other); - } - else - { - // TODO(tkiley): How do we set the result to be toppish? Does it matter? - return abstract_objectt::merge(other); - } + + return abstract_objectt::merge(other); } abstract_object_pointert constant_abstract_valuet::merge_constant_constant( - const constant_abstract_value_pointert &other) const + const abstract_value_pointert &other) const { - if(is_bottom()) - { - return std::make_shared(*other); - } - else - { - // Can we actually merge these value - if(value == other->value) - { - return shared_from_this(); - } - else - { - return abstract_objectt::merge(other); - } - } + auto other_expr = other->to_constant(); + if(is_bottom() && other_expr.is_constant()) + return std::make_shared(other_expr); + + if(value == other_expr) // Can we actually merge these value + return shared_from_this(); + + return abstract_objectt::merge(other); } void constant_abstract_valuet::get_statistics( diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index 0e9b4af533a..0cf91bd7de3 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -19,12 +19,9 @@ class constant_abstract_valuet : public abstract_value_objectt { -private: - typedef sharing_ptrt - constant_abstract_value_pointert; - public: explicit constant_abstract_valuet(const typet &t); + explicit constant_abstract_valuet(const exprt &t); constant_abstract_valuet(const typet &t, bool tp, bool bttm); constant_abstract_valuet( const exprt &e, @@ -39,6 +36,7 @@ class constant_abstract_valuet : public abstract_value_objectt value_range_implementation_ptrt value_range_implementation() const override; exprt to_constant() const override; + constant_interval_exprt to_interval() const override; void output( std::ostream &out, @@ -75,7 +73,7 @@ class constant_abstract_valuet : public abstract_value_objectt abstract_object_pointert merge(abstract_object_pointert other) const override; private: - /// Merges another constant abstract value into this one + /// Merges another abstract value into this one /// /// \param other: the abstract object to merge with /// @@ -83,7 +81,7 @@ class constant_abstract_valuet : public abstract_value_objectt /// unless the merge is the same as this abstract object, in which /// case it returns this. abstract_object_pointert - merge_constant_constant(const constant_abstract_value_pointert &other) const; + merge_constant_constant(const abstract_value_pointert &other) const; exprt value; }; diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 857c9753d46..62f6af5ab81 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -282,6 +282,19 @@ exprt interval_abstract_valuet::to_constant() const #endif } +size_t interval_abstract_valuet::internal_hash() const +{ + return std::hash{}(interval.pretty()); +} + +bool interval_abstract_valuet::internal_equality( + const abstract_object_pointert &other) const +{ + auto cast_other = + std::dynamic_pointer_cast(other); + return cast_other && interval == cast_other->interval; +} + void interval_abstract_valuet::output( std::ostream &out, const ai_baset &ai, @@ -329,8 +342,8 @@ void interval_abstract_valuet::output( abstract_object_pointert interval_abstract_valuet::merge(abstract_object_pointert other) const { - interval_abstract_value_pointert cast_other = - std::dynamic_pointer_cast(other); + abstract_value_pointert cast_other = + std::dynamic_pointer_cast(other); if(cast_other) { return merge_intervals(cast_other); @@ -342,31 +355,31 @@ interval_abstract_valuet::merge(abstract_object_pointert other) const } /// Merge another interval abstract object with this one -/// \param other The interval abstract object to merge with +/// \param other The abstract value object to merge with /// \return This if the other interval is subsumed by this, /// other if this is subsumed by other. /// Otherwise, a new interval abstract object /// with the smallest interval that subsumes both /// this and other -abstract_object_pointert interval_abstract_valuet::merge_intervals( - interval_abstract_value_pointert other) const +abstract_object_pointert +interval_abstract_valuet::merge_intervals(abstract_value_pointert &other) const { - if(is_bottom() || other->interval.contains(interval)) - { - return other; - } - else if(other->is_bottom() || interval.contains(other->interval)) - { + if(other->is_bottom()) return shared_from_this(); - } - else - { - return std::make_shared(constant_interval_exprt( - constant_interval_exprt::get_min( - interval.get_lower(), other->interval.get_lower()), - constant_interval_exprt::get_max( - interval.get_upper(), other->interval.get_upper()))); - } + + auto other_interval = other->to_interval(); + + if(is_bottom()) + return std::make_shared(other_interval); + + if(interval.contains(other_interval)) + return shared_from_this(); + + return std::make_shared(constant_interval_exprt( + constant_interval_exprt::get_min( + interval.get_lower(), other_interval.get_lower()), + constant_interval_exprt::get_max( + interval.get_upper(), other_interval.get_upper()))); } abstract_object_pointert diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 3ed58b18060..e1362475aee 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -41,11 +41,14 @@ class interval_abstract_valuet : public abstract_value_objectt value_range_implementation_ptrt value_range_implementation() const override; exprt to_constant() const override; - const constant_interval_exprt &to_interval() const + constant_interval_exprt to_interval() const override { return interval; } + size_t internal_hash() const override; + bool internal_equality(const abstract_object_pointert &other) const override; + void output( std::ostream &out, const class ai_baset &ai, @@ -68,7 +71,7 @@ class interval_abstract_valuet : public abstract_value_objectt sharing_ptrt; abstract_object_pointert - merge_intervals(interval_abstract_value_pointert other) const; + merge_intervals(abstract_value_pointert &other) const; abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index dbe0472d4a6..b7371f6f006 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -9,6 +9,7 @@ /// \file /// Value Set Abstract Object +#include "interval_abstract_value.h" #include #include #include @@ -162,6 +163,25 @@ value_set_abstract_objectt::value_range_implementation() const return make_value_set_value_range(values); } +exprt value_set_abstract_objectt::to_constant() const +{ + verify(); + + if(values.size() == 1) + return values.first()->to_constant(); + + auto interval = to_interval(); + if(interval.is_single_value_interval()) + return interval.get_lower(); + + return abstract_objectt::to_constant(); +} + +constant_interval_exprt value_set_abstract_objectt::to_interval() const +{ + return values.to_interval(); +} + abstract_object_pointert value_set_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, @@ -199,7 +219,8 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values( if(unwrapped_values.size() > max_value_set_size) { - return unwrapped_values.to_interval(); + return std::make_shared( + unwrapped_values.to_interval()); } //if(unwrapped_values.size() == 1) //{ @@ -215,19 +236,19 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values( abstract_object_pointert value_set_abstract_objectt::merge(abstract_object_pointert other) const { + auto union_values = !is_bottom() ? values : abstract_object_sett{}; + auto other_value_set = std::dynamic_pointer_cast(other); if(other_value_set) { - auto union_values = values; union_values.insert(other_value_set->get_values()); return resolve_values(union_values); } auto other_value = - std::dynamic_pointer_cast(other); + std::dynamic_pointer_cast(other); if(other_value) { - auto union_values = values; union_values.insert(other_value); return resolve_values(union_values); } @@ -254,6 +275,7 @@ void value_set_abstract_objectt::set_values( set_not_top(); values = other_values; } + set_not_bottom(); verify(); } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index a3ed7b81a5d..70ee9679ba7 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -36,12 +36,8 @@ class value_set_abstract_objectt : public abstract_value_objectt, value_range_implementation_ptrt value_range_implementation() const override; /// \copydoc abstract_objectt::to_constant - exprt to_constant() const override - { - verify(); - return values.size() == 1 ? (*values.begin())->to_constant() - : abstract_objectt::to_constant(); - } + exprt to_constant() const override; + constant_interval_exprt to_interval() const override; /// Getter for the set of stored abstract objects. /// \return the values represented by this abstract object diff --git a/unit/Makefile b/unit/Makefile index 7873549e5d9..1ffbe8c1a6e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,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/merge.cpp \ analyses/variable-sensitivity/interval_abstract_value/meet.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index 870fe543db2..4c310b743ce 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -10,102 +10,172 @@ #include +#include +#include #include SCENARIO( - "merge_abstract_object", + "merge abstract object", "[core][analyses][variable-sensitivity][abstract_object][merge]") { - GIVEN("Two abstract objects of type pointer") + GIVEN("merging two abstract objects") { - const typet object_type = signedbv_typet(32); - WHEN("Both are top") + WHEN("merging TOP with TOP") { - abstract_object_pointert op1 = - std::make_shared(object_type, true, false); + abstract_object_pointert op1 = make_top_object(); + abstract_object_pointert op2 = make_top_object(); - abstract_object_pointert op2 = - std::make_shared(object_type, true, false); + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); - bool modifications; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modifications); + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED(result, modified); + EXPECT_TOP(result); + } + } + WHEN("merging TOP with BOTTOM") + { + abstract_object_pointert op1 = make_top_object(); + abstract_object_pointert op2 = make_bottom_object(); + + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); - THEN("The result is the original abstract object") + THEN("result is unmodified TOP") { - // Simple correctness of merge - REQUIRE_FALSE(modifications); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + EXPECT_UNMODIFIED(result, modified); + EXPECT_TOP(result); + } + } + WHEN("merging BOTTOM with TOP") + { + abstract_object_pointert op1 = make_bottom_object(); + abstract_object_pointert op2 = make_top_object(); + + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); - // Is optimal - REQUIRE(op1 == result); + THEN("result is modified TOP") + { + EXPECT_MODIFIED(result, modified); + EXPECT_TOP(result); } } - WHEN("The first is top, the second is bottom") + WHEN("merging BOTTOM with BOTTOM") { - abstract_object_pointert op1 = - std::make_shared(object_type, true, false); + abstract_object_pointert op1 = make_bottom_object(); + abstract_object_pointert op2 = make_bottom_object(); + + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); - abstract_object_pointert op2 = - std::make_shared(object_type, false, true); + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED(result, modified); + EXPECT_BOTTOM(result); + } + } + } - bool modifications; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modifications); + GIVEN("an abstract object and a constant") + { + const typet type = signedbv_typet(32); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + WHEN("merging TOP with 1") + { + auto top1 = make_top_object(); + auto op2 = make_constant(val1, environment, ns); - THEN("The result is the original abstract object") + bool modified; + auto result = abstract_objectt::merge(top1, op2, modified); + + THEN("the result is unmodified TOP") { - // Simple correctness of merge - REQUIRE_FALSE(modifications); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + EXPECT_UNMODIFIED(result, modified); + EXPECT_TOP(result); + } + } + WHEN("merging TOP with TOP constant") + { + auto top1 = make_top_object(); + auto top2 = make_top_constant(); - // Is optimal - REQUIRE(op1 == result); + bool modified; + auto result = abstract_objectt::merge(top1, top2, modified); + + THEN("the result is unmodified TOP") + { + EXPECT_UNMODIFIED(result, modified); + EXPECT_TOP(result); } } - WHEN("The first is bottom and the second is top") + WHEN("merging TOP with BOTTOM constant") { - abstract_object_pointert op1 = - std::make_shared(object_type, false, true); - abstract_object_pointert op2 = - std::make_shared(object_type, true, false); + auto top1 = make_top_object(); + auto bottom2 = make_bottom_constant(); - bool modifications; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modifications); + bool modified; + auto result = abstract_objectt::merge(top1, bottom2, modified); - THEN("The result is top and a new abstract object") + THEN("the result is unmodified TOP") { - // Simple correctness of merge - REQUIRE(modifications); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + EXPECT_UNMODIFIED(result, modified); + EXPECT_TOP(result); + } + } + WHEN("merging BOTTOM with 1") + { + auto op1 = make_bottom_object(); + auto op2 = make_constant(val1, environment, ns); + + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); - REQUIRE_FALSE(op1 == result); + THEN("the result is modified TOP") + { + EXPECT_MODIFIED(result, modified); + EXPECT_TOP(result); } } - WHEN("Both are bottom") + WHEN("merging BOTTOM with TOP constant") { - abstract_object_pointert op1 = - std::make_shared(object_type, false, true); - abstract_object_pointert op2 = - std::make_shared(object_type, false, true); + auto op1 = make_bottom_object(); + auto top2 = make_top_constant(); - bool modifications; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modifications); + bool modified; + auto result = abstract_objectt::merge(op1, top2, modified); - THEN("The result is the original abstract object") + THEN("the result is modified TOP") { - // Simple correctness of merge - REQUIRE_FALSE(modifications); - REQUIRE_FALSE(result->is_top()); - REQUIRE(result->is_bottom()); + EXPECT_MODIFIED(result, modified); + EXPECT_TOP(result); + } + } + WHEN("merging BOTTOM with BOTTOM constant") + { + auto bottom1 = make_bottom_object(); + auto bottom2 = make_bottom_constant(); - // Is optimal - REQUIRE(op1 == result); + bool modified; + auto result = abstract_objectt::merge(bottom1, bottom2, modified); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED(result, modified); + EXPECT_BOTTOM(result); } } } diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 149d112067a..c0ad2a18fd5 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -6,27 +6,14 @@ \*******************************************************************/ -#include -#include -#include #include #include #include -#include -#include -#include -#include -#include -struct constant_merge_result -{ - bool modified; - std::shared_ptr result; -}; +#include -static constant_merge_result merge( - std::shared_ptr op1, - std::shared_ptr op2) +static merge_result +merge(abstract_object_pointert op1, abstract_object_pointert op2) { bool modified; auto result = abstract_objectt::merge(op1, op2, modified); @@ -34,25 +21,19 @@ static constant_merge_result merge( return {modified, as_constant(result)}; } -static abstract_object_pointert make_bottom_object() -{ - return std::make_shared(integer_typet(), false, true); -} - -static abstract_object_pointert make_top_object() -{ - return std::make_shared(integer_typet(), true, false); -} - SCENARIO( - "merge_constant_abstract_value", + "merge constant_abstract_value", "[core][analyses][variable-sensitivity][constant_abstract_value][merge]") { - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); - - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::constant_domain()); + const typet type = signedbv_typet(32); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); symbol_tablet symbol_table; @@ -67,9 +48,9 @@ SCENARIO( auto merged = merge(op1, op2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { - EXPECT_UNMODIFIED(merged.result, merged.modified, val1); + EXPECT_UNMODIFIED(merged, val1); } } WHEN("merging 1 with 2") @@ -79,297 +60,413 @@ SCENARIO( auto merged = merge(op1, op2); - THEN("result should be TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with TOP") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_top_constant(); + auto top2 = make_top_constant(); - auto merged = merge(op1, op2); + auto merged = merge(op1, top2); - THEN("result should be TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with BOTTOM") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_bottom_constant(); + auto bottom2 = make_bottom_constant(); - auto merged = merge(op1, op2); + auto merged = merge(op1, bottom2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { - EXPECT_UNMODIFIED(merged.result, merged.modified, val1); + EXPECT_UNMODIFIED(merged, val1); } } WHEN("merging TOP with 1") { - auto op1 = make_top_constant(); + auto top1 = make_top_constant(); auto op2 = make_constant(val1, environment, ns); - auto merged = merge(op1, op2); + auto merged = merge(top1, op2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging TOP with TOP") { - auto op1 = make_top_constant(); - auto op2 = make_top_constant(); + auto top1 = make_top_constant(); + auto top2 = make_top_constant(); - auto merged = merge(op1, op2); + auto merged = merge(top1, top2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging TOP with BOTTOM") { - auto op1 = make_top_constant(); - auto op2 = make_bottom_constant(); + auto top1 = make_top_constant(); + auto bottom2 = make_bottom_constant(); - auto merged = merge(op1, op2); + auto merged = merge(top1, bottom2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging BOTTOM with 1") { - auto op1 = make_bottom_constant(); + auto bottom1 = make_bottom_constant(); auto op2 = make_constant(val1, environment, ns); - auto merged = merge(op1, op2); + auto merged = merge(bottom1, op2); - THEN("the result is 1") + THEN("result is modified 1") { - EXPECT(merged.result, val1); + EXPECT_MODIFIED(merged, val1); } } WHEN("merging BOTTOM with TOP") { - auto op1 = make_bottom_constant(); - auto op2 = make_top_constant(); + auto bottom1 = make_bottom_constant(); + auto top2 = make_top_constant(); - auto merged = merge(op1, op2); + auto merged = merge(bottom1, top2); - THEN("result should be TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with BOTTOM") { - auto op1 = make_bottom_constant(); - auto op2 = make_bottom_constant(); + auto bottom1 = make_bottom_constant(); + auto bottom2 = make_bottom_constant(); - auto merged = merge(op1, op2); + auto merged = merge(bottom1, bottom2); - THEN("result is BOTTOM") + THEN("result is unmodified BOTTOM") { - EXPECT_BOTTOM(merged.result); + EXPECT_UNMODIFIED_BOTTOM(merged); } } } -} - -SCENARIO( - "merging a constant with an abstract object", - "[core][analyses][variable-sensitivity][constant_abstract_value][merge]") -{ - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); - - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::constant_domain()); - abstract_environmentt environment{object_factory}; - environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); GIVEN("merging a constant and an abstract object") { WHEN("merging 1 with TOP") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_top_object(); + auto top2 = make_top_object(); - auto merged = merge(op1, op2); + auto merged = merge(op1, top2); - THEN("result is TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with BOTTOM") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_bottom_object(); + auto bottom2 = make_bottom_object(); + + auto merged = merge(op1, bottom2); + + THEN("result is unmodified 1") + { + EXPECT_UNMODIFIED(merged, val1); + } + } + WHEN("merging TOP constant with TOP") + { + auto top1 = make_top_constant(); + auto top2 = make_top_object(); + + auto merged = merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP constant with BOTTOM") + { + auto top1 = make_top_constant(); + auto bottom2 = make_bottom_object(); + + auto merged = merge(top1, bottom2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM constant with TOP") + { + auto bottom1 = make_bottom_constant(); + auto top2 = make_top_object(); + + auto merged = merge(bottom1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM constant with BOTTOM") + { + auto bottom1 = make_bottom_constant(); + auto top2 = make_bottom_object(); + + auto merged = merge(bottom1, top2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); + } + } + } + + GIVEN("merging a constant and an interval") + { + WHEN("merging 1 with [1, 1]") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val1, val1, environment, ns); auto merged = merge(op1, op2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { - EXPECT_UNMODIFIED(merged.result, merged.modified, val1); + EXPECT_UNMODIFIED(merged, val1); } } - WHEN("merging constant TOP with TOP") + WHEN("merging 1 with [1, 2]") { - auto op1 = make_top_constant(); - auto op2 = make_top_object(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); auto merged = merge(op1, op2); - THEN("result is TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging constant TOP with BOTTOM") + WHEN("merging 1 with [2, 2]") { - auto op1 = make_top_constant(); - auto op2 = make_bottom_object(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val2, val2, environment, ns); auto merged = merge(op1, op2); - THEN("result is TOP") + THEN("result is modified TOP") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging constant BOTTOM with TOP") + WHEN("merging BOTTOM with [1, 1]") { auto op1 = make_bottom_constant(); - auto op2 = make_top_object(); + auto op2 = make_interval(val1, val1, environment, ns); auto merged = merge(op1, op2); - THEN("result is TOP") + THEN("result is modified 1") { - EXPECT_TOP(merged.result); + EXPECT_MODIFIED(merged, val1); } } - WHEN("merging constant BOTTOM with BOTTOM") + WHEN("merging BOTTOM with [1, 2]") { auto op1 = make_bottom_constant(); - auto op2 = make_bottom_object(); + auto op2 = make_interval(val1, val2, environment, ns); auto merged = merge(op1, op2); - THEN("result is TOP") + THEN("result is modified TOP") { - EXPECT_BOTTOM(merged.result); + EXPECT_MODIFIED_TOP(merged); } } } -} -SCENARIO( - "merging an abstract object with a constant", - "[core][analyses][variable-sensitivity][constant_abstract_value][merge]") -{ - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); + GIVEN("merging a constant and a value set") + { + WHEN("merging 1 with { 1 }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set(val1, environment, ns); - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::constant_domain()); - abstract_environmentt environment{object_factory}; - environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto merged = merge(op1, op2); - GIVEN("an abstract object and a constant") - { - WHEN("merging TOP with 1") + THEN("result is unmodified 1") + { + EXPECT_UNMODIFIED(merged, val1); + } + } + WHEN("merging 1 with { 2 }") { - auto op1 = make_top_object(); - auto op2 = make_constant(val1, environment, ns); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set(val2, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); - THEN("the result is TOP") + THEN("result is modified TOP") { - EXPECT_UNMODIFIED(result, modified); - EXPECT_TOP(result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging TOP with constant TOP") + WHEN("merging 1 with { 1, 2 }") { - auto op1 = make_top_object(); - auto op2 = make_top_constant(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set({val1, val2}, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); - THEN("the result is TOP") + THEN("result is modified TOP") { - EXPECT_UNMODIFIED(result, modified); - EXPECT_TOP(result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging TOP with constant BOTTOM") + WHEN("merging 1 with { [ 1, 1 ] }") { - auto op1 = make_top_object(); - auto op2 = make_bottom_constant(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = + make_value_set(constant_interval_exprt(val1, val1), environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); - THEN("the result is TOP") + THEN("result is unmodified 1") { - EXPECT_UNMODIFIED(result, modified); - EXPECT_TOP(result); + EXPECT_UNMODIFIED(merged, val1); } } - WHEN("merging BOTTOM with 1") + WHEN("merging 1 with { 1, [1, 1] }") { - auto op1 = make_bottom_object(); - auto op2 = make_constant(val1, environment, ns); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set( + {val1, constant_interval_exprt(val1, val1)}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified 1") + { + EXPECT_UNMODIFIED(merged, val1); + } + } + WHEN("merging 1 with { [ 2, 2 ] }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = + make_value_set(constant_interval_exprt(val2, val2), environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); - THEN("the result is TOP") + THEN("result is modified TOP") { - EXPECT_TOP(result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging BOTTOM with constant TOP") + WHEN("merging 1 with { [ 1, 2 ] }") { - auto op1 = make_bottom_object(); - auto op2 = make_top_constant(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = + make_value_set(constant_interval_exprt(val1, val2), environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); - THEN("the result is TOP") + THEN("result is modified TOP") { - EXPECT_TOP(result); + EXPECT_MODIFIED_TOP(merged); } } - WHEN("merging BOTTOM with constant BOTTOM") + WHEN("merging 1 with { 1, [ 1, 2 ] }") { - auto op1 = make_bottom_object(); - auto op2 = make_bottom_constant(); + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set( + {val1, constant_interval_exprt(val1, val2)}, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with { 1 }") + { + auto op1 = make_bottom_constant(); + auto op2 = make_value_set(val1, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified 1") + { + EXPECT_MODIFIED(merged, val1); + } + } + WHEN("merging BOTTOM with { 1, 2 }") + { + auto op1 = make_bottom_constant(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with { [ 1, 1 ] }") + { + auto op1 = make_bottom_constant(); + auto op2 = + make_value_set(constant_interval_exprt(val1, val1), environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified 1") + { + EXPECT_MODIFIED(merged, val1); + } + } + WHEN("merging BOTTOM with { [ 1, 2 ] }") + { + auto op1 = make_bottom_constant(); + auto op2 = + make_value_set(constant_interval_exprt(val1, val2), environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with { 1, [ 1, 2 ] }") + { + auto op1 = make_bottom_constant(); + auto op2 = make_value_set( + {val1, constant_interval_exprt(val1, val2)}, environment, ns); + + auto merged = merge(op1, op2); - THEN("The original AO should be returned") + THEN("result is modified TOP") { - EXPECT_UNMODIFIED(result, modified); - EXPECT_BOTTOM(result); + EXPECT_MODIFIED_TOP(merged); } } } diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp new file mode 100644 index 00000000000..4a8c5a13def --- /dev/null +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -0,0 +1,507 @@ +/*******************************************************************\ + + Module: Unit tests for intervalabstract_valuet::merge + + Author: Jez Higgins. + +\*******************************************************************/ + +#include +#include +#include + +#include + +static merge_result +merge(abstract_object_pointert op1, abstract_object_pointert op2) +{ + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); + + return {modified, as_interval(result)}; +} + +SCENARIO( + "merge interval_abstract_value", + "[core][analyses][variable-sensitivity][interval_abstract_value][merge]") +{ + const typet type = signedbv_typet(32); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + const exprt val3 = from_integer(3, type); + const exprt val4 = from_integer(4, type); + const exprt val5 = from_integer(5, type); + const exprt val6 = from_integer(6, type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("merging two intervals") + { + WHEN("merging [1, 2] with [1, 2]") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 2]") + { + EXPECT_UNMODIFIED(merged, val1, val2); + } + } + WHEN("merging [1, 5] with [2, 3]") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_interval(val2, val3, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [2, 3] with [1, 5]") + { + auto op1 = make_interval(val2, val3, environment, ns); + auto op2 = make_interval(val1, val5, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 5]") + { + EXPECT_MODIFIED(merged, val1, val5); + } + } + WHEN("merging [1, 2] with [4, 5]") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_interval(val4, val5, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 5]") + { + EXPECT_MODIFIED(merged, val1, val5); + } + } + WHEN("merging [4, 5] with [1, 2]") + { + auto op1 = make_interval(val4, val5, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 5]") + { + EXPECT_MODIFIED(merged, val1, val5); + } + } + WHEN("merging [2, 4] with [1, 3]") + { + auto op1 = make_interval(val2, val4, environment, ns); + auto op2 = make_interval(val1, val3, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging [1, 3] with [2, 4]") + { + auto op1 = make_interval(val1, val3, environment, ns); + auto op2 = make_interval(val2, val4, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging [1, 2] with TOP") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto top2 = make_top_interval(); + + auto merged = merge(op1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging [1, 2] with BOTTOM") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto bottom2 = make_bottom_interval(); + + auto merged = merge(op1, bottom2); + + THEN("result is unmodified [1, 2]") + { + EXPECT_UNMODIFIED(merged, val1, val2); + } + } + WHEN("merging TOP with [1, 2]") + { + auto top1 = make_top_interval(); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = merge(top1, op2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with TOP") + { + auto top1 = make_top_interval(); + auto top2 = make_top_interval(); + + auto merged = merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with BOTTOM") + { + auto top1 = make_top_interval(); + auto bottom2 = make_bottom_interval(); + + auto merged = merge(top1, bottom2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with [1, 2]") + { + auto bottom1 = make_bottom_interval(); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = merge(bottom1, op2); + + THEN("result is modified [1, 2]") + { + EXPECT_MODIFIED(merged, val1, val2); + } + } + WHEN("merging BOTTOM with TOP") + { + auto bottom1 = make_bottom_interval(); + auto top2 = make_top_interval(); + + auto merged = merge(bottom1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with BOTTOM") + { + auto bottom1 = make_bottom_interval(); + auto bottom2 = make_bottom_interval(); + + auto merged = merge(bottom1, bottom2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); + } + } + } + + GIVEN("merging an interval and an abstract object") + { + WHEN("merging[1, 2] with TOP") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto top2 = make_top_object(); + + auto merged = merge(op1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging[1, 2] with BOTTOM") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto bottom2 = make_bottom_object(); + + auto merged = merge(op1, bottom2); + + THEN("result is unmodified [1, 2]") + { + EXPECT_UNMODIFIED(merged, val1, val2); + } + } + WHEN("merging TOP interval with TOP") + { + auto top1 = make_top_interval(); + auto top2 = make_top_object(); + + auto merged = merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP interval with BOTTOM") + { + auto top1 = make_top_interval(); + auto bottom2 = make_bottom_object(); + + auto merged = merge(top1, bottom2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM interval with TOP") + { + auto bottom1 = make_bottom_interval(); + auto top2 = make_top_object(); + + auto merged = merge(bottom1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM interval with BOTTOM") + { + auto bottom1 = make_bottom_interval(); + auto top2 = make_bottom_object(); + + auto merged = merge(bottom1, top2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); + } + } + } + + GIVEN("merging an interval and a constant") + { + WHEN("merging [1, 5] with 1") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_constant(val1, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [1, 5] with 3") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_constant(val3, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [1, 5] with 5") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_constant(val5, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [3, 4] with 6") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_constant(val6, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 6]") + { + EXPECT_MODIFIED(merged, val3, val6); + } + } + WHEN("merging [3, 4] with 1") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_constant(val1, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging BOTTOM with 3") + { + auto op1 = make_bottom_interval(); + auto op2 = make_constant(val3, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 3]") + { + EXPECT_MODIFIED(merged, val3, val3); + } + } + } + + GIVEN("merging an interval and a value_set") + { + WHEN("merging [1, 5] with { 1, 3, 5 }") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_value_set({val1, val3, val5}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [1, 5] with { 3 }") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_value_set({val3}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + WHEN("merging [3, 4] with { 6 }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_value_set({val6}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 6]") + { + EXPECT_MODIFIED(merged, val3, val6); + } + } + WHEN("merging [3, 4] with { 4, 6 }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_value_set({val4, val6}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 6]") + { + EXPECT_MODIFIED(merged, val3, val6); + } + } + WHEN("merging [3, 4] with { 1 }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_value_set({val1}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging [3, 4] with { 1, 3 }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_value_set({val1, val3}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging [3, 4] with { [4, 6] }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = + make_value_set({constant_interval_exprt(val4, val6)}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 6]") + { + EXPECT_MODIFIED(merged, val3, val6); + } + } + WHEN("merging [3, 4] with { 1, [3, 3] }") + { + auto op1 = make_interval(val3, val4, environment, ns); + auto op2 = make_value_set( + {val1, constant_interval_exprt(val3, val3)}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 4]") + { + EXPECT_MODIFIED(merged, val1, val4); + } + } + WHEN("merging BOTTOM with { 3 }") + { + auto op1 = make_bottom_interval(); + auto op2 = make_value_set({val3}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [3, 3]") + { + EXPECT_MODIFIED(merged, val3, val3); + } + } + WHEN("merging BOTTOM with { 1, 3, 6 }") + { + auto op1 = make_bottom_interval(); + auto op2 = make_value_set({val1, val3, val6}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified [1, 6]") + { + EXPECT_MODIFIED(merged, val1, val6); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/module_dependencies.txt b/unit/analyses/variable-sensitivity/interval_abstract_value/module_dependencies.txt index f4c536408fa..2375189ecd5 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/module_dependencies.txt +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/module_dependencies.txt @@ -1,3 +1,4 @@ analyses testing-utils +util diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index 2b8803ed156..38525d59083 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -6,17 +6,17 @@ \*******************************************************************/ -#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h" #include +#include #include #include #include SCENARIO( - "constants expression evaluation", + "value expression evaluation", "[core][analyses][variable-sensitivity][constant_abstract_value][value_set_" - "abstract_object][expression_transform]") + "abstract_object][interval_abstract_value][expression_transform]") { const typet type = signedbv_typet(32); const exprt val1 = from_integer(1, type); @@ -595,9 +595,9 @@ SCENARIO( auto op2 = make_value_set({interval12, val1}, environment, ns); auto result = add_as_value_set(op1, op2, environment, ns); - THEN("= { [2,4], [2,3], [2,3], 2 }") - { // duplicate interval ok as first pass. Will be eliminated in due course. - EXPECT(result, {interval24, interval23, interval23, val2}); + THEN("= { [2,4], [2,3], 2 }") + { + EXPECT(result, {interval24, interval23, val2}); } } } diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/module_dependencies.txt b/unit/analyses/variable-sensitivity/value_expression_evaluation/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index bce312fcad7..9c0f9be9c5a 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -16,239 +16,384 @@ #include #include +static merge_result +merge(abstract_object_pointert op1, abstract_object_pointert op2) +{ + bool modified; + auto result = abstract_objectt::merge(op1, op2, modified); + + return {modified, as_value_set(result)}; +} + SCENARIO( - "merging two value_set_abstract_objects", + "merging value sets", "[core][analyses][variable-sensitivity][value_set_abstract_object][merge]") { - GIVEN("Two value sets") + const typet type = signedbv_typet(32); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + const exprt val3 = from_integer(3, type); + const exprt val4 = from_integer(4, type); + const exprt val5 = from_integer(5, type); + const exprt val6 = from_integer(6, type); + + auto object_factory = variable_sensitivity_object_factoryt::configured_with( + vsd_configt::value_set()); + auto environment = abstract_environmentt{object_factory}; + environment.make_top(); + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + GIVEN("merging two value sets") { - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); - const exprt val3 = from_integer(3, integer_typet()); - const exprt val4 = from_integer(4, integer_typet()); - - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::value_set()); - auto environment = abstract_environmentt{object_factory}; - environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; - WHEN("merging { 1 } with { 1 }") { auto op1 = make_value_set(val1, environment, ns); auto op2 = make_value_set(val1, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); - - THEN("the result { 1 } is unchanged ") + THEN("result is unmodified { 1 }") { - EXPECT_UNMODIFIED(value_set_result, modified, {val1}); + EXPECT_UNMODIFIED(result, {val1}); } } - WHEN("merging { 1 } with { 2 }") { auto op1 = make_value_set(val1, environment, ns); auto op2 = make_value_set(val2, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); - - THEN("the result is { 1, 2 }") + THEN("result is modified { 1, 2 }") { - EXPECT(value_set_result, {val1, val2}); + EXPECT_MODIFIED(result, {val1, val2}); } } - WHEN("merging { 1, 2 } with { 2 }") { auto op1 = make_value_set({val1, val2}, environment, ns); auto op2 = make_value_set(val2, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); - - THEN("the result { 1, 2 } is unchanged") + THEN("result unmodified { 1, 2 }") { - EXPECT_UNMODIFIED(value_set_result, modified, {val1, val2}); + EXPECT_UNMODIFIED(result, {val1, val2}); } } - WHEN("merging { 1, 2 } with { 3, 4 }") { auto op1 = make_value_set({val1, val2}, environment, ns); auto op2 = make_value_set({val3, val4}, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); - - auto value_set_result = as_value_set(result); + auto result = merge(op1, op2); - THEN("the result is { 1, 2, 3, 4 }") + THEN("result is modified { 1, 2, 3, 4 }") { - EXPECT(value_set_result, {val1, val2, val3, val4}); + EXPECT_MODIFIED(result, {val1, val2, val3, val4}); } } - WHEN("merging { 1, 2, 3 } with { 1, 3, 4 }") { auto op1 = make_value_set({val1, val2, val3}, environment, ns); auto op2 = make_value_set({val1, val3, val4}, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); + THEN("result is modified { 1, 2, 3, 4 }") + { + EXPECT_MODIFIED(result, {val1, val2, val3, val4}); + } + } + WHEN("merging {1, 2} with TOP") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto top2 = make_top_value_set(); - THEN("the result is { 1, 2, 3, 4 }") + auto merged = merge(op1, top2); + + THEN("result is modified TOP") { - EXPECT(value_set_result, {val1, val2, val3, val4}); + EXPECT_MODIFIED_TOP(merged); } } - } -} + WHEN("merging {1, 2} with BOTTOM") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto bottom2 = make_bottom_value_set(); -SCENARIO( - "merging a value_set with a constant", - "[core][analyses][variable-sensitivity][value_set_abstract_object][merge]") -{ - GIVEN("A value set and a constant") - { - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); - const exprt val3 = from_integer(3, integer_typet()); - const exprt val4 = from_integer(4, integer_typet()); - - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::value_set()); - auto environment = abstract_environmentt{object_factory}; - environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto merged = merge(op1, bottom2); - WHEN("merging { 1 } with 1") + THEN("result is unmodified {1, 2}") + { + EXPECT_UNMODIFIED(merged, {val1, val2}); + } + } + WHEN("merging TOP with {1, 2}") { - auto op1 = make_value_set(val1, environment, ns); - auto op2 = make_constant(val1, environment, ns); + auto top1 = make_top_value_set(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = merge(top1, op2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with TOP") + { + auto top1 = make_top_value_set(); + auto top2 = make_top_value_set(); + + auto merged = merge(top1, top2); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with BOTTOM") + { + auto top1 = make_top_value_set(); + auto bottom2 = make_bottom_value_set(); - auto value_set_result = as_value_set(result); + auto merged = merge(top1, bottom2); - THEN("the result { 1 } is unchanged ") + THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(value_set_result, modified, {val1}); + EXPECT_UNMODIFIED_TOP(merged); } } + WHEN("merging BOTTOM with {1, 2}") + { + auto bottom1 = make_bottom_value_set(); + auto op2 = make_value_set({val1, val2}, environment, ns); - WHEN("merging { 1 } with 2") + auto merged = merge(bottom1, op2); + + THEN("result is modified {1, 2}") + { + EXPECT_MODIFIED(merged, {val1, val2}); + } + } + WHEN("merging BOTTOM with TOP") { - auto op1 = make_value_set(val1, environment, ns); - auto op2 = make_constant(val2, environment, ns); + auto bottom1 = make_bottom_value_set(); + auto top2 = make_top_value_set(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(bottom1, top2); - auto value_set_result = as_value_set(result); + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with BOTTOM") + { + auto bottom1 = make_bottom_value_set(); + auto bottom2 = make_bottom_value_set(); - THEN("the result is { 1, 2 }") + auto merged = merge(bottom1, bottom2); + + THEN("result is unmodified BOTTOM") { - EXPECT(value_set_result, {val1, val2}); + EXPECT_UNMODIFIED_BOTTOM(merged); } } + } - WHEN("merging { 1, 2 } with 2") + GIVEN("merging a value_set and an abstract object") + { + WHEN("merging {1, 2} with TOP") { auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = make_constant(val2, environment, ns); + auto top2 = make_top_object(); + + auto merged = merge(op1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging {1, 2} with BOTTOM") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto bottom2 = make_bottom_object(); + + auto merged = merge(op1, bottom2); + + THEN("result is unmodified {1, 2}") + { + EXPECT_UNMODIFIED(merged, {val1, val2}); + } + } + WHEN("merging TOP value set with TOP") + { + auto top1 = make_top_value_set(); + auto top2 = make_top_object(); + + auto merged = merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP value set with BOTTOM") + { + auto top1 = make_top_value_set(); + auto bottom2 = make_bottom_object(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto merged = merge(top1, bottom2); - auto value_set_result = as_value_set(result); + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM value set with TOP") + { + auto bottom1 = make_bottom_value_set(); + auto top2 = make_top_object(); + + auto merged = merge(bottom1, top2); - THEN("the result { 1, 2 } is unchanged") + THEN("result is modified TOP") { - EXPECT_UNMODIFIED(value_set_result, modified, {val1, val2}); + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM value set with BOTTOM") + { + auto bottom1 = make_bottom_value_set(); + auto top2 = make_bottom_object(); + + auto merged = merge(bottom1, top2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); } } } -} -SCENARIO( - "merging a value_set with a TOP value", - "[core][analyses][variable-sensitivity][value_set_abstract_object][merge]") -{ - GIVEN("A value set and a TOP constant") + GIVEN("merging a value set and a constant") { - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); + WHEN("merging { 1 } with 1") + { + auto op1 = make_value_set(val1, environment, ns); + auto op2 = make_constant(val1, environment, ns); - auto object_factory = variable_sensitivity_object_factoryt::configured_with( - vsd_configt::value_set()); - auto environment = abstract_environmentt{object_factory}; - environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto result = merge(op1, op2); - WHEN("merging { 1, 2 } with TOP constant") + THEN("result unmodified { 1 }") + { + EXPECT_UNMODIFIED(result, {val1}); + } + } + WHEN("merging { 1 } with 2") { - auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = std::make_shared(val1.type()); - REQUIRE(op2->is_top()); + auto op1 = make_value_set(val1, environment, ns); + auto op2 = make_constant(val2, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); + THEN("result is modified { 1, 2 }") + { + EXPECT_MODIFIED(result, {val1, val2}); + } + } + WHEN("merging { 1, 2, 3 } with 2") + { + auto op1 = make_value_set({val1, val2, val3}, environment, ns); + auto op2 = make_constant(val2, environment, ns); + + auto result = merge(op1, op2); - THEN("the result is top") + THEN("result is unmodified { 1, 2, 3 }") { - EXPECT_TOP(value_set_result); + EXPECT_UNMODIFIED(result, {val1, val2, val3}); } } + WHEN("merging { 1, 3 } with 2") + { + auto op1 = make_value_set({val1, val3}, environment, ns); + auto op2 = make_constant(val2, environment, ns); - WHEN("merging { 1, 2 } with TOP interval") + auto result = merge(op1, op2); + + THEN("result is modified { 1, 2, 3 }") + { + EXPECT_MODIFIED(result, {val1, val2, val3}); + } + } + WHEN("merging BOTTOM with 2") { - auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = - std::make_shared(unsignedbv_typet(32)); - REQUIRE(op2->is_top()); + auto op1 = make_bottom_value_set(); + auto op2 = make_constant(val2, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = merge(op1, op2); - auto value_set_result = as_value_set(result); + THEN("result is modified { 2 }") + { + EXPECT_MODIFIED(result, {val2}); + } + } + } + + GIVEN("merging a value_set and an interval") + { + auto interval_1_5 = constant_interval_exprt(val1, val5); + + WHEN("merging { 1, 2, 3 } with [1, 5]") + { + auto op1 = make_value_set({val1, val3, val5}, environment, ns); + auto op2 = make_interval(val1, val5, environment, ns); - THEN("the result is top") + auto merged = merge(op1, op2); + + THEN("result is modified { 1, 3, 5, [1, 5]}") { - EXPECT_TOP(value_set_result); + EXPECT_MODIFIED(merged, {val1, val3, val5, interval_1_5}); } } + WHEN("merging { [1, 5] } with [1, 5]") + { + auto op1 = make_value_set(interval_1_5, environment, ns); + auto op2 = make_interval(val1, val5, environment, ns); - WHEN("merging { 1, 2 } with TOP value-set") + auto merged = merge(op1, op2); + + THEN("result is unmodified {[1, 5]}") + { + EXPECT_UNMODIFIED(merged, {interval_1_5}); + } + } + WHEN("merging { 1, 2, [1, 5] } with [1, 5]") { - auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = std::make_shared(val1.type()); - REQUIRE(op2->is_top()); + auto op1 = make_value_set({val1, val2, interval_1_5}, environment, ns); + auto op2 = make_interval(val1, val5, environment, ns); + + auto merged = merge(op1, op2); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + THEN("result is unmodified { 1, 2, [1, 5]}") + { + EXPECT_UNMODIFIED(merged, {val1, val2, interval_1_5}); + } + } + WHEN("merging BOTTOM with [1, 5]") + { + auto op1 = make_bottom_value_set(); + auto op2 = make_interval(val1, val5, environment, ns); - auto value_set_result = as_value_set(result); + auto merged = merge(op1, op2); - THEN("the result is top") + THEN("result is modified {[1, 5]}") { - EXPECT_TOP(value_set_result); + EXPECT_MODIFIED(merged, {interval_1_5}); } } } diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/module_dependencies.txt b/unit/analyses/variable-sensitivity/value_set_abstract_object/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 52b7543b877..cf770c677ad 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -60,6 +60,12 @@ std::shared_ptr make_top_interval() signedbv_typet(32), true, false); } +std::shared_ptr make_bottom_interval() +{ + return std::make_shared( + signedbv_typet(32), false, true); +} + std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns) { @@ -86,11 +92,27 @@ std::shared_ptr make_value_set( return vs; } +std::shared_ptr make_bottom_value_set() +{ + return std::make_shared( + integer_typet(), false, true); +} + std::shared_ptr make_top_value_set() { return std::make_shared(integer_typet()); } +abstract_object_pointert make_bottom_object() +{ + return std::make_shared(integer_typet(), false, true); +} + +abstract_object_pointert make_top_object() +{ + return std::make_shared(integer_typet(), true, false); +} + std::shared_ptr as_constant(const abstract_object_pointert &aop) { @@ -258,6 +280,13 @@ void EXPECT_UNMODIFIED( CHECK_FALSE(modified); } +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified) +{ + CHECK(modified); +} + void EXPECT_UNMODIFIED( std::shared_ptr &result, bool modified, @@ -267,6 +296,31 @@ void EXPECT_UNMODIFIED( EXPECT(result, expected_value); } +void EXPECT_UNMODIFIED( + merge_result &result, + exprt expected_value) +{ + EXPECT_UNMODIFIED(result.result, result.modified, expected_value); +} + +void EXPECT_UNMODIFIED( + std::shared_ptr &result, + bool modified, + exprt lower_value, + exprt upper_value) +{ + CHECK_FALSE(modified); + EXPECT(result, lower_value, upper_value); +} + +void EXPECT_UNMODIFIED( + merge_result &result, + exprt lower_value, + exprt upper_value) +{ + EXPECT_UNMODIFIED(result.result, result.modified, lower_value, upper_value); +} + void EXPECT_UNMODIFIED( std::shared_ptr &result, bool modified, @@ -276,6 +330,63 @@ void EXPECT_UNMODIFIED( EXPECT(result, expected_values); } +void EXPECT_UNMODIFIED( + merge_result &result, + const std::vector &expected_values) +{ + EXPECT_UNMODIFIED(result.result, result.modified, expected_values); +} + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified, + exprt expected_value) +{ + CHECK(modified); + EXPECT(result, expected_value); +} + +void EXPECT_MODIFIED( + merge_result &result, + exprt expected_value) +{ + EXPECT_MODIFIED(result.result, result.modified, expected_value); +} + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified, + exprt lower_value, + exprt upper_value) +{ + CHECK(modified); + EXPECT(result, lower_value, upper_value); +} + +void EXPECT_MODIFIED( + merge_result &result, + exprt lower_value, + exprt upper_value) +{ + EXPECT_MODIFIED(result.result, result.modified, lower_value, upper_value); +} + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified, + const std::vector &expected_values) +{ + CHECK(modified); + EXPECT(result, expected_values); +} + +void EXPECT_MODIFIED( + merge_result &result, + const std::vector &expected_values) +{ + EXPECT_MODIFIED(result.result, result.modified, expected_values); +} + void EXPECT_TOP(std::shared_ptr result) { REQUIRE(result); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 570f1ad07e1..be214a96bbc 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -6,6 +6,9 @@ \*******************************************************************/ +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_TEST_HELPERS_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_TEST_HELPERS_H + #include #include #include @@ -26,6 +29,7 @@ std::shared_ptr make_interval( abstract_environmentt &env, namespacet &ns); std::shared_ptr make_top_interval(); +std::shared_ptr make_bottom_interval(); std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); @@ -35,8 +39,12 @@ std::shared_ptr make_value_set( abstract_environmentt &env, namespacet &ns); +std::shared_ptr make_bottom_value_set(); std::shared_ptr make_top_value_set(); +abstract_object_pointert make_bottom_object(); +abstract_object_pointert make_top_object(); + std::shared_ptr as_constant(const abstract_object_pointert &aop); @@ -71,20 +79,117 @@ void EXPECT_TOP(std::shared_ptr &result); void EXPECT_BOTTOM(std::shared_ptr result); +template +struct merge_result +{ + bool modified; + std::shared_ptr result; +}; + void EXPECT_UNMODIFIED( std::shared_ptr &result, bool modified); +template +void EXPECT_UNMODIFIED(merge_result &result) +{ + auto ao = std::dynamic_pointer_cast(result.result); + EXPECT_UNMODIFIED(ao, result.modified); +} + +template +void EXPECT_UNMODIFIED_TOP(merge_result &result) +{ + auto ao = std::dynamic_pointer_cast(result.result); + EXPECT_UNMODIFIED(ao, result.modified); + EXPECT_TOP(result.result); +} + +template +void EXPECT_UNMODIFIED_BOTTOM(merge_result &result) +{ + auto ao = std::dynamic_pointer_cast(result.result); + EXPECT_UNMODIFIED(ao, result.modified); + EXPECT_BOTTOM(result.result); +} + +template +void EXPECT_MODIFIED_TOP(merge_result &result) +{ + auto ao = std::dynamic_pointer_cast(result.result); + EXPECT_MODIFIED(ao, result.modified); + EXPECT_TOP(result.result); +} + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified); + +template +void EXPECT_MODIFIED(merge_result &result) +{ + auto ao = std::dynamic_pointer_cast(result.result); + EXPECT_MODIFIED(ao, result.modified); +} + void EXPECT_UNMODIFIED( std::shared_ptr &result, bool modified, exprt expected_value); void EXPECT_UNMODIFIED( + merge_result &result, + exprt expected_value); + +void EXPECT_UNMODIFIED( + std::shared_ptr &result, + bool modified, + exprt lower_value, + exprt upper_value); + +void EXPECT_UNMODIFIED( + merge_result &result, + exprt lower_value, + exprt upper_value); + +void EXPECT_UNMODIFIED( + std::shared_ptr &result, + bool modified, + const std::vector &expected_values); + +void EXPECT_UNMODIFIED( + merge_result &result, + const std::vector &expected_values); + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified, + exprt expected_value); + +void EXPECT_MODIFIED( + merge_result &result, + exprt expected_value); + +void EXPECT_MODIFIED( + std::shared_ptr &result, + bool modified, + exprt lower_value, + exprt upper_value); + +void EXPECT_MODIFIED( + merge_result &result, + exprt lower_value, + exprt upper_value); + +void EXPECT_MODIFIED( std::shared_ptr &result, bool modified, const std::vector &expected_values); +void EXPECT_MODIFIED( + merge_result &result, + const std::vector &expected_values); + std::shared_ptr add( const abstract_object_pointert &op1, const abstract_object_pointert &op2, @@ -114,3 +219,5 @@ std::shared_ptr add_as_value_set( const abstract_object_pointert &op3, abstract_environmentt &environment, namespacet &ns); + +#endif