From e327ef2b1a34b14651fe38780c7b51df8226bea4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 11 Aug 2018 14:59:58 +0000 Subject: [PATCH] replace_symbolt: hide {expr,type}_map Values should only be added via insert. Add expr_map access functions as some code still does access the expr_map. --- src/analyses/constant_propagator.cpp | 33 +++++++++++++-------------- src/analyses/constant_propagator.h | 4 ++-- src/goto-programs/link_goto_model.cpp | 2 +- src/util/replace_symbol.h | 23 +++++++++++++++++++ unit/util/replace_symbol.cpp | 8 +++++++ 5 files changed, 50 insertions(+), 20 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index a62c5b76b98..9023953391f 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -298,8 +298,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const return false; if(expr.id()==ID_symbol) - if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())== - replace_const.expr_map.end()) + if(!replace_const.replaces_symbol(to_symbol_expr(expr).get_identifier())) return false; if(expr.id()==ID_index) @@ -337,8 +336,7 @@ bool constant_propagator_domaint::valuest::is_constant_address_of( /// Do not call this when iterating over replace_const.expr_map! bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id) { - replace_symbolt::expr_mapt::size_type n_erased= - replace_const.expr_map.erase(id); + const auto n_erased = replace_const.erase(id); INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all"); @@ -351,7 +349,7 @@ void constant_propagator_domaint::valuest::set_dirty_to_top( const namespacet &ns) { typedef replace_symbolt::expr_mapt expr_mapt; - expr_mapt &expr_map=replace_const.expr_map; + expr_mapt &expr_map = replace_const.get_expr_map(); for(expr_mapt::iterator it=expr_map.begin(); it!=expr_map.end();) @@ -377,19 +375,19 @@ void constant_propagator_domaint::valuest::output( if(is_bottom) { out << " bottom\n"; - DATA_INVARIANT(replace_const.expr_map.empty(), + DATA_INVARIANT(is_empty(), "If the domain is bottom, the map must be empty"); return; } INVARIANT(!is_bottom, "Have handled bottom"); - if(replace_const.expr_map.empty()) + if(is_empty()) { out << "top\n"; return; } - for(const auto &p : replace_const.expr_map) + for(const auto &p : replace_const.get_expr_map()) { out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n'; } @@ -424,20 +422,21 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) bool changed=false; - replace_symbolt::expr_mapt &expr_map=replace_const.expr_map; - const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map; - // handle top - if(src_expr_map.empty()) + if(src.is_empty()) { // change if it was not top - changed=!expr_map.empty(); + changed = !is_empty(); set_to_top(); return changed; } + replace_symbolt::expr_mapt &expr_map = replace_const.get_expr_map(); + const replace_symbolt::expr_mapt &src_expr_map = + src.replace_const.get_expr_map(); + // remove those that are // - different in src // - do not exist in src @@ -484,12 +483,12 @@ bool constant_propagator_domaint::valuest::meet( bool changed=false; - for(const auto &m : src.replace_const.expr_map) + for(const auto &m : src.replace_const.get_expr_map()) { - replace_symbolt::expr_mapt::iterator - c_it=replace_const.expr_map.find(m.first); + replace_symbolt::expr_mapt::const_iterator c_it = + replace_const.get_expr_map().find(m.first); - if(c_it!=replace_const.expr_map.end()) + if(c_it != replace_const.get_expr_map().end()) { if(c_it->second!=m.second) { diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 529dce612f3..80a3579fcf8 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -105,7 +105,7 @@ class constant_propagator_domaint:public ai_domain_baset void set_to(const irep_idt &lhs, const exprt &rhs) { - replace_const.expr_map[lhs]=rhs; + replace_const.get_expr_map()[lhs] = rhs; is_bottom=false; } @@ -129,7 +129,7 @@ class constant_propagator_domaint:public ai_domain_baset bool is_empty() const { - return replace_const.expr_map.empty(); + return replace_const.empty(); } void output(std::ostream &out, const namespacet &ns) const; diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index be7c761cdff..5342c7a8fdb 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -140,7 +140,7 @@ static bool link_functions( rename_symbols_in_function(dest_it->second, final_id, macro_application); } - if(!object_type_updates.expr_map.empty()) + if(!object_type_updates.empty()) { Forall_goto_functions(dest_it, dest_functions) Forall_goto_program_instructions(iit, dest_it->second.body) diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index e3b0f65f0a6..d178bdddf4b 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// Replace expression or type symbols by an expression or type, respectively. class replace_symbolt { public: @@ -79,9 +80,31 @@ class replace_symbolt return expr_map.empty() && type_map.empty(); } + std::size_t erase(const irep_idt &id) + { + return expr_map.erase(id) + type_map.erase(id); + } + + bool replaces_symbol(const irep_idt &id) const + { + return expr_map.find(id) != expr_map.end() || + type_map.find(id) != type_map.end(); + } + replace_symbolt(); virtual ~replace_symbolt(); + const expr_mapt &get_expr_map() const + { + return expr_map; + } + + expr_mapt &get_expr_map() + { + return expr_map; + } + +protected: expr_mapt expr_map; type_mapt type_map; diff --git a/unit/util/replace_symbol.cpp b/unit/util/replace_symbol.cpp index ad5190c8353..8e9cbe98eef 100644 --- a/unit/util/replace_symbol.cpp +++ b/unit/util/replace_symbol.cpp @@ -26,7 +26,11 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]") exprt other_expr("other"); replace_symbolt r; + REQUIRE(r.empty()); + r.insert("a", other_expr); + REQUIRE(r.replaces_symbol("a")); + REQUIRE(r.get_expr_map().size() == 1); REQUIRE(r.replace(binary) == false); REQUIRE(binary.op0() == other_expr); @@ -37,8 +41,12 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]") REQUIRE(r.replace(s2) == true); REQUIRE(s2 == symbol_exprt("b", typet("some_type"))); + REQUIRE(r.replace(array_type) == false); REQUIRE(array_type.size() == other_expr); + + REQUIRE(r.erase("a") == 1); + REQUIRE(r.empty()); } TEST_CASE("Lvalue only", "[core][util][replace_symbol]")