From a33e0d0c71fadefd62fa1f8c69ea9572308ec155 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 18 May 2021 16:40:01 +0100 Subject: [PATCH 01/19] Add abstract_objectt::to_predicate Very basic initial implementation - top, bottom, or unknown. --- .../variable-sensitivity/abstract_object.cpp | 9 ++++ .../variable-sensitivity/abstract_object.h | 11 +++++ unit/Makefile | 1 + .../abstract_object/to_predicate.cpp | 48 ++++++++++++++++++ .../constant_abstract_value/to_predicate.cpp | 49 +++++++++++++++++++ 5 files changed, 118 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp create mode 100644 unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index c070a366884..9233a59c2c8 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -172,6 +172,15 @@ exprt abstract_objectt::to_constant() const return nil_exprt(); } +exprt abstract_objectt::to_predicate(exprt name) const +{ + if(is_top()) + return true_exprt(); + if(is_bottom()) + return false_exprt(); + return nil_exprt(); +} + void abstract_objectt::output( std::ostream &out, const ai_baset &ai, diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 171d88e0126..2fe69715754 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -171,6 +171,17 @@ class abstract_objectt : public std::enable_shared_from_this /// that allows an object to be built from a value. virtual exprt to_constant() const; + /// Converts to an invariant expression + /// + /// \param name - the variable name to substitute into the expression + /// \return Returns an exprt representing the object as an invariant. + /// + /// The the abstract element represents a single value the expression will + /// have the form _name = value_, if the value is an interval it will have the + /// the form _lower <= name <= upper_, etc. + /// If the value is bottom returns false, if top returns true. + exprt to_predicate(exprt name) const; + /** * A helper function to evaluate writing to a component of an * abstract object. More precise abstractions may override this to diff --git a/unit/Makefile b/unit/Makefile index 53e4f9acfad..9abe454d0ab 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ analyses/variable-sensitivity/abstract_object/merge.cpp \ analyses/variable-sensitivity/abstract_object/index_range.cpp \ + analyses/variable-sensitivity/abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..4e743bd73b4 --- /dev/null +++ b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp @@ -0,0 +1,48 @@ +/*******************************************************************\ + + Module: Tests for abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include + +SCENARIO( + "abstract object to predicate", + "[core][analyses][variable-sensitivity][abstract_object][to_predicate]") +{ + GIVEN("an abstract object") + { + WHEN("it is TOP") + { + auto obj = make_top_object(); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is true") + { + REQUIRE(pred == true_exprt()); + } + } + WHEN("it is BOTTOM") + { + auto obj = make_bottom_object(); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is false") + { + REQUIRE(pred == false_exprt()); + } + } + WHEN("it is neither TOP nor BOTTOM") + { + auto obj = std::make_shared(integer_typet(), false, false); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is nil") + { + REQUIRE(pred == nil_exprt()); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp new file mode 100644 index 00000000000..8d4c2ae7c67 --- /dev/null +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -0,0 +1,49 @@ +/*******************************************************************\ + + Module: Tests for abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include + +SCENARIO( + "constant_abstract_object to predicate", + "[core][analyses][variable-sensitivity][constant_abstract_value][to_predicate]") +{ + GIVEN("an abstract object") + { + WHEN("it is TOP") + { + auto obj = make_top_object(); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is true") + { + REQUIRE(pred == true_exprt()); + } + } + WHEN("it is BOTTOM") + { + auto obj = make_bottom_object(); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is false") + { + REQUIRE(pred == false_exprt()); + } + } + WHEN("it is neither TOP nor BOTTOM") + { + auto obj = + std::make_shared(integer_typet(), false, false); + auto pred = obj->to_predicate(nil_exprt()); + THEN("predicate is nil") + { + REQUIRE(pred == nil_exprt()); + } + } + } +} \ No newline at end of file From 5fa51fcf97437f510172232f62a71692913581c7 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 19 May 2021 11:00:01 +0100 Subject: [PATCH 02/19] constant_abstract_valuet::to_predicate --- .../variable-sensitivity/abstract_object.cpp | 7 ++- .../variable-sensitivity/abstract_object.h | 7 ++- .../constant_abstract_value.cpp | 5 +++ .../constant_abstract_value.h | 2 + unit/Makefile | 1 + .../abstract_object/to_predicate.cpp | 6 +-- .../constant_abstract_value/to_predicate.cpp | 45 +++++++++++++------ 7 files changed, 54 insertions(+), 19 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index 9233a59c2c8..5b4fe7553e7 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -172,12 +172,17 @@ exprt abstract_objectt::to_constant() const return nil_exprt(); } -exprt abstract_objectt::to_predicate(exprt name) const +exprt abstract_objectt::to_predicate(const exprt &name) const { if(is_top()) return true_exprt(); if(is_bottom()) return false_exprt(); + return to_predicate_internal(name); +} + +exprt abstract_objectt::to_predicate_internal(const exprt &name) const +{ return nil_exprt(); } diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 2fe69715754..6f35a117fc3 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -180,7 +180,7 @@ class abstract_objectt : public std::enable_shared_from_this /// have the form _name = value_, if the value is an interval it will have the /// the form _lower <= name <= upper_, etc. /// If the value is bottom returns false, if top returns true. - exprt to_predicate(exprt name) const; + exprt to_predicate(const exprt &name) const; /** * A helper function to evaluate writing to a component of an @@ -378,6 +378,11 @@ class abstract_objectt : public std::enable_shared_from_this { } + /// to_predicate implementation - derived classes will override + /// \param name - the variable name to substitute into the expression + /// \return Returns an exprt representing the object as an invariant. + virtual exprt to_predicate_internal(const exprt &name) const; + /** * Helper function for abstract_objectt::abstract_object_merge to perform any * additional actions after the base abstract_object_merge has completed it's diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 5b8b092bebf..915d3234c0b 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -144,6 +144,11 @@ abstract_value_pointert constant_abstract_valuet::constrain( return as_value(mutable_clone()); } +exprt constant_abstract_valuet::to_predicate_internal(const exprt &name) const +{ + return equal_exprt(name, value); +} + void constant_abstract_valuet::get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index 2e983f90e41..a23620c37a7 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -82,6 +82,8 @@ class constant_abstract_valuet : public abstract_value_objectt meet_with_value(const abstract_value_pointert &other) const override; private: + exprt to_predicate_internal(const exprt &name) const override; + exprt value; }; diff --git a/unit/Makefile b/unit/Makefile index 9abe454d0ab..9fb84bc8223 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -19,6 +19,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ + analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/eval.cpp \ analyses/variable-sensitivity/eval-member-access.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp index 4e743bd73b4..948085c23c8 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp @@ -6,13 +6,12 @@ \*******************************************************************/ -#include #include #include #include SCENARIO( - "abstract object to predicate", + "constant to predicate", "[core][analyses][variable-sensitivity][abstract_object][to_predicate]") { GIVEN("an abstract object") @@ -37,7 +36,8 @@ SCENARIO( } WHEN("it is neither TOP nor BOTTOM") { - auto obj = std::make_shared(integer_typet(), false, false); + auto obj = + std::make_shared(integer_typet(), false, false); auto pred = obj->to_predicate(nil_exprt()); THEN("predicate is nil") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index 8d4c2ae7c67..8fcd746a8f7 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ - Module: Tests for abstract_objectt::to_predicate + Module: Tests for constant_abstract_valuet::to_predicate Author: Jez Higgins @@ -9,17 +9,34 @@ #include #include #include -#include +#include +#include SCENARIO( - "constant_abstract_object to predicate", - "[core][analyses][variable-sensitivity][constant_abstract_value][to_predicate]") + "constant_abstract_value to predicate", + "[core][analyses][variable-sensitivity][constant_abstract_value][to_" + "predicate]") { - GIVEN("an abstract object") + const typet type = signedbv_typet(32); + const exprt val2 = from_integer(2, type); + + const exprt x_name = symbol_exprt(dstringt("x"), type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("constant_abstract_value") { WHEN("it is TOP") { - auto obj = make_top_object(); + auto obj = make_top_constant(); auto pred = obj->to_predicate(nil_exprt()); THEN("predicate is true") { @@ -28,22 +45,22 @@ SCENARIO( } WHEN("it is BOTTOM") { - auto obj = make_bottom_object(); + auto obj = make_bottom_constant(); auto pred = obj->to_predicate(nil_exprt()); THEN("predicate is false") { REQUIRE(pred == false_exprt()); } } - WHEN("it is neither TOP nor BOTTOM") + WHEN("x = 2") { - auto obj = - std::make_shared(integer_typet(), false, false); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is nil") + auto obj = make_constant(val2, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is x == 2") { - REQUIRE(pred == nil_exprt()); + auto repr = expr_to_str(pred); + REQUIRE(repr == "x == 2"); } } } -} \ No newline at end of file +} From 3b663b196d3ccf4877dd4c8c76c446036519303f Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 19 May 2021 11:24:02 +0100 Subject: [PATCH 03/19] interval_abstract_valuet::to_predicate --- .../interval_abstract_value.cpp | 11 +++ .../interval_abstract_value.h | 2 + unit/Makefile | 1 + .../interval_abstract_value/to_predicate.cpp | 78 +++++++++++++++++++ 4 files changed, 92 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 449b8d942a4..c293ac2eca1 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -463,6 +463,17 @@ abstract_value_pointert interval_abstract_valuet::constrain( make_interval(constant_interval_exprt(lower_bound, upper_bound))); } +exprt interval_abstract_valuet::to_predicate_internal(const exprt &name) const +{ + if(interval.is_single_value_interval()) + return equal_exprt(name, interval.get_lower()); + + auto lower_bound = binary_relation_exprt(interval.get_lower(), ID_le, name); + auto upper_bound = binary_relation_exprt(name, ID_le, interval.get_upper()); + + return and_exprt(lower_bound, upper_bound); +} + void interval_abstract_valuet::get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 45c04cbb3ef..7a7b55a2316 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -95,6 +95,8 @@ class interval_abstract_valuet : public abstract_value_objectt meet_with_value(const abstract_value_pointert &other) const override; private: + exprt to_predicate_internal(const exprt &name) const override; + constant_interval_exprt interval; void set_top_internal() override; diff --git a/unit/Makefile b/unit/Makefile index 9fb84bc8223..2088cd1dd63 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -26,6 +26,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp \ analyses/variable-sensitivity/interval_abstract_value/meet.cpp \ analyses/variable-sensitivity/interval_abstract_value/merge.cpp \ + analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp new file mode 100644 index 00000000000..4253bdf96d6 --- /dev/null +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp @@ -0,0 +1,78 @@ +/*******************************************************************\ + + Module: Tests for interval_abstract_valuet::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "interval_abstract_value to predicate", + "[core][analyses][variable-sensitivity][interval_abstract_value][to_" + "predicate]") +{ + const typet type = signedbv_typet(32); + const exprt val0 = from_integer(0, type); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + + const exprt x_name = symbol_exprt(dstringt("x"), type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("interval_abstract_value") + { + WHEN("it is TOP") + { + auto obj = make_top_interval(); + auto pred = obj->to_predicate(x_name); + THEN("predicate is true") + { + REQUIRE(pred == true_exprt()); + } + } + WHEN("it is BOTTOM") + { + auto obj = make_bottom_interval(); + auto pred = obj->to_predicate(x_name); + THEN("predicate is false") + { + REQUIRE(pred == false_exprt()); + } + } + WHEN("[ 2 ]") + { + auto obj = make_interval(val2, val2, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "x == 2"); + } + } + WHEN("[ 0, 2 ]") + { + auto obj = make_interval(val0, val2, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 2"); + } + } + } +} From f3dafafb190fb4b148bf37b1660a8fb2af494135 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 19 May 2021 13:27:31 +0100 Subject: [PATCH 04/19] value_set_abstract_objectt::to_predicate --- .../value_set_abstract_object.cpp | 20 +++ .../value_set_abstract_object.h | 6 +- unit/Makefile | 1 + .../to_predicate.cpp | 163 ++++++++++++++++++ 4 files changed, 188 insertions(+), 2 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 43a27ea1d64..9919f9263a7 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -119,6 +119,8 @@ static bool are_any_top(const abstract_object_sett &set); static bool is_set_extreme(const typet &type, const abstract_object_sett &set); static abstract_object_sett compact_values(const abstract_object_sett &values); +static abstract_object_sett +non_destructive_compact(const abstract_object_sett &values); static abstract_object_sett widen_value_set( const abstract_object_sett &values, const constant_interval_exprt &lhs, @@ -334,6 +336,24 @@ abstract_value_pointert value_set_abstract_objectt::constrain( return as_value(resolve_values(constrained_values)); } +exprt value_set_abstract_objectt::to_predicate_internal(const exprt &name) const +{ + auto compacted = non_destructive_compact(values); + if(compacted.size() == 1) + return compacted.first()->to_predicate(name); + + auto all_predicates = exprt::operandst{}; + std::transform( + compacted.begin(), + compacted.end(), + std::back_inserter(all_predicates), + [&name](const abstract_object_pointert &value) { + return value->to_predicate(name); + }); + + return or_exprt(all_predicates); +} + void value_set_abstract_objectt::output( std::ostream &out, const ai_baset &ai, diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index da672d1a988..cc57f592dc3 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -82,10 +82,12 @@ class value_set_abstract_objectt : public abstract_value_objectt, abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const; + void set_top_internal() override; + + exprt to_predicate_internal(const exprt &name) const override; + // data abstract_object_sett values; - - void set_top_internal() override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H diff --git a/unit/Makefile b/unit/Makefile index 2088cd1dd63..062c42a71b1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -37,6 +37,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp \ analyses/variable-sensitivity/value_set_abstract_object/meet.cpp \ analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \ + analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ ansi-c/expr2c.cpp \ diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..79627f512bd --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -0,0 +1,163 @@ +/*******************************************************************\ + + Module: Tests for value_set_abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "value_set_abstract_object to predicate", + "[core][analyses][variable-sensitivity][value_set_abstract_object][to_" + "predicate]") +{ + const typet type = signedbv_typet(32); + const exprt val0 = from_integer(0, type); + const exprt val1 = from_integer(1, type); + const exprt val2 = from_integer(2, type); + const exprt val3 = from_integer(3, type); + const exprt interval_0_1 = constant_interval_exprt(val0, val1); + const exprt interval_1_2 = constant_interval_exprt(val1, val2); + const exprt interval_0_2 = constant_interval_exprt(val1, val2); + const exprt interval_2_3 = constant_interval_exprt(val2, val3); + + const exprt x_name = symbol_exprt(dstringt("x"), type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("value_set_abstract_object") + { + WHEN("it is TOP") + { + auto obj = make_top_value_set(); + auto pred = obj->to_predicate(x_name); + THEN("predicate is true") + { + REQUIRE(pred == true_exprt()); + } + } + WHEN("it is BOTTOM") + { + auto obj = make_bottom_value_set(); + auto pred = obj->to_predicate(x_name); + THEN("predicate is false") + { + REQUIRE(pred == false_exprt()); + } + } + WHEN("{ 2 }") + { + auto obj = make_value_set(val2, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "x == 2"); + } + } + WHEN("{ 0, 2 }") + { + auto obj = make_value_set({val0, val2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is x == 0 || x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "x == 0 || x == 2"); + } + } + WHEN("{ 0, 1, 2 }") + { + auto obj = make_value_set({val0, val1, val2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is x == 0 || x == 1 || x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "x == 0 || x == 1 || x == 2"); + } + } + WHEN("{ [0, 1] }") + { + auto obj = make_value_set(interval_0_1, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 1") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 1"); + } + } + WHEN("{ [0, 1], 2 }") + { + auto obj = make_value_set({interval_0_1, val2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 1 || x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 1 || x == 2"); + } + } + WHEN("{ [0, 1], 2, 3 }") + { + auto obj = make_value_set({interval_0_1, val2, val3}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 1 || x == 3 || x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 1 || x == 3 || x == 2"); + } + } + WHEN("{ [0, 1], 1, 2 }") + { + auto obj = make_value_set({interval_0_1, val1, val2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 1 || x == 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 1 || x == 2"); + } + } + WHEN("{ [0, 1], [1, 2] }") + { + auto obj = make_value_set({interval_0_1, interval_1_2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 2"); + } + } + WHEN("{ [0, 2], [1, 2] }") + { + auto obj = make_value_set({interval_0_1, interval_1_2}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 2") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "0 <= x && x <= 2"); + } + } + WHEN("{ [0, 1], [2, 3] }") + { + auto obj = make_value_set({interval_0_1, interval_2_3}, environment, ns); + auto pred = obj->to_predicate(x_name); + THEN("predicate is 0 <= x && x <= 1 || 2 <= x && x <= 3") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "2 <= x && x <= 3 || 0 <= x && x <= 1"); + } + } + } +} From c0c2e7cc890ddbc8261d0f3a9b53512c859851ab Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 19 May 2021 15:41:56 +0100 Subject: [PATCH 05/19] Pulled out THEN_PREDICATE helper --- .../abstract_object/to_predicate.cpp | 12 +-- .../constant_abstract_value/to_predicate.cpp | 19 +---- .../interval_abstract_value/to_predicate.cpp | 26 +----- .../to_predicate.cpp | 81 ++++--------------- .../variable_sensitivity_test_helpers.cpp | 11 +++ .../variable_sensitivity_test_helpers.h | 4 + 6 files changed, 41 insertions(+), 112 deletions(-) diff --git a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp index 948085c23c8..d3f3bd33119 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp @@ -19,20 +19,12 @@ SCENARIO( WHEN("it is TOP") { auto obj = make_top_object(); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is true") - { - REQUIRE(pred == true_exprt()); - } + THEN_PREDICATE(obj, "TRUE"); } WHEN("it is BOTTOM") { auto obj = make_bottom_object(); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is false") - { - REQUIRE(pred == false_exprt()); - } + THEN_PREDICATE(obj, "FALSE"); } WHEN("it is neither TOP nor BOTTOM") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index 8fcd746a8f7..684179b81c3 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -37,30 +37,17 @@ SCENARIO( WHEN("it is TOP") { auto obj = make_top_constant(); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is true") - { - REQUIRE(pred == true_exprt()); - } + THEN_PREDICATE(obj, "TRUE"); } WHEN("it is BOTTOM") { auto obj = make_bottom_constant(); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is false") - { - REQUIRE(pred == false_exprt()); - } + THEN_PREDICATE(obj, "FALSE"); } WHEN("x = 2") { auto obj = make_constant(val2, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "x == 2"); - } + THEN_PREDICATE(obj, "x == 2"); } } } diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp index 4253bdf96d6..0f8ee5b8fea 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp @@ -39,40 +39,22 @@ SCENARIO( WHEN("it is TOP") { auto obj = make_top_interval(); - auto pred = obj->to_predicate(x_name); - THEN("predicate is true") - { - REQUIRE(pred == true_exprt()); - } + THEN_PREDICATE(obj, "TRUE"); } WHEN("it is BOTTOM") { auto obj = make_bottom_interval(); - auto pred = obj->to_predicate(x_name); - THEN("predicate is false") - { - REQUIRE(pred == false_exprt()); - } + THEN_PREDICATE(obj, "FALSE"); } WHEN("[ 2 ]") { auto obj = make_interval(val2, val2, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "x == 2"); - } + THEN_PREDICATE(obj, "x == 2"); } WHEN("[ 0, 2 ]") { auto obj = make_interval(val0, val2, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 2"); } } } diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp index 79627f512bd..b963978c767 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -44,40 +44,28 @@ SCENARIO( WHEN("it is TOP") { auto obj = make_top_value_set(); - auto pred = obj->to_predicate(x_name); - THEN("predicate is true") - { - REQUIRE(pred == true_exprt()); - } + THEN_PREDICATE(obj, "TRUE"); } WHEN("it is BOTTOM") { auto obj = make_bottom_value_set(); - auto pred = obj->to_predicate(x_name); - THEN("predicate is false") - { - REQUIRE(pred == false_exprt()); - } + THEN_PREDICATE(obj, "FALSE"); } WHEN("{ 2 }") { auto obj = make_value_set(val2, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "x == 2"); - } + THEN_PREDICATE(obj, "x == 2"); + } + WHEN("{ [2, 2] }") + { + auto obj = + make_value_set(constant_interval_exprt(val2, val2), environment, ns); + THEN_PREDICATE(obj, "x == 2"); } WHEN("{ 0, 2 }") { auto obj = make_value_set({val0, val2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is x == 0 || x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "x == 0 || x == 2"); - } + THEN_PREDICATE(obj, "x == 0 || x == 2"); } WHEN("{ 0, 1, 2 }") { @@ -92,72 +80,37 @@ SCENARIO( WHEN("{ [0, 1] }") { auto obj = make_value_set(interval_0_1, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 1") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 1"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 1"); } WHEN("{ [0, 1], 2 }") { auto obj = make_value_set({interval_0_1, val2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 1 || x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 1 || x == 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2"); } WHEN("{ [0, 1], 2, 3 }") { auto obj = make_value_set({interval_0_1, val2, val3}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 1 || x == 3 || x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 1 || x == 3 || x == 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 3 || x == 2"); } WHEN("{ [0, 1], 1, 2 }") { auto obj = make_value_set({interval_0_1, val1, val2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 1 || x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 1 || x == 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2"); } WHEN("{ [0, 1], [1, 2] }") { auto obj = make_value_set({interval_0_1, interval_1_2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 2"); } WHEN("{ [0, 2], [1, 2] }") { auto obj = make_value_set({interval_0_1, interval_1_2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "0 <= x && x <= 2"); - } + THEN_PREDICATE(obj, "0 <= x && x <= 2"); } WHEN("{ [0, 1], [2, 3] }") { auto obj = make_value_set({interval_0_1, interval_2_3}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is 0 <= x && x <= 1 || 2 <= x && x <= 3") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "2 <= x && x <= 3 || 0 <= x && x <= 1"); - } + THEN_PREDICATE(obj, "2 <= x && x <= 3 || 0 <= x && x <= 1"); } } } diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index ca66f243b9f..8976481cd56 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -521,3 +521,14 @@ std::shared_ptr add_as_value_set( REQUIRE(vs); return vs; } + +void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out) +{ + const auto x_name = symbol_exprt(dstringt("x"), obj->type()); + auto pred = obj->to_predicate(x_name); + THEN("predicate is " + out) + { + auto repr = expr_to_str(pred); + REQUIRE(repr == out); + } +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index f3fdf50acac..6bf4ba38956 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -251,4 +251,8 @@ std::shared_ptr add_as_value_set( std::string expr_to_str(const exprt &expr); std::string exprs_to_str(const std::vector &values); +void THEN_PREDICATE( + const abstract_object_pointert &obj, + const std::string &out); + #endif From b84e3608d0ca0e0a4dde4446662469991f62b74d Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 20 May 2021 09:11:52 +0100 Subject: [PATCH 06/19] Add context_abstract_object::to_predicate Relax to_predicate visibility from private to protected to enable this. --- src/analyses/variable-sensitivity/abstract_object.h | 10 +++++----- .../variable-sensitivity/constant_abstract_value.h | 2 +- .../variable-sensitivity/context_abstract_object.cpp | 5 +++++ .../variable-sensitivity/context_abstract_object.h | 2 ++ .../variable-sensitivity/interval_abstract_value.h | 2 +- .../variable-sensitivity/value_set_abstract_object.h | 4 ++-- 6 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index 6f35a117fc3..eb72dcc4a9a 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -363,6 +363,11 @@ class abstract_objectt : public std::enable_shared_from_this return shared_from_this() == other; } + /// to_predicate implementation - derived classes will override + /// \param name - the variable name to substitute into the expression + /// \return Returns an exprt representing the object as an invariant. + virtual exprt to_predicate_internal(const exprt &name) const; + private: /// To enforce copy-on-write these are private and have read-only accessors typet t; @@ -378,11 +383,6 @@ class abstract_objectt : public std::enable_shared_from_this { } - /// to_predicate implementation - derived classes will override - /// \param name - the variable name to substitute into the expression - /// \return Returns an exprt representing the object as an invariant. - virtual exprt to_predicate_internal(const exprt &name) const; - /** * Helper function for abstract_objectt::abstract_object_merge to perform any * additional actions after the base abstract_object_merge has completed it's diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index a23620c37a7..e2b23cf6736 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -81,9 +81,9 @@ class constant_abstract_valuet : public abstract_value_objectt abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; -private: exprt to_predicate_internal(const exprt &name) const override; +private: exprt value; }; diff --git a/src/analyses/variable-sensitivity/context_abstract_object.cpp b/src/analyses/variable-sensitivity/context_abstract_object.cpp index 969e6f7c91d..08f9e9d66a2 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/context_abstract_object.cpp @@ -160,6 +160,11 @@ abstract_object_pointert context_abstract_objectt::unwrap_context() const return child_abstract_object->unwrap_context(); } +exprt context_abstract_objectt::to_predicate_internal(const exprt &name) const +{ + return child_abstract_object->to_predicate(name); +} + void context_abstract_objectt::get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/context_abstract_object.h b/src/analyses/variable-sensitivity/context_abstract_object.h index 4e98f9fe2f1..c340a822303 100644 --- a/src/analyses/variable-sensitivity/context_abstract_object.h +++ b/src/analyses/variable-sensitivity/context_abstract_object.h @@ -117,6 +117,8 @@ class context_abstract_objectt : public abstract_objectt bool merging_write) const override; bool has_been_modified(const abstract_object_pointert &before) const override; + + exprt to_predicate_internal(const exprt &name) const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 7a7b55a2316..3ad901b0dea 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -94,9 +94,9 @@ class interval_abstract_valuet : public abstract_value_objectt abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; -private: exprt to_predicate_internal(const exprt &name) const override; +private: constant_interval_exprt interval; void set_top_internal() override; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index cc57f592dc3..239ec93c04e 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -69,6 +69,8 @@ class value_set_abstract_objectt : public abstract_value_objectt, abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override; + exprt to_predicate_internal(const exprt &name) const override; + private: /// Setter for updating the stored values /// \param other_values: the new (non-empty) set of values @@ -84,8 +86,6 @@ class value_set_abstract_objectt : public abstract_value_objectt, void set_top_internal() override; - exprt to_predicate_internal(const exprt &name) const override; - // data abstract_object_sett values; }; From a74af9cf7c39377b5cedf05574d7a4fed8e14e71 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 20 May 2021 09:56:03 +0100 Subject: [PATCH 07/19] Pull struct helpers out of full_struct merge unit tests --- unit/Makefile | 1 + .../full_struct_abstract_object/merge.cpp | 318 +++++++----------- .../struct_builder.cpp | 86 +++++ .../struct_builder.h | 38 +++ 4 files changed, 252 insertions(+), 191 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp create mode 100644 unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h diff --git a/unit/Makefile b/unit/Makefile index 062c42a71b1..da28338b507 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -29,6 +29,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ + analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \ 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 b23038bf5c7..0eac317b15b 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -16,80 +16,20 @@ #include #include #include +#include #include +#include #include #include typedef full_array_abstract_objectt::full_array_pointert full_array_abstract_object_pointert; -// Util - -class struct_utilt +exprt to_expr(int v) { -public: - struct_utilt(abstract_environmentt &enviroment, const namespacet &ns) - : enviroment(enviroment), ns(ns) - { - } - - exprt read_component( - full_struct_abstract_objectt::constant_struct_pointert struct_object, - const member_exprt &component) const - { - return struct_object->expression_transform(component, {}, enviroment, ns) - ->to_constant(); - } - - // At the moment the full_struct_abstract_object does not support - // initialization directly from an exprt so we manually write the components - full_struct_abstract_objectt::constant_struct_pointert - build_struct(const struct_exprt &starting_value) - { - std::shared_ptr result = - std::make_shared( - starting_value, enviroment, ns); - - struct_typet struct_type(to_struct_type(starting_value.type())); - size_t comp_index = 0; - for(const exprt &op : starting_value.operands()) - { - const auto &component = struct_type.components()[comp_index]; - std::shared_ptr new_result = result->write( - enviroment, - ns, - std::stack(), - member_exprt(nil_exprt(), component.get_name(), component.type()), - enviroment.eval(op, ns), - false); - result = std::dynamic_pointer_cast( - new_result); - - ++comp_index; - } - - return result; - } - - full_struct_abstract_objectt::constant_struct_pointert - build_top_struct(const typet &struct_type) - { - return std::make_shared( - struct_type, true, false); - } - - full_struct_abstract_objectt::constant_struct_pointert - build_bottom_struct(const typet &struct_type) - { - return std::make_shared( - struct_type, false, true); - } - -private: - abstract_environmentt &enviroment; - const namespacet ns; -}; + return from_integer(v, integer_typet()); +} SCENARIO( "merge_full_struct_abstract_object", @@ -99,26 +39,10 @@ SCENARIO( GIVEN("Two structs with 3 components, whose 1st component are the same") { // struct val1 = {.a = 1, .b = 2, .c = 3} - struct_typet struct_type; - struct_union_typet::componentt comp_a("a", integer_typet()); - struct_union_typet::componentt comp_b("b", integer_typet()); - struct_union_typet::componentt comp_c("c", integer_typet()); - struct_type.components().push_back(comp_a); - struct_type.components().push_back(comp_b); - struct_type.components().push_back(comp_c); - - exprt::operandst val1_op; - val1_op.push_back(from_integer(1, integer_typet())); - val1_op.push_back(from_integer(2, integer_typet())); - val1_op.push_back(from_integer(3, integer_typet())); - struct_exprt val1(val1_op, struct_type); - - // struct val1 = {.a = 1, .b = 4, .c = 5} - exprt::operandst val2_op; - val2_op.push_back(from_integer(1, integer_typet())); - val2_op.push_back(from_integer(4, integer_typet())); - val2_op.push_back(from_integer(5, integer_typet())); - struct_exprt val2(val2_op, struct_type); + auto val1 = std::map{{"a", 1}, {"b", 2}, {"c", 3}}; + + // struct val2 = {.a = 1, .b = 4, .c = 5} + auto val2 = std::map{{"a", 1}, {"b", 4}, {"c", 5}}; // index_exprt for reading from an array const member_exprt a(nil_exprt(), "a", integer_typet()); @@ -127,21 +51,19 @@ SCENARIO( auto object_factory = variable_sensitivity_object_factoryt::configured_with( vsd_configt::constant_domain()); - abstract_environmentt enviroment(object_factory); - enviroment.make_top(); + abstract_environmentt environment(object_factory); + environment.make_top(); symbol_tablet symbol_table; namespacet ns(symbol_table); - struct_utilt util(enviroment, ns); - WHEN("Merging two constant struct AOs with the same contents") { - auto op1 = util.build_struct(val1); - auto op2 = util.build_struct(val1); + auto op1 = build_struct(val1, environment, ns); + auto op2 = build_struct(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original struct AO should be returned") @@ -153,9 +75,15 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == val1.op0()); - REQUIRE(util.read_component(cast_result, b) == val1.op1()); - REQUIRE(util.read_component(cast_result, c) == val1.op2()); + REQUIRE( + read_component(cast_result, a, environment, ns) == + to_expr(val1["a"])); + REQUIRE( + read_component(cast_result, b, environment, ns) == + to_expr(val1["b"])); + REQUIRE( + read_component(cast_result, c, environment, ns) == + to_expr(val1["c"])); // Is optimal REQUIRE_FALSE(result.modified); @@ -163,12 +91,12 @@ SCENARIO( } WHEN("Merging two constant struct AOs with the different contents") { - auto op1 = util.build_struct(val1); - auto op2 = util.build_struct(val2); + auto op1 = build_struct(val1, environment, ns); + auto op2 = build_struct(val2, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN( @@ -182,9 +110,11 @@ SCENARIO( REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == val1.op0()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE( + read_component(cast_result, a, environment, ns) == + to_expr(val1["a"])); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // Since it has modified, we definitely shouldn't be reusing the pointer REQUIRE(result.modified); @@ -195,12 +125,12 @@ SCENARIO( "Merging a constant struct AO with a value " "with a constant struct AO set to top") { - auto op1 = util.build_struct(val1); - auto op2 = util.build_top_struct(struct_type); + auto op1 = build_struct(val1, environment, ns); + auto op2 = build_top_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("A new constant struct AO set to top should be returned") @@ -212,9 +142,9 @@ SCENARIO( REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == nil_exprt()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE(read_component(cast_result, a, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // We can't reuse the abstract object as the value has changed REQUIRE(result.modified); @@ -225,12 +155,12 @@ SCENARIO( "Merging a constant struct AO with a value " "with a constant struct AO set to bottom") { - auto op1 = util.build_struct(val1); - auto op2 = util.build_bottom_struct(struct_type); + auto op1 = build_struct(val1, environment, ns); + auto op2 = build_bottom_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original const AO should be returned") @@ -242,9 +172,15 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == val1.op0()); - REQUIRE(util.read_component(cast_result, b) == val1.op1()); - REQUIRE(util.read_component(cast_result, c) == val1.op2()); + REQUIRE( + read_component(cast_result, a, environment, ns) == + to_expr(val1["a"])); + REQUIRE( + read_component(cast_result, b, environment, ns) == + to_expr(val1["b"])); + REQUIRE( + read_component(cast_result, c, environment, ns) == + to_expr(val1["c"])); // Is optimal REQUIRE_FALSE(result.modified); @@ -255,12 +191,12 @@ SCENARIO( "Merging a constant struct AO set to top " "with a constant struct AO with a value") { - auto op1 = util.build_top_struct(struct_type); - auto op2 = util.build_struct(val1); + auto op1 = build_top_struct(); + auto op2 = build_struct(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original constant struct AO should be returned") @@ -272,9 +208,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == nil_exprt()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE(read_component(cast_result, a, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // Is optimal REQUIRE_FALSE(result.modified); @@ -285,12 +221,12 @@ SCENARIO( "Merging a constant struct AO set to top " "with a constant struct AO set to top") { - auto op1 = util.build_top_struct(struct_type); - auto op2 = util.build_top_struct(struct_type); + auto op1 = build_top_struct(); + auto op2 = build_top_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original constant struct AO should be returned") @@ -302,9 +238,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == nil_exprt()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE(read_component(cast_result, a, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // Is optimal REQUIRE_FALSE(result.modified); @@ -315,12 +251,12 @@ SCENARIO( "Merging a constant struct AO set to top " "with a constant struct AO set to bottom") { - auto op1 = util.build_top_struct(struct_type); - auto op2 = util.build_bottom_struct(struct_type); + auto op1 = build_top_struct(); + auto op2 = build_bottom_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original constant struct AO should be returned") @@ -332,9 +268,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == nil_exprt()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE(read_component(cast_result, a, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // Is optimal REQUIRE_FALSE(result.modified); @@ -345,12 +281,12 @@ SCENARIO( "Merging a constant struct AO set to bottom " "with a constant struct AO with a value") { - auto op1 = util.build_bottom_struct(struct_type); - auto op2 = util.build_struct(val1); + auto op1 = build_bottom_struct(); + auto op2 = build_struct(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("A new AO should be returned with op2s valuee") @@ -362,9 +298,15 @@ SCENARIO( REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == val1.op0()); - REQUIRE(util.read_component(cast_result, b) == val1.op1()); - REQUIRE(util.read_component(cast_result, c) == val1.op2()); + REQUIRE( + read_component(cast_result, a, environment, ns) == + to_expr(val1["a"])); + REQUIRE( + read_component(cast_result, b, environment, ns) == + to_expr(val1["b"])); + REQUIRE( + read_component(cast_result, c, environment, ns) == + to_expr(val1["c"])); // Is optimal REQUIRE(result.modified); @@ -375,12 +317,12 @@ SCENARIO( "Merging a constant struct AO set to bottom " "with a constant struct AO set to top") { - auto op1 = util.build_bottom_struct(struct_type); - auto op2 = util.build_top_struct(struct_type); + auto op1 = build_bottom_struct(); + auto op2 = build_top_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("A new constant struct AO should be returned set to top ") @@ -392,9 +334,9 @@ SCENARIO( REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == nil_exprt()); - REQUIRE(util.read_component(cast_result, b) == nil_exprt()); - REQUIRE(util.read_component(cast_result, c) == nil_exprt()); + REQUIRE(read_component(cast_result, a, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, b, environment, ns) == nil_exprt()); + REQUIRE(read_component(cast_result, c, environment, ns) == nil_exprt()); // Is optimal REQUIRE(result.modified); @@ -405,12 +347,12 @@ SCENARIO( "Merging a constant struct AO set to bottom " "with a constant struct AO set to bottom") { - auto op1 = util.build_bottom_struct(struct_type); - auto op2 = util.build_bottom_struct(struct_type); + auto op1 = build_bottom_struct(); + auto op2 = build_bottom_struct(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("The original bottom AO should be returned") @@ -432,13 +374,12 @@ SCENARIO( "Merging constant struct AO with value " "with a abstract object set to top") { - const auto &op1 = util.build_struct(val1); - const auto &op2 = - std::make_shared(val1.type(), true, false); + auto op1 = build_struct(val1, environment, ns); + auto op2 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); @@ -460,13 +401,12 @@ SCENARIO( "Merging constant struct AO with value " "with a abstract object set to bottom") { - const auto &op1 = util.build_struct(val1); - const auto &op2 = - std::make_shared(val1.type(), false, true); + auto op1 = build_struct(val1, environment, ns); + auto op2 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); THEN("We should get the same constant struct AO back") @@ -478,9 +418,15 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_component(cast_result, a) == val1.op0()); - REQUIRE(util.read_component(cast_result, b) == val1.op1()); - REQUIRE(util.read_component(cast_result, c) == val1.op2()); + REQUIRE( + read_component(cast_result, a, environment, ns) == + to_expr(val1["a"])); + REQUIRE( + read_component(cast_result, b, environment, ns) == + to_expr(val1["b"])); + REQUIRE( + read_component(cast_result, c, environment, ns) == + to_expr(val1["c"])); // Is optimal REQUIRE_FALSE(result.modified); @@ -491,9 +437,8 @@ SCENARIO( "Merging constant struct AO set to top " "with a abstract object set to top") { - const auto &op1 = util.build_top_struct(struct_type); - const auto &op2 = - std::make_shared(val1.type(), true, false); + auto op1 = build_top_struct(); + auto op2 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -508,7 +453,7 @@ SCENARIO( REQUIRE(result.object == op1); // Is type still correct - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); // Though we may become top or bottom, the type should be unchanged @@ -519,9 +464,8 @@ SCENARIO( "Merging constant struct AO set to top " "with a abstract object set to bottom") { - const auto &op1 = util.build_top_struct(struct_type); - const auto &op2 = - std::make_shared(val1.type(), false, true); + auto op1 = build_top_struct(); + auto op2 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Should get the same abstract object back") @@ -535,7 +479,7 @@ SCENARIO( REQUIRE(result.object == op1); // Is type still correct - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); // Though we may become top or bottom, the type should be unchanged @@ -546,9 +490,8 @@ SCENARIO( "Merging constant struct AO set to bottom " " with a abstract object set to top") { - const auto &op1 = util.build_bottom_struct(struct_type); - const auto &op2 = - std::make_shared(val1.type(), true, false); + auto op1 = build_bottom_struct(); + auto op2 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return a new top abstract object of the same type") @@ -561,7 +504,7 @@ SCENARIO( // We don't optimize for returning the second parameter if we can // Is type still correct - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); // Though we may become top or bottom, the type should be unchanged @@ -570,9 +513,8 @@ SCENARIO( } WHEN("Merging constant struct AO set to bottom with a AO set to bottom") { - const auto &op1 = util.build_bottom_struct(struct_type); - const auto &op2 = - std::make_shared(val1.type(), false, true); + auto op1 = build_bottom_struct(); + auto op2 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return the original abstract object") @@ -587,7 +529,7 @@ SCENARIO( REQUIRE(result.object == op1); // Is type still correct - const auto &cast_result = + auto cast_result = std::dynamic_pointer_cast( result.object); // Though we may become top or bottom, the type should be unchanged @@ -596,9 +538,8 @@ SCENARIO( } WHEN("Merging AO set to top with a constant struct AO with a value") { - const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_struct(val1); + auto op2 = build_struct(val1, environment, ns); + auto op1 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -614,9 +555,8 @@ SCENARIO( } WHEN("Merging AO set to top with a constant struct AO set to top") { - const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_top_struct(struct_type); + auto op2 = build_top_struct(); + auto op1 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -632,9 +572,8 @@ SCENARIO( } WHEN("Merging AO set to top with a constant struct AO set to bottom") { - const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_bottom_struct(struct_type); + auto op2 = build_bottom_struct(); + auto op1 = make_top_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -650,9 +589,8 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant struct AO with a value") { - const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_struct(val1); + auto op2 = build_struct(val1, environment, ns); + auto op1 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -670,9 +608,8 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant struct AO set to top") { - const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_top_struct(struct_type); + auto op2 = build_top_struct(); + auto op1 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -688,9 +625,8 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant struct AO set to bottom") { - const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_bottom_struct(struct_type); + auto op2 = build_bottom_struct(); + auto op1 = make_bottom_object(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp new file mode 100644 index 00000000000..693e89e01a9 --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp @@ -0,0 +1,86 @@ +/*******************************************************************\ + + Module: Unit tests helpers for structs + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ +#include +#include +#include + +full_struct_abstract_objectt::constant_struct_pointert build_struct( + const struct_exprt &starting_value, + abstract_environmentt &environment, + const namespacet &ns) +{ + auto result = std::make_shared( + starting_value, environment, ns); + + auto struct_type = to_struct_type(starting_value.type()); + size_t comp_index = 0; + for(const exprt &op : starting_value.operands()) + { + const auto &component = struct_type.components()[comp_index]; + auto new_result = result->write( + environment, + ns, + std::stack(), + member_exprt(nil_exprt(), component.get_name(), component.type()), + environment.eval(op, ns), + false); + + result = + std::dynamic_pointer_cast(new_result); + + ++comp_index; + } + + return result; +} + +full_struct_abstract_objectt::constant_struct_pointert build_struct( + const std::map &members, + abstract_environmentt &environment, + const namespacet &ns) +{ + struct_typet struct_type; + exprt::operandst val1_op; + + for(auto &member : members) + { + auto component = + struct_union_typet::componentt(member.first, integer_typet()); + struct_type.components().push_back(component); + + auto value = from_integer(member.second, integer_typet()); + val1_op.push_back(value); + } + + auto val1 = struct_exprt(val1_op, struct_type); + return build_struct(val1, environment, ns); +} + +full_struct_abstract_objectt::constant_struct_pointert build_top_struct() +{ + struct_typet struct_type; + return std::make_shared( + struct_type, true, false); +} + +full_struct_abstract_objectt::constant_struct_pointert build_bottom_struct() +{ + struct_typet struct_type; + return std::make_shared( + struct_type, false, true); +} + +exprt read_component( + full_struct_abstract_objectt::constant_struct_pointert struct_object, + const member_exprt &component, + const abstract_environmentt &environment, + const namespacet &ns) +{ + return struct_object->expression_transform(component, {}, environment, ns) + ->to_constant(); +} diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h new file mode 100644 index 00000000000..28078bd94f2 --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h @@ -0,0 +1,38 @@ +/*******************************************************************\ + + Module: Unit tests helpers for structs + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H + +#include + +#include + +class abstract_environmentt; +class namespacet; + +full_struct_abstract_objectt::constant_struct_pointert build_struct( + const struct_exprt &starting_value, + abstract_environmentt &environment, + const namespacet &ns); + +full_struct_abstract_objectt::constant_struct_pointert build_struct( + const std::map &members, + abstract_environmentt &environment, + const namespacet &ns); + +exprt read_component( + full_struct_abstract_objectt::constant_struct_pointert struct_object, + const member_exprt &component, + const abstract_environmentt &environment, + const namespacet &ns); + +full_struct_abstract_objectt::constant_struct_pointert build_top_struct(); + +full_struct_abstract_objectt::constant_struct_pointert build_bottom_struct(); + +#endif From 3e6302cff731d83d0f952358d754fe8daa1fc801 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 20 May 2021 12:21:04 +0100 Subject: [PATCH 08/19] full_struct_abstract_objectt::to_predicate --- .../full_struct_abstract_object.cpp | 21 ++++++ .../full_struct_abstract_object.h | 2 + unit/Makefile | 1 + .../struct_builder.cpp | 6 +- .../struct_builder.h | 3 +- .../to_predicate.cpp | 75 +++++++++++++++++++ 6 files changed, 105 insertions(+), 3 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index 1911bab4c47..403b923243e 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -307,6 +307,27 @@ abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements( } } +exprt full_struct_abstract_objectt::to_predicate_internal( + const exprt &name) const +{ + auto all_predicates = exprt::operandst{}; + + for(auto field : map.get_sorted_view()) + { + auto field_name = member_exprt(name, field.first, name.type()); + auto field_expr = field.second->to_predicate(field_name); + + if(!field_expr.is_true()) + all_predicates.push_back(field_expr); + } + + if(all_predicates.empty()) + return true_exprt(); + if(all_predicates.size() == 1) + return all_predicates.front(); + return and_exprt(all_predicates); +} + void full_struct_abstract_objectt::statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.h b/src/analyses/variable-sensitivity/full_struct_abstract_object.h index f587278d734..cf39c399267 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.h @@ -169,6 +169,8 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt< abstract_object_pointert merge( const abstract_object_pointert &other, const widen_modet &widen_mode) const override; + + exprt to_predicate_internal(const exprt &name) const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H diff --git a/unit/Makefile b/unit/Makefile index da28338b507..85477c911c6 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -30,6 +30,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \ + analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \ diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp index 693e89e01a9..1725466161d 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp @@ -53,8 +53,10 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct( struct_union_typet::componentt(member.first, integer_typet()); struct_type.components().push_back(component); - auto value = from_integer(member.second, integer_typet()); - val1_op.push_back(value); + if(member.second != TOP_MEMBER) + val1_op.push_back(from_integer(member.second, integer_typet())); + else + val1_op.push_back(nil_exprt()); } auto val1 = struct_exprt(val1_op, struct_type); diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h index 28078bd94f2..f1a9e069cc9 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.h @@ -8,7 +8,7 @@ #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_STRUCT_BUILDER_H -#include +#include #include @@ -20,6 +20,7 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct( abstract_environmentt &environment, const namespacet &ns); +const int TOP_MEMBER = std::numeric_limits::max(); full_struct_abstract_objectt::constant_struct_pointert build_struct( const std::map &members, abstract_environmentt &environment, diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..5f145b03d65 --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp @@ -0,0 +1,75 @@ +/*******************************************************************\ + + Module: Tests for full_struct_abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include + +#include +#include +#include + +#include +#include + +SCENARIO( + "struct to predicate", + "[core][analyses][variable-sensitivity][full_struct_abstract_object][to_" + "predicate]") +{ + auto object_factory = variable_sensitivity_object_factoryt::configured_with( + vsd_configt::constant_domain()); + abstract_environmentt environment(object_factory); + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("full_struct_abstract_object to predicate") + { + WHEN("it is TOP") + { + auto obj = build_top_struct(); + THEN_PREDICATE(obj, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto obj = build_bottom_struct(); + THEN_PREDICATE(obj, "FALSE"); + } + WHEN("{ .a = 1 }") + { + auto obj = build_struct({{"a", 1}}, environment, ns); + THEN_PREDICATE(obj, "x.a == 1"); + } + WHEN("{ .a = 1, .b = 2, .c = 3 }") + { + auto obj = build_struct({{"a", 1}, {"b", 2}, {"c", 3}}, environment, ns); + THEN_PREDICATE(obj, "x.a == 1 && x.b == 2 && x.c == 3"); + } + WHEN("{ .a = 1, .b = 2, .c = TOP }") + { + auto obj = + build_struct({{"a", 1}, {"b", 2}, {"c", TOP_MEMBER}}, environment, ns); + THEN_PREDICATE(obj, "x.a == 1 && x.b == 2"); + } + WHEN("{ .a = TOP, .b = 2, .c = TOP }") + { + auto obj = build_struct( + {{"a", TOP_MEMBER}, {"b", 2}, {"c", TOP_MEMBER}}, environment, ns); + THEN_PREDICATE(obj, "x.b == 2"); + } + WHEN("{ .a = TOP, .b = TOP, .c = TOP }") + { + auto obj = build_struct( + {{"a", TOP_MEMBER}, {"b", TOP_MEMBER}, {"c", TOP_MEMBER}}, + environment, + ns); + THEN_PREDICATE(obj, "TRUE"); + } + } +} From d55329c93da15b9caa7faae6548fac4730703dda Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 20 May 2021 15:59:13 +0100 Subject: [PATCH 09/19] Pull array helpers out of full_array merge unit tests --- unit/Makefile | 1 + .../array_builder.cpp | 63 +++++ .../array_builder.h | 33 +++ .../full_array_abstract_object/merge.cpp | 243 +++++++----------- .../full_struct_abstract_object/merge.cpp | 19 +- .../variable_sensitivity_test_helpers.cpp | 6 + .../variable_sensitivity_test_helpers.h | 1 + 7 files changed, 207 insertions(+), 159 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp create mode 100644 unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h diff --git a/unit/Makefile b/unit/Makefile index 85477c911c6..01ae29de7bb 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -28,6 +28,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/interval_abstract_value/merge.cpp \ analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ + analyses/variable-sensitivity/full_struct_abstract_object/array_builder.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp \ diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp new file mode 100644 index 00000000000..13f22be6f51 --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp @@ -0,0 +1,63 @@ +/*******************************************************************\ + + Module: Unit tests helpers for arrays + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +full_array_abstract_objectt::full_array_pointert build_array( + const exprt &array_expr, + abstract_environmentt &environment, + const namespacet &ns) +{ + return std::make_shared( + array_expr, environment, ns); +} + +full_array_abstract_objectt::full_array_pointert build_array( + const std::vector &array, + abstract_environmentt &environment, + const namespacet &ns) +{ + const array_typet array_type( + integer_typet(), from_integer(array.size(), integer_typet())); + + exprt::operandst element_ops; + + for(auto element : array) + element_ops.push_back(from_integer(element, integer_typet())); + + auto array_expr = array_exprt(element_ops, array_type); + return build_array(array_expr, environment, ns); +} + +full_array_abstract_objectt::full_array_pointert build_top_array() +{ + auto array_type = + array_typet(integer_typet(), from_integer(3, integer_typet())); + return std::make_shared(array_type, true, false); +} + +full_array_abstract_objectt::full_array_pointert build_bottom_array() +{ + auto array_type = + array_typet(integer_typet(), from_integer(3, integer_typet())); + return std::make_shared(array_type, false, true); +} + +exprt read_index( + full_array_abstract_objectt::full_array_pointert array_object, + const index_exprt &index, + abstract_environmentt &environment, + const namespacet &ns) +{ + return array_object->expression_transform(index, {}, environment, ns) + ->to_constant(); +} diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h new file mode 100644 index 00000000000..99ff94d95be --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + + Module: Unit tests helpers for arrays + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ +#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_ARRAY_BUILDER_H +#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_ARRAY_BUILDER_H + +#include + +full_array_abstract_objectt::full_array_pointert build_array( + const exprt &array_expr, + abstract_environmentt &environment, + const namespacet &ns); + +full_array_abstract_objectt::full_array_pointert build_array( + const std::vector &array, + abstract_environmentt &environment, + const namespacet &ns); + +full_array_abstract_objectt::full_array_pointert build_top_array(); + +full_array_abstract_objectt::full_array_pointert build_bottom_array(); + +exprt read_index( + full_array_abstract_objectt::full_array_pointert array_object, + const index_exprt &index, + abstract_environmentt &environment, + const namespacet &ns); + +#endif diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp index b95b949d9ce..bfcb08db072 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ - Module: Unit tests for constant_array_abstract_object::merge + Module: Unit tests for full_array_abstract_objectt::merge Author: DiffBlue Limited. @@ -8,63 +8,19 @@ #include #include -#include -#include -#include #include #include #include +#include #include +#include + #include #include - -typedef full_array_abstract_objectt::full_array_pointert - full_array_abstract_object_pointert; - -// Util - -class array_utilt -{ -public: - array_utilt(const abstract_environmentt &enviroment, const namespacet &ns) - : enviroment(enviroment), ns(ns) - { - } - - full_array_abstract_objectt::full_array_pointert - build_array(const exprt &array_expr) - { - return std::make_shared( - array_expr, enviroment, ns); - } - - full_array_abstract_objectt::full_array_pointert - build_top_array(const typet &array_type) - { - return std::make_shared( - array_type, true, false); - } - - full_array_abstract_objectt::full_array_pointert - build_bottom_array(const typet &array_type) - { - return std::make_shared( - array_type, false, true); - } - - exprt read_index( - full_array_abstract_object_pointert array_object, - const index_exprt &index) const - { - return array_object->expression_transform(index, {}, enviroment, ns) - ->to_constant(); - } - -private: - const abstract_environmentt &enviroment; - const namespacet ns; -}; +#include +#include +#include SCENARIO( "merge_constant_array_abstract_object", @@ -73,22 +29,10 @@ SCENARIO( { GIVEN("Two arrays of size 3, whose first elements are the same") { - const array_typet array_type( - integer_typet(), from_integer(3, integer_typet())); - - // int val1[3] = {1, 2, 3} - exprt::operandst val1_op; - val1_op.push_back(from_integer(1, integer_typet())); - val1_op.push_back(from_integer(2, integer_typet())); - val1_op.push_back(from_integer(3, integer_typet())); - exprt val1 = array_exprt(val1_op, array_type); - + // int val2[3] = {1, 2, 3} + auto val1 = std::vector{1, 2, 3}; // int val2[3] = {1, 4, 5} - exprt::operandst val2_op; - val2_op.push_back(from_integer(1, integer_typet())); - val2_op.push_back(from_integer(4, integer_typet())); - val2_op.push_back(from_integer(5, integer_typet())); - exprt val2 = array_exprt(val2_op, array_type); + auto val2 = std::vector{1, 4, 5}; // index_exprt for reading from an array const index_exprt i0 = @@ -100,17 +44,15 @@ SCENARIO( auto object_factory = variable_sensitivity_object_factoryt::configured_with( vsd_configt::constant_domain()); - abstract_environmentt enviroment(object_factory); - enviroment.make_top(); + abstract_environmentt environment(object_factory); + environment.make_top(); symbol_tablet symbol_table; namespacet ns(symbol_table); - array_utilt util(enviroment, ns); - WHEN("Merging two constant array AOs with the same array") { - auto op1 = util.build_array(val1); - auto op2 = util.build_array(val1); + auto op1 = build_array(val1, environment, ns); + auto op2 = build_array(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -126,9 +68,12 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == val1.operands()[0]); - REQUIRE(util.read_index(cast_result, i1) == val1.operands()[1]); - REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); + REQUIRE( + read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); + REQUIRE( + read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); + REQUIRE( + read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); // Is optimal REQUIRE(result.object == op1); @@ -136,8 +81,8 @@ SCENARIO( } WHEN("Merging two constant array AOs with different value arrays") { - auto op1 = util.build_array(val1); - auto op2 = util.build_array(val2); + auto op1 = build_array(val1, environment, ns); + auto op2 = build_array(val2, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -156,9 +101,10 @@ SCENARIO( REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == val1.operands()[0]); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE( + read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // Since it has modified, we definitely shouldn't be reusing the pointer REQUIRE_FALSE(result.object == op1); @@ -168,8 +114,8 @@ SCENARIO( "Merging a constant array AO with a value " "with a constant array AO set to top") { - auto op1 = util.build_array(val1); - auto op2 = util.build_top_array(array_type); + auto op1 = build_array(val1, environment, ns); + auto op2 = build_top_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -185,9 +131,9 @@ SCENARIO( REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // We can't reuse the abstract object as the value has changed REQUIRE(result.object != op1); @@ -197,8 +143,8 @@ SCENARIO( "Merging a constant array AO with a value " "with a constant array AO set to bottom") { - auto op1 = util.build_array(val1); - auto op2 = util.build_bottom_array(array_type); + auto op1 = build_array(val1, environment, ns); + auto op2 = build_bottom_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -214,9 +160,12 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == val1.operands()[0]); - REQUIRE(util.read_index(cast_result, i1) == val1.operands()[1]); - REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); + REQUIRE( + read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); + REQUIRE( + read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); + REQUIRE( + read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); // Is optimal REQUIRE(result.object == op1); @@ -226,8 +175,8 @@ SCENARIO( "Merging a constant array AO set to top " "with a constant array AO with a value") { - auto op1 = util.build_top_array(array_type); - auto op2 = util.build_array(val1); + auto op1 = build_top_array(); + auto op2 = build_array(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -243,9 +192,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // Is optimal REQUIRE(result.object == op1); @@ -255,8 +204,8 @@ SCENARIO( "Merging a constant array AO set to top " "with a constant array AO set to top") { - auto op1 = util.build_top_array(array_type); - auto op2 = util.build_top_array(array_type); + auto op1 = build_top_array(); + auto op2 = build_top_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -272,9 +221,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // Is optimal REQUIRE(result.object == op1); @@ -284,8 +233,8 @@ SCENARIO( "Merging a constant array AO set to top " "with a constant array AO set to bottom") { - auto op1 = util.build_top_array(array_type); - auto op2 = util.build_bottom_array(array_type); + auto op1 = build_top_array(); + auto op2 = build_bottom_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -301,9 +250,9 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // Is optimal REQUIRE(result.object == op1); @@ -313,8 +262,8 @@ SCENARIO( "Merging a constant array AO set to bottom " "with a constant array AO with a value") { - auto op1 = util.build_bottom_array(array_type); - auto op2 = util.build_array(val1); + auto op1 = build_bottom_array(); + auto op2 = build_array(val1, environment, ns); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -330,9 +279,12 @@ SCENARIO( REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == val1.operands()[0]); - REQUIRE(util.read_index(cast_result, i1) == val1.operands()[1]); - REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); + REQUIRE( + read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); + REQUIRE( + read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); + REQUIRE( + read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); // Is optimal REQUIRE(result.object != op1); @@ -342,8 +294,8 @@ SCENARIO( "Merging a constant array AO set to bottom " "with a constant array AO set to top") { - auto op1 = util.build_bottom_array(array_type); - auto op2 = util.build_top_array(array_type); + auto op1 = build_bottom_array(); + auto op2 = build_top_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -359,9 +311,9 @@ SCENARIO( REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i1) == nil_exprt()); - REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); + REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); + REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); // Is optimal REQUIRE(result.object != op1); @@ -371,8 +323,8 @@ SCENARIO( "Merging a constant array AO set to bottom " "with a constant array AO set to bottom") { - auto op1 = util.build_bottom_array(array_type); - auto op2 = util.build_bottom_array(array_type); + auto op1 = build_bottom_array(); + auto op2 = build_bottom_array(); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -397,9 +349,9 @@ SCENARIO( "Merging constant array AO with value " "with a abstract object set to top") { - const auto &op1 = util.build_array(val1); + const auto &op1 = build_array(val1, environment, ns); const auto &op2 = - std::make_shared(val1.type(), true, false); + std::make_shared(op1->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -425,9 +377,9 @@ SCENARIO( "Merging constant array AO with value " "with a abstract object set to bottom") { - const auto &op1 = util.build_array(val1); + const auto &op1 = build_array(val1, environment, ns); const auto &op2 = - std::make_shared(val1.type(), false, true); + std::make_shared(op1->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -443,9 +395,12 @@ SCENARIO( REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(util.read_index(cast_result, i0) == val1.operands()[0]); - REQUIRE(util.read_index(cast_result, i1) == val1.operands()[1]); - REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); + REQUIRE( + read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); + REQUIRE( + read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); + REQUIRE( + read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); // Is optimal REQUIRE(result.object == op1); @@ -455,9 +410,9 @@ SCENARIO( "Merging constant array AO set to top " "with a abstract object set to top") { - const auto &op1 = util.build_top_array(array_type); + const auto &op1 = build_top_array(); const auto &op2 = - std::make_shared(val1.type(), true, false); + std::make_shared(op1->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -483,9 +438,9 @@ SCENARIO( "Merging constant array AO set to top " "with a abstract object set to bottom") { - const auto &op1 = util.build_top_array(array_type); + const auto &op1 = build_top_array(); const auto &op2 = - std::make_shared(val1.type(), false, true); + std::make_shared(op1->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Should get the same abstract object back") @@ -510,9 +465,9 @@ SCENARIO( "Merging constant array AO set to bottom " " with a abstract object set to top") { - const auto &op1 = util.build_bottom_array(array_type); + const auto &op1 = build_bottom_array(); const auto &op2 = - std::make_shared(val1.type(), true, false); + std::make_shared(op1->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return a new top abstract object of the same type") @@ -534,9 +489,9 @@ SCENARIO( } WHEN("Merging constant array AO set to bottom with a AO set to bottom") { - const auto &op1 = util.build_bottom_array(array_type); + const auto &op1 = build_bottom_array(); const auto &op2 = - std::make_shared(val1.type(), false, true); + std::make_shared(op1->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return the original abstract object") @@ -559,9 +514,9 @@ SCENARIO( } WHEN("Merging AO set to top with a constant array AO with a value") { + const auto &op2 = build_array(val1, environment, ns); const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_array(val1); + std::make_shared(op2->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -577,9 +532,9 @@ SCENARIO( } WHEN("Merging AO set to top with a constant array AO set to top") { + const auto &op2 = build_top_array(); const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_top_array(array_type); + std::make_shared(op2->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -595,9 +550,9 @@ SCENARIO( } WHEN("Merging AO set to top with a constant array AO set to bottom") { + const auto &op2 = build_bottom_array(); const auto &op1 = - std::make_shared(val1.type(), true, false); - const auto &op2 = util.build_bottom_array(array_type); + std::make_shared(op2->type(), true, false); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") @@ -613,9 +568,9 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant array AO with a value") { + const auto &op2 = build_array(val1, environment, ns); const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_array(val1); + std::make_shared(op2->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -633,9 +588,9 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant array AO set to top") { + const auto &op2 = build_array(val1, environment, ns); const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_top_array(array_type); + std::make_shared(op2->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); @@ -651,9 +606,9 @@ SCENARIO( } WHEN("Merging AO set to bottom with a constant array AO set to bottom") { + const auto &op2 = build_bottom_array(); const auto &op1 = - std::make_shared(val1.type(), false, true); - const auto &op2 = util.build_bottom_array(array_type); + std::make_shared(op2->type(), false, true); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); 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 0eac317b15b..2c243267d3c 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -8,28 +8,17 @@ #include #include -#include -#include -#include #include #include -#include -#include #include #include - #include -#include -#include - -typedef full_array_abstract_objectt::full_array_pointert - full_array_abstract_object_pointert; -exprt to_expr(int v) -{ - return from_integer(v, integer_typet()); -} +#include +#include +#include +#include SCENARIO( "merge_full_struct_abstract_object", diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 8976481cd56..587798bb9f3 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -17,6 +17,7 @@ #include +#include #include #include #include @@ -164,6 +165,11 @@ bool set_contains(const abstract_object_sett &set, const exprt &val) static std::string interval_to_str(const constant_interval_exprt &expr); +exprt to_expr(int v) +{ + return from_integer(v, integer_typet()); +} + std::string expr_to_str(const exprt &expr) { if(expr.id() == ID_constant_interval) diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 6bf4ba38956..acb46965e40 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -248,6 +248,7 @@ std::shared_ptr add_as_value_set( abstract_environmentt &environment, namespacet &ns); +exprt to_expr(int v); std::string expr_to_str(const exprt &expr); std::string exprs_to_str(const std::vector &values); From 04921dd4f1907a4ae0b62e93ac33b1fc5c7fa8f6 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 20 May 2021 16:27:47 +0100 Subject: [PATCH 10/19] full_array_abstract_objectt::to_predicate --- .../full_array_abstract_object.cpp | 23 +++++++ .../full_array_abstract_object.h | 2 + unit/Makefile | 3 +- .../array_builder.cpp | 9 ++- .../array_builder.h | 1 + .../full_array_abstract_object/merge.cpp | 1 - .../to_predicate.cpp | 67 +++++++++++++++++++ 7 files changed, 102 insertions(+), 4 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 04b962a3658..e9d850a2948 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -10,6 +10,7 @@ #include #include +#include #include #include "abstract_value_object.h" @@ -401,6 +402,28 @@ abstract_object_pointert full_array_abstract_objectt::visit_sub_elements( } } +exprt full_array_abstract_objectt::to_predicate_internal( + const exprt &name) const +{ + auto all_predicates = exprt::operandst{}; + + for(auto field : map.get_sorted_view()) + { + auto ii = from_integer(field.first.to_long(), integer_typet()); + auto index = index_exprt(name, ii); + auto field_expr = field.second->to_predicate(index); + + if(!field_expr.is_true()) + all_predicates.push_back(field_expr); + } + + if(all_predicates.empty()) + return true_exprt(); + if(all_predicates.size() == 1) + return all_predicates.front(); + return and_exprt(all_predicates); +} + void full_array_abstract_objectt::statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.h b/src/analyses/variable-sensitivity/full_array_abstract_object.h index 0c261ff0d72..93b81bb523b 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.h @@ -212,6 +212,8 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt< abstract_object_pointert full_array_merge( const full_array_pointert &other, const widen_modet &widen_mode) const; + + exprt to_predicate_internal(const exprt &name) const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H diff --git a/unit/Makefile b/unit/Makefile index 01ae29de7bb..958b5958633 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,7 +20,9 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \ + analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ + analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/eval.cpp \ analyses/variable-sensitivity/eval-member-access.cpp \ analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp \ @@ -28,7 +30,6 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/interval_abstract_value/merge.cpp \ analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \ - analyses/variable-sensitivity/full_struct_abstract_object/array_builder.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp \ analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp \ diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp index 13f22be6f51..da2d6c0b4ee 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp @@ -9,7 +9,7 @@ #include #include #include -#include +#include #include full_array_abstract_objectt::full_array_pointert build_array( @@ -32,7 +32,12 @@ full_array_abstract_objectt::full_array_pointert build_array( exprt::operandst element_ops; for(auto element : array) - element_ops.push_back(from_integer(element, integer_typet())); + { + if(element != TOP_MEMBER) + element_ops.push_back(from_integer(element, integer_typet())); + else + element_ops.push_back(nil_exprt()); + } auto array_expr = array_exprt(element_ops, array_type); return build_array(array_expr, environment, ns); diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h index 99ff94d95be..d36cae3cd83 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h @@ -15,6 +15,7 @@ full_array_abstract_objectt::full_array_pointert build_array( abstract_environmentt &environment, const namespacet &ns); +const int TOP_MEMBER = std::numeric_limits::max(); full_array_abstract_objectt::full_array_pointert build_array( const std::vector &array, abstract_environmentt &environment, diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp index bfcb08db072..f934dfeb6f4 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -11,7 +11,6 @@ #include #include -#include #include #include #include diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..4d999ab1b16 --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + + Module: Tests for full_array_abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +SCENARIO( + "array to predicate", + "[core][analyses][variable-sensitivity][full_array_abstract_object][to_" + "predicate]") +{ + auto object_factory = variable_sensitivity_object_factoryt::configured_with( + vsd_configt::constant_domain()); + abstract_environmentt environment(object_factory); + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("full_array_abstract_object to predicate") + { + WHEN("it is TOP") + { + auto obj = build_top_array(); + THEN_PREDICATE(obj, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto obj = build_bottom_array(); + THEN_PREDICATE(obj, "FALSE"); + } + WHEN("[ 1 ]") + { + auto obj = build_array({1}, environment, ns); + THEN_PREDICATE(obj, "x[0] == 1"); + } + WHEN("[ 1, 2, 3 ]") + { + auto obj = build_array({1, 2, 3}, environment, ns); + THEN_PREDICATE(obj, "x[0] == 1 && x[1] == 2 && x[2] == 3"); + } + WHEN("[ 1, 2, TOP ]") + { + auto obj = build_array({1, 2, TOP_MEMBER}, environment, ns); + THEN_PREDICATE(obj, "x[0] == 1 && x[1] == 2"); + } + WHEN("[ TOP, 2, TOP ]") + { + auto obj = build_array({TOP_MEMBER, 2, TOP_MEMBER}, environment, ns); + THEN_PREDICATE(obj, "x[1] == 2"); + } + WHEN("[ TOP, TOP, TOP ]") + { + auto obj = + build_array({TOP_MEMBER, TOP_MEMBER, TOP_MEMBER}, environment, ns); + THEN_PREDICATE(obj, "TRUE"); + } + } +} From 153244a4b86f0cb35e9bce2cb55916774d3e5b37 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 4 Aug 2021 09:01:01 +0100 Subject: [PATCH 11/19] sort value set to_predicate subexpressions --- .../value_set_abstract_object.cpp | 1 + .../value_set_abstract_object/to_predicate.cpp | 15 +++++---------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 9919f9263a7..dff9753b837 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -350,6 +350,7 @@ exprt value_set_abstract_objectt::to_predicate_internal(const exprt &name) const [&name](const abstract_object_pointert &value) { return value->to_predicate(name); }); + std::sort(all_predicates.begin(), all_predicates.end()); return or_exprt(all_predicates); } diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp index b963978c767..dec14931876 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -70,12 +70,7 @@ SCENARIO( WHEN("{ 0, 1, 2 }") { auto obj = make_value_set({val0, val1, val2}, environment, ns); - auto pred = obj->to_predicate(x_name); - THEN("predicate is x == 0 || x == 1 || x == 2") - { - auto repr = expr_to_str(pred); - REQUIRE(repr == "x == 0 || x == 1 || x == 2"); - } + THEN_PREDICATE(obj, "x == 0 || x == 1 || x == 2"); } WHEN("{ [0, 1] }") { @@ -85,17 +80,17 @@ SCENARIO( WHEN("{ [0, 1], 2 }") { auto obj = make_value_set({interval_0_1, val2}, environment, ns); - THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2"); + THEN_PREDICATE(obj, "x == 2 || 0 <= x && x <= 1"); } WHEN("{ [0, 1], 2, 3 }") { auto obj = make_value_set({interval_0_1, val2, val3}, environment, ns); - THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 3 || x == 2"); + THEN_PREDICATE(obj, "x == 2 || x == 3 || 0 <= x && x <= 1"); } WHEN("{ [0, 1], 1, 2 }") { auto obj = make_value_set({interval_0_1, val1, val2}, environment, ns); - THEN_PREDICATE(obj, "0 <= x && x <= 1 || x == 2"); + THEN_PREDICATE(obj, "x == 2 || 0 <= x && x <= 1"); } WHEN("{ [0, 1], [1, 2] }") { @@ -110,7 +105,7 @@ SCENARIO( WHEN("{ [0, 1], [2, 3] }") { auto obj = make_value_set({interval_0_1, interval_2_3}, environment, ns); - THEN_PREDICATE(obj, "2 <= x && x <= 3 || 0 <= x && x <= 1"); + THEN_PREDICATE(obj, "0 <= x && x <= 1 || 2 <= x && x <= 3"); } } } From b424445ef5a250caa7d2a2c7c0a6db50b04af17c Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 4 Aug 2021 10:07:32 +0100 Subject: [PATCH 12/19] constant pointer to_predicate --- .../constant_pointer_abstract_object.cpp | 6 ++ .../constant_pointer_abstract_object.h | 2 + unit/Makefile | 1 + .../module_dependencies.txt | 3 + .../to_predicate.cpp | 59 +++++++++++++++++++ 5 files changed, 71 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/constant_pointer_abstract_object/module_dependencies.txt create mode 100644 unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index 308da073b2f..c6d5e60f852 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -388,3 +388,9 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr( return true_exprt(); return nil_exprt(); } + +exprt constant_pointer_abstract_objectt::to_predicate_internal( + const exprt &name) const +{ + return equal_exprt(name, value_stack.to_expression()); +} diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h index ad7c4d5e628..e72b03dcb3b 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h @@ -145,6 +145,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt CLONE + exprt to_predicate_internal(const exprt &name) const override; + private: bool same_target(abstract_object_pointert other) const; exprt offset() const; diff --git a/unit/Makefile b/unit/Makefile index 958b5958633..c5698ebf21e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -20,6 +20,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \ + analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp \ diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/module_dependencies.txt b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..468767c2080 --- /dev/null +++ b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp @@ -0,0 +1,59 @@ +/*******************************************************************\ + + Module: Tests for constant_pointer_abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + +SCENARIO( + "constant_pointer_abstract_object to predicate", + "[core][analyses][variable-sensitivity][constant_pointer_abstract_object][to_" + "predicate]") +{ + const auto int_type = signedbv_typet(32); + const auto ptr_type = pointer_typet(int_type, 32); + const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type); + + const auto x_name = symbol_exprt(dstringt("x"), int_type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("constant_pointer_abstract_object") + { + WHEN("it is TOP") + { + auto obj = std::make_shared( + ptr_type, true, false); + THEN_PREDICATE(obj, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto obj = std::make_shared( + ptr_type, false, true); + THEN_PREDICATE(obj, "FALSE"); + } + WHEN("points to a &symbol") + { + const auto address_of = address_of_exprt(val2_symbol); + auto obj = std::make_shared( + address_of, environment, ns); + THEN_PREDICATE(obj, "x == &val2"); + } + } +} From 4914c31fe6d7ab18d0a1c02f90c97531a74c4752 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 5 Aug 2021 16:03:28 +0100 Subject: [PATCH 13/19] value_set of pointers to_predicate --- .../value_set_pointer_abstract_object.cpp | 19 +++++ .../value_set_pointer_abstract_object.h | 2 + unit/Makefile | 1 + .../module_dependencies.txt | 3 + .../to_predicate.cpp | 75 +++++++++++++++++++ 5 files changed, 100 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/module_dependencies.txt create mode 100644 unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp 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 53c5203d511..d65895d8d41 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -229,6 +229,25 @@ abstract_object_pointert value_set_pointer_abstract_objectt::merge( return abstract_objectt::merge(other, widen_mode); } +exprt value_set_pointer_abstract_objectt::to_predicate_internal( + const exprt &name) const +{ + if(values.size() == 1) + return values.first()->to_predicate(name); + + auto all_predicates = exprt::operandst{}; + std::transform( + values.begin(), + values.end(), + std::back_inserter(all_predicates), + [&name](const abstract_object_pointert &value) { + return value->to_predicate(name); + }); + std::sort(all_predicates.begin(), all_predicates.end()); + + return or_exprt(all_predicates); +} + void value_set_pointer_abstract_objectt::set_values( const abstract_object_sett &other_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 e7cf55a32bf..61b9a16bc71 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -98,6 +98,8 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, const abstract_object_pointert &other, const widen_modet &widen_mode) const override; + exprt to_predicate_internal(const exprt &name) const override; + private: /// Update the set of stored values to \p new_values. Build a new abstract /// object of the right type if necessary. diff --git a/unit/Makefile b/unit/Makefile index c5698ebf21e..d166474a973 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -44,6 +44,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \ analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp \ + analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ ansi-c/expr2c.cpp \ ansi-c/max_malloc_size.cpp \ diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/module_dependencies.txt b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp new file mode 100644 index 00000000000..16c796e3df6 --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp @@ -0,0 +1,75 @@ +/*******************************************************************\ + + Module: Tests for value_set_pointer_abstract_objectt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +template +std::shared_ptr make_vsp(Args &&... args) +{ + return std::make_shared( + std::forward(args)...); +} + +SCENARIO( + "value_set_pointer_abstract_object to predicate", + "[core][analyses][variable-sensitivity][value_set_pointer_abstract_object][" + "to_predicate]") +{ + const auto int_type = signedbv_typet(32); + const auto ptr_type = pointer_typet(int_type, 32); + const auto val1_symbol = symbol_exprt(dstringt("val1"), int_type); + const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type); + + const auto x_name = symbol_exprt(dstringt("x"), int_type); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + abstract_environmentt environment{object_factory}; + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("value_set_pointer_abstract_object") + { + WHEN("it is TOP") + { + auto obj = make_vsp(ptr_type, true, false); + THEN_PREDICATE(obj, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto obj = make_vsp(ptr_type, false, true); + THEN_PREDICATE(obj, "FALSE"); + } + WHEN("points to a &symbol") + { + const auto address_of = address_of_exprt(val2_symbol); + auto obj = make_vsp(address_of, environment, ns); + THEN_PREDICATE(obj, "x == &val2"); + } + WHEN("points to { &val1, &val2 } ") + { + auto address_of_val1 = address_of_exprt(val1_symbol); + auto address_of_val2 = address_of_exprt(val2_symbol); + auto p1 = make_vsp(address_of_val1, environment, ns); + auto p2 = make_vsp(address_of_val2, environment, ns); + + auto obj = abstract_objectt::merge(p1, p2, widen_modet::no).object; + THEN_PREDICATE(obj, "x == &val1 || x == &val2"); + } + } +} From c90017c03fb54d5d4ecac0fc9f194965757450f3 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Thu, 5 Aug 2021 16:13:19 +0100 Subject: [PATCH 14/19] Annotate abstract_object::to_predicate. Shouldn't ever end up being called --- .../variable-sensitivity/abstract_object.cpp | 1 + unit/Makefile | 1 - .../abstract_object/to_predicate.cpp | 40 ------------------- 3 files changed, 1 insertion(+), 41 deletions(-) delete mode 100644 unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index 5b4fe7553e7..cc82089a9ae 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -183,6 +183,7 @@ exprt abstract_objectt::to_predicate(const exprt &name) const exprt abstract_objectt::to_predicate_internal(const exprt &name) const { + UNREACHABLE; return nil_exprt(); } diff --git a/unit/Makefile b/unit/Makefile index d166474a973..7b595af97eb 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -16,7 +16,6 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ analyses/variable-sensitivity/abstract_object/merge.cpp \ analyses/variable-sensitivity/abstract_object/index_range.cpp \ - analyses/variable-sensitivity/abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ analyses/variable-sensitivity/constant_abstract_value/merge.cpp \ analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp deleted file mode 100644 index d3f3bd33119..00000000000 --- a/unit/analyses/variable-sensitivity/abstract_object/to_predicate.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/*******************************************************************\ - - Module: Tests for abstract_objectt::to_predicate - - Author: Jez Higgins - -\*******************************************************************/ - -#include -#include -#include - -SCENARIO( - "constant to predicate", - "[core][analyses][variable-sensitivity][abstract_object][to_predicate]") -{ - GIVEN("an abstract object") - { - WHEN("it is TOP") - { - auto obj = make_top_object(); - THEN_PREDICATE(obj, "TRUE"); - } - WHEN("it is BOTTOM") - { - auto obj = make_bottom_object(); - THEN_PREDICATE(obj, "FALSE"); - } - WHEN("it is neither TOP nor BOTTOM") - { - auto obj = - std::make_shared(integer_typet(), false, false); - auto pred = obj->to_predicate(nil_exprt()); - THEN("predicate is nil") - { - REQUIRE(pred == nil_exprt()); - } - } - } -} From 574b5b18835dfd2240629308ed60eaa75337e417 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 6 Aug 2021 09:52:36 +0100 Subject: [PATCH 15/19] abstract_environmentt::to_predicate --- .../abstract_environment.cpp | 23 ++++++ .../abstract_environment.h | 6 ++ unit/Makefile | 1 + .../module_dependencies.txt | 3 + .../abstract_environment/to_predicate.cpp | 73 +++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 10 +++ .../variable_sensitivity_test_helpers.h | 1 + 7 files changed, 117 insertions(+) create mode 100644 unit/analyses/variable-sensitivity/abstract_environment/module_dependencies.txt create mode 100644 unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index bf5820c5698..d0fbe36550c 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -419,6 +419,29 @@ void abstract_environmentt::output( out << "}\n"; } +exprt abstract_environmentt::to_predicate() const +{ + if(is_bottom()) + return false_exprt(); + if(is_top()) + return true_exprt(); + + auto predicates = std::vector { }; + for(const auto &entry : map.get_view()) + { + auto sym = entry.first; + auto val = entry.second; + + auto pred = val->to_predicate(symbol_exprt(sym, val->type())); + + predicates.push_back(pred); + } + + if(predicates.size() == 1) + return predicates.front(); + return and_exprt(predicates); +} + bool abstract_environmentt::verify() const { decltype(map)::viewt view; diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index a530c949138..568db3af852 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -224,6 +224,12 @@ class abstract_environmentt void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const; + /// Gives a boolean condition that is true for all values represented by the + /// environment. + /// + /// \return An exprt describing the environment + exprt to_predicate() const; + /// Check the structural invariants are maintained. /// In this case this is checking there aren't any null pointer mapped values bool verify() const; diff --git a/unit/Makefile b/unit/Makefile index 7b595af97eb..72905deb8e2 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -14,6 +14,7 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ + analyses/variable-sensitivity/abstract_environment/to_predicate.cpp \ analyses/variable-sensitivity/abstract_object/merge.cpp \ analyses/variable-sensitivity/abstract_object/index_range.cpp \ analyses/variable-sensitivity/constant_abstract_value/meet.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_environment/module_dependencies.txt b/unit/analyses/variable-sensitivity/abstract_environment/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/abstract_environment/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp new file mode 100644 index 00000000000..934d97518a1 --- /dev/null +++ b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + + Module: Tests for abstract_environmentt::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include + +SCENARIO( + "abstract_environment to predicate", + "[core][analyses][variable-sensitivity][abstract_environment][to_predicate]") +{ + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("an abstract environment") + { + WHEN("it is TOP") + { + auto env = abstract_environmentt{object_factory}; + env.make_top(); + THEN_PREDICATE(env, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto env = abstract_environmentt{object_factory}; + env.make_bottom(); + THEN_PREDICATE(env, "FALSE"); + } + WHEN("contains x = 2") + { + auto env = abstract_environmentt{object_factory}; + env.make_top(); + + auto type = signedbv_typet(32); + auto val2 = make_constant(from_integer(2, type), env, ns); + auto x_name = symbol_exprt(dstringt("x"), type); + + env.assign(x_name, val2, ns); + + THEN_PREDICATE(env, "x == 2"); + } + WHEN("contains x = 2, y = 3") + { + auto env = abstract_environmentt{object_factory}; + env.make_top(); + + auto type = signedbv_typet(32); + auto val2 = make_constant(from_integer(2, type), env, ns); + auto x_name = symbol_exprt(dstringt("x"), type); + + auto val3 = make_constant(from_integer(3, type), env, ns); + auto y_name = symbol_exprt(dstringt("y"), type); + + env.assign(x_name, val2, ns); + env.assign(y_name, val3, ns); + + THEN_PREDICATE(env, "y == 3 && x == 2"); + } + } +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 587798bb9f3..d739d105812 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -538,3 +538,13 @@ void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out) REQUIRE(repr == out); } } + +void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out) +{ + auto pred = env.to_predicate(); + THEN("predicate is " + out) + { + auto repr = expr_to_str(pred); + REQUIRE(repr == out); + } +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index acb46965e40..18330be2d98 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -255,5 +255,6 @@ std::string exprs_to_str(const std::vector &values); void THEN_PREDICATE( const abstract_object_pointert &obj, const std::string &out); +void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out); #endif From a04a5295a5c39c9e38b1126c89839788ccdf0641 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 6 Aug 2021 10:02:34 +0100 Subject: [PATCH 16/19] simplify map.get_view calls --- .../abstract_environment.cpp | 20 ++++++------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index d0fbe36550c..b28d7fa6d21 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -408,14 +408,13 @@ void abstract_environmentt::output( { out << "{\n"; - decltype(map)::viewt view; - map.get_view(view); - for(const auto &entry : view) + for(const auto &entry : map.get_view()) { out << entry.first << " () -> "; entry.second->output(out, ai, ns); out << "\n"; } + out << "}\n"; } @@ -426,12 +425,11 @@ exprt abstract_environmentt::to_predicate() const if(is_top()) return true_exprt(); - auto predicates = std::vector { }; + auto predicates = std::vector{}; for(const auto &entry : map.get_view()) { auto sym = entry.first; auto val = entry.second; - auto pred = val->to_predicate(symbol_exprt(sym, val->type())); predicates.push_back(pred); @@ -444,9 +442,7 @@ exprt abstract_environmentt::to_predicate() const bool abstract_environmentt::verify() const { - decltype(map)::viewt view; - map.get_view(view); - for(const auto &entry : view) + for(const auto &entry : map.get_view()) { if(entry.second == nullptr) { @@ -483,9 +479,7 @@ abstract_environmentt::modified_symbols( { // Find all symbols who have different write locations in each map std::vector symbols_diff; - decltype(first.map)::viewt view; - first.map.get_view(view); - for(const auto &entry : view) + for(const auto &entry : first.map.get_view()) { const auto &second_entry = second.map.find(entry.first); if(second_entry.has_value()) @@ -528,10 +522,8 @@ abstract_environmentt::gather_statistics(const namespacet &ns) const { abstract_object_statisticst statistics = {}; statistics.number_of_globals = count_globals(ns); - decltype(map)::viewt view; - map.get_view(view); abstract_object_visitedt visited; - for(auto const &object : view) + for(auto const &object : map.get_view()) { if(visited.find(object.second) == visited.end()) { From e6f5ffaa54cfb2683533e60681adf8977b5de8cc Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 6 Aug 2021 10:07:24 +0100 Subject: [PATCH 17/19] variable_sensitivity_domaint::to_predicate Wrapper that calls down into abstract_environmentt::to_predicate --- .../variable-sensitivity/variable_sensitivity_domain.cpp | 5 +++++ .../variable-sensitivity/variable_sensitivity_domain.h | 6 +++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 2be28ef0088..4fa5c800dda 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -176,6 +176,11 @@ void variable_sensitivity_domaint::output( abstract_state.output(out, ai, ns); } +exprt variable_sensitivity_domaint::to_predicate() const +{ + return abstract_state.to_predicate(); +} + void variable_sensitivity_domaint::make_bottom() { abstract_state.make_bottom(); diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index a8983941a3f..7dc70c02663 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -146,7 +146,11 @@ class variable_sensitivity_domaint : public ai_domain_baset void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; - void output(std::ostream &out) const; + /// Gives a Boolean condition that is true for all values represented by the + /// domain. This allows domains to be converted into program invariants. + /// + /// \return exprt describing the domain + exprt to_predicate() const override; /// Computes the join between "this" and "b". /// From 664f02185261b45f66357a64736322648497ec04 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 6 Aug 2021 11:10:35 +0100 Subject: [PATCH 18/19] test to show to_predicate doesn't need to take a symbol --- .../constant_abstract_value/to_predicate.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index 684179b81c3..a7bcf1899ba 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -49,5 +49,17 @@ SCENARIO( auto obj = make_constant(val2, environment, ns); THEN_PREDICATE(obj, "x == 2"); } + WHEN("(1 + 2) = 3") + { + auto val1 = from_integer(1, type); + auto c3 = make_constant(from_integer(3, type), environment, ns); + + auto pred = c3->to_predicate(plus_exprt(val1, val2)); + THEN("predicate is (1 + 2) = 3") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "1 + 2 == 3"); + } + } } } From 7af8e92db2434a40b800036587ea28ac4a3cd22a Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 6 Aug 2021 11:40:08 +0100 Subject: [PATCH 19/19] vsd to_predicate(expr) --- .../variable_sensitivity_domain.cpp | 26 +++++ .../variable_sensitivity_domain.h | 3 + unit/Makefile | 1 + .../module_dependencies.txt | 3 + .../to_predicate.cpp | 105 ++++++++++++++++++ .../variable_sensitivity_test_helpers.cpp | 16 ++- .../variable_sensitivity_test_helpers.h | 4 + 7 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 unit/analyses/variable-sensitivity/variable_sensitivity_domain/module_dependencies.txt create mode 100644 unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 4fa5c800dda..fda9446f1dd 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -181,6 +181,32 @@ exprt variable_sensitivity_domaint::to_predicate() const return abstract_state.to_predicate(); } +exprt variable_sensitivity_domaint::to_predicate( + const exprt &expr, + const namespacet &ns) const +{ + auto result = abstract_state.eval(expr, ns); + return result->to_predicate(expr); +} + +exprt variable_sensitivity_domaint::to_predicate( + const exprt::operandst &exprs, + const namespacet &ns) const +{ + if(exprs.empty()) + return false_exprt(); + if(exprs.size() == 1) + return to_predicate(exprs.front(), ns); + + auto predicates = std::vector{}; + std::transform( + exprs.cbegin(), + exprs.cend(), + std::back_inserter(predicates), + [this, &ns](const exprt &expr) { return to_predicate(expr, ns); }); + return and_exprt(predicates); +} + void variable_sensitivity_domaint::make_bottom() { abstract_state.make_bottom(); diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 7dc70c02663..993b2223679 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -152,6 +152,9 @@ class variable_sensitivity_domaint : public ai_domain_baset /// \return exprt describing the domain exprt to_predicate() const override; + exprt to_predicate(const exprt &expr, const namespacet &ns) const; + exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const; + /// Computes the join between "this" and "b". /// /// \param b: the other domain diff --git a/unit/Makefile b/unit/Makefile index 72905deb8e2..68a16dc3b0e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -45,6 +45,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp \ analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp \ + analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ ansi-c/expr2c.cpp \ ansi-c/max_malloc_size.cpp \ diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/module_dependencies.txt b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/module_dependencies.txt new file mode 100644 index 00000000000..ac96be3c1ef --- /dev/null +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/module_dependencies.txt @@ -0,0 +1,3 @@ +analyses +testing-utils +util diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp new file mode 100644 index 00000000000..7d40afe4718 --- /dev/null +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp @@ -0,0 +1,105 @@ +/*******************************************************************\ + + Module: Tests for variable_sensitivity_domaint::to_predicate + + Author: Jez Higgins + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +SCENARIO( + "variable_sensitivity_domain to predicate", + "[core][analyses][variable-sensitivity][variable_sensitivity_domain][to_" + "predicate]") +{ + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + + GIVEN("to_predicate()") + { + WHEN("it is TOP") + { + auto domain = variable_sensitivity_domaint(object_factory, config); + domain.make_top(); + THEN_PREDICATE(domain, "TRUE"); + } + WHEN("it is BOTTOM") + { + auto domain = variable_sensitivity_domaint(object_factory, config); + domain.make_bottom(); + THEN_PREDICATE(domain, "FALSE"); + } + } + GIVEN("to_predicate(expr)") + { + WHEN("1 + 2") + { + auto type = signedbv_typet(32); + auto val1 = from_integer(1, type); + auto val2 = from_integer(2, type); + + auto domain = variable_sensitivity_domaint(object_factory, config); + domain.make_top(); + + auto pred = domain.to_predicate(plus_exprt(val1, val2), ns); + THEN("predicate is 1 + 2 == 3") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "1 + 2 == 3"); + } + } + } + GIVEN("to_predicate(std::vector)") + { + auto domain = variable_sensitivity_domaint(object_factory, config); + domain.make_top(); + + auto type = signedbv_typet(32); + auto val1 = from_integer(1, type); + auto val2 = from_integer(2, type); + auto val3 = from_integer(3, type); + auto onePlusTwo = plus_exprt(val1, val2); + auto twoPlusThree = plus_exprt(val2, val3); + + WHEN("{ }") + { + auto pred = domain.to_predicate(std::vector(), ns); + THEN("predicate is FALSE") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "FALSE"); + } + } + WHEN("{ 1 + 2 }") + { + auto pred = domain.to_predicate({onePlusTwo}, ns); + THEN("predicate is 1 + 2 == 3") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "1 + 2 == 3"); + } + } + + WHEN("{ 1 + 2, 2 + 3 }") + { + auto pred = domain.to_predicate({onePlusTwo, twoPlusThree}, ns); + THEN("predicate is 1 + 2 == 3 && 2 + 3 == 5") + { + auto repr = expr_to_str(pred); + REQUIRE(repr == "1 + 2 == 3 && 2 + 3 == 5"); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index d739d105812..08db37edfc6 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -12,6 +12,7 @@ #include #include #include +#include #include @@ -539,12 +540,23 @@ void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out) } } -void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out) +void THEN_PREDICATE(const exprt &pred, const std::string &out) { - auto pred = env.to_predicate(); THEN("predicate is " + out) { auto repr = expr_to_str(pred); REQUIRE(repr == out); } } + +void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out) +{ + THEN_PREDICATE(env.to_predicate(), out); +} + +void THEN_PREDICATE( + const variable_sensitivity_domaint &domain, + const std::string &out) +{ + THEN_PREDICATE(domain.to_predicate(), out); +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 18330be2d98..fe0e067fb66 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -18,6 +18,7 @@ class constant_abstract_valuet; class constant_interval_exprt; class interval_abstract_valuet; class value_set_abstract_objectt; +class variable_sensitivity_domaint; std::shared_ptr make_constant(exprt val, abstract_environmentt &env, namespacet &ns); @@ -256,5 +257,8 @@ void THEN_PREDICATE( const abstract_object_pointert &obj, const std::string &out); void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out); +void THEN_PREDICATE( + const variable_sensitivity_domaint &domain, + const std::string &out); #endif