From 26760d38b11cab910d1b3bbf468ebe4280161c1c Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 24 Nov 2021 02:31:03 +0000 Subject: [PATCH 1/3] fix writeset inclusion checks on DEAD instructions When handling DEAD instructions in function/loop assigns clause instrumentation, the instruction iterator was not being incremented correctly. This led to instrumentation outside of the function/loop scope, and spurious write set inclusion violations. Moreover, for loops, declarations of some temporaries (those involved in the "initialization" of loop counter, for instance) are "outside" of the loop identified by CBMC, so we no longer raise an exception on not finding a corresponding DECL for each DEAD. These variables are writable because they appear as assigns clause targets, not because they were local DECLs. --- regression/contracts/loop_assigns-05/main.c | 59 +++++++++++++++++++ .../contracts/loop_assigns-05/test.desc | 19 ++++++ src/goto-instrument/contracts/contracts.cpp | 22 ++++--- 3 files changed, 93 insertions(+), 7 deletions(-) create mode 100644 regression/contracts/loop_assigns-05/main.c create mode 100644 regression/contracts/loop_assigns-05/test.desc diff --git a/regression/contracts/loop_assigns-05/main.c b/regression/contracts/loop_assigns-05/main.c new file mode 100644 index 00000000000..454aa2e4117 --- /dev/null +++ b/regression/contracts/loop_assigns-05/main.c @@ -0,0 +1,59 @@ +#include + +int j; + +int lowerbound() +{ + return 0; +} + +int upperbound() +{ + return 10; +} + +void incr(int *i) +{ + (*i)++; +} + +void body_1(int i) +{ + j = i; +} + +void body_2(int *i) +{ + (*i)++; + (*i)--; +} + +int body_3(int *i) +{ + (*i)++; + if(*i == 4) + return 1; + + (*i)--; + return 0; +} + +int main() +{ + for(int i = lowerbound(); i < upperbound(); incr(&i)) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_loop_invariant(i != 0 ==> j + 1 == i) + // clang-format on + { + body_1(i); + + if(body_3(&i)) + return 1; + + body_2(&i); + } + + assert(j == 9); +} diff --git a/regression/contracts/loop_assigns-05/test.desc b/regression/contracts/loop_assigns-05/test.desc new file mode 100644 index 00000000000..78091d38b81 --- /dev/null +++ b/regression/contracts/loop_assigns-05/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[body_1.\d+\] .* Check that j is assignable: SUCCESS$ +^\[body_2.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[body_3.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[incr.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks write set inclusion checks in presence of function calls, +which are inlined, and also checks that DEAD instructions introduced during +inlining is correctly handled. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 4cb4af3d077..7ddf4d34de7 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1054,20 +1054,28 @@ void code_contractst::check_frame_conditions( assigns_clauset::conditional_address_ranget{assigns, symbol}); if(symbol_car != assigns.get_write_set().end()) { - instruction_it++; auto invalidation_assignment = goto_programt::make_assignment( symbol_car->validity_condition_var, false_exprt{}, instruction_it->source_location()); - // note that instruction_it is not advanced by this call, - // so no need to move it backwards - body.insert_before_swap(instruction_it, invalidation_assignment); + // note that the CAR must be invalidated _after_ the DEAD instruction + body.insert_after( + instruction_it, + add_pragma_disable_assigns_check(invalidation_assignment)); } else { - throw incorrect_goto_program_exceptiont( - "Found a `DEAD` variable without corresponding `DECL`!", - instruction_it->source_location()); + // For loops, the loop_head appears after the DECL of counters, + // and any other temporaries introduced during "initialization". + // However, they go `DEAD` (possible conditionally) inside the loop, + // in presence of return statements. + // Notice that for them those variables be writable, + // they must appear as assigns targets anyway, + // but their DECL statements are outside of the loop. + log.warning() << "Found a `DEAD` variable " + << name2string(symbol.get_identifier()) + << " without corresponding `DECL`, at: " + << instruction_it->source_location() << messaget::eom; } } else if( From 911db55caf14f8d9135a8e1d828c5b5f8cf78d1a Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 24 Nov 2021 02:33:49 +0000 Subject: [PATCH 2/3] refactor function call inling for code contracts Function call inlining was earlier performed on the same function multiple times if it had multiple loops. We refactor the inlining call out and only inline the function once, even if it has multiple loops. --- src/goto-instrument/contracts/contracts.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 7ddf4d34de7..9dae6635c72 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -256,10 +256,13 @@ void code_contractst::check_apply_loop_contracts( // Forward the loop_head iterator until the start of the body. // This is necessary because complex C loop_head conditions could be // converted to multiple GOTO instructions (e.g. temporaries are introduced). + // If the loop_head location shifts to a different function, + // assume that it's an inlined function and keep skipping. // FIXME: This simple approach wouldn't work when // the loop guard in the source file is split across multiple lines. const auto head_loc = loop_head->source_location(); - while(loop_head->source_location() == head_loc) + while(loop_head->source_location() == head_loc || + loop_head->source_location().get_function() != head_loc.get_function()) loop_head++; // At this point, we are just past the loop head, @@ -678,6 +681,12 @@ void code_contractst::apply_loop_contract( local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); + if(!natural_loops.loop_map.size()) + return; + + goto_function_inline( + goto_functions, function_name, ns, log.get_message_handler()); + // A graph node type that stores information about a loop. // We create a DAG representing nesting of various loops in goto_function, // sort them topologically, and instrument them in the top-sorted order. @@ -992,7 +1001,11 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function_obj->second.body, instruction_it, snapshot_instructions); }; - // Insert aliasing assertions + // Inline all function calls. + goto_function_inline( + goto_functions, function_obj->first, ns, log.get_message_handler()); + + // Insert write set inclusion checks. check_frame_conditions( function_obj->first, function_obj->second.body, @@ -1010,8 +1023,6 @@ void code_contractst::check_frame_conditions( const goto_programt::targett &instruction_end, assigns_clauset &assigns) { - goto_function_inline(goto_functions, function, ns, log.get_message_handler()); - for(; instruction_it != instruction_end; ++instruction_it) { const auto &pragmas = instruction_it->source_location().get_pragmas(); From abd36cf471867973832188dd50a5be44f6430a48 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 24 Nov 2021 03:06:07 +0000 Subject: [PATCH 3/3] instrument loop head for inclusion checks as well Previously, only loop body was being instrumented for write set inclusion checks. This could miss checking writes performed by the loop guard, if it has side effects. In this PR, we also instrument the loop guard with inclusion checks. --- src/goto-instrument/contracts/contracts.cpp | 24 ++++++++++++--------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 9dae6635c72..1f1cea11320 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -189,6 +189,10 @@ void code_contractst::check_apply_loop_contracts( insert_before_swap_and_advance( goto_function.body, loop_head, snapshot_instructions); }; + + // Perform write set instrumentation on the entire loop. + check_frame_conditions( + function_name, goto_function.body, loop_head, loop_end, loop_assigns); } havoc_assigns_targetst havoc_gen(modifies, ns); @@ -251,7 +255,10 @@ void code_contractst::check_apply_loop_contracts( // Assume invariant & decl the variant temporaries (just before loop guard). // Use insert_before_swap to preserve jumps to loop head. - insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + insert_before_swap_and_advance( + goto_function.body, + loop_head, + add_pragma_disable_assigns_check(generated_code)); // Forward the loop_head iterator until the start of the body. // This is necessary because complex C loop_head conditions could be @@ -270,13 +277,6 @@ void code_contractst::check_apply_loop_contracts( auto loop_body = loop_head; loop_head--; - // Perform write set instrumentation before adding anything else to loop body. - if(assigns.is_not_nil()) - { - check_frame_conditions( - function_name, goto_function.body, loop_body, loop_end, loop_assigns); - } - // Generate: assignments to store the multidimensional decreases clause's // value just before the loop body (but just after the loop guard) if(!decreases_clause.is_nil()) @@ -290,7 +290,8 @@ void code_contractst::check_apply_loop_contracts( converter.goto_convert(old_decreases_assignment, generated_code, mode); } - goto_function.body.destructive_insert(loop_body, generated_code); + goto_function.body.destructive_insert( + loop_body, add_pragma_disable_assigns_check(generated_code)); } // Generate: assert(invariant) just after the loop exits @@ -340,7 +341,10 @@ void code_contractst::check_apply_loop_contracts( } } - insert_before_swap_and_advance(goto_function.body, loop_end, generated_code); + insert_before_swap_and_advance( + goto_function.body, + loop_end, + add_pragma_disable_assigns_check(generated_code)); // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume();