diff --git a/src/goto-symex/simplify_expr_with_value_set.cpp b/src/goto-symex/simplify_expr_with_value_set.cpp index 24a519f6364..5a01367b569 100644 --- a/src/goto-symex/simplify_expr_with_value_set.cpp +++ b/src/goto-symex/simplify_expr_with_value_set.cpp @@ -19,6 +19,10 @@ Author: Michael Tautschnig #include "goto_symex_can_forward_propagate.h" +#include +#include +#include + /// Try to evaluate a simple pointer comparison. /// \param operation: ID_equal or ID_not_equal /// \param symbol_expr: The symbol expression in the condition @@ -155,6 +159,62 @@ simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality( return unchanged(expr); } +/// Compute the object number (in \ref value_sett::object_numbering) of the +/// root object of the object numbered \p object_number, or return an empty +/// std::optional when the object is "unknown," "invalid," or a failed symbol. +/// Results are cached: the numbering is global, append-only, and maps numbers +/// to immutable expressions, so a result computed once remains valid for the +/// lifetime of the program. This matters as value sets are repeatedly +/// re-inspected element by element in +/// \ref simplify_expr_with_value_sett::simplify_inequality_pointer_object, +/// which makes the per-element cost of testing for failed symbols and of +/// numbering root objects a dominant cost of symbolic execution when value +/// sets grow large. +static std::optional +root_object_number(object_numberingt::number_type object_number) +{ + enum class statet : std::uint8_t + { + NOT_COMPUTED, + EXCLUDED, + VALID + }; + struct cache_entryt + { + statet state = statet::NOT_COMPUTED; + object_numberingt::number_type root_object_number = 0; + }; + static std::vector cache; + + if(cache.size() <= object_number) + cache.resize(object_number + 1); + + cache_entryt &entry = cache[object_number]; + if(entry.state == statet::NOT_COMPUTED) + { + const exprt &object = value_sett::object_numbering[object_number]; + const exprt &root_object = object_descriptor_exprt::root_object(object); + + if( + object.id() == ID_unknown || object.id() == ID_invalid || + is_failed_symbol(root_object)) + { + entry.state = statet::EXCLUDED; + } + else + { + entry.state = statet::VALID; + entry.root_object_number = + value_sett::object_numbering.number(root_object); + } + } + + if(entry.state == statet::EXCLUDED) + return {}; + else + return entry.root_object_number; +} + simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality_pointer_object( const binary_relation_exprt &expr) @@ -162,45 +222,59 @@ simplify_expr_with_value_sett::simplify_inequality_pointer_object( PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal); PRECONDITION(expr.is_boolean()); + // Collect the objects that `pointer` may point to, as a set of object + // numbers in value_sett::object_numbering. Working with object numbers + // rather than materialized expressions avoids both the cost of building an + // object_descriptor_exprt per value-set element and the cost of comparing + // deep expression trees when populating the set: the numbering is + // hash-consed, so each distinct expression is numbered once and set + // operations are operations over integers. An empty set means "no + // information". auto collect_objects = [this](const exprt &pointer) { - std::set objects; + std::set objects; if(auto address_of = expr_try_dynamic_cast(pointer)) { - objects.insert( - object_descriptor_exprt::root_object(address_of->object())); + objects.insert(value_sett::object_numbering.number( + object_descriptor_exprt::root_object(address_of->object()))); } else if(auto ssa_expr = expr_try_dynamic_cast(pointer)) { ssa_exprt l1_expr{*ssa_expr}; l1_expr.remove_level_2(); - const std::vector value_set_elements = - value_set.get_value_set(l1_expr, ns); + const value_sett::object_mapt value_set_elements = + value_set.get_value_set(l1_expr, ns, false); - for(const auto &value_set_element : value_set_elements) + for(const auto &object_number_and_offset : value_set_elements.read()) { - if( - value_set_element.id() == ID_unknown || - value_set_element.id() == ID_invalid || - is_failed_symbol( - to_object_descriptor_expr(value_set_element).root_object())) + auto object_number = root_object_number(object_number_and_offset.first); + + if(!object_number.has_value()) { objects.clear(); break; } - objects.insert( - to_object_descriptor_expr(value_set_element).root_object()); + objects.insert(*object_number); } } return objects; }; - auto lhs_objects = + const auto lhs_objects = collect_objects(to_pointer_object_expr(expr.lhs()).pointer()); - auto rhs_objects = + + // an empty set of objects on either side means we cannot simplify, so don't + // bother collecting the objects of the other side + if(lhs_objects.empty()) + return simplify_exprt::simplify_inequality_pointer_object(expr); + + const auto rhs_objects = collect_objects(to_pointer_object_expr(expr.rhs()).pointer()); + if(rhs_objects.empty()) + return simplify_exprt::simplify_inequality_pointer_object(expr); + if(lhs_objects.size() == 1 && lhs_objects == rhs_objects) { // there is exactly one pointed-to object on both left-hand and right-hand @@ -209,14 +283,23 @@ simplify_expr_with_value_sett::simplify_inequality_pointer_object( : changed(static_cast(false_exprt{})); } - std::list intersection; - std::set_intersection( - lhs_objects.begin(), - lhs_objects.end(), - rhs_objects.begin(), - rhs_objects.end(), - std::back_inserter(intersection)); - if(!lhs_objects.empty() && !rhs_objects.empty() && intersection.empty()) + auto lhs_it = lhs_objects.begin(); + auto rhs_it = rhs_objects.begin(); + bool intersection_empty = true; + while(lhs_it != lhs_objects.end() && rhs_it != rhs_objects.end()) + { + if(*lhs_it < *rhs_it) + ++lhs_it; + else if(*rhs_it < *lhs_it) + ++rhs_it; + else + { + intersection_empty = false; + break; + } + } + + if(intersection_empty) { // all pointed-to objects on the left-hand side are different from any of // the pointed-to objects on the right-hand side diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 73119a8ffb6..b2d6cd7a33e 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -237,6 +237,19 @@ class value_sett /// are object_descriptor_exprt or have id ID_invalid or ID_unknown. std::vector get_value_set(exprt expr, const namespacet &ns) const; + /// Gets values pointed to by `expr`, including following dereference + /// operators (i.e. this is not a simple lookup in `valuest`). Unlike the + /// single-argument overload above, the result is returned as a map over + /// object numbers (in \ref object_numbering), avoiding materializing an + /// `object_descriptor_exprt` per element. + /// \param expr: query expression + /// \param ns: global namespace + /// \param is_simplified: if false, simplify `expr` before reading. + /// \return the set of object numbers pointed to, together with per-object + /// offsets + object_mapt + get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const; + void clear() { values.clear(); @@ -419,15 +432,6 @@ class value_sett void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns); protected: - /// Reads the set of objects pointed to by `expr`, including making - /// recursive lookups for dereference operations etc. - /// \param expr: query expression - /// \param ns: global namespace - /// \param is_simplified: if false, simplify `expr` before reading. - /// \return the set of object numbers pointed to - object_mapt - get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const; - /// See the other overload of `get_reference_set`. This one returns object /// numbers and offsets instead of expressions. void get_reference_set(