From be65c8a7ff959b6cdc01fc8c3b7a53592e0809e5 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 30 Jan 2021 23:41:26 +0000 Subject: [PATCH 1/5] Reorganised pointer representation hierarchy Introduce new base class, abstract_pointer_objectt. It should be, but is not yet, an abstract (in C++ terms) class as it's not intended to be directly instantiable. pointer_abstract_object now renamed two_value_pointer_abstract_objectt. constant_pointer_abstract_objectt and two_value_pointer_abstract_objectt are now peers. Deleted the unused value_set_pointer_abstract_objectt in anticipation of reintroducing a more functional value-set pointer representation shortly. --- scripts/expected_doxygen_warnings.txt | 4 +- src/analyses/Makefile | 24 +++--- .../abstract_environment.cpp | 2 +- ...object.cpp => abstract_pointer_object.cpp} | 35 ++++----- ...act_object.h => abstract_pointer_object.h} | 74 +++++-------------- .../constant_pointer_abstract_object.cpp | 22 +++--- .../constant_pointer_abstract_object.h | 8 +- .../two_value_pointer_abstract_object.h | 47 ++++++++++++ .../value_set_pointer_abstract_object.cpp | 23 ------ .../value_set_pointer_abstract_object.h | 30 -------- .../variable_sensitivity_domain.cpp | 2 +- .../variable_sensitivity_object_factory.cpp | 2 +- .../variable_sensitivity_object_factory.h | 2 +- unit/Makefile | 1 - .../value_set/pointer_abstract_object.cpp | 20 ----- 15 files changed, 112 insertions(+), 184 deletions(-) rename src/analyses/variable-sensitivity/{pointer_abstract_object.cpp => abstract_pointer_object.cpp} (72%) rename src/analyses/variable-sensitivity/{pointer_abstract_object.h => abstract_pointer_object.h} (59%) create mode 100644 src/analyses/variable-sensitivity/two_value_pointer_abstract_object.h delete mode 100644 src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp delete mode 100644 src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h delete mode 100644 unit/analyses/variable-sensitivity/value_set/pointer_abstract_object.cpp diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index a733c2bfa57..fe612650860 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -97,6 +97,6 @@ warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (1 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'std_types.h' not generated, too many nodes (122), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'std_expr.h' not generated, too many nodes (244), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'std_types.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 78ed45a9f1b..e03c312391a 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -33,29 +33,27 @@ SRC = ai.cpp \ static_analysis.cpp \ uncaught_exceptions_analysis.cpp \ uninitialized_domain.cpp \ - variable-sensitivity/abstract_object.cpp \ variable-sensitivity/abstract_environment.cpp \ + variable-sensitivity/abstract_object.cpp \ + variable-sensitivity/abstract_pointer_object.cpp \ variable-sensitivity/abstract_value_object.cpp \ variable-sensitivity/constant_abstract_value.cpp \ variable-sensitivity/constant_pointer_abstract_object.cpp \ variable-sensitivity/context_abstract_object.cpp \ - variable-sensitivity/write_location_context.cpp \ - variable-sensitivity/pointer_abstract_object.cpp \ - variable-sensitivity/variable_sensitivity_domain.cpp \ - variable-sensitivity/variable_sensitivity_object_factory.cpp \ - variable-sensitivity/full_struct_abstract_object.cpp \ - variable-sensitivity/full_array_abstract_object.cpp \ - variable-sensitivity/write_stack.cpp \ - variable-sensitivity/write_stack_entry.cpp \ variable-sensitivity/data_dependency_context.cpp \ - variable-sensitivity/value_set_abstract_object.cpp \ - variable-sensitivity/variable_sensitivity_dependence_graph.cpp \ + variable-sensitivity/full_array_abstract_object.cpp \ + variable-sensitivity/full_struct_abstract_object.cpp \ variable-sensitivity/interval_abstract_value.cpp \ + variable-sensitivity/three_way_merge_abstract_interpreter.cpp \ variable-sensitivity/value_set_abstract_object.cpp \ variable-sensitivity/value_set_abstract_value.cpp \ - variable-sensitivity/value_set_pointer_abstract_object.cpp \ - variable-sensitivity/three_way_merge_abstract_interpreter.cpp \ variable-sensitivity/variable_sensitivity_configuration.cpp \ + variable-sensitivity/variable_sensitivity_dependence_graph.cpp \ + variable-sensitivity/variable_sensitivity_domain.cpp \ + variable-sensitivity/variable_sensitivity_object_factory.cpp \ + variable-sensitivity/write_location_context.cpp \ + variable-sensitivity/write_stack.cpp \ + variable-sensitivity/write_stack_entry.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index 0d07c2d715b..76bb5f0325f 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -11,8 +11,8 @@ #include #include #include -#include #include +#include #include #include #include diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp similarity index 72% rename from src/analyses/variable-sensitivity/pointer_abstract_object.cpp rename to src/analyses/variable-sensitivity/abstract_pointer_object.cpp index b80692fd42c..cd9fd243142 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp @@ -5,20 +5,17 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com \*******************************************************************/ -#include -#include #include +#include -#include "pointer_abstract_object.h" - -pointer_abstract_objectt::pointer_abstract_objectt(const typet &t) +abstract_pointer_objectt::abstract_pointer_objectt(const typet &t) : abstract_objectt(t) { PRECONDITION(t.id() == ID_pointer); } -pointer_abstract_objectt::pointer_abstract_objectt( +abstract_pointer_objectt::abstract_pointer_objectt( const typet &type, bool top, bool bottom) @@ -27,7 +24,7 @@ pointer_abstract_objectt::pointer_abstract_objectt( PRECONDITION(type.id() == ID_pointer); } -pointer_abstract_objectt::pointer_abstract_objectt( +abstract_pointer_objectt::abstract_pointer_objectt( const exprt &e, const abstract_environmentt &environment, const namespacet &ns) @@ -36,22 +33,20 @@ pointer_abstract_objectt::pointer_abstract_objectt( PRECONDITION(e.type().id() == ID_pointer); } -abstract_object_pointert pointer_abstract_objectt::expression_transform( +abstract_object_pointert abstract_pointer_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_dereference(environment, ns); - } return abstract_objectt::expression_transform( expr, operands, environment, ns); } -abstract_object_pointert pointer_abstract_objectt::write( +abstract_object_pointert abstract_pointer_objectt::write( abstract_environmentt &environment, const namespacet &ns, const std::stack &stack, @@ -62,7 +57,7 @@ abstract_object_pointert pointer_abstract_objectt::write( return write_dereference(environment, ns, stack, value, merging_write); } -abstract_object_pointert pointer_abstract_objectt::read_dereference( +abstract_object_pointert abstract_pointer_objectt::read_dereference( const abstract_environmentt &env, const namespacet &ns) const { @@ -72,10 +67,8 @@ abstract_object_pointert pointer_abstract_objectt::read_dereference( return env.abstract_object_factory(pointed_to_type, ns, true, false); } -#include - -abstract_object_pointert pointer_abstract_objectt::write_dereference( - abstract_environmentt &environment, +abstract_object_pointert abstract_pointer_objectt::write_dereference( + abstract_environmentt &env, const namespacet &ns, const std::stack &stack, const abstract_object_pointert &value, @@ -83,16 +76,14 @@ abstract_object_pointert pointer_abstract_objectt::write_dereference( { if(is_top() || is_bottom()) { - environment.havoc("Writing to a 2value pointer"); + env.havoc("Writing to a 2value pointer"); return shared_from_this(); } - else - { - return std::make_shared(type(), true, false); - } + + return std::make_shared(type(), true, false); } -void pointer_abstract_objectt::get_statistics( +void abstract_pointer_objectt::get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, diff --git a/src/analyses/variable-sensitivity/pointer_abstract_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h similarity index 59% rename from src/analyses/variable-sensitivity/pointer_abstract_object.h rename to src/analyses/variable-sensitivity/abstract_pointer_object.h index 4cfb6c9c8f6..2afc81534a4 100644 --- a/src/analyses/variable-sensitivity/pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.h @@ -8,22 +8,21 @@ /// \file /// The base of all pointer abstractions -#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H -#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H - -#include +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H #include -class typet; -class constant_exprt; -class abstract_environmentt; +class abstract_pointer_tag +{ +}; -class pointer_abstract_objectt : public abstract_objectt +class abstract_pointer_objectt : public abstract_objectt, + public abstract_pointer_tag { public: /// \param type: the type the abstract_object is representing - explicit pointer_abstract_objectt(const typet &type); + explicit abstract_pointer_objectt(const typet &type); /// Start the abstract object at either top or bottom or neither /// Asserts if both top and bottom are true @@ -31,55 +30,24 @@ class pointer_abstract_objectt : public abstract_objectt /// \param type: the type the abstract_object is representing /// \param top: is the abstract_object starting as top /// \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; + abstract_pointer_objectt(const typet &type, bool top, bool bottom); /// \param expr: the expression to use as the starting pointer for /// an abstract object /// \param environment: the environment in which the pointer is being /// created /// \param ns: the current namespace - explicit pointer_abstract_objectt( + explicit abstract_pointer_objectt( const exprt &expr, const abstract_environmentt &environment, const namespacet &ns); - /** - * A helper function to evaluate writing to a component of an - * abstract object. More precise abstractions may override this to - * update what they are storing for a specific component. - * - * \param environment the abstract environment - * \param ns the current namespace - * \param stack the remaining stack of expressions on the LHS to evaluate - * \param specifier the expression uses to access a specific component - * \param value the value we are trying to write to the component - * \param merging_write if true, this and all future writes will be merged - * with the current value - * - * \return the abstract_objectt representing the result of writing - * to a specific component. - */ + abstract_object_pointert expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const override; + abstract_object_pointert write( abstract_environmentt &environment, const namespacet &ns, @@ -95,9 +63,7 @@ class pointer_abstract_objectt : public abstract_objectt const namespacet &ns) const override; protected: - CLONE - - /// A helper function to read elements from an array. More precise + /// Evaluate reading the pointer's value. More precise /// abstractions may override this to provide more precise results. /// /// \param env: the environment @@ -108,8 +74,8 @@ class pointer_abstract_objectt : public abstract_objectt const abstract_environmentt &env, const namespacet &ns) const; - /// A helper function to evaluate writing to a pointers value. More - /// precise abstractions may override this provide more precise results. + /// Evaluate writing to a pointer's value. More precise abstractions + /// may override this provide more precise results. /// /// \param environment: the abstract environment /// \param ns: the namespace @@ -132,4 +98,4 @@ class pointer_abstract_objectt : public abstract_objectt bool merging_write) const; }; -#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_POINTER_ABSTRACT_OBJECT_H +#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index 55530f9f019..7e0c17af007 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -18,7 +18,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt( const typet &type) - : pointer_abstract_objectt(type) + : abstract_pointer_objectt(type) { PRECONDITION(type.id() == ID_pointer); } @@ -27,14 +27,14 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt( const typet &type, bool top, bool bottom) - : pointer_abstract_objectt(type, top, bottom) + : abstract_pointer_objectt(type, top, bottom) { PRECONDITION(type.id() == ID_pointer); } constant_pointer_abstract_objectt::constant_pointer_abstract_objectt( const constant_pointer_abstract_objectt &old) - : pointer_abstract_objectt(old), value_stack(old.value_stack) + : abstract_pointer_objectt(old), value_stack(old.value_stack) { } @@ -42,7 +42,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt( const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) - : pointer_abstract_objectt(expr, environment, ns), + : abstract_pointer_objectt(expr, environment, ns), value_stack(expr, environment, ns) { PRECONDITION(expr.type().id() == ID_pointer); @@ -68,13 +68,13 @@ constant_pointer_abstract_objectt::merge(abstract_object_pointert other) const else { // TODO(tkiley): How do we set the result to be toppish? - return pointer_abstract_objectt::merge(other); + return abstract_pointer_objectt::merge(other); } } abstract_object_pointert constant_pointer_abstract_objectt::merge_constant_pointers( - const constant_pointer_abstract_pointert other) const + const constant_pointer_abstract_pointert &other) const { if(is_bottom()) { @@ -91,7 +91,7 @@ constant_pointer_abstract_objectt::merge_constant_pointers( } else { - return pointer_abstract_objectt::merge(other); + return abstract_pointer_objectt::merge(other); } } } @@ -100,7 +100,7 @@ exprt constant_pointer_abstract_objectt::to_constant() const { if(is_top() || is_bottom()) { - return pointer_abstract_objectt::to_constant(); + return abstract_pointer_objectt::to_constant(); } else { @@ -117,7 +117,7 @@ void constant_pointer_abstract_objectt::output( { if(is_top() || is_bottom() || value_stack.is_top_value()) { - pointer_abstract_objectt::output(out, ai, ns); + abstract_pointer_objectt::output(out, ai, ns); } else { @@ -180,7 +180,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference( { if(is_top() || is_bottom() || value_stack.is_top_value()) { - return pointer_abstract_objectt::write_dereference( + return abstract_pointer_objectt::write_dereference( environment, ns, stack, new_value, merging_write); } else @@ -225,7 +225,7 @@ void constant_pointer_abstract_objectt::get_statistics( const abstract_environmentt &env, const namespacet &ns) const { - pointer_abstract_objectt::get_statistics(statistics, visited, env, ns); + abstract_pointer_objectt::get_statistics(statistics, visited, env, ns); // don't bother following nullptr if(!is_top() && !is_bottom() && !value_stack.is_top_value()) { diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h index 448a1b0c770..06270928ae4 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h @@ -13,10 +13,10 @@ #include -#include +#include #include -class constant_pointer_abstract_objectt : public pointer_abstract_objectt +class constant_pointer_abstract_objectt : public abstract_pointer_objectt { private: typedef sharing_ptrt @@ -134,8 +134,8 @@ class constant_pointer_abstract_objectt : public pointer_abstract_objectt /// \return Returns a new abstract object that is the result of the merge /// unless the merge is the same as this abstract object, in which /// case it returns this. - abstract_object_pointert - merge_constant_pointers(const constant_pointer_abstract_pointert other) const; + abstract_object_pointert merge_constant_pointers( + const constant_pointer_abstract_pointert &other) const; write_stackt value_stack; }; diff --git a/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.h b/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.h new file mode 100644 index 00000000000..14a2293f823 --- /dev/null +++ b/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + + Module: analyses variable-sensitivity + + Author: Thomas Kiley, thomas.kiley@diffblue.com + +\*******************************************************************/ +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H + +#include + +class two_value_pointer_abstract_objectt : public abstract_pointer_objectt +{ +public: + /// \param type: the type the abstract_object is representing + explicit two_value_pointer_abstract_objectt(const typet &type) + : abstract_pointer_objectt(type) + { + } + + /// Start the abstract object at either top or bottom or neither + /// Asserts if both top and bottom are true + /// + /// \param type: the type the abstract_object is representing + /// \param top: is the abstract_object starting as top + /// \param bottom: is the abstract_object starting as bottom + two_value_pointer_abstract_objectt(const typet &type, bool top, bool bottom) + : abstract_pointer_objectt(type, top, bottom) + { + } + + /// \param expr: the expression to use as the starting pointer for + /// an abstract object + /// \param environment: the environment in which the pointer is being + /// created + /// \param ns: the current namespace + two_value_pointer_abstract_objectt( + const exprt &expr, + const abstract_environmentt &environment, + const namespacet &ns) + : abstract_pointer_objectt(expr, environment, ns) + { + } +}; + +#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp deleted file mode 100644 index 3fb70bcf9c6..00000000000 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ /dev/null @@ -1,23 +0,0 @@ - -/*******************************************************************\ - - Module: analyses variable-sensitivity variable-sensitivity-value-set - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include "value_set_pointer_abstract_object.h" - -abstract_object_pointert -value_set_pointer_abstract_objectt::merge(abstract_object_pointert other) const -{ - return shared_from_this(); -} - -value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( - const typet &type) - : pointer_abstract_objectt(type) -{ -} - diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h deleted file mode 100644 index aba059ad2b2..00000000000 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ /dev/null @@ -1,30 +0,0 @@ -/*******************************************************************\ - - Module: analyses variable-sensitivity variable-sensitivity-value-set - - Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Pointers pointing to a limited-size set of possible targets - -// NOLINTNEXTLINE(whitespace/line_length) -#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H -// NOLINTNEXTLINE(whitespace/line_length) -#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H - -#include "pointer_abstract_object.h" - -class value_set_pointer_abstract_objectt : public pointer_abstract_objectt -{ -public: - explicit value_set_pointer_abstract_objectt(const typet &type); - - abstract_object_pointert merge(abstract_object_pointert other) const override; - - CLONE -}; - -// NOLINTNEXTLINE(whitespace/line_length) -#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 768b2d47083..5d3d9988f13 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -10,7 +10,7 @@ Date: April 2016 #include -#include +#include #include #include diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index dadbc072842..81b9b32b6fc 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -158,7 +158,7 @@ variable_sensitivity_object_factoryt::get_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); case POINTER_INSENSITIVE: - return initialize_abstract_object( + return initialize_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); case POINTER_SENSITIVE: return initialize_abstract_object( diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h index 52d7a183500..27e298cbe53 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h @@ -22,8 +22,8 @@ #include #include #include -#include #include +#include #include #include #include diff --git a/unit/Makefile b/unit/Makefile index ff37116bb75..5c3dde99d43 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -24,7 +24,6 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ analyses/variable-sensitivity/value_set/abstract_value.cpp \ - analyses/variable-sensitivity/value_set/pointer_abstract_object.cpp \ ansi-c/max_malloc_size.cpp \ ansi-c/type2name.cpp \ big-int/big-int.cpp \ diff --git a/unit/analyses/variable-sensitivity/value_set/pointer_abstract_object.cpp b/unit/analyses/variable-sensitivity/value_set/pointer_abstract_object.cpp deleted file mode 100644 index a796d0a898e..00000000000 --- a/unit/analyses/variable-sensitivity/value_set/pointer_abstract_object.cpp +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for value set pointer abstract objects - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include "value_set_test_common.h" -#include - -TEST_CASE( - "A value set pointer abstract object created from type is top", - VALUE_SET_TEST_TAGS) -{ - value_set_pointer_abstract_objectt abstract_object( - pointer_typet(signedbv_typet{32}, 32)); - REQUIRE(abstract_object.is_top()); - REQUIRE(!abstract_object.is_bottom()); -} From 4bb4246ca55485da6b7becc250807d4c7e5164c1 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 2 Feb 2021 16:24:29 +0000 Subject: [PATCH 2/5] Divide value-set of values from value-set of pointers Stripped back value_set_abstract_object now it doesn't have to deal with pointers. Pulled out abstract_object_sett as a type not just an alias. Add behaviour with functions pulled across from value_set_abstract_objectt and value_set_pointer_abstract_objectt. --- src/analyses/Makefile | 2 + .../abstract_object_set.cpp | 36 ++ .../abstract_object_set.h | 83 +++++ .../value_set_abstract_object.cpp | 188 ++-------- .../value_set_abstract_object.h | 35 +- .../value_set_pointer_abstract_object.cpp | 322 ++++++++++++++++++ .../value_set_pointer_abstract_object.h | 115 +++++++ .../variable_sensitivity_configuration.cpp | 4 +- .../variable_sensitivity_configuration.h | 1 + .../variable_sensitivity_object_factory.cpp | 4 + 10 files changed, 594 insertions(+), 196 deletions(-) create mode 100644 src/analyses/variable-sensitivity/abstract_object_set.cpp create mode 100644 src/analyses/variable-sensitivity/abstract_object_set.h create mode 100644 src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp create mode 100644 src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h diff --git a/src/analyses/Makefile b/src/analyses/Makefile index e03c312391a..79bd7722dc8 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -35,6 +35,7 @@ SRC = ai.cpp \ uninitialized_domain.cpp \ variable-sensitivity/abstract_environment.cpp \ variable-sensitivity/abstract_object.cpp \ + variable-sensitivity/abstract_object_set.cpp \ variable-sensitivity/abstract_pointer_object.cpp \ variable-sensitivity/abstract_value_object.cpp \ variable-sensitivity/constant_abstract_value.cpp \ @@ -47,6 +48,7 @@ SRC = ai.cpp \ variable-sensitivity/three_way_merge_abstract_interpreter.cpp \ variable-sensitivity/value_set_abstract_object.cpp \ variable-sensitivity/value_set_abstract_value.cpp \ + variable-sensitivity/value_set_pointer_abstract_object.cpp \ variable-sensitivity/variable_sensitivity_configuration.cpp \ variable-sensitivity/variable_sensitivity_dependence_graph.cpp \ variable-sensitivity/variable_sensitivity_domain.cpp \ diff --git a/src/analyses/variable-sensitivity/abstract_object_set.cpp b/src/analyses/variable-sensitivity/abstract_object_set.cpp new file mode 100644 index 00000000000..8075d494fa8 --- /dev/null +++ b/src/analyses/variable-sensitivity/abstract_object_set.cpp @@ -0,0 +1,36 @@ +/*******************************************************************\ + + Module: analyses variable-sensitivity + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ + +#include +#include + +static bool by_length(const std::string &lhs, const std::string &rhs) +{ + if(lhs.size() < rhs.size()) + return true; + if(lhs.size() > rhs.size()) + return false; + return lhs < rhs; +} + +void abstract_object_sett::output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const +{ + std::vector output_values; + for(const auto &value : values) + { + std::ostringstream ss; + value->output(ss, ai, ns); + output_values.emplace_back(ss.str()); + } + std::sort(output_values.begin(), output_values.end(), by_length); + + join_strings(out, output_values.begin(), output_values.end(), ", "); +} diff --git a/src/analyses/variable-sensitivity/abstract_object_set.h b/src/analyses/variable-sensitivity/abstract_object_set.h new file mode 100644 index 00000000000..1f5de7b6974 --- /dev/null +++ b/src/analyses/variable-sensitivity/abstract_object_set.h @@ -0,0 +1,83 @@ +/*******************************************************************\ + + Module: analyses variable-sensitivity + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ + +/// \file +/// an unordered set of value objects + +#ifndef CBMC_ABSTRACT_OBJECT_SET_H +#define CBMC_ABSTRACT_OBJECT_SET_H + +#include +#include + +class abstract_object_sett +{ +public: + using value_sett = std::unordered_set< + abstract_object_pointert, + abstract_hashert, + abstract_equalert>; + using const_iterator = value_sett::const_iterator; + using value_type = value_sett::value_type; + using size_type = value_sett::size_type; + + void insert(const abstract_object_pointert &o) + { + values.insert(o); + } + void insert(abstract_object_pointert &&o) + { + values.insert(std::move(o)); + } + void insert(const abstract_object_sett &rhs) + { + values.insert(rhs.begin(), rhs.end()); + } + + abstract_object_pointert first() const + { + return *begin(); + } + + const_iterator begin() const + { + return values.begin(); + } + const_iterator end() const + { + return values.end(); + } + + value_sett::size_type size() const + { + return values.size(); + } + bool empty() const + { + return values.empty(); + } + + bool operator==(const abstract_object_sett &rhs) const + { + return values == rhs.values; + } + + void + output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const; + +private: + value_sett values; +}; + +class value_set_tag +{ +public: + virtual const abstract_object_sett &get_values() const = 0; +}; + +#endif //CBMC_ABSTRACT_OBJECT_SET_H diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index d15453b2e25..a60d277da63 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -15,9 +15,6 @@ #include #include #include -#include - -using abstract_object_sett = value_set_abstract_objectt::abstract_object_sett; class value_set_index_ranget : public index_ranget { @@ -53,18 +50,6 @@ index_range_ptrt make_value_set_index_range(const abstract_object_sett &vals) return std::make_shared(vals); } -/// Determine abstract-type of an abstract object \p other. -/// \param other: the abstract object to get the type of -/// \return the abstract-type of \p other -value_set_abstract_objectt::abstract_typet -get_type(const abstract_object_pointert &other); - -/// Determine abstract-type of an expression-type \p type. -/// \param type: the expression type to get the abstract-type of -/// \return the abstract-type of \p type -value_set_abstract_objectt::abstract_typet -type_to_abstract_type(const typet &type); - exprt rewrite_expression( const exprt &expr, const std::vector &ops); @@ -126,19 +111,9 @@ void for_each_comb(const std::vector &super_con, F f) } value_set_abstract_objectt::value_set_abstract_objectt(const typet &type) - : abstract_value_objectt(type), my_type(type_to_abstract_type(type)) + : abstract_value_objectt(type) { - switch(my_type) - { - case abstract_typet::POINTER: - values.insert(std::make_shared(type)); - break; - case abstract_typet::CONSTANT: - values.insert(std::make_shared(type)); - break; - case abstract_typet::UNSUPPORTED: - UNREACHABLE; - } + values.insert(std::make_shared(type)); verify(); } @@ -146,22 +121,9 @@ value_set_abstract_objectt::value_set_abstract_objectt( const typet &type, bool top, bool bottom) - : abstract_value_objectt(type, top, bottom), - my_type(type_to_abstract_type(type)) + : abstract_value_objectt(type, top, bottom) { - switch(my_type) - { - case abstract_typet::POINTER: - values.insert( - std::make_shared(type, top, bottom)); - break; - case abstract_typet::CONSTANT: - values.insert( - std::make_shared(type, top, bottom)); - break; - case abstract_typet::UNSUPPORTED: - UNREACHABLE; - } + values.insert(std::make_shared(type, top, bottom)); verify(); } @@ -169,22 +131,10 @@ value_set_abstract_objectt::value_set_abstract_objectt( const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) - : abstract_value_objectt(expr.type(), false, false), - my_type(type_to_abstract_type(expr.type())) + : abstract_value_objectt(expr.type(), false, false) { - switch(my_type) - { - case abstract_typet::POINTER: - values.insert(std::make_shared( - expr, environment, ns)); - break; - case abstract_typet::CONSTANT: - values.insert( - std::make_shared(expr, environment, ns)); - break; - case abstract_typet::UNSUPPORTED: - UNREACHABLE; - } + values.insert( + std::make_shared(expr, environment, ns)); verify(); } @@ -213,7 +163,7 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( abstract_object_sett resulting_objects; - auto dispatcher = *values.begin(); + auto dispatcher = values.first(); for_each_comb( collective_operands, [&resulting_objects, &dispatcher, &expr, &environment, &ns]( @@ -249,9 +199,9 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( abstract_object_sett resulting_objects; if(all_true || indeterminate) - resulting_objects.insert(true_result.begin(), true_result.end()); + resulting_objects.insert(true_result); if(all_false || indeterminate) - resulting_objects.insert(false_result.begin(), false_result.end()); + resulting_objects.insert(false_result); return resolve_new_values(resulting_objects, env); } @@ -290,44 +240,29 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values( auto unwrapped_values = unwrap_and_extract_values(new_values); - abstract_typet new_type = get_type(*unwrapped_values.begin()); - if( - unwrapped_values.size() > max_value_set_size && - new_type == abstract_typet::CONSTANT) + if(unwrapped_values.size() > max_value_set_size) { return to_interval(unwrapped_values); } - if(unwrapped_values.size() == 1 && new_type == abstract_typet::UNSUPPORTED) - { - return (*unwrapped_values.begin()); - } + //if(unwrapped_values.size() == 1) + //{ + // return (*unwrapped_values.begin()); + //} auto result = std::dynamic_pointer_cast(mutable_clone()); - - if( - unwrapped_values.size() > max_value_set_size || - new_type == abstract_typet::UNSUPPORTED) - { - result->set_top(); - } - else - { - result->set_values(unwrapped_values); - } + result->set_values(unwrapped_values); return result; } abstract_object_pointert value_set_abstract_objectt::merge(abstract_object_pointert other) const { - auto cast_other = - std::dynamic_pointer_cast(other); - if(cast_other && cast_other->get_my_type() == get_my_type()) + auto cast_other = std::dynamic_pointer_cast(other); + if(cast_other) { auto union_values = values; - union_values.insert( - cast_other->get_values().begin(), cast_other->get_values().end()); + union_values.insert(cast_other->get_values()); return resolve_values(union_values); } @@ -338,10 +273,6 @@ abstract_object_pointert value_set_abstract_objectt::to_interval( const abstract_object_sett &other_values) const { PRECONDITION(!other_values.empty()); - if(get_type(*other_values.begin()) == abstract_typet::POINTER) - return std::make_shared( - type(), true, false); - PRECONDITION(get_type(*other_values.begin()) == abstract_typet::CONSTANT); exprt lower_expr = (*other_values.begin())->to_constant(); exprt upper_expr = (*other_values.begin())->to_constant(); @@ -355,37 +286,15 @@ abstract_object_pointert value_set_abstract_objectt::to_interval( constant_interval_exprt(lower_expr, upper_expr)); } -bool value_set_abstract_objectt::verify() const -{ - CHECK_RETURN(my_type != abstract_typet::UNSUPPORTED); - for(const auto &value : values) - { - CHECK_RETURN( - !std::dynamic_pointer_cast(value)); - CHECK_RETURN(get_type(value) == my_type); - } - return true; -} - void value_set_abstract_objectt::set_values( const abstract_object_sett &other_values) { PRECONDITION(!other_values.empty()); set_not_top(); - my_type = get_type(*other_values.begin()); values = other_values; verify(); } -bool by_length(const std::string &lhs, const std::string &rhs) -{ - if(lhs.size() < rhs.size()) - return true; - if(lhs.size() > rhs.size()) - return false; - return lhs < rhs; -} - void value_set_abstract_objectt::output( std::ostream &out, const ai_baset &ai, @@ -403,58 +312,12 @@ void value_set_abstract_objectt::output( { out << "value-set-begin: "; - std::vector output_values; - for(const auto &value : values) - { - std::ostringstream ss; - value->output(ss, ai, ns); - output_values.emplace_back(ss.str()); - } - std::sort(output_values.begin(), output_values.end(), by_length); - - join_strings(out, output_values.begin(), output_values.end(), ", "); + values.output(out, ai, ns); out << " :value-set-end"; } } -value_set_abstract_objectt::abstract_typet -get_type(const abstract_object_pointert &other) -{ - using abstract_typet = value_set_abstract_objectt::abstract_typet; - - PRECONDITION( - !std::dynamic_pointer_cast(other)); - PRECONDITION(!std::dynamic_pointer_cast(other)); - PRECONDITION( - !std::dynamic_pointer_cast(other)); - - if(std::dynamic_pointer_cast(other)) - return abstract_typet::POINTER; - if(std::dynamic_pointer_cast(other)) - return abstract_typet::CONSTANT; - UNREACHABLE; - return abstract_typet::UNSUPPORTED; -} - -value_set_abstract_objectt::abstract_typet -type_to_abstract_type(const typet &type) -{ - using abstract_typet = value_set_abstract_objectt::abstract_typet; - - if(type.id() == ID_pointer) - return abstract_typet::POINTER; - - if( - type.id() == ID_signedbv || type.id() == ID_unsignedbv || - type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool || - type.id() == ID_integer || type.id() == ID_c_bit_field || - type.id() == ID_floatbv) - return abstract_typet::CONSTANT; - - return abstract_typet::UNSUPPORTED; -} - exprt rewrite_expression( const exprt &expr, const std::vector &ops) @@ -473,8 +336,8 @@ unwrap_operands(const std::vector &operands) for(const auto &op : operands) { - auto vsab = std::dynamic_pointer_cast( - maybe_unwrap_context(op)); + auto vsab = + std::dynamic_pointer_cast(maybe_unwrap_context(op)); INVARIANT(vsab, "should be a value set abstract object"); unwrapped.push_back(vsab->get_values()); } @@ -499,15 +362,14 @@ abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) { auto const &value_as_set = - std::dynamic_pointer_cast( - maybe_singleton); + std::dynamic_pointer_cast(maybe_singleton); if(value_as_set) { PRECONDITION(value_as_set->get_values().size() == 1); PRECONDITION(!std::dynamic_pointer_cast( - *value_as_set->get_values().begin())); + value_as_set->get_values().first())); - return *value_as_set->get_values().begin(); + return value_as_set->get_values().first(); } else return maybe_singleton; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 242b2108366..9c93f594400 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -12,21 +12,13 @@ #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H -#include - +#include #include -class value_set_abstract_objectt : public abstract_value_objectt +class value_set_abstract_objectt : public abstract_value_objectt, + public value_set_tag { public: - using value_set_abstract_object_ptrt = - std::shared_ptr; - - using abstract_object_sett = std::unordered_set< - abstract_object_pointert, - abstract_hashert, - abstract_equalert>; - /// \copydoc abstract_objectt::abstract_objectt(const typet&) explicit value_set_abstract_objectt(const typet &type); @@ -60,7 +52,7 @@ class value_set_abstract_objectt : public abstract_value_objectt /// Getter for the set of stored abstract objects. /// \return the values represented by this abstract object - const abstract_object_sett &get_values() const + const abstract_object_sett &get_values() const override { return values; } @@ -69,21 +61,6 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \param other_values: the new (non-empty) set of values void set_values(const abstract_object_sett &other_values); - /// Distinguish the type of abstract objects stored in this value-set. - enum class abstract_typet - { - CONSTANT, - POINTER, - UNSUPPORTED - }; - - /// Getter for the type of stored values - /// \return the abstract-type stored here - abstract_typet get_my_type() const - { - return my_type; - } - /// The threshold size for value-sets: past this threshold the object is /// either converted to interval or marked as `top`. static const size_t max_value_set_size = 10; @@ -134,7 +111,6 @@ class value_set_abstract_objectt : public abstract_value_objectt resolve_values(const abstract_object_sett &new_values) const; // data - abstract_typet my_type; abstract_object_sett values; /// Cast the set of values \p other_values to an interval. @@ -142,9 +118,6 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \return the interval-abstract-object containing \p other_values abstract_object_pointert to_interval(const abstract_object_sett &other_values) const; - - /// \copydoc abstract_objectt::verify - bool verify() const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp new file mode 100644 index 00000000000..729a85eac88 --- /dev/null +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -0,0 +1,322 @@ +/*******************************************************************\ + + Module: analyses variable-sensitivity + + Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Value Set of Pointer Abstract Object + +#include "abstract_aggregate_object.h" +#include +#include +#include + +static exprt rewrite_expression( + const exprt &expr, + const std::vector &ops); + +static std::vector +unwrap_operands(const std::vector &operands); + +static abstract_object_sett +unwrap_and_extract_values(const abstract_object_sett &values); + +/// Helper for converting singleton value sets into its only value. +/// \p maybe_singleton: either a set of abstract values or a single value +/// \return an abstract value without context +static abstract_object_pointert +maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); + +/// Helper for converting context objects into its abstract-value children +/// \p maybe_wrapped: either an abstract value (or a set of those) or one +/// wrapped in a context +/// \return an abstract value without context (though it might be as set) +static abstract_object_pointert +maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped); + +/// Recursively construct a combination \p sub_con from \p super_con and once +/// constructed call \p f. +/// \param super_con: vector of some containers storing the values +/// \param sub_con: the one combination being currently constructed +/// \param f: callable with side-effects +template +void apply_comb( + const std::vector &super_con, + std::vector &sub_con, + F f) +{ + size_t n = sub_con.size(); + if(n == super_con.size()) + f(sub_con); + else + { + for(const auto &value : super_con[n]) + { + sub_con.push_back(value); + apply_comb(super_con, sub_con, f); + sub_con.pop_back(); + } + } +} + +/// Call the function \p f on every combination of elements in \p super_con. +/// Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> -> +/// f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3). +/// \param super_con: vector of some containers storing the values +/// \param f: callable with side-effects +template +void for_each_comb(const std::vector &super_con, F f) +{ + std::vector sub_con; + apply_comb(super_con, sub_con, f); +} + +value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( + const typet &type) + : abstract_pointer_objectt(type) +{ + values.insert(std::make_shared(type)); +} + +value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( + const typet &type, + bool top, + bool bottom) + : abstract_pointer_objectt(type, top, bottom) +{ + values.insert( + std::make_shared(type, top, bottom)); +} + +value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( + const exprt &expr, + const abstract_environmentt &environment, + const namespacet &ns) + : abstract_pointer_objectt(expr.type(), false, false) +{ + values.insert( + std::make_shared(expr, environment, ns)); +} + +abstract_object_pointert +value_set_pointer_abstract_objectt::expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const +{ + PRECONDITION(operands.size() == expr.operands().size()); + + auto collective_operands = unwrap_operands(operands); + + if(expr.id() == ID_if) + return evaluate_conditional( + expr.type(), collective_operands, environment, ns); + + abstract_object_sett resulting_objects; + + auto dispatcher = values.first(); + for_each_comb( + collective_operands, + [&resulting_objects, &dispatcher, &expr, &environment, &ns]( + const std::vector &ops) { + auto rewritten_expr = rewrite_expression(expr, ops); + resulting_objects.insert( + dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); + }); + + return resolve_new_values(resulting_objects, environment); +} + +abstract_object_pointert +value_set_pointer_abstract_objectt::evaluate_conditional( + const typet &type, + const std::vector &operands, + const abstract_environmentt &env, + const namespacet &ns) const +{ + auto const condition = operands[0]; + + auto const true_result = operands[1]; + auto const false_result = operands[2]; + + auto all_true = true; + auto all_false = true; + for(auto v : condition) + { + auto expr = v->to_constant(); + all_true = all_true && expr.is_true(); + all_false = all_false && expr.is_false(); + } + auto indeterminate = !all_true && !all_false; + + abstract_object_sett resulting_objects; + if(all_true || indeterminate) + resulting_objects.insert(true_result); + if(all_false || indeterminate) + resulting_objects.insert(false_result); + return resolve_new_values(resulting_objects, env); +} + +abstract_object_pointert value_set_pointer_abstract_objectt::write( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const exprt &specifier, + const abstract_object_pointert &value, + bool merging_write) const +{ + abstract_object_sett new_values; + for(const auto &st_value : values) + { + new_values.insert( + st_value->write(environment, ns, stack, specifier, value, merging_write)); + } + return resolve_new_values(new_values, environment); +} + +abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment) const +{ + auto result = resolve_values(new_values); + return environment.add_object_context(result); +} + +abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values( + const abstract_object_sett &new_values) const +{ + PRECONDITION(!new_values.empty()); + + if(new_values == values) + return shared_from_this(); + + auto unwrapped_values = unwrap_and_extract_values(new_values); + + auto result = std::dynamic_pointer_cast( + mutable_clone()); + + if(unwrapped_values.size() > max_value_set_size) + { + result->set_top(); + } + else + { + result->set_values(unwrapped_values); + } + return result; +} + +abstract_object_pointert +value_set_pointer_abstract_objectt::merge(abstract_object_pointert other) const +{ + auto cast_other = std::dynamic_pointer_cast(other); + if(cast_other) + { + auto union_values = values; + union_values.insert(cast_other->get_values()); + return resolve_values(union_values); + } + + return abstract_objectt::merge(other); +} + +void value_set_pointer_abstract_objectt::set_values( + const abstract_object_sett &other_values) +{ + PRECONDITION(!other_values.empty()); + set_not_top(); + values = other_values; +} + +void value_set_pointer_abstract_objectt::output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const +{ + if(is_top()) + { + out << "TOP"; + } + else if(is_bottom()) + { + out << "BOTTOM"; + } + else + { + out << "value-set-begin: "; + + values.output(out, ai, ns); + + out << " :value-set-end"; + } +} + +exprt rewrite_expression( + const exprt &expr, + const std::vector &ops) +{ + auto operands_expr = exprt::operandst{}; + for(auto v : ops) + operands_expr.push_back(v->to_constant()); + auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr)); + return rewritten_expr; +} + +std::vector +unwrap_operands(const std::vector &operands) +{ + auto unwrapped = std::vector{}; + + for(const auto &op : operands) + { + auto vsab = + std::dynamic_pointer_cast(maybe_unwrap_context(op)); + INVARIANT(vsab, "should be a value set abstract object"); + unwrapped.push_back(vsab->get_values()); + } + + return unwrapped; +} + +abstract_object_sett +unwrap_and_extract_values(const abstract_object_sett &values) +{ + abstract_object_sett unwrapped_values; + for(auto const &value : values) + { + unwrapped_values.insert( + maybe_extract_single_value(maybe_unwrap_context(value))); + } + + return unwrapped_values; +} + +abstract_object_pointert +maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) +{ + auto const &value_as_set = + std::dynamic_pointer_cast(maybe_singleton); + if(value_as_set) + { + PRECONDITION(value_as_set->get_values().size() == 1); + PRECONDITION(!std::dynamic_pointer_cast( + value_as_set->get_values().first())); + + return value_as_set->get_values().first(); + } + else + return maybe_singleton; +} + +abstract_object_pointert +maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped) +{ + auto const &context_value = + std::dynamic_pointer_cast(maybe_wrapped); + + return context_value ? context_value->unwrap_context() : maybe_wrapped; +} diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h new file mode 100644 index 00000000000..62af1be3340 --- /dev/null +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -0,0 +1,115 @@ +/*******************************************************************\ + + Module: analyses variable-sensitivity + + Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Value Set of Pointer Abstract Object + +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H + +#include +#include + +class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, + public value_set_tag +{ +public: + /// \copydoc abstract_objectt::abstract_objectt(const typet&) + explicit value_set_pointer_abstract_objectt(const typet &type); + + /// \copydoc abstract_objectt::abstract_objectt(const typet &, bool, bool) + value_set_pointer_abstract_objectt(const typet &type, bool top, bool bottom); + + value_set_pointer_abstract_objectt( + const exprt &expr, + const abstract_environmentt &environment, + const namespacet &ns); + + /// \copydoc abstract_objectt::to_constant + exprt to_constant() const override + { + verify(); + return values.size() == 1 ? (*values.begin())->to_constant() + : abstract_objectt::to_constant(); + } + + /// \copydoc abstract_objectt::expression_transform + /// + /// Transforms the \p expr for every combination of \p operands (since these + /// can be value-sets as well). + abstract_object_pointert expression_transform( + const exprt &expr, + const std::vector &operands, + const abstract_environmentt &environment, + const namespacet &ns) const override; + + /// Getter for the set of stored abstract objects. + /// \return the values represented by this abstract object + const abstract_object_sett &get_values() const + { + return values; + } + + /// Setter for updating the stored values + /// \param other_values: the new (non-empty) set of values + void set_values(const abstract_object_sett &other_values); + + /// The threshold size for value-sets: past this threshold the object is + /// either converted to interval or marked as `top`. + static const size_t max_value_set_size = 10; + + /// \copydoc abstract_objectt::write + /// + /// Delegate writing to stored values. + abstract_object_pointert write( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const exprt &specifier, + const abstract_object_pointert &value, + bool merging_write) const override; + + void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) + const override; + +protected: + CLONE + + /// \copydoc abstract_object::merge + abstract_object_pointert merge(abstract_object_pointert other) const override; + +private: + abstract_object_pointert evaluate_conditional( + const typet &type, + const std::vector &operands, + const abstract_environmentt &env, + const namespacet &ns) const; + + /// Update the set of stored values to \p new_values. Build a new abstract + /// object of the right type if necessary. + /// \param new_values: potentially new set of values + /// \param environment: the abstract environment + /// \return the abstract object representing \p new_values (either 'this' or + /// something new) + abstract_object_pointert resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment) const; + + /// Update the set of stored values to \p new_values. Build a new abstract + /// object of the right type if necessary. + /// \param new_values: potentially new set of values + /// \return the abstract object representing \p new_values (either 'this' or + /// something new) + abstract_object_pointert + resolve_values(const abstract_object_sett &new_values) const; + + // data + abstract_object_sett values; +}; + +#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_POINTER_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index 33a96fc70fb..1ffc5f8bbbf 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp @@ -58,7 +58,7 @@ vsd_configt vsd_configt::value_set() { vsd_configt config{}; config.value_abstract_type = VALUE_SET; - config.pointer_abstract_type = VALUE_SET; + config.pointer_abstract_type = VALUE_SET_OF_POINTERS; config.struct_abstract_type = STRUCT_SENSITIVE; config.array_abstract_type = ARRAY_SENSITIVE; return config; @@ -83,7 +83,7 @@ const vsd_configt::option_mappingt vsd_configt::value_option_mappings = { const vsd_configt::option_mappingt vsd_configt::pointer_option_mappings = { {"top-bottom", POINTER_INSENSITIVE}, {"constants", POINTER_SENSITIVE}, - {"value-set", VALUE_SET}}; + {"value-set", VALUE_SET_OF_POINTERS}}; const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = { {"top-bottom", STRUCT_INSENSITIVE}, diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h index 29457b442cd..dc44535e061 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h @@ -21,6 +21,7 @@ enum ABSTRACT_OBJECT_TYPET INTERVAL, ARRAY_SENSITIVE, ARRAY_INSENSITIVE, + VALUE_SET_OF_POINTERS, POINTER_SENSITIVE, POINTER_INSENSITIVE, STRUCT_SENSITIVE, diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 81b9b32b6fc..8f8b71aaeb4 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -8,6 +8,7 @@ #include "variable_sensitivity_object_factory.h" #include "full_array_abstract_object.h" #include "value_set_abstract_value.h" +#include "value_set_pointer_abstract_object.h" template abstract_object_pointert @@ -163,6 +164,9 @@ variable_sensitivity_object_factoryt::get_abstract_object( case POINTER_SENSITIVE: return initialize_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); + case VALUE_SET_OF_POINTERS: + return initialize_abstract_object( + followed_type, top, bottom, e, environment, ns, configuration); case STRUCT_INSENSITIVE: return initialize_abstract_object( From 7d483d404397f3038236ef6c84b140033089dfd2 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Feb 2021 15:37:30 +0000 Subject: [PATCH 3/5] Dereferencing a value-set of pointers Remove expression_transform and write from value-set of pointers. Dereference value-set of pointers to a single value --- .../goto-analyzer/pointer-dereference/main.c | 11 ++ .../pointer-dereference/test-constants.desc | 7 ++ .../pointer-dereference/test-top-bottom.desc | 7 ++ .../pointer-dereference/test-value-sets.desc | 7 ++ .../abstract_pointer_object.h | 2 +- .../value_set_pointer_abstract_object.cpp | 112 ++---------------- .../value_set_pointer_abstract_object.h | 31 +---- 7 files changed, 48 insertions(+), 129 deletions(-) create mode 100644 regression/goto-analyzer/pointer-dereference/main.c create mode 100644 regression/goto-analyzer/pointer-dereference/test-constants.desc create mode 100644 regression/goto-analyzer/pointer-dereference/test-top-bottom.desc create mode 100644 regression/goto-analyzer/pointer-dereference/test-value-sets.desc diff --git a/regression/goto-analyzer/pointer-dereference/main.c b/regression/goto-analyzer/pointer-dereference/main.c new file mode 100644 index 00000000000..ea7b7207ec2 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int a = 10; + int *p = &a; + + int q = *p; + + assert(q == a); +} diff --git a/regression/goto-analyzer/pointer-dereference/test-constants.desc b/regression/goto-analyzer/pointer-dereference/test-constants.desc new file mode 100644 index 00000000000..9c6c0f0b7fa --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference/test-constants.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers constants +^\[main.assertion.1\] line 10 assertion q == a: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc b/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc new file mode 100644 index 00000000000..8c498fb94f7 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference/test-top-bottom.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers top-bottom +^\[main.assertion.1\] line 10 assertion q == a: UNKNOWN +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-dereference/test-value-sets.desc b/regression/goto-analyzer/pointer-dereference/test-value-sets.desc new file mode 100644 index 00000000000..5a2d3ecb552 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference/test-value-sets.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers value-set +^\[main.assertion.1\] line 10 assertion q == a: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h index 2afc81534a4..24e3792ba5c 100644 --- a/src/analyses/variable-sensitivity/abstract_pointer_object.h +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.h @@ -62,7 +62,6 @@ class abstract_pointer_objectt : public abstract_objectt, const abstract_environmentt &env, const namespacet &ns) const override; -protected: /// Evaluate reading the pointer's value. More precise /// abstractions may override this to provide more precise results. /// @@ -74,6 +73,7 @@ class abstract_pointer_objectt : public abstract_objectt, const abstract_environmentt &env, const namespacet &ns) const; +protected: /// Evaluate writing to a pointer's value. More precise abstractions /// may override this provide more precise results. /// 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 729a85eac88..8e1bc9f04e8 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -14,13 +14,6 @@ #include #include -static exprt rewrite_expression( - const exprt &expr, - const std::vector &ops); - -static std::vector -unwrap_operands(const std::vector &operands); - static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values); @@ -101,81 +94,25 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( std::make_shared(expr, environment, ns)); } -abstract_object_pointert -value_set_pointer_abstract_objectt::expression_transform( - const exprt &expr, - const std::vector &operands, - const abstract_environmentt &environment, - const namespacet &ns) const -{ - PRECONDITION(operands.size() == expr.operands().size()); - - auto collective_operands = unwrap_operands(operands); - - if(expr.id() == ID_if) - return evaluate_conditional( - expr.type(), collective_operands, environment, ns); - - abstract_object_sett resulting_objects; - - auto dispatcher = values.first(); - for_each_comb( - collective_operands, - [&resulting_objects, &dispatcher, &expr, &environment, &ns]( - const std::vector &ops) { - auto rewritten_expr = rewrite_expression(expr, ops); - resulting_objects.insert( - dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); - }); - - return resolve_new_values(resulting_objects, environment); -} - -abstract_object_pointert -value_set_pointer_abstract_objectt::evaluate_conditional( - const typet &type, - const std::vector &operands, +abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference( const abstract_environmentt &env, const namespacet &ns) const { - auto const condition = operands[0]; - - auto const true_result = operands[1]; - auto const false_result = operands[2]; - - auto all_true = true; - auto all_false = true; - for(auto v : condition) + if(is_top() || is_bottom()) { - auto expr = v->to_constant(); - all_true = all_true && expr.is_true(); - all_false = all_false && expr.is_false(); + return env.abstract_object_factory( + type().subtype(), ns, is_top(), !is_top()); } - auto indeterminate = !all_true && !all_false; - - abstract_object_sett resulting_objects; - if(all_true || indeterminate) - resulting_objects.insert(true_result); - if(all_false || indeterminate) - resulting_objects.insert(false_result); - return resolve_new_values(resulting_objects, env); -} -abstract_object_pointert value_set_pointer_abstract_objectt::write( - abstract_environmentt &environment, - const namespacet &ns, - const std::stack &stack, - const exprt &specifier, - const abstract_object_pointert &value, - bool merging_write) const -{ - abstract_object_sett new_values; - for(const auto &st_value : values) + abstract_object_sett results; + for(auto value : values) { - new_values.insert( - st_value->write(environment, ns, stack, specifier, value, merging_write)); + auto pointer = + std::dynamic_pointer_cast(value); + results.insert(pointer->read_dereference(env, ns)); } - return resolve_new_values(new_values, environment); + + return results.first(); } abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values( @@ -255,33 +192,6 @@ void value_set_pointer_abstract_objectt::output( } } -exprt rewrite_expression( - const exprt &expr, - const std::vector &ops) -{ - auto operands_expr = exprt::operandst{}; - for(auto v : ops) - operands_expr.push_back(v->to_constant()); - auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr)); - return rewritten_expr; -} - -std::vector -unwrap_operands(const std::vector &operands) -{ - auto unwrapped = std::vector{}; - - for(const auto &op : operands) - { - auto vsab = - std::dynamic_pointer_cast(maybe_unwrap_context(op)); - INVARIANT(vsab, "should be a value set abstract object"); - unwrapped.push_back(vsab->get_values()); - } - - return unwrapped; -} - abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values) { 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 62af1be3340..0ff08e28b61 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -38,19 +38,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, : abstract_objectt::to_constant(); } - /// \copydoc abstract_objectt::expression_transform - /// - /// Transforms the \p expr for every combination of \p operands (since these - /// can be value-sets as well). - abstract_object_pointert expression_transform( - const exprt &expr, - const std::vector &operands, - const abstract_environmentt &environment, - const namespacet &ns) const override; - /// Getter for the set of stored abstract objects. /// \return the values represented by this abstract object - const abstract_object_sett &get_values() const + const abstract_object_sett &get_values() const override { return values; } @@ -63,16 +53,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, /// either converted to interval or marked as `top`. static const size_t max_value_set_size = 10; - /// \copydoc abstract_objectt::write - /// - /// Delegate writing to stored values. - abstract_object_pointert write( - abstract_environmentt &environment, - const namespacet &ns, - const std::stack &stack, - const exprt &specifier, - const abstract_object_pointert &value, - bool merging_write) const override; + abstract_object_pointert read_dereference( + const abstract_environmentt &env, + const namespacet &ns) const override; void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; @@ -84,12 +67,6 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, abstract_object_pointert merge(abstract_object_pointert other) const override; private: - abstract_object_pointert evaluate_conditional( - const typet &type, - const std::vector &operands, - const abstract_environmentt &env, - const namespacet &ns) const; - /// Update the set of stored values to \p new_values. Build a new abstract /// object of the right type if necessary. /// \param new_values: potentially new set of values From 62e5320325b081d7115582a19436c9a694ff24b0 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Feb 2021 16:10:11 +0000 Subject: [PATCH 4/5] Test confirming dereferencing a pointer to an indeterminate value Test uses intervals. Value-sets should also work but we can't write that test yet as we needs more work on asserting value-set equality. --- .../main.c | 16 ++++++++++++++++ .../test-intervals-constants.desc | 7 +++++++ .../test-intervals-top-bottom.desc | 7 +++++++ .../test-intervals-value-sets.desc | 7 +++++++ 4 files changed, 37 insertions(+) create mode 100644 regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c create mode 100644 regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc create mode 100644 regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc create mode 100644 regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c b/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c new file mode 100644 index 00000000000..e501f842f30 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/main.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int unknown; + int a = 10; + + int *p = &a; + + if(unknown) + a = 15; + + int q = *p; + + assert(q == a); +} diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc new file mode 100644 index 00000000000..f688ea2ab0f --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-constants.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants +^\[main.assertion.1\] line 15 assertion q == a: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc new file mode 100644 index 00000000000..4be05332a55 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-top-bottom.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom +^\[main.assertion.1\] line 15 assertion q == a: UNKNOWN +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc new file mode 100644 index 00000000000..1468aca72f3 --- /dev/null +++ b/regression/goto-analyzer/pointer-dereference-indeterminate-values/test-intervals-value-sets.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set +^\[main.assertion.1\] line 15 assertion q == a: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- From df4160701c9f96f94b4d8641fc36ea28518567bb Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Feb 2021 16:16:17 +0000 Subject: [PATCH 5/5] Write through a value-set-pointer Tests determinate and indeterminate write through a pointer --- .../main.c | 17 +++++++++++++ .../test-intervals-constants.desc | 7 ++++++ .../test-intervals-top-bottom.desc | 7 ++++++ .../test-intervals-value-sets.desc | 7 ++++++ .../pointer-write-through/main.c | 11 +++++++++ .../pointer-write-through/test-constants.desc | 7 ++++++ .../test-top-bottom.desc | 7 ++++++ .../test-value-sets.desc | 7 ++++++ .../abstract_pointer_object.h | 1 - .../value_set_pointer_abstract_object.cpp | 24 +++++++++++++++++++ .../value_set_pointer_abstract_object.h | 7 ++++++ 11 files changed, 101 insertions(+), 1 deletion(-) create mode 100644 regression/goto-analyzer/pointer-write-through-indeterminate/main.c create mode 100644 regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc create mode 100644 regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc create mode 100644 regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc create mode 100644 regression/goto-analyzer/pointer-write-through/main.c create mode 100644 regression/goto-analyzer/pointer-write-through/test-constants.desc create mode 100644 regression/goto-analyzer/pointer-write-through/test-top-bottom.desc create mode 100644 regression/goto-analyzer/pointer-write-through/test-value-sets.desc diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/main.c b/regression/goto-analyzer/pointer-write-through-indeterminate/main.c new file mode 100644 index 00000000000..3e983a025ec --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through-indeterminate/main.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int unknown; + int a = 10; + int b = 10; + int *p = &a; + + if(unknown) + { + b = 15; + *p = 15; + } + + assert(*p == b); +} diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc new file mode 100644 index 00000000000..5f6414cd927 --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-constants.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers constants +^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc new file mode 100644 index 00000000000..fc850b8e590 --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-top-bottom.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers top-bottom +^\[main.assertion.1\] line 16 assertion \*p == b: UNKNOWN +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc new file mode 100644 index 00000000000..77ae5116c1d --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through-indeterminate/test-intervals-value-sets.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-values intervals --vsd-pointers value-set +^\[main.assertion.1\] line 16 assertion \*p == b: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-write-through/main.c b/regression/goto-analyzer/pointer-write-through/main.c new file mode 100644 index 00000000000..6a5cc63dca0 --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through/main.c @@ -0,0 +1,11 @@ +#include + +int main() +{ + int a = 10; + int *p = &a; + + *p = 15; + + assert(a == 15); +} diff --git a/regression/goto-analyzer/pointer-write-through/test-constants.desc b/regression/goto-analyzer/pointer-write-through/test-constants.desc new file mode 100644 index 00000000000..bd09812d2e2 --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through/test-constants.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers constants +^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc b/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc new file mode 100644 index 00000000000..7d2abb2834f --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through/test-top-bottom.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers top-bottom +^\[main.assertion.1\] line 10 assertion a == 15: UNKNOWN +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/pointer-write-through/test-value-sets.desc b/regression/goto-analyzer/pointer-write-through/test-value-sets.desc new file mode 100644 index 00000000000..32f0f02564f --- /dev/null +++ b/regression/goto-analyzer/pointer-write-through/test-value-sets.desc @@ -0,0 +1,7 @@ +CORE +main.c +--verify --variable-sensitivity --vsd-pointers value-set +^\[main.assertion.1\] line 10 assertion a == 15: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h index 24e3792ba5c..365cf710deb 100644 --- a/src/analyses/variable-sensitivity/abstract_pointer_object.h +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.h @@ -73,7 +73,6 @@ class abstract_pointer_objectt : public abstract_objectt, const abstract_environmentt &env, const namespacet &ns) const; -protected: /// Evaluate writing to a pointer's value. More precise abstractions /// may override this provide more precise results. /// 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 8e1bc9f04e8..f800c7b5f07 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -115,6 +115,30 @@ abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference( return results.first(); } +abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const abstract_object_pointert &new_value, + bool merging_write) const +{ + if(is_top() || is_bottom()) + { + return abstract_pointer_objectt::write_dereference( + environment, ns, stack, new_value, merging_write); + } + + for(auto value : values) + { + auto pointer = + std::dynamic_pointer_cast(value); + pointer->write_dereference( + environment, ns, stack, new_value, merging_write); + } + + return shared_from_this(); +} + abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values( const abstract_object_sett &new_values, const abstract_environmentt &environment) const 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 0ff08e28b61..b2cb6f0f8a2 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -57,6 +57,13 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, const abstract_environmentt &env, const namespacet &ns) const override; + abstract_object_pointert write_dereference( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const abstract_object_pointert &new_value, + bool merging_write) const override; + void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override;