From 60d683fd370bad644bc8a10b5d6550f98de595c4 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 6 Oct 2021 21:36:38 +0000 Subject: [PATCH 1/3] Fix initialization of invalid CARs --- src/goto-instrument/contracts/assigns.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 49142f80aec..f6b71e4cb74 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -86,6 +86,15 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() instructions.add(goto_programt::make_decl(lower_bound_address_var, location)); instructions.add(goto_programt::make_decl(upper_bound_address_var, location)); + instructions.add(goto_programt::make_assignment( + lower_bound_address_var, + null_pointer_exprt{to_pointer_type(slice.first.type())}, + location)); + instructions.add(goto_programt::make_assignment( + upper_bound_address_var, + null_pointer_exprt{to_pointer_type(slice.first.type())}, + location)); + goto_programt skip_program; const auto skip_target = skip_program.add(goto_programt::make_skip(location)); From 8da66dac65aaa467ba530470e41dfae031795c33 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 6 Oct 2021 23:12:56 +0000 Subject: [PATCH 2/3] Replace containment -> inclusion throughout --- src/goto-instrument/contracts/contracts.cpp | 8 ++++---- src/goto-instrument/contracts/contracts.h | 14 ++++++-------- 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index c5df716f2e8..6ca3934e232 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -637,7 +637,7 @@ void code_contractst::instrument_assign_statement( "The first instruction of instrument_assign_statement should always be" " an assignment"); - add_containment_check( + add_inclusion_check( program, assigns_clause, instruction_it, instruction_it->assign_lhs()); } @@ -678,7 +678,7 @@ void code_contractst::instrument_call_statement( } else if(callee_name == "free") { - add_containment_check( + add_inclusion_check( body, assigns, instruction_it, @@ -846,12 +846,12 @@ void code_contractst::check_frame_conditions( { const exprt &havoc_argument = dereference_exprt( to_typecast_expr(instruction_it->get_other().operands().front()).op()); - add_containment_check(body, assigns, instruction_it, havoc_argument); + add_inclusion_check(body, assigns, instruction_it, havoc_argument); } } } -void code_contractst::add_containment_check( +void code_contractst::add_inclusion_check( goto_programt &program, const assigns_clauset &assigns, goto_programt::instructionst::iterator &instruction_it, diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 70d10e926a1..523d464ebbf 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -134,7 +134,7 @@ class code_contractst /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. - void add_containment_check( + void add_inclusion_check( goto_programt &, const assigns_clauset &, goto_programt::instructionst::iterator &, @@ -144,19 +144,17 @@ class code_contractst /// a goto statement that jumps back. bool check_for_looped_mallocs(const goto_programt &program); - /// Inserts an assertion statement into program before the assignment + /// Inserts an assertion into program immediately before the assignment /// instruction_it, to ensure that the left-hand-side of the assignment - /// aliases some expression in original_references, unless it is contained - /// in freely assignable set. + /// is "included" in the (conditional address ranges in the) write set. void instrument_assign_statement( goto_programt::instructionst::iterator &, goto_programt &, assigns_clauset &); - /// Inserts an assertion statement into program before the function call at - /// ins_it, to ensure that any memory which may be written by the call is - /// aliased by some expression in assigns_references, unless it is contained - /// in freely assignable set. + /// Inserts an assertion into program immediately before the function call at + /// instruction_it, to ensure that all memory locations written to by the + // callee are "included" in the (conditional address ranges in the) write set. void instrument_call_statement( goto_programt::instructionst::iterator &, const irep_idt &, From 998d1417e0bddac3106a6bd03e05c045fb4edd67 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 6 Oct 2021 21:36:38 +0000 Subject: [PATCH 3/3] Fix invalidation of CARs on free and DEAD Previously, corresponding CARs were completely removed on DEAD instructions. While this is "okay" for unconditionally dead symbols, it resulted in spurious non-assignable errors when symbols were only conditionally DEAD, e.g. RETURN within a conditional block. Previously, invalid CARs from free calls were simply left behind, because (in theory) the CAR validation condition should automatically guard against conditions. However, in both these cases, we need to check dead/deallocated status of individual objects to avoid spurious errors from CBMC's internal pointer checks, which only track a single dead/deallocated object nondeterministically. --- .../assigns_enforce_free_dead/main.c | 65 ++++++++++ .../assigns_enforce_free_dead/test.desc | 43 +++++++ .../test_aliasing_ensure_indirect/test.desc | 2 +- src/goto-instrument/contracts/contracts.cpp | 118 ++++++++++++++++-- src/goto-instrument/contracts/contracts.h | 5 +- 5 files changed, 221 insertions(+), 12 deletions(-) create mode 100644 regression/contracts/assigns_enforce_free_dead/main.c create mode 100644 regression/contracts/assigns_enforce_free_dead/test.desc diff --git a/regression/contracts/assigns_enforce_free_dead/main.c b/regression/contracts/assigns_enforce_free_dead/main.c new file mode 100644 index 00000000000..d62c5553ab1 --- /dev/null +++ b/regression/contracts/assigns_enforce_free_dead/main.c @@ -0,0 +1,65 @@ +#include +#include + +int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p) +{ + if(p && *p) + **p = 0; + + { + int y; + y = 1; + *x = 0; + + if(nondet_bool()) + return 0; + + if(p) + *p = &y; + + // y goes DEAD here, unconditionally + } + + if(p && *p) + **p = 0; + + int a = 1; + + if(x == NULL) + { + return 1; + // a goes DEAD here, conditionally + } + + int *z = malloc(100 * sizeof(int)); + int *w = NULL; + + if(z) + { + w = &(z[10]); + *w = 0; + + int *q = &(z[20]); + *q = 1; + // q goes DEAD here, unconditionally + } + + free(z); + + z = malloc(sizeof(int)); + if(nondet_bool()) + { + free(z); + // here z is deallocated, conditionally + } + + *x = 1; + x = 0; +} + +int main() +{ + int z; + int *x = malloc(sizeof(int)); + foo(&z, &x); +} diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc new file mode 100644 index 00000000000..425e9705f27 --- /dev/null +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -0,0 +1,43 @@ +CORE +main.c +--enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check +^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^\[foo.\d+\] line \d+ Check that \*p is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ +^.*tmp_cc\$\d+.*: FAILURE$ +-- +Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. + +Since several variables are assigned multiple times, +we rule out all failures using the negative regex matches above. + +We also check (using positive regex matches above) that +`**p` should be assignable in one case and should not be assignable in the other. + +Finally, we check that there should be no "internal" assertion failures +on `tmp_cc` variables used to track CARs. diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 2870f741cbf..69df6b6065c 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract foo --enforce-contract bar +--enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6ca3934e232..c4bef3bc0a7 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -37,7 +37,6 @@ Date: February 2016 #include #include -#include "assigns.h" #include "memory_predicates.h" #include "utils.h" @@ -669,21 +668,98 @@ void code_contractst::instrument_call_statement( auto snapshot_instructions = car->generate_snapshot_instructions(); insert_before_swap_and_advance( body, instruction_it, snapshot_instructions); - // since CAR was inserted *after* the malloc, + // since CAR was inserted *after* the malloc call, // move the instruction pointer backward, // because the caller increments it in a `for` loop instruction_it--; } - return; } else if(callee_name == "free") { - add_inclusion_check( + const auto free_car = add_inclusion_check( body, assigns, instruction_it, pointer_object(instruction_it->call_arguments().front())); - return; + + // skip all invalidation business if we're freeing invalid memory + goto_programt alias_checking_instructions, skip_program; + alias_checking_instructions.add(goto_programt::make_goto( + skip_program.add( + goto_programt::make_skip(instruction_it->source_location)), + not_exprt{free_car.validity_condition_var}, + instruction_it->source_location)); + + // Since the argument to free may be an "alias" (but not identical) + // to existing CARs' source_expr, structural equality wouldn't work. + // Moreover, multiple CARs in the writeset might be aliased to the + // same underlying object. + // So, we first find the corresponding CAR using `same_object` checks. + std::unordered_set write_set_validity_addrs; + for(const auto &w_car : assigns.get_write_set()) + { + const auto object_validity_var_addr = + new_tmp_symbol( + pointer_type(bool_typet{}), + instruction_it->source_location, + symbol_table.lookup_ref(function).mode, + symbol_table) + .symbol_expr(); + write_set_validity_addrs.insert(object_validity_var_addr); + + alias_checking_instructions.add(goto_programt::make_decl( + object_validity_var_addr, instruction_it->source_location)); + // if the CAR was defined on the same_object as the one being `free`d, + // record its validity variable's address, otherwise record NULL + alias_checking_instructions.add(goto_programt::make_assignment( + object_validity_var_addr, + if_exprt{ + and_exprt{ + w_car.validity_condition_var, + same_object( + free_car.lower_bound_address_var, w_car.lower_bound_address_var)}, + address_of_exprt{w_car.validity_condition_var}, + null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}}, + instruction_it->source_location)); + } + + alias_checking_instructions.destructive_append(skip_program); + insert_before_swap_and_advance( + body, instruction_it, alias_checking_instructions); + + // move past the call and then insert the invalidation instructions + instruction_it++; + + // skip all invalidation business if we're freeing invalid memory + goto_programt invalidation_instructions; + skip_program.clear(); + invalidation_instructions.add(goto_programt::make_goto( + skip_program.add( + goto_programt::make_skip(instruction_it->source_location)), + not_exprt{free_car.validity_condition_var}, + instruction_it->source_location)); + + // invalidate all recorded CAR validity variables + for(const auto &w_car_validity_addr : write_set_validity_addrs) + { + goto_programt w_car_skip_program; + invalidation_instructions.add(goto_programt::make_goto( + w_car_skip_program.add( + goto_programt::make_skip(instruction_it->source_location)), + null_pointer(w_car_validity_addr), + instruction_it->source_location)); + invalidation_instructions.add(goto_programt::make_assignment( + dereference_exprt{w_car_validity_addr}, + false_exprt{}, + instruction_it->source_location)); + invalidation_instructions.destructive_append(w_car_skip_program); + } + + invalidation_instructions.destructive_append(skip_program); + insert_before_swap_and_advance( + body, instruction_it, invalidation_instructions); + + instruction_it--; } } @@ -823,9 +899,9 @@ void code_contractst::check_frame_conditions( auto snapshot_instructions = car->generate_snapshot_instructions(); insert_before_swap_and_advance( body, instruction_it, snapshot_instructions); - // since CAR was inserted *after* the DECL, + // since CAR was inserted *after* the DECL instruction, // move the instruction pointer backward, - // because the caller increments it in a `for` loop + // because the `for` loop takes care of the increment instruction_it--; } else if(instruction_it->is_assign()) @@ -838,7 +914,28 @@ void code_contractst::check_frame_conditions( } else if(instruction_it->is_dead()) { - assigns.remove_from_write_set(instruction_it->dead_symbol()); + const auto &symbol = instruction_it->dead_symbol(); + // CAR equality and hash are defined on source_expr alone, + // therefore this temporary CAR should be "found" + const auto &symbol_car = assigns.get_write_set().find( + 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); + } + else + { + throw incorrect_goto_program_exceptiont( + "Found a `DEAD` variable without corresponding `DECL`!", + instruction_it->source_location); + } } else if( instruction_it->is_other() && @@ -851,7 +948,8 @@ void code_contractst::check_frame_conditions( } } -void code_contractst::add_inclusion_check( +const assigns_clauset::conditional_address_ranget +code_contractst::add_inclusion_check( goto_programt &program, const assigns_clauset &assigns, goto_programt::instructionst::iterator &instruction_it, @@ -868,6 +966,8 @@ void code_contractst::add_inclusion_check( assertion.instructions.back().source_location.set_comment( "Check that " + from_expr(ns, expr.id(), expr) + " is assignable"); insert_before_swap_and_advance(program, instruction_it, assertion); + + return car; } bool code_contractst::enforce_contract(const irep_idt &function) diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 523d464ebbf..bd79f6e3b7c 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -30,6 +30,8 @@ Date: February 2016 #include #include +#include "assigns.h" + #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" #define HELP_LOOP_CONTRACTS \ " --apply-loop-contracts\n" \ @@ -44,7 +46,6 @@ Date: February 2016 #define HELP_ENFORCE_CONTRACT \ " --enforce-contract wrap fun with an assertion of its contract\n" -class assigns_clauset; class local_may_aliast; class replace_symbolt; @@ -134,7 +135,7 @@ class code_contractst /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. - void add_inclusion_check( + const assigns_clauset::conditional_address_ranget add_inclusion_check( goto_programt &, const assigns_clauset &, goto_programt::instructionst::iterator &,