From e68aefa80afb6157aed7fbf5573059e91f3c0b6d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 8 Dec 2022 23:48:58 +0000 Subject: [PATCH 1/3] r/w/rw_ok and pointer_in_range depend on deallocated and dead_object The evaluation of these expressions depends on the specific values of __CPROVER_deallocated and __CPROVER_dead_object at the time the expression is used. Therefore, create new prophecy_* variants of these expressions to retain the properties expected of an expression (as opposed to a statement/function call). These prophecy_* expressions can safely be passed on to back-ends, be simplified, and do not need to be rewritten during instrumentation. For now, they are just handled by lowering the expressions (in the SAT and SMT back-ends). We may, in future, decide to have back-end specific (and possibly more efficient) handling of these. --- .../test.desc | 2 +- .../test.desc | 2 +- src/ansi-c/expr2c.cpp | 53 ++++ src/ansi-c/expr2c_class.h | 5 + src/ansi-c/goto_check_c.cpp | 3 + src/cprover/state_encoding.cpp | 14 + .../contracts/instrument_spec_assigns.cpp | 10 +- src/goto-instrument/contracts/utils.cpp | 6 +- src/goto-programs/builtin_functions.cpp | 5 +- src/goto-programs/goto_clean_expr.cpp | 36 +++ src/solvers/flattening/bv_pointers.cpp | 13 + src/solvers/smt2/smt2_conv.cpp | 24 ++ .../smt2_incremental/convert_expr_to_smt.cpp | 30 ++ .../smt2_incremental_decision_procedure.cpp | 25 +- src/util/irep_ids.def | 4 + src/util/pointer_expr.cpp | 27 ++ src/util/pointer_expr.h | 273 ++++++++++++++++++ src/util/simplify_expr.cpp | 12 + src/util/simplify_expr_class.h | 10 + src/util/simplify_expr_pointer.cpp | 20 ++ 20 files changed, 565 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc index e47d8a997b3..f9e2f4ce61b 100644 --- a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc +++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc @@ -1,7 +1,7 @@ CORE new-smt-backend test.c --malloc-may-fail --malloc-fail-null -^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$ +^\[free.precondition.\d+] line \d+ double free: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc index a70db820b5a..4c07a4c52ba 100644 --- a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc +++ b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc @@ -4,7 +4,7 @@ test.c ^EXIT=0$ ^SIGNAL=0$ Checking assertions -^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS +^\[free.precondition.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS -- Invariant check failed -- diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 9578d6d7376..dcf84fcfdde 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3572,6 +3572,26 @@ std::string expr2ct::convert_r_or_w_ok(const r_or_w_ok_exprt &src) return dest; } +std::string +expr2ct::convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src) +{ + // we hide prophecy expressions in C-style output + std::string dest = src.id() == ID_prophecy_r_ok ? "R_OK" + : src.id() == ID_prophecy_w_ok ? "W_OK" + : "RW_OK"; + + dest += '('; + + unsigned p; + dest += convert_with_precedence(src.pointer(), p); + dest += ", "; + dest += convert_with_precedence(src.size(), p); + + dest += ')'; + + return dest; +} + std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src) { std::string dest = CPROVER_PREFIX "pointer_in_range"; @@ -3590,6 +3610,26 @@ std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src) return dest; } +std::string expr2ct::convert_prophecy_pointer_in_range( + const prophecy_pointer_in_range_exprt &src) +{ + // we hide prophecy expressions in C-style output + std::string dest = CPROVER_PREFIX "pointer_in_range"; + + dest += '('; + + unsigned p; + dest += convert_with_precedence(src.lower_bound(), p); + dest += ", "; + dest += convert_with_precedence(src.pointer(), p); + dest += ", "; + dest += convert_with_precedence(src.upper_bound(), p); + + dest += ')'; + + return dest; +} + std::string expr2ct::convert_with_precedence( const exprt &src, unsigned &precedence) @@ -4002,9 +4042,22 @@ std::string expr2ct::convert_with_precedence( else if(src.id() == ID_r_ok || src.id() == ID_w_ok || src.id() == ID_rw_ok) return convert_r_or_w_ok(to_r_or_w_ok_expr(src)); + else if( + auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(src)) + { + return convert_prophecy_r_or_w_ok(*prophecy_r_or_w_ok); + } + else if(src.id() == ID_pointer_in_range) return convert_pointer_in_range(to_pointer_in_range_expr(src)); + else if(src.id() == ID_prophecy_pointer_in_range) + { + return convert_prophecy_pointer_in_range( + to_prophecy_pointer_in_range_expr(src)); + } + auto function_string_opt = convert_function(src); if(function_string_opt.has_value()) return *function_string_opt; diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 2a09024a7de..07d73975a3f 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -28,6 +28,8 @@ class qualifierst; class namespacet; class r_or_w_ok_exprt; class pointer_in_range_exprt; +class prophecy_r_or_w_ok_exprt; +class prophecy_pointer_in_range_exprt; class expr2ct { @@ -285,7 +287,10 @@ class expr2ct std::string convert_bitreverse(const bitreverse_exprt &src); std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src); + std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src); std::string convert_pointer_in_range(const pointer_in_range_exprt &src); + std::string + convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src); }; #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index b051a09f244..1ec029f3ff7 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1444,6 +1444,8 @@ void goto_check_ct::pointer_primitive_check( const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok) ? to_r_or_w_ok_expr(expr).pointer() + : can_cast_expr(expr) + ? to_prophecy_r_or_w_ok_expr(expr).pointer() : to_unary_expr(expr).op(); CHECK_RETURN(pointer.type().id() == ID_pointer); @@ -1484,6 +1486,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr) // will equally be non-deterministic. return can_cast_expr(expr) || expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok || + can_cast_expr(expr) || expr.id() == ID_is_dynamic_object; } diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 2ea684d7fae..8a124afa06e 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -294,6 +294,20 @@ exprt state_encodingt::evaluate_expr_rec( : ID_state_rw_ok; return ternary_exprt(new_id, state, pointer, size, what.type()); } + else if( + const auto r_or_w_ok_expr = + expr_try_dynamic_cast(what)) + { + // we replace prophecy expressions by our state + auto pointer = + evaluate_expr_rec(loc, state, r_or_w_ok_expr->pointer(), bound_symbols); + auto size = + evaluate_expr_rec(loc, state, r_or_w_ok_expr->size(), bound_symbols); + auto new_id = what.id() == ID_prophecy_r_ok ? ID_state_r_ok + : what.id() == ID_prophecy_w_ok ? ID_state_w_ok + : ID_state_rw_ok; + return ternary_exprt(new_id, state, pointer, size, what.type()); + } else if(what.id() == ID_is_cstring) { // we need to add the state diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index e941c0732d3..03f76c16ba6 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -644,9 +644,13 @@ exprt instrument_spec_assignst::target_validity_expr( // (or is NULL if we allow it explicitly). // This assertion will be falsified whenever `start_address` is invalid or // not of the right size (or is NULL if we do not allow it explicitly). - auto result = - or_exprt{not_exprt{car.condition()}, - w_ok_exprt{car.target_start_address(), car.target_size()}}; + symbol_exprt deallocated = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + auto result = or_exprt{ + not_exprt{car.condition()}, + prophecy_w_ok_exprt{ + car.target_start_address(), car.target_size(), deallocated, dead}}; if(allow_null_target) result.add_to_operands(null_object(car.target_start_address())); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 3e2eb26326f..01bac940fef 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -178,7 +178,11 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) const auto size_of_expr_opt = size_of_expr(expr.type(), ns); CHECK_RETURN(size_of_expr_opt.has_value()); - validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt}); + symbol_exprt deallocated = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + validity_checks.push_back(prophecy_r_ok_exprt{ + deref->pointer(), *size_of_expr_opt, deallocated, dead}); } for(const auto &op : expr.operands()) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index b5a049f2d81..2916a611bcd 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -669,7 +669,10 @@ void goto_convertt::do_havoc_slice( // char nondet_contents[argument[1]]; // __CPROVER_array_replace(p, nondet_contents); - r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]); + symbol_exprt deallocated = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + prophecy_w_ok_exprt ok_expr{arguments[0], arguments[1], deallocated, dead}; ok_expr.add_source_location() = source_location; source_locationt annotated_location = source_location; annotated_location.set("user-provided", false); diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 737c5205fc5..1bb8c1c579f 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" +#include #include #include #include @@ -73,6 +74,15 @@ bool goto_convertt::needs_cleaning(const exprt &expr) return true; } + // Rewrite rw_ok and pointer_in_range front-end expressions into ones + // including prophecy expressions. + if( + can_cast_expr(expr) || + can_cast_expr(expr)) + { + return true; + } + // We can't flatten quantified expressions by introducing new literals for // conditional expressions. This is because the body of the quantified // may refer to bound variables, which are not visible outside the scope @@ -436,6 +446,32 @@ void goto_convertt::clean_expr( expr.operands().size() == 1, "ID_compound_literal has a single operand"); expr = to_unary_expr(expr).op(); } + else if(auto r_or_w_ok = expr_try_dynamic_cast(expr)) + { + const auto &id = expr.id(); + expr = + prophecy_r_or_w_ok_exprt{ + id == ID_r_ok ? ID_prophecy_r_ok + : id == ID_w_ok ? ID_prophecy_w_ok + : ID_prophecy_rw_ok, + r_or_w_ok->pointer(), + r_or_w_ok->size(), + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} + .with_source_location(expr); + } + else if( + auto pointer_in_range = expr_try_dynamic_cast(expr)) + { + expr = + prophecy_pointer_in_range_exprt{ + pointer_in_range->lower_bound(), + pointer_in_range->pointer(), + pointer_in_range->upper_bound(), + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} + .with_source_location(expr); + } } void goto_convertt::clean_expr_address_of( diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 09973306a93..be28f5eef2e 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include /// Map bytes according to the configured endianness. The key difference to /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level @@ -204,6 +205,18 @@ literalt bv_pointerst::convert_rest(const exprt &expr) bv_utilst::representationt::UNSIGNED)); } } + else if( + auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(expr)) + { + return convert(simplify_expr(prophecy_r_or_w_ok->lower(ns), ns)); + } + else if( + auto prophecy_pointer_in_range = + expr_try_dynamic_cast(expr)) + { + return convert(simplify_expr(prophecy_pointer_in_range->lower(ns), ns)); + } return SUB::convert_rest(expr); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2cb65bcff1e..0f04d0ce6f3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4864,6 +4864,30 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr) !has_byte_operator(lowered_expr), "lower_byte_operators should remove all byte operators"); + // Perform rewrites that may introduce new symbols + for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end(); + it != itend;) // no ++it + { + if( + auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(*it)) + { + exprt lowered = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns); + it.mutate() = lowered; + it.next_sibling_or_parent(); + } + else if( + auto prophecy_pointer_in_range = + expr_try_dynamic_cast(*it)) + { + exprt lowered = simplify_expr(prophecy_pointer_in_range->lower(ns), ns); + it.mutate() = lowered; + it.next_sibling_or_parent(); + } + else + ++it; + } + // Now create symbols for all composite expressions present in lowered_expr: find_symbols(lowered_expr); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 5f0a97ad98e..45bd6fd79f3 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1463,6 +1463,24 @@ static smt_termt convert_expr_to_smt( count_trailing_zeros.pretty()); } +static smt_termt convert_expr_to_smt( + const prophecy_r_or_w_ok_exprt &prophecy_r_or_w_ok, + const sub_expression_mapt &converted) +{ + UNREACHABLE_BECAUSE( + "prophecy_r_or_w_ok expression should have been lowered by the decision " + "procedure before conversion to smt terms"); +} + +static smt_termt convert_expr_to_smt( + const prophecy_pointer_in_range_exprt &prophecy_pointer_in_range, + const sub_expression_mapt &converted) +{ + UNREACHABLE_BECAUSE( + "prophecy_pointer_in_range expression should have been lowered by the " + "decision procedure before conversion to smt terms"); +} + static smt_termt dispatch_expr_to_smt_conversion( const exprt &expr, const sub_expression_mapt &converted, @@ -1798,6 +1816,18 @@ static smt_termt dispatch_expr_to_smt_conversion( { return convert_expr_to_smt(*count_trailing_zeros, converted); } + if( + const auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*prophecy_r_or_w_ok, converted); + } + if( + const auto prophecy_pointer_in_range = + expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*prophecy_pointer_in_range, converted); + } UNIMPLEMENTED_FEATURE( "Generation of SMT formula for unknown kind of expression: " + diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 16b26ce3a3f..29a873e60d0 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -7,6 +7,7 @@ #include #include #include +#include #include #include #include @@ -273,6 +274,25 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret( solver_process->send(is_dynamic_object_function.declaration); } +static exprt lower_rw_ok_pointer_in_range(exprt expr, const namespacet &ns) +{ + expr.visit_pre([&ns](exprt &expr) { + if( + auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(expr)) + { + expr = simplify_expr(prophecy_r_or_w_ok->lower(ns), ns); + } + else if( + auto prophecy_pointer_in_range = + expr_try_dynamic_cast(expr)) + { + expr = simplify_expr(prophecy_pointer_in_range->lower(ns), ns); + } + }); + return expr; +} + void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( const exprt &in_expr) { @@ -623,8 +643,9 @@ void smt2_incremental_decision_proceduret::define_object_properties() exprt smt2_incremental_decision_proceduret::lower(exprt expression) const { - const exprt lowered = struct_encoding.encode( - lower_enum(lower_byte_operators(expression, ns), ns)); + const exprt lowered = struct_encoding.encode(lower_enum( + lower_byte_operators(lower_rw_ok_pointer_in_range(expression, ns), ns), + ns)); log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { if(lowered != expression) debug << "lowered to -\n " << lowered.pretty(2, 0) << messaget::eom; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e66f620b755..3fc64bc77e3 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -904,6 +904,10 @@ IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-) IREP_ID_ONE(field_sensitive_ssa) IREP_ID_ONE(checked_assigns) IREP_ID_ONE(enum_is_in_range) +IREP_ID_ONE(prophecy_rw_ok) +IREP_ID_ONE(prophecy_r_ok) +IREP_ID_ONE(prophecy_w_ok) +IREP_ID_ONE(prophecy_pointer_in_range) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp index 38a3af19039..939cd04b6cb 100644 --- a/src/util/pointer_expr.cpp +++ b/src/util/pointer_expr.cpp @@ -238,3 +238,30 @@ exprt pointer_in_range_exprt::lower() const binary_relation_exprt( pointer_offset(op1()), ID_le, pointer_offset(op2()))}); } + +exprt prophecy_r_or_w_ok_exprt::lower(const namespacet &ns) const +{ + return and_exprt{ + {not_exprt{null_object(pointer())}, + not_exprt{is_invalid_pointer_exprt{pointer()}}, + not_exprt{same_object(pointer(), deallocated_ptr())}, + not_exprt{same_object(pointer(), dead_ptr())}, + not_exprt{object_lower_bound(pointer(), nil_exprt())}, + not_exprt{object_upper_bound(pointer(), size())}}}; +} + +exprt prophecy_pointer_in_range_exprt::lower(const namespacet &ns) const +{ + return and_exprt{ + {same_object(op0(), op1()), + same_object(op1(), op2()), + prophecy_r_ok_exprt( + op0(), + minus_exprt(pointer_offset(op2()), pointer_offset(op0())), + deallocated_ptr(), + dead_ptr()) + .lower(ns), + binary_relation_exprt(pointer_offset(op0()), ID_le, pointer_offset(op1())), + binary_relation_exprt( + pointer_offset(op1()), ID_le, pointer_offset(op2()))}}; +} diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h index baface3794d..d3130b3110c 100644 --- a/src/util/pointer_expr.h +++ b/src/util/pointer_expr.h @@ -447,6 +447,94 @@ inline pointer_in_range_exprt &to_pointer_in_range_expr(exprt &expr) return static_cast(expr); } +/// pointer_in_range (see \ref pointer_in_range_exprt) with prophecy expressions +/// to encode whether a pointer refers to a deallocated or out-of-scope object. +class prophecy_pointer_in_range_exprt : public expr_protectedt +{ +public: + prophecy_pointer_in_range_exprt( + exprt a, + exprt b, + exprt c, + exprt is_deallocated, + exprt is_dead) + : expr_protectedt( + ID_prophecy_pointer_in_range, + bool_typet{}, + {std::move(a), + std::move(b), + std::move(c), + std::move(is_deallocated), + std::move(is_dead)}) + { + PRECONDITION(op0().type().id() == ID_pointer); + PRECONDITION(op1().type().id() == ID_pointer); + PRECONDITION(op2().type().id() == ID_pointer); + } + + const exprt &lower_bound() const + { + return op0(); + } + + const exprt &pointer() const + { + return op1(); + } + + const exprt &upper_bound() const + { + return op2(); + } + + const exprt &deallocated_ptr() const + { + return op3(); + } + + const exprt &dead_ptr() const + { + return operands()[4]; + } + + // translate into equivalent conjunction + exprt lower(const namespacet &ns) const; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_prophecy_pointer_in_range; +} + +inline void validate_expr(const prophecy_pointer_in_range_exprt &value) +{ + validate_operands( + value, 5, "prophecy_pointer_in_range must have five operands"); +} + +inline const prophecy_pointer_in_range_exprt & +to_prophecy_pointer_in_range_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_prophecy_pointer_in_range); + DATA_INVARIANT( + expr.operands().size() == 5, + "prophecy_pointer_in_range must have five operands"); + return static_cast(expr); +} + +/// \copydoc to_prophecy_pointer_in_range_expr(const exprt &) +/// \ingroup gr_std_expr +inline prophecy_pointer_in_range_exprt & +to_prophecy_pointer_in_range_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_prophecy_pointer_in_range); + DATA_INVARIANT( + expr.operands().size() == 5, + "prophecy_pointer_in_range must have five operands"); + return static_cast(expr); +} + /// \brief Operator to return the address of an object class address_of_exprt : public unary_exprt { @@ -925,6 +1013,191 @@ inline const w_ok_exprt &to_w_ok_expr(const exprt &expr) return ret; } +/// \brief A base class for a predicate that indicates that an +/// address range is ok to read or write or both +class prophecy_r_or_w_ok_exprt : public expr_protectedt +{ +public: + prophecy_r_or_w_ok_exprt( + irep_idt id, + exprt pointer, + exprt size, + exprt is_deallocated, + exprt is_dead) + : expr_protectedt( + id, + bool_typet{}, + {std::move(pointer), + std::move(size), + std::move(is_deallocated), + std::move(is_dead)}) + { + } + + prophecy_r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size) + : prophecy_r_or_w_ok_exprt( + id, + std::move(pointer), + std::move(size), + nil_exprt{}, + nil_exprt{}) + { + } + + const exprt &pointer() const + { + return op0(); + } + + const exprt &size() const + { + return op1(); + } + + const exprt &deallocated_ptr() const + { + return op2(); + } + + exprt &deallocated_ptr() + { + return op2(); + } + + const exprt &dead_ptr() const + { + return op3(); + } + + exprt &dead_ptr() + { + return op3(); + } + + /// Lower an r_or_w_ok_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower(const namespacet &ns) const; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_prophecy_r_ok || base.id() == ID_prophecy_w_ok || + base.id() == ID_prophecy_rw_ok; +} + +inline void validate_expr(const prophecy_r_or_w_ok_exprt &value) +{ + validate_operands(value, 4, "r_or_w_ok must have four operands"); +} + +inline const prophecy_r_or_w_ok_exprt & +to_prophecy_r_or_w_ok_expr(const exprt &expr) +{ + PRECONDITION( + expr.id() == ID_prophecy_r_ok || expr.id() == ID_prophecy_w_ok || + expr.id() == ID_prophecy_rw_ok); + auto &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \brief A predicate that indicates that an address range is ok to read +class prophecy_r_ok_exprt : public prophecy_r_or_w_ok_exprt +{ +public: + prophecy_r_ok_exprt( + exprt pointer, + exprt size, + exprt is_deallocated, + exprt is_dead) + : prophecy_r_or_w_ok_exprt( + ID_prophecy_r_ok, + std::move(pointer), + std::move(size), + std::move(is_deallocated), + std::move(is_dead)) + { + } + + prophecy_r_ok_exprt(exprt pointer, exprt size) + : prophecy_r_ok_exprt( + std::move(pointer), + std::move(size), + nil_exprt{}, + nil_exprt{}) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_prophecy_r_ok; +} + +inline void validate_expr(const prophecy_r_ok_exprt &value) +{ + validate_operands(value, 4, "r_ok must have four operands"); +} + +inline const prophecy_r_ok_exprt &to_prophecy_r_ok_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_prophecy_r_ok); + const prophecy_r_ok_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \brief A predicate that indicates that an address range is ok to write +class prophecy_w_ok_exprt : public prophecy_r_or_w_ok_exprt +{ +public: + prophecy_w_ok_exprt( + exprt pointer, + exprt size, + exprt is_deallocated, + exprt is_dead) + : prophecy_r_or_w_ok_exprt( + ID_prophecy_w_ok, + std::move(pointer), + std::move(size), + std::move(is_deallocated), + std::move(is_dead)) + { + } + + prophecy_w_ok_exprt(exprt pointer, exprt size) + : prophecy_w_ok_exprt( + std::move(pointer), + std::move(size), + nil_exprt{}, + nil_exprt{}) + { + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_prophecy_w_ok; +} + +inline void validate_expr(const prophecy_w_ok_exprt &value) +{ + validate_operands(value, 4, "w_ok must have four operands"); +} + +inline const prophecy_w_ok_exprt &to_prophecy_w_ok_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_prophecy_w_ok); + const prophecy_w_ok_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + /// \brief Pointer-typed bitvector constant annotated with the pointer /// expression that the bitvector is the numeric representation of. /// This variation of a constant expression is only used in the context of a diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 5c62282d74b..428bda505dc 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2993,6 +2993,18 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_bitreverse(to_bitreverse_expr(expr)); } + else if( + const auto prophecy_r_or_w_ok = + expr_try_dynamic_cast(expr)) + { + r = simplify_prophecy_r_or_w_ok(*prophecy_r_or_w_ok); + } + else if( + const auto prophecy_pointer_in_range = + expr_try_dynamic_cast(expr)) + { + r = simplify_prophecy_pointer_in_range(*prophecy_pointer_in_range); + } if(!no_change_join_operands) r = changed(r); diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index f1ecb47e4a4..5e834c35421 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -65,6 +65,8 @@ class plus_exprt; class pointer_object_exprt; class pointer_offset_exprt; class popcount_exprt; +class prophecy_pointer_in_range_exprt; +class prophecy_r_or_w_ok_exprt; class refined_string_exprt; class shift_exprt; class sign_exprt; @@ -228,6 +230,14 @@ class simplify_exprt /// Try to simplify find-first-set to a constant expression. NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &); + /// Try to simplify prophecy_{r,w,rw}_ok to a constant expression. + NODISCARD resultt<> + simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &); + + /// Try to simplify prophecy_pointer_in_range to a constant expression. + NODISCARD resultt<> + simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &); + // auxiliary bool simplify_if_implies( exprt &expr, const exprt &cond, bool truth, bool &new_truth); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index c774d5c3bbe..1334d4e645f 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -692,3 +692,23 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr) else return std::move(new_expr); } + +simplify_exprt::resultt<> simplify_exprt::simplify_prophecy_r_or_w_ok( + const prophecy_r_or_w_ok_exprt &expr) +{ + exprt new_expr = simplify_rec(expr.lower(ns)); + if(!new_expr.is_constant()) + return unchanged(expr); + else + return std::move(new_expr); +} + +simplify_exprt::resultt<> simplify_exprt::simplify_prophecy_pointer_in_range( + const prophecy_pointer_in_range_exprt &expr) +{ + exprt new_expr = simplify_rec(expr.lower(ns)); + if(!new_expr.is_constant()) + return unchanged(expr); + else + return std::move(new_expr); +} From a699145bae2fcac01b5eb1bb88f4a8d411a5e374 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 8 Dec 2022 20:46:55 +0000 Subject: [PATCH 2/3] Remove {r,w,rw}_ok and pointer_in_range expansion from C front-end These expressions are now rewritten to their prophecy_* counterparts by goto-program conversion, and back-ends directly handle these prophecy_* expressions. Unconditional rewrites by goto_check_ct (even when no checks are enabled) are no longer necessary. Fixes: #7377 --- src/ansi-c/goto_check_c.cpp | 59 ------------------------------------- 1 file changed, 59 deletions(-) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 1ec029f3ff7..26e437195b9 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -228,7 +228,6 @@ class goto_check_ct void conversion_check(const exprt &, const guardt &); void float_overflow_check(const exprt &, const guardt &); void nan_check(const exprt &, const guardt &); - optionalt expand_pointer_checks(exprt); std::string array_name(const exprt &); @@ -1995,62 +1994,6 @@ void goto_check_ct::check(const exprt &expr) check_rec(expr, identity); } -/// expand the r_ok, w_ok, rw_ok, pointer_in_range predicates -optionalt goto_check_ct::expand_pointer_checks(exprt expr) -{ - bool modified = false; - - for(auto &op : expr.operands()) - { - auto op_result = expand_pointer_checks(op); - if(op_result.has_value()) - { - op = *op_result; - modified = true; - } - } - - if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok) - { - // these get an address as first argument and a size as second - DATA_INVARIANT( - expr.operands().size() == 2, "r/w_ok must have two operands"); - - const auto conditions = get_pointer_dereferenceable_conditions( - to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size()); - - exprt::operandst conjuncts; - - for(const auto &c : conditions) - conjuncts.push_back(c.assertion); - - exprt c = conjunction(conjuncts); - if(enable_simplify) - simplify(c, ns); - return c; - } - else if(expr.id() == ID_pointer_in_range) - { - const auto &pointer_in_range_expr = to_pointer_in_range_expr(expr); - - auto expanded = pointer_in_range_expr.lower(); - - // rec. call - auto expanded_rec_opt = expand_pointer_checks(expanded); - if(expanded_rec_opt.has_value()) - expanded = *expanded_rec_opt; - - if(enable_simplify) - simplify(expanded, ns); - - return expanded; - } - else if(modified) - return std::move(expr); - else - return {}; -} - void goto_check_ct::memory_leak_check(const irep_idt &function_id) { const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak"); @@ -2270,8 +2213,6 @@ void goto_check_ct::goto_check( } } - i.transform([this](exprt expr) { return expand_pointer_checks(expr); }); - for(auto &instruction : new_code.instructions) { if(instruction.source_location().is_nil()) From e26121765200015838ef42054f1d55195a71cc25 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Aug 2023 10:08:56 +0000 Subject: [PATCH 3/3] Move rw_ok rewriting to separate pass This reverts selected changes from "r/w/rw_ok and pointer_in_range depend on deallocated and dead_object" for transformations of goto programs can now safely introduce rw_ok expressions into the goto program. Not all analyses, however, are able to cope with these expressions. Dependence graphs (and any analyses building upon these), for example, also require this rewriting. goto-instrument is adjusted accordingly. --- .../test.desc | 2 +- .../test.desc | 2 +- src/cbmc/cbmc_parse_options.cpp | 1 + src/cprover/state_encoding.cpp | 14 ---- .../goto_analyzer_parse_options.cpp | 1 + src/goto-diff/goto_diff_parse_options.cpp | 1 + .../contracts/instrument_spec_assigns.cpp | 10 +-- src/goto-instrument/contracts/utils.cpp | 6 +- .../goto_instrument_parse_options.cpp | 4 + src/goto-programs/Makefile | 1 + src/goto-programs/builtin_functions.cpp | 5 +- src/goto-programs/goto_clean_expr.cpp | 36 -------- src/goto-programs/process_goto_program.cpp | 4 + src/goto-programs/rewrite_rw_ok.cpp | 83 +++++++++++++++++++ src/goto-programs/rewrite_rw_ok.h | 27 ++++++ .../goto_synthesizer_parse_options.cpp | 1 + 16 files changed, 130 insertions(+), 68 deletions(-) create mode 100644 src/goto-programs/rewrite_rw_ok.cpp create mode 100644 src/goto-programs/rewrite_rw_ok.h diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc index f9e2f4ce61b..e47d8a997b3 100644 --- a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc +++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc @@ -1,7 +1,7 @@ CORE new-smt-backend test.c --malloc-may-fail --malloc-fail-null -^\[free.precondition.\d+] line \d+ double free: SUCCESS$ +^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc index 4c07a4c52ba..a70db820b5a 100644 --- a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc +++ b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc @@ -4,7 +4,7 @@ test.c ^EXIT=0$ ^SIGNAL=0$ Checking assertions -^\[free.precondition.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS +^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS -- Invariant check failed -- diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8867e612a83..882dbf4c13e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -406,6 +406,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) PARSE_OPTIONS_GOTO_TRACE(cmdline, options); // Options for process_goto_program + options.set_option("rewrite-rw-ok", true); options.set_option("rewrite-union", true); if(cmdline.isset("smt1")) diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 8a124afa06e..2ea684d7fae 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -294,20 +294,6 @@ exprt state_encodingt::evaluate_expr_rec( : ID_state_rw_ok; return ternary_exprt(new_id, state, pointer, size, what.type()); } - else if( - const auto r_or_w_ok_expr = - expr_try_dynamic_cast(what)) - { - // we replace prophecy expressions by our state - auto pointer = - evaluate_expr_rec(loc, state, r_or_w_ok_expr->pointer(), bound_symbols); - auto size = - evaluate_expr_rec(loc, state, r_or_w_ok_expr->size(), bound_symbols); - auto new_id = what.id() == ID_prophecy_r_ok ? ID_state_r_ok - : what.id() == ID_prophecy_w_ok ? ID_state_w_ok - : ID_state_rw_ok; - return ternary_exprt(new_id, state, pointer, size, what.type()); - } else if(what.id() == ID_is_cstring) { // we need to add the state diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 840621d0baf..b64119b6b9e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -393,6 +393,7 @@ int goto_analyzer_parse_optionst::doit() // Preserve backwards compatibility in processing options.set_option("partial-inline", true); + options.set_option("rewrite-rw-ok", false); options.set_option("rewrite-union", false); options.set_option("remove-returns", true); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 55a129324b9..b30a71df7d3 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -65,6 +65,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-properties", cmdline.isset("show-properties")); // Options for process_goto_program + options.set_option("rewrite-rw-ok", false); options.set_option("rewrite-union", true); } diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 03f76c16ba6..e941c0732d3 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -644,13 +644,9 @@ exprt instrument_spec_assignst::target_validity_expr( // (or is NULL if we allow it explicitly). // This assertion will be falsified whenever `start_address` is invalid or // not of the right size (or is NULL if we do not allow it explicitly). - symbol_exprt deallocated = - ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); - symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - auto result = or_exprt{ - not_exprt{car.condition()}, - prophecy_w_ok_exprt{ - car.target_start_address(), car.target_size(), deallocated, dead}}; + auto result = + or_exprt{not_exprt{car.condition()}, + w_ok_exprt{car.target_start_address(), car.target_size()}}; if(allow_null_target) result.add_to_operands(null_object(car.target_start_address())); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 01bac940fef..3e2eb26326f 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -178,11 +178,7 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) const auto size_of_expr_opt = size_of_expr(expr.type(), ns); CHECK_RETURN(size_of_expr_opt.has_value()); - symbol_exprt deallocated = - ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); - symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - validity_checks.push_back(prophecy_r_ok_exprt{ - deref->pointer(), *size_of_expr_opt, deallocated, dead}); + validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt}); } for(const auto &op : expr.operands()) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6d8bd441e7a..c58c6a7b3c4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -569,6 +570,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-reaching-definitions")) { do_indirect_call_and_rtti_removal(); + rewrite_rw_ok(goto_model); const namespacet ns(goto_model.symbol_table); reaching_definitions_analysist rd_analysis(ns); @@ -581,6 +583,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-dependence-graph")) { do_indirect_call_and_rtti_removal(); + rewrite_rw_ok(goto_model); const namespacet ns(goto_model.symbol_table); dependence_grapht dependence_graph(ns); @@ -1767,6 +1770,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() { do_indirect_call_and_rtti_removal(); do_remove_returns(); + rewrite_rw_ok(goto_model); log.warning() << "**** WARNING: Experimental option --full-slice, " << "analysis results may be unsound. See " diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 3d6a56f5416..f2557edc4c9 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -56,6 +56,7 @@ SRC = allocate_objects.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ restrict_function_pointers.cpp \ + rewrite_rw_ok.cpp \ rewrite_union.cpp \ resolve_inherited_component.cpp \ safety_checker.cpp \ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 2916a611bcd..b5a049f2d81 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -669,10 +669,7 @@ void goto_convertt::do_havoc_slice( // char nondet_contents[argument[1]]; // __CPROVER_array_replace(p, nondet_contents); - symbol_exprt deallocated = - ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); - symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - prophecy_w_ok_exprt ok_expr{arguments[0], arguments[1], deallocated, dead}; + r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]); ok_expr.add_source_location() = source_location; source_locationt annotated_location = source_location; annotated_location.set("user-provided", false); diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 1bb8c1c579f..737c5205fc5 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" -#include #include #include #include @@ -74,15 +73,6 @@ bool goto_convertt::needs_cleaning(const exprt &expr) return true; } - // Rewrite rw_ok and pointer_in_range front-end expressions into ones - // including prophecy expressions. - if( - can_cast_expr(expr) || - can_cast_expr(expr)) - { - return true; - } - // We can't flatten quantified expressions by introducing new literals for // conditional expressions. This is because the body of the quantified // may refer to bound variables, which are not visible outside the scope @@ -446,32 +436,6 @@ void goto_convertt::clean_expr( expr.operands().size() == 1, "ID_compound_literal has a single operand"); expr = to_unary_expr(expr).op(); } - else if(auto r_or_w_ok = expr_try_dynamic_cast(expr)) - { - const auto &id = expr.id(); - expr = - prophecy_r_or_w_ok_exprt{ - id == ID_r_ok ? ID_prophecy_r_ok - : id == ID_w_ok ? ID_prophecy_w_ok - : ID_prophecy_rw_ok, - r_or_w_ok->pointer(), - r_or_w_ok->size(), - ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), - ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} - .with_source_location(expr); - } - else if( - auto pointer_in_range = expr_try_dynamic_cast(expr)) - { - expr = - prophecy_pointer_in_range_exprt{ - pointer_in_range->lower_bound(), - pointer_in_range->pointer(), - pointer_in_range->upper_bound(), - ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), - ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} - .with_source_location(expr); - } } void goto_convertt::clean_expr_address_of( diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 57cbdd6115b..15341312159 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -23,6 +23,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include #include +#include #include #include #include @@ -70,6 +71,9 @@ bool process_goto_program( if(options.get_bool_option("rewrite-union")) rewrite_union(goto_model); + if(options.get_bool_option("rewrite-rw-ok")) + rewrite_rw_ok(goto_model); + // add generic checks log.status() << "Generic Property Instrumentation" << messaget::eom; goto_check_c(options, goto_model, log.get_message_handler()); diff --git a/src/goto-programs/rewrite_rw_ok.cpp b/src/goto-programs/rewrite_rw_ok.cpp new file mode 100644 index 00000000000..09433e5d8df --- /dev/null +++ b/src/goto-programs/rewrite_rw_ok.cpp @@ -0,0 +1,83 @@ +/*******************************************************************\ + +Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "rewrite_rw_ok.h" + +#include +#include + +#include + +static optionalt rewrite_rw_ok(exprt expr, const namespacet &ns) +{ + bool unchanged = true; + + for(auto it = expr.depth_begin(), itend = expr.depth_end(); + it != itend;) // no ++it + { + if(auto r_or_w_ok = expr_try_dynamic_cast(*it)) + { + const auto &id = it->id(); + exprt replacement = + prophecy_r_or_w_ok_exprt{ + id == ID_r_ok ? ID_prophecy_r_ok + : id == ID_w_ok ? ID_prophecy_w_ok + : ID_prophecy_rw_ok, + r_or_w_ok->pointer(), + r_or_w_ok->size(), + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} + .with_source_location(*it); + + it.mutate() = std::move(replacement); + unchanged = false; + it.next_sibling_or_parent(); + } + else if( + auto pointer_in_range = + expr_try_dynamic_cast(*it)) + { + exprt replacement = + prophecy_pointer_in_range_exprt{ + pointer_in_range->lower_bound(), + pointer_in_range->pointer(), + pointer_in_range->upper_bound(), + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(), + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()} + .with_source_location(*it); + + it.mutate() = std::move(replacement); + unchanged = false; + it.next_sibling_or_parent(); + } + else + ++it; + } + + if(unchanged) + return {}; + else + return std::move(expr); +} + +static void rewrite_rw_ok( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns) +{ + for(auto &instruction : goto_function.body.instructions) + instruction.transform( + [&ns](exprt expr) { return rewrite_rw_ok(expr, ns); }); +} + +void rewrite_rw_ok(goto_modelt &goto_model) +{ + const namespacet ns(goto_model.symbol_table); + + for(auto &gf_entry : goto_model.goto_functions.function_map) + rewrite_rw_ok(gf_entry.second, ns); +} diff --git a/src/goto-programs/rewrite_rw_ok.h b/src/goto-programs/rewrite_rw_ok.h new file mode 100644 index 00000000000..269ce9365a2 --- /dev/null +++ b/src/goto-programs/rewrite_rw_ok.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Rewrite r/w/rw_ok expressions to ones including prophecy variables recording +/// the state. + +#ifndef CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H +#define CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H + +class goto_modelt; + +/// Replace all occurrences of `r_ok_exprt`, `w_ok_exprt`, `rw_ok_exprt`, +/// `pointer_in_range_exprt` by their prophecy variants +/// `prophecy_r_or_w_ok_exprt` and `prophecy_pointer_in_range_exprt`, +/// respectively. +/// Each analysis may choose to natively support `r_ok_exprt` etc. (like +/// `cprover_parse_optionst` does) or may instead require the expression to be +/// lowered to other primitives (like `goto_symext`). +void rewrite_rw_ok(goto_modelt &); + +#endif // CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 72c1050aceb..5729c9c29b6 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -199,6 +199,7 @@ optionst goto_synthesizer_parse_optionst::get_options() options.set_option("depth", UINT32_MAX); options.set_option("exploration-strategy", "lifo"); options.set_option("symex-cache-dereferences", false); + options.set_option("rewrite-rw-ok", true); options.set_option("rewrite-union", true); options.set_option("self-loops-to-assumptions", true);