From df46cbe88ba6383840dcf46946bd118cc393e15d Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 20 Mar 2021 15:38:57 +0000 Subject: [PATCH 1/7] constant_abstract_value merge test tidy-up --- .../constant_abstract_value/merge.cpp | 198 +++++++++--------- .../expression_evaluation.cpp | 6 +- .../variable_sensitivity_test_helpers.cpp | 56 +++++ .../variable_sensitivity_test_helpers.h | 36 ++++ 4 files changed, 189 insertions(+), 107 deletions(-) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 149d112067a..b2169a6d697 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; @@ -69,7 +50,7 @@ SCENARIO( THEN("the result 1 is unchanged") { - EXPECT_UNMODIFIED(merged.result, merged.modified, val1); + EXPECT_UNMODIFIED(merged, val1); } } WHEN("merging 1 with 2") @@ -87,9 +68,9 @@ SCENARIO( 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") { @@ -99,21 +80,21 @@ SCENARIO( 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") { - 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") { @@ -122,10 +103,10 @@ SCENARIO( } 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") { @@ -134,10 +115,10 @@ SCENARIO( } 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") { @@ -146,22 +127,22 @@ SCENARIO( } 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") { - 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") { @@ -170,13 +151,14 @@ SCENARIO( } 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") { + CHECK_FALSE(merged.modified); EXPECT_BOTTOM(merged.result); } } @@ -184,14 +166,18 @@ SCENARIO( } SCENARIO( - "merging a constant with an abstract object", + "merge constant_abstract_value 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()); + 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; @@ -202,9 +188,9 @@ SCENARIO( 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") { @@ -214,57 +200,57 @@ SCENARIO( 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, op2); + auto merged = merge(op1, bottom2); THEN("the result 1 is unchanged") { - EXPECT_UNMODIFIED(merged.result, merged.modified, val1); + EXPECT_UNMODIFIED(merged, val1); } } - WHEN("merging constant TOP with TOP") + WHEN("merging TOP constant with TOP") { - auto op1 = make_top_constant(); - auto op2 = make_top_object(); + auto top1 = make_top_constant(); + auto top2 = make_top_object(); - auto merged = merge(op1, op2); + auto merged = merge(top1, top2); THEN("result is TOP") { EXPECT_TOP(merged.result); } } - WHEN("merging constant TOP with BOTTOM") + WHEN("merging TOP constant with BOTTOM") { - auto op1 = make_top_constant(); - auto op2 = make_bottom_object(); + auto top1 = make_top_constant(); + auto bottom2 = make_bottom_object(); - auto merged = merge(op1, op2); + auto merged = merge(top1, bottom2); THEN("result is TOP") { EXPECT_TOP(merged.result); } } - WHEN("merging constant BOTTOM with TOP") + WHEN("merging BOTTOM constant with TOP") { - auto op1 = make_bottom_constant(); - auto op2 = make_top_object(); + auto bottom1 = make_bottom_constant(); + auto top2 = make_top_object(); - auto merged = merge(op1, op2); + auto merged = merge(bottom1, top2); THEN("result is TOP") { EXPECT_TOP(merged.result); } } - WHEN("merging constant BOTTOM with BOTTOM") + WHEN("merging BOTTOM constant with BOTTOM") { - auto op1 = make_bottom_constant(); - auto op2 = make_bottom_object(); + auto bottom1 = make_bottom_constant(); + auto top2 = make_bottom_object(); - auto merged = merge(op1, op2); + auto merged = merge(bottom1, top2); THEN("result is TOP") { @@ -278,11 +264,15 @@ 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()); - - 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; @@ -292,11 +282,11 @@ SCENARIO( { WHEN("merging TOP with 1") { - auto op1 = make_top_object(); + auto top1 = make_top_object(); auto op2 = make_constant(val1, environment, ns); bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(top1, op2, modified); THEN("the result is TOP") { @@ -304,13 +294,13 @@ SCENARIO( EXPECT_TOP(result); } } - WHEN("merging TOP with constant TOP") + WHEN("merging TOP with TOP constant") { - auto op1 = make_top_object(); - auto op2 = make_top_constant(); + auto top1 = make_top_object(); + auto top2 = make_top_constant(); bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(top1, top2, modified); THEN("the result is TOP") { @@ -318,13 +308,13 @@ SCENARIO( EXPECT_TOP(result); } } - WHEN("merging TOP with constant BOTTOM") + WHEN("merging TOP with BOTTOM constant") { - auto op1 = make_top_object(); - auto op2 = make_bottom_constant(); + auto top1 = make_top_object(); + auto bottom2 = make_bottom_constant(); bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(top1, bottom2, modified); THEN("the result is TOP") { @@ -345,26 +335,26 @@ SCENARIO( EXPECT_TOP(result); } } - WHEN("merging BOTTOM with constant TOP") + WHEN("merging BOTTOM with TOP constant") { auto op1 = make_bottom_object(); - auto op2 = make_top_constant(); + auto top2 = make_top_constant(); bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, top2, modified); THEN("the result is TOP") { EXPECT_TOP(result); } } - WHEN("merging BOTTOM with constant BOTTOM") + WHEN("merging BOTTOM with BOTTOM constant") { - auto op1 = make_bottom_object(); - auto op2 = make_bottom_constant(); + auto bottom1 = make_bottom_object(); + auto bottom2 = make_bottom_constant(); bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(bottom1, bottom2, modified); THEN("The original AO should be returned") { 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..9ec820d0c16 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); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 52b7543b877..6e581c99276 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -91,6 +91,16 @@ 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) { @@ -267,6 +277,13 @@ 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, @@ -276,6 +293,45 @@ 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, + 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..08aec4f082a 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -37,6 +37,9 @@ std::shared_ptr make_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,6 +74,13 @@ 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); @@ -81,10 +91,36 @@ void EXPECT_UNMODIFIED( exprt expected_value); void EXPECT_UNMODIFIED( + merge_result &result, + exprt expected_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, 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, From c9abd82c619ec48a2786c971a25c839a36bbcd79 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 20 Mar 2021 16:04:27 +0000 Subject: [PATCH 2/7] Tidying work on abstact_objectt and constant_abstract_valuet merge tests Combine related scenarios. Use consistent language in THEN clauses. Use consistent expectations. --- .../abstract_object/merge.cpp | 194 ++++++++++++------ .../constant_abstract_value/merge.cpp | 168 +++------------ .../variable_sensitivity_test_helpers.cpp | 7 + .../variable_sensitivity_test_helpers.h | 18 ++ 4 files changed, 185 insertions(+), 202 deletions(-) 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 b2169a6d697..e7e307f817d 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -48,7 +48,7 @@ SCENARIO( auto merged = merge(op1, op2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { EXPECT_UNMODIFIED(merged, val1); } @@ -60,8 +60,9 @@ SCENARIO( auto merged = merge(op1, op2); - THEN("result should be TOP") + THEN("result is modified TOP") { + EXPECT_MODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -72,8 +73,9 @@ SCENARIO( auto merged = merge(op1, top2); - THEN("result should be TOP") + THEN("result is modified TOP") { + EXPECT_MODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -84,7 +86,7 @@ SCENARIO( auto merged = merge(op1, bottom2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { EXPECT_UNMODIFIED(merged, val1); } @@ -96,8 +98,9 @@ SCENARIO( auto merged = merge(top1, op2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { + EXPECT_UNMODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -108,8 +111,9 @@ SCENARIO( auto merged = merge(top1, top2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { + EXPECT_UNMODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -120,8 +124,9 @@ SCENARIO( auto merged = merge(top1, bottom2); - THEN("result should be TOP") + THEN("result is unmodified TOP") { + EXPECT_UNMODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -132,7 +137,7 @@ SCENARIO( auto merged = merge(bottom1, op2); - THEN("the result is 1") + THEN("result is modified 1") { EXPECT_MODIFIED(merged, val1); } @@ -144,8 +149,9 @@ SCENARIO( auto merged = merge(bottom1, top2); - THEN("result should be TOP") + THEN("result is modified TOP") { + EXPECT_MODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -156,32 +162,13 @@ SCENARIO( auto merged = merge(bottom1, bottom2); - THEN("result is BOTTOM") + THEN("result is unmodified BOTTOM") { - CHECK_FALSE(merged.modified); + EXPECT_UNMODIFIED(merged); EXPECT_BOTTOM(merged.result); } } } -} - -SCENARIO( - "merge constant_abstract_value with an abstract object", - "[core][analyses][variable-sensitivity][constant_abstract_value][merge]") -{ - 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); GIVEN("merging a constant and an abstract object") { @@ -192,8 +179,9 @@ SCENARIO( auto merged = merge(op1, top2); - THEN("result is TOP") + THEN("result is modified TOP") { + EXPECT_MODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -204,7 +192,7 @@ SCENARIO( auto merged = merge(op1, bottom2); - THEN("the result 1 is unchanged") + THEN("result is unmodified 1") { EXPECT_UNMODIFIED(merged, val1); } @@ -216,8 +204,9 @@ SCENARIO( auto merged = merge(top1, top2); - THEN("result is TOP") + THEN("result is unmodified TOP") { + EXPECT_UNMODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -228,8 +217,9 @@ SCENARIO( auto merged = merge(top1, bottom2); - THEN("result is TOP") + THEN("result is unmodified TOP") { + EXPECT_UNMODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -240,8 +230,9 @@ SCENARIO( auto merged = merge(bottom1, top2); - THEN("result is TOP") + THEN("result is modified TOP") { + EXPECT_MODIFIED(merged); EXPECT_TOP(merged.result); } } @@ -252,115 +243,12 @@ SCENARIO( auto merged = merge(bottom1, top2); - THEN("result is TOP") + THEN("result is unmodified BOTTOM") { + EXPECT_UNMODIFIED(merged); EXPECT_BOTTOM(merged.result); } } } } -SCENARIO( - "merging an abstract object with a constant", - "[core][analyses][variable-sensitivity][constant_abstract_value][merge]") -{ - 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); - - GIVEN("an abstract object and a constant") - { - WHEN("merging TOP with 1") - { - auto top1 = make_top_object(); - auto op2 = make_constant(val1, environment, ns); - - bool modified; - auto result = abstract_objectt::merge(top1, op2, modified); - - THEN("the result is TOP") - { - EXPECT_UNMODIFIED(result, modified); - EXPECT_TOP(result); - } - } - WHEN("merging TOP with TOP constant") - { - auto top1 = make_top_object(); - auto top2 = make_top_constant(); - - bool modified; - auto result = abstract_objectt::merge(top1, top2, modified); - - THEN("the result is TOP") - { - EXPECT_UNMODIFIED(result, modified); - EXPECT_TOP(result); - } - } - WHEN("merging TOP with BOTTOM constant") - { - auto top1 = make_top_object(); - auto bottom2 = make_bottom_constant(); - - bool modified; - auto result = abstract_objectt::merge(top1, bottom2, modified); - - THEN("the result is TOP") - { - 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); - - THEN("the result is TOP") - { - EXPECT_TOP(result); - } - } - WHEN("merging BOTTOM with TOP constant") - { - auto op1 = make_bottom_object(); - auto top2 = make_top_constant(); - - bool modified; - auto result = abstract_objectt::merge(op1, top2, modified); - - THEN("the result is TOP") - { - EXPECT_TOP(result); - } - } - WHEN("merging BOTTOM with BOTTOM constant") - { - auto bottom1 = make_bottom_object(); - auto bottom2 = make_bottom_constant(); - - bool modified; - auto result = abstract_objectt::merge(bottom1, bottom2, modified); - - THEN("The original AO should be returned") - { - EXPECT_UNMODIFIED(result, modified); - EXPECT_BOTTOM(result); - } - } - } -} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 6e581c99276..e90599d5831 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -268,6 +268,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, diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 08aec4f082a..0fd98074d15 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -85,6 +85,24 @@ 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); +} + +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, From 6d3c463d57d8b7307f6494f0a25a0b4321f16cd4 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 20 Mar 2021 16:38:25 +0000 Subject: [PATCH 3/7] Extend constant_abstract_valuet to merge with other value representations Can successfully merge with matching intervals and value sets, including from bottom. Goes TOP otherwise. --- .../abstract_value_object.h | 2 + .../constant_abstract_value.cpp | 44 ++-- .../constant_abstract_value.h | 9 +- .../constant_abstract_value/merge.cpp | 231 +++++++++++++++++- 4 files changed, 253 insertions(+), 33 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 65f9ca690e2..29adcb7104b 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -291,4 +291,6 @@ class abstract_value_objectt : public abstract_objectt, value_range_implementation() const = 0; }; +using abstract_value_pointert = sharing_ptrt; + #endif \ No newline at end of file diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index a5d490c3aec..00576ff0d88 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, @@ -104,38 +109,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..d2e7de61da7 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, @@ -75,7 +72,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 +80,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/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index e7e307f817d..cf8e65fe8cc 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -250,5 +250,234 @@ SCENARIO( } } } -} + 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("result is unmodified 1") + { + EXPECT_UNMODIFIED(merged, val1); + } + } + WHEN("merging 1 with [1, 2]") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging 1 with [2, 2]") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val2, val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging BOTTOM with [1, 1]") + { + auto op1 = make_bottom_constant(); + auto op2 = make_interval(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_interval(val1, val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + } + + 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 merged = merge(op1, op2); + + THEN("result is unmodified 1") + { + EXPECT_UNMODIFIED(merged, val1); + } + } + WHEN("merging 1 with { 2 }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set(val2, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging 1 with { 1, 2 }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging 1 with { [ 1, 1 ] }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = + make_value_set(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); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging 1 with { [ 1, 2 ] }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = + make_value_set(constant_interval_exprt(val1, val2), environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + WHEN("merging 1 with { 1, [ 1, 2 ] }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set( + {val1, constant_interval_exprt(val1, val2)}, environment, ns); + + auto merged = merge(op1, op2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + 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(merged); + EXPECT_TOP(merged.result); + } + } + 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(merged); + EXPECT_TOP(merged.result); + } + } + 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("result is modified TOP") + { + EXPECT_MODIFIED(merged); + EXPECT_TOP(merged.result); + } + } + } +} From a3d1b75ecca8fd8f51aa45f734f42e3b6acad5bc Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 25 Mar 2021 10:03:35 +0000 Subject: [PATCH 4/7] Add abstract_value_objectt::to_interval() Analogous to to_constant, it returns a constant_interval_exprt that expresses the range of the value. For constants the interval is across whatever the constant is, for intervals it is their interval(!) and for value_sets it is the interval between the smallest and largest values in the set. Used to intervals to merge with any other value type. This commit includes unit tests for interval_abstract_objectt::merge. --- .../abstract_object_set.cpp | 5 +- .../abstract_object_set.h | 7 +- .../abstract_value_object.cpp | 8 +- .../abstract_value_object.h | 5 +- .../constant_abstract_value.cpp | 5 + .../constant_abstract_value.h | 1 + .../interval_abstract_value.cpp | 40 +- .../interval_abstract_value.h | 4 +- .../value_set_abstract_object.cpp | 16 +- .../value_set_abstract_object.h | 8 +- unit/Makefile | 1 + .../constant_abstract_value/merge.cpp | 69 +-- .../interval_abstract_value/merge.cpp | 481 ++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 42 ++ .../variable_sensitivity_test_helpers.h | 47 ++ 15 files changed, 655 insertions(+), 84 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp diff --git a/src/analyses/variable-sensitivity/abstract_object_set.cpp b/src/analyses/variable-sensitivity/abstract_object_set.cpp index 9336b6e560b..fe91fa3a662 100644 --- a/src/analyses/variable-sensitivity/abstract_object_set.cpp +++ b/src/analyses/variable-sensitivity/abstract_object_set.cpp @@ -37,7 +37,7 @@ 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()); @@ -49,6 +49,5 @@ abstract_object_pointert abstract_object_sett::to_interval() lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr); upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr); } - 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 29adcb7104b..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. @@ -293,4 +296,4 @@ class abstract_value_objectt : public abstract_objectt, using abstract_value_pointert = sharing_ptrt; -#endif \ No newline at end of file +#endif diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 00576ff0d88..ae3f9462195 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -91,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, diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index d2e7de61da7..0cf91bd7de3 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -36,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, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 857c9753d46..9579577452c 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -329,8 +329,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 +342,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..26a8193abe6 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -41,7 +41,7 @@ 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; } @@ -68,7 +68,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..a835b7ad0f7 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,18 @@ value_set_abstract_objectt::value_range_implementation() const return make_value_set_value_range(values); } +exprt value_set_abstract_objectt::to_constant() const +{ + verify(); + return values.size() == 1 ? (*values.begin())->to_constant() + : 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 +212,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) //{ 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/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index cf8e65fe8cc..43297919203 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -62,8 +62,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with TOP") @@ -75,8 +74,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with BOTTOM") @@ -100,8 +98,7 @@ SCENARIO( THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging TOP with TOP") @@ -113,8 +110,7 @@ SCENARIO( THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging TOP with BOTTOM") @@ -126,8 +122,7 @@ SCENARIO( THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging BOTTOM with 1") @@ -151,8 +146,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with BOTTOM") @@ -164,8 +158,7 @@ SCENARIO( THEN("result is unmodified BOTTOM") { - EXPECT_UNMODIFIED(merged); - EXPECT_BOTTOM(merged.result); + EXPECT_UNMODIFIED_BOTTOM(merged); } } } @@ -181,8 +174,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with BOTTOM") @@ -206,8 +198,7 @@ SCENARIO( THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging TOP constant with BOTTOM") @@ -219,8 +210,7 @@ SCENARIO( THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_UNMODIFIED_TOP(merged); } } WHEN("merging BOTTOM constant with TOP") @@ -232,8 +222,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM constant with BOTTOM") @@ -245,8 +234,7 @@ SCENARIO( THEN("result is unmodified BOTTOM") { - EXPECT_UNMODIFIED(merged); - EXPECT_BOTTOM(merged.result); + EXPECT_UNMODIFIED_BOTTOM(merged); } } } @@ -274,8 +262,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with [2, 2]") @@ -287,8 +274,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with [1, 1]") @@ -312,8 +298,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } } @@ -341,8 +326,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with { 1, 2 }") @@ -354,8 +338,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with { [ 1, 1 ] }") @@ -381,8 +364,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with { [ 1, 2 ] }") @@ -395,8 +377,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging 1 with { 1, [ 1, 2 ] }") @@ -409,8 +390,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with { 1 }") @@ -434,8 +414,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with { [ 1, 1 ] }") @@ -461,8 +440,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.result); + EXPECT_MODIFIED_TOP(merged); } } WHEN("merging BOTTOM with { 1, [ 1, 2 ] }") @@ -475,8 +453,7 @@ SCENARIO( THEN("result is modified TOP") { - EXPECT_MODIFIED(merged); - EXPECT_TOP(merged.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..573c6313a80 --- /dev/null +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -0,0 +1,481 @@ +/*******************************************************************\ + + 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 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); + } + } + } +} \ No newline at end of file diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index e90599d5831..e8756e97b77 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) { @@ -291,6 +297,24 @@ void EXPECT_UNMODIFIED( 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, @@ -323,6 +347,24 @@ void EXPECT_MODIFIED( 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, diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 0fd98074d15..61ba8ac0707 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -26,6 +26,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); @@ -92,6 +93,30 @@ void EXPECT_UNMODIFIED(merge_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); @@ -112,6 +137,17 @@ 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, @@ -130,6 +166,17 @@ 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, From 249ca308a5d21a56aedb9a58fd9b76c09dbcc876 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 25 Mar 2021 16:26:29 +0000 Subject: [PATCH 5/7] Add interval internal_hash/equality Intervals can be added to value sets correctly now we're hashing on value rather than identity. --- .../interval_abstract_value.cpp | 13 +++++++++++++ .../variable-sensitivity/interval_abstract_value.h | 3 +++ .../expression_evaluation.cpp | 6 +++--- 3 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 9579577452c..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, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 26a8193abe6..e1362475aee 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -46,6 +46,9 @@ class interval_abstract_valuet : public abstract_value_objectt 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, 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 9ec820d0c16..38525d59083 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -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}); } } } From 714cee3175fafe800c70ee45476ba38144ceef87 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 25 Mar 2021 13:56:21 +0000 Subject: [PATCH 6/7] Correct value_set merge implementation. Ensure bottom flag is cleared when returning a new object. Intervals and constants can be merged into the a set. Extend abstract_object_set to_interval to handle intervals in the set --- .../variable-sensitivity/abstract_object.h | 4 + .../abstract_object_set.cpp | 17 +- .../value_set_abstract_object.cpp | 7 +- .../interval_abstract_value/merge.cpp | 28 +- .../module_dependencies.txt | 1 + .../module_dependencies.txt | 3 + .../value_set_abstract_object/merge.cpp | 407 ++++++++++++------ .../module_dependencies.txt | 3 + .../variable_sensitivity_test_helpers.cpp | 6 + .../variable_sensitivity_test_helpers.h | 6 + 10 files changed, 342 insertions(+), 140 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/value_expression_evaluation/module_dependencies.txt create mode 100644 unit/analyses/variable-sensitivity/value_set_abstract_object/module_dependencies.txt 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 fe91fa3a662..92a2a96437b 100644 --- a/src/analyses/variable-sensitivity/abstract_object_set.cpp +++ b/src/analyses/variable-sensitivity/abstract_object_set.cpp @@ -41,13 +41,20 @@ 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 constant_interval_exprt(lower_expr, upper_expr); } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index a835b7ad0f7..3fc9f8d22d7 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -229,19 +229,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); } @@ -268,6 +268,7 @@ void value_set_abstract_objectt::set_values( set_not_top(); values = other_values; } + set_not_bottom(); verify(); } diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp index 573c6313a80..4a8c5a13def 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -453,6 +453,32 @@ SCENARIO( 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(); @@ -478,4 +504,4 @@ SCENARIO( } } } -} \ No newline at end of file +} 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/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 e8756e97b77..cf770c677ad 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -92,6 +92,12 @@ 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()); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 61ba8ac0707..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 @@ -36,6 +39,7 @@ 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(); @@ -215,3 +219,5 @@ std::shared_ptr add_as_value_set( const abstract_object_pointert &op3, abstract_environmentt &environment, namespacet &ns); + +#endif From b3baa4082dfe2eecd5ffb6bc4da6ec1b1311c318 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 27 Mar 2021 10:10:25 +0000 Subject: [PATCH 7/7] Improve value_set to_constant() For multi-valued sets, calculate the interval then, if it's a single value interval return a constant, otherwise use the base operation. --- .../value_set_abstract_object.cpp | 11 +++++++++-- .../constant_abstract_value/merge.cpp | 13 +++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 3fc9f8d22d7..b7371f6f006 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -166,8 +166,15 @@ value_set_abstract_objectt::value_range_implementation() const exprt value_set_abstract_objectt::to_constant() const { verify(); - return values.size() == 1 ? (*values.begin())->to_constant() - : abstract_objectt::to_constant(); + + 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 diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 43297919203..c0ad2a18fd5 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -354,6 +354,19 @@ SCENARIO( EXPECT_UNMODIFIED(merged, val1); } } + WHEN("merging 1 with { 1, [1, 1] }") + { + 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);