diff --git a/regression/cbmc/Array_UF22/main.c b/regression/cbmc/Array_UF22/main.c index 20ece5e5fe7..dff613e2422 100644 --- a/regression/cbmc/Array_UF22/main.c +++ b/regression/cbmc/Array_UF22/main.c @@ -1,6 +1,7 @@ int main() { - int a[2] = {0}; - int b[2] = {0}; + int x; + int a[2] = {x}; + int b[2] = {x}; __CPROVER_assert(__CPROVER_array_equal(a, b), "equal"); } diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 878826470ce..80b9c778a45 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -416,13 +416,13 @@ bool constant_propagator_domaint::ai_simplify( return partial_evaluate(values, condition, ns); } -class constant_propagator_is_constantt : public is_constantt +class constant_propagator_can_forward_propagatet : public can_forward_propagatet { public: - constant_propagator_is_constantt( + constant_propagator_can_forward_propagatet( const replace_symbolt &replace_const, const namespacet &ns) - : is_constantt(ns), replace_const(replace_const) + : can_forward_propagatet(ns), replace_const(replace_const) { } @@ -437,7 +437,7 @@ class constant_propagator_is_constantt : public is_constantt if(expr.id() == ID_symbol) return is_constant(to_symbol_expr(expr).get_identifier()); - return is_constantt::is_constant(expr); + return can_forward_propagatet::is_constant(expr); } const replace_symbolt &replace_const; @@ -447,14 +447,15 @@ bool constant_propagator_domaint::valuest::is_constant( const exprt &expr, const namespacet &ns) const { - return constant_propagator_is_constantt(replace_const, ns)(expr); + return constant_propagator_can_forward_propagatet(replace_const, ns)(expr); } bool constant_propagator_domaint::valuest::is_constant( const irep_idt &id, const namespacet &ns) const { - return constant_propagator_is_constantt(replace_const, ns).is_constant(id); + return constant_propagator_can_forward_propagatet(replace_const, ns) + .is_constant(id); } /// Do not call this when iterating over replace_const.expr_map! diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index e2f82bc6f85..4263bd79051 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -4495,23 +4495,60 @@ void c_typecheck_baset::typecheck_side_effect_assignment( throw 0; } -class is_compile_time_constantt : public is_constantt +/// Architecturally similar to \ref can_forward_propagatet, but specialized for +/// what is a constexpr, i.e., an expression that can be fully evaluated at +/// compile time. +class is_compile_time_constantt { public: - explicit is_compile_time_constantt(const namespacet &ns) : is_constantt(ns) + explicit is_compile_time_constantt(const namespacet &ns) : ns(ns) { } + /// returns true iff the expression can be considered constant + bool operator()(const exprt &e) const + { + return is_constant(e); + } + protected: - bool is_constant(const exprt &e) const override + const namespacet &ns; + + /// This function determines what expressions are to be propagated as + /// "constants" + bool is_constant(const exprt &e) const { if(e.id() == ID_infinity) return true; - else - return is_constantt::is_constant(e); + + if(e.is_constant()) + return true; + + if(e.id() == ID_address_of) + { + return is_constant_address_of(to_address_of_expr(e).object()); + } + else if( + e.id() == ID_typecast || e.id() == ID_array_of || e.id() == ID_plus || + e.id() == ID_mult || e.id() == ID_array || e.id() == ID_with || + e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union || + e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt || + e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge || + e.id() == ID_if || e.id() == ID_not || e.id() == ID_and || + e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand || + e.id() == ID_bitor || e.id() == ID_bitxor) + { + return std::all_of( + e.operands().begin(), e.operands().end(), [this](const exprt &op) { + return is_constant(op); + }); + } + + return false; } - bool is_constant_address_of(const exprt &e) const override + /// this function determines which reference-typed expressions are constant + bool is_constant_address_of(const exprt &e) const { if(e.id() == ID_symbol) { @@ -4522,8 +4559,27 @@ class is_compile_time_constantt : public is_constantt return true; else if(e.id() == ID_label) return true; - else - return is_constantt::is_constant_address_of(e); + else if(e.id() == ID_index) + { + const index_exprt &index_expr = to_index_expr(e); + + return is_constant_address_of(index_expr.array()) && + is_constant(index_expr.index()); + } + else if(e.id() == ID_member) + { + return is_constant_address_of(to_member_expr(e).compound()); + } + else if(e.id() == ID_dereference) + { + const dereference_exprt &deref = to_dereference_expr(e); + + return is_constant(deref.pointer()); + } + else if(e.id() == ID_string_constant) + return true; + + return false; } }; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp index f6917a91fec..a0ed6b09afc 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp @@ -66,7 +66,7 @@ assignst dfcc_infer_loop_assigns( // widen or drop targets that depend on loop-locals or are non-constant, // ie. depend on other locations assigned by the loop. // e.g: if the loop assigns {i, a[i]}, then a[i] is non-constant. - havoc_utils_is_constantt is_constant(assigns, ns); + havoc_utils_can_forward_propagatet is_constant(assigns, ns); assignst result; for(const auto &expr : assigns) { diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 1de892e76d7..654fb9fa880 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -341,7 +341,7 @@ void widen_assigns(assignst &assigns, const namespacet &ns) { assignst result; - havoc_utils_is_constantt is_constant(assigns, ns); + havoc_utils_can_forward_propagatet is_constant(assigns, ns); for(const auto &e : assigns) { diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h index d0b02301109..4cf32769f01 100644 --- a/src/goto-instrument/havoc_utils.h +++ b/src/goto-instrument/havoc_utils.h @@ -24,22 +24,25 @@ class goto_programt; typedef std::set assignst; /// \brief A class containing utility functions for havocing expressions. -class havoc_utils_is_constantt : public is_constantt +class havoc_utils_can_forward_propagatet : public can_forward_propagatet { public: - explicit havoc_utils_is_constantt(const assignst &mod, const namespacet &ns) - : is_constantt(ns), assigns(mod) + explicit havoc_utils_can_forward_propagatet( + const assignst &mod, + const namespacet &ns) + : can_forward_propagatet(ns), assigns(mod) { } bool is_constant(const exprt &expr) const override { - // Besides the "usual" constants (checked in is_constantt::is_constant), - // we also treat unmodified symbols as constants + // Besides the "usual" constants (checked in + // can_forward_propagatet::is_constant), we also treat unmodified symbols as + // constants if(expr.id() == ID_symbol && assigns.find(expr) == assigns.end()) return true; - return is_constantt::is_constant(expr); + return can_forward_propagatet::is_constant(expr); } protected: @@ -102,7 +105,7 @@ class havoc_utilst protected: const assignst &assigns; - const havoc_utils_is_constantt is_constant; + const havoc_utils_can_forward_propagatet is_constant; }; #endif // CPROVER_GOTO_INSTRUMENT_HAVOC_UTILS_H diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index 38ec76b31d7..fb8e382f437 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -7,11 +7,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com \*******************************************************************/ #include "goto_state.h" -#include "goto_symex_is_constant.h" -#include "goto_symex_state.h" #include +#include "goto_symex_can_forward_propagate.h" +#include "goto_symex_state.h" + /// Print the constant propagation map in a human-friendly format. /// This is primarily for use from the debugger; please don't delete me just /// because there aren't any current callers. @@ -91,7 +92,7 @@ void goto_statet::apply_condition( if(is_ssa_expr(rhs)) std::swap(lhs, rhs); - if(is_ssa_expr(lhs) && goto_symex_is_constantt(ns)(rhs)) + if(is_ssa_expr(lhs) && goto_symex_can_forward_propagatet(ns)(rhs)) { const ssa_exprt &ssa_lhs = to_ssa_expr(lhs); INVARIANT( @@ -141,7 +142,7 @@ void goto_statet::apply_condition( if(is_ssa_expr(rhs)) std::swap(lhs, rhs); - if(!is_ssa_expr(lhs) || !goto_symex_is_constantt(ns)(rhs)) + if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs)) return; if(rhs.is_true()) diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_can_forward_propagate.h similarity index 71% rename from src/goto-symex/goto_symex_is_constant.h rename to src/goto-symex/goto_symex_can_forward_propagate.h index b3e93248943..dcd6eb63c71 100644 --- a/src/goto-symex/goto_symex_is_constant.h +++ b/src/goto-symex/goto_symex_can_forward_propagate.h @@ -9,16 +9,17 @@ Author: Michael Tautschig, tautschn@amazon.com /// \file /// GOTO Symex constant propagation -#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H -#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H +#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H +#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H #include #include -class goto_symex_is_constantt : public is_constantt +class goto_symex_can_forward_propagatet : public can_forward_propagatet { public: - explicit goto_symex_is_constantt(const namespacet &ns) : is_constantt(ns) + explicit goto_symex_can_forward_propagatet(const namespacet &ns) + : can_forward_propagatet(ns) { } @@ -56,8 +57,8 @@ class goto_symex_is_constantt : public is_constantt #endif } - return is_constantt::is_constant(expr); + return can_forward_propagatet::is_constant(expr); } }; -#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H +#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_CAN_FORWARD_PROPAGATE_H diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 7bb55a18693..5cc2e512bce 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "goto_symex_is_constant.h" +#include "goto_symex_can_forward_propagate.h" #include "symex_target_equation.h" static void get_l1_name(exprt &expr); @@ -112,7 +112,7 @@ renamedt goto_symex_statet::assignment( "pointer handling for concurrency is unsound"); // Update constant propagation map -- the RHS is L2 - if(!is_shared && record_value && goto_symex_is_constantt(ns)(rhs)) + if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs)) { const auto propagation_entry = propagation.find(l1_identifier); if(!propagation_entry.has_value()) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index bcfa6c0f191..b0f82868f6e 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "goto_symex.h" -#include "goto_symex_is_constant.h" +#include "goto_symex_can_forward_propagate.h" #include "path_storage.h" #include @@ -204,7 +204,7 @@ static optionalt> try_evaluate_pointer_comparison( if(!symbol_expr_lhs) return {}; - if(!goto_symex_is_constantt(ns)(rhs)) + if(!goto_symex_can_forward_propagatet(ns)(rhs)) return {}; return try_evaluate_pointer_comparison( diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index e681bb2fed6..ab7bfb148b9 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -160,7 +160,7 @@ void enumerative_loop_contracts_synthesizert::synthesize_assigns( if(new_assign.id() == ID_index || new_assign.id() == ID_dereference) { address_of_exprt address_of_new_assigns(new_assign); - havoc_utils_is_constantt is_constant(assigns_map[loop_id], ns); + havoc_utils_can_forward_propagatet is_constant(assigns_map[loop_id], ns); if(!is_constant(address_of_new_assigns)) { new_assign = pointer_object(address_of_new_assigns); diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 089dc217aa2..a04952856bc 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -226,31 +226,34 @@ const exprt &skip_typecast(const exprt &expr) /// This function determines what expressions are to be propagated as /// "constants" -bool is_constantt::is_constant(const exprt &expr) const +bool can_forward_propagatet::is_constant(const exprt &expr) const { - if(expr.is_constant()) - return true; + if( + expr.id() == ID_symbol || expr.id() == ID_nondet_symbol || + expr.id() == ID_side_effect) + { + return false; + } 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 || - expr.id() == ID_empty_union || expr.id() == ID_equal || - expr.id() == ID_notequal || expr.id() == ID_lt || expr.id() == ID_le || - expr.id() == ID_gt || expr.id() == ID_ge || expr.id() == ID_if || - expr.id() == ID_not || expr.id() == ID_and || expr.id() == ID_or || - expr.id() == ID_bitnot || expr.id() == ID_bitand || expr.id() == ID_bitor || - expr.id() == ID_bitxor || expr.id() == ID_byte_update_big_endian || - expr.id() == ID_byte_update_little_endian) + else if(auto index = expr_try_dynamic_cast(expr)) { - return std::all_of( - expr.operands().begin(), expr.operands().end(), [this](const exprt &e) { - return is_constant(e); - }); + if(!is_constant(index->array()) || !index->index().is_constant()) + return false; + + const auto &array_type = to_array_type(index->array().type()); + if(!array_type.size().is_constant()) + return false; + + const mp_integer size = + numeric_cast_v(to_constant_expr(array_type.size())); + const mp_integer index_int = + numeric_cast_v(to_constant_expr(index->index())); + + return index_int >= 0 && index_int < size; } else if(auto be = expr_try_dynamic_cast(expr)) { @@ -269,7 +272,7 @@ bool is_constantt::is_constant(const exprt &expr) const numeric_cast_v(to_constant_expr(be->offset())) * be->get_bits_per_byte(); - return offset_bits + *extract_bits <= *op_bits; + return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits; } else if(auto eb = expr_try_dynamic_cast(expr)) { @@ -292,12 +295,18 @@ bool is_constantt::is_constant(const exprt &expr) const return lower_bound >= 0 && lower_bound <= upper_bound && upper_bound < src_bits; } - - return false; + else + { + // std::all_of returns true when there are no operands + return std::all_of( + expr.operands().begin(), expr.operands().end(), [this](const exprt &e) { + return is_constant(e); + }); + } } /// this function determines which reference-typed expressions are constant -bool is_constantt::is_constant_address_of(const exprt &expr) const +bool can_forward_propagatet::is_constant_address_of(const exprt &expr) const { if(expr.id() == ID_symbol) { diff --git a/src/util/expr_util.h b/src/util/expr_util.h index 3b31c1de156..b423dcdd9fb 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -82,13 +82,13 @@ 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 +/// An implementation may 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 +class can_forward_propagatet { public: - explicit is_constantt(const namespacet &ns) : ns(ns) + explicit can_forward_propagatet(const namespacet &ns) : ns(ns) { } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index c7925260cfe..1ac767222dd 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1986,7 +1986,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) if(subexpr.has_value() && subexpr.value() != expr) return changed(simplify_rec(subexpr.value())); // recursive call - if(is_constantt(ns)(expr)) + if(can_forward_propagatet(ns)(expr)) return changed(simplify_rec(lower_byte_extract(expr, ns))); return unchanged(expr); diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp index 435427e4712..29bb54a7d6f 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Unit tests for goto_symex_is_constantt +Module: Unit tests for goto_symex_can_forward_propagatet Author: Diffblue Ltd. @@ -11,7 +11,7 @@ Author: Diffblue Ltd. #include #include -#include +#include #include SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") @@ -24,7 +24,7 @@ SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") sizeof_constant.set(ID_C_c_sizeof_type, int_type); symbol_exprt non_constant("x", int_type); - goto_symex_is_constantt is_constant(ns); + goto_symex_can_forward_propagatet is_constant(ns); GIVEN("Sizeof expression multiplied by a non-constant") {