From 4f9b5cca482fb9e84b7e3538fe54f121795cde0e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 9 Nov 2022 14:03:59 -0600 Subject: [PATCH] CONTRACTS: add inductive checks for assigns clauses --- .../contracts/loop_assigns-02/test.desc | 4 +-- src/goto-instrument/contracts/contracts.cpp | 27 +++++++++++++------ .../contracts/instrument_spec_assigns.cpp | 20 +++++++++++--- .../contracts/instrument_spec_assigns.h | 8 ++++++ src/goto-instrument/havoc_utils.cpp | 9 ------- src/goto-instrument/havoc_utils.h | 6 ----- 6 files changed, 46 insertions(+), 28 deletions(-) diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc index 205356864ef..9c7e89e2add 100644 --- a/regression/contracts/loop_assigns-02/test.desc +++ b/regression/contracts/loop_assigns-02/test.desc @@ -5,9 +5,9 @@ main.c ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is inductively assignable: FAILURE$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ +^\*\* 1 of 12 failed \(2 iterations\) ^VERIFICATION FAILED$ -- -- diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 58512048d59..d0e329f72bc 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -89,10 +89,9 @@ void code_contractst::check_apply_loop_contracts( // // ... preamble ... // ,- initialize loop_entry history vars; - // | entered_loop = false - // loop assigns check | initial_invariant_val = invariant_expr; - // - unchecked, temps | in_base_case = true; - // func assigns check | snapshot (write_set); + // loop assigns check | entered_loop = false + // - unchecked, temps | initial_invariant_val = invariant_expr; + // func assigns check | in_base_case = true; // - disabled via pragma | goto HEAD; // | STEP: // --. | assert (initial_invariant_val); @@ -104,10 +103,12 @@ void code_contractst::check_apply_loop_contracts( // loop assigns check ,- ... eval guard ... // + assertions added | if (!guard) // func assigns check | goto EXIT; - // - disabled via pragma `- ... loop body ... + // - disabled via pragma | snapshot (write_set); + // `- ... loop body ... // ,- entered_loop = true // | if (in_base_case) // | goto STEP; + // | assert CAR_begin in CAR_end // loop assigns check | assert (invariant_expr); // - unchecked, temps | new_variant_val = decreases_clause_expr; // func assigns check | assert (new_variant_val < old_variant_val); @@ -256,9 +257,8 @@ void code_contractst::check_apply_loop_contracts( // Insert instrumentation // This must be done before havocing the write set. - // FIXME: this is not true for write set targets that - // might depend on other write set targets. - pre_loop_head_instrs.destructive_append(snapshot_instructions); + goto_function.body.destructive_insert( + std::next(loop_head), snapshot_instructions); // Insert a jump to the loop head // (skipping over the step case initialization code below) @@ -387,6 +387,17 @@ void code_contractst::check_apply_loop_contracts( pre_loop_end_instrs.add(goto_programt::make_goto( step_case_target, in_base_case, loop_head_location)); + // Adding checks that demonstrating that the loop assigns clause is an + // inductive invariant. + // CAR_begin should be included in CAR_end + goto_programt assigns_inductive_check_instrs; + for(const auto &target : to_havoc) + { + instrument_spec_assigns.check_inclusion_induction( + target, assigns_inductive_check_instrs); + pre_loop_end_instrs.destructive_append(assigns_inductive_check_instrs); + } + // The following code is only reachable in the step case, // i.e., when in_base_case == false, // because of the unconditional jump above. diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 2fc087e3a59..9741eed11fd 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -149,7 +149,17 @@ void instrument_spec_assignst::check_inclusion_assignment( // create temporary car but do not track const auto car = create_car_expr(true_exprt{}, lhs); create_snapshot(car, dest); - inclusion_check_assertion(car, false, true, dest); + inclusion_check_assertion(car, false, true, false, dest); +} + +void instrument_spec_assignst::check_inclusion_induction( + const exprt &lhs, + goto_programt &dest) const +{ + // create temporary car but do not track + const auto car = create_car_expr(true_exprt{}, lhs); + create_snapshot(car, dest); + inclusion_check_assertion(car, false, true, true, dest); } void instrument_spec_assignst::track_static_locals(goto_programt &dest) @@ -313,7 +323,7 @@ void instrument_spec_assignst:: create_snapshot(car, dest); // check inclusion, allowing null and not allowing stack allocated locals - inclusion_check_assertion(car, true, false, dest); + inclusion_check_assertion(car, true, false, false, dest); // invalidate aliases of the freed object invalidate_heap_and_spec_aliases(car, dest); @@ -680,6 +690,7 @@ void instrument_spec_assignst::inclusion_check_assertion( const car_exprt &car, bool allow_null_lhs, bool include_stack_allocated, + bool is_inductive_check, goto_programt &dest) const { source_locationt source_location(car.source_location()); @@ -705,7 +716,10 @@ void instrument_spec_assignst::inclusion_check_assertion( else comment += id2string(orig_comment); - comment += " is assignable"; + if(is_inductive_check) + comment += " is inductively assignable"; + else + comment += " is assignable"; source_location.set_comment(comment); dest.add(goto_programt::make_assertion( diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index ea91cd0ce99..e39db1b84a8 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -442,6 +442,12 @@ class instrument_spec_assignst const exprt &expr, goto_programt &dest); + /// Generates inclusion check instructions for inductive checks of + /// the write set + /// \param lhs the assignment lhs or argument to havoc/havoc_object + /// \param dest destination program to append instructions to + void check_inclusion_induction(const exprt &lhs, goto_programt &dest) const; + /// Instruments a sequence of instructions with inclusion checks. /// If `pred` is not provided, /// then all instructions are instrumented. @@ -547,11 +553,13 @@ class instrument_spec_assignst /// \param allow_null_lhs if true, allow the lhs to be NULL /// \param include_stack_allocated if true, include stack allocated targets /// in the inclusion check. + /// \param is_inductive_check if true, assertions are for inductive check. /// \param dest destination program to append instructions to void inclusion_check_assertion( const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, + bool is_inductive_check, goto_programt &dest) const; /// \brief Adds an assignment in dest to invalidate the tracked car if diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp index 185b010140b..4d74d8172eb 100644 --- a/src/goto-instrument/havoc_utils.cpp +++ b/src/goto-instrument/havoc_utils.cpp @@ -31,15 +31,6 @@ void havoc_utilst::append_havoc_code_for_expr( const exprt &expr, goto_programt &dest) const { - if(expr.id() == ID_index || expr.id() == ID_dereference) - { - address_of_exprt address_of_expr(expr); - if(!is_constant(address_of_expr)) - { - append_object_havoc_code_for_expr(location, address_of_expr, dest); - return; - } - } append_scalar_havoc_code_for_expr(location, expr, dest); } diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h index eb9710a4794..e49c1edf614 100644 --- a/src/goto-instrument/havoc_utils.h +++ b/src/goto-instrument/havoc_utils.h @@ -64,12 +64,6 @@ class havoc_utilst /// \brief Append goto instructions to havoc a single expression `expr` /// - /// If `expr` is an array index or object dereference expression, - /// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`, - /// then instructions are generated to havoc the entire underlying object. - /// Otherwise, e.g. for a[0] or *(b+i) when `i` is a known constant, - /// the instructions are generated to only havoc the scalar value of `expr`. - /// /// \param location The source location to annotate on the havoc instruction /// \param expr The expression to havoc /// \param dest The destination goto program to append the instructions to