diff --git a/regression/contracts/assigns_enforce_18/main.c b/regression/contracts/assigns_enforce_18/main.c new file mode 100644 index 00000000000..ef1ae4d163c --- /dev/null +++ b/regression/contracts/assigns_enforce_18/main.c @@ -0,0 +1,43 @@ +#include +#include + +int x = 0; +int y = 0; + +void foo(int *xp, int *xq, int a) __CPROVER_assigns(*xp) +{ + a = 2; + int *yp = malloc(sizeof(int)); + free(yp); + int z = 3; + *xp = 1; + y = -1; +} + +void bar(int *a, int *b) __CPROVER_assigns(*a, *b) +{ + free(a); + *b = 0; +} + +void baz(int *a, int *c) __CPROVER_assigns(*a) +{ + free(c); + *a = 0; +} + +int main() +{ + int z = 0; + foo(&x, &z, z); + assert(x == 1); + assert(y == -1); + assert(z == 0); + int *a = malloc(sizeof(*a)); + int b = 1; + bar(a, &b); + assert(b == 0); + int *c = malloc(sizeof(*c)); + baz(&y, c); + return 0; +} diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc new file mode 100644 index 00000000000..ba62f3a2b2e --- /dev/null +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -0,0 +1,25 @@ +CORE +main.c +--enforce-all-contracts _ --pointer-primitive-check +^EXIT=10$ +^SIGNAL=0$ +^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$ +^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$ +^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ +^.* 2 of \d+ failed \(\d+ iteration.*\)$ +^VERIFICATION FAILED$ +-- +^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$ +^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$ +^.* 3 of \d+ failed (\d+ iterations)$ +-- +Checks whether contract enforcement works with functions that deallocate memory. +We had problems before when freeing a variable, but still keeping it on +the writable set, which lead to deallocated variables issues. +Now, if a memory is deallocated, we remove it from the our freely assignable set. diff --git a/regression/contracts/assigns_enforce_19/main.c b/regression/contracts/assigns_enforce_19/main.c new file mode 100644 index 00000000000..2069f227d90 --- /dev/null +++ b/regression/contracts/assigns_enforce_19/main.c @@ -0,0 +1,33 @@ +#include + +static int b = 0; +static int c = 0; + +int f() __CPROVER_assigns() +{ + static int a = 0; + a++; + return a; +} + +int g(int *points_to_b, int *points_to_c) + __CPROVER_assigns(b) // Error: it should also mention c +{ + b = 1; + c = 2; + *points_to_b = 1; + *points_to_c = 2; +} + +int main() +{ + assert(f() == 1); + assert(f() == 2); + assert(b == 0); + assert(c == 0); + g(&b, &c); + assert(b == 1); + assert(c == 2); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_19/test.desc b/regression/contracts/assigns_enforce_19/test.desc new file mode 100644 index 00000000000..a2063f2bfa1 --- /dev/null +++ b/regression/contracts/assigns_enforce_19/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$ +^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$ +^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$ +^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$ +^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether contract enforcement works with (local and global) static variables. +Local static variables should be part of the local write set. +Global static variables should be included in the global write set, +otherwise any assignment to it is invalid. diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index 98d5e666406..10849448fc9 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -6,7 +6,7 @@ main.c ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$ ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$ ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[f4.\d+\] line \d+ Check that p is assignable: FAILURE$ +^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc index 28accca893f..0d3a03e4367 100644 --- a/regression/contracts/assigns_validity_pointer_04/test.desc +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -1,9 +1,11 @@ -KNOWNBUG +CORE main.c --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$ +^.* 1 of \d+ failed \(\d+ iteration.*\)$ +^VERIFICATION FAILED$ // bar ASSERT \*foo::x > 0 IF ¬\(\*foo::x = 3\) THEN GOTO \d @@ -17,9 +19,3 @@ This test checks support for a malloced pointer that is assigned to by a function (bar and baz). Both functions bar and baz are being replaced by their function contracts, while the calling function foo is being checked (by enforcing it's function contracts). - -BUG: `z` is being assigned to in `foo`, but is not in `foo`s assigns clause! -This test is expected to pass but it should not. -It somehow used to (and still does on *nix), but that seems buggy. -Most likely the bug is related to `freely_assignable_symbols`, -which would be properly fixed in a subsequent PR. diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index b033cfa8763..20b6f8c961d 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -23,7 +23,6 @@ assigns_clauset::targett::targett( const assigns_clauset &parent, const exprt &expr) : address(address_of_exprt(normalize(expr))), - expr(expr), id(expr.id()), parent(parent) { @@ -89,17 +88,18 @@ assigns_clauset::assigns_clauset( const exprt &expr, const messaget &log, const namespacet &ns) - : expr(expr), log(log), ns(ns) + : location(expr.source_location()), log(log), ns(ns) { for(const auto &target_expr : expr.operands()) { - add_target(target_expr); + add_to_global_write_set(target_expr); } } -void assigns_clauset::add_target(const exprt &target_expr) +void assigns_clauset::add_to_global_write_set(const exprt &target_expr) { - auto insertion_succeeded = targets.emplace(*this, target_expr).second; + auto insertion_succeeded = + global_write_set.emplace(*this, target_expr).second; if(!insertion_succeeded) { @@ -110,32 +110,50 @@ void assigns_clauset::add_target(const exprt &target_expr) } } -void assigns_clauset::remove_target(const exprt &target_expr) +void assigns_clauset::remove_from_global_write_set(const exprt &target_expr) { - targets.erase(targett(*this, targett::normalize(target_expr))); + global_write_set.erase(targett(*this, target_expr)); +} + +void assigns_clauset::add_to_local_write_set(const exprt &expr) +{ + local_write_set.emplace(*this, expr); +} + +void assigns_clauset::remove_from_local_write_set(const exprt &expr) +{ + local_write_set.erase(targett(*this, expr)); } goto_programt assigns_clauset::generate_havoc_code() const { modifiest modifies; - for(const auto &target : targets) + for(const auto &target : global_write_set) + modifies.insert(target.address.object()); + + for(const auto &target : local_write_set) modifies.insert(target.address.object()); goto_programt havoc_statements; - append_havoc_code(expr.source_location(), modifies, havoc_statements); + append_havoc_code(location, modifies, havoc_statements); return havoc_statements; } exprt assigns_clauset::generate_containment_check(const exprt &lhs) const { // If write set is empty, no assignment is allowed. - if(targets.empty()) + if(global_write_set.empty() && local_write_set.empty()) return false_exprt(); const auto lhs_address = address_of_exprt(targett::normalize(lhs)); exprt::operandst condition; - for(const auto &target : targets) + for(const auto &target : local_write_set) + { + condition.push_back(target.generate_containment_check(lhs_address)); + } + + for(const auto &target : global_write_set) { condition.push_back(target.generate_containment_check(lhs_address)); } @@ -145,11 +163,16 @@ exprt assigns_clauset::generate_containment_check(const exprt &lhs) const exprt assigns_clauset::generate_subset_check( const assigns_clauset &subassigns) const { - if(subassigns.targets.empty()) + if(subassigns.global_write_set.empty()) return true_exprt(); + INVARIANT( + subassigns.local_write_set.empty(), + "Local write set for function calls should be empty at this point.\n" + + subassigns.location.as_string()); + exprt result = true_exprt(); - for(const auto &subtarget : subassigns.targets) + for(const auto &subtarget : subassigns.global_write_set) { // TODO: Optimize the implication generated due to the validity check. // In some cases, e.g. when `subtarget` is known to be `NULL`, @@ -158,7 +181,12 @@ exprt assigns_clauset::generate_subset_check( w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type())); exprt::operandst current_subtarget_found_conditions; - for(const auto &target : targets) + for(const auto &target : global_write_set) + { + current_subtarget_found_conditions.push_back( + target.generate_containment_check(subtarget.address)); + } + for(const auto &target : local_write_set) { current_subtarget_found_conditions.push_back( target.generate_containment_check(subtarget.address)); diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 5b9d334364d..1071ce8fb79 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -34,38 +34,40 @@ class assigns_clauset bool operator==(const targett &other) const { - return expr == other.expr; + return address == other.address; } struct hasht { std::size_t operator()(const targett &target) const { - return irep_hash{}(target.expr); + return irep_hash{}(target.address); } }; const address_of_exprt address; - const exprt &expr; const irep_idt &id; const assigns_clauset &parent; }; assigns_clauset(const exprt &, const messaget &, const namespacet &); - void add_target(const exprt &); - void remove_target(const exprt &); + void add_to_global_write_set(const exprt &); + void remove_from_global_write_set(const exprt &); + void add_to_local_write_set(const exprt &); + void remove_from_local_write_set(const exprt &); goto_programt generate_havoc_code() const; exprt generate_containment_check(const exprt &) const; exprt generate_subset_check(const assigns_clauset &) const; - const exprt &expr; + const source_locationt &location; const messaget &log; const namespacet &ns; protected: - std::unordered_set targets; + std::unordered_set global_write_set; + std::unordered_set local_write_set; }; #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 4aad2ec3b74..a79e24f28cc 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -666,24 +666,9 @@ goto_functionst &code_contractst::get_goto_functions() return goto_functions; } -exprt code_contractst::create_alias_expression( - const exprt &lhs, - std::vector &aliasable_references) -{ - exprt::operandst operands; - operands.reserve(aliasable_references.size()); - for(auto aliasable : aliasable_references) - { - operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type()))); - } - return disjunction(operands); -} - void code_contractst::instrument_assign_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, - exprt &assigns, - std::set &freely_assignable_symbols, assigns_clauset &assigns_clause) { INVARIANT( @@ -693,26 +678,33 @@ void code_contractst::instrument_assign_statement( const exprt &lhs = instruction_iterator->assign_lhs(); - if( - freely_assignable_symbols.find(lhs.get(ID_identifier)) == - freely_assignable_symbols.end()) + // Local static variables are not declared locally, therefore, they are not + // included in the local write set during declaration. We check here whether + // lhs of the assignment is a local static variable and, if it is indeed + // true, we add lhs to our local write set before checking the assignment. + if(lhs.id() == ID_symbol) { - 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); + auto lhs_sym = ns.lookup(lhs.get(ID_identifier)); + if( + lhs_sym.is_static_lifetime && + lhs_sym.location.get_function() == + instruction_iterator->source_location.get_function()) + 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); } void code_contractst::instrument_call_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, - exprt &assigns, - std::set &freely_assignable_symbols, assigns_clauset &assigns_clause) { INVARIANT( @@ -742,25 +734,34 @@ void code_contractst::instrument_call_statement( instruction_iterator++; if(instruction_iterator->is_assign()) { - const exprt &rhs = instruction_iterator->assign_rhs(); - INVARIANT( - rhs.id() == ID_typecast, - "malloc is called but the result is not cast. Excluding result from " - "the assignable memory frame."); - typet cast_type = rhs.type(); - - // Make freshly allocated memory assignable, if we can determine its type. - assigns_clause.add_target(dereference_exprt(rhs)); + instrument_assign_statement( + instruction_iterator, program, assigns_clause); + const exprt &lhs = instruction_iterator->assign_lhs(); + assigns_clause.add_to_local_write_set(dereference_exprt(lhs)); } return; // assume malloc edits no pre-existing memory objects. } + 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"); + 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; + } if( instruction_iterator->call_lhs().is_not_nil() && - instruction_iterator->call_lhs().id() == ID_symbol && - freely_assignable_symbols.find( - to_symbol_expr(instruction_iterator->call_lhs()).get_identifier()) == - freely_assignable_symbols.end()) + instruction_iterator->call_lhs().id() == ID_symbol) { const auto alias_expr = assigns_clause.generate_containment_check( instruction_iterator->call_lhs()); @@ -896,24 +897,28 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) return true; } + // Get assigns clause for function + const symbolt &target = ns.lookup(function); + assigns_clauset assigns( + to_code_with_contract_type(target.type).assigns(), log, ns); + + // Adds formal parameters to freely assignable set + for(auto ¶meter : to_code_type(target.type).parameters()) + { + assigns.add_to_local_write_set( + ns.lookup(parameter.get_identifier()).symbol_expr()); + } + // Insert aliasing assertions - check_frame_conditions(program, ns.lookup(function)); + check_frame_conditions(program, assigns); return false; } void code_contractst::check_frame_conditions( goto_programt &program, - const symbolt &target) + assigns_clauset &assigns) { - const auto &type = to_code_with_contract_type(target.type); - exprt assigns_expr = type.assigns(); - - assigns_clauset assigns(assigns_expr, log, ns); - - // Create a list of variables that are okay to assign. - std::set freely_assignable_symbols; - for(auto instruction_it = program.instructions.begin(); instruction_it != program.instructions.end(); ++instruction_it) @@ -921,18 +926,13 @@ void code_contractst::check_frame_conditions( if(instruction_it->is_decl()) { // Local variables are always freely assignable - freely_assignable_symbols.insert( - instruction_it->get_decl().symbol().get_identifier()); - - assigns.add_target(instruction_it->get_decl().symbol()); + assigns.add_to_local_write_set(instruction_it->get_decl().symbol()); } else if(instruction_it->is_assign()) { instrument_assign_statement( instruction_it, program, - assigns_expr, - freely_assignable_symbols, assigns); } else if(instruction_it->is_function_call()) @@ -940,16 +940,11 @@ void code_contractst::check_frame_conditions( instrument_call_statement( instruction_it, program, - assigns_expr, - freely_assignable_symbols, assigns); } else if(instruction_it->is_dead()) { - freely_assignable_symbols.erase( - instruction_it->get_dead().symbol().get_identifier()); - - assigns.remove_target(instruction_it->get_dead().symbol()); + assigns.remove_from_local_write_set(instruction_it->get_dead().symbol()); } } } diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 97da9806748..ea020b47645 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -150,7 +150,7 @@ class code_contractst /// Insert assertion statements into the goto program to ensure that /// assigned memory is within the assignable memory frame. - void check_frame_conditions(goto_programt &program, const symbolt &target); + void check_frame_conditions(goto_programt &, assigns_clauset &); /// Check if there are any malloc statements which may be repeated because of /// a goto statement that jumps back. @@ -159,31 +159,20 @@ class code_contractst /// Inserts an assertion statement into program 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_exprs. + /// in freely assignable set. void instrument_assign_statement( - goto_programt::instructionst::iterator &instruction_it, - goto_programt &program, - exprt &assigns, - std::set &freely_assignable_symbols, - assigns_clauset &assigns_clause); + 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_exprs. + /// aliased by some expression in assigns_references, unless it is contained + /// in freely assignable set. void instrument_call_statement( - goto_programt::instructionst::iterator &ins_it, - goto_programt &program, - exprt &assigns, - std::set &freely_assignable_symbols, - assigns_clauset &assigns_clause); - - /// Creates a boolean expression which is true when there exists an expression - /// in aliasable_references with the same pointer object and pointer offset as - /// the address of lhs. - exprt create_alias_expression( - const exprt &lhs, - std::vector &aliasable_references); + goto_programt::instructionst::iterator &, + goto_programt &, + assigns_clauset &); /// Apply loop contracts, whenever available, to all loops in `function`. /// Loop invariants, loop variants, and loop assigns clauses.