diff --git a/regression/goto-instrument/constant-propagation1/main.c b/regression/goto-instrument/constant-propagation1/main.c new file mode 100644 index 00000000000..66892537b31 --- /dev/null +++ b/regression/goto-instrument/constant-propagation1/main.c @@ -0,0 +1,18 @@ +#include + +void main() +{ + unsigned char n; + __CPROVER_assume(n > 0); // To keep division well defined + __CPROVER_assume(n * n > 0); // To keep division well defined + + unsigned char i = 0; + unsigned char j = 0; + + unsigned char aux1 = i / (n * n); + for (i = 0; i < n; ++i, aux1 = i / (n * n)) { + for (j = 0; j < n; ++j) { + } + } + assert(i != n); +} diff --git a/regression/goto-instrument/constant-propagation1/test.desc b/regression/goto-instrument/constant-propagation1/test.desc new file mode 100644 index 00000000000..e67a04dedf6 --- /dev/null +++ b/regression/goto-instrument/constant-propagation1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--constant-propagator --unwind 3 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 77c7d7f92d0..a63a4d4e1c6 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -22,7 +22,6 @@ SRC = ai.cpp \ locals.cpp \ natural_loops.cpp \ reaching_definitions.cpp \ - replace_symbol_ext.cpp \ static_analysis.cpp \ uncaught_exceptions_analysis.cpp \ uninitialized_domain.cpp \ diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index aef07c8d3f1..19f684d681f 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Constant Propagation +Module: Constant propagation Author: Peter Schrammel @@ -18,107 +18,27 @@ Author: Peter Schrammel #include #include #include - -exprt concatenate_array_id( - const exprt &array, const exprt &index, - const typet &type) -{ - std::string a, idx, identifier; - a = array.get_string(ID_identifier); - - if (index.id()==ID_typecast) - idx = index.op0().get_string(ID_value); - else - idx = index.get_string(ID_value); - - mp_integer i=string2integer(idx); - identifier=a+"["+integer2string(i)+"]"; - symbol_exprt new_expr(identifier, type); - - return new_expr; -} - -exprt concatenate_array_id( - const exprt &array, const mp_integer &index, - const typet &type) -{ - std::string a, identifier; - a = array.get_string(ID_identifier); - identifier=a+"["+integer2string(index)+"]"; - symbol_exprt new_expr(identifier, type); - - return new_expr; -} +#include void constant_propagator_domaint::assign_rec( valuest &values, - const exprt &lhs, const exprt &rhs, + const exprt &lhs, + const exprt &rhs, const namespacet &ns) { - const typet & lhs_type = ns.follow(lhs.type()); - const typet & rhs_type = ns.follow(rhs.type()); + if(lhs.id()!=ID_symbol) + return; -#ifdef DEBUG - std::cout << "assign: " << from_expr(ns, "", lhs) - << " := " << from_type(ns, "", rhs_type) << '\n'; -#endif + const symbol_exprt &s=to_symbol_expr(lhs); - if(lhs.id()==ID_symbol && rhs.id()==ID_if) - { - exprt cond=rhs.op0(); - assert(cond.operands().size()==2); - if(values.is_constant(cond.op0()) - && values.is_constant(cond.op1())) - { - if(cond.op0().id()==ID_index) - { - exprt index=cond.op0(); - exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type()); - values.replace_const(new_expr); - cond.op0()=new_expr; - cond = simplify_expr(cond,ns); - } - else - UNREACHABLE; + exprt tmp=rhs; + values.replace_const(tmp); + simplify(tmp, ns); - assign(values, to_symbol_expr(lhs), cond, ns); - } - } - else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array - && rhs_type.id()!=ID_struct - && rhs_type.id()!=ID_union) - { - if(values.is_constant(rhs)) - assign(values, to_symbol_expr(lhs), rhs, ns); - else - values.set_to_top(to_symbol_expr(lhs)); - } - else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array - && rhs_type.id()==ID_array) - { - exprt new_expr; - mp_integer idx=0; - forall_operands(it, rhs) - { - new_expr=concatenate_array_id(lhs, idx, it->type()); - assign(values, to_symbol_expr(new_expr), *it, ns); - idx = idx +1; - } - } - else if (lhs.id()==ID_index) - { - if (values.is_constant(lhs.op1()) - && values.is_constant(rhs)) - { - exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type()); - assign(values, to_symbol_expr(new_expr), rhs, ns); - } - } -#if 0 - else // TODO: could make field or array element-sensitive - { - } -#endif + if(tmp.is_constant()) + values.set_to(s, tmp); + else + values.set_to_top(s); } void constant_propagator_domaint::transform( @@ -127,16 +47,31 @@ void constant_propagator_domaint::transform( ai_baset &ai, const namespacet &ns) { - #ifdef DEBUG +#ifdef DEBUG + std::cout << "Transform from/to:\n"; std::cout << from->location_number << " --> " << to->location_number << '\n'; - #endif +#endif #ifdef DEBUG - std::cout << "before:\n"; + std::cout << "Before:\n"; output(std::cout, ai, ns); #endif + // When the domain is used with constant_propagator_ait, + // information about dirty variables and config flags are + // available. Otherwise, the below will be null and we use default + // values + const constant_propagator_ait *cp= + dynamic_cast(&ai); + bool have_dirty=(cp!=nullptr); + + // Transform on a domain that is bottom is possible + // if a branch is impossible the target can still wind + // up on the work list. + if(values.is_bottom) + return; + if(from->is_decl()) { const code_declt &code_decl=to_code_decl(from->code); @@ -146,8 +81,8 @@ void constant_propagator_domaint::transform( else if(from->is_assign()) { const code_assignt &assignment=to_code_assign(from->code); - const exprt &lhs = assignment.lhs(); - const exprt &rhs = assignment.rhs(); + const exprt &lhs=assignment.lhs(); + const exprt &rhs=assignment.rhs(); assign_rec(values, lhs, rhs, ns); } else if(from->is_assume()) @@ -159,19 +94,21 @@ void constant_propagator_domaint::transform( exprt g; if(from->get_target()==to) - g = simplify_expr(from->guard, ns); + g=simplify_expr(from->guard, ns); else - g = simplify_expr(not_exprt(from->guard), ns); + g=simplify_expr(not_exprt(from->guard), ns); - if (g.is_false()) + if(g.is_false()) values.set_to_bottom(); else { - //TODO: we need to support widening! - if (g.is_constant()) - values.set_to_top(); - else - two_way_propagate_rec(g, ns); + two_way_propagate_rec(g, ns); + // If two way propagate is enabled then it may be possible to detect + // that the branch condition is infeasible and thus the domain should + // be set to bottom. Without it the domain will only be set to bottom + // if the guard expression is trivially (i.e. without context) false. + INVARIANT(!values.is_bottom, + "Without two-way propagation this should be impossible."); } } else if(from->is_dead()) @@ -181,30 +118,91 @@ void constant_propagator_domaint::transform( } else if(from->is_function_call()) { - const exprt &function=to_code_function_call(from->code).function(); + const code_function_callt &function_call=to_code_function_call(from->code); + const exprt &function=function_call.function(); + + const locationt& next=std::next(from); if(function.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - - if(identifier=="__CPROVER_set_must" || - identifier=="__CPROVER_get_must" || - identifier=="__CPROVER_set_may" || - identifier=="__CPROVER_get_may" || - identifier=="__CPROVER_cleanup" || - identifier=="__CPROVER_clear_may" || - identifier=="__CPROVER_clear_must") + // called function identifier + const symbol_exprt &symbol_expr=to_symbol_expr(function); + const irep_idt id=symbol_expr.get_identifier(); + + if(to==next) { + if(id==CPROVER_PREFIX "set_must" || + id==CPROVER_PREFIX "get_must" || + id==CPROVER_PREFIX "set_may" || + id==CPROVER_PREFIX "get_may" || + id==CPROVER_PREFIX "cleanup" || + id==CPROVER_PREFIX "clear_may" || + id==CPROVER_PREFIX "clear_must") + { + // no effect on constants + } + else + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } } else - values.set_to_top(); + { + // we have an actual call + + // parameters of called function + const symbolt &symbol=ns.lookup(id); + const code_typet &code_type=to_code_type(symbol.type); + const code_typet::parameterst ¶meters=code_type.parameters(); + + const code_function_callt::argumentst &arguments= + function_call.arguments(); + + code_typet::parameterst::const_iterator p_it=parameters.begin(); + for(const auto &arg : arguments) + { + if(p_it==parameters.end()) + break; + + const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type()); + assign_rec(values, parameter_expr, arg, ns); + + ++p_it; + } + } } else - values.set_to_top(); + { + // unresolved call + INVARIANT(to==next, "Unresolved call can only be approximated if a skip"); + + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } } + else if(from->is_end_function()) + { + // erase parameters + + const irep_idt id=from->function; + const symbolt &symbol=ns.lookup(id); + + const code_typet &type=to_code_type(symbol.type); + + for(const auto ¶m : type.parameters()) + values.set_to_top(param.get_identifier()); + } + + INVARIANT(from->is_goto() || !values.is_bottom, + "Transform only sets bottom by using branch conditions"); #ifdef DEBUG - std::cout << "after:\n"; + std::cout << "After:\n"; output(std::cout, ai, ns); #endif } @@ -218,8 +216,11 @@ bool constant_propagator_domaint::two_way_propagate_rec( #ifdef DEBUG std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n'; #endif - bool change = false; + bool change=false; + + // this seems to be buggy at present +#if 0 if(expr.id()==ID_and) { // need a fixed point here to get the most out of it @@ -229,38 +230,29 @@ bool constant_propagator_domaint::two_way_propagate_rec( forall_operands(it, expr) if(two_way_propagate_rec(*it, ns)) - change = true; + change=true; } while(change); } else if(expr.id()==ID_equal) { - const exprt &lhs = expr.op0(); - const exprt &rhs = expr.op1(); + const exprt &lhs=expr.op0(); + const exprt &rhs=expr.op1(); // two-way propagation - valuest copy_values = values; + valuest copy_values=values; assign_rec(copy_values, lhs, rhs, ns); if(!values.is_constant(rhs) || values.is_constant(lhs)) - assign_rec(values, rhs, lhs, ns); - change = values.meet(copy_values); + assign_rec(values, rhs, lhs, ns); + change=values.meet(copy_values); } +#endif #ifdef DEBUG std::cout << "two_way_propagate_rec: " << change << '\n'; #endif - return change; -} -void constant_propagator_domaint::assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const -{ - values.replace_const(rhs); - rhs = simplify_expr(rhs, ns); - dest.set_to(lhs, rhs); + return change; } /// Simplify the condition given context-sensitive knowledge from the abstract @@ -277,17 +269,6 @@ bool constant_propagator_domaint::ai_simplify( return b; } -bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const -{ - exprt new_expr = concatenate_array_id(expr.op0(), - expr.op1(), expr.type()); - - if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) == - replace_const.expr_map.end()) - return false; - - return true; -} bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const { @@ -300,12 +281,12 @@ 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()) == + if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())== replace_const.expr_map.end()) return false; - if (expr.id()==ID_index) - return is_array_constant(expr); + if(expr.id()==ID_index) + return false; if(expr.id()==ID_address_of) return is_constant_address_of(to_address_of_expr(expr).object()); @@ -339,19 +320,35 @@ 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 result = false; + replace_symbolt::expr_mapt::size_type n_erased= + replace_const.expr_map.erase(id); - replace_symbolt::expr_mapt::iterator r_it = - replace_const.expr_map.find(id); + INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all"); - if(r_it != replace_const.expr_map.end()) + return n_erased>0; +} + + +void constant_propagator_domaint::valuest::set_dirty_to_top( + const dirtyt &dirty, + const namespacet &ns) +{ + typedef replace_symbolt::expr_mapt expr_mapt; + expr_mapt &expr_map=replace_const.expr_map; + + for(expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) { - assert(!is_bottom); - replace_const.expr_map.erase(r_it); - result = true; - } + const irep_idt id=it->first; - return result; + const symbolt &symbol=ns.lookup(id); + + if((!symbol.is_procedure_local() || dirty(id)) && + !symbol.type.get_bool(ID_C_constant)) + it=expr_map.erase(it); + else + it++; + } } void constant_propagator_domaint::valuest::output( @@ -361,11 +358,24 @@ void constant_propagator_domaint::valuest::output( out << "const map:\n"; if(is_bottom) + { out << " bottom\n"; + DATA_INVARIANT(replace_const.expr_map.empty(), + "If the domain is bottom, the map must be empty"); + return; + } + + INVARIANT(!is_bottom, "Have handled bottom"); + if(replace_const.expr_map.empty()) + { + out << "top\n"; + return; + } - for(const auto &replace_pair : replace_const.expr_map) - out << ' ' << replace_pair.first << "=" - << from_expr(ns, "", replace_pair.second) << '\n'; + for(const auto &p : replace_const.expr_map) + { + out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n'; + } } void constant_propagator_domaint::output( @@ -387,38 +397,62 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) // just copy if(is_bottom) { - replace_const = src.replace_const; - is_bottom = src.is_bottom; + PRECONDITION(!src.is_bottom); + replace_const=src.replace_const; // copy + is_bottom=false; return true; } - bool changed = false; + INVARIANT(!is_bottom && !src.is_bottom, "Case handled"); - // set everything to top that is not in src - for(replace_symbolt::expr_mapt::const_iterator - it=replace_const.expr_map.begin(); - it!=replace_const.expr_map.end(); - ) // no it++ + 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()) { - const replace_symbolt::expr_mapt::const_iterator - b_it=src.replace_const.expr_map.find(it->first); + // change if it was not top + changed=!expr_map.empty(); - if(b_it==src.replace_const.expr_map.end()) + set_to_top(); + + return changed; + } + + // remove those that are + // - different in src + // - do not exist in src + for(replace_symbolt::expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) + { + const irep_idt id=it->first; + const exprt &expr=it->second; + + replace_symbolt::expr_mapt::const_iterator s_it; + s_it=src_expr_map.find(id); + + if(s_it!=src_expr_map.end()) { - //cannot use set_to_top here - replace_const.expr_map.erase(it); - changed = true; - break; + // check value + const exprt &src_expr=s_it->second; + + if(expr!=src_expr) + { + it=expr_map.erase(it); + changed=true; + } + else + it++; } else { - const exprt previous=it->second; - replace_const.expr_map[b_it->first]=b_it->second; - if (it->second != previous) changed = true; - - it++; + it=expr_map.erase(it); + changed=true; } } + return changed; } @@ -429,16 +463,16 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) if(src.is_bottom || is_bottom) return false; - bool changed = false; + bool changed=false; - for(const auto &src_replace_pair : src.replace_const.expr_map) + for(const auto &m : src.replace_const.expr_map) { - replace_symbolt::expr_mapt::iterator c_it= - replace_const.expr_map.find(src_replace_pair.first); + replace_symbolt::expr_mapt::iterator + c_it=replace_const.expr_map.find(m.first); if(c_it!=replace_const.expr_map.end()) { - if(c_it->second!=src_replace_pair.second) + if(c_it->second!=m.second) { set_to_bottom(); changed=true; @@ -447,7 +481,7 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) } else { - set_to(src_replace_pair.first, src_replace_pair.second); + set_to(m.first, m.second); changed=true; } } @@ -472,21 +506,6 @@ void constant_propagator_ait::replace( replace(f_it->second, ns); } -void constant_propagator_ait::replace_array_symbol(exprt &expr) -{ - if (expr.id()==ID_index) - expr = concatenate_array_id(expr.op0(), - expr.op1(), expr.type()); - - Forall_operands(it, expr) - { - if (it->id()==ID_equal) - replace_array_symbol(it->op0()); - else if (it->id()==ID_index) - replace_array_symbol(expr.op0()); - } - -} void constant_propagator_ait::replace( goto_functionst::goto_functiont &goto_function, @@ -494,9 +513,9 @@ void constant_propagator_ait::replace( { Forall_goto_program_instructions(it, goto_function.body) { - state_mapt::iterator s_it = state_map.find(it); + state_mapt::iterator s_it=state_map.find(it); - if(s_it == state_map.end()) + if(s_it==state_map.end()) continue; replace_types_rec(s_it->second.values.replace_const, it->code); @@ -504,32 +523,32 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - replace_array_symbol(it->guard); s_it->second.values.replace_const(it->guard); - it->guard = simplify_expr(it->guard, ns); + simplify(it->guard, ns); } else if(it->is_assign()) { - exprt &rhs = to_code_assign(it->code).rhs(); + exprt &rhs=to_code_assign(it->code).rhs(); s_it->second.values.replace_const(rhs); - rhs = simplify_expr(rhs, ns); - if (rhs.id()==ID_constant) + simplify(rhs, ns); + if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { s_it->second.values.replace_const( to_code_function_call(it->code).function()); - simplify_expr(to_code_function_call(it->code).function(), ns); - exprt::operandst &args = + simplify(to_code_function_call(it->code).function(), ns); + + exprt::operandst &args= to_code_function_call(it->code).arguments(); - for(exprt::operandst::iterator o_it = args.begin(); - o_it != args.end(); ++o_it) + for(exprt::operandst::iterator o_it=args.begin(); + o_it!=args.end(); ++o_it) { s_it->second.values.replace_const(*o_it); - *o_it = simplify_expr(*o_it, ns); + simplify(*o_it, ns); } } else if(it->is_other()) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0e2e65383a3..695aea8782f 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -12,93 +12,116 @@ Author: Peter Schrammel #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H -#include "ai.h" +#include +#include -#include "replace_symbol_ext.h" +#include "ai.h" +#include "dirty.h" class constant_propagator_domaint:public ai_domain_baset { public: - void transform( - locationt, - locationt, - ai_baset &, - const namespacet &) final; - void output( - std::ostream &, - const ai_baset &, - const namespacet &) const final; - void make_top() final { values.set_to_top(); } - void make_bottom() final { values.set_to_bottom(); } - void make_entry() final { values.set_to_top(); } - bool merge(const constant_propagator_domaint &, locationt, locationt); + virtual void transform( + locationt from, + locationt to, + ai_baset &ai_base, + const namespacet &ns) override; + + virtual void output( + std::ostream &out, + const ai_baset &ai_base, + const namespacet &ns) const override; + + bool merge( + const constant_propagator_domaint &other, + locationt from, + locationt to); virtual bool ai_simplify( exprt &condition, const namespacet &ns) const override; + virtual void make_bottom() override + { + values.set_to_bottom(); + } + + virtual void make_top() override + { + values.set_to_top(); + } + + virtual void make_entry() override + { + make_top(); + } + struct valuest { public: - valuest():is_bottom(true) { } + valuest():is_bottom(true) {} // maps variables to constants - replace_symbol_extt replace_const; + replace_symbolt replace_const; bool is_bottom; - void output(std::ostream &, const namespacet &) const; - bool merge(const valuest &src); bool meet(const valuest &src); - void set_to_bottom() + // set whole state + + inline void set_to_bottom() { replace_const.clear(); - is_bottom = true; + is_bottom=true; } - void set_to(const irep_idt &lhs_id, const exprt &rhs_val) + inline void set_to_top() { - replace_const.expr_map[lhs_id] = rhs_val; - is_bottom = false; + replace_const.clear(); + is_bottom=false; } - void set_to(const symbol_exprt &lhs, const exprt &rhs_val) + // set single identifier + + inline void set_to(const irep_idt &lhs, const exprt &rhs) { - set_to(lhs.get_identifier(), rhs_val); + replace_const.expr_map[lhs]=rhs; + is_bottom=false; } - bool is_constant(const exprt &expr) const; - bool is_array_constant(const exprt &expr) const; - bool is_constant_address_of(const exprt &expr) const; - bool set_to_top(const irep_idt &id); + inline 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()); } - void set_to_top() + bool set_to_top(const irep_idt &id); + + void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); + + bool is_constant(const exprt &expr) const; + bool is_array_constant(const exprt &expr) const; + bool is_constant_address_of(const exprt &expr) const; + + bool is_empty() const { - replace_const.clear(); - is_bottom = false; + return replace_const.expr_map.empty(); } + void output(std::ostream &out, const namespacet &ns) const; }; valuest values; -private: - void assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const; - +protected: void assign_rec( valuest &values, - const exprt &lhs, - const exprt &rhs, + const exprt &lhs, const exprt &rhs, const namespacet &ns); bool two_way_propagate_rec( @@ -109,8 +132,13 @@ class constant_propagator_domaint:public ai_domain_baset class constant_propagator_ait:public ait { public: + explicit constant_propagator_ait(const goto_functionst &goto_functions): + dirty(goto_functions) + { + } + constant_propagator_ait( - goto_modelt &goto_model) + goto_modelt &goto_model):dirty(goto_model.goto_functions) { const namespacet ns(goto_model.symbol_table); operator()(goto_model.goto_functions, ns); @@ -119,18 +147,17 @@ class constant_propagator_ait:public ait constant_propagator_ait( goto_functionst::goto_functiont &goto_function, - const namespacet &ns) + const namespacet &ns):dirty(goto_function) { operator()(goto_function, ns); replace(goto_function, ns); } + dirtyt dirty; + protected: friend class constant_propagator_domaint; - void replace_array_symbol( - exprt &expr); - void replace( goto_functionst::goto_functiont &, const namespacet &); @@ -142,7 +169,6 @@ class constant_propagator_ait:public ait void replace_types_rec( const replace_symbolt &replace_const, exprt &expr); - }; #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp deleted file mode 100644 index 18e0474629b..00000000000 --- a/src/analyses/replace_symbol_ext.cpp +++ /dev/null @@ -1,76 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -/// \file -/// Modified expression replacement for constant propagator - -#include "replace_symbol_ext.h" - -#include -#include - -/// does not replace object in address_of expressions -bool replace_symbol_extt::replace(exprt &dest) const -{ - bool result=true; - - // first look at type - - if(have_to_replace(dest.type())) - if(!replace_symbolt::replace(dest.type())) - result=false; - - // now do expression itself - - if(!have_to_replace(dest)) - return result; - - // do not replace object in address_of expressions - if(dest.id()==ID_address_of) - { - const exprt &object = to_address_of_expr(dest).object(); - if(object.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(object.get(ID_identifier)); - - if(it!=expr_map.end()) - return false; - } - } - else if(dest.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); - - if(it!=expr_map.end()) - { - dest=it->second; - return false; - } - } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; - - const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - - if(c_sizeof_type.is_not_nil() && - !replace_symbolt::replace( - static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; - - const irept &va_arg_type=dest.find(ID_C_va_arg_type); - - if(va_arg_type.is_not_nil() && - !replace_symbolt::replace(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; - - return result; -} diff --git a/src/analyses/replace_symbol_ext.h b/src/analyses/replace_symbol_ext.h deleted file mode 100644 index 05d7226be40..00000000000 --- a/src/analyses/replace_symbol_ext.h +++ /dev/null @@ -1,23 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -/// \file -/// Modified expression replacement for constant propagator - -#ifndef CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H -#define CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H - -#include - -class replace_symbol_extt:public replace_symbolt -{ -public: - virtual bool replace(exprt &dest) const; -}; - -#endif // CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 2585a69e61d..14765af113f 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -27,9 +27,11 @@ void replace_symbolt::insert( old_expr.get_identifier(), new_expr)); } -bool replace_symbolt::replace(exprt &dest) const +bool replace_symbolt::replace( + exprt &dest, + const bool replace_with_const) const { - bool result=true; + bool result=true; // unchanged // first look at type @@ -42,33 +44,75 @@ bool replace_symbolt::replace(exprt &dest) const if(!have_to_replace(dest)) return result; - if(dest.id()==ID_symbol) + if(dest.id()==ID_member) + { + member_exprt &me=to_member_expr(dest); + + if(!replace(me.struct_op(), replace_with_const)) // Could give non l-value. + result=false; + } + else if(dest.id()==ID_index) + { + index_exprt &ie=to_index_expr(dest); + + if(!replace(ie.array(), replace_with_const)) // Could give non l-value. + result=false; + + if(!replace(ie.index())) + result=false; + } + else if(dest.id()==ID_address_of) + { + address_of_exprt &aoe=to_address_of_expr(dest); + + if(!replace(aoe.object(), false)) + result=false; + } + else if(dest.id()==ID_symbol) { + const symbol_exprt &s=to_symbol_expr(dest); + expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); + expr_map.find(s.get_identifier()); if(it!=expr_map.end()) { - dest=it->second; + const exprt &e=it->second; + + if(!replace_with_const && e.is_constant()) // Would give non l-value. + return true; + + dest=e; + return false; } } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; + else + { + Forall_operands(it, dest) + if(!replace(*it)) + result=false; + } const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - if(c_sizeof_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; + if(c_sizeof_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_c_sizeof_type)); + + if(!replace(type)) + result=false; + } const irept &va_arg_type=dest.find(ID_C_va_arg_type); - if(va_arg_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; + if(va_arg_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_va_arg_type)); + + if(!replace(type)) + result=false; + } return result; } diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index ebc1102e921..26e246a94cd 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -38,7 +38,22 @@ class replace_symbolt type_map.insert(std::pair(identifier, type)); } - virtual bool replace(exprt &dest) const; + /// \brief Replaces a symbol with a constant + /// If you are replacing symbols with constants in an l-value, you can + /// create something that is not an l-value. For example if your + /// l-value is "a[i]" then substituting i for a constant results in an + /// l-value but substituting a for a constant (array) wouldn't. This + /// only applies to the "top level" of the expression, for example, it + /// is OK to replace b with a constant array in a[b[0]]. + /// + /// \param dest The expression in which to do the replacement + /// \param replace_with_const If false then it disables the rewrites that + /// could result in something that is not an l-value. + /// + virtual bool replace( + exprt &dest, + const bool replace_with_const=true) const; + virtual bool replace(typet &dest) const; void operator()(exprt &dest) const