From 954b2e150080ebb65eacaf6e7b907de7afd2e468 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 09:55:03 +0000 Subject: [PATCH 1/9] Bring value expression evaluation tests into a single scenario As we look to do cross-representation evaluation, it's no longer meanful to have separate tests for "expressions involving constants", etc --- unit/Makefile | 3 +- .../expression_evaluation.cpp | 95 ------------------- .../expression_evaluation.cpp | 95 ++++++++++++++++--- .../variable_sensitivity_test_helpers.cpp | 11 +++ .../variable_sensitivity_test_helpers.h | 10 +- 5 files changed, 99 insertions(+), 115 deletions(-) delete mode 100644 unit/analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp rename unit/analyses/variable-sensitivity/{value_set_abstract_object => value_expression_evaluation}/expression_evaluation.cpp (66%) diff --git a/unit/Makefile b/unit/Makefile index 5cccff397c1..7873549e5d9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -16,7 +16,6 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ analyses/variable-sensitivity/abstract_object/merge.cpp \ analyses/variable-sensitivity/abstract_object/index_range.cpp \ - analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/eval.cpp \ @@ -24,8 +23,8 @@ SRC += analyses/ai/ai.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 \ + analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \ analyses/variable-sensitivity/value_set/abstract_value.cpp \ - analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp \ analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ ansi-c/max_malloc_size.cpp \ diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp deleted file mode 100644 index d442c00bc9d..00000000000 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for constant_abstract_valuet::expression_transform - - Author: Jez Higgins, jez@jezuk.co.uk - -\*******************************************************************/ - -#include "../variable_sensitivity_test_helpers.h" -#include -#include -#include -#include - -SCENARIO( - "constants expression evaluation", - "[core][analyses][variable-sensitivity][constant_abstract_value][expression_" - "transform]") -{ - const exprt val1 = from_integer(1, integer_typet()); - const exprt val2 = from_integer(2, integer_typet()); - const exprt val3 = from_integer(3, integer_typet()); - - 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("adding two constants") - { - WHEN("1 + 2") - { - auto op1 = make_constant(val1, environment, ns); - auto op2 = make_constant(val2, environment, ns); - auto result = add_as_constant(op1, op2, environment, ns); - - THEN("= 3") - { - EXPECT(result, val3); - } - } - WHEN("1 + TOP") - { - auto op1 = make_constant(val1, environment, ns); - auto op2 = make_constant(val2, true); - auto result = add_as_constant(op1, op2, environment, ns); - - THEN("= TOP") - { - EXPECT_TOP(result); - } - } - WHEN("TOP + 1") - { - auto op1 = make_constant(val1, true); - auto op2 = make_constant(val2, environment, ns); - auto result = add_as_constant(op1, op2, environment, ns); - - THEN("= TOP") - { - EXPECT_TOP(result); - } - } - } - GIVEN("adding a constant and a value set") - { - WHEN("1 + { 2 }") - { - auto op1 = make_constant(val1, environment, ns); - auto op2 = make_value_set(val2, environment, ns); - auto result = add_as_value_set(op1, op2, environment, ns); - - THEN("= { 3 }") - { - EXPECT(result, {val3}); - } - } - WHEN("1 + { 1, 2 }") - { - auto op1 = make_constant(val1, environment, ns); - auto op2 = make_value_set({val1, val2}, environment, ns); - auto result = add_as_value_set(op1, op2, environment, ns); - - THEN("= { 2, 3 }") - { - EXPECT(result, {val2, val3}); - } - } - } -} diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp similarity index 66% rename from unit/analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp rename to unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index dc9a97ded64..03bab195a83 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -1,21 +1,21 @@ /*******************************************************************\ - Module: Unit tests for value_set_abstract_valuet::expression_transform + Module: Unit tests for abstract_value_objectt::expression_transform Author: Jez Higgins, jez@jezuk.co.uk \*******************************************************************/ -#include "../variable_sensitivity_test_helpers.h" +#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h" #include #include #include #include SCENARIO( - "value_set expression evaluation", - "[core][analyses][variable-sensitivity][value_set_abstract_object][" - "expression_transform]") + "constants expression evaluation", + "[core][analyses][variable-sensitivity][constant_abstract_value][value_set_" + "abstract_object][expression_transform]") { const exprt val1 = from_integer(1, integer_typet()); const exprt val2 = from_integer(2, integer_typet()); @@ -23,15 +23,80 @@ SCENARIO( const exprt val4 = from_integer(4, integer_typet()); const exprt val5 = from_integer(5, integer_typet()); - auto config = vsd_configt::value_set(); + 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); - auto environment = abstract_environmentt{object_factory}; + abstract_environmentt environment{object_factory}; environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("adding two constants") + { + WHEN("1 + 2") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_constant(val2, environment, ns); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= 3") + { + EXPECT(result, val3); + } + } + } + GIVEN("adding a constant and TOP") + { + WHEN("1 + TOP constant") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_constant(val2, true); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("TOP constant + 1") + { + auto op1 = make_top_constant(); + auto op2 = make_constant(val1, environment, ns); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + } + GIVEN("adding a constant and a value set") + { + WHEN("1 + { 2 }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set(val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { 3 }") + { + EXPECT(result, {val3}); + } + } + WHEN("1 + { 2, 3, 4 }") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_value_set({val2, val3, val4}, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { 3, 4, 5 }") + { + EXPECT(result, {val3, val4, val5}); + } + } + } GIVEN("adding two value_sets") { @@ -93,15 +158,15 @@ SCENARIO( } GIVEN("adding a value set and a constant") { - WHEN("{ 1 } + 1") + WHEN("{ 2 } + 1") { - auto op1 = make_value_set(val1, environment, ns); + auto op1 = make_value_set(val2, environment, ns); auto op2 = make_constant(val1, environment, ns); auto result = add_as_value_set(op1, op2, environment, ns); - THEN("= { 2 }") + THEN("= { 3 }") { - EXPECT(result, {val2}); + EXPECT(result, {val3}); } } WHEN("{ 2, 3, 4 } + 1") @@ -150,7 +215,7 @@ SCENARIO( WHEN("{ 1, 2 } + TOP constant") { auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = std::make_shared(val1.type()); + auto op2 = make_top_constant(); REQUIRE(op2->is_top()); auto result = add_as_value_set(op1, op2, environment, ns); @@ -163,7 +228,7 @@ SCENARIO( WHEN("{ 1, 2 } + TOP value_set") { auto op1 = make_value_set({val1, val2}, environment, ns); - auto op2 = std::make_shared(val1.type()); + auto op2 = make_top_value_set(); REQUIRE(op2->is_top()); auto result = add_as_value_set(op1, op2, environment, ns); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 120d31c954a..aef8273b5e2 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -9,6 +9,7 @@ #include "variable_sensitivity_test_helpers.h" #include #include +#include #include #include @@ -30,6 +31,11 @@ make_constant(exprt val, bool top) return std::make_shared(val.type(), top, !top); } +std::shared_ptr make_top_constant() +{ + return std::make_shared(integer_typet()); +} + std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, @@ -43,6 +49,11 @@ std::shared_ptr make_value_set( return vs; } +std::shared_ptr make_top_value_set() +{ + return std::make_shared(integer_typet()); +} + std::shared_ptr as_constant(const abstract_object_pointert &aop) { diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index b711dbae812..61398ec1d14 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -9,20 +9,24 @@ #include #include -std::shared_ptr -make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); - std::shared_ptr make_constant(exprt val, abstract_environmentt &env, namespacet &ns); std::shared_ptr make_constant(exprt val, bool top); +std::shared_ptr make_top_constant(); + +std::shared_ptr +make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); + std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, namespacet &ns); +std::shared_ptr make_top_value_set(); + std::shared_ptr as_constant(const abstract_object_pointert &aop); From 522cd4826d4c7d91931d21cd5eba9937415982e5 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 10:06:48 +0000 Subject: [PATCH 2/9] If a value is TOP, we can ignore its representation during dispatch --- .../abstract_value_object.cpp | 5 ++-- .../expression_evaluation.cpp | 24 ++++++++++++++++++- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index 9890dd1325c..00e732b034c 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -135,8 +135,9 @@ bool any_of_type(const std::vector &operands) operands.begin(), operands.end(), [](const abstract_object_pointert &p) { - return std::dynamic_pointer_cast(p) != - nullptr; + return (!p->is_top()) && + (std::dynamic_pointer_cast(p) != + nullptr); }) != operands.end(); } 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 03bab195a83..12db05aafe9 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -52,7 +52,18 @@ SCENARIO( WHEN("1 + TOP constant") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_constant(val2, true); + auto op2 = make_top_constant(); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("1 + TOP value_set") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_top_value_set(); auto result = add_as_constant(op1, op2, environment, ns); THEN("= TOP") @@ -66,6 +77,17 @@ SCENARIO( auto op2 = make_constant(val1, environment, ns); auto result = add_as_constant(op1, op2, environment, ns); + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("TOP value_set + 1") + { + auto op1 = make_top_value_set(); + auto op2 = make_constant(val1, environment, ns); + auto result = add_as_constant(op1, op2, environment, ns); + THEN("= TOP") { EXPECT_TOP(result); From 9ed46bbf0e82744d139f314ca7638b6cc54f42ec Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 10:20:47 +0000 Subject: [PATCH 3/9] Pull out make_bottom_constant() unit test helper --- .../constant_abstract_value/merge.cpp | 40 +++++++++---------- .../variable_sensitivity_test_helpers.cpp | 11 ++--- .../variable_sensitivity_test_helpers.h | 4 +- 3 files changed, 27 insertions(+), 28 deletions(-) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index c0c6e5f63d4..149d112067a 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -87,7 +87,7 @@ SCENARIO( WHEN("merging 1 with TOP") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_constant(val1, true); + auto op2 = make_top_constant(); auto merged = merge(op1, op2); @@ -99,7 +99,7 @@ SCENARIO( WHEN("merging 1 with BOTTOM") { auto op1 = make_constant(val1, environment, ns); - auto op2 = make_constant(val1, false); + auto op2 = make_bottom_constant(); auto merged = merge(op1, op2); @@ -110,7 +110,7 @@ SCENARIO( } WHEN("merging TOP with 1") { - auto op1 = make_constant(val1, true); + auto op1 = make_top_constant(); auto op2 = make_constant(val1, environment, ns); auto merged = merge(op1, op2); @@ -122,8 +122,8 @@ SCENARIO( } WHEN("merging TOP with TOP") { - auto op1 = make_constant(val1, true); - auto op2 = make_constant(val1, true); + auto op1 = make_top_constant(); + auto op2 = make_top_constant(); auto merged = merge(op1, op2); @@ -134,8 +134,8 @@ SCENARIO( } WHEN("merging TOP with BOTTOM") { - auto op1 = make_constant(val1, true); - auto op2 = make_constant(val1, false); + auto op1 = make_top_constant(); + auto op2 = make_bottom_constant(); auto merged = merge(op1, op2); @@ -146,7 +146,7 @@ SCENARIO( } WHEN("merging BOTTOM with 1") { - auto op1 = make_constant(val1, false); + auto op1 = make_bottom_constant(); auto op2 = make_constant(val1, environment, ns); auto merged = merge(op1, op2); @@ -158,8 +158,8 @@ SCENARIO( } WHEN("merging BOTTOM with TOP") { - auto op1 = make_constant(val1, false); - auto op2 = make_constant(val1, true); + auto op1 = make_bottom_constant(); + auto op2 = make_top_constant(); auto merged = merge(op1, op2); @@ -170,8 +170,8 @@ SCENARIO( } WHEN("merging BOTTOM with BOTTOM") { - auto op1 = make_constant(val1, false); - auto op2 = make_constant(val1, false); + auto op1 = make_bottom_constant(); + auto op2 = make_bottom_constant(); auto merged = merge(op1, op2); @@ -225,7 +225,7 @@ SCENARIO( } WHEN("merging constant TOP with TOP") { - auto op1 = make_constant(val1, true); + auto op1 = make_top_constant(); auto op2 = make_top_object(); auto merged = merge(op1, op2); @@ -237,7 +237,7 @@ SCENARIO( } WHEN("merging constant TOP with BOTTOM") { - auto op1 = make_constant(val1, true); + auto op1 = make_top_constant(); auto op2 = make_bottom_object(); auto merged = merge(op1, op2); @@ -249,7 +249,7 @@ SCENARIO( } WHEN("merging constant BOTTOM with TOP") { - auto op1 = make_constant(val1, false); + auto op1 = make_bottom_constant(); auto op2 = make_top_object(); auto merged = merge(op1, op2); @@ -261,7 +261,7 @@ SCENARIO( } WHEN("merging constant BOTTOM with BOTTOM") { - auto op1 = make_constant(val1, false); + auto op1 = make_bottom_constant(); auto op2 = make_bottom_object(); auto merged = merge(op1, op2); @@ -307,7 +307,7 @@ SCENARIO( WHEN("merging TOP with constant TOP") { auto op1 = make_top_object(); - auto op2 = make_constant(val1, true); + auto op2 = make_top_constant(); bool modified; auto result = abstract_objectt::merge(op1, op2, modified); @@ -321,7 +321,7 @@ SCENARIO( WHEN("merging TOP with constant BOTTOM") { auto op1 = make_top_object(); - auto op2 = make_constant(val1, false); + auto op2 = make_bottom_constant(); bool modified; auto result = abstract_objectt::merge(op1, op2, modified); @@ -348,7 +348,7 @@ SCENARIO( WHEN("merging BOTTOM with constant TOP") { auto op1 = make_bottom_object(); - auto op2 = make_constant(val1, true); + auto op2 = make_top_constant(); bool modified; auto result = abstract_objectt::merge(op1, op2, modified); @@ -361,7 +361,7 @@ SCENARIO( WHEN("merging BOTTOM with constant BOTTOM") { auto op1 = make_bottom_object(); - auto op2 = make_constant(val1, false); + auto op2 = make_bottom_constant(); bool modified; auto result = abstract_objectt::merge(op1, op2, modified); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index aef8273b5e2..24032ce1048 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -25,15 +25,16 @@ make_constant(exprt val, abstract_environmentt &env, namespacet &ns) return std::make_shared(val, env, ns); } -std::shared_ptr -make_constant(exprt val, bool top) +std::shared_ptr make_top_constant() { - return std::make_shared(val.type(), top, !top); + return std::make_shared( + integer_typet(), true, false); } -std::shared_ptr make_top_constant() +std::shared_ptr make_bottom_constant() { - return std::make_shared(integer_typet()); + return std::make_shared( + integer_typet(), false, true); } std::shared_ptr make_value_set( diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 61398ec1d14..2dd1c5411e7 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -12,10 +12,8 @@ std::shared_ptr make_constant(exprt val, abstract_environmentt &env, namespacet &ns); -std::shared_ptr -make_constant(exprt val, bool top); - std::shared_ptr make_top_constant(); +std::shared_ptr make_bottom_constant(); std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); From 4f8376c7426de348d6c7cfa3a96299761295ceea Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 10:41:58 +0000 Subject: [PATCH 4/9] All interval expression evaluation unit tests --- .../expression_evaluation.cpp | 37 ++++++++++++-- .../variable_sensitivity_test_helpers.cpp | 48 +++++++++++++++++++ .../variable_sensitivity_test_helpers.h | 21 ++++++++ 3 files changed, 101 insertions(+), 5 deletions(-) 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 12db05aafe9..39de7185403 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -17,11 +17,12 @@ SCENARIO( "[core][analyses][variable-sensitivity][constant_abstract_value][value_set_" "abstract_object][expression_transform]") { - 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()); - const exprt val5 = from_integer(5, integer_typet()); + 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); auto config = vsd_configt::constant_domain(); config.context_tracking.data_dependency_context = false; @@ -120,6 +121,32 @@ SCENARIO( } } + GIVEN("adding two intervals") + { + WHEN("[1,1] + [2,2]") + { + auto op1 = make_interval(val1, val1, environment, ns); + auto op2 = make_interval(val2, val2, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [3,3]") + { + EXPECT(result, val3, val3); + } + } + WHEN("[1,2] + [1,2]") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [2,4]") + { + EXPECT(result, val2, val4); + } + } + } + GIVEN("adding two value_sets") { WHEN("{ 1 } + { 1 }") diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 24032ce1048..d7b942cf33b 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -37,6 +37,16 @@ std::shared_ptr make_bottom_constant() integer_typet(), false, true); } +std::shared_ptr make_interval( + exprt vall, + exprt valh, + abstract_environmentt &env, + namespacet &ns) +{ + auto interval = constant_interval_exprt(vall, valh); + return std::make_shared(interval, env, ns); +} + std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, @@ -61,6 +71,12 @@ as_constant(const abstract_object_pointert &aop) return std::dynamic_pointer_cast(aop); } +std::shared_ptr +as_interval(const abstract_object_pointert &aop) +{ + return std::dynamic_pointer_cast(aop); +} + std::shared_ptr as_value_set(const abstract_object_pointert &aop) { @@ -130,6 +146,24 @@ void EXPECT( REQUIRE(result_expr == expected_value); } +void EXPECT( + std::shared_ptr &result, + exprt lower_value, + exprt upper_value) +{ + REQUIRE(result); + + REQUIRE_FALSE(result->is_top()); + REQUIRE_FALSE(result->is_bottom()); + + auto expected_interval = constant_interval_exprt(lower_value, upper_value); + auto result_expr = result->to_interval(); + INFO( + "Expect " + expr_to_str(result_expr) + " to equal " + + expr_to_str(expected_interval)); + REQUIRE(result_expr == expected_interval); +} + void EXPECT( std::shared_ptr &result, const std::vector &expected_values) @@ -236,6 +270,20 @@ std::shared_ptr add_as_constant( return cv; } +std::shared_ptr add_as_interval( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2, + abstract_environmentt &environment, + namespacet &ns) +{ + auto result = add(op1, op2, environment, ns); + auto i = as_interval(result); + + INFO("Result should be an interval") + REQUIRE(i); + return i; +} + std::shared_ptr add_as_value_set( const abstract_object_pointert &op1, const abstract_object_pointert &op2, diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 2dd1c5411e7..6eaa1a4d11d 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -7,6 +7,7 @@ \*******************************************************************/ #include +#include #include std::shared_ptr @@ -15,6 +16,12 @@ make_constant(exprt val, abstract_environmentt &env, namespacet &ns); std::shared_ptr make_top_constant(); std::shared_ptr make_bottom_constant(); +std::shared_ptr make_interval( + exprt vall, + exprt valh, + abstract_environmentt &env, + namespacet &ns); + std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); @@ -28,6 +35,9 @@ std::shared_ptr make_top_value_set(); std::shared_ptr as_constant(const abstract_object_pointert &aop); +std::shared_ptr +as_interval(const abstract_object_pointert &aop); + std::shared_ptr as_value_set(const abstract_object_pointert &aop); @@ -37,6 +47,11 @@ void EXPECT( std::shared_ptr &result, exprt expected_value); +void EXPECT( + std::shared_ptr &result, + exprt lower_value, + exprt upper_value); + void EXPECT( std::shared_ptr &result, const std::vector &expected_values); @@ -67,6 +82,12 @@ std::shared_ptr add_as_constant( abstract_environmentt &environment, namespacet &ns); +std::shared_ptr add_as_interval( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2, + abstract_environmentt &environment, + namespacet &ns); + std::shared_ptr add_as_value_set( const abstract_object_pointert &op1, const abstract_object_pointert &op2, From 9e2d4d7bd61ea3a2dfa17a70c423d36815bf9e94 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 11:20:47 +0000 Subject: [PATCH 5/9] Expressions with TOP intervals return TOP --- .../abstract_value_object.h | 6 +- .../interval_abstract_value.cpp | 6 + .../interval_abstract_value.h | 2 + .../expression_evaluation.cpp | 141 +++++++++++++++++- .../variable_sensitivity_test_helpers.cpp | 7 +- .../variable_sensitivity_test_helpers.h | 7 + 6 files changed, 162 insertions(+), 7 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 0b5a5384834..65f9ca690e2 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -287,10 +287,8 @@ class abstract_value_objectt : public abstract_objectt, virtual index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const = 0; - virtual value_range_implementation_ptrt value_range_implementation() const - { - return util_make_unique(); - } + virtual value_range_implementation_ptrt + value_range_implementation() const = 0; }; #endif \ No newline at end of file diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 7e68b2678b8..5fdeb8cd703 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -427,6 +427,12 @@ interval_abstract_valuet::index_range_implementation(const namespacet &ns) const return make_interval_index_range(interval, ns); } +value_range_implementation_ptrt +interval_abstract_valuet::value_range_implementation() const +{ + return make_single_value_range(shared_from_this()); +} + void interval_abstract_valuet::get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index fec22eab2c8..3ed58b18060 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -38,6 +38,8 @@ class interval_abstract_valuet : public abstract_value_objectt index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override; + value_range_implementation_ptrt value_range_implementation() const override; + exprt to_constant() const override; const constant_interval_exprt &to_interval() const { 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 39de7185403..b0ec76fe4e7 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -61,6 +61,17 @@ SCENARIO( EXPECT_TOP(result); } } + WHEN("1 + TOP interval") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_top_interval(); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } WHEN("1 + TOP value_set") { auto op1 = make_constant(val1, environment, ns); @@ -83,6 +94,17 @@ SCENARIO( EXPECT_TOP(result); } } + WHEN("TOP interval + 1") + { + auto op1 = make_top_interval(); + auto op2 = make_constant(val1, environment, ns); + auto result = add_as_constant(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } WHEN("TOP value_set + 1") { auto op1 = make_top_value_set(); @@ -146,6 +168,75 @@ SCENARIO( } } } + GIVEN("adding an interval and TOP") + { + WHEN("[1,2] + TOP constant") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_top_constant(); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("[1,2] + TOP interval") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_top_interval(); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("[1,2] + TOP value_set") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_top_value_set(); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("TOP constant + [1,2]") + { + auto op1 = make_top_constant(); + auto op2 = make_interval(val1, val2, environment, ns); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("TOP interval + [1,2]") + { + auto op1 = make_top_interval(); + auto op2 = make_interval(val1, val2, environment, ns); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + WHEN("TOP value_set + [1,2]") + { + auto op1 = make_top_value_set(); + auto op2 = make_interval(val1, val2, environment, ns); + auto result = add(op1, op2, environment, ns); + + THEN("= TOP") + { + EXPECT_TOP(result); + } + } + } GIVEN("adding two value_sets") { @@ -265,7 +356,18 @@ SCENARIO( { auto op1 = make_value_set({val1, val2}, environment, ns); auto op2 = make_top_constant(); - REQUIRE(op2->is_top()); + + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("the result is top") + { + EXPECT_TOP(result); + } + } + WHEN("{ 1, 2 } + TOP interval") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto op2 = make_top_interval(); auto result = add_as_value_set(op1, op2, environment, ns); @@ -278,7 +380,42 @@ SCENARIO( { auto op1 = make_value_set({val1, val2}, environment, ns); auto op2 = make_top_value_set(); - REQUIRE(op2->is_top()); + + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("the result is top") + { + EXPECT_TOP(result); + } + } + WHEN("TOP constant + { 1, 2 }") + { + auto op1 = make_top_constant(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("the result is top") + { + EXPECT_TOP(result); + } + } + WHEN("TOP interval + { 1, 2 }") + { + auto op1 = make_top_interval(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("the result is top") + { + EXPECT_TOP(result); + } + } + WHEN("TOP value_set + { 1, 2 }") + { + auto op1 = make_top_value_set(); + auto op2 = make_value_set({val1, val2}, environment, ns); auto result = add_as_value_set(op1, op2, environment, ns); diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index d7b942cf33b..6444afa71b0 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -47,6 +47,11 @@ std::shared_ptr make_interval( return std::make_shared(interval, env, ns); } +std::shared_ptr make_top_interval() +{ + return std::make_shared( + signedbv_typet(32), true, false); +} std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, @@ -240,7 +245,7 @@ void EXPECT_BOTTOM(std::shared_ptr result) REQUIRE(result->is_bottom()); } -static std::shared_ptr add( +std::shared_ptr add( const abstract_object_pointert &op1, const abstract_object_pointert &op2, abstract_environmentt &environment, diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 6eaa1a4d11d..c4e71c2e57c 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -21,6 +21,7 @@ std::shared_ptr make_interval( exprt valh, abstract_environmentt &env, namespacet &ns); +std::shared_ptr make_top_interval(); std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); @@ -76,6 +77,12 @@ void EXPECT_UNMODIFIED( bool modified, const std::vector &expected_values); +std::shared_ptr add( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2, + abstract_environmentt &environment, + namespacet &ns); + std::shared_ptr add_as_constant( const abstract_object_pointert &op1, const abstract_object_pointert &op2, From 4e67c0ec76822598b9a6c301af993c91236e1f3f Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 11:36:40 +0000 Subject: [PATCH 6/9] Expressions with intervals and constants --- .../expression_evaluation.cpp | 50 +++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 5 +- 2 files changed, 51 insertions(+), 4 deletions(-) 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 b0ec76fe4e7..1abee0fc9cb 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -117,6 +117,31 @@ SCENARIO( } } } + GIVEN("adding a constant and an interval") + { + WHEN("1 + [2,2]") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val2, val2, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [3,3]") + { + EXPECT(result, val3, val3); + } + } + WHEN("1 + [2,4]") + { + auto op1 = make_constant(val1, environment, ns); + auto op2 = make_interval(val2, val4, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [3,5]") + { + EXPECT(result, val3, val5); + } + } + } GIVEN("adding a constant and a value set") { WHEN("1 + { 2 }") @@ -237,6 +262,31 @@ SCENARIO( } } } + GIVEN("adding an interval and a constant") + { + WHEN("[2,2] + 1") + { + auto op1 = make_interval(val2, val2, environment, ns); + auto op2 = make_constant(val1, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [3,3]") + { + EXPECT(result, val3, val3); + } + } + WHEN("[2,4] + 1") + { + auto op1 = make_interval(val2, val4, environment, ns); + auto op2 = make_constant(val1, environment, ns); + auto result = add_as_interval(op1, op2, environment, ns); + + THEN("= [3,5]") + { + EXPECT(result, val3, val5); + } + } + } GIVEN("adding two value_sets") { diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 6444afa71b0..38efd2997de 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -9,8 +9,8 @@ #include "variable_sensitivity_test_helpers.h" #include #include -#include #include +#include #include std::shared_ptr @@ -163,9 +163,6 @@ void EXPECT( auto expected_interval = constant_interval_exprt(lower_value, upper_value); auto result_expr = result->to_interval(); - INFO( - "Expect " + expr_to_str(result_expr) + " to equal " + - expr_to_str(expected_interval)); REQUIRE(result_expr == expected_interval); } From 5aa4b92ddbd2879763b6bed87574e7c64a0d6f88 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 15:15:16 +0000 Subject: [PATCH 7/9] Enable mixed value-set and interval expression evaluation rewrite_expression has, incorrectly, expected every term in the rewritten expression to be a constant. When there are intervals in play, this is clearly not the case. When we encounter an interval, don't attempt to coerce it to a constant expression, simply use the existing operand. --- .../abstract_value_object.cpp | 16 +++- .../expression_evaluation.cpp | 80 +++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 22 ++++- 3 files changed, 114 insertions(+), 4 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index 00e732b034c..5138cee161a 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -556,13 +556,25 @@ class value_set_evaluator rewrite_expression(const std::vector &ops) const { auto operands_expr = exprt::operandst{}; - for(auto v : ops) - operands_expr.push_back(v->to_constant()); + for(size_t i = 0; i != expression.operands().size(); ++i) + { + const auto &v = ops[i]; + if(is_constant_value(v)) + operands_expr.push_back(v->to_constant()); + else + operands_expr.push_back(expression.operands()[i]); + } auto rewritten_expr = exprt(expression.id(), expression.type(), std::move(operands_expr)); return rewritten_expr; } + static bool is_constant_value(const abstract_object_pointert &v) + { + return std::dynamic_pointer_cast(v) != + nullptr; + } + std::vector operands_as_ranges() const { auto unwrapped = std::vector{}; 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 1abee0fc9cb..bcf1f12a201 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -287,6 +287,46 @@ SCENARIO( } } } + GIVEN("adding an interval and a value-set of constants") + { + WHEN("[2,2] + { 1 }") + { + auto op1 = make_interval(val2, val2, environment, ns); + auto op2 = make_value_set(val1, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[3,3]}") + { + EXPECT(result, {constant_interval_exprt(val3, val3)}); + } + } + WHEN("[2,4] + { 1 }") + { + auto op1 = make_interval(val2, val4, environment, ns); + auto op2 = make_value_set(val1, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[3,5]}") + { + EXPECT(result, {constant_interval_exprt(val3, val5)}); + } + } + WHEN("[1,2] + { 1, 2, 3 }") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_value_set({val1, val2, val3}, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[2,3], [3,4], [4,5]}") + { + EXPECT( + result, + {constant_interval_exprt(val2, val3), + constant_interval_exprt(val3, val4), + constant_interval_exprt(val4, val5)}); + } + } + } GIVEN("adding two value_sets") { @@ -371,6 +411,46 @@ SCENARIO( } } } + GIVEN("adding a value-set of constants and an interval") + { + WHEN("{ 1 } + [2,2]") + { + auto op1 = make_value_set(val1, environment, ns); + auto op2 = make_interval(val2, val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[3,3]}") + { + EXPECT(result, {constant_interval_exprt(val3, val3)}); + } + } + WHEN("{ 1 } + [2,4]") + { + auto op1 = make_value_set(val1, environment, ns); + auto op2 = make_interval(val2, val4, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[3,5]}") + { + EXPECT(result, {constant_interval_exprt(val3, val5)}); + } + } + WHEN("{ 1, 2, 3 } + [1,2]") + { + auto op1 = make_value_set({val1, val2, val3}, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= {[2,3], [3,4], [4,5]}") + { + EXPECT( + result, + {constant_interval_exprt(val2, val3), + constant_interval_exprt(val3, val4), + constant_interval_exprt(val4, val5)}); + } + } + } GIVEN("multiple operands") { WHEN("{ 1, 2, 3 } + 1 + 1") diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 38efd2997de..ced378525f7 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -93,13 +93,22 @@ bool set_contains(const abstract_object_sett &set, const exprt &val) auto i = std::find_if( set.begin(), set.end(), [&val](const abstract_object_pointert &lhs) { auto l = lhs->to_constant(); + auto interval = + std::dynamic_pointer_cast(lhs); + if(interval) + l = interval->to_interval(); return l == val; }); return i != set.end(); } -std::string expr_to_str(const exprt &expr) +static std::string interval_to_str(const constant_interval_exprt &expr); + +static std::string expr_to_str(const exprt &expr) { + if(expr.id() == ID_constant_interval) + return interval_to_str(to_constant_interval_expr(expr)); + auto st = symbol_tablet{}; auto ns = namespacet{st}; auto expr_str = std::string{}; @@ -110,6 +119,13 @@ std::string expr_to_str(const exprt &expr) return expr_str; } +static std::string interval_to_str(const constant_interval_exprt &expr) +{ + auto lower = expr_to_str(expr.get_lower()); + auto upper = expr_to_str(expr.get_upper()); + return "[" + lower + "," + upper + "]"; +} + template std::string container_to_str(const Container &con, UnaryOp unaryOp) { @@ -125,7 +141,9 @@ std::string container_to_str(const Container &con, UnaryOp unaryOp) std::string set_to_str(const abstract_object_sett &set) { return container_to_str(set, [](const abstract_object_pointert &lhs) { - return expr_to_str(lhs->to_constant()); + auto i = std::dynamic_pointer_cast(lhs); + return i ? interval_to_str(i->to_interval()) + : expr_to_str(lhs->to_constant()); }); } From cdf11c324ad758aeebd212c3f90383464f21afd8 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Mar 2021 16:26:45 +0000 Subject: [PATCH 8/9] More tests to confirm value-sets of intervals behaviour --- .../expression_evaluation.cpp | 149 ++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 38 +++-- .../variable_sensitivity_test_helpers.h | 8 +- 3 files changed, 182 insertions(+), 13 deletions(-) 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 bcf1f12a201..c1f10c66aed 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -451,6 +451,155 @@ SCENARIO( } } } + GIVEN("adding a value-set of intervals and constants with a constant") + { + auto interval12 = constant_interval_exprt(val1, val2); + auto interval23 = constant_interval_exprt(val2, val3); + auto interval34 = constant_interval_exprt(val3, val4); + auto interval45 = constant_interval_exprt(val4, val5); + + WHEN("{ [1,2] } + 2") + { + auto op1 = make_value_set(interval12, environment, ns); + auto op2 = make_constant(val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [3,4] }") + { + EXPECT(result, {interval34}); + } + } + WHEN("{ [1,2], 3 } + 2") + { + auto op1 = make_value_set({interval12, val3}, environment, ns); + auto op2 = make_constant(val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [3,4], 5 }") + { + EXPECT(result, {interval34, val5}); + } + } + WHEN("{ [1,2], [2,3] } + 2") + { + auto op1 = make_value_set({interval12, interval23}, environment, ns); + auto op2 = make_constant(val2, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [3,4], [4,5] }") + { + EXPECT(result, {interval34, interval45}); + } + } + } + GIVEN("adding a value-set of intervals and constants with an interval") + { + auto interval12 = constant_interval_exprt(val1, val2); + auto interval23 = constant_interval_exprt(val2, val3); + auto interval34 = constant_interval_exprt(val3, val4); + auto interval45 = constant_interval_exprt(val4, val5); + auto interval24 = constant_interval_exprt(val2, val4); + auto interval35 = constant_interval_exprt(val3, val5); + + WHEN("{ [1,2] } + [1,2]") + { + auto op1 = make_value_set(interval12, environment, ns); + auto op2 = make_interval(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4] }") + { + EXPECT(result, {interval24}); + } + } + WHEN("{ [1,2], 1 } + [1,2]") + { + auto op1 = make_value_set({interval12, val1}, environment, ns); + auto op2 = make_interval(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4], [2,3] }") + { + EXPECT(result, {interval24, interval23}); + } + } + WHEN("{ [1,2], [2,3] } + [1,2]") + { + auto op1 = make_value_set({interval12, interval23}, environment, ns); + auto op2 = make_interval(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4], [3,5] }") + { + EXPECT(result, {interval24, interval35}); + } + } + } + GIVEN("adding a value-set of intervals and constants with a value-set") + { + auto interval12 = constant_interval_exprt(val1, val2); + auto interval23 = constant_interval_exprt(val2, val3); + auto interval34 = constant_interval_exprt(val3, val4); + auto interval45 = constant_interval_exprt(val4, val5); + auto interval24 = constant_interval_exprt(val2, val4); + auto interval35 = constant_interval_exprt(val3, val5); + + WHEN("{ [1,2] } + { 1, 2 }") + { + auto op1 = make_value_set(interval12, environment, ns); + auto op2 = make_value_set({val1, val2}, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,3], [3,4] }") + { + EXPECT(result, {interval23, interval34}); + } + } + WHEN("{ [1,2] } + { [1,2] }") + { + auto op1 = make_value_set(interval12, environment, ns); + auto op2 = make_value_set(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4] }") + { + EXPECT(result, {interval24}); + } + } + WHEN("{ [1,2], 1 } + { [1,2] }") + { + auto op1 = make_value_set({interval12, val1}, environment, ns); + auto op2 = make_value_set(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4], [2,3] }") + { + EXPECT(result, {interval24, interval23}); + } + } + WHEN("{ [1,2], [2,3] } + { [1,2] }") + { + auto op1 = make_value_set({interval12, interval23}, environment, ns); + auto op2 = make_interval(interval12, environment, ns); + auto result = add_as_value_set(op1, op2, environment, ns); + + THEN("= { [2,4], [3,5] }") + { + EXPECT(result, {interval24, interval35}); + } + } + WHEN("{ [1,2], 1 } + { [1,2], 1 }") + { + auto op1 = make_value_set({interval12, val1}, environment, ns); + 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}); + } + } + } GIVEN("multiple operands") { WHEN("{ 1, 2, 3 } + 1 + 1") diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index ced378525f7..4e86c817484 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -13,12 +13,6 @@ #include #include -std::shared_ptr -make_value_set(exprt val, abstract_environmentt &env, namespacet &ns) -{ - return std::make_shared(val, env, ns); -} - std::shared_ptr make_constant(exprt val, abstract_environmentt &env, namespacet &ns) { @@ -38,13 +32,21 @@ std::shared_ptr make_bottom_constant() } std::shared_ptr make_interval( - exprt vall, - exprt valh, + const exprt &vall, + const exprt &valh, abstract_environmentt &env, namespacet &ns) { auto interval = constant_interval_exprt(vall, valh); - return std::make_shared(interval, env, ns); + return make_interval(interval, env, ns); +} + +std::shared_ptr make_interval( + const constant_interval_exprt &val, + abstract_environmentt &env, + namespacet &ns) +{ + return std::make_shared(val, env, ns); } std::shared_ptr make_top_interval() @@ -52,6 +54,14 @@ std::shared_ptr make_top_interval() return std::make_shared( signedbv_typet(32), true, false); } + +std::shared_ptr +make_value_set(exprt val, abstract_environmentt &env, namespacet &ns) +{ + auto vals = std::vector{val}; + return make_value_set(vals, env, ns); +} + std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, @@ -59,8 +69,14 @@ std::shared_ptr make_value_set( { auto initial_values = abstract_object_sett{}; for(auto v : vals) - initial_values.insert(make_constant(v, env, ns)); - auto vs = make_value_set(vals[0], env, ns); + { + if(v.id() == ID_constant_interval) + initial_values.insert( + std::make_shared(v, env, ns)); + else + initial_values.insert(make_constant(v, env, ns)); + } + auto vs = std::make_shared(vals[0], env, ns); vs->set_values(initial_values); return vs; } diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index c4e71c2e57c..9899a940201 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -17,8 +17,12 @@ std::shared_ptr make_top_constant(); std::shared_ptr make_bottom_constant(); std::shared_ptr make_interval( - exprt vall, - exprt valh, + const exprt &vall, + const exprt &valh, + abstract_environmentt &env, + namespacet &ns); +std::shared_ptr make_interval( + const constant_interval_exprt &val, abstract_environmentt &env, namespacet &ns); std::shared_ptr make_top_interval(); From b86dbcf6f15ccf433134950d5557095888a03df9 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 5 Mar 2021 16:58:01 +0000 Subject: [PATCH 9/9] value_set index_range should flatten contained values into one range A constant of, say, 5 has a index_range of 5. A value_set of { 5, 6, 9 } therefore has an index_range of 5,6,9. An interval of [1, 3] has an index_range of 1,2,3. A value_set containing that interval should have the same index_range. A value_set of multiple constants and intervals should have an index_range which is the union of its contents index_range. --- .../value_set_abstract_object.cpp | 23 ++-- .../abstract_object/index_range.cpp | 129 ++++++++++++++---- .../variable_sensitivity_test_helpers.cpp | 28 +++- .../variable_sensitivity_test_helpers.h | 4 + 4 files changed, 148 insertions(+), 36 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index efaa39fa8ee..dbe0472d4a6 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -11,18 +11,17 @@ #include #include -#include #include #include #include static index_range_implementation_ptrt -make_value_set_index_range(const abstract_object_sett &vals); +make_value_set_index_range(const std::set &vals); class value_set_index_ranget : public index_range_implementationt { public: - explicit value_set_index_ranget(const abstract_object_sett &vals) + explicit value_set_index_ranget(const std::set &vals) : values(vals), cur(), next(values.begin()) { PRECONDITION(!values.empty()); @@ -37,7 +36,7 @@ class value_set_index_ranget : public index_range_implementationt if(next == values.end()) return false; - cur = (*next)->to_constant(); + cur = *next; ++next; return true; } @@ -47,13 +46,13 @@ class value_set_index_ranget : public index_range_implementationt } private: - const abstract_object_sett &values; + std::set values; exprt cur; - abstract_object_sett::const_iterator next; + std::set::const_iterator next; }; static index_range_implementation_ptrt -make_value_set_index_range(const abstract_object_sett &vals) +make_value_set_index_range(const std::set &vals) { return util_make_unique(vals); } @@ -146,7 +145,15 @@ value_set_abstract_objectt::index_range_implementation( if(values.empty()) return make_indeterminate_index_range(); - return make_value_set_index_range(values); + std::set flattened; + for(const auto &o : values) + { + const auto &v = std::dynamic_pointer_cast(o); + for(auto e : v->index_range(ns)) + flattened.insert(e); + } + + return make_value_set_index_range(flattened); } value_range_implementation_ptrt diff --git a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp index 766100ebd12..8e5f1b8ccca 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp @@ -1,17 +1,16 @@ +#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h" #include -#include #include #include #include #include #include -#include #include #include SCENARIO( "index_range for constant_abstract_values" - "[core][analyses][variable-sensitivity][constant_abstract_value][index-" + "[core][analyses][variable-sensitivity][constant_abstract_value][index_" "range]") { auto type = signedbv_typet(32); @@ -26,8 +25,7 @@ SCENARIO( { auto int_value = 99; auto value_expr = from_integer(int_value, type); - auto value = - std::make_shared(value_expr, env, ns); + auto value = make_constant(value_expr, env, ns); auto range = value->index_range(ns); @@ -59,7 +57,7 @@ SCENARIO( GIVEN("a top constant's range is has a single nil expression") { - auto value = std::make_shared(type); + auto value = make_top_constant(); auto range = value->index_range(ns); @@ -78,7 +76,7 @@ SCENARIO( SCENARIO( "index_range for interval_abstract_values" - "[core][analyses][variable-sensitivity][interval_abstract_value][index-" + "[core][analyses][variable-sensitivity][interval_abstract_value][index_" "range]") { auto object_factory = variable_sensitivity_object_factoryt::configured_with( @@ -91,7 +89,7 @@ SCENARIO( GIVEN("a top intervals's range is empty") { - auto value = std::make_shared(type, true, false); + auto value = make_top_interval(); auto range = value->index_range(ns); @@ -105,8 +103,7 @@ SCENARIO( { auto int_value = 99; auto value_expr = from_integer(int_value, type); - auto value = - std::make_shared(value_expr, env, ns); + auto value = make_interval(value_expr, value_expr, env, ns); auto range = value->index_range(ns); @@ -127,12 +124,9 @@ SCENARIO( GIVEN("a [99,100] interval's index_range has two elements") { auto int_value = 99; - auto value_expr = from_integer(int_value, type); - auto value = std::make_shared( - constant_interval_exprt( - from_integer(int_value, type), from_integer(int_value + 1, type), type), - env, - ns); + auto lower = from_integer(int_value, type); + auto upper = from_integer(int_value + 1, type); + auto value = make_interval(lower, upper, env, ns); auto range = value->index_range(ns); @@ -159,12 +153,9 @@ SCENARIO( GIVEN("a [99,102] interval's index_range has four elements") { auto int_value = 99; - auto value_expr = from_integer(int_value, type); - auto value = std::make_shared( - constant_interval_exprt( - from_integer(int_value, type), from_integer(int_value + 3, type), type), - env, - ns); + auto lower = from_integer(int_value, type); + auto upper = from_integer(int_value + 3, type); + auto value = make_interval(lower, upper, env, ns); auto range = value->index_range(ns); @@ -186,7 +177,7 @@ SCENARIO( SCENARIO( "index_range for value_set_abstract_values" - "[core][analyses][variable-sensitivity][value_set_abstract_value][index-" + "[core][analyses][variable-sensitivity][value_set_abstract_value][index_" "range]") { auto object_factory = variable_sensitivity_object_factoryt::configured_with( @@ -197,10 +188,9 @@ SCENARIO( namespacet ns(symbol_table); auto type = signedbv_typet(32); - GIVEN("a value_set is empty") + GIVEN("a TOP value_set is empty") { - auto value = - std::make_shared(type, true, false); + auto value = make_top_value_set(); auto range = value->index_range(ns); THEN("range should have a nil expr") @@ -214,4 +204,91 @@ SCENARIO( REQUIRE(i == range.end()); } } + GIVEN("a value_set { 99, 100, 101, 102 } index_range has four elements") + { + auto int_value = 99; + auto _99 = from_integer(int_value, type); + auto _100 = from_integer(100, type); + auto _101 = from_integer(101, type); + auto _102 = from_integer(102, type); + auto value = make_value_set({_99, _100, _101, _102}, env, ns); + + auto range = value->index_range(ns); + + THEN("range has four values") + { + auto values = std::vector(); + for(const auto &e : range) + values.push_back(to_constant_expr(e)); + + REQUIRE(values.size() == 4); + EXPECT(values, {_99, _100, _101, _102}); + } + } + GIVEN("a value_set { [99, 102] } index_range has four elements") + { + auto int_value = 99; + auto _99 = from_integer(int_value, type); + auto _100 = from_integer(100, type); + auto _101 = from_integer(101, type); + auto _102 = from_integer(102, type); + auto _99_102 = constant_interval_exprt(_99, _102); + auto value = make_value_set({_99_102}, env, ns); + + auto range = value->index_range(ns); + + THEN("range has four values") + { + auto values = std::vector(); + for(const auto &e : range) + values.push_back(to_constant_expr(e)); + + REQUIRE(values.size() == 4); + EXPECT(values, {_99, _100, _101, _102}); + } + } + GIVEN("a value_set { 99, 100, [101, 102] } index_range has four elements") + { + auto int_value = 99; + auto _99 = from_integer(int_value, type); + auto _100 = from_integer(100, type); + auto _101 = from_integer(101, type); + auto _102 = from_integer(102, type); + auto _101_102 = constant_interval_exprt(_101, _102); + auto value = make_value_set({_99, _101_102, _100}, env, ns); + + auto range = value->index_range(ns); + + THEN("range has four values") + { + auto values = std::vector(); + for(const auto &e : range) + values.push_back(to_constant_expr(e)); + + REQUIRE(values.size() == 4); + EXPECT(values, {_99, _100, _101, _102}); + } + } + GIVEN("a value_set { [99, 102], 100, 101 } index_range has four elements") + { + auto int_value = 99; + auto _99 = from_integer(int_value, type); + auto _100 = from_integer(100, type); + auto _101 = from_integer(101, type); + auto _102 = from_integer(102, type); + auto _99_102 = constant_interval_exprt(_99, _102); + auto value = make_value_set({_99_102, _100, _101}, env, ns); + + auto range = value->index_range(ns); + + THEN("range has four values") + { + auto values = std::vector(); + for(const auto &e : range) + values.push_back(to_constant_expr(e)); + + REQUIRE(values.size() == 4); + EXPECT(values, {_99, _100, _101, _102}); + } + } } diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 4e86c817484..31b6e1e756c 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -104,6 +104,13 @@ as_value_set(const abstract_object_pointert &aop) return std::dynamic_pointer_cast(aop); } +bool set_contains(const std::vector &set, const exprt &val) +{ + auto i = std::find_if( + set.begin(), set.end(), [&val](const exprt &lhs) { return lhs == val; }); + return i != set.end(); +} + bool set_contains(const abstract_object_sett &set, const exprt &val) { auto i = std::find_if( @@ -210,14 +217,31 @@ void EXPECT( REQUIRE_FALSE(result->is_bottom()); auto values = result->get_values(); + auto value_string = set_to_str(values); + auto expected_string = exprs_to_str(expected_values); + + INFO("Expect " + value_string + " to match " + expected_string); REQUIRE(values.size() == expected_values.size()); - auto value_string = set_to_str(values); + for(auto &ev : expected_values) + { + INFO("Expect " + value_string + " to match " + expected_string); + REQUIRE(set_contains(values, ev)); + } +} + +void EXPECT( + const std::vector &values, + const std::vector &expected_values) +{ + auto value_string = exprs_to_str(values); auto expected_string = exprs_to_str(expected_values); + INFO("Expect " + value_string + " to match " + expected_string); + REQUIRE(values.size() == expected_values.size()); for(auto &ev : expected_values) { - INFO("Expect " + value_string + " to include " + expected_string); + INFO("Expect " + value_string + " to match " + expected_string); REQUIRE(set_contains(values, ev)); } } diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 9899a940201..570f1ad07e1 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -61,6 +61,10 @@ void EXPECT( std::shared_ptr &result, const std::vector &expected_values); +void EXPECT( + const std::vector &values, + const std::vector &expected_values); + void EXPECT_TOP(std::shared_ptr result); void EXPECT_TOP(std::shared_ptr &result);