From f7ff4bf8d5625fea87af947d87c2ef437358aabd Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 20 Sep 2021 20:33:52 +0000 Subject: [PATCH 1/2] Check frame conditions before __CPROVER_havoc_object Signed-off-by: Felipe R. Monteiro --- .../contracts/assigns_enforce_20/main.c | 19 ++++++++++++++++++ .../contracts/assigns_enforce_20/test.desc | 11 ++++++++++ src/goto-instrument/contracts/contracts.cpp | 20 ++++++++++++++++++- 3 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 regression/contracts/assigns_enforce_20/main.c create mode 100644 regression/contracts/assigns_enforce_20/test.desc diff --git a/regression/contracts/assigns_enforce_20/main.c b/regression/contracts/assigns_enforce_20/main.c new file mode 100644 index 00000000000..5ff7211df3b --- /dev/null +++ b/regression/contracts/assigns_enforce_20/main.c @@ -0,0 +1,19 @@ +#include +#include + +int x = 0; + +void foo(int *y) __CPROVER_assigns() +{ + __CPROVER_havoc_object(y); + x = 2; +} + +int main() +{ + int *y = malloc(sizeof(*y)); + *y = 0; + foo(y); + assert(x == 2); + return 0; +} diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc new file mode 100644 index 00000000000..8ccf467a53a --- /dev/null +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether contract enforcement works with __CPROVER_havoc_object. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 9f4f0188b10..2d848d81f82 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -748,7 +748,8 @@ void code_contractst::instrument_call_statement( called_name = to_symbol_expr(instruction_iterator->call_function()).get_identifier(); } - + log.warning() << "called function: " << id2string(called_name) + << messaget::eom; if(called_name == "malloc") { // malloc statments return a void pointer, which is then cast and assigned @@ -972,6 +973,23 @@ void code_contractst::check_frame_conditions( { assigns.remove_from_local_write_set(instruction_it->get_dead().symbol()); } + else if( + instruction_it->is_other() && + instruction_it->get_other().get_statement() == ID_havoc_object) + { + goto_programt alias_assertion; + const exprt &havoc_argument = dereference_exprt( + to_typecast_expr(instruction_it->get_other().operands().front()).op()); + alias_assertion.add(goto_programt::make_assertion( + assigns.generate_containment_check(havoc_argument), + instruction_it->source_location)); + alias_assertion.instructions.back().source_location.set_comment( + "Check that " + from_expr(ns, havoc_argument.id(), havoc_argument) + + " is assignable"); + assigns.remove_from_local_write_set(havoc_argument); + assigns.remove_from_global_write_set(havoc_argument); + insert_before_swap_and_advance(program, instruction_it, alias_assertion); + } } } From 7075866f5c9aaab6c363600a37400c996dee1bfd Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 20 Sep 2021 21:31:22 +0000 Subject: [PATCH 2/2] Adds procedure to inject containment checks Signed-off-by: Felipe R. Monteiro --- src/goto-instrument/contracts/contracts.cpp | 60 ++++++++------------- src/goto-instrument/contracts/contracts.h | 8 +++ 2 files changed, 31 insertions(+), 37 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 2d848d81f82..ebd6e964c20 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -715,14 +715,7 @@ void code_contractst::instrument_assign_statement( assigns_clause.add_to_local_write_set(lhs); } - goto_programt alias_assertion; - alias_assertion.add(goto_programt::make_assertion( - assigns_clause.generate_containment_check(lhs), - instruction_iterator->source_location)); - alias_assertion.instructions.back().source_location.set_comment( - "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); - insert_before_swap_and_advance( - program, instruction_iterator, alias_assertion); + add_containment_check(program, assigns_clause, instruction_iterator, lhs); } void code_contractst::instrument_call_statement( @@ -748,8 +741,7 @@ void code_contractst::instrument_call_statement( called_name = to_symbol_expr(instruction_iterator->call_function()).get_identifier(); } - log.warning() << "called function: " << id2string(called_name) - << messaget::eom; + if(called_name == "malloc") { // malloc statments return a void pointer, which is then cast and assigned @@ -767,19 +759,12 @@ void code_contractst::instrument_call_statement( } else if(called_name == "free") { - goto_programt alias_assertion; const exprt &lhs_dereference = dereference_exprt( to_typecast_expr(instruction_iterator->call_arguments().front()).op()); - alias_assertion.add(goto_programt::make_assertion( - assigns_clause.generate_containment_check(lhs_dereference), - instruction_iterator->source_location)); - alias_assertion.instructions.back().source_location.set_comment( - "Check that " + from_expr(ns, lhs_dereference.id(), lhs_dereference) + - " is assignable"); + add_containment_check( + program, assigns_clause, instruction_iterator, lhs_dereference); assigns_clause.remove_from_local_write_set(lhs_dereference); assigns_clause.remove_from_global_write_set(lhs_dereference); - insert_before_swap_and_advance( - program, instruction_iterator, alias_assertion); return; } @@ -787,17 +772,11 @@ void code_contractst::instrument_call_statement( instruction_iterator->call_lhs().is_not_nil() && instruction_iterator->call_lhs().id() == ID_symbol) { - const auto alias_expr = assigns_clause.generate_containment_check( + add_containment_check( + program, + assigns_clause, + instruction_iterator, instruction_iterator->call_lhs()); - - goto_programt alias_assertion; - alias_assertion.add(goto_programt::make_assertion( - alias_expr, instruction_iterator->source_location)); - alias_assertion.instructions.back().source_location.set_comment( - "Check that " + from_expr(ns, alias_expr.id(), alias_expr) + - " is assignable"); - insert_before_swap_and_advance( - program, instruction_iterator, alias_assertion); } const symbolt &called_symbol = ns.lookup(called_name); @@ -977,22 +956,29 @@ void code_contractst::check_frame_conditions( instruction_it->is_other() && instruction_it->get_other().get_statement() == ID_havoc_object) { - goto_programt alias_assertion; const exprt &havoc_argument = dereference_exprt( to_typecast_expr(instruction_it->get_other().operands().front()).op()); - alias_assertion.add(goto_programt::make_assertion( - assigns.generate_containment_check(havoc_argument), - instruction_it->source_location)); - alias_assertion.instructions.back().source_location.set_comment( - "Check that " + from_expr(ns, havoc_argument.id(), havoc_argument) + - " is assignable"); + add_containment_check(program, assigns, instruction_it, havoc_argument); assigns.remove_from_local_write_set(havoc_argument); assigns.remove_from_global_write_set(havoc_argument); - insert_before_swap_and_advance(program, instruction_it, alias_assertion); } } } +void code_contractst::add_containment_check( + goto_programt &program, + const assigns_clauset &assigns, + goto_programt::instructionst::iterator &instruction_it, + const exprt &expr) +{ + goto_programt assertion; + assertion.add(goto_programt::make_assertion( + assigns.generate_containment_check(expr), instruction_it->source_location)); + 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); +} + bool code_contractst::enforce_contract(const irep_idt &function) { // Add statements to the source function diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ea020b47645..4727a14f0b2 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -152,6 +152,14 @@ class code_contractst /// assigned memory is within the assignable memory frame. void check_frame_conditions(goto_programt &, assigns_clauset &); + /// Inserts an assertion into the goto program to ensure that + /// an expression is within the assignable memory frame. + void add_containment_check( + goto_programt &, + const assigns_clauset &, + goto_programt::instructionst::iterator &, + const exprt &); + /// Check if there are any malloc statements which may be repeated because of /// a goto statement that jumps back. bool check_for_looped_mallocs(const goto_programt &program);