diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 8218efdf428..ea002102d36 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -70,16 +70,19 @@ void value_sett::update_entry( auto existing_entry = values.find(index); if(existing_entry.has_value()) { - entryt replacement = *existing_entry; if(add_to_sets) { - if(make_union(replacement.object_map, new_values)) - values.replace(index, std::move(replacement)); + if(make_union_would_change(existing_entry->get().object_map, new_values)) + { + values.update(index, [&new_values, this](entryt &entry) { + make_union(entry.object_map, new_values); + }); + } } else { - replacement.object_map = new_values; - values.replace(index, std::move(replacement)); + values.update( + index, [&new_values](entryt &entry) { entry.object_map = new_values; }); } } else @@ -90,8 +93,8 @@ void value_sett::update_entry( } } -bool value_sett::insert( - object_mapt &dest, +value_sett::insert_actiont value_sett::get_insert_action( + const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const { @@ -100,108 +103,113 @@ bool value_sett::insert( if(entry==dest.read().end()) { // new - dest.write()[n] = offset; - return true; + return insert_actiont::INSERT; } else if(!entry->second) - return false; // no change + return insert_actiont::NONE; else if(offset && *entry->second == *offset) - return false; // no change + return insert_actiont::NONE; else - { - dest.write()[n].reset(); - return true; - } + return insert_actiont::RESET_OFFSET; } -void value_sett::output( - const namespacet &ns, - std::ostream &out) const +bool value_sett::insert( + object_mapt &dest, + object_numberingt::number_type n, + const offsett &offset) const { - valuest::viewt view; - values.get_view(view); + auto insert_action = get_insert_action(dest, n, offset); + if(insert_action == insert_actiont::NONE) + return false; - for(const auto &values_entry : view) - { - irep_idt identifier, display_name; + auto &new_offset = dest.write()[n]; + if(insert_action == insert_actiont::INSERT) + new_offset = offset; + else + new_offset.reset(); - const entryt &e = values_entry.second; + return true; +} + +void value_sett::output(const namespacet &ns, std::ostream &out) const +{ + values.iterate([&](const irep_idt &, const entryt &e) { + irep_idt identifier, display_name; if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) { - display_name=id2string(e.identifier)+e.suffix; - identifier=""; + display_name = id2string(e.identifier) + e.suffix; + identifier = ""; } - else if(e.identifier=="value_set::return_value") + else if(e.identifier == "value_set::return_value") { - display_name="RETURN_VALUE"+e.suffix; - identifier=""; + display_name = "RETURN_VALUE" + e.suffix; + identifier = ""; } else { - #if 0 - const symbolt &symbol=ns.lookup(e.identifier); - display_name=id2string(symbol.display_name())+e.suffix; - identifier=symbol.name; - #else - identifier=id2string(e.identifier); - display_name=id2string(identifier)+e.suffix; - #endif +#if 0 + const symbolt &symbol=ns.lookup(e.identifier); + display_name=id2string(symbol.display_name())+e.suffix; + identifier=symbol.name; +#else + identifier = id2string(e.identifier); + display_name = id2string(identifier) + e.suffix; +#endif } out << display_name; out << " = { "; - const object_map_dt &object_map=e.object_map.read(); + const object_map_dt &object_map = e.object_map.read(); - std::size_t width=0; + std::size_t width = 0; - for(object_map_dt::const_iterator - o_it=object_map.begin(); - o_it!=object_map.end(); + for(object_map_dt::const_iterator o_it = object_map.begin(); + o_it != object_map.end(); o_it++) { - const exprt &o=object_numbering[o_it->first]; + const exprt &o = object_numbering[o_it->first]; std::string result; - if(o.id()==ID_invalid || o.id()==ID_unknown) - result=from_expr(ns, identifier, o); + if(o.id() == ID_invalid || o.id() == ID_unknown) + result = from_expr(ns, identifier, o); else { - result="<"+from_expr(ns, identifier, o)+", "; + result = "<" + from_expr(ns, identifier, o) + ", "; if(o_it->second) result += integer2string(*o_it->second) + ""; else - result+='*'; + result += '*'; if(o.type().is_nil()) - result+=", ?"; + result += ", ?"; else - result+=", "+from_type(ns, identifier, o.type()); + result += ", " + from_type(ns, identifier, o.type()); - result+='>'; + result += '>'; } out << result; - width+=result.size(); + width += result.size(); object_map_dt::const_iterator next(o_it); next++; - if(next!=object_map.end()) + if(next != object_map.end()) { out << ", "; - if(width>=40) + if(width >= 40) out << "\n "; } } out << " } \n"; - } + }); } exprt value_sett::to_expr(const object_map_dt::value_type &it) const @@ -236,10 +244,12 @@ bool value_sett::make_union(const value_sett::valuest &new_values) { if(delta_entry.in_both) { - entryt merged_entry = *values.find(delta_entry.k); - if(make_union(merged_entry.object_map, delta_entry.m.object_map)) + if(make_union_would_change( + delta_entry.other_m.object_map, delta_entry.m.object_map)) { - values.replace(delta_entry.k, std::move(merged_entry)); + values.update(delta_entry.k, [&](entryt &existing_entry) { + make_union(existing_entry.object_map, delta_entry.m.object_map); + }); result = true; } } @@ -253,6 +263,24 @@ bool value_sett::make_union(const value_sett::valuest &new_values) return result; } +bool value_sett::make_union_would_change( + const object_mapt &dest, + const object_mapt &src) const +{ + for(const auto &number_and_offset : src.read()) + { + if( + get_insert_action( + dest, number_and_offset.first, number_and_offset.second) != + insert_actiont::NONE) + { + return true; + } + } + + return false; +} + bool value_sett::make_union(object_mapt &dest, const object_mapt &src) const { bool result=false; diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index d5537d0502f..fb11101050f 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -232,6 +232,24 @@ class value_sett object_numberingt::number_type n, const offsett &offset) const; + enum class insert_actiont + { + INSERT, + RESET_OFFSET, + NONE + }; + + /// Determines what would happen if object number \p n was inserted into map + /// \p dest with offset \p offset -- the possibilities being, nothing (the + /// entry is already present), a new entry would be inserted (no existing + /// entry with number \p n was found), or an existing entry's offset would be + /// reset (indicating there is already an entry with number \p n, but with + /// differing offset). + insert_actiont get_insert_action( + const object_mapt &dest, + object_numberingt::number_type n, + const offsett &offset) const; + /// Adds an expression and offset to an object map. If the /// destination map has an existing element for the same expression /// with a differing offset its offset is marked unknown. @@ -360,6 +378,13 @@ class value_sett /// \return true if anything changed. bool make_union(object_mapt &dest, const object_mapt &src) const; + /// Determines whether merging two RHS expression sets would cause any change + /// \param dest: set that would be merged into + /// \param src: set that would be merged in + /// \return true if anything changed. + bool make_union_would_change(const object_mapt &dest, const object_mapt &src) + const; + /// Merges an entire existing value_sett's data into this one /// \param new_values: new values to merge in /// \return true if anything changed. diff --git a/src/util/invariant.cpp b/src/util/invariant.cpp index 1f1ff7f07ac..8d457de4c13 100644 --- a/src/util/invariant.cpp +++ b/src/util/invariant.cpp @@ -16,6 +16,8 @@ Author: Martin Brain, martin.brain@diffblue.com #include +bool cbmc_invariants_should_throw = false; + // Backtraces compiler and C library specific // So we should include something explicitly from the C library // to check if the C library is glibc. @@ -26,7 +28,6 @@ Author: Martin Brain, martin.brain@diffblue.com #include #include - /// Attempts to demangle the function name assuming the glibc /// format of stack entry: /// diff --git a/src/util/invariant.h b/src/util/invariant.h index ce63707a639..8463054ca71 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -64,6 +64,28 @@ Author: Martin Brain, martin.brain@diffblue.com ** CPROVER_INVARIANT_* macros. */ +/// Set this to true to cause invariants to throw a C++ exception rather than +/// abort the program. This is currently untested behaviour, and may fail to +/// clean up partly-completed CBMC operations or release resources. You should +/// probably only use this to gather or report more information about the +/// failure and then abort. Default off. +extern bool cbmc_invariants_should_throw; + +/// Helper to enable invariant throwing as above bounded to an object lifetime: +struct cbmc_invariants_should_throwt +{ + bool old_state; + cbmc_invariants_should_throwt() : old_state(cbmc_invariants_should_throw) + { + cbmc_invariants_should_throw = true; + } + + ~cbmc_invariants_should_throwt() + { + cbmc_invariants_should_throw = old_state; + } +}; + /// A logic error, augmented with a distinguished field to hold a backtrace. /// Classes that extend this one should share the same initial constructor /// parameters: their constructor signature should be of the form: @@ -230,10 +252,14 @@ CBMC_NORETURN backtrace, condition, std::forward(params)...); - // We now have a structured exception ready to use; - // in future this is the place to put a 'throw'. - report_exception_to_stderr(to_throw); - abort(); + + if(cbmc_invariants_should_throw) + throw to_throw; + else + { + report_exception_to_stderr(to_throw); + abort(); + } } /// This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'. diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h index 0d9e307a6af..748b1658e67 100644 --- a/src/util/sharing_map.h +++ b/src/util/sharing_map.h @@ -138,22 +138,25 @@ Author: Daniel Poetzl /// to one of the maps, nodes are copied and sharing is lessened as described in /// the following. /// -/// The replace(), insert(), and erase() operations interact with sharing as -/// follows: +/// The replace(), insert(), update() and erase() operations interact with +/// sharing as follows: /// - When a key-value pair is inserted into the map (or a value of an existing -/// pair is replaced) and its position is in a shared subtree, already existing -/// nodes from the root of the subtree to the position of the key-value pair are -/// copied and integrated with the map, and new nodes are created as needed. +/// pair is replaced or updated) and its position is in a shared subtree, +/// already existing nodes from the root of the subtree to the position of the +/// key-value pair are copied and integrated with the map, and new nodes are +/// created as needed. /// - When a key-value pair is erased from the map that is in a shared subtree, /// nodes from the root of the subtree to the last node that will still exist on /// the path to the erased element after the element has been removed are /// copied and integrated with the map, and the remaining nodes are removed. /// -/// The replace() operation is the only method where sharing could unnecessarily -/// be broken. This would happen when replacing an old value with a new equal -/// value. The sharing map provides a debug mode to detect such cases. When the -/// template parameter `fail_if_equal` is set to true, then the replace() method -/// yields an invariant violation when the new value is equal to the old value. +/// The replace() and update() operations are the only method where sharing +/// could unnecessarily be broken. This would happen when replacing an old +/// value with a new equal value, or calling update but making no change. The +/// sharing map provides a debug mode to detect such cases. When the template +/// parameter `fail_if_equal` is set to true, then the replace() and update() +/// methods yield an invariant violation when the new value is equal to the old +/// value. /// For this to work, the type of the values stored in the map needs to have a /// defined equality operator (operator==). /// @@ -198,17 +201,48 @@ class sharing_mapt typedef typename innert::to_mapt to_mapt; typedef typename innert::leaf_listt leaf_listt; - struct truet + struct falset { bool operator()(const mapped_type &lhs, const mapped_type &rhs) { - return true; + return false; } }; typedef - typename std::conditional, truet>::type - value_equalt; + typename std::conditional, falset>:: + type value_equalt; + + struct noop_value_comparatort + { + explicit noop_value_comparatort(const mapped_type &) + { + } + + bool operator()(const mapped_type &) + { + return false; + } + }; + + struct real_value_comparatort + { + mapped_type old_value; + explicit real_value_comparatort(const mapped_type &old_value) + : old_value(old_value) + { + } + + bool operator()(const mapped_type &new_value) + { + return old_value == new_value; + } + }; + + typedef typename std::conditional< + fail_if_equal, + real_value_comparatort, + noop_value_comparatort>::type value_comparatort; public: // interface @@ -222,6 +256,19 @@ class sharing_mapt /// \param k: The key of the element to erase void erase(const key_type &k); + /// Erase element if it exists + /// + /// Complexity: + /// - Worst case: O(H * S + M) + /// - Best case: O(H) + /// + /// \param k: The key of the element to erase + void erase_if_exists(const key_type &k) + { + if(has_key(k)) + erase(k); + } + /// Insert element, element must not exist in map /// /// Complexity: @@ -243,6 +290,20 @@ class sharing_mapt /// \param m: The mapped value to replace the old value with template void replace(const key_type &k, valueU &&m); + + /// Update an element in place; element must exist in map + /// + /// Rationale: this avoids copy-out / edit / replace sequences without leaking + /// a non-const reference + /// + /// Complexity: as \ref sharing_mapt::replace + /// + /// \param k: The key of the element to update + /// \param mutator: function to apply to the existing value. Must not store + /// the reference; should make some change to the stored value (if you are + /// unsure if you need to make a change, use \ref find beforehand) + void update(const key_type &k, std::function mutator); + /// Find element /// /// Complexity: @@ -383,6 +444,18 @@ class sharing_mapt delta_viewt &delta_view, const bool only_common = true) const; + /// Call a function for every key-value pair in the map. + /// + /// Complexity: as \ref sharing_mapt::get_view + void + iterate(std::function f) const + { + if(empty()) + return; + + iterate(map, 0, f); + } + #if !defined(_MSC_VER) /// Stats about sharing between several sharing map instances. An instance of /// this class is returned by the get_sharing_map_stats_* functions. @@ -909,12 +982,31 @@ ::replace(const key_type &k, valueU &&m) PRECONDITION(lp != nullptr); // key must exist in map INVARIANT( - value_equalt()(as_const(lp)->get_value(), m), + !value_equalt()(as_const(lp)->get_value(), m), "values should not be replaced with equal values to maximize sharing"); lp->set_value(std::forward(m)); } +SHARING_MAPT(void) +::update(const key_type &k, std::function mutator) +{ + innert *cp = get_container_node(k); + SM_ASSERT(cp != nullptr); + + leaft *lp = cp->find_leaf(k); + PRECONDITION(lp != nullptr); // key must exist in map + + value_comparatort comparator(as_const(lp)->get_value()); + + lp->mutate_value(mutator); + + INVARIANT( + !comparator(as_const(lp)->get_value()), + "sharing_mapt::update should make some change. Consider using read-only " + "method to check if an update is needed beforehand"); +} + SHARING_MAPT2(optionalt>)::find( const key_type &k) const { diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index 2a0fdebd107..1e4d838818b 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -511,6 +511,16 @@ SN_TYPE_PAR_DEF class sharing_node_leaft : public sharing_node_baset SN_ASSERT(data.use_count() == 1); } + void mutate_value(std::function mutator) + { + SN_ASSERT(data); + + if(data.use_count() > 1) + data = make_small_shared_ptr(data->k, data->v); + + mutator(data->v); + } + protected: datat data; }; diff --git a/unit/util/sharing_map.cpp b/unit/util/sharing_map.cpp index b44a2e9b03d..f89f9b3133e 100644 --- a/unit/util/sharing_map.cpp +++ b/unit/util/sharing_map.cpp @@ -19,6 +19,9 @@ Author: Daniel Poetzl typedef sharing_mapt sharing_map_standardt; +typedef sharing_mapt + sharing_map_debugt; + class sharing_map_internalt : public sharing_map_standardt { friend void sharing_map_internals_test(); @@ -28,14 +31,16 @@ typedef sharing_mapt sharing_map_error_checkt; // helpers -void fill(sharing_map_standardt &sm) +template +void fill(some_sharing_mapt &sm) { sm.insert("i", "0"); sm.insert("j", "1"); sm.insert("k", "2"); } -void fill2(sharing_map_standardt &sm) +template +void fill2(some_sharing_mapt &sm) { sm.insert("l", "3"); sm.insert("m", "4"); @@ -156,7 +161,7 @@ TEST_CASE("Sharing map interface", "[core][util]") REQUIRE(!sm.has_key("k")); } - SECTION("Replace elements") + SECTION("Replace and update elements") { sharing_map_standardt sm; fill(sm); @@ -165,6 +170,23 @@ TEST_CASE("Sharing map interface", "[core][util]") auto r = sm.find("i"); REQUIRE(r); REQUIRE(r->get() == "9"); + + sm.update("i", [](std::string &str) { str += "0"; }); + auto r2 = sm.find("i"); + REQUIRE(r2); + REQUIRE(r2->get() == "90"); + + { + cbmc_invariants_should_throwt invariants_throw; + sharing_map_debugt debug_sm; + fill(debug_sm); + REQUIRE_NOTHROW( + debug_sm.update("i", [](std::string &str) { str += "1"; })); + REQUIRE_THROWS(debug_sm.update("i", [](std::string &str) {})); + + REQUIRE_NOTHROW(debug_sm.replace("i", "abc")); + REQUIRE_THROWS(debug_sm.replace("i", "abc")); + } } SECTION("Retrieve elements") @@ -201,6 +223,12 @@ TEST_CASE("Sharing map interface", "[core][util]") sm.erase("j"); REQUIRE(!sm.has_key("j")); + sm.erase_if_exists("j"); + REQUIRE(!sm.has_key("j")); + sm.insert("j", "1"); + sm.erase_if_exists("j"); + REQUIRE(!sm.has_key("j")); + sm.insert("i", "0"); sm.insert("j", "1"); @@ -269,7 +297,7 @@ TEST_CASE("Sharing map collisions", "[core][util]") REQUIRE(!sm.has_key(some_keyt(8))); } -TEST_CASE("Sharing map views", "[core][util]") +TEST_CASE("Sharing map views and iteration", "[core][util]") { SECTION("View of empty map") { @@ -321,6 +349,25 @@ TEST_CASE("Sharing map views", "[core][util]") REQUIRE((pairs[3] == pt("l", "3"))); } + SECTION("Iterate") + { + sharing_map_standardt sm; + fill(sm); + + typedef std::pair pt; + std::vector pairs; + + sm.iterate([&pairs](const irep_idt &key, const std::string &value) { + pairs.push_back({key, value}); + }); + + std::sort(pairs.begin(), pairs.end()); + REQUIRE(pairs.size() == 3); + REQUIRE((pairs[0] == pt("i", "0"))); + REQUIRE((pairs[1] == pt("j", "1"))); + REQUIRE((pairs[2] == pt("k", "2"))); + } + SECTION("Delta view (no sharing, same keys)") { sharing_map_standardt sm1;