diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 9023953391f..9a849be93eb 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -214,7 +214,7 @@ void constant_propagator_domaint::transform( const code_typet &type=to_code_type(symbol.type); for(const auto ¶m : type.parameters()) - values.set_to_top(param.get_identifier()); + values.set_to_top(symbol_exprt(param.get_identifier(), param.type())); } INVARIANT(from->is_goto() || !values.is_bottom, @@ -334,9 +334,10 @@ 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) +bool constant_propagator_domaint::valuest::set_to_top( + const symbol_exprt &symbol_expr) { - const auto n_erased = replace_const.erase(id); + const auto n_erased = replace_const.erase(symbol_expr.get_identifier()); INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all"); @@ -360,7 +361,9 @@ void constant_propagator_domaint::valuest::set_dirty_to_top( if((!symbol.is_procedure_local() || dirty(id)) && !symbol.type.get_bool(ID_C_constant)) - it=expr_map.erase(it); + { + it = replace_const.erase(it); + } else it++; } @@ -456,7 +459,7 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) if(expr!=src_expr) { - it=expr_map.erase(it); + it = replace_const.erase(it); changed=true; } else @@ -464,7 +467,7 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) } else { - it=expr_map.erase(it); + it = replace_const.erase(it); changed=true; } } @@ -499,10 +502,11 @@ bool constant_propagator_domaint::valuest::meet( } else { + const typet &m_id_type = ns.lookup(m.first).type; DATA_INVARIANT( - base_type_eq(ns.lookup(m.first).type, m.second.type(), ns), + base_type_eq(m_id_type, m.second.type(), ns), "type of constant to be stored should match"); - set_to(m.first, m.second); + set_to(symbol_exprt(m.first, m_id_type), m.second); changed=true; } } @@ -558,7 +562,7 @@ bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes( { constant_propagator_domaint child(*this); child.values.set_to( - ID_cprover_rounding_mode_str, + symbol_exprt(ID_cprover_rounding_mode_str, integer_typet()), from_integer(rounding_modes[i], integer_typet())); exprt result = expr; if(child.replace_constants_and_simplify(result, ns)) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 11e51774892..62c3cb919f9 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -111,25 +111,13 @@ class constant_propagator_domaint:public ai_domain_baset return !is_bottom && replace_const.empty(); } - // set single identifier - - void set_to(const irep_idt &lhs, const exprt &rhs) - { - replace_const.get_expr_map()[lhs] = rhs; - is_bottom=false; - } - void set_to(const symbol_exprt &lhs, const exprt &rhs) { - set_to(lhs.get_identifier(), rhs); - } - - bool set_to_top(const symbol_exprt &expr) - { - return set_to_top(expr.get_identifier()); + replace_const.set(lhs, rhs); + is_bottom=false; } - bool set_to_top(const irep_idt &id); + bool set_to_top(const symbol_exprt &expr); void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index ac4a27d2772..e1307592e6b 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -30,6 +30,13 @@ void replace_symbolt::insert( old_expr.get_identifier(), new_expr)); } +void replace_symbolt::set(const symbol_exprt &old_expr, const exprt &new_expr) +{ + PRECONDITION(old_expr.type() == new_expr.type()); + expr_map[old_expr.get_identifier()] = new_expr; +} + + bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const { expr_mapt::const_iterator it = expr_map.find(s.get_identifier()); diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index be9b9e95d51..c44fc306707 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -26,9 +26,15 @@ class replace_symbolt public: typedef std::unordered_map expr_mapt; + /// Sets old_expr to be replaced by new_expr if we don't already have a + /// replacement; otherwise does nothing (i.e. std::map::insert-like + /// behaviour). void insert(const class symbol_exprt &old_expr, const exprt &new_expr); + /// Sets old_expr to be replaced by new_expr + void set(const class symbol_exprt &old_expr, const exprt &new_expr); + virtual bool replace(exprt &dest) const; virtual bool replace(typet &dest) const; @@ -57,6 +63,11 @@ class replace_symbolt return expr_map.erase(id); } + expr_mapt::iterator erase(expr_mapt::iterator it) + { + return expr_map.erase(it); + } + bool replaces_symbol(const irep_idt &id) const { return expr_map.find(id) != expr_map.end();