From c372994b3a1757f9b3c5fbdc02f0502a7e506198 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 3 Dec 2020 12:42:10 +0000 Subject: [PATCH 01/16] index expression unit test --- .../eval-member-access.cpp | 111 ++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/eval-member-access.cpp diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp new file mode 100644 index 00000000000..276d53863e1 --- /dev/null +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -0,0 +1,111 @@ +#include + +#include +#include +#include +#include +#include +#include + +exprt make_array( + std::vector contents, + abstract_environmentt &environment, + namespacet &ns +); + +exprt fetch_element( + int index, + exprt &array, + abstract_environmentt &environment, + namespacet &ns +); + +SCENARIO( + "eval-member-access", + "[core][analyses][variable-sensitivity][eval-member-access]") +{ + auto environment = abstract_environmentt { + variable_sensitivity_object_factoryt::configured_with(vsd_configt::constant_domain()) + }; + environment.make_top(); // Domains are bottom on construction + + symbol_tablet symbol_table; + namespacet ns { symbol_table }; + + GIVEN("An array of size 3") + { + auto values = std::vector{ 1, 2, 3 }; + auto array = make_array(values, environment, ns); + + WHEN("getting index 0") { + auto result_expr = fetch_element(0, array, environment, ns); + + THEN("we get the first element") { + REQUIRE(result_expr == from_integer(values[0], integer_typet())); + } + } + WHEN("getting index 2") { + auto result_expr = fetch_element(2, array, environment, ns); + + THEN("we get the third element") { + REQUIRE(result_expr == from_integer(values[2], integer_typet())); + } + } + WHEN("getting index 5") { + auto result_value = fetch_element(5, array, environment, ns); + + THEN("we get a nil element") { + REQUIRE(result_value == nil_exprt()); + } + } + } +} + +exprt fetch_element( + int index, + exprt &array, + abstract_environmentt &environment, + namespacet &ns +) { + auto index_expression = index_exprt(array, from_integer(index, integer_typet())); + auto first_element = environment.eval(index_expression, ns); + + REQUIRE(std::dynamic_pointer_cast(first_element)); + const auto unwrapped = + std::dynamic_pointer_cast(first_element) + ->unwrap_context(); + auto value = std::dynamic_pointer_cast(unwrapped); + REQUIRE(value); + return value->to_constant(); +} + +exprt make_array( + std::vector contents, + abstract_environmentt &environment, + namespacet &ns +) { + const array_typet array_type( + integer_typet(), + from_integer(contents.size(), integer_typet()) + ); + + // int val1[3] = {1, 2, 3} + exprt::operandst array_elements; + for (auto v : contents) { + array_elements.push_back( + from_integer(v, integer_typet()) + ); + } + + auto populate_array = array_exprt(array_elements, array_type); + auto array_value = std::make_shared( + populate_array, environment, ns); + + auto array = symbolt(); + array.name = array.base_name = array.pretty_name = "array"; + array.type = array_type; + + environment.assign(array.symbol_expr(), array_value, ns); + + return array.symbol_expr(); +} From de45be55672c20f3d47c0c11f7420a6eedbb6b3a Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 15 Dec 2020 13:39:39 +0000 Subject: [PATCH 02/16] Add eval-expression-transform to unit tests --- unit/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/unit/Makefile b/unit/Makefile index d8891690144..33a32434ef9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -18,6 +18,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/eval.cpp \ + analyses/variable-sensitivity/eval-member-access.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 \ From 75e45c7ef9aaf8c05a12b77f82bef58c89aa5c08 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 3 Dec 2020 15:03:26 +0000 Subject: [PATCH 03/16] expand out array index unit test --- .../eval-member-access.cpp | 147 ++++++++++++------ 1 file changed, 97 insertions(+), 50 deletions(-) diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index 276d53863e1..805273aeefb 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -7,56 +7,88 @@ #include #include -exprt make_array( +void test_array( std::vector contents, abstract_environmentt &environment, - namespacet &ns -); + namespacet &ns); -exprt fetch_element( - int index, - exprt &array, - abstract_environmentt &environment, - namespacet &ns -); +const auto TOP = -99; SCENARIO( "eval-member-access", "[core][analyses][variable-sensitivity][eval-member-access]") { - auto environment = abstract_environmentt { - variable_sensitivity_object_factoryt::configured_with(vsd_configt::constant_domain()) - }; + auto environment = + abstract_environmentt{variable_sensitivity_object_factoryt::configured_with( + vsd_configt::constant_domain())}; environment.make_top(); // Domains are bottom on construction symbol_tablet symbol_table; - namespacet ns { symbol_table }; + namespacet ns{symbol_table}; - GIVEN("An array of size 3") + GIVEN("An array of {1, 2, 3}") { - auto values = std::vector{ 1, 2, 3 }; - auto array = make_array(values, environment, ns); + test_array({1, 2, 3}, environment, ns); + } + GIVEN("An array of {1, 2, TOP}") + { + test_array({1, 2, TOP}, environment, ns); + } + GIVEN("An array of {TOP, 2, TOP}") + { + test_array({TOP, 2, TOP}, environment, ns); + } +} + +exprt make_array( + std::vector contents, + abstract_environmentt &environment, + namespacet &ns); + +exprt fetch_element( + int index, + exprt &array, + abstract_environmentt &environment, + namespacet &ns); - WHEN("getting index 0") { - auto result_expr = fetch_element(0, array, environment, ns); +exprt integer_expression(int i); +exprt top_expression(); - THEN("we get the first element") { - REQUIRE(result_expr == from_integer(values[0], integer_typet())); - } +void test_array( + std::vector values, + abstract_environmentt &environment, + namespacet &ns) +{ + auto array = make_array(values, environment, ns); + + WHEN("getting index 0") + { + auto result_expr = fetch_element(0, array, environment, ns); + + THEN("we get the first element") + { + auto result_str = result_expr.pretty(); + REQUIRE(result_expr == integer_expression(values[0])); } - WHEN("getting index 2") { - auto result_expr = fetch_element(2, array, environment, ns); + } + WHEN("getting index 2") + { + auto result_expr = fetch_element(2, array, environment, ns); - THEN("we get the third element") { - REQUIRE(result_expr == from_integer(values[2], integer_typet())); - } + THEN("we get the third element") + { + auto result_str = result_expr.pretty(); + REQUIRE(result_expr == integer_expression(values[2])); } - WHEN("getting index 5") { - auto result_value = fetch_element(5, array, environment, ns); + } + WHEN("getting index 5") + { + auto result_expr = fetch_element(5, array, environment, ns); - THEN("we get a nil element") { - REQUIRE(result_value == nil_exprt()); - } + THEN("we get a nil element") + { + auto result_str = result_expr.pretty(); + REQUIRE(result_expr == nil_exprt()); } } } @@ -65,15 +97,20 @@ exprt fetch_element( int index, exprt &array, abstract_environmentt &environment, - namespacet &ns -) { - auto index_expression = index_exprt(array, from_integer(index, integer_typet())); - auto first_element = environment.eval(index_expression, ns); - - REQUIRE(std::dynamic_pointer_cast(first_element)); - const auto unwrapped = - std::dynamic_pointer_cast(first_element) - ->unwrap_context(); + namespacet &ns) +{ + auto index_expression = + index_exprt(array, from_integer(index, integer_typet())); + auto element = environment.eval(index_expression, ns); + + auto object = + std::dynamic_pointer_cast(element); + REQUIRE(object); + + if(object->is_top()) // oh! + return object->to_constant(); + + const auto unwrapped = object->unwrap_context(); auto value = std::dynamic_pointer_cast(unwrapped); REQUIRE(value); return value->to_constant(); @@ -82,24 +119,22 @@ exprt fetch_element( exprt make_array( std::vector contents, abstract_environmentt &environment, - namespacet &ns -) { + namespacet &ns) +{ const array_typet array_type( - integer_typet(), - from_integer(contents.size(), integer_typet()) - ); + integer_typet(), from_integer(contents.size(), integer_typet())); - // int val1[3] = {1, 2, 3} exprt::operandst array_elements; - for (auto v : contents) { - array_elements.push_back( - from_integer(v, integer_typet()) - ); + for(auto v : contents) + { + array_elements.push_back(integer_expression(v)); } auto populate_array = array_exprt(array_elements, array_type); auto array_value = std::make_shared( populate_array, environment, ns); + REQUIRE_FALSE(array_value->is_top()); + REQUIRE_FALSE(array_value->is_bottom()); auto array = symbolt(); array.name = array.base_name = array.pretty_name = "array"; @@ -109,3 +144,15 @@ exprt make_array( return array.symbol_expr(); } + +exprt integer_expression(int i) +{ + return (i == TOP) ? top_expression() : from_integer(i, integer_typet()); +} + +exprt top_expression() +{ + auto top_value = + std::make_shared(integer_typet(), true, false); + return top_value->to_constant(); +} \ No newline at end of file From af3eb526643055daa9c2754074ad7d1bdd3e3b8e Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 13:36:04 +0000 Subject: [PATCH 04/16] Remove redundant value_set_array_abstract_object overrides --- .../value_set_array_abstract_object.cpp | 16 ---------------- .../value_set_array_abstract_object.h | 10 ---------- 2 files changed, 26 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_array_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_array_abstract_object.cpp index 1c3f1c235c9..59d2bd64e87 100644 --- a/src/analyses/variable-sensitivity/value_set_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_array_abstract_object.cpp @@ -14,14 +14,6 @@ value_set_array_abstract_objectt::value_set_array_abstract_objectt( { } -abstract_object_pointert value_set_array_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return array_abstract_objectt::read(env, specifier, ns); -} - abstract_object_pointert value_set_array_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, @@ -34,14 +26,6 @@ abstract_object_pointert value_set_array_abstract_objectt::write( environment, ns, stack, specifier, value, merging_write); } -abstract_object_pointert value_set_array_abstract_objectt::read_index( - const abstract_environmentt &env, - const index_exprt &index, - const namespacet &ns) const -{ - return array_abstract_objectt::read_index(env, index, ns); -} - abstract_object_pointert value_set_array_abstract_objectt::write_index( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/value_set_array_abstract_object.h b/src/analyses/variable-sensitivity/value_set_array_abstract_object.h index f1211c872f1..a72283761a3 100644 --- a/src/analyses/variable-sensitivity/value_set_array_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_array_abstract_object.h @@ -21,11 +21,6 @@ class value_set_array_abstract_objectt : public array_abstract_objectt public: explicit value_set_array_abstract_objectt(const typet &type); - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - abstract_object_pointert write( abstract_environmentt &environment, const namespacet &ns, @@ -36,11 +31,6 @@ class value_set_array_abstract_objectt : public array_abstract_objectt CLONE protected: - abstract_object_pointert read_index( - const abstract_environmentt &env, - const index_exprt &index, - const namespacet &ns) const override; - abstract_object_pointert write_index( abstract_environmentt &environment, const namespacet &ns, From e62d4f12c3f817ced7eba8907d2d8ace1bf0bfdc Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 15:06:54 +0000 Subject: [PATCH 05/16] Move index_expression evaluation into array_abstract_object Move it out of abstract_environment. --- .../abstract_enviroment.cpp | 15 +++++++++---- .../array_abstract_object.cpp | 18 +++++++++++++++ .../array_abstract_object.h | 22 +++++++++++++++++++ 3 files changed, 51 insertions(+), 4 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index a6ee6a03d44..dc2311b7b80 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -78,11 +78,18 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const } else if(simplified_id == ID_index) { - index_exprt index_expr(to_index_expr(simplified_expr)); - abstract_object_pointert array_abstract_object = - eval(index_expr.array(), ns); + auto access_expr = (to_binary_expr(simplified_expr)); + auto target = eval(access_expr.lhs(), ns); - return array_abstract_object->read(*this, index_expr, ns); + std::vector operands; + + for(const auto &op : access_expr.operands()) + { + operands.push_back(eval(op, ns)); + } + + return target->expression_transform(access_expr, operands, *this, ns); + //return target->read(*this, access_expr, ns); } else if(simplified_id == ID_array) { diff --git a/src/analyses/variable-sensitivity/array_abstract_object.cpp b/src/analyses/variable-sensitivity/array_abstract_object.cpp index bdff3801f9e..7d898b527f2 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/array_abstract_object.cpp @@ -35,6 +35,24 @@ array_abstract_objectt::array_abstract_objectt( PRECONDITION(e.type().id() == ID_array); } +abstract_object_pointert array_abstract_objectt::expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const +{ + if (expr.id() == ID_index) + { + return read(environment, expr, ns); + } + + return abstract_objectt::expression_transform( + expr, + operands, + environment, + ns); +} + abstract_object_pointert array_abstract_objectt::read( const abstract_environmentt &env, const exprt &specifier, diff --git a/src/analyses/variable-sensitivity/array_abstract_object.h b/src/analyses/variable-sensitivity/array_abstract_object.h index 677f445262b..112e392531f 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.h +++ b/src/analyses/variable-sensitivity/array_abstract_object.h @@ -42,6 +42,28 @@ class array_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns); + /// Interface for transforms + /// + /// \param expr: the expression to evaluate and find the result of it. + /// This will be the symbol referred to be op0() + /// \param operands: an abstract_object (pointer) that represent + /// the possible values of each operand + /// \param environment: the abstract environment in which the + /// expression is being evaluated + /// \param ns: the current variable namespace + /// + /// \return Returns the abstract_object representing the result of + /// this expression to the maximum precision available. + /// + /// To try and resolve different expressions with the maximum level + /// of precision available. + abstract_object_pointert expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const override; + + /** * A helper function to evaluate an abstract object contained * within a container object. More precise abstractions may override this From 8798ccce1fd077cf4a25025cd5d1c529b5206459 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:01:09 +0000 Subject: [PATCH 06/16] Very simple union member access test union_abstract_object is only top or bottom, consequently this test tells us very little beyond telling us union member access works doesn't explode. However there is nowhere else in the tests that doing anything at all with unions, so it is a least a little backstop. --- .../simple-union-access/test.desc | 15 +++++++++++ .../goto-analyzer/simple-union-access/union.c | 26 +++++++++++++++++++ .../eval-member-access.cpp | 2 +- 3 files changed, 42 insertions(+), 1 deletion(-) create mode 100644 regression/goto-analyzer/simple-union-access/test.desc create mode 100644 regression/goto-analyzer/simple-union-access/union.c diff --git a/regression/goto-analyzer/simple-union-access/test.desc b/regression/goto-analyzer/simple-union-access/test.desc new file mode 100644 index 00000000000..68f4f677d29 --- /dev/null +++ b/regression/goto-analyzer/simple-union-access/test.desc @@ -0,0 +1,15 @@ +CORE +union.c +--variable-sensitivity --vsd --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] line 14 x.a==0: UNKNOWN$ +^\[main.assertion.2\] line 15 x.a==1: UNKNOWN$ +^\[main.assertion.3\] line 16 x.b==0: UNKNOWN$ +^\[main.assertion.4\] line 17 x.b==1: UNKNOWN$ +^\[main.assertion.5\] line 20 x.a==0: UNKNOWN$ +^\[main.assertion.6\] line 21 x.a==1: UNKNOWN$ +^\[main.assertion.7\] line 22 x.b==0: UNKNOWN$ +^\[main.assertion.8\] line 23 x.b==1: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/simple-union-access/union.c b/regression/goto-analyzer/simple-union-access/union.c new file mode 100644 index 00000000000..1cdf2e7b921 --- /dev/null +++ b/regression/goto-analyzer/simple-union-access/union.c @@ -0,0 +1,26 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test if we can represent constant structs + union union_struct + { + int a; + int b; + }; + + union union_struct x = {0}; + x.a = 0; + __CPROVER_assert(x.a == 0, "x.a==0"); + __CPROVER_assert(x.a == 1, "x.a==1"); + __CPROVER_assert(x.b == 0, "x.b==0"); + __CPROVER_assert(x.b == 1, "x.b==1"); + + x.b = 1; + __CPROVER_assert(x.a == 0, "x.a==0"); + __CPROVER_assert(x.a == 1, "x.a==1"); + __CPROVER_assert(x.b == 0, "x.b==0"); + __CPROVER_assert(x.b == 1, "x.b==1"); + + return 0; +} diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index 805273aeefb..aeb179bcfbc 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -155,4 +155,4 @@ exprt top_expression() auto top_value = std::make_shared(integer_typet(), true, false); return top_value->to_constant(); -} \ No newline at end of file +} From 474479cc92f5885324ae797cce36ad2a167f39fb Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:05:01 +0000 Subject: [PATCH 07/16] Move member expression evaluation into struct_abstract_object Move it out of abstract_environment. union_abstract_objects can also be the target of member expressions, but this is not implemented in the current code so I've left it out of here too. --- .../abstract_enviroment.cpp | 14 +++++--- .../struct_abstract_object.cpp | 33 +++++++++++++++++++ .../struct_abstract_object.h | 21 ++++++++++++ 3 files changed, 63 insertions(+), 5 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index dc2311b7b80..a5cabab930a 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -53,12 +53,17 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const } else if(simplified_id == ID_member) { - member_exprt member_expr(to_member_expr(simplified_expr)); + auto access_expr = simplified_expr; + auto target = eval(access_expr.operands()[0], ns); - const exprt &parent = member_expr.compound(); + std::vector operands; - abstract_object_pointert parent_abstract_object = eval(parent, ns); - return parent_abstract_object->read(*this, member_expr, ns); + for(const auto &op : access_expr.operands()) + { + operands.push_back(eval(op, ns)); + } + + return target->expression_transform(access_expr, operands, *this, ns); } else if(simplified_id == ID_address_of) { @@ -89,7 +94,6 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const } return target->expression_transform(access_expr, operands, *this, ns); - //return target->read(*this, access_expr, ns); } else if(simplified_id == ID_array) { diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.cpp b/src/analyses/variable-sensitivity/struct_abstract_object.cpp index 6632d35d825..81b290fb38c 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/struct_abstract_object.cpp @@ -37,6 +37,39 @@ struct_abstract_objectt::struct_abstract_objectt( PRECONDITION(ns.follow(e.type()).id() == ID_struct); } +/// Interface for transforms +/// +/// \param expr: the expression to evaluate and find the result of it. +/// This will be the symbol referred to be op0() +/// \param operands: an abstract_object (pointer) that represent +/// the possible values of each operand +/// \param environment: the abstract environment in which the +/// expression is being evaluated +/// \param ns: the current variable namespace +/// +/// \return Returns the abstract_object representing the result of +/// this expression to the maximum precision available. +/// +/// To try and resolve different expressions with the maximum level +/// of precision available. +abstract_object_pointert struct_abstract_objectt::expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const +{ + if (expr.id() == ID_member) + { + return read(environment, expr, ns); + } + + return abstract_objectt::expression_transform( + expr, + operands, + environment, + ns); +} + abstract_object_pointert struct_abstract_objectt::read( const abstract_environmentt &env, const exprt &specifier, diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.h b/src/analyses/variable-sensitivity/struct_abstract_object.h index 13ed56b64f4..63cd97a3234 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.h +++ b/src/analyses/variable-sensitivity/struct_abstract_object.h @@ -32,6 +32,27 @@ class struct_abstract_objectt : public abstract_objectt /// Asserts if both top and bottom are true struct_abstract_objectt(const typet &type, bool top, bool bottom); + /// Interface for transforms + /// + /// \param expr: the expression to evaluate and find the result of it. + /// This will be the symbol referred to be op0() + /// \param operands: an abstract_object (pointer) that represent + /// the possible values of each operand + /// \param environment: the abstract environment in which the + /// expression is being evaluated + /// \param ns: the current variable namespace + /// + /// \return Returns the abstract_object representing the result of + /// this expression to the maximum precision available. + /// + /// To try and resolve different expressions with the maximum level + /// of precision available. + abstract_object_pointert expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const override; + /// \param expr: the expression to use as the starting pointer for /// an abstract object /// \param environment: the environment in which the pointer is being From 405bab3ed2ae5d25f9a4d30baa5f2b99a968880c Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:11:35 +0000 Subject: [PATCH 08/16] Combine member_expr and index_expr cases together --- .../variable-sensitivity/abstract_enviroment.cpp | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index a5cabab930a..310c0a9627d 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -51,7 +51,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const return found_symbol_value; } } - else if(simplified_id == ID_member) + else if(simplified_id == ID_member || simplified_id == ID_index) { auto access_expr = simplified_expr; auto target = eval(access_expr.operands()[0], ns); @@ -81,20 +81,6 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const return pointer_abstract_object->read(*this, nil_exprt(), ns); } - else if(simplified_id == ID_index) - { - auto access_expr = (to_binary_expr(simplified_expr)); - auto target = eval(access_expr.lhs(), ns); - - std::vector operands; - - for(const auto &op : access_expr.operands()) - { - operands.push_back(eval(op, ns)); - } - - return target->expression_transform(access_expr, operands, *this, ns); - } else if(simplified_id == ID_array) { return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); From ba9dbf52516892d49013b1bb84abc3a7e0a12b0b Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:23:53 +0000 Subject: [PATCH 09/16] Removed redundant value_set_pointer_abstract_object member functions --- .../value_set_pointer_abstract_object.cpp | 14 -------------- .../value_set_pointer_abstract_object.h | 9 --------- 2 files changed, 23 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp index 2ef2a695144..614209189b1 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -15,14 +15,6 @@ value_set_pointer_abstract_objectt::merge(abstract_object_pointert other) const return shared_from_this(); } -abstract_object_pointert value_set_pointer_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return pointer_abstract_objectt::read(env, specifier, ns); -} - abstract_object_pointert value_set_pointer_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, @@ -40,12 +32,6 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( : pointer_abstract_objectt(type) { } -abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference( - const abstract_environmentt &env, - const namespacet &ns) const -{ - return pointer_abstract_objectt::read_dereference(env, ns); -} abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference( abstract_environmentt &environment, diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h index 04e1945d771..ef4caf7a308 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -23,11 +23,6 @@ class value_set_pointer_abstract_objectt : public pointer_abstract_objectt abstract_object_pointert merge(abstract_object_pointert other) const override; - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - abstract_object_pointert write( abstract_environmentt &environment, const namespacet &ns, @@ -38,10 +33,6 @@ class value_set_pointer_abstract_objectt : public pointer_abstract_objectt CLONE protected: - abstract_object_pointert read_dereference( - const abstract_environmentt &env, - const namespacet &ns) const override; - abstract_object_pointert write_dereference( abstract_environmentt &environment, const namespacet &ns, From a5f16cfe6f83e34547cbababbc26ea3e6e2f7608 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:30:45 +0000 Subject: [PATCH 10/16] Move dereference evaluation into pointer_abstract_object Move it out of abstract_environment. --- .../abstract_enviroment.cpp | 10 +-------- .../pointer_abstract_object.cpp | 18 ++++++++++++++++ .../pointer_abstract_object.h | 21 +++++++++++++++++++ .../struct_abstract_object.cpp | 15 ------------- 4 files changed, 40 insertions(+), 24 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index 310c0a9627d..aa23007f948 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -51,7 +51,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const return found_symbol_value; } } - else if(simplified_id == ID_member || simplified_id == ID_index) + else if(simplified_id == ID_member || simplified_id == ID_index || simplified_id == ID_dereference) { auto access_expr = simplified_expr; auto target = eval(access_expr.operands()[0], ns); @@ -73,14 +73,6 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const // Store the abstract object in the pointer return pointer_object; } - else if(simplified_id == ID_dereference) - { - dereference_exprt dereference(to_dereference_expr(simplified_expr)); - abstract_object_pointert pointer_abstract_object = - eval(dereference.pointer(), ns); - - return pointer_abstract_object->read(*this, nil_exprt(), ns); - } else if(simplified_id == ID_array) { return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp index 4321567d603..ad6c6070e07 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp @@ -36,6 +36,24 @@ pointer_abstract_objectt::pointer_abstract_objectt( PRECONDITION(e.type().id() == ID_pointer); } +abstract_object_pointert pointer_abstract_objectt::expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const +{ + if (expr.id() == ID_dereference) + { + return read(environment, expr, ns); + } + + return abstract_objectt::expression_transform( + expr, + operands, + environment, + ns); +} + abstract_object_pointert pointer_abstract_objectt::read( const abstract_environmentt &env, const exprt &specifier, diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.h b/src/analyses/variable-sensitivity/pointer_abstract_object.h index f604a73152a..eed0659d1c2 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/pointer_abstract_object.h @@ -33,6 +33,27 @@ class pointer_abstract_objectt : public abstract_objectt /// \param bottom: is the abstract_object starting as bottom pointer_abstract_objectt(const typet &type, bool top, bool bottom); + /// Interface for transforms + /// + /// \param expr: the expression to evaluate and find the result of it. + /// This will be the symbol referred to be op0() + /// \param operands: an abstract_object (pointer) that represent + /// the possible values of each operand + /// \param environment: the abstract environment in which the + /// expression is being evaluated + /// \param ns: the current variable namespace + /// + /// \return Returns the abstract_object representing the result of + /// this expression to the maximum precision available. + /// + /// To try and resolve different expressions with the maximum level + /// of precision available. + abstract_object_pointert expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const override; + /// \param expr: the expression to use as the starting pointer for /// an abstract object /// \param environment: the environment in which the pointer is being diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.cpp b/src/analyses/variable-sensitivity/struct_abstract_object.cpp index 81b290fb38c..9d0381781da 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/struct_abstract_object.cpp @@ -37,21 +37,6 @@ struct_abstract_objectt::struct_abstract_objectt( PRECONDITION(ns.follow(e.type()).id() == ID_struct); } -/// Interface for transforms -/// -/// \param expr: the expression to evaluate and find the result of it. -/// This will be the symbol referred to be op0() -/// \param operands: an abstract_object (pointer) that represent -/// the possible values of each operand -/// \param environment: the abstract environment in which the -/// expression is being evaluated -/// \param ns: the current variable namespace -/// -/// \return Returns the abstract_object representing the result of -/// this expression to the maximum precision available. -/// -/// To try and resolve different expressions with the maximum level -/// of precision available. abstract_object_pointert struct_abstract_objectt::expression_transform( const exprt &expr, const std::vector &operands, From 1407cd44058b5471537027876086e605a9111bb3 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:32:46 +0000 Subject: [PATCH 11/16] Remove redundant cast --- src/analyses/variable-sensitivity/abstract_enviroment.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index aa23007f948..5e0c20072a0 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -83,8 +83,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const } else if(simplified_id == ID_constant) { - return abstract_object_factory( - simplified_expr.type(), to_constant_expr(simplified_expr), ns); + return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); } else { From 7af43f3b60d0344cf44e288b455099b235be3774 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:36:12 +0000 Subject: [PATCH 12/16] Combine array, struct, and constant handlers --- .../variable-sensitivity/abstract_enviroment.cpp | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index 5e0c20072a0..8401e661d2e 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -73,15 +73,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const // Store the abstract object in the pointer return pointer_object; } - else if(simplified_id == ID_array) - { - return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); - } - else if(simplified_id == ID_struct) - { - return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); - } - else if(simplified_id == ID_constant) + else if(simplified_id == ID_array || simplified_id == ID_struct || simplified_id == ID_constant) { return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); } From a983bd5c33d357f36eb3e5bcbe2903c750e462d6 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 8 Dec 2020 16:46:25 +0000 Subject: [PATCH 13/16] Factored out eval_operands helper function --- .../abstract_enviroment.cpp | 45 ++++++++++++------- 1 file changed, 29 insertions(+), 16 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index 8401e661d2e..b6a9705ec68 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -27,6 +27,11 @@ # include #endif +std::vector eval_operands( + const exprt &expr, + const abstract_environmentt &env, + const namespacet &ns); + abstract_object_pointert abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const { @@ -56,14 +61,11 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const auto access_expr = simplified_expr; auto target = eval(access_expr.operands()[0], ns); - std::vector operands; - - for(const auto &op : access_expr.operands()) - { - operands.push_back(eval(op, ns)); - } - - return target->expression_transform(access_expr, operands, *this, ns); + return target->expression_transform( + access_expr, + eval_operands(access_expr, *this, ns), + *this, + ns); } else if(simplified_id == ID_address_of) { @@ -428,14 +430,11 @@ abstract_object_pointert abstract_environmentt::eval_expression( abstract_object_pointert eval_obj = abstract_object_factory(e.type(), ns, true); - std::vector operands; - - for(const auto &op : e.operands()) - { - operands.push_back(eval(op, ns)); - } - - return eval_obj->expression_transform(e, operands, *this, ns); + return eval_obj->expression_transform( + e, + eval_operands(e, *this, ns), + *this, + ns); } void abstract_environmentt::erase(const symbol_exprt &expr) @@ -507,3 +506,17 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const } return statistics; } + +std::vector eval_operands( + const exprt &expr, + const abstract_environmentt &env, + const namespacet &ns) +{ + std::vector operands; + + for(const auto &op : expr.operands()) + operands.push_back(env.eval(op, ns)); + + return operands; +} + From c8f3e487be382a41f81d286de7b291792397a90f Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 9 Dec 2020 11:28:32 +0000 Subject: [PATCH 14/16] Clang format --- .../simple-union-access/test.desc | 16 ++++++++-------- .../goto-analyzer/simple-union-access/union.c | 3 +-- .../abstract_enviroment.cpp | 19 ++++++++----------- .../array_abstract_object.cpp | 7 ++----- .../array_abstract_object.h | 1 - .../pointer_abstract_object.cpp | 7 ++----- .../struct_abstract_object.cpp | 7 ++----- 7 files changed, 23 insertions(+), 37 deletions(-) diff --git a/regression/goto-analyzer/simple-union-access/test.desc b/regression/goto-analyzer/simple-union-access/test.desc index 68f4f677d29..1fc9abf3465 100644 --- a/regression/goto-analyzer/simple-union-access/test.desc +++ b/regression/goto-analyzer/simple-union-access/test.desc @@ -3,13 +3,13 @@ union.c --variable-sensitivity --vsd --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] line 14 x.a==0: UNKNOWN$ -^\[main.assertion.2\] line 15 x.a==1: UNKNOWN$ -^\[main.assertion.3\] line 16 x.b==0: UNKNOWN$ -^\[main.assertion.4\] line 17 x.b==1: UNKNOWN$ -^\[main.assertion.5\] line 20 x.a==0: UNKNOWN$ -^\[main.assertion.6\] line 21 x.a==1: UNKNOWN$ -^\[main.assertion.7\] line 22 x.b==0: UNKNOWN$ -^\[main.assertion.8\] line 23 x.b==1: UNKNOWN$ +^\[main.assertion.1\] line 13 x.a==0: UNKNOWN$ +^\[main.assertion.2\] line 14 x.a==1: UNKNOWN$ +^\[main.assertion.3\] line 15 x.b==0: UNKNOWN$ +^\[main.assertion.4\] line 16 x.b==1: UNKNOWN$ +^\[main.assertion.5\] line 19 x.a==0: UNKNOWN$ +^\[main.assertion.6\] line 20 x.a==1: UNKNOWN$ +^\[main.assertion.7\] line 21 x.b==0: UNKNOWN$ +^\[main.assertion.8\] line 22 x.b==1: UNKNOWN$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/simple-union-access/union.c b/regression/goto-analyzer/simple-union-access/union.c index 1cdf2e7b921..6be803d606e 100644 --- a/regression/goto-analyzer/simple-union-access/union.c +++ b/regression/goto-analyzer/simple-union-access/union.c @@ -3,8 +3,7 @@ int main(int argc, char *argv[]) { // Test if we can represent constant structs - union union_struct - { + union union_struct { int a; int b; }; diff --git a/src/analyses/variable-sensitivity/abstract_enviroment.cpp b/src/analyses/variable-sensitivity/abstract_enviroment.cpp index b6a9705ec68..5fdb8a59aba 100644 --- a/src/analyses/variable-sensitivity/abstract_enviroment.cpp +++ b/src/analyses/variable-sensitivity/abstract_enviroment.cpp @@ -56,16 +56,15 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const return found_symbol_value; } } - else if(simplified_id == ID_member || simplified_id == ID_index || simplified_id == ID_dereference) + else if( + simplified_id == ID_member || simplified_id == ID_index || + simplified_id == ID_dereference) { auto access_expr = simplified_expr; auto target = eval(access_expr.operands()[0], ns); return target->expression_transform( - access_expr, - eval_operands(access_expr, *this, ns), - *this, - ns); + access_expr, eval_operands(access_expr, *this, ns), *this, ns); } else if(simplified_id == ID_address_of) { @@ -75,7 +74,9 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const // Store the abstract object in the pointer return pointer_object; } - else if(simplified_id == ID_array || simplified_id == ID_struct || simplified_id == ID_constant) + else if( + simplified_id == ID_array || simplified_id == ID_struct || + simplified_id == ID_constant) { return abstract_object_factory(simplified_expr.type(), simplified_expr, ns); } @@ -431,10 +432,7 @@ abstract_object_pointert abstract_environmentt::eval_expression( abstract_object_factory(e.type(), ns, true); return eval_obj->expression_transform( - e, - eval_operands(e, *this, ns), - *this, - ns); + e, eval_operands(e, *this, ns), *this, ns); } void abstract_environmentt::erase(const symbol_exprt &expr) @@ -519,4 +517,3 @@ std::vector eval_operands( return operands; } - diff --git a/src/analyses/variable-sensitivity/array_abstract_object.cpp b/src/analyses/variable-sensitivity/array_abstract_object.cpp index 7d898b527f2..9400c8b67bd 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/array_abstract_object.cpp @@ -41,16 +41,13 @@ abstract_object_pointert array_abstract_objectt::expression_transform( const abstract_environmentt &environment, const namespacet &ns) const { - if (expr.id() == ID_index) + if(expr.id() == ID_index) { return read(environment, expr, ns); } return abstract_objectt::expression_transform( - expr, - operands, - environment, - ns); + expr, operands, environment, ns); } abstract_object_pointert array_abstract_objectt::read( diff --git a/src/analyses/variable-sensitivity/array_abstract_object.h b/src/analyses/variable-sensitivity/array_abstract_object.h index 112e392531f..da25e853b3b 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.h +++ b/src/analyses/variable-sensitivity/array_abstract_object.h @@ -63,7 +63,6 @@ class array_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns) const override; - /** * A helper function to evaluate an abstract object contained * within a container object. More precise abstractions may override this diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp index ad6c6070e07..0d15f8a3d4d 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp @@ -42,16 +42,13 @@ abstract_object_pointert pointer_abstract_objectt::expression_transform( const abstract_environmentt &environment, const namespacet &ns) const { - if (expr.id() == ID_dereference) + if(expr.id() == ID_dereference) { return read(environment, expr, ns); } return abstract_objectt::expression_transform( - expr, - operands, - environment, - ns); + expr, operands, environment, ns); } abstract_object_pointert pointer_abstract_objectt::read( diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.cpp b/src/analyses/variable-sensitivity/struct_abstract_object.cpp index 9d0381781da..09f9a0ed37c 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/struct_abstract_object.cpp @@ -43,16 +43,13 @@ abstract_object_pointert struct_abstract_objectt::expression_transform( const abstract_environmentt &environment, const namespacet &ns) const { - if (expr.id() == ID_member) + if(expr.id() == ID_member) { return read(environment, expr, ns); } return abstract_objectt::expression_transform( - expr, - operands, - environment, - ns); + expr, operands, environment, ns); } abstract_object_pointert struct_abstract_objectt::read( From 97b6d877a47a96a0fd4b5e6b060ad428234ef630 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 15 Dec 2020 10:24:47 +0000 Subject: [PATCH 15/16] Remove abstract_objectt::read member function Now we've moved some work into expression_transform, we don't need a read member on the base class. --- .../variable-sensitivity/abstract_object.cpp | 8 ------- .../variable-sensitivity/abstract_object.h | 17 -------------- .../array_abstract_object.cpp | 10 +-------- .../array_abstract_object.h | 17 -------------- .../context_abstract_object.cpp | 22 ------------------- .../context_abstract_object.h | 5 ----- .../pointer_abstract_object.cpp | 10 +-------- .../pointer_abstract_object.h | 17 -------------- .../struct_abstract_object.cpp | 10 +-------- .../struct_abstract_object.h | 17 -------------- .../union_abstract_object.cpp | 8 ------- .../union_abstract_object.h | 17 -------------- .../value_set_abstract_object.cpp | 12 ---------- .../value_set_abstract_object.h | 8 ------- .../constant_array_abstract_object/merge.cpp | 3 ++- .../full_struct_abstract_object/merge.cpp | 3 ++- 16 files changed, 7 insertions(+), 177 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index ed26f4fc450..fe7b992bbee 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -136,14 +136,6 @@ abstract_object_pointert abstract_objectt::expression_transform( return environment.abstract_object_factory(copy.type(), copy, ns); } -abstract_object_pointert abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return shared_from_this(); -} - abstract_object_pointert abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 66b07e9d030..0ffdd44a289 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -177,23 +177,6 @@ class abstract_objectt : public std::enable_shared_from_this /// that allows an object to be built from a value. virtual exprt to_constant() const; - /** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - */ - virtual abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const; - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/array_abstract_object.cpp b/src/analyses/variable-sensitivity/array_abstract_object.cpp index 9400c8b67bd..6f900147def 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/array_abstract_object.cpp @@ -43,21 +43,13 @@ abstract_object_pointert array_abstract_objectt::expression_transform( { if(expr.id() == ID_index) { - return read(environment, expr, ns); + return read_index(environment, to_index_expr(expr), ns); } return abstract_objectt::expression_transform( expr, operands, environment, ns); } -abstract_object_pointert array_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return this->read_index(env, to_index_expr(specifier), ns); -} - abstract_object_pointert array_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/array_abstract_object.h b/src/analyses/variable-sensitivity/array_abstract_object.h index da25e853b3b..a564b98a747 100644 --- a/src/analyses/variable-sensitivity/array_abstract_object.h +++ b/src/analyses/variable-sensitivity/array_abstract_object.h @@ -63,23 +63,6 @@ class array_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns) const override; - /** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - */ - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/context_abstract_object.cpp b/src/analyses/variable-sensitivity/context_abstract_object.cpp index ba30633694c..a4bc26e68d6 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/context_abstract_object.cpp @@ -30,28 +30,6 @@ void context_abstract_objectt::set_not_top_internal() set_child(child_abstract_object->clear_top()); } -/** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - * For the dependency context, the operation is simply delegated to the - * child object - */ -abstract_object_pointert context_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return child_abstract_object->read(env, specifier, ns); -} - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/context_abstract_object.h b/src/analyses/variable-sensitivity/context_abstract_object.h index 03611620ade..0b30b69c279 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.h +++ b/src/analyses/variable-sensitivity/context_abstract_object.h @@ -107,11 +107,6 @@ class context_abstract_objectt : public abstract_objectt void set_top_internal() override; void set_not_top_internal() override; - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - abstract_object_pointert write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp index 0d15f8a3d4d..7a3bd8a0b71 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/pointer_abstract_object.cpp @@ -44,21 +44,13 @@ abstract_object_pointert pointer_abstract_objectt::expression_transform( { if(expr.id() == ID_dereference) { - return read(environment, expr, ns); + return read_dereference(environment, ns); } return abstract_objectt::expression_transform( expr, operands, environment, ns); } -abstract_object_pointert pointer_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return read_dereference(env, ns); -} - abstract_object_pointert pointer_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.h b/src/analyses/variable-sensitivity/pointer_abstract_object.h index eed0659d1c2..4cfb6c9c8f6 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/pointer_abstract_object.h @@ -64,23 +64,6 @@ class pointer_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns); - /** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - */ - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.cpp b/src/analyses/variable-sensitivity/struct_abstract_object.cpp index 09f9a0ed37c..154b07fd658 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/struct_abstract_object.cpp @@ -45,21 +45,13 @@ abstract_object_pointert struct_abstract_objectt::expression_transform( { if(expr.id() == ID_member) { - return read(environment, expr, ns); + return read_component(environment, to_member_expr(expr), ns); } return abstract_objectt::expression_transform( expr, operands, environment, ns); } -abstract_object_pointert struct_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return this->read_component(env, to_member_expr(specifier), ns); -} - abstract_object_pointert struct_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/struct_abstract_object.h b/src/analyses/variable-sensitivity/struct_abstract_object.h index 63cd97a3234..b3282a82d14 100644 --- a/src/analyses/variable-sensitivity/struct_abstract_object.h +++ b/src/analyses/variable-sensitivity/struct_abstract_object.h @@ -63,23 +63,6 @@ class struct_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns); - /** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - */ - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/union_abstract_object.cpp b/src/analyses/variable-sensitivity/union_abstract_object.cpp index 447db275f6d..247e632f7a4 100644 --- a/src/analyses/variable-sensitivity/union_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/union_abstract_object.cpp @@ -36,14 +36,6 @@ union_abstract_objectt::union_abstract_objectt( PRECONDITION(ns.follow(expr.type()).id() == ID_union); } -abstract_object_pointert union_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - return read_component(env, to_member_expr(specifier), ns); -} - abstract_object_pointert union_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/union_abstract_object.h b/src/analyses/variable-sensitivity/union_abstract_object.h index 4339bb539cc..3e98c2233b1 100644 --- a/src/analyses/variable-sensitivity/union_abstract_object.h +++ b/src/analyses/variable-sensitivity/union_abstract_object.h @@ -42,23 +42,6 @@ class union_abstract_objectt : public abstract_objectt const abstract_environmentt &environment, const namespacet &ns); - /** - * A helper function to evaluate an abstract object contained - * within a container object. More precise abstractions may override this - * to return more precise results. - * - * \param env the abstract environment - * \param specifier a modifier expression, such as an array index or field - * specifier used to indicate access to a specific component - * \param ns the current namespace - * - * \return the abstract_objectt representing the value of the read component. - */ - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index ec3096832dd..0ea62399d71 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -111,18 +111,6 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( return resolve_new_values(resulting_objects); } -abstract_object_pointert value_set_abstract_objectt::read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const -{ - abstract_object_sett new_values; - for(const auto &st_value : values) - new_values.insert(st_value->read(env, specifier, ns)); - - return resolve_new_values(new_values); -} - abstract_object_pointert value_set_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index d5f154cfd48..1f78d5df817 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -89,14 +89,6 @@ class value_set_abstract_objectt : public abstract_valuet /// either converted to interval or marked as `top`. static const size_t max_value_set_size = 10; - /// \copydoc abstract_objectt::read - /// - /// Delegate reading to stored values. - abstract_object_pointert read( - const abstract_environmentt &env, - const exprt &specifier, - const namespacet &ns) const override; - /// \copydoc abstract_objectt::write /// /// Delegate writing to stored values. diff --git a/unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp index 805f27203ab..d251255568e 100644 --- a/unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp @@ -61,7 +61,8 @@ class array_utilt constant_array_abstract_object_pointert array_object, const index_exprt &index) const { - return array_object->read(enviroment, index, ns)->to_constant(); + return array_object->expression_transform(index, {}, enviroment, ns) + ->to_constant(); } private: diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp index 70fd010c2d1..452b8f45abb 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -42,7 +42,8 @@ class struct_utilt full_struct_abstract_objectt::constant_struct_pointert struct_object, const member_exprt &component) const { - return struct_object->read(enviroment, component, ns)->to_constant(); + return struct_object->expression_transform(component, {}, enviroment, ns) + ->to_constant(); } // At the moment the full_struct_abstract_object does not support From 7ead4af0d3ca31b8c07a1687c64ba30d692b76bb Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 15 Dec 2020 15:35:06 +0000 Subject: [PATCH 16/16] Remove redundant command line options --- regression/goto-analyzer/simple-union-access/test.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-analyzer/simple-union-access/test.desc b/regression/goto-analyzer/simple-union-access/test.desc index 1fc9abf3465..fdf58c00d49 100644 --- a/regression/goto-analyzer/simple-union-access/test.desc +++ b/regression/goto-analyzer/simple-union-access/test.desc @@ -1,6 +1,6 @@ CORE union.c ---variable-sensitivity --vsd --verify +--variable-sensitivity --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] line 13 x.a==0: UNKNOWN$