diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7a7530274dd..4f7af63273e 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -79,122 +80,6 @@ void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr) ssa_expr.set_level_1(it->second.second); } -/// This function determines what expressions are to be propagated as -/// "constants" -bool goto_symex_statet::constant_propagation(const exprt &expr) const -{ - if(expr.is_constant()) - return true; - - if(expr.id()==ID_address_of) - { - const address_of_exprt &address_of_expr=to_address_of_expr(expr); - - return constant_propagation_reference(address_of_expr.object()); - } - else if(expr.id()==ID_typecast) - { - const typecast_exprt &typecast_expr=to_typecast_expr(expr); - - return constant_propagation(typecast_expr.op()); - } - else if(expr.id()==ID_plus) - { - forall_operands(it, expr) - if(!constant_propagation(*it)) - return false; - - return true; - } - else if(expr.id()==ID_mult) - { - // propagate stuff with sizeof in it - forall_operands(it, expr) - { - if(it->find(ID_C_c_sizeof_type).is_not_nil()) - return true; - else if(!constant_propagation(*it)) - return false; - } - - return true; - } - else if(expr.id()==ID_array) - { - forall_operands(it, expr) - if(!constant_propagation(*it)) - return false; - - return true; - } - else if(expr.id()==ID_array_of) - { - return constant_propagation(expr.op0()); - } - else if(expr.id()==ID_with) - { - // this is bad - /* - forall_operands(it, expr) - if(!constant_propagation(expr.op0())) - return false; - - return true; - */ - return false; - } - else if(expr.id()==ID_struct) - { - forall_operands(it, expr) - if(!constant_propagation(*it)) - return false; - - return true; - } - else if(expr.id()==ID_union) - { - forall_operands(it, expr) - if(!constant_propagation(*it)) - return false; - - return true; - } - // byte_update works, byte_extract may be out-of-bounds - else if(expr.id()==ID_byte_update_big_endian || - expr.id()==ID_byte_update_little_endian) - { - forall_operands(it, expr) - if(!constant_propagation(*it)) - return false; - - return true; - } - - return false; -} - -/// this function determines which reference-typed expressions are constant -bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const -{ - if(expr.id()==ID_symbol) - return true; - else if(expr.id()==ID_index) - { - const index_exprt &index_expr=to_index_expr(expr); - - return constant_propagation_reference(index_expr.array()) && - constant_propagation(index_expr.index()); - } - else if(expr.id()==ID_member) - { - return constant_propagation_reference(to_member_expr(expr).compound()); - } - else if(expr.id()==ID_string_constant) - return true; - - return false; -} - /// write to a variable static bool check_renaming(const exprt &expr); @@ -297,6 +182,41 @@ static void assert_l2_renaming(const exprt &expr) #endif } +class goto_symex_is_constantt : public is_constantt +{ +protected: + bool is_constant(const exprt &expr) const override + { + if(expr.id() == ID_mult) + { + // propagate stuff with sizeof in it + forall_operands(it, expr) + { + if(it->find(ID_C_c_sizeof_type).is_not_nil()) + return true; + else if(!is_constant(*it)) + return false; + } + + return true; + } + else if(expr.id() == ID_with) + { + // this is bad + /* + forall_operands(it, expr) + if(!is_constant(expr.op0())) + return false; + + return true; + */ + return false; + } + + return is_constantt::is_constant(expr); + } +}; + void goto_symex_statet::assignment( ssa_exprt &lhs, // L0/L1 const exprt &rhs, // L2 @@ -341,7 +261,7 @@ void goto_symex_statet::assignment( // for value propagation -- the RHS is L2 - if(!is_shared && record_value && constant_propagation(rhs)) + if(!is_shared && record_value && goto_symex_is_constantt()(rhs)) propagation.values[l1_identifier]=rhs; else propagation.remove(l1_identifier); diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 60623bfc26f..201389c5f4b 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -179,10 +179,6 @@ class goto_symex_statet final bool record_value, bool allow_pointer_unsoundness=false); - // what to propagate - bool constant_propagation(const exprt &expr) const; - bool constant_propagation_reference(const exprt &expr) const; - // undoes all levels of renaming void get_original_name(exprt &expr) const; void get_original_name(typet &type) const; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index d9d05afa885..69597ce385e 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -6,10 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "expr_util.h" +#include #include + #include "expr.h" #include "expr_iterator.h" #include "fixedbv.h" @@ -222,3 +223,55 @@ const exprt &skip_typecast(const exprt &expr) return skip_typecast(to_typecast_expr(expr).op()); } + +/// This function determines what expressions are to be propagated as +/// "constants" +bool is_constantt::is_constant(const exprt &expr) const +{ + if(expr.is_constant()) + return true; + + if(expr.id() == ID_address_of) + { + return is_constant_address_of(to_address_of_expr(expr).object()); + } + else if( + expr.id() == ID_typecast || expr.id() == ID_array_of || + expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array || + expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union || + // byte_update works, byte_extract may be out-of-bounds + expr.id() == ID_byte_update_big_endian || + expr.id() == ID_byte_update_little_endian) + { + return std::all_of( + expr.operands().begin(), expr.operands().end(), [this](const exprt &e) { + return is_constant(e); + }); + } + + return false; +} + +/// this function determines which reference-typed expressions are constant +bool is_constantt::is_constant_address_of(const exprt &expr) const +{ + if(expr.id() == ID_symbol) + { + return true; + } + else if(expr.id() == ID_index) + { + const index_exprt &index_expr = to_index_expr(expr); + + return is_constant_address_of(index_expr.array()) && + is_constant(index_expr.index()); + } + else if(expr.id() == ID_member) + { + return is_constant_address_of(to_member_expr(expr).compound()); + } + else if(expr.id() == ID_string_constant) + return true; + + return false; +} diff --git a/src/util/expr_util.h b/src/util/expr_util.h index aea069e5ee1..f65643474a6 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -78,4 +78,23 @@ if_exprt lift_if(const exprt &, std::size_t operand_number); /// find the expression nested inside typecasts, if any const exprt &skip_typecast(const exprt &expr); +/// Determine whether an expression is constant. A literal constant is +/// constant, but so are, e.g., sums over constants or addresses of objects. +/// An implementation derive from this class to refine what it considers +/// constant in a particular context by overriding is_constant and/or +/// is_constant_address_of. +class is_constantt +{ +public: + /// returns true iff the expression can be considered constant + bool operator()(const exprt &e) const + { + return is_constant(e); + } + +protected: + virtual bool is_constant(const exprt &) const; + virtual bool is_constant_address_of(const exprt &) const; +}; + #endif // CPROVER_UTIL_EXPR_UTIL_H