From 2ba7118b933b4af5c0075d04b33b4a82373c8c13 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 9 Nov 2022 13:25:58 +0000 Subject: [PATCH] Byte extract and extract bits can be constant When all operands are constants and the extract is fully within bounds of the source object then the result is constant. This permits constant-propagating byte-extract operations from pointers that are address-of. --- .../memcpy-01/constant-propagation.desc | 8 ++++ src/analyses/constant_propagator.cpp | 25 ++++++----- src/analyses/constant_propagator.h | 4 +- src/ansi-c/c_typecheck_expr.cpp | 4 +- src/goto-instrument/contracts/contracts.cpp | 2 +- src/goto-instrument/contracts/utils.cpp | 4 +- src/goto-instrument/contracts/utils.h | 4 +- src/goto-instrument/havoc_loops.cpp | 14 ++++-- src/goto-instrument/havoc_utils.h | 6 ++- src/goto-instrument/k_induction.cpp | 20 +++++++-- src/goto-symex/goto_state.cpp | 4 +- src/goto-symex/goto_symex_is_constant.h | 5 +++ src/goto-symex/goto_symex_state.cpp | 2 +- src/goto-symex/symex_goto.cpp | 2 +- src/util/expr_util.cpp | 45 ++++++++++++++++++- src/util/expr_util.h | 6 +++ unit/analyses/constant_propagator.cpp | 17 +++---- unit/goto-symex/is_constant.cpp | 14 +++--- 18 files changed, 137 insertions(+), 49 deletions(-) create mode 100644 regression/cbmc-library/memcpy-01/constant-propagation.desc diff --git a/regression/cbmc-library/memcpy-01/constant-propagation.desc b/regression/cbmc-library/memcpy-01/constant-propagation.desc new file mode 100644 index 00000000000..96f8562f647 --- /dev/null +++ b/regression/cbmc-library/memcpy-01/constant-propagation.desc @@ -0,0 +1,8 @@ +CORE +main.c +--show-vcc +main::1::m!0@1#1 = .*byte_extract_(big|little)_endian\(cast\(44, signedbv\[\d+\]\*\), 0, signedbv\[\d+\]\).* +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 27e5f3f4841..9e324df4e03 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -100,7 +100,7 @@ void constant_propagator_domaint::assign_rec( exprt tmp = rhs; partial_evaluate(dest_values, tmp, ns); - if(dest_values.is_constant(tmp)) + if(dest_values.is_constant(tmp, ns)) { DATA_INVARIANT( ns.lookup(s).type == tmp.type(), @@ -393,7 +393,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( // two-way propagation valuest copy_values=values; assign_rec(copy_values, lhs, rhs, ns, cp, false); - if(!values.is_constant(rhs) || values.is_constant(lhs)) + if(!values.is_constant(rhs, ns) || values.is_constant(lhs, ns)) assign_rec(values, rhs, lhs, ns, cp, false); change = values.meet(copy_values, ns); } @@ -419,9 +419,10 @@ bool constant_propagator_domaint::ai_simplify( class constant_propagator_is_constantt : public is_constantt { public: - explicit constant_propagator_is_constantt( - const replace_symbolt &replace_const) - : replace_const(replace_const) + constant_propagator_is_constantt( + const replace_symbolt &replace_const, + const namespacet &ns) + : is_constantt(ns), replace_const(replace_const) { } @@ -442,14 +443,18 @@ class constant_propagator_is_constantt : public is_constantt const replace_symbolt &replace_const; }; -bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const +bool constant_propagator_domaint::valuest::is_constant( + const exprt &expr, + const namespacet &ns) const { - return constant_propagator_is_constantt(replace_const)(expr); + return constant_propagator_is_constantt(replace_const, ns)(expr); } -bool constant_propagator_domaint::valuest::is_constant(const irep_idt &id) const +bool constant_propagator_domaint::valuest::is_constant( + const irep_idt &id, + const namespacet &ns) const { - return constant_propagator_is_constantt(replace_const).is_constant(id); + return constant_propagator_is_constantt(replace_const, ns).is_constant(id); } /// Do not call this when iterating over replace_const.expr_map! @@ -657,7 +662,7 @@ bool constant_propagator_domaint::partial_evaluate( // if the current rounding mode is top we can // still get a non-top result by trying all rounding // modes and checking if the results are all the same - if(!known_values.is_constant(rounding_mode_identifier())) + if(!known_values.is_constant(rounding_mode_identifier(), ns)) return partial_evaluate_with_all_rounding_modes(known_values, expr, ns); return replace_constants_and_simplify(known_values, expr, ns); diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index b054db09c35..3ab62f19c67 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -123,9 +123,9 @@ class constant_propagator_domaint:public ai_domain_baset void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); - bool is_constant(const exprt &expr) const; + bool is_constant(const exprt &expr, const namespacet &ns) const; - bool is_constant(const irep_idt &id) const; + bool is_constant(const irep_idt &id, const namespacet &ns) const; bool is_empty() const { diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index cd41c414c86..ed4ec5e21c1 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -4394,13 +4394,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment( class is_compile_time_constantt : public is_constantt { public: - explicit is_compile_time_constantt(const namespacet &ns) : ns(ns) + explicit is_compile_time_constantt(const namespacet &ns) : is_constantt(ns) { } protected: - const namespacet &ns; - bool is_constant(const exprt &e) const override { if(e.id() == ID_infinity) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 5db3567eb3b..c91d97d1e46 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -213,7 +213,7 @@ void code_contractst::check_apply_loop_contracts( // If the set contains pairs (i, a[i]), // we widen them to (i, __CPROVER_POINTER_OBJECT(a)) - widen_assigns(to_havoc); + widen_assigns(to_havoc, ns); log.debug() << "No loop assigns clause provided. Inferred targets: {"; // Add inferred targets to the loop assigns clause. diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 5570a62a194..e442b063eb7 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -247,11 +247,11 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) std::string::npos; } -void widen_assigns(assignst &assigns) +void widen_assigns(assignst &assigns, const namespacet &ns) { assignst result; - havoc_utils_is_constantt is_constant(assigns); + havoc_utils_is_constantt is_constant(assigns, ns); for(const auto &e : assigns) { diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 99595940b90..b1fd631f656 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -24,7 +24,7 @@ class havoc_if_validt : public havoc_utilst { public: havoc_if_validt(const assignst &mod, const namespacet &ns) - : havoc_utilst(mod), ns(ns) + : havoc_utilst(mod, ns), ns(ns) { } @@ -175,7 +175,7 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`, /// then replace it by the entire underlying object. Otherwise, e.g. for a[i] or /// *(b+i) when `i` is a known constant, keep the expression in the result. -void widen_assigns(assignst &assigns); +void widen_assigns(assignst &assigns, const namespacet &ns); /// This function recursively searches \p expression to find nested or /// non-nested quantified expressions. When a quantified expression is found, diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index 92e73cb68ac..1e4f768a5cd 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -27,11 +27,13 @@ class havoc_loopst havoc_loopst( function_assignst &_function_assigns, - goto_functiont &_goto_function) + goto_functiont &_goto_function, + const namespacet &ns) : goto_function(_goto_function), local_may_alias(_goto_function), function_assigns(_function_assigns), - natural_loops(_goto_function.body) + natural_loops(_goto_function.body), + ns(ns) { havoc_loops(); } @@ -41,6 +43,7 @@ class havoc_loopst local_may_aliast local_may_alias; function_assignst &function_assigns; natural_loops_mutablet natural_loops; + const namespacet &ns; typedef std::set assignst; typedef const natural_loops_mutablet::natural_loopt loopt; @@ -66,7 +69,7 @@ void havoc_loopst::havoc_loop( // build the havocking code goto_programt havoc_code; - havoc_utilst havoc_gen(assigns); + havoc_utilst havoc_gen(assigns, ns); havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code); // Now havoc at the loop head. Use insert_swap to @@ -118,5 +121,8 @@ void havoc_loops(goto_modelt &goto_model) function_assignst function_assigns(goto_model.goto_functions); for(auto &gf_entry : goto_model.goto_functions.function_map) - havoc_loopst(function_assigns, gf_entry.second); + { + havoc_loopst( + function_assigns, gf_entry.second, namespacet{goto_model.symbol_table}); + } } diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h index 19a0ca57815..e5b425c9996 100644 --- a/src/goto-instrument/havoc_utils.h +++ b/src/goto-instrument/havoc_utils.h @@ -27,7 +27,8 @@ typedef std::set assignst; class havoc_utils_is_constantt : public is_constantt { public: - explicit havoc_utils_is_constantt(const assignst &mod) : assigns(mod) + explicit havoc_utils_is_constantt(const assignst &mod, const namespacet &ns) + : is_constantt(ns), assigns(mod) { } @@ -48,7 +49,8 @@ class havoc_utils_is_constantt : public is_constantt class havoc_utilst { public: - explicit havoc_utilst(const assignst &mod) : assigns(mod), is_constant(mod) + explicit havoc_utilst(const assignst &mod, const namespacet &ns) + : assigns(mod), is_constant(mod, ns) { } diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index 531e3f4f04e..d85c8fcd3d5 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -28,14 +28,16 @@ class k_inductiont goto_functiont &_goto_function, bool _base_case, bool _step_case, - unsigned _k) + unsigned _k, + const namespacet &ns) : function_id(_function_id), goto_function(_goto_function), local_may_alias(_goto_function), natural_loops(_goto_function.body), base_case(_base_case), step_case(_step_case), - k(_k) + k(_k), + ns(ns) { k_induction(); } @@ -49,6 +51,8 @@ class k_inductiont const bool base_case, step_case; const unsigned k; + const namespacet &ns; + void k_induction(); void process_loop( @@ -97,7 +101,7 @@ void k_inductiont::process_loop( // build the havocking code goto_programt havoc_code; - havoc_utilst havoc_gen(assigns); + havoc_utilst havoc_gen(assigns, ns); havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code); // unwind to get k+1 copies @@ -165,5 +169,13 @@ void k_induction( unsigned k) { for(auto &gf_entry : goto_model.goto_functions.function_map) - k_inductiont(gf_entry.first, gf_entry.second, base_case, step_case, k); + { + k_inductiont( + gf_entry.first, + gf_entry.second, + base_case, + step_case, + k, + namespacet{goto_model.symbol_table}); + } } diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index 6f994f82cf3..38ec76b31d7 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -91,7 +91,7 @@ void goto_statet::apply_condition( if(is_ssa_expr(rhs)) std::swap(lhs, rhs); - if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs)) + if(is_ssa_expr(lhs) && goto_symex_is_constantt(ns)(rhs)) { const ssa_exprt &ssa_lhs = to_ssa_expr(lhs); INVARIANT( @@ -141,7 +141,7 @@ void goto_statet::apply_condition( if(is_ssa_expr(rhs)) std::swap(lhs, rhs); - if(!is_ssa_expr(lhs) || !goto_symex_is_constantt()(rhs)) + if(!is_ssa_expr(lhs) || !goto_symex_is_constantt(ns)(rhs)) return; if(rhs.is_true()) diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_is_constant.h index d76e3e19c69..50f9e08e48e 100644 --- a/src/goto-symex/goto_symex_is_constant.h +++ b/src/goto-symex/goto_symex_is_constant.h @@ -17,6 +17,11 @@ Author: Michael Tautschig, tautschn@amazon.com class goto_symex_is_constantt : public is_constantt { +public: + explicit goto_symex_is_constantt(const namespacet &ns) : is_constantt(ns) + { + } + protected: bool is_constant(const exprt &expr) const override { diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 670f94bfa02..de2856b0807 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -110,7 +110,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()(rhs)) + if(!is_shared && record_value && goto_symex_is_constantt(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 22b94528e68..8e4e7a335ae 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -204,7 +204,7 @@ static optionalt> try_evaluate_pointer_comparison( if(!symbol_expr_lhs) return {}; - if(!goto_symex_is_constantt()(rhs)) + if(!goto_symex_is_constantt(ns)(rhs)) return {}; return try_evaluate_pointer_comparison( diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 20de36077f4..ead31db6ee9 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -9,12 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" #include "arith_tools.h" +#include "bitvector_expr.h" +#include "byte_operators.h" #include "c_types.h" #include "config.h" #include "expr_iterator.h" #include "namespace.h" #include "pointer_expr.h" -#include "std_expr.h" +#include "pointer_offset_size.h" #include #include @@ -238,7 +240,6 @@ bool is_constantt::is_constant(const exprt &expr) const 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 || - // byte_update works, byte_extract may be out-of-bounds expr.id() == ID_byte_update_big_endian || expr.id() == ID_byte_update_little_endian) { @@ -247,6 +248,46 @@ bool is_constantt::is_constant(const exprt &expr) const return is_constant(e); }); } + else if(auto be = expr_try_dynamic_cast(expr)) + { + if(!is_constant(be->op()) || !be->offset().is_constant()) + return false; + + const auto op_bits = pointer_offset_bits(be->op().type(), ns); + if(!op_bits.has_value()) + return false; + + const auto extract_bits = pointer_offset_bits(be->type(), ns); + if(!extract_bits.has_value()) + return false; + + const mp_integer offset_bits = + numeric_cast_v(to_constant_expr(be->offset())) * + be->get_bits_per_byte(); + + return offset_bits + *extract_bits <= *op_bits; + } + else if(auto eb = expr_try_dynamic_cast(expr)) + { + if( + !is_constant(eb->src()) || !eb->lower().is_constant() || + !eb->upper().is_constant()) + { + return false; + } + + const auto src_bits = pointer_offset_bits(eb->src().type(), ns); + if(!src_bits.has_value()) + return false; + + const mp_integer lower_bound = + numeric_cast_v(to_constant_expr(eb->lower())); + const mp_integer upper_bound = + numeric_cast_v(to_constant_expr(eb->upper())); + + return lower_bound >= 0 && lower_bound <= upper_bound && + upper_bound < src_bits; + } return false; } diff --git a/src/util/expr_util.h b/src/util/expr_util.h index 2a6044083b7..3b31c1de156 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -88,6 +88,10 @@ const exprt &skip_typecast(const exprt &expr); class is_constantt { public: + explicit is_constantt(const namespacet &ns) : ns(ns) + { + } + /// returns true iff the expression can be considered constant bool operator()(const exprt &e) const { @@ -95,6 +99,8 @@ class is_constantt } protected: + const namespacet &ns; + virtual bool is_constant(const exprt &) const; virtual bool is_constant_address_of(const exprt &) const; }; diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index 73661f0c7cd..0b0ca0fec6b 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -89,8 +89,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") { const auto &final_domain = constant_propagator[test_instruction]; - REQUIRE(final_domain.values.is_constant(local_x.symbol_expr())); - REQUIRE(final_domain.values.is_constant(local_y.symbol_expr())); + REQUIRE(final_domain.values.is_constant(local_x.symbol_expr(), ns)); + REQUIRE(final_domain.values.is_constant(local_y.symbol_expr(), ns)); } } @@ -103,8 +103,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") { const auto &final_domain = constant_propagator[test_instruction]; - REQUIRE(final_domain.values.is_constant(local_x.symbol_expr())); - REQUIRE(!final_domain.values.is_constant(local_y.symbol_expr())); + REQUIRE(final_domain.values.is_constant(local_x.symbol_expr(), ns)); + REQUIRE(!final_domain.values.is_constant(local_y.symbol_expr(), ns)); } } } @@ -181,8 +181,9 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") { const auto &final_domain = constant_propagator[test_instruction]; - REQUIRE(final_domain.values.is_constant(bool_local.symbol_expr())); - REQUIRE(final_domain.values.is_constant(c_bool_local.symbol_expr())); + REQUIRE(final_domain.values.is_constant(bool_local.symbol_expr(), ns)); + REQUIRE( + final_domain.values.is_constant(c_bool_local.symbol_expr(), ns)); } } } @@ -332,7 +333,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") { exprt bool_local = bool_locals[i].symbol_expr(); - REQUIRE(final_domain.values.is_constant(bool_local)); + REQUIRE(final_domain.values.is_constant(bool_local, ns)); final_domain.values.replace_const.replace(bool_local); @@ -349,7 +350,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") { exprt c_bool_local = c_bool_locals[i].symbol_expr(); - REQUIRE(final_domain.values.is_constant(c_bool_local)); + REQUIRE(final_domain.values.is_constant(c_bool_local, ns)); final_domain.values.replace_const.replace(c_bool_local); diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp index 5ffa64f1e29..435427e4712 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -6,21 +6,25 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include - -#include - #include +#include #include +#include + +#include +#include SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") { + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + signedbv_typet int_type(32); constant_exprt sizeof_constant("4", int_type); sizeof_constant.set(ID_C_c_sizeof_type, int_type); symbol_exprt non_constant("x", int_type); - goto_symex_is_constantt is_constant; + goto_symex_is_constantt is_constant(ns); GIVEN("Sizeof expression multiplied by a non-constant") {