diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc index 89294fe5af8..d2ccbddd023 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc @@ -4,5 +4,5 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^main::1::1::i .* \[5, 5\] @ \[6\] -^main::1::p .* \[2, 20\] @ \[5\] +^main::1::p .* \[2, 1F9\] @ \[5\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc index d5b01044381..a06a1f142af 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc @@ -4,5 +4,5 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\] -^main::1::p .* value-set-begin: 2, 17, 32 :value-set-end @ \[5\] +^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\] -- diff --git a/regression/goto-analyzer/value-set-convert-to-interval/main.c b/regression/goto-analyzer/value-set-compact-01/main.c similarity index 100% rename from regression/goto-analyzer/value-set-convert-to-interval/main.c rename to regression/goto-analyzer/value-set-compact-01/main.c diff --git a/regression/goto-analyzer/value-set-convert-to-interval/test.desc b/regression/goto-analyzer/value-set-compact-01/test.desc similarity index 75% rename from regression/goto-analyzer/value-set-convert-to-interval/test.desc rename to regression/goto-analyzer/value-set-compact-01/test.desc index 45b4d120bd1..509bfdfd705 100644 --- a/regression/goto-analyzer/value-set-convert-to-interval/test.desc +++ b/regression/goto-analyzer/value-set-compact-01/test.desc @@ -5,5 +5,5 @@ main.c ^SIGNAL=0$ main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\] -main::1::c .* \[14, 1E\] @ \[30\] +main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\] -- diff --git a/regression/goto-analyzer/value-set-compact-02/main.c b/regression/goto-analyzer/value-set-compact-02/main.c new file mode 100644 index 00000000000..364d8706e7c --- /dev/null +++ b/regression/goto-analyzer/value-set-compact-02/main.c @@ -0,0 +1,49 @@ +#include + +extern int x; + +int main(void) +{ + int a[1] = {0}; + switch(x) + { + case 1: + a[0] = 1; + break; + case 2: + a[0] = 2; + break; + case 3: + a[0] = 3; + break; + case 4: + a[0] = 4; + break; + case 5: + a[0] = 5; + break; + case 6: + a[0] = 6; + break; + case 7: + a[0] = 7; + break; + case 8: + a[0] = 8; + break; + case 9: + a[0] = 9; + break; + case 10: + a[0] = 10; + break; + case 11: + a[0] = 11; + break; + case 12: + a[0] = 12; + break; + } + + return 0; +} diff --git a/regression/goto-analyzer/value-set-compact-02/test.desc b/regression/goto-analyzer/value-set-compact-02/test.desc new file mode 100644 index 00000000000..797e9c24848 --- /dev/null +++ b/regression/goto-analyzer/value-set-compact-02/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element --show +^EXIT=0$ +^SIGNAL=0$ +main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\] +-- diff --git a/regression/goto-analyzer/value-set-compact-03/main.c b/regression/goto-analyzer/value-set-compact-03/main.c new file mode 100644 index 00000000000..3deb1f5ed1f --- /dev/null +++ b/regression/goto-analyzer/value-set-compact-03/main.c @@ -0,0 +1,55 @@ +#include + +extern int x; + +struct S +{ + int a; +}; + +int main(void) +{ + struct S a; + a.a = 0; + switch(x) + { + case 1: + a.a = 1; + break; + case 2: + a.a = 2; + break; + case 3: + a.a = 3; + break; + case 4: + a.a = 4; + break; + case 5: + a.a = 5; + break; + case 6: + a.a = 6; + break; + case 7: + a.a = 7; + break; + case 8: + a.a = 8; + break; + case 9: + a.a = 9; + break; + case 10: + a.a = 10; + break; + case 11: + a.a = 11; + break; + case 12: + a.a = 12; + break; + } + + return 0; +} diff --git a/regression/goto-analyzer/value-set-compact-03/test.desc b/regression/goto-analyzer/value-set-compact-03/test.desc new file mode 100644 index 00000000000..64f922f90a4 --- /dev/null +++ b/regression/goto-analyzer/value-set-compact-03/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --show +^EXIT=0$ +^SIGNAL=0$ +main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .* +-- diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 79bd7722dc8..9637db57551 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -47,7 +47,6 @@ SRC = ai.cpp \ variable-sensitivity/interval_abstract_value.cpp \ variable-sensitivity/three_way_merge_abstract_interpreter.cpp \ variable-sensitivity/value_set_abstract_object.cpp \ - variable-sensitivity/value_set_abstract_value.cpp \ variable-sensitivity/value_set_pointer_abstract_object.cpp \ variable-sensitivity/variable_sensitivity_configuration.cpp \ variable-sensitivity/variable_sensitivity_dependence_graph.cpp \ diff --git a/src/analyses/variable-sensitivity/abstract_aggregate_object.h b/src/analyses/variable-sensitivity/abstract_aggregate_object.h index fe42c11428d..43a6bca6368 100644 --- a/src/analyses/variable-sensitivity/abstract_aggregate_object.h +++ b/src/analyses/variable-sensitivity/abstract_aggregate_object.h @@ -127,7 +127,8 @@ class abstract_aggregate_objectt : public abstract_objectt, static bool merge_shared_maps( const sharing_mapt &map1, const sharing_mapt &map2, - sharing_mapt &out_map) + sharing_mapt &out_map, + const widen_modet &widen_mode) { bool modified = false; @@ -137,13 +138,12 @@ class abstract_aggregate_objectt : public abstract_objectt, for(auto &item : delta_view) { - bool changes = false; - abstract_object_pointert v_new = - abstract_objectt::merge(item.m, item.get_other_map_value(), changes); - if(changes) + auto v_new = + abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode); + if(v_new.modified) { modified = true; - out_map.replace(item.k, v_new); + out_map.replace(item.k, v_new.object); } } diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index f2cb079499f..b473730c36e 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -312,38 +312,33 @@ abstract_object_pointert abstract_environmentt::add_object_context( return object_factory->wrap_with_context(abstract_object); } -bool abstract_environmentt::merge(const abstract_environmentt &env) +bool abstract_environmentt::merge( + const abstract_environmentt &env, + widen_modet widen_mode) { // for each entry in the incoming environment we need to either add it // if it is new, or merge with the existing key if it is not present - if(bottom) { *this = env; return !env.bottom; } - else if(env.bottom) - { + + if(env.bottom) return false; - } - else - { - // For each element in the intersection of map and env.map merge - // If the result of the merge is top, remove from the map - bool modified = false; - decltype(env.map)::delta_viewt delta_view; - env.map.get_delta_view(map, delta_view); - for(const auto &entry : delta_view) - { - bool object_modified = false; - abstract_object_pointert new_object = abstract_objectt::merge( - entry.get_other_map_value(), entry.m, object_modified); - modified |= object_modified; - map.replace(entry.k, new_object); - } - return modified; + // For each element in the intersection of map and env.map merge + // If the result of the merge is top, remove from the map + bool modified = false; + for(const auto &entry : env.map.get_delta_view(map)) + { + auto merge_result = + abstract_objectt::merge(entry.get_other_map_value(), entry.m, widen_mode); + modified |= merge_result.modified; + map.replace(entry.k, merge_result.object); } + + return modified; } void abstract_environmentt::havoc(const std::string &havoc_string) @@ -508,12 +503,8 @@ std::vector eval_operands( /////////// abstract_value_pointert as_value(const abstract_object_pointert &obj) { - auto context_value = - std::dynamic_pointer_cast(obj); - - return context_value - ? as_value(context_value->unwrap_context()) - : std::dynamic_pointer_cast(obj); + return std::dynamic_pointer_cast( + obj->unwrap_context()); } bool is_value(const abstract_object_pointert &obj) diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index 67a27f7d65c..d2fb80a6cfe 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -25,6 +25,12 @@ class variable_sensitivity_object_factoryt; using variable_sensitivity_object_factory_ptrt = std::shared_ptr; +enum class widen_modet +{ + no, + could_widen +}; + class abstract_environmentt { public: @@ -180,9 +186,10 @@ class abstract_environmentt /// Computes the join between "this" and "b" /// /// \param env: the other environment + /// \param widen_mode: indicates if this is a widening merge /// /// \return A Boolean, true when the merge has changed something - virtual bool merge(const abstract_environmentt &env); + virtual bool merge(const abstract_environmentt &env, widen_modet widen_mode); /// This should be used as a default case / everything else has failed /// The string is so that I can easily find and diagnose cases where this diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index 1dbaf3be9f4..af28380484b 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -48,8 +48,9 @@ const typet &abstract_objectt::type() const return t; } -abstract_object_pointert -abstract_objectt::merge(const abstract_object_pointert &other) const +abstract_object_pointert abstract_objectt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { return abstract_object_merge(other); } @@ -182,26 +183,16 @@ void abstract_objectt::output( } } -abstract_object_pointert abstract_objectt::merge( +abstract_objectt::combine_result abstract_objectt::merge( const abstract_object_pointert &op1, const abstract_object_pointert &op2, - bool &out_modifications) + const widen_modet &widen_mode) { abstract_object_pointert result = op1->should_use_base_merge(op2) ? op1->abstract_object_merge(op2) - : op1->merge(op2); + : op1->merge(op2, widen_mode); // If no modifications, we will return the original pointer - out_modifications = result != op1; - - return result; -} - -abstract_object_pointert abstract_objectt::merge( - const abstract_object_pointert &op1, - const abstract_object_pointert &op2) -{ - bool dummy; - return merge(op1, op2, dummy); + return {result, result != op1}; } bool abstract_objectt::should_use_base_merge( @@ -210,18 +201,15 @@ bool abstract_objectt::should_use_base_merge( return is_top() || other->is_bottom() || other->is_top(); } -abstract_object_pointert abstract_objectt::meet( +abstract_objectt::combine_result abstract_objectt::meet( const abstract_object_pointert &op1, - const abstract_object_pointert &op2, - bool &out_modifications) + const abstract_object_pointert &op2) { abstract_object_pointert result = op1->should_use_base_meet(op2) ? op1->abstract_object_meet(op2) : op1->meet(op2); // If no modifications, we will return the original pointer - out_modifications = result != op1; - - return result; + return {result, result != op1}; } bool abstract_objectt::should_use_base_meet( diff --git a/src/analyses/variable-sensitivity/abstract_object.h b/src/analyses/variable-sensitivity/abstract_object.h index dffc3c44c68..171d88e0126 100644 --- a/src/analyses/variable-sensitivity/abstract_object.h +++ b/src/analyses/variable-sensitivity/abstract_object.h @@ -36,6 +36,7 @@ class abstract_environmentt; class namespacet; struct abstract_object_statisticst; +enum class widen_modet; #define CLONE \ internal_abstract_object_pointert mutable_clone() const override \ @@ -244,28 +245,29 @@ class abstract_objectt : public std::enable_shared_from_this /// \param op2: the second abstract object to merge /// \param out_modifications: reference to a flag indicating modification /// - /// \return The merged abstract object with the same sensitivity as the - /// first parameter. out_modifications will be true if the resulting - /// abstract object is different from op1 - static abstract_object_pointert merge( + /// \return A pair containing the merged abstract object with the same + /// sensitivity as op1, and a modified flag which + /// will be true if the merged abstract object is different from op1 + struct combine_result + { + abstract_object_pointert object; + bool modified; + }; + static combine_result merge( const abstract_object_pointert &op1, const abstract_object_pointert &op2, - bool &out_modifications); - static abstract_object_pointert merge( - const abstract_object_pointert &op1, - const abstract_object_pointert &op2); + const widen_modet &widen_mode); /// Interface method for the meet operation. Decides whether to use the base /// implementation or if a more precise abstraction is attainable. /// \param op1 lhs object for meet /// \param op2 rhs object for meet - /// \param out_modifications reference to a flag indicating modification - /// (result is not op1) - /// \return resulting object after meet - static abstract_object_pointert meet( + /// \return A pair containing the merged abstract object with the same + /// sensitivity as op1, and a modified flag which + /// will be true if the returned object is different from op1 + static combine_result meet( const abstract_object_pointert &op1, - const abstract_object_pointert &op2, - bool &out_modifications); + const abstract_object_pointert &op2); /// Base implementation of the meet operation: only used if no more precise /// abstraction can be used, can only result in {TOP, BOTTOM, one of the @@ -422,10 +424,12 @@ class abstract_objectt : public std::enable_shared_from_this /// the object would be unchanged, then would return itself. /// /// \param other: The object to merge with this + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns the result of the merge. - virtual abstract_object_pointert - merge(const abstract_object_pointert &other) const; + virtual abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const; /// Helper function for base meet. Two cases: return itself (if trivially /// contained in other); return BOTTOM otherwise. diff --git a/src/analyses/variable-sensitivity/abstract_object_set.h b/src/analyses/variable-sensitivity/abstract_object_set.h index 300704f8006..8374ff0f366 100644 --- a/src/analyses/variable-sensitivity/abstract_object_set.h +++ b/src/analyses/variable-sensitivity/abstract_object_set.h @@ -44,6 +44,12 @@ class abstract_object_sett insert(value); } + void push_back(const abstract_object_pointert &v) + { + // alias for insert so we can use back_inserter + values.insert(v); + } + abstract_object_pointert first() const { return *begin(); diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index e1e53b4578b..4d081d286da 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -178,6 +178,40 @@ abstract_object_pointert abstract_value_objectt::expression_transform( return transform(expr, operands, environment, ns); } +abstract_object_pointert abstract_value_objectt::write( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const exprt &specifier, + const abstract_object_pointert &value, + bool merging_write) const +{ + UNREACHABLE; // Should not ever call write on a value; +} + +abstract_object_pointert abstract_value_objectt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const +{ + auto cast_other = + std::dynamic_pointer_cast(other); + if(cast_other) + return merge_with_value(cast_other, widen_mode); + + return abstract_objectt::merge(other, widen_mode); +} + +abstract_object_pointert +abstract_value_objectt::meet(const abstract_object_pointert &other) const +{ + auto cast_other = + std::dynamic_pointer_cast(other); + if(cast_other) + return meet_with_value(cast_other); + + return abstract_objectt::meet(other); +} + // evaluation helpers template abstract_object_pointert make_top(const typet &type) @@ -469,7 +503,7 @@ class interval_evaluator interval_abstract_value_pointert make_interval(const exprt &expr) const { - return std::make_shared(expr, environment, ns); + return interval_abstract_valuet::make_interval(expr, environment, ns); } const exprt &expression; @@ -518,7 +552,7 @@ class value_set_evaluator auto resulting_objects = evaluate_each_combination(ranges); - return resolve_values(resulting_objects); + return value_set_abstract_objectt::make_value_set(resulting_objects); } /// Evaluate expression for every combination of values in \p value_ranges. @@ -594,64 +628,6 @@ class value_set_evaluator return unwrapped; } - static abstract_object_sett - unwrap_and_extract_values(const abstract_object_sett &values) - { - abstract_object_sett unwrapped_values; - for(auto const &value : values) - { - unwrapped_values.insert( - maybe_extract_single_value(value->unwrap_context())); - } - - return unwrapped_values; - } - - static abstract_object_pointert - maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) - { - auto const &value_as_set = - std::dynamic_pointer_cast(maybe_singleton); - if(value_as_set) - { - PRECONDITION(value_as_set->get_values().size() == 1); - PRECONDITION(!std::dynamic_pointer_cast( - value_as_set->get_values().first())); - - return value_as_set->get_values().first(); - } - else - return maybe_singleton; - } - - static abstract_object_pointert - resolve_values(const abstract_object_sett &new_values) - { - PRECONDITION(!new_values.empty()); - - auto unwrapped_values = unwrap_and_extract_values(new_values); - - if(unwrapped_values.size() > value_set_abstract_objectt::max_value_set_size) - return make_interval(unwrapped_values); - - return make_value_set(unwrapped_values); - } - - static abstract_object_pointert - make_interval(const abstract_object_sett &values) - { - return std::make_shared(values.to_interval()); - } - - static abstract_object_pointert - make_value_set(const abstract_object_sett &values) - { - const auto &type = values.first()->type(); - auto value_set = std::make_shared(type); - value_set->set_values(values); - return value_set; - } - static abstract_object_pointert evaluate_conditional(const std::vector &ops) { @@ -675,7 +651,7 @@ class value_set_evaluator resulting_objects.insert(true_result); if(all_false || indeterminate) resulting_objects.insert(false_result); - return resolve_values(resulting_objects); + return value_set_abstract_objectt::make_value_set(resulting_objects); } const exprt &expression; diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 970453aa81e..2b617cd733e 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -290,7 +290,38 @@ class abstract_value_objectt : public abstract_objectt, virtual sharing_ptrt constrain(const exprt &lower, const exprt &upper) const = 0; + abstract_object_pointert write( + abstract_environmentt &environment, + const namespacet &ns, + const std::stack &stack, + const exprt &specifier, + const abstract_object_pointert &value, + bool merging_write) const final; + protected: + using abstract_value_pointert = sharing_ptrt; + + /// Attempts to do a value/value merge if both are constants, + /// otherwise falls back to the parent merge + /// + /// \param other: the abstract object to merge with + /// \param widen_mode: Indicates if this is a widening merge + /// + /// \return Returns the result of the merge + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const final; + + abstract_object_pointert + meet(const abstract_object_pointert &other) const final; + + virtual abstract_object_pointert merge_with_value( + const abstract_value_pointert &other, + const widen_modet &widen_mode) const = 0; + + virtual abstract_object_pointert + meet_with_value(const abstract_value_pointert &other) const = 0; + virtual index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const = 0; diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 4175d52e776..5b8b092bebf 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -111,19 +111,9 @@ void constant_abstract_valuet::output( } } -abstract_object_pointert -constant_abstract_valuet::merge(const abstract_object_pointert &other) const -{ - auto cast_other = - std::dynamic_pointer_cast(other); - if(cast_other) - return merge_with_value(cast_other); - - return abstract_objectt::merge(other); -} - abstract_object_pointert constant_abstract_valuet::merge_with_value( - const abstract_value_pointert &other) const + const abstract_value_pointert &other, + const widen_modet &widen_mode) const { auto other_expr = other->to_constant(); if(is_bottom() && other_expr.is_constant()) @@ -132,18 +122,7 @@ abstract_object_pointert constant_abstract_valuet::merge_with_value( if(value == other_expr) // Can we actually merge these value return shared_from_this(); - return abstract_objectt::merge(other); -} - -abstract_object_pointert -constant_abstract_valuet::meet(const abstract_object_pointert &other) const -{ - auto cast_other = - std::dynamic_pointer_cast(other); - if(cast_other) - return meet_with_value(cast_other); - - return abstract_objectt::meet(other); + return abstract_objectt::merge(other, widen_mode); } abstract_object_pointert constant_abstract_valuet::meet_with_value( diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index 9aab78aa074..2e983f90e41 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -66,30 +66,22 @@ class constant_abstract_valuet : public abstract_value_objectt protected: CLONE - /// Attempts to do a constant/constant merge if both are constants, - /// otherwise falls back to the parent merge - /// - /// \param other: the abstract object to merge with - /// - /// \return Returns the result of the merge - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; - abstract_object_pointert - meet(const abstract_object_pointert &other) const override; - -private: /// Merges another abstract value into this one /// /// \param other: the abstract object to merge with + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns a new abstract object that is the result of the merge /// unless the merge is the same as this abstract object, in which /// case it returns this. + abstract_object_pointert merge_with_value( + const abstract_value_pointert &other, + const widen_modet &widen_mode) const override; + abstract_object_pointert - merge_with_value(const abstract_value_pointert &other) const; - abstract_object_pointert - meet_with_value(const abstract_value_pointert &other) const; + meet_with_value(const abstract_value_pointert &other) const override; +private: exprt value; }; diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index 11f0b3b0300..6cbd1eaba3e 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -57,43 +57,32 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt( } abstract_object_pointert constant_pointer_abstract_objectt::merge( - const abstract_object_pointert &other) const + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { auto cast_other = std::dynamic_pointer_cast(other); if(cast_other) - { - return merge_constant_pointers(cast_other); - } - else - { - // TODO(tkiley): How do we set the result to be toppish? - return abstract_pointer_objectt::merge(other); - } + return merge_constant_pointers(cast_other, widen_mode); + + return abstract_pointer_objectt::merge(other, widen_mode); } abstract_object_pointert constant_pointer_abstract_objectt::merge_constant_pointers( - const constant_pointer_abstract_pointert &other) const + const constant_pointer_abstract_pointert &other, + const widen_modet &widen_mode) const { if(is_bottom()) - { return std::make_shared(*other); - } - else - { - bool matching_pointer = - value_stack.to_expression() == other->value_stack.to_expression(); - if(matching_pointer) - { - return shared_from_this(); - } - else - { - return abstract_pointer_objectt::merge(other); - } - } + bool matching_pointers = + value_stack.to_expression() == other->value_stack.to_expression(); + + if(matching_pointers) + return shared_from_this(); + + return abstract_pointer_objectt::merge(other, widen_mode); } exprt constant_pointer_abstract_objectt::to_constant() const @@ -196,7 +185,8 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference( { abstract_object_pointert pointed_value = environment.eval(value, ns); abstract_object_pointert merged_value = - abstract_objectt::merge(pointed_value, new_value); + abstract_objectt::merge(pointed_value, new_value, widen_modet::no) + .object; environment.assign(value, merged_value, ns); } else diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h index 78ce3cb70d5..baf09eba2bc 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h @@ -119,10 +119,12 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt /// constant pointer merge /// /// \param op1: the pointer being merged + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns the result of the merge. - abstract_object_pointert - merge(const abstract_object_pointert &op1) const override; + abstract_object_pointert merge( + const abstract_object_pointert &op1, + const widen_modet &widen_mode) const override; CLONE @@ -131,12 +133,14 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt /// value, we merge, otherwise we set to top. /// /// \param other: the pointer being merged + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns a new abstract object that is the result of the merge /// unless the merge is the same as this abstract object, in which /// case it returns this. abstract_object_pointert merge_constant_pointers( - const constant_pointer_abstract_pointert &other) const; + const constant_pointer_abstract_pointert &other, + const widen_modet &widen_mode) const; write_stackt value_stack; }; diff --git a/src/analyses/variable-sensitivity/data_dependency_context.cpp b/src/analyses/variable-sensitivity/data_dependency_context.cpp index 1ba44273e39..f3ab4cf3936 100644 --- a/src/analyses/variable-sensitivity/data_dependency_context.cpp +++ b/src/analyses/variable-sensitivity/data_dependency_context.cpp @@ -230,12 +230,14 @@ abstract_object_pointert data_dependency_contextt::update_location_context( * object with a given abstract_object * * \param other the abstract object to merge with + * \param widen_mode: Indicates if this is a widening merge * * \return the result of the merge, or 'this' if the merge would not change * the current abstract object */ -abstract_object_pointert -data_dependency_contextt::merge(const abstract_object_pointert &other) const +abstract_object_pointert data_dependency_contextt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { auto cast_other = std::dynamic_pointer_cast(other); @@ -244,12 +246,12 @@ data_dependency_contextt::merge(const abstract_object_pointert &other) const { const auto merged_parent = std::dynamic_pointer_cast( - this->write_location_contextt::merge(other)); + this->write_location_contextt::merge(other, widen_mode)); return combine(cast_other, merged_parent); } - return abstract_objectt::merge(other); + return abstract_objectt::merge(other, widen_mode); } abstract_object_pointert diff --git a/src/analyses/variable-sensitivity/data_dependency_context.h b/src/analyses/variable-sensitivity/data_dependency_context.h index 7261c125d26..de8669313db 100644 --- a/src/analyses/variable-sensitivity/data_dependency_context.h +++ b/src/analyses/variable-sensitivity/data_dependency_context.h @@ -69,8 +69,9 @@ class data_dependency_contextt : public write_location_contextt protected: CLONE - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const override; abstract_object_pointert meet(const abstract_object_pointert &other) const override; diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 340bca67d69..04b962a3658 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -39,8 +39,10 @@ abstract_object_pointert apply_to_index_range( { auto at_index = fn(index_exprt(index_expr.array(), index)); - result = (result == nullptr) ? at_index - : abstract_objectt::merge(result, at_index); + result = + (result == nullptr) + ? at_index + : abstract_objectt::merge(result, at_index, widen_modet::no).object; if(result->is_top()) // no point in continuing once we've gone top break; @@ -97,47 +99,40 @@ void full_array_abstract_objectt::set_top_internal() map.clear(); } -abstract_object_pointert -full_array_abstract_objectt::merge(const abstract_object_pointert &other) const +abstract_object_pointert full_array_abstract_objectt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { auto cast_other = std::dynamic_pointer_cast(other); if(cast_other) - { - return full_array_merge(cast_other); - } - else - { - // TODO(tkiley): How do we set the result to be toppish? Does it matter? - return abstract_aggregate_baset::merge(other); - } + return full_array_merge(cast_other, widen_mode); + + return abstract_aggregate_baset::merge(other, widen_mode); } abstract_object_pointert full_array_abstract_objectt::full_array_merge( - const full_array_pointert other) const + const full_array_pointert &other, + const widen_modet &widen_mode) const { if(is_bottom()) - { return std::make_shared(*other); + + const auto &result = + std::dynamic_pointer_cast(mutable_clone()); + + bool modified = merge_shared_maps(map, other->map, result->map, widen_mode); + if(!modified) + { + DATA_INVARIANT(verify(), "Structural invariants maintained"); + return shared_from_this(); } else { - const auto &result = - std::dynamic_pointer_cast(mutable_clone()); - - bool modified = merge_shared_maps(map, other->map, result->map); - if(!modified) - { - DATA_INVARIANT(verify(), "Structural invariants maintained"); - return shared_from_this(); - } - else - { - INVARIANT(!result->is_top(), "Merge of maps will not generate top"); - INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom"); - DATA_INVARIANT(result->verify(), "Structural invariants maintained"); - return result; - } + INVARIANT(!result->is_top(), "Merge of maps will not generate top"); + INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom"); + DATA_INVARIANT(result->verify(), "Structural invariants maintained"); + return result; } } @@ -229,7 +224,8 @@ abstract_object_pointert full_array_abstract_objectt::read_element( // Merge each known element into the TOP value for(const auto &element : map.get_view()) - result = abstract_objectt::merge(result, element.second); + result = + abstract_objectt::merge(result, element.second, widen_modet::no).object; return result; } @@ -342,7 +338,9 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( if(old_value.has_value()) // if not found it's top, so nothing to merge { result->map.replace( - index_value, abstract_objectt::merge(old_value.value(), value)); + index_value, + abstract_objectt::merge(old_value.value(), value, widen_modet::no) + .object); } DATA_INVARIANT(result->verify(), "Structural invariants maintained"); diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.h b/src/analyses/variable-sensitivity/full_array_abstract_object.h index 18a1d54e535..0c261ff0d72 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.h @@ -122,10 +122,12 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt< /// If it can't, falls back to parent merge /// /// \param other: The object to merge in + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns the result of the merge. - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const override; /// To validate that the struct object is in a valid state. /// This means either it is top or bottom, or if neither of those @@ -202,12 +204,14 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt< /// Merges an array into this array /// /// \param other: The object to merge in + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns a new abstract object that is the result of the merge /// unless the merge is the same as this abstract object, in which /// case it returns this.. - abstract_object_pointert - full_array_merge(const full_array_pointert other) const; + abstract_object_pointert full_array_merge( + const full_array_pointert &other, + const widen_modet &widen_mode) const; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_ARRAY_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index 60e214adabf..1911bab4c47 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -175,7 +175,10 @@ abstract_object_pointert full_struct_abstract_objectt::write_component( return result; } - result->map.replace(c, abstract_objectt::merge(old_value.value(), value)); + result->map.replace( + c, + abstract_objectt::merge(old_value.value(), value, widen_modet::no) + .object); } else { @@ -235,48 +238,41 @@ bool full_struct_abstract_objectt::verify() const return (is_top() || is_bottom()) == map.empty(); } -abstract_object_pointert -full_struct_abstract_objectt::merge(const abstract_object_pointert &other) const +abstract_object_pointert full_struct_abstract_objectt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { constant_struct_pointert cast_other = std::dynamic_pointer_cast(other); if(cast_other) - { - return merge_constant_structs(cast_other); - } - else - { - // TODO(tkiley): How do we set the result to be toppish? Does it matter? - return abstract_aggregate_baset::merge(other); - } + return merge_constant_structs(cast_other, widen_mode); + + return abstract_aggregate_baset::merge(other, widen_mode); } abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs( - constant_struct_pointert other) const + constant_struct_pointert other, + const widen_modet &widen_mode) const { if(is_bottom()) - { return std::make_shared(*other); + + const auto &result = + std::dynamic_pointer_cast(mutable_clone()); + + bool modified = merge_shared_maps(map, other->map, result->map, widen_mode); + + if(!modified) + { + DATA_INVARIANT(verify(), "Structural invariants maintained"); + return shared_from_this(); } else { - const auto &result = - std::dynamic_pointer_cast(mutable_clone()); - - bool modified = merge_shared_maps(map, other->map, result->map); - - if(!modified) - { - DATA_INVARIANT(verify(), "Structural invariants maintained"); - return shared_from_this(); - } - else - { - INVARIANT(!result->is_top(), "Merge of maps will not generate top"); - INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom"); - DATA_INVARIANT(result->verify(), "Structural invariants maintained"); - return result; - } + INVARIANT(!result->is_top(), "Merge of maps will not generate top"); + INVARIANT(!result->is_bottom(), "Merge of maps will not generate bottom"); + DATA_INVARIANT(result->verify(), "Structural invariants maintained"); + return result; } } diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.h b/src/analyses/variable-sensitivity/full_struct_abstract_object.h index 05cbae7e9d2..f587278d734 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.h @@ -95,12 +95,14 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt< /// Performs an element wise merge of the map for each struct /// /// \param other: the other object being merged + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns a new abstract object that is the result of the merge /// unless the merge is the same as this abstract object, in which /// case it returns this. - abstract_object_pointert - merge_constant_structs(constant_struct_pointert other) const; + abstract_object_pointert merge_constant_structs( + constant_struct_pointert other, + const widen_modet &widen_mode) const; protected: CLONE @@ -161,10 +163,12 @@ class full_struct_abstract_objectt : public abstract_aggregate_objectt< /// Otherwise we call back to the parent merge. /// /// \param other: the other object being merged + /// \param widen_mode: Indicates if this is a widening merge /// /// \return Returns the result of the merge. - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const override; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index c8b7d64690a..c7b63956eca 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -22,13 +22,6 @@ static index_range_implementation_ptrt make_interval_index_range( const constant_interval_exprt &interval, const namespacet &n); -template -std::shared_ptr make_interval(Args &&... args) -{ - return std::make_shared( - std::forward(args)...); -} - class interval_index_ranget : public index_range_implementationt { public: @@ -256,6 +249,13 @@ interval_abstract_valuet::interval_abstract_valuet( { } +interval_abstract_valuet::interval_abstract_valuet( + const exprt &lower, + const exprt &upper) + : interval_abstract_valuet(constant_interval_exprt(lower, upper)) +{ +} + interval_abstract_valuet::interval_abstract_valuet( const exprt &e, const abstract_environmentt &environment, @@ -346,30 +346,37 @@ void interval_abstract_valuet::output( } } -abstract_object_pointert -interval_abstract_valuet::merge(const abstract_object_pointert &other) const +abstract_object_pointert widening_merge( + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) { - abstract_value_pointert cast_other = - std::dynamic_pointer_cast(other); - if(cast_other) - { - return merge_with_value(cast_other); - } - else - { - return abstract_objectt::merge(other); - } + auto lower_bound = + constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower()); + auto upper_bound = + constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper()); + auto range = plus_exprt( + minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); + + auto dummy_symbol_table = symbol_tablet{}; + auto dummy_namespace = namespacet{dummy_symbol_table}; + + // should extend lower bound? + if(rhs.get_lower() < lhs.get_lower()) + lower_bound = + simplify_expr(minus_exprt(lower_bound, range), dummy_namespace); + // should extend upper bound? + if(lhs.get_upper() < rhs.get_upper()) + upper_bound = + simplify_expr(plus_exprt(upper_bound, range), dummy_namespace); + + // new interval ... + auto new_interval = constant_interval_exprt(lower_bound, upper_bound); + return interval_abstract_valuet::make_interval(new_interval); } -/// Merge another interval abstract object with this one -/// \param other The abstract value object to merge with -/// \return This if the other interval is subsumed by this, -/// other if this is subsumed by other. -/// Otherwise, a new interval abstract object -/// with the smallest interval that subsumes both -/// this and other abstract_object_pointert interval_abstract_valuet::merge_with_value( - const abstract_value_pointert &other) const + const abstract_value_pointert &other, + const widen_modet &widen_mode) const { if(other->is_bottom()) return shared_from_this(); @@ -382,30 +389,17 @@ abstract_object_pointert interval_abstract_valuet::merge_with_value( if(interval.contains(other_interval)) return shared_from_this(); - return make_interval(constant_interval_exprt( - constant_interval_exprt::get_min( - interval.get_lower(), other_interval.get_lower()), - constant_interval_exprt::get_max( - interval.get_upper(), other_interval.get_upper()))); -} + if(widen_mode == widen_modet::could_widen) + return widening_merge(interval, other_interval); -abstract_object_pointert -interval_abstract_valuet::meet(const abstract_object_pointert &other) const -{ - auto cast_other = - std::dynamic_pointer_cast(other); - if(cast_other) - return meet_with_value(cast_other); + auto lower_bound = constant_interval_exprt::get_min( + interval.get_lower(), other_interval.get_lower()); + auto upper_bound = constant_interval_exprt::get_max( + interval.get_upper(), other_interval.get_upper()); - return abstract_objectt::meet(other); + return make_interval(lower_bound, upper_bound); } -/// Meet another interval abstract object with this one -/// \param other The interval abstract object to meet with -/// \return This if the other interval subsumes this, -/// other if this subsumes other. -/// Otherwise, a new interval abstract object -/// with the intersection interval (of this and other) abstract_object_pointert interval_abstract_valuet::meet_with_value( const abstract_value_pointert &other) const { diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 3db4813e706..4a02192c4a5 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -25,12 +25,21 @@ class interval_abstract_valuet : public abstract_value_objectt interval_abstract_valuet(const typet &t, bool tp, bool bttm); explicit interval_abstract_valuet(const constant_interval_exprt &e); + interval_abstract_valuet(const exprt &lower, const exprt &upper); interval_abstract_valuet( const exprt &e, const abstract_environmentt &environment, const namespacet &ns); + template + static std::shared_ptr + make_interval(Args &&... args) + { + return std::make_shared( + std::forward(args)...); + } + ~interval_abstract_valuet() override = default; index_range_implementation_ptrt @@ -63,20 +72,29 @@ class interval_abstract_valuet : public abstract_value_objectt protected: CLONE - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; - abstract_object_pointert - meet(const abstract_object_pointert &other) const override; - -private: - using interval_abstract_value_pointert = - sharing_ptrt; + /// Merge another interval abstract object with this one + /// \param other The abstract value object to merge with + /// \param widen_mode: Indicates if this is a widening merge + /// \return This if the other interval is subsumed by this, + /// other if this is subsumed by other. + /// Otherwise, a new interval abstract object + /// with the smallest interval that subsumes both + /// this and other + abstract_object_pointert merge_with_value( + const abstract_value_pointert &other, + const widen_modet &widen_mode) const override; + + /// Meet another interval abstract object with this one + /// \param other The interval abstract object to meet with + /// \return This if the other interval subsumes this, + /// other if this subsumes other. + /// Otherwise, a new interval abstract object + /// with the intersection interval (of this and other) abstract_object_pointert - merge_with_value(const abstract_value_pointert &other) const; - abstract_object_pointert - meet_with_value(const abstract_value_pointert &other) const; + meet_with_value(const abstract_value_pointert &other) const override; +private: constant_interval_exprt interval; }; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 605317ac894..5f157851458 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -9,17 +9,18 @@ /// \file /// Value Set Abstract Object -#include "interval_abstract_value.h" +#include #include #include +#include #include +#include #include +#include #include -#include "abstract_environment.h" - static index_range_implementation_ptrt make_value_set_index_range(const std::set &vals); @@ -115,6 +116,12 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); static bool are_any_top(const abstract_object_sett &set); +static abstract_object_sett compact_values(const abstract_object_sett &values); +static abstract_object_sett widen_value_set( + const abstract_object_sett &values, + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs); + value_set_abstract_objectt::value_set_abstract_objectt(const typet &type) : abstract_value_objectt(type) { @@ -143,6 +150,22 @@ value_set_abstract_objectt::value_set_abstract_objectt( verify(); } +abstract_object_pointert value_set_abstract_objectt::make_value_set( + const abstract_object_sett &initial_values) +{ + PRECONDITION(!initial_values.empty()); + + auto values = unwrap_and_extract_values(initial_values); + + values = compact_values(values); + + const auto &type = values.first()->type(); + auto value_set = + std::make_shared(type, false, false); + value_set->set_values(values); + return value_set; +} + index_range_implementation_ptrt value_set_abstract_objectt::index_range_implementation( const namespacet &ns) const @@ -186,25 +209,9 @@ constant_interval_exprt value_set_abstract_objectt::to_interval() const return values.to_interval(); } -abstract_object_pointert value_set_abstract_objectt::write( - abstract_environmentt &environment, - const namespacet &ns, - const std::stack &stack, - const exprt &specifier, - const abstract_object_pointert &value, - bool merging_write) const -{ - abstract_object_sett new_values; - for(const auto &st_value : values) - { - new_values.insert( - st_value->write(environment, ns, stack, specifier, value, merging_write)); - } - return resolve_new_values(new_values, environment); -} - abstract_object_pointert value_set_abstract_objectt::merge_with_value( - const abstract_value_pointert &other) const + const abstract_value_pointert &other, + const widen_modet &widen_mode) const { auto union_values = !is_bottom() ? values : abstract_object_sett{}; @@ -214,6 +221,18 @@ abstract_object_pointert value_set_abstract_objectt::merge_with_value( else union_values.insert(other); + auto has_values = [](const abstract_object_pointert &v) { + return !v->is_top() && !v->is_bottom(); + }; + + if( + widen_mode == widen_modet::could_widen && has_values(shared_from_this()) && + has_values(other)) + { + union_values = + widen_value_set(union_values, to_interval(), other->to_interval()); + } + return resolve_values(union_values); } @@ -255,14 +274,6 @@ abstract_object_pointert value_set_abstract_objectt::meet_with_value( return resolve_values(meet_values); } -abstract_object_pointert value_set_abstract_objectt::resolve_new_values( - const abstract_object_sett &new_values, - const abstract_environmentt &environment) const -{ - auto result = resolve_values(new_values); - return environment.add_object_context(result); -} - abstract_object_pointert value_set_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const { @@ -271,42 +282,7 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values( if(new_values == values) return shared_from_this(); - auto unwrapped_values = unwrap_and_extract_values(new_values); - - if(unwrapped_values.size() > max_value_set_size) - { - return std::make_shared( - unwrapped_values.to_interval()); - } - //if(unwrapped_values.size() == 1) - //{ - // return (*unwrapped_values.begin()); - //} - - auto result = - std::dynamic_pointer_cast(mutable_clone()); - result->set_values(unwrapped_values); - return result; -} - -abstract_object_pointert -value_set_abstract_objectt::merge(const abstract_object_pointert &other) const -{ - auto other_value = as_value(other); - if(other_value) - return merge_with_value(other_value); - - return abstract_objectt::merge(other); -} - -abstract_object_pointert -value_set_abstract_objectt::meet(const abstract_object_pointert &other) const -{ - auto other_value = as_value(other); - if(other_value) - return meet_with_value(other_value); - - return abstract_objectt::meet(other); + return make_value_set(new_values); } void value_set_abstract_objectt::set_top_internal() @@ -379,24 +355,12 @@ void value_set_abstract_objectt::output( } } -static abstract_object_pointert -maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped) -{ - auto const &context_value = - std::dynamic_pointer_cast(maybe_wrapped); - - return context_value ? context_value->unwrap_context() : maybe_wrapped; -} - static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values) { abstract_object_sett unwrapped_values; for(auto const &value : values) - { - unwrapped_values.insert( - maybe_extract_single_value(maybe_unwrap_context(value))); - } + unwrapped_values.insert(maybe_extract_single_value(value)); return unwrapped_values; } @@ -404,8 +368,8 @@ unwrap_and_extract_values(const abstract_object_sett &values) static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) { - auto const &value_as_set = - std::dynamic_pointer_cast(maybe_singleton); + auto const &value_as_set = std::dynamic_pointer_cast( + maybe_singleton->unwrap_context()); if(value_as_set) { PRECONDITION(value_as_set->get_values().size() == 1); @@ -425,3 +389,228 @@ static bool are_any_top(const abstract_object_sett &set) return value->is_top(); }) != set.end(); } + +///////////////// +static abstract_object_sett +non_destructive_compact(const abstract_object_sett &values); +static abstract_object_sett +destructive_compact(abstract_object_sett values, int slice = 3); +static bool value_is_not_contained_in( + const abstract_object_pointert &object, + const std::vector &intervals); + +static abstract_object_sett compact_values(const abstract_object_sett &values) +{ + if(values.size() <= value_set_abstract_objectt::max_value_set_size) + return values; + + auto compacted = non_destructive_compact(values); + if(compacted.size() <= value_set_abstract_objectt::max_value_set_size) + return compacted; + + compacted = destructive_compact(values); + + return compacted; +} + +static exprt eval_expr(const exprt &e); +static bool is_le(const exprt &lhs, const exprt &rhs); +static abstract_object_sett collapse_values_in_intervals( + const abstract_object_sett &values, + const std::vector &intervals); +static void +collapse_overlapping_intervals(std::vector &intervals); + +static std::vector +collect_intervals(const abstract_object_sett &values) +{ + auto intervals = std::vector{}; + for(auto const &object : values) + { + auto value = + std::dynamic_pointer_cast(object); + auto as_expr = value->to_interval(); + if(!as_expr.is_single_value_interval()) + intervals.push_back(as_expr); + } + + collapse_overlapping_intervals(intervals); + + return intervals; +} + +void collapse_overlapping_intervals( + std::vector &intervals) +{ + std::sort( + intervals.begin(), + intervals.end(), + [](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) { + return is_le(lhs.get_lower(), rhs.get_lower()); + }); + + size_t index = 1; + while(index < intervals.size()) + { + auto &lhs = intervals[index - 1]; + auto &rhs = intervals[index]; + + bool overlap = is_le(rhs.get_lower(), lhs.get_upper()); + if(overlap) + { + auto upper = is_le(lhs.get_upper(), rhs.get_upper()) ? rhs.get_upper() + : lhs.get_upper(); + auto expanded = constant_interval_exprt(lhs.get_lower(), upper); + lhs = expanded; + intervals.erase(intervals.begin() + index); + } + else + ++index; + } +} + +static abstract_object_sett +non_destructive_compact(const abstract_object_sett &values) +{ + auto intervals = collect_intervals(values); + if(intervals.empty()) + return values; + + return collapse_values_in_intervals(values, intervals); +} + +static abstract_object_sett collapse_values_in_intervals( + const abstract_object_sett &values, + const std::vector &intervals) +{ + auto collapsed = abstract_object_sett{}; + // for each value, including the intervals + // keep it if it is not in any of the intervals + std::copy_if( + values.begin(), + values.end(), + std::back_inserter(collapsed), + [&intervals](const abstract_object_pointert &object) { + return value_is_not_contained_in(object, intervals); + }); + std::transform( + intervals.begin(), + intervals.end(), + std::back_inserter(collapsed), + [](const constant_interval_exprt &interval) { + return interval_abstract_valuet::make_interval(interval); + }); + return collapsed; +} + +static abstract_object_sett +destructive_compact(abstract_object_sett values, int slice) +{ + auto value_count = values.size(); + auto width = values.to_interval(); + auto slice_width = eval_expr(div_exprt( + minus_exprt(width.get_upper(), width.get_lower()), + from_integer(slice, width.type()))); + + auto lower_boundary = eval_expr(plus_exprt(width.get_lower(), slice_width)); + auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width)); + if( + lower_boundary == + upper_start) // adjust boundary so intervals aren't immediately combined + upper_start = eval_expr( + plus_exprt(upper_start, from_integer(1, lower_boundary.type()))); + + auto lower_slice = constant_interval_exprt(width.get_lower(), lower_boundary); + auto upper_slice = constant_interval_exprt(upper_start, width.get_upper()); + + values.insert(interval_abstract_valuet::make_interval(lower_slice)); + values.insert(interval_abstract_valuet::make_interval(upper_slice)); + + auto compacted = non_destructive_compact(values); + if(compacted.size() == value_count) + return destructive_compact(compacted, --slice); + + return compacted; +} // destructive_compact + +static bool value_is_not_contained_in( + const abstract_object_pointert &object, + const std::vector &intervals) +{ + auto value = std::dynamic_pointer_cast(object); + auto as_expr = value->to_interval(); + + return std::none_of( + intervals.begin(), + intervals.end(), + [&as_expr](const constant_interval_exprt &interval) { + return interval.contains(as_expr); + }); +} + +static exprt eval_expr(const exprt &e) +{ + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + return simplify_expr(e, ns); +} + +static bool is_le(const exprt &lhs, const exprt &rhs) +{ + auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs); + return eval_expr(is_le_expr).is_true(); +} + +static abstract_object_sett widen_value_set( + const abstract_object_sett &values, + const constant_interval_exprt &lhs, + const constant_interval_exprt &rhs) +{ + if(lhs.contains(rhs)) + return values; + + auto widened_ends = std::vector{}; + + auto lower_bound = + constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower()); + auto upper_bound = + constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper()); + auto range = plus_exprt( + minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type())); + + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + // should extend lower bound? + if(rhs.get_lower() < lhs.get_lower()) + { + auto widened_lower_bound = constant_interval_exprt( + simplify_expr(minus_exprt(lower_bound, range), ns), lower_bound); + widened_ends.push_back(widened_lower_bound); + for(auto &obj : values) + { + auto value = std::dynamic_pointer_cast(obj); + auto as_expr = value->to_interval(); + if(is_le(as_expr.get_lower(), lower_bound)) + widened_ends.push_back(as_expr); + } + } + // should extend upper bound? + if(lhs.get_upper() < rhs.get_upper()) + { + auto widened_upper_bound = constant_interval_exprt( + upper_bound, simplify_expr(plus_exprt(upper_bound, range), ns)); + widened_ends.push_back(widened_upper_bound); + for(auto &obj : values) + { + auto value = std::dynamic_pointer_cast(obj); + auto as_expr = value->to_interval(); + if(is_le(upper_bound, as_expr.get_upper())) + widened_ends.push_back(as_expr); + } + } + + collapse_overlapping_intervals(widened_ends); + return collapse_values_in_intervals(values, widened_ends); +} diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 9cf396be9cd..da672d1a988 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -30,6 +30,9 @@ class value_set_abstract_objectt : public abstract_value_objectt, const abstract_environmentt &environment, const namespacet &ns); + static abstract_object_pointert + make_value_set(const abstract_object_sett &initial_values); + index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override; @@ -49,47 +52,27 @@ class value_set_abstract_objectt : public abstract_value_objectt, return values; } - /// Setter for updating the stored values - /// \param other_values: the new (non-empty) set of values - void set_values(const abstract_object_sett &other_values); - /// The threshold size for value-sets: past this threshold the object is /// either converted to interval or marked as `top`. static const size_t max_value_set_size = 10; - /// \copydoc abstract_objectt::write - /// - /// Delegate writing to stored values. - abstract_object_pointert write( - abstract_environmentt &environment, - const namespacet &ns, - const std::stack &stack, - const exprt &specifier, - const abstract_object_pointert &value, - bool merging_write) const override; - void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; protected: CLONE - /// \copydoc abstract_object::merge - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge_with_value( + const abstract_value_pointert &other, + const widen_modet &widen_mode) const override; + abstract_object_pointert - meet(const abstract_object_pointert &other) const override; + meet_with_value(const abstract_value_pointert &other) const override; private: - /// Update the set of stored values to \p new_values. Build a new abstract - /// object of the right type if necessary. - /// \param new_values: potentially new set of values - /// \param environment: the abstract environment - /// \return the abstract object representing \p new_values (either 'this' or - /// something new) - abstract_object_pointert resolve_new_values( - const abstract_object_sett &new_values, - const abstract_environmentt &environment) const; + /// Setter for updating the stored values + /// \param other_values: the new (non-empty) set of values + void set_values(const abstract_object_sett &other_values); /// Update the set of stored values to \p new_values. Build a new abstract /// object of the right type if necessary. @@ -99,11 +82,6 @@ class value_set_abstract_objectt : public abstract_value_objectt, abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const; - abstract_object_pointert - merge_with_value(const abstract_value_pointert &other) const; - abstract_object_pointert - meet_with_value(const abstract_value_pointert &other) const; - // data abstract_object_sett values; diff --git a/src/analyses/variable-sensitivity/value_set_abstract_value.cpp b/src/analyses/variable-sensitivity/value_set_abstract_value.cpp deleted file mode 100644 index d71608d6b2b..00000000000 --- a/src/analyses/variable-sensitivity/value_set_abstract_value.cpp +++ /dev/null @@ -1,214 +0,0 @@ -/*******************************************************************\ - - Module: analyses variable-sensitivity variable-sensitivity-value-set - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include "value_set_abstract_value.h" - -#include -#include - -#include - -value_set_abstract_valuet::value_set_abstract_valuet( - const typet &type, - bool top, - bool bottom) - : abstract_objectt{type, top, bottom}, values{} -{ -} - -const value_set_abstract_valuet::valuest & -value_set_abstract_valuet::get_values() const -{ - PRECONDITION(!is_top()); - PRECONDITION(!is_bottom()); - return values; -} - -abstract_object_pointert -value_set_abstract_valuet::merge(const abstract_object_pointert &other) const -{ - if(is_top()) - { - return shared_from_this(); - } - - if(other->is_top()) - { - return other; - } - - if(is_bottom()) - { - return other; - } - - if(other->is_bottom()) - { - return shared_from_this(); - } - - if( - auto other_value_set = - dynamic_cast(other.get())) - { - valuest merged_values{values}; - auto const &other_values = other_value_set->get_values(); - merged_values.insert(other_values.begin(), other_values.end()); - return std::make_shared( - type(), std::move(merged_values)); - } - return abstract_objectt::merge(other); -} - -value_set_abstract_valuet::value_set_abstract_valuet( - const typet &type, - valuest values) - : abstract_objectt{type, values.size() > max_value_set_size, values.empty()}, - values{std::move(values)} -{ - if(values.size() > max_value_set_size) - { - this->values.clear(); - } -} - -value_set_abstract_valuet::value_set_abstract_valuet( - exprt expr, - const abstract_environmentt &environment, - const namespacet &ns) - : value_set_abstract_valuet{expr.type(), valuest{expr}} -{ -} - -exprt value_set_abstract_valuet::to_constant() const -{ - if(!is_top() && !is_bottom() && values.size() == 1) - { - return *values.begin(); - } - return abstract_objectt::to_constant(); -} - -void value_set_abstract_valuet::output( - std::ostream &out, - const class ai_baset &, - const namespacet &ns) const -{ - if(is_bottom()) - { - out << "BOTTOM"; - return; - } - else if(is_top()) - { - out << "TOP"; - return; - } - - std::vector vals; - for(const auto &elem : values) - { - vals.push_back(expr2c(elem, ns)); - } - - std::sort(vals.begin(), vals.end()); - - out << "{ "; - for(const auto &val : vals) - { - out << val << " "; - } - out << "}"; -} - -static void merge_all_possible_results( - std::shared_ptr &out_value, - const exprt &expr, - const std::vector &operand_value_sets, - const namespacet &ns, - std::vector &operands_so_far) -{ - if(expr.operands().size() == operands_so_far.size()) - { - exprt expr_with_evaluated_operands_filled_in = expr; - expr_with_evaluated_operands_filled_in.operands() = operands_so_far; - simplify(expr_with_evaluated_operands_filled_in, ns); - if(expr_with_evaluated_operands_filled_in.is_constant()) - { - auto post_merge = abstract_objectt::merge( - out_value, - std::make_shared( - expr.type(), - value_set_abstract_valuet::valuest{ - expr_with_evaluated_operands_filled_in})); - if( - auto post_merge_casted = - std::dynamic_pointer_cast( - post_merge)) - { - out_value = post_merge_casted; - return; - } - } - out_value = std::make_shared(expr.type()); - } - else - { - for(auto const &operand_value : - operand_value_sets[operands_so_far.size()]->get_values()) - { - operands_so_far.push_back(operand_value); - merge_all_possible_results( - out_value, expr, operand_value_sets, ns, operands_so_far); - operands_so_far.pop_back(); - } - } -} - -static std::shared_ptr -merge_all_possible_results( - const exprt &expr, - const std::vector &operand_value_sets, - const namespacet &ns) -{ - const bool is_top = false; - const bool is_bottom = true; - auto result_abstract_value = - std::make_shared( - expr.type(), is_top, is_bottom); - auto operands_so_far = std::vector{}; - merge_all_possible_results( - result_abstract_value, expr, operand_value_sets, ns, operands_so_far); - return result_abstract_value; -} - -abstract_object_pointert value_set_abstract_valuet::expression_transform( - const exprt &expr, - const std::vector &operands, - const abstract_environmentt &environment, - const namespacet &ns) const -{ - // TODO possible special case handling for things like - // __CPROVER_rounding_mode where we know what valid values look like - // which we could make use of in place of TOP - auto operand_value_sets = std::vector{}; - for(auto const &possible_value_set : operands) - { - PRECONDITION(possible_value_set != nullptr); - const auto as_value_set = - dynamic_cast(possible_value_set.get()); - if( - as_value_set == nullptr || as_value_set->is_top() || - as_value_set->is_bottom()) - { - return std::make_shared(expr.type()); - } - operand_value_sets.push_back(as_value_set); - } - return merge_all_possible_results(expr, operand_value_sets, ns); -} diff --git a/src/analyses/variable-sensitivity/value_set_abstract_value.h b/src/analyses/variable-sensitivity/value_set_abstract_value.h deleted file mode 100644 index d339a4d4357..00000000000 --- a/src/analyses/variable-sensitivity/value_set_abstract_value.h +++ /dev/null @@ -1,68 +0,0 @@ -/*******************************************************************\ - - Module: analyses variable-sensitivity variable-sensitivity-value-set - - Author: Diffblue Ltd. - -\*******************************************************************/ - -/// \file -/// Value sets for primitives - -// NOLINTNEXTLINE(whitespace/line_length) -#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H -// NOLINTNEXTLINE(whitespace/line_length) -#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H - -#include - -#include - -class value_set_abstract_valuet : public abstract_objectt -{ -public: - using valuest = std::unordered_set; - - explicit value_set_abstract_valuet( - const typet &type, - bool top = true, - bool bottom = false); - value_set_abstract_valuet( - exprt expr, - const abstract_environmentt &environment, - const namespacet &ns); - value_set_abstract_valuet(const typet &type, valuest values); - - /// Get the possible values for this abstract object. - /// Only meaningful when this is neither TOP nor BOTTOM. - const valuest &get_values() const; - - CLONE - - /// TODO arbitrary limit, make configurable - static constexpr std::size_t max_value_set_size = 10; - - exprt to_constant() const override; - - abstract_object_pointert expression_transform( - const exprt &expr, - const std::vector &operands, - const abstract_environmentt &environment, - const namespacet &ns) const override; - - void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) - const override; - -protected: - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; - -private: - /// If BOTTOM then empty. - /// If neither BOTTOM or TOP then the exact set of values. - /// If TOP this field doesn't mean anything and shouldn't be looked at. - valuest values; -}; - -// NOLINTNEXTLINE(whitespace/line_length) -#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_VALUE_H diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp index 5167de20b7a..07fc3fab966 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -24,13 +24,6 @@ unwrap_and_extract_values(const abstract_object_sett &values); static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); -/// Helper for converting context objects into its abstract-value children -/// \p maybe_wrapped: either an abstract value (or a set of those) or one -/// wrapped in a context -/// \return an abstract value without context (though it might be as set) -static abstract_object_pointert -maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped); - /// Recursively construct a combination \p sub_con from \p super_con and once /// constructed call \p f. /// \param super_con: vector of some containers storing the values @@ -140,14 +133,6 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference( return shared_from_this(); } -abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values( - const abstract_object_sett &new_values, - const abstract_environmentt &environment) const -{ - auto result = resolve_values(new_values); - return environment.add_object_context(result); -} - abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const { @@ -173,7 +158,8 @@ abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values( } abstract_object_pointert value_set_pointer_abstract_objectt::merge( - const abstract_object_pointert &other) const + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { auto cast_other = std::dynamic_pointer_cast(other); if(cast_other) @@ -183,7 +169,7 @@ abstract_object_pointert value_set_pointer_abstract_objectt::merge( return resolve_values(union_values); } - return abstract_objectt::merge(other); + return abstract_objectt::merge(other, widen_mode); } void value_set_pointer_abstract_objectt::set_values( @@ -223,8 +209,7 @@ unwrap_and_extract_values(const abstract_object_sett &values) abstract_object_sett unwrapped_values; for(auto const &value : values) { - unwrapped_values.insert( - maybe_extract_single_value(maybe_unwrap_context(value))); + unwrapped_values.insert(maybe_extract_single_value(value)); } return unwrapped_values; @@ -233,8 +218,8 @@ unwrap_and_extract_values(const abstract_object_sett &values) abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) { - auto const &value_as_set = - std::dynamic_pointer_cast(maybe_singleton); + auto const &value_as_set = std::dynamic_pointer_cast( + maybe_singleton->unwrap_context()); if(value_as_set) { PRECONDITION(value_as_set->get_values().size() == 1); @@ -246,12 +231,3 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) else return maybe_singleton; } - -abstract_object_pointert -maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped) -{ - auto const &context_value = - std::dynamic_pointer_cast(maybe_wrapped); - - return context_value ? context_value->unwrap_context() : maybe_wrapped; -} diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h index 8975eae1ba3..bce89cafbed 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -71,20 +71,11 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt, CLONE /// \copydoc abstract_object::merge - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const override; private: - /// Update the set of stored values to \p new_values. Build a new abstract - /// object of the right type if necessary. - /// \param new_values: potentially new set of values - /// \param environment: the abstract environment - /// \return the abstract object representing \p new_values (either 'this' or - /// something new) - abstract_object_pointert resolve_new_values( - const abstract_object_sett &new_values, - const abstract_environmentt &environment) const; - /// Update the set of stored values to \p new_values. Build a new abstract /// object of the right type if necessary. /// \param new_values: potentially new set of values diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index f127d9c2cfc..5dde92aedb1 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp @@ -35,8 +35,6 @@ vsd_configt vsd_configt::from_options(const optionst &options) config.context_tracking.last_write_context = true; config.context_tracking.data_dependency_context = options.get_bool_option("data-dependencies"); - config.advanced_sensitivities.new_value_set = - options.get_bool_option("new-value-set"); config.flow_sensitivity = (options.get_bool_option("flow-insensitive")) ? flow_sensitivityt::insensitive diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 2370629e4f1..f47f75e43ad 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -201,9 +201,10 @@ bool variable_sensitivity_domaint::merge( std::cout << "Merging from/to:\n " << from->location_number << " --> " << to->location_number << '\n'; #endif - + auto widen_mode = + from->should_widen(*to) ? widen_modet::could_widen : widen_modet::no; // Use the abstract_environment merge - bool any_changes = abstract_state.merge(b.abstract_state); + bool any_changes = abstract_state.merge(b.abstract_state, widen_mode); DATA_INVARIANT(abstract_state.verify(), "Structural invariant"); return any_changes; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 9b298ab93ba..4bb1a8cfd16 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -7,7 +7,6 @@ \*******************************************************************/ #include "variable_sensitivity_object_factory.h" #include "full_array_abstract_object.h" -#include "value_set_abstract_value.h" #include "value_set_pointer_abstract_object.h" template @@ -144,11 +143,6 @@ variable_sensitivity_object_factoryt::get_abstract_object( return initialize_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); case VALUE_SET: - if(configuration.advanced_sensitivities.new_value_set) - { - return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); - } return initialize_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); diff --git a/src/analyses/variable-sensitivity/write_location_context.cpp b/src/analyses/variable-sensitivity/write_location_context.cpp index b94de3f1520..090ac61d73e 100644 --- a/src/analyses/variable-sensitivity/write_location_context.cpp +++ b/src/analyses/variable-sensitivity/write_location_context.cpp @@ -102,20 +102,37 @@ abstract_object_pointert write_location_contextt::write( * object with a given abstract_object * * \param other the abstract object to merge with + * \param widen_mode: Indicates if this is a widening merge * * \return the result of the merge, or 'this' if the merge would not change * the current abstract object */ -abstract_object_pointert -write_location_contextt::merge(const abstract_object_pointert &other) const +abstract_object_pointert write_location_contextt::merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const { auto cast_other = std::dynamic_pointer_cast(other); if(cast_other) - return combine(cast_other, abstract_objectt::merge); + { + auto merge_fn = [&widen_mode]( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2) { + return abstract_objectt::merge(op1, op2, widen_mode); + }; + return combine(cast_other, merge_fn); + } - return abstract_objectt::merge(other); + return abstract_objectt::merge(other, widen_mode); +} + +// need wrapper function here to disambiguate meet overload +abstract_objectt::combine_result object_meet( + const abstract_object_pointert &op1, + const abstract_object_pointert &op2) +{ + return abstract_objectt::meet(op1, op2); } abstract_object_pointert @@ -125,7 +142,7 @@ write_location_contextt::meet(const abstract_object_pointert &other) const std::dynamic_pointer_cast(other); if(cast_other) - return combine(cast_other, abstract_objectt::meet); + return combine(cast_other, object_meet); return abstract_objectt::meet(other); } @@ -134,10 +151,7 @@ abstract_object_pointert write_location_contextt::combine( const write_location_context_ptrt &other, combine_fn fn) const { - bool child_modified = false; - - auto merged_child = - fn(child_abstract_object, other->child_abstract_object, child_modified); + auto combined_child = fn(child_abstract_object, other->child_abstract_object); abstract_objectt::locationst location_union = get_location_union(other->get_last_written_locations()); @@ -145,13 +159,13 @@ abstract_object_pointert write_location_contextt::combine( bool merge_locations = location_union.size() > get_last_written_locations().size(); - if(child_modified || merge_locations) + if(combined_child.modified || merge_locations) { const auto &result = std::dynamic_pointer_cast(mutable_clone()); - if(child_modified) + if(combined_child.modified) { - result->set_child(merged_child); + result->set_child(combined_child.object); } if(merge_locations) { diff --git a/src/analyses/variable-sensitivity/write_location_context.h b/src/analyses/variable-sensitivity/write_location_context.h index f62cbea6e0b..57c100e5934 100644 --- a/src/analyses/variable-sensitivity/write_location_context.h +++ b/src/analyses/variable-sensitivity/write_location_context.h @@ -99,8 +99,9 @@ class write_location_contextt : public context_abstract_objectt protected: CLONE - abstract_object_pointert - merge(const abstract_object_pointert &other) const override; + abstract_object_pointert merge( + const abstract_object_pointert &other, + const widen_modet &widen_mode) const override; abstract_object_pointert meet(const abstract_object_pointert &other) const override; @@ -122,10 +123,9 @@ class write_location_contextt : public context_abstract_objectt virtual abstract_objectt::locationst get_last_written_locations() const; private: - using combine_fn = abstract_object_pointert (*)( + using combine_fn = std::function; using write_location_context_ptrt = std::shared_ptr; diff --git a/unit/Makefile b/unit/Makefile index d2447f7d127..88d7c054396 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -23,14 +23,16 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/eval-member-access.cpp \ analyses/variable-sensitivity/interval_abstract_value/meet.cpp \ analyses/variable-sensitivity/interval_abstract_value/merge.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 \ analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \ analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \ analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \ - analyses/variable-sensitivity/value_set/abstract_value.cpp \ + analyses/variable-sensitivity/value_set_abstract_object/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/widening_merge.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ ansi-c/max_malloc_size.cpp \ ansi-c/type2name.cpp \ diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index 28c46916942..22891493a92 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -27,12 +27,11 @@ SCENARIO( abstract_object_pointert op1 = make_top_object(); abstract_object_pointert op2 = make_top_object(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_TOP(result); } } @@ -41,12 +40,11 @@ SCENARIO( abstract_object_pointert op1 = make_top_object(); abstract_object_pointert op2 = make_bottom_object(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("result is unmodified TOP") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_TOP(result); } } @@ -55,12 +53,11 @@ SCENARIO( abstract_object_pointert op1 = make_bottom_object(); abstract_object_pointert op2 = make_top_object(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("result is modified TOP") { - EXPECT_MODIFIED(result, modified); + EXPECT_MODIFIED(result); EXPECT_TOP(result); } } @@ -69,12 +66,11 @@ SCENARIO( abstract_object_pointert op1 = make_bottom_object(); abstract_object_pointert op2 = make_bottom_object(); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("result is unmodified BOTTOM") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_BOTTOM(result); } } @@ -101,12 +97,11 @@ SCENARIO( auto top1 = make_top_object(); auto op2 = make_constant(val1, environment, ns); - bool modified; - auto result = abstract_objectt::merge(top1, op2, modified); + auto result = abstract_objectt::merge(top1, op2, widen_modet::no); THEN("the result is unmodified TOP") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_TOP(result); } } @@ -115,12 +110,11 @@ SCENARIO( auto top1 = make_top_object(); auto top2 = make_top_constant(); - bool modified; - auto result = abstract_objectt::merge(top1, top2, modified); + auto result = abstract_objectt::merge(top1, top2, widen_modet::no); THEN("the result is unmodified TOP") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_TOP(result); } } @@ -129,12 +123,11 @@ SCENARIO( auto top1 = make_top_object(); auto bottom2 = make_bottom_constant(); - bool modified; - auto result = abstract_objectt::merge(top1, bottom2, modified); + auto result = abstract_objectt::merge(top1, bottom2, widen_modet::no); THEN("the result is unmodified TOP") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_TOP(result); } } @@ -143,12 +136,11 @@ SCENARIO( auto op1 = make_bottom_object(); auto op2 = make_constant(val1, environment, ns); - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("the result is modified TOP") { - EXPECT_MODIFIED(result, modified); + EXPECT_MODIFIED(result); EXPECT_TOP(result); } } @@ -157,12 +149,11 @@ SCENARIO( auto op1 = make_bottom_object(); auto top2 = make_top_constant(); - bool modified; - auto result = abstract_objectt::merge(op1, top2, modified); + auto result = abstract_objectt::merge(op1, top2, widen_modet::no); THEN("the result is modified TOP") { - EXPECT_MODIFIED(result, modified); + EXPECT_MODIFIED(result); EXPECT_TOP(result); } } @@ -171,12 +162,11 @@ SCENARIO( auto bottom1 = make_bottom_object(); auto bottom2 = make_bottom_constant(); - bool modified; - auto result = abstract_objectt::merge(bottom1, bottom2, modified); + auto result = abstract_objectt::merge(bottom1, bottom2, widen_modet::no); THEN("result is unmodified BOTTOM") { - EXPECT_UNMODIFIED(result, modified); + EXPECT_UNMODIFIED(result); EXPECT_BOTTOM(result); } } diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp index b0b4e3f456d..bc9a36a8ede 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp @@ -16,9 +16,8 @@ static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) { - bool modified; - auto result = abstract_objectt::meet(op1, op2, modified); - return as_constant(result); + auto result = abstract_objectt::meet(op1, op2); + return as_constant(result.object); } static void THEN_BOTTOM(std::shared_ptr &result) diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 0b8c776fdf8..4e7f873bebd 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -16,10 +16,9 @@ static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) { - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - return {modified, as_constant(result)}; + return {result.modified, as_constant(result.object)}; } SCENARIO( diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index 6ffeecc384b..bcf69aa2c86 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -1,3 +1,10 @@ +/*******************************************************************\ + + Module: Array Access Unit Tests + + Author: Jez Higgins + +\*******************************************************************/ #include #include @@ -110,8 +117,8 @@ exprt fetch_element( if(object->is_top()) // oh! return object->to_constant(); - const auto unwrapped = object->unwrap_context(); - auto value = std::dynamic_pointer_cast(unwrapped); + auto value = + std::dynamic_pointer_cast(object->unwrap_context()); REQUIRE(value); return value->to_constant(); } diff --git a/unit/analyses/variable-sensitivity/eval.cpp b/unit/analyses/variable-sensitivity/eval.cpp index 08f0ab1146d..6161674f281 100644 --- a/unit/analyses/variable-sensitivity/eval.cpp +++ b/unit/analyses/variable-sensitivity/eval.cpp @@ -50,11 +50,9 @@ SCENARIO( std::dynamic_pointer_cast(result)); REQUIRE_FALSE(result->is_top()); REQUIRE_FALSE(result->is_bottom()); - const auto unwrapped = - std::dynamic_pointer_cast(result) - ->unwrap_context(); auto result_as_interval = - std::dynamic_pointer_cast(unwrapped); + std::dynamic_pointer_cast( + result->unwrap_context()); REQUIRE(result_as_interval); REQUIRE( result_as_interval->to_interval().get_lower() == 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 b20fcb2f051..b95b949d9ce 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -107,25 +107,23 @@ SCENARIO( array_utilt util(enviroment, ns); - abstract_object_pointert result; - bool modified = false; - WHEN("Merging two constant array AOs with the same array") { auto op1 = util.build_array(val1); auto op2 = util.build_array(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant array AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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]); @@ -133,7 +131,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN("Merging two constant array AOs with different value arrays") @@ -141,10 +139,11 @@ SCENARIO( auto op1 = util.build_array(val1); auto op2 = util.build_array(val2); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN( "A new constant array AO whose first value is the same and " @@ -154,7 +153,7 @@ SCENARIO( REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + 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]); @@ -162,7 +161,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // Since it has modified, we definitely shouldn't be reusing the pointer - REQUIRE_FALSE(result == op1); + REQUIRE_FALSE(result.object == op1); } } WHEN( @@ -172,17 +171,18 @@ SCENARIO( auto op1 = util.build_array(val1); auto op2 = util.build_top_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new constant array AO set to top should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); @@ -190,7 +190,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // We can't reuse the abstract object as the value has changed - REQUIRE(result != op1); + REQUIRE(result.object != op1); } } WHEN( @@ -200,17 +200,18 @@ SCENARIO( auto op1 = util.build_array(val1); auto op2 = util.build_bottom_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original const AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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]); @@ -218,7 +219,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -228,17 +229,18 @@ SCENARIO( auto op1 = util.build_top_array(array_type); auto op2 = util.build_array(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant array AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); @@ -246,7 +248,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -256,17 +258,18 @@ SCENARIO( auto op1 = util.build_top_array(array_type); auto op2 = util.build_top_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant array AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); @@ -274,7 +277,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -284,17 +287,18 @@ SCENARIO( auto op1 = util.build_top_array(array_type); auto op2 = util.build_bottom_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant array AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); @@ -302,7 +306,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -312,17 +316,18 @@ SCENARIO( auto op1 = util.build_bottom_array(array_type); auto op2 = util.build_array(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new AO should be returned with op2s valuee") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + 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]); @@ -330,7 +335,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); // Is optimal - REQUIRE(result != op1); + REQUIRE(result.object != op1); } } WHEN( @@ -340,17 +345,18 @@ SCENARIO( auto op1 = util.build_bottom_array(array_type); auto op2 = util.build_top_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new constant array AO should be returned set to top ") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_index(cast_result, i0) == nil_exprt()); @@ -358,7 +364,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == nil_exprt()); // Is optimal - REQUIRE(result != op1); + REQUIRE(result.object != op1); } } WHEN( @@ -368,22 +374,23 @@ SCENARIO( auto op1 = util.build_bottom_array(array_type); auto op2 = util.build_bottom_array(array_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original bottom AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE(cast_result->is_bottom()); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -394,12 +401,11 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("We should get a new AO of the same type but set to top") { @@ -407,12 +413,12 @@ SCENARIO( REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); // Since it has modified, we definitely shouldn't be reusing the pointer - REQUIRE_FALSE(result == op1); + REQUIRE_FALSE(result.object == op1); } } WHEN( @@ -423,19 +429,18 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("We should get the same constant array AO back") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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]); @@ -443,7 +448,7 @@ SCENARIO( REQUIRE(util.read_index(cast_result, i2) == val1.operands()[2]); // Is optimal - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } WHEN( @@ -454,23 +459,22 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("We should get the same abstract object back") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -483,22 +487,21 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Should get the same abstract object back") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -511,21 +514,20 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return a new top abstract object of the same type") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // We don't optimize for returning the second parameter if we can // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -536,22 +538,21 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return the original abstract object") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE_FALSE(result->is_top()); - REQUIRE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE(result.object->is_bottom()); // Optimization check - REQUIRE(result == op1); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -562,19 +563,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_array(val1); - bool modified; - - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to top with a constant array AO set to top") @@ -583,18 +581,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_top_array(array_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to top with a constant array AO set to bottom") @@ -603,18 +599,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_bottom_array(array_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to bottom with a constant array AO with a value") @@ -623,17 +617,16 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_array(val1); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The a new top AO should be returned") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(typeid(result.get()) == typeid(const abstract_objectt *)); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE( + typeid(result.object.get()) == typeid(const abstract_objectt *)); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); } // We don't optimize for returning the second parameter if we can @@ -644,16 +637,14 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_top_array(array_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The a new top AO should be returned") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // We don't optimize for returning the second parameter if we can } @@ -664,18 +655,16 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_bottom_array(array_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE_FALSE(result->is_top()); - REQUIRE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE(result.object->is_bottom()); - REQUIRE(result == op1); + REQUIRE(result.object == op1); } } } 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 a222b7a1519..b23038bf5c7 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -134,25 +134,23 @@ SCENARIO( struct_utilt util(enviroment, ns); - abstract_object_pointert result; - bool modified = false; - WHEN("Merging two constant struct AOs with the same contents") { auto op1 = util.build_struct(val1); auto op2 = util.build_struct(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original struct AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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()); @@ -160,7 +158,7 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == val1.op2()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); } } WHEN("Merging two constant struct AOs with the different contents") @@ -168,10 +166,11 @@ SCENARIO( auto op1 = util.build_struct(val1); auto op2 = util.build_struct(val2); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN( "A new constant struct AO whose a component is the same and the " "b and c are set to top") @@ -180,7 +179,7 @@ SCENARIO( REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == val1.op0()); @@ -188,7 +187,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // Since it has modified, we definitely shouldn't be reusing the pointer - REQUIRE_FALSE(result == op1); + REQUIRE(result.modified); + REQUIRE_FALSE(result.object == op1); } } WHEN( @@ -198,17 +198,18 @@ SCENARIO( auto op1 = util.build_struct(val1); auto op2 = util.build_top_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new constant struct AO set to top should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == nil_exprt()); @@ -216,7 +217,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // We can't reuse the abstract object as the value has changed - REQUIRE(result != op1); + REQUIRE(result.modified); + REQUIRE(result.object != op1); } } WHEN( @@ -226,17 +228,18 @@ SCENARIO( auto op1 = util.build_struct(val1); auto op2 = util.build_bottom_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original const AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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()); @@ -244,7 +247,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == val1.op2()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -254,17 +258,18 @@ SCENARIO( auto op1 = util.build_top_struct(struct_type); auto op2 = util.build_struct(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant struct AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == nil_exprt()); @@ -272,7 +277,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -282,17 +288,18 @@ SCENARIO( auto op1 = util.build_top_struct(struct_type); auto op2 = util.build_top_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant struct AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == nil_exprt()); @@ -300,7 +307,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -310,17 +318,18 @@ SCENARIO( auto op1 = util.build_top_struct(struct_type); auto op2 = util.build_bottom_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original constant struct AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == nil_exprt()); @@ -328,7 +337,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -338,17 +348,18 @@ SCENARIO( auto op1 = util.build_bottom_struct(struct_type); auto op2 = util.build_struct(val1); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new AO should be returned with op2s valuee") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == val1.op0()); @@ -356,7 +367,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == val1.op2()); // Is optimal - REQUIRE(result != op1); + REQUIRE(result.modified); + REQUIRE(result.object != op1); } } WHEN( @@ -366,17 +378,18 @@ SCENARIO( auto op1 = util.build_bottom_struct(struct_type); auto op2 = util.build_top_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("A new constant struct AO should be returned set to top ") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); REQUIRE(util.read_component(cast_result, a) == nil_exprt()); @@ -384,7 +397,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == nil_exprt()); // Is optimal - REQUIRE(result != op1); + REQUIRE(result.modified); + REQUIRE(result.object != op1); } } WHEN( @@ -394,22 +408,24 @@ SCENARIO( auto op1 = util.build_bottom_struct(struct_type); auto op2 = util.build_bottom_struct(struct_type); - result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("The original bottom AO should be returned") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + REQUIRE_FALSE(result.modified); REQUIRE_FALSE(cast_result->is_top()); REQUIRE(cast_result->is_bottom()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -420,12 +436,11 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("We should get a new AO of the same type but set to top") { @@ -433,12 +448,12 @@ SCENARIO( REQUIRE(cast_result); // Correctness of merge - REQUIRE(modified); + REQUIRE(result.modified); REQUIRE(cast_result->is_top()); REQUIRE_FALSE(cast_result->is_bottom()); // Since it has modified, we definitely shouldn't be reusing the pointer - REQUIRE_FALSE(result == op1); + REQUIRE_FALSE(result.object == op1); } } WHEN( @@ -449,19 +464,18 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); THEN("We should get the same constant struct AO back") { // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); // Correctness of merge - REQUIRE_FALSE(modified); + 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()); @@ -469,7 +483,8 @@ SCENARIO( REQUIRE(util.read_component(cast_result, c) == val1.op2()); // Is optimal - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } WHEN( @@ -480,23 +495,22 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("We should get the same abstract object back") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -509,22 +523,21 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Should get the same abstract object back") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -537,21 +550,20 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), true, false); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return a new top abstract object of the same type") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // We don't optimize for returning the second parameter if we can // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -562,22 +574,22 @@ SCENARIO( const auto &op2 = std::make_shared(val1.type(), false, true); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("Return the original abstract object") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE_FALSE(result->is_top()); - REQUIRE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE(result.object->is_bottom()); // Optimization check - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); // Is type still correct const auto &cast_result = - std::dynamic_pointer_cast(result); + std::dynamic_pointer_cast( + result.object); // Though we may become top or bottom, the type should be unchanged REQUIRE(cast_result); } @@ -588,19 +600,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_struct(val1); - bool modified; - - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to top with a constant struct AO set to top") @@ -609,18 +618,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_top_struct(struct_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to top with a constant struct AO set to bottom") @@ -629,18 +636,16 @@ SCENARIO( std::make_shared(val1.type(), true, false); const auto &op2 = util.build_bottom_struct(struct_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Is optimal - REQUIRE(op1 == result); + REQUIRE(result.object == op1); } } WHEN("Merging AO set to bottom with a constant struct AO with a value") @@ -649,17 +654,16 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_struct(val1); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The a new top AO should be returned") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(typeid(result.get()) == typeid(const abstract_objectt *)); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE( + typeid(result.object.get()) == typeid(const abstract_objectt *)); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); } // We don't optimize for returning the second parameter if we can @@ -670,16 +674,14 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_top_struct(struct_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The a new top AO should be returned") { // Simple correctness of merge - REQUIRE(modified); - REQUIRE(result->is_top()); - REQUIRE_FALSE(result->is_bottom()); + REQUIRE(result.modified); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // We don't optimize for returning the second parameter if we can } @@ -690,18 +692,17 @@ SCENARIO( std::make_shared(val1.type(), false, true); const auto &op2 = util.build_bottom_struct(struct_type); - bool modified; - abstract_object_pointert result = - abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); THEN("The original AO should be returned") { // Simple correctness of merge - REQUIRE_FALSE(modified); - REQUIRE_FALSE(result->is_top()); - REQUIRE(result->is_bottom()); + REQUIRE_FALSE(result.modified); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE(result.object->is_bottom()); - REQUIRE(result == op1); + REQUIRE_FALSE(result.modified); + REQUIRE(result.object == op1); } } } diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp index a4990a2ac32..198e78f0da1 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp @@ -20,9 +20,8 @@ static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) { - bool modified; - auto result = abstract_objectt::meet(op1, op2, modified); - return as_interval(result); + auto result = abstract_objectt::meet(op1, op2); + return as_interval(result.object); } static void THEN_BOTTOM(std::shared_ptr &result) diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp index e0f737ec051..a8e97f2faa5 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ - Module: Unit tests for intervalabstract_valuet::merge + Module: Unit tests for interval_abstract_valuet::merge Author: Jez Higgins. @@ -16,10 +16,9 @@ static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) { - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - return {modified, as_interval(result)}; + return {result.modified, as_interval(result.object)}; } SCENARIO( diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp new file mode 100644 index 00000000000..110a7b46a42 --- /dev/null +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -0,0 +1,306 @@ +/*******************************************************************\ + + Module: Unit tests for interval_abstract_valuet::merge + + Author: Jez Higgins. + +\*******************************************************************/ + +#include +#include +#include + +#include +#include + +static merge_result +widening_merge(abstract_object_pointert op1, abstract_object_pointert op2) +{ + auto result = abstract_objectt::merge(op1, op2, widen_modet::could_widen); + + return {result.modified, as_interval(result.object)}; +} + +SCENARIO( + "widening merge interval_abstract_value", + "[core][analyses][variable-sensitivity][interval_abstract_value][merge]") +{ + 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 val4 = from_integer(4, type); + const exprt val5 = from_integer(5, type); + const exprt val8 = from_integer(8, type); + const exprt val10 = from_integer(10, type); + const exprt val1minus = from_integer(-1, type); + const exprt val2minus = from_integer(-2, type); + const exprt val3minus = from_integer(-3, type); + const exprt val4minus = from_integer(-4, type); + const exprt val5minus = from_integer(-5, type); + const exprt val8minus = from_integer(-8, type); + const exprt val10minus = from_integer(-10, 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 merges which don't widen") + { + WHEN("merging [1, 2] with [1, 2]") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is unmodified [1, 2]") + { + EXPECT_UNMODIFIED(merged, val1, val2); + } + } + WHEN("merging [1, 5] with [2, 3]") + { + auto op1 = make_interval(val1, val5, environment, ns); + auto op2 = make_interval(val2, val3, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is unmodified [1, 5]") + { + EXPECT_UNMODIFIED(merged, val1, val5); + } + } + } + + GIVEN("widening merges with TOP or BOTTOM") + { + WHEN("merging [1, 2] with TOP") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto top2 = make_top_interval(); + + auto merged = widening_merge(op1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging [1, 2] with BOTTOM") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto bottom2 = make_bottom_interval(); + + auto merged = widening_merge(op1, bottom2); + + THEN("result is unmodified [1, 2]") + { + EXPECT_UNMODIFIED(merged, val1, val2); + } + } + WHEN("merging TOP with [1, 2]") + { + auto top1 = make_top_interval(); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = widening_merge(top1, op2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with [1, 2]") + { + auto bottom1 = make_bottom_interval(); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = widening_merge(bottom1, op2); + + THEN("result is modified [1, 2]") + { + EXPECT_MODIFIED(merged, val1, val2); + } + } + WHEN("merging TOP with TOP") + { + auto top1 = make_top_interval(); + auto top2 = make_top_interval(); + + auto merged = widening_merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with BOTTOM") + { + auto top1 = make_top_interval(); + auto bottom2 = make_bottom_interval(); + + auto merged = widening_merge(top1, bottom2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with TOP") + { + auto bottom1 = make_bottom_interval(); + auto top2 = make_top_interval(); + + auto merged = widening_merge(bottom1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with BOTTOM") + { + auto bottom1 = make_bottom_interval(); + auto bottom2 = make_bottom_interval(); + + auto merged = widening_merge(bottom1, bottom2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); + } + } + } + + GIVEN("interval merges which do widen") + { + WHEN("merging [1, 3] with [2, 4]") + { + auto op1 = make_interval(val1, val3, environment, ns); + auto op2 = make_interval(val2, val4, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - [1, 8]") + { + EXPECT_MODIFIED(merged, val1, val8); + } + } + WHEN("merging [2, 4] with [1, 3]") + { + auto op1 = make_interval(val2, val4, environment, ns); + auto op2 = make_interval(val1, val3, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - [-3, 4]") + { + EXPECT_MODIFIED(merged, val3minus, val4); + } + } + WHEN("merging [1, 2] with [4, 5]") + { + auto op1 = make_interval(val1, val2, environment, ns); + auto op2 = make_interval(val4, val5, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - [1, 10]") + { + EXPECT_MODIFIED(merged, val1, val10); + } + } + WHEN("merging [4, 5] with [1, 2]") + { + auto op1 = make_interval(val4, val5, environment, ns); + auto op2 = make_interval(val1, val2, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - [-4, 5]") + { + EXPECT_MODIFIED(merged, val4minus, val5); + } + } + WHEN("merging [2, 3] with [1, 5]") + { + auto op1 = make_interval(val2, val3, environment, ns); + auto op2 = make_interval(val1, val5, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is widen both bounds - [-4, 10]") + { + EXPECT_MODIFIED(merged, val4minus, val10); + } + } + WHEN("merging [-3, -1] with [-4, -2]") + { + auto op1 = make_interval(val3minus, val1minus, environment, ns); + auto op2 = make_interval(val4minus, val2minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - [-8, -1]") + { + EXPECT_MODIFIED(merged, val8minus, val1minus); + } + } + WHEN("merging [-4, -2] with [-3, -1]") + { + auto op1 = make_interval(val4minus, val2minus, environment, ns); + auto op2 = make_interval(val3minus, val1minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - [-4, 3]") + { + EXPECT_MODIFIED(merged, val4minus, val3); + } + } + WHEN("merging [-2, -1] with [-5, -4]") + { + auto op1 = make_interval(val2minus, val1minus, environment, ns); + auto op2 = make_interval(val5minus, val4minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - [-10, -1]") + { + EXPECT_MODIFIED(merged, val10minus, val1minus); + } + } + WHEN("merging [-5, -4] with [-2, -1]") + { + auto op1 = make_interval(val5minus, val4minus, environment, ns); + auto op2 = make_interval(val2minus, val1minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - [-5, 4]") + { + EXPECT_MODIFIED(merged, val5minus, val4); + } + } + WHEN("merging [-3, -2] with [-5, -1]") + { + auto op1 = make_interval(val3minus, val2minus, environment, ns); + auto op2 = make_interval(val5minus, val1minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is widen both bounds - [-10, 4]") + { + EXPECT_MODIFIED(merged, val10minus, val4); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp b/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp deleted file mode 100644 index 9a27aba7dc1..00000000000 --- a/unit/analyses/variable-sensitivity/value_set/abstract_value.cpp +++ /dev/null @@ -1,499 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for value set abstract values - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include "value_set_test_common.h" - -#include -#include -#include -#include - -#include - -#include -#include - -#include -#include -#include - -namespace -{ -// NOLINTNEXTLINE(readability/identifiers) -class ContainsAllOf - : public Catch::MatcherBase -{ -private: - std::vector should_contain_values; - -public: - template - explicit ContainsAllOf(Args &&... should_contain_values) - : should_contain_values{std::forward(should_contain_values)...} - { - } - - bool match(const value_set_abstract_valuet::valuest &values) const override - { - for(auto const &value : should_contain_values) - { - if(values.count(value) == 0) - { - return false; - } - } - return true; - } - - std::string describe() const override - { - std::ostringstream oss{}; - auto const ns = namespacet{symbol_tablet{}}; - oss << "contains all of { "; - bool first = true; - for(auto const &value : should_contain_values) - { - if(!first) - { - oss << ", "; - } - first = false; - oss << expr2c(value, ns); - } - oss << " }"; - return oss.str(); - } -}; -} // namespace - -std::unique_ptr domain_factory() -{ - auto configuration = vsd_configt{}; - auto vs_object_factory = - std::make_shared(configuration); - - return util_make_unique( - vs_object_factory, configuration); -} - -TEST_CASE( - "A value set abstract object created from type is top", - VALUE_SET_TEST_TAGS) -{ - value_set_abstract_valuet abstract_value(signedbv_typet{32}); - REQUIRE(abstract_value.is_top()); - REQUIRE(!abstract_value.is_bottom()); -} - -TEST_CASE( - "A value set created from a single value represents that value", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value = from_integer(10, type); - auto const value_set = value_set_abstract_valuet{type, {value}}; - - REQUIRE(!value_set.is_top()); - REQUIRE(!value_set.is_bottom()); - REQUIRE(value_set.get_values().size() == 1); - REQUIRE_THAT(value_set.get_values(), ContainsAllOf{value}); -} - -TEST_CASE( - "A value set created from multiple values represents all of them", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value1 = from_integer(10, type); - auto const value2 = from_integer(36, type); - auto const value3 = from_integer(42, type); - auto const value_set = - value_set_abstract_valuet{type, {value1, value2, value3}}; - - REQUIRE(!value_set.is_top()); - REQUIRE(!value_set.is_bottom()); - REQUIRE(value_set.get_values().size() == 3); - REQUIRE_THAT(value_set.get_values(), ContainsAllOf(value1, value2, value3)); -} - -TEST_CASE( - "A value set created from an empty set is bottom", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value_set = - value_set_abstract_valuet{type, value_set_abstract_valuet::valuest{}}; - REQUIRE(!value_set.is_top()); - REQUIRE(value_set.is_bottom()); -} - -TEST_CASE( - "A value set created with too many elements is TOP", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto values = value_set_abstract_valuet::valuest{}; - for(std::size_t i = 0; i <= value_set_abstract_valuet::max_value_set_size; - ++i) - { - values.insert(from_integer(i, type)); - } - auto const value_set = value_set_abstract_valuet{type, values}; - - REQUIRE(value_set.is_top()); - REQUIRE(!value_set.is_bottom()); -} - -TEST_CASE( - "A value set created by merging two single value-value sets contains both " - "values", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value1 = from_integer(10, type); - auto const value2 = from_integer(42, type); - using valuest = value_set_abstract_valuet::valuest; - auto const value_set1 = - std::make_shared(type, valuest{value1}); - auto const value_set2 = - std::make_shared(type, valuest{value2}); - - bool out_modifications; - auto const merged_abstract_object = - abstract_objectt::merge(value_set1, value_set2, out_modifications); - auto const merged_value_set = - std::dynamic_pointer_cast( - merged_abstract_object); - - REQUIRE(merged_value_set != nullptr); - REQUIRE(!merged_value_set->is_top()); - REQUIRE(!merged_value_set->is_bottom()); - REQUIRE(merged_value_set->get_values().size() == 2); - REQUIRE_THAT(merged_value_set->get_values(), ContainsAllOf(value1, value2)); -} - -TEST_CASE( - "A value set created by merging two multi-value value sets contains all " - "values from both of them", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value1 = from_integer(10, type); - auto const value2 = from_integer(20, type); - auto const value3 = from_integer(30, type); - using valuest = value_set_abstract_valuet::valuest; - auto const value_set1 = - std::make_shared(type, valuest{value1, value2}); - auto const value_set2 = - std::make_shared(type, valuest{value2, value3}); - - bool out_modifications; - auto const merged_abstracted_object = - abstract_objectt::merge(value_set1, value_set2, out_modifications); - auto const merged_value_set = - std::dynamic_pointer_cast( - merged_abstracted_object); - - REQUIRE(merged_value_set != nullptr); - REQUIRE(!merged_value_set->is_top()); - REQUIRE(!merged_value_set->is_bottom()); - REQUIRE(merged_value_set->get_values().size() == 3); - REQUIRE_THAT( - merged_value_set->get_values(), ContainsAllOf(value1, value2, value3)); -} - -TEST_CASE( - "The result of merging two value sets is TOP if both are non-top value sets " - "and the resulting set would have too many elements", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - using valuest = value_set_abstract_valuet::valuest; - auto values = valuest{}; - for(std::size_t i = 0; i < value_set_abstract_valuet::max_value_set_size; ++i) - { - values.insert(from_integer(i, type)); - } - - auto const straw_that_broke_the_camels_back = - from_integer(value_set_abstract_valuet::max_value_set_size, type); - - auto const value_set1 = - std::make_shared(type, values); - REQUIRE(!value_set1->is_top()); - - auto const value_set2 = std::make_shared( - type, valuest{straw_that_broke_the_camels_back}); - REQUIRE(!value_set2->is_top()); - - bool out_modifications; - auto const merged_abstract_object = - abstract_objectt::merge(value_set1, value_set2, out_modifications); - auto const merged_value_set = - std::dynamic_pointer_cast( - merged_abstract_object); - - REQUIRE(merged_value_set != nullptr); - REQUIRE(merged_value_set->is_top()); - REQUIRE(!merged_value_set->is_bottom()); -} - -TEST_CASE( - "The result of merging two value sets is top if one of them is TOP", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value = from_integer(10, type); - using valuest = value_set_abstract_valuet::valuest; - auto const value_set1 = - std::make_shared(type, valuest{value}); - auto const value_set2 = std::make_shared(type); - - bool out_modifications; - auto const merged_abstract_object = - abstract_objectt::merge(value_set1, value_set2, out_modifications); - - REQUIRE(merged_abstract_object->is_top()); - REQUIRE(!merged_abstract_object->is_bottom()); -} - -TEST_CASE( - "Make sure the output method works correctly with a value set with 0 " - "elements", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value_set = - value_set_abstract_valuet{type, value_set_abstract_valuet::valuest{}}; - - const ait ai{domain_factory()}; - - std::stringstream ss; - value_set.output(ss, ai, namespacet{symbol_tablet{}}); - REQUIRE(ss.str() == "BOTTOM"); -} - -TEST_CASE( - "Make sure the output method works correctly with a value set with 1 element", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value = from_integer(10, type); - auto const value_set = value_set_abstract_valuet{type, {value}}; - - const ait ai{domain_factory()}; - - std::stringstream ss; - value_set.output(ss, ai, namespacet{symbol_tablet{}}); - REQUIRE(ss.str() == "{ 10 }"); -} - -TEST_CASE( - "Make sure the output method works correctly with a value set with 3 " - "elements", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value1 = from_integer(10, type); - auto const value2 = from_integer(12, type); - auto const value3 = from_integer(14, type); - auto const value_set = - value_set_abstract_valuet{type, {value1, value2, value3}}; - - const ait ai{domain_factory()}; - - std::stringstream ss; - value_set.output(ss, ai, namespacet{symbol_tablet{}}); - REQUIRE(ss.str() == "{ 10 12 14 }"); -} - -TEST_CASE( - "Make sure that the output method works with a TOP value set", - VALUE_SET_TEST_TAGS) -{ - // Build and ensure value set is TOP - auto const type = signedbv_typet{32}; - auto values = value_set_abstract_valuet::valuest{}; - for(std::size_t i = 0; i <= value_set_abstract_valuet::max_value_set_size; - ++i) - { - values.insert(from_integer(i, type)); - } - auto const value_set = value_set_abstract_valuet{type, values}; - REQUIRE(value_set.is_top()); - - const ait ai{domain_factory()}; - - std::stringstream ss; - value_set.output(ss, ai, namespacet{symbol_tablet{}}); - REQUIRE(ss.str() == "TOP"); -} - -TEST_CASE( - "Value set abstract value that is TOP can not be turned into a constant", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value_set = value_set_abstract_valuet{type}; - - REQUIRE(value_set.to_constant() == nil_exprt{}); -} - -TEST_CASE( - "Value set abstract value that is bottom can not be turned into a constant", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value_set = - value_set_abstract_valuet{type, value_set_abstract_valuet::valuest{}}; - - REQUIRE(value_set.to_constant() == nil_exprt{}); -} - -TEST_CASE( - "Value set with multiple possible values can not be turned into a constant", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto values = value_set_abstract_valuet::valuest{}; - values.insert(from_integer(0, type)); - values.insert(from_integer(1, type)); - auto const value_set = value_set_abstract_valuet{type, values}; - - REQUIRE(value_set.to_constant() == nil_exprt{}); -} - -TEST_CASE( - "Value set with exactly one possible value can be turned into a constant", - VALUE_SET_TEST_TAGS) -{ - auto const type = signedbv_typet{32}; - auto const value = from_integer(0, type); - auto const value_set = - value_set_abstract_valuet{type, value_set_abstract_valuet::valuest{value}}; - - REQUIRE(value_set.to_constant() == value); -} - -static abstract_environmentt get_value_set_abstract_environment() -{ - vsd_configt config; - config.value_abstract_type = VALUE_SET; - config.advanced_sensitivities.new_value_set = true; - config.context_tracking.data_dependency_context = false; - config.context_tracking.last_write_context = false; - auto object_factory = - variable_sensitivity_object_factoryt::configured_with(config); - auto environment = abstract_environmentt{object_factory}; - environment.make_top(); - return environment; -} - -TEST_CASE("Eval on an constant gives us that constant", VALUE_SET_TEST_TAGS) -{ - const auto environment = get_value_set_abstract_environment(); - namespacet ns{symbol_tablet{}}; - const auto zero = from_integer(0, signedbv_typet{32}); - const auto eval_result = environment.eval(zero, ns); - REQUIRE(eval_result != nullptr); - REQUIRE(!eval_result->is_top()); - REQUIRE(!eval_result->is_bottom()); - const auto eval_result_as_value_set = - std::dynamic_pointer_cast( - eval_result->unwrap_context()); - REQUIRE(eval_result_as_value_set != nullptr); - REQUIRE(eval_result_as_value_set->get_values().size() == 1); - REQUIRE_THAT(eval_result_as_value_set->get_values(), ContainsAllOf{zero}); -} - -TEST_CASE( - "Eval on a plus expression with constant operands gives us the result of " - "that plus", - VALUE_SET_TEST_TAGS) -{ - const auto environment = get_value_set_abstract_environment(); - namespacet ns{symbol_tablet{}}; - const auto s32_type = signedbv_typet{32}; - const auto three = from_integer(3, s32_type); - const auto five = from_integer(5, s32_type); - const auto three_plus_five = plus_exprt{three, five}; - - auto eval_result = environment.eval(three_plus_five, ns); - REQUIRE(eval_result != nullptr); - REQUIRE(!eval_result->is_top()); - REQUIRE(!eval_result->is_bottom()); - - const auto eval_result_as_value_set = - std::dynamic_pointer_cast( - eval_result->unwrap_context()); - REQUIRE(eval_result_as_value_set != nullptr); - const auto eight = from_integer(8, s32_type); - REQUIRE(eval_result_as_value_set->get_values().size() == 1); - REQUIRE_THAT(eval_result_as_value_set->get_values(), ContainsAllOf{eight}); -} - -TEST_CASE( - "Eval on a multiply expression on symbols gives us the results of that " - "multiplication", - VALUE_SET_TEST_TAGS) -{ - auto environment = get_value_set_abstract_environment(); - symbol_tablet symbol_table; - - const auto s32_type = signedbv_typet{32}; - - symbolt a_symbol{}; - a_symbol.name = a_symbol.pretty_name = a_symbol.base_name = "a"; - a_symbol.is_lvalue = true; - a_symbol.type = s32_type; - symbol_table.add(a_symbol); - - symbolt b_symbol{}; - b_symbol.name = b_symbol.pretty_name = b_symbol.base_name = "b"; - b_symbol.is_lvalue = true; - b_symbol.type = s32_type; - symbol_table.add(b_symbol); - symbol_table.add(b_symbol); - - const namespacet ns{symbol_table}; - - const auto three = from_integer(3, s32_type); - const auto four = from_integer(4, s32_type); - const auto five = from_integer(5, s32_type); - const auto six = from_integer(6, s32_type); - - const auto three_or_five = std::make_shared( - s32_type, value_set_abstract_valuet::valuest{three, five}); - environment.assign(a_symbol.symbol_expr(), three_or_five, ns); - - const auto four_or_six = std::make_shared( - s32_type, value_set_abstract_valuet::valuest{four, six}); - environment.assign(b_symbol.symbol_expr(), four_or_six, ns); - - const auto a_times_b = - mult_exprt{a_symbol.symbol_expr(), b_symbol.symbol_expr()}; - - const auto eval_result = environment.eval(a_times_b, ns); - REQUIRE(eval_result != nullptr); - REQUIRE(!eval_result->is_top()); - REQUIRE(!eval_result->is_bottom()); - - const auto eval_result_as_value_set = - std::dynamic_pointer_cast( - eval_result->unwrap_context()); - REQUIRE(eval_result_as_value_set != nullptr); - REQUIRE(eval_result_as_value_set->get_values().size() == 4); - - const auto twelve = from_integer(12, s32_type); - const auto eighteen = from_integer(18, s32_type); - const auto twenty = from_integer(20, s32_type); - const auto twentyfour = from_integer(30, s32_type); - REQUIRE_THAT( - eval_result_as_value_set->get_values(), - ContainsAllOf(twelve, eighteen, twenty, twentyfour)); -} diff --git a/unit/analyses/variable-sensitivity/value_set/module_dependencies.txt b/unit/analyses/variable-sensitivity/value_set/module_dependencies.txt deleted file mode 100644 index d44f66043f7..00000000000 --- a/unit/analyses/variable-sensitivity/value_set/module_dependencies.txt +++ /dev/null @@ -1,4 +0,0 @@ -analyses -ansi-c -testing-utils -util diff --git a/unit/analyses/variable-sensitivity/value_set/value_set_test_common.h b/unit/analyses/variable-sensitivity/value_set/value_set_test_common.h deleted file mode 100644 index 55e23d02f39..00000000000 --- a/unit/analyses/variable-sensitivity/value_set/value_set_test_common.h +++ /dev/null @@ -1,18 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for value set pointer abstract objects - -Author: Diffblue Ltd. - -\*******************************************************************/ - -// NOLINTNEXTLINE(whitespace/line_length) -#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_VALUE_SET_TEST_COMMON_H -// NOLINTNEXTLINE(whitespace/line_length) -#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_VALUE_SET_TEST_COMMON_H - -#include -#define VALUE_SET_TEST_TAGS "[core][analyses][variable-sensitivity][value-set]" - -// NOLINTNEXTLINE(whitespace/line_length) -#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_VALUE_SET_TEST_COMMON_H diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp new file mode 100644 index 00000000000..956364b6220 --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp @@ -0,0 +1,291 @@ +/*******************************************************************\ + + Module: Unit tests for value_set_abstract_valuet compacting + + Compacting occurs when the value_set get 'large', and takes two forms + non-destructive (eg, can we merge constants into an existing interval + with no loss of precision) and destructive (creating intervals from + the constants, or merging existing intervals). + + Author: Jez Higgins, jez@jezuk.co.uk + +\*******************************************************************/ + +#include +#include + +#include + +#include +#include +#include + +SCENARIO( + "compacting value sets", + "[core][analysis][variable-sensitivity][value_set_abstract_object][compact]") +{ + const typet type = signedbv_typet(32); + auto val0 = from_integer(0, type); + auto val1 = from_integer(1, type); + auto val2 = from_integer(2, type); + auto val3 = from_integer(3, type); + auto val4 = from_integer(4, type); + auto val5 = from_integer(5, type); + auto val6 = from_integer(6, type); + auto val7 = from_integer(7, type); + auto val8 = from_integer(8, type); + auto val9 = from_integer(9, type); + auto val10 = from_integer(10, type); + auto val11 = from_integer(11, type); + auto val12 = from_integer(12, type); + auto interval_5_10 = constant_interval_exprt(val5, val10); + auto interval_1_10 = constant_interval_exprt(val1, val10); + + auto config = vsd_configt::constant_domain(); + config.context_tracking.data_dependency_context = false; + config.context_tracking.last_write_context = false; + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(config); + auto environment = abstract_environmentt{object_factory}; + environment.make_top(); + auto symbol_table = symbol_tablet{}; + auto ns = namespacet{symbol_table}; + + GIVEN("compact values into existing interval") + { + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [5, 10]") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + interval_5_10}, + environment, + ns); + THEN("{ 1, 2, 3, 4, [5, 10] }") + { + EXPECT(value_set, {val1, val2, val3, val4, interval_5_10}); + } + } + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [1, 10]") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + interval_1_10}, + environment, + ns); + THEN("{ [1, 10] }") + { + EXPECT(value_set, {interval_1_10}); + } + } + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, [5, 10]") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + val11, + val12, + interval_5_10}, + environment, + ns); + THEN("{ 1, 2, 3, 4, 11, 12, [5, 10] }") + { + EXPECT( + value_set, {val1, val2, val3, val4, val11, val12, interval_5_10}); + } + } + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [1, 10], [5, 10]") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + interval_1_10, + interval_5_10}, + environment, + ns); + THEN("{ [1, 10] }") + { + EXPECT(value_set, {interval_1_10}); + } + } + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, [5, 10], [1, 10]") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + val11, + val12, + interval_5_10, + interval_1_10}, + environment, + ns); + THEN("{ 11, 12, [1, 10] }") + { + EXPECT(value_set, {val11, val12, interval_1_10}); + } + } + } + + GIVEN("compact overlapping interval together") + { + auto interval_1_2 = constant_interval_exprt(val1, val2); + auto interval_2_3 = constant_interval_exprt(val2, val3); + auto interval_3_4 = constant_interval_exprt(val3, val4); + auto interval_4_5 = constant_interval_exprt(val4, val5); + auto interval_8_10 = constant_interval_exprt(val8, val10); + auto interval_9_12 = constant_interval_exprt(val9, val12); + auto val13 = from_integer(13, type); + auto val14 = from_integer(14, type); + auto val15 = from_integer(15, type); + + WHEN( + "compacting { 0, [1, 2], [2, 3], [3, 4], [4, 5], 6, 7, [8, 10], [9, 12], " + "13, 14, 15 }") + { + auto value_set = make_value_set( + {val0, + interval_1_2, + interval_2_3, + interval_3_4, + interval_4_5, + val6, + val7, + interval_8_10, + interval_9_12, + val13, + val14, + val15}, + environment, + ns); + THEN("{ 0, [1, 5], 6, 7, [9, 12], 13, 14, 15 }") + { + auto interval_1_5 = constant_interval_exprt(val1, val5); + auto interval_8_12 = constant_interval_exprt(val8, val12); + EXPECT( + value_set, + {val0, interval_1_5, val6, val7, interval_8_12, val13, val14, val15}); + } + } + WHEN( + "compacting { [1, 2], [2, 3], [3, 4], [4, 5], [8, 10], [9, 12], 0, 1, 2, " + "3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 }") + { + auto value_set = make_value_set( + {val0, val1, val2, val3, val4, + val5, val6, val7, val8, val9, + val10, val11, val12, val13, val14, + val15, interval_1_2, interval_2_3, interval_3_4, interval_4_5, + interval_8_10, interval_9_12}, + environment, + ns); + THEN("{ 0, [1, 5], 6, 7, [9, 12], 13, 14, 15 }") + { + auto interval_1_5 = constant_interval_exprt(val1, val5); + auto interval_8_12 = constant_interval_exprt(val8, val12); + EXPECT( + value_set, + {val0, interval_1_5, val6, val7, interval_8_12, val13, val14, val15}); + } + } + } + + GIVEN("compact values into new intervals") + { + WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 }") + { + auto value_set = make_value_set( + {val1, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + val11, + val12}, + environment, + ns); + THEN("{ [1, 4], 5, 6, 7, 8, [9, 12] }") + { + auto interval_1_4 = constant_interval_exprt(val1, val4); + auto interval_9_12 = constant_interval_exprt(val9, val12); + + EXPECT( + value_set, {val5, val6, val7, val8, interval_1_4, interval_9_12}); + } + } + + WHEN( + "compacting { -100, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 100 } - pathalogical " + "case with outliers") + { + auto val100minus = from_integer(-100, type); + auto val100 = from_integer(100, type); + auto value_set = make_value_set( + {val100minus, + val2, + val3, + val4, + val5, + val6, + val7, + val8, + val9, + val10, + val11, + val100}, + environment, + ns); + THEN("{ [-100, 0], [1, 100] }") + { + auto interval_100minus_0 = constant_interval_exprt(val100minus, val0); + auto interval_1_100 = constant_interval_exprt(val1, val100); + EXPECT(value_set, {interval_100minus_0, interval_1_100}); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp index 7f4d2c48752..adef5bb9303 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp @@ -20,9 +20,8 @@ static std::shared_ptr meet(abstract_object_pointert const &op1, abstract_object_pointert const &op2) { - bool modified; - auto result = abstract_objectt::meet(op1, op2, modified); - return as_value_set(result); + auto result = abstract_objectt::meet(op1, op2); + return as_value_set(result.object); } static void diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index 785cd9dee2e..887ab0d505f 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -18,10 +18,9 @@ static merge_result merge(abstract_object_pointert op1, abstract_object_pointert op2) { - bool modified; - auto result = abstract_objectt::merge(op1, op2, modified); + auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - return {modified, as_value_set(result)}; + return {result.modified, as_value_set(result.object)}; } SCENARIO( diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp new file mode 100644 index 00000000000..42b526f2759 --- /dev/null +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp @@ -0,0 +1,386 @@ +/*******************************************************************\ + + Module: Unit tests for value_set_abstract_objectt::merge + + Author: Jez Higgins. + +\*******************************************************************/ + +#include +#include +#include + +#include +#include + +static merge_result +widening_merge(abstract_object_pointert op1, abstract_object_pointert op2) +{ + auto result = abstract_objectt::merge(op1, op2, widen_modet::could_widen); + + return {result.modified, as_value_set(result.object)}; +} + +SCENARIO( + "widening merge value_set_abstract_object", + "[core][analyses][variable-sensitivity][value_set_abstract_object][merge]") +{ + auto type = signedbv_typet(32); + auto val0 = from_integer(0, type); + auto val1 = from_integer(1, type); + auto val2 = from_integer(2, type); + auto val3 = from_integer(3, type); + auto val4 = from_integer(4, type); + auto val5 = from_integer(5, type); + auto val6 = from_integer(6, type); + auto val7 = from_integer(7, type); + auto val8 = from_integer(8, type); + auto val9 = from_integer(9, type); + auto val10 = from_integer(10, type); + auto val11 = from_integer(11, type); + auto val12 = from_integer(12, type); + auto val13 = from_integer(13, type); + auto val1minus = from_integer(-1, type); + auto val2minus = from_integer(-2, type); + auto val3minus = from_integer(-3, type); + auto val4minus = from_integer(-4, type); + auto val5minus = from_integer(-5, type); + auto val8minus = from_integer(-8, type); + auto val10minus = from_integer(-10, 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 merges which don't widen") + { + WHEN("merging {1, 2} with {1, 2}") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is unmodified {1, 2}") + { + EXPECT_UNMODIFIED(merged, {val1, val2}); + } + } + WHEN("merging {1, 5} with {2, 3}") + { + auto op1 = make_value_set({val1, val5}, environment, ns); + auto op2 = make_value_set({val2, val3}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is unmodified {1, 2, 3, 5}") + { + EXPECT_MODIFIED(merged, {val1, val2, val3, val5}); + } + } + WHEN("merging { 1, 4, 7, 10, 13 } with { 2, 3, 5, 6, 8, 9, 11, 12 }") + { + auto op1 = + make_value_set({val1, val4, val7, val10, val13}, environment, ns); + auto op2 = make_value_set( + {val2, val3, val5, val6, val8, val9, val11, val12}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("result is compacted but not widened { [1, 5], 6, 7, 8, [9, 13]") + { + auto interval_1_5 = constant_interval_exprt(val1, val5); + auto interval_9_13 = constant_interval_exprt(val9, val13); + EXPECT_MODIFIED( + merged, {interval_1_5, val6, val7, val8, interval_9_13}); + } + } + } + + GIVEN("widening merges with TOP or BOTTOM") + { + WHEN("merging {1, 2} with TOP") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto top2 = make_top_value_set(); + + auto merged = widening_merge(op1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging {1, 2} with BOTTOM") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto bottom2 = make_bottom_value_set(); + + auto merged = widening_merge(op1, bottom2); + + THEN("result is unmodified {1, 2}") + { + EXPECT_UNMODIFIED(merged, {val1, val2}); + } + } + WHEN("merging TOP with {1, 2}") + { + auto top1 = make_top_value_set(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = widening_merge(top1, op2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with {1, 2}") + { + auto bottom1 = make_bottom_value_set(); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = widening_merge(bottom1, op2); + + THEN("result is modified {1, 2}") + { + EXPECT_MODIFIED(merged, {val1, val2}); + } + } + WHEN("merging TOP with TOP") + { + auto top1 = make_top_value_set(); + auto top2 = make_top_value_set(); + + auto merged = widening_merge(top1, top2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging TOP with BOTTOM") + { + auto top1 = make_top_value_set(); + auto bottom2 = make_bottom_value_set(); + + auto merged = widening_merge(top1, bottom2); + + THEN("result is unmodified TOP") + { + EXPECT_UNMODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with TOP") + { + auto bottom1 = make_bottom_value_set(); + auto top2 = make_top_value_set(); + + auto merged = widening_merge(bottom1, top2); + + THEN("result is modified TOP") + { + EXPECT_MODIFIED_TOP(merged); + } + } + WHEN("merging BOTTOM with BOTTOM") + { + auto bottom1 = make_bottom_value_set(); + auto bottom2 = make_bottom_value_set(); + + auto merged = widening_merge(bottom1, bottom2); + + THEN("result is unmodified BOTTOM") + { + EXPECT_UNMODIFIED_BOTTOM(merged); + } + } + } + + GIVEN("value_set merges which do widen") + { + WHEN("merging {1, 3} with {2, 4}") + { + auto op1 = make_value_set({val1, val3}, environment, ns); + auto op2 = make_value_set({val2, val4}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - {1, 2, 3, [4, 8]}") + { + auto interval_4_8 = constant_interval_exprt(val4, val8); + EXPECT_MODIFIED(merged, {val1, val2, val3, interval_4_8}); + } + } + WHEN("merging {2, 4} with {1, 3}") + { + auto op1 = make_value_set({val2, val4}, environment, ns); + auto op2 = make_value_set({val1, val3}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-3, 1], 2, 3, 4}") + { + auto interval_3minus_1 = + constant_interval_exprt(from_integer(-3, type), val1); + EXPECT_MODIFIED(merged, {val2, val3, val4, interval_3minus_1}); + } + } + WHEN("merging {1, 2} with {4, 5}") + { + auto op1 = make_value_set({val1, val2}, environment, ns); + auto op2 = make_value_set({val4, val5}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper bound - {1, 2, 4, [5, 10]") + { + auto interval_5_10 = constant_interval_exprt(val5, val10); + EXPECT_MODIFIED(merged, {val1, val2, val4, interval_5_10}); + } + } + WHEN("merging {4, 5} with {1, 2}") + { + auto op1 = make_value_set({val4, val5}, environment, ns); + auto op2 = make_value_set({val1, val2}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-4, 1], 2, 4, 5}") + { + auto interval_4minus_1 = + constant_interval_exprt(from_integer(-4, type), val1); + EXPECT_MODIFIED(merged, {interval_4minus_1, val2, val4, val4}); + } + } + WHEN("merging {[1, 3]} with {2, 4}") + { + auto interval_1_3 = constant_interval_exprt(val1, val3); + auto op1 = make_value_set(interval_1_3, environment, ns); + auto op2 = make_value_set({val2, val4}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper-bound, {[1, 3], 2 [4, 8]}") + { + auto interval_4_8 = constant_interval_exprt(val4, val8); + EXPECT_MODIFIED(merged, {interval_1_3, val2, interval_4_8}); + } + } + WHEN("merging {[1, 3]} with {[2, 4]}") + { + auto interval_1_3 = constant_interval_exprt(val1, val3); + auto interval_2_4 = constant_interval_exprt(val2, val4); + auto op1 = make_value_set(interval_1_3, environment, ns); + auto op2 = make_value_set(interval_2_4, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen upper-bound, {[1, 3], [2, 8]}") + { + auto interval_2_8 = constant_interval_exprt(val2, val8); + EXPECT_MODIFIED(merged, {interval_1_3, interval_2_8}); + } + } + WHEN("merging {[2, 4]} with {1, 3}") + { + auto interval_2_4 = constant_interval_exprt(val2, val4); + auto op1 = make_value_set(interval_2_4, environment, ns); + auto op2 = make_value_set({val1, val3}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-3, 1], 3, [2, 4]}") + { + auto interval_3minus_1 = + constant_interval_exprt(from_integer(-3, type), val1); + EXPECT_MODIFIED(merged, {interval_2_4, val3, interval_3minus_1}); + } + } + WHEN("merging {[2, 4]} with {[1, 3]}") + { + auto interval_2_4 = constant_interval_exprt(val2, val4); + auto interval_1_3 = constant_interval_exprt(val1, val3); + auto op1 = make_value_set(interval_2_4, environment, ns); + auto op2 = make_value_set(interval_1_3, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-3, 3], [2, 4]}") + { + auto interval_3minus_3 = + constant_interval_exprt(from_integer(-3, type), val3); + EXPECT_MODIFIED(merged, {interval_3minus_3, interval_2_4}); + } + } + WHEN("merging {-3, -1} with {-4, -2}") + { + auto op1 = make_value_set({val3minus, val1minus}, environment, ns); + auto op2 = make_value_set({val4minus, val2minus}, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-8, -4], -3, -2, -1}") + { + EXPECT_MODIFIED( + merged, + {constant_interval_exprt(val8minus, val4minus), + val3minus, + val2minus, + val1minus}); + } + } + WHEN("merging {[-3, -1]} with {[-4, -2]}") + { + auto interval31minus = constant_interval_exprt(val3minus, val1minus); + auto interval42minus = constant_interval_exprt(val4minus, val2minus); + auto op1 = make_value_set(interval31minus, environment, ns); + auto op2 = make_value_set(interval42minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-8, -2], [-3, -1]}") + { + EXPECT_MODIFIED( + merged, + {constant_interval_exprt(val8minus, val2minus), interval31minus}); + } + } + WHEN("merging {-3, -1} with {[-4, -2]}") + { + auto interval42minus = constant_interval_exprt(val4minus, val2minus); + auto op1 = make_value_set({val3minus, val1minus}, environment, ns); + auto op2 = make_value_set(interval42minus, environment, ns); + + auto merged = widening_merge(op1, op2); + + THEN("widen lower bound - {[-8, -2], -1}") + { + EXPECT_MODIFIED( + merged, {constant_interval_exprt(val8minus, val2minus), val1minus}); + } + } + WHEN("merging {[-3, -1]} with {-4, -2}") + { + auto interval31minus = constant_interval_exprt(val3minus, val1minus); + auto op1 = make_value_set(interval31minus, environment, ns); + auto op2 = make_value_set({val4minus, val2minus}, environment, ns); + + auto merged = widening_merge(op1, op2); + THEN("widen lower bound - {[-8, -4], [-3, -1], -2}") + { + EXPECT_MODIFIED( + merged, + {constant_interval_exprt(val8minus, val4minus), + interval31minus, + val2minus}); + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index f99a7db4306..ca66f243b9f 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -76,14 +76,14 @@ std::shared_ptr make_bottom_interval() signedbv_typet(32), false, true); } -std::shared_ptr +std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns) { auto vals = std::vector{val}; return make_value_set(vals, env, ns); } -std::shared_ptr make_value_set( +std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, namespacet &ns) @@ -97,20 +97,20 @@ std::shared_ptr make_value_set( else initial_values.insert(make_constant(v, env, ns)); } - auto vs = std::make_shared(vals[0], env, ns); - vs->set_values(initial_values); - return vs; + + auto vs = value_set_abstract_objectt::make_value_set(initial_values); + return std::dynamic_pointer_cast(vs); } -std::shared_ptr make_bottom_value_set() +std::shared_ptr make_bottom_value_set() { - return std::make_shared( + return std::make_shared( integer_typet(), false, true); } -std::shared_ptr make_top_value_set() +std::shared_ptr make_top_value_set() { - return std::make_shared(integer_typet()); + return std::make_shared(integer_typet()); } abstract_object_pointert make_bottom_object() @@ -409,6 +409,11 @@ void EXPECT_TOP(std::shared_ptr result) REQUIRE_FALSE(result->is_bottom()); } +void EXPECT_TOP(abstract_objectt::combine_result const &result) +{ + EXPECT_TOP(result.object); +} + void EXPECT_TOP(std::shared_ptr &result) { REQUIRE(result); @@ -430,6 +435,11 @@ void EXPECT_BOTTOM(std::shared_ptr result) REQUIRE(result->is_bottom()); } +void EXPECT_BOTTOM(abstract_objectt::combine_result const &result) +{ + EXPECT_BOTTOM(result.object); +} + std::shared_ptr add( const abstract_object_pointert &op1, const abstract_object_pointert &op2, diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index 4b9ed63233a..f3fdf50acac 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -41,16 +41,16 @@ std::shared_ptr make_interval( std::shared_ptr make_top_interval(); std::shared_ptr make_bottom_interval(); -std::shared_ptr +std::shared_ptr make_value_set(exprt val, abstract_environmentt &env, namespacet &ns); -std::shared_ptr make_value_set( +std::shared_ptr make_value_set( const std::vector &vals, abstract_environmentt &env, namespacet &ns); -std::shared_ptr make_bottom_value_set(); -std::shared_ptr make_top_value_set(); +std::shared_ptr make_bottom_value_set(); +std::shared_ptr make_top_value_set(); abstract_object_pointert make_bottom_object(); abstract_object_pointert make_top_object(); @@ -85,10 +85,14 @@ void EXPECT( void EXPECT_TOP(std::shared_ptr result); +void EXPECT_TOP(abstract_objectt::combine_result const &result); + void EXPECT_TOP(std::shared_ptr &result); void EXPECT_BOTTOM(std::shared_ptr result); +void EXPECT_BOTTOM(abstract_objectt::combine_result const &result); + template struct merge_result { @@ -171,6 +175,13 @@ void EXPECT_UNMODIFIED( merge_result &result, const std::vector &expected_values); +template +void EXPECT_UNMODIFIED(abstract_objectt::combine_result const &result) +{ + auto object = std::dynamic_pointer_cast(result.object); + EXPECT_UNMODIFIED(object, result.modified); +} + void EXPECT_MODIFIED( std::shared_ptr &result, bool modified, @@ -200,6 +211,13 @@ void EXPECT_MODIFIED( merge_result &result, const std::vector &expected_values); +template +void EXPECT_MODIFIED(abstract_objectt::combine_result const &result) +{ + auto object = std::dynamic_pointer_cast(result.object); + EXPECT_MODIFIED(object, result.modified); +} + std::shared_ptr add( const abstract_object_pointert &op1, const abstract_object_pointert &op2,