From ddf9a0466c9ecd6baf75d4ea47625ef3a3d4a731 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Wed, 8 Sep 2021 22:14:10 +0000 Subject: [PATCH 1/3] Refactor assigns clause implementation + usused fields (e.g., `function_id`, `init_block`) are removed, + redundant functions (e.g. `pointer_for`) are removed, + const references are used throughout consistently + targets are tracked in an `unordered_set` as opposed to `vector` + introduced a "normalize" method for extracting base object of arrays + API renamed for clarity --- .../contracts/assigns_repeated_ignored/main.c | 13 ++ .../assigns_repeated_ignored/test.desc | 11 ++ src/goto-instrument/contracts/assigns.cpp | 150 ++++++++---------- src/goto-instrument/contracts/assigns.h | 85 +++++----- src/goto-instrument/contracts/contracts.cpp | 21 ++- 5 files changed, 139 insertions(+), 141 deletions(-) create mode 100644 regression/contracts/assigns_repeated_ignored/main.c create mode 100644 regression/contracts/assigns_repeated_ignored/test.desc diff --git a/regression/contracts/assigns_repeated_ignored/main.c b/regression/contracts/assigns_repeated_ignored/main.c new file mode 100644 index 00000000000..2a270ca8367 --- /dev/null +++ b/regression/contracts/assigns_repeated_ignored/main.c @@ -0,0 +1,13 @@ +int foo(int *x) __CPROVER_assigns(*x, *x) +{ + *x = *x + 0; + return *x + 5; +} + +int main() +{ + int n = 4; + n = foo(&n); + + return 0; +} diff --git a/regression/contracts/assigns_repeated_ignored/test.desc b/regression/contracts/assigns_repeated_ignored/test.desc new file mode 100644 index 00000000000..a08522e0627 --- /dev/null +++ b/regression/contracts/assigns_repeated_ignored/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^Ignored duplicate expression '\*x' in assigns clause at file main\.c line \d+$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that repeated expressions in assigns clauses are +correctly detected and ignored. diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 9f8a9aae503..1b6fc7a86d5 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Specify write set in function contracts. +Module: Specify write set in code contracts. Author: Felipe R. Monteiro @@ -19,129 +19,112 @@ Date: July 2021 #include #include -assigns_clause_targett::assigns_clause_targett( - const exprt &object, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id) - : contract(contract), - init_block(), - log(log_parameter), - target(pointer_for(object)), - target_id(object.id()) +assigns_clauset::targett::targett( + const assigns_clauset &parent, + const exprt &expr) + : expr(address_of_exprt(expr)), id(expr.id()), parent(parent) { - INVARIANT( - target.type().id() == ID_pointer, - "Assigns clause targets should be stored as pointer expressions."); } -assigns_clause_targett::~assigns_clause_targett() +exprt assigns_clauset::targett::normalize(const exprt &expr) { + if(expr.id() != ID_address_of) + return expr; + + const auto &object = to_address_of_expr(expr).object(); + if(object.id() != ID_index) + return object; + + return to_index_expr(object).array(); } -exprt assigns_clause_targett::alias_expression(const exprt &lhs) +exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const { exprt::operandst condition; - exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object() - : pointer_for(lhs); + const auto lhs_ptr = + (lhs.id() == ID_address_of) ? lhs : address_of_exprt(lhs); // __CPROVER_w_ok(target, sizeof(target)) condition.push_back(w_ok_exprt( - target, - size_of_expr(dereference_exprt(target).type(), contract.ns).value())); + expr, size_of_expr(dereference_exprt(expr).type(), parent.ns).value())); // __CPROVER_same_object(lhs, target) - condition.push_back(same_object(lhs_ptr, target)); + condition.push_back(same_object(lhs_ptr, expr)); // If assigns target was a dereference, comparing objects is enough - if(target_id == ID_dereference) + if(id == ID_dereference) { return conjunction(condition); } - const exprt lhs_offset = pointer_offset(lhs_ptr); - const exprt target_offset = pointer_offset(target); + const auto lhs_offset = pointer_offset(lhs_ptr); + const auto own_offset = pointer_offset(expr); // __CPROVER_offset(lhs) >= __CPROVER_offset(target) - condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, target_offset)); + condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset)); - const exprt region_lhs = plus_exprt( + const auto lhs_region = plus_exprt( typecast_exprt::conditional_cast( - size_of_expr(lhs.type(), contract.ns).value(), lhs_offset.type()), + size_of_expr(lhs.type(), parent.ns).value(), lhs_offset.type()), lhs_offset); - const exprt region_target = plus_exprt( + const exprt own_region = plus_exprt( typecast_exprt::conditional_cast( - size_of_expr(dereference_exprt(target).type(), contract.ns).value(), - target_offset.type()), - target_offset); + size_of_expr(dereference_exprt(expr).type(), parent.ns).value(), + own_offset.type()), + own_offset); // (sizeof(lhs) + __CPROVER_offset(lhs)) <= // (sizeof(target) + __CPROVER_offset(target)) - condition.push_back(binary_relation_exprt(region_lhs, ID_le, region_target)); + condition.push_back(binary_relation_exprt(lhs_region, ID_le, own_region)); return conjunction(condition); } -exprt assigns_clause_targett::compatible_expression( - const assigns_clause_targett &called_target) -{ - return same_object(called_target.get_target(), target); -} - -const exprt &assigns_clause_targett::get_target() const +exprt assigns_clauset::targett::generate_compatibility_check( + const assigns_clauset::targett &other_target) const { - return target; + return same_object(other_target.expr, expr); } assigns_clauset::assigns_clauset( - const exprt &assigns, - code_contractst &contract, - const irep_idt function_id, - messaget log_parameter) - : assigns(assigns), - parent(contract), - function_id(function_id), - log(log_parameter) + const exprt &expr, + const messaget &log, + const namespacet &ns) + : expr(expr), log(log), ns(ns) { - for(exprt target : assigns.operands()) + for(const auto &target_expr : expr.operands()) { - add_target(target); + add_target(target_expr); } } -assigns_clauset::~assigns_clauset() +void assigns_clauset::add_target(const exprt &target_expr) { - for(assigns_clause_targett *target : targets) + auto insertion_succeeded = + targets.emplace(*this, targett::normalize(target_expr)).second; + + if(!insertion_succeeded) { - delete target; + log.warning() << "Ignored duplicate expression '" + << from_expr(ns, target_expr.id(), target_expr) + << "' in assigns clause at " + << target_expr.source_location().as_string() << messaget::eom; } } -void assigns_clauset::add_target(exprt target) -{ - assigns_clause_targett *new_target = new assigns_clause_targett( - (target.id() == ID_address_of) - ? to_index_expr(to_address_of_expr(target).object()).array() - : target, - parent, - log, - function_id); - targets.push_back(new_target); -} - -goto_programt assigns_clauset::havoc_code() +goto_programt assigns_clauset::generate_havoc_code() const { modifiest modifies; - for(const auto &t : targets) - modifies.insert(to_address_of_expr(t->get_target()).object()); + for(const auto &target : targets) + modifies.insert(to_address_of_expr(target.expr).object()); goto_programt havoc_statements; - append_havoc_code(assigns.source_location(), modifies, havoc_statements); + append_havoc_code(expr.source_location(), modifies, havoc_statements); return havoc_statements; } -exprt assigns_clauset::alias_expression(const exprt &lhs) +exprt assigns_clauset::generate_alias_check(const exprt &lhs) const { // If write set is empty, no assignment is allowed. if(targets.empty()) @@ -150,15 +133,15 @@ exprt assigns_clauset::alias_expression(const exprt &lhs) } exprt::operandst condition; - for(assigns_clause_targett *target : targets) + for(const auto &target : targets) { - condition.push_back(target->alias_expression(lhs)); + condition.push_back(target.generate_alias_check(lhs)); } return disjunction(condition); } -exprt assigns_clauset::compatible_expression( - const assigns_clauset &called_assigns) +exprt assigns_clauset::generate_compatibility_check( + const assigns_clauset &called_assigns) const { if(called_assigns.targets.empty()) { @@ -167,11 +150,11 @@ exprt assigns_clauset::compatible_expression( bool first_clause = true; exprt result = true_exprt(); - for(assigns_clause_targett *called_target : called_assigns.targets) + for(const auto &called_target : called_assigns.targets) { bool first_iter = true; exprt current_target_compatible = false_exprt(); - for(assigns_clause_targett *target : targets) + for(const auto &target : targets) { if(first_iter) { @@ -180,22 +163,22 @@ exprt assigns_clauset::compatible_expression( // Validating the called target through __CPROVER_w_ok() is // only useful when the called target is a dereference - const auto &called_target_ptr = called_target->get_target(); + const auto &called_target_ptr = called_target.expr; if( to_address_of_expr(called_target_ptr).object().id() == ID_dereference) { // or_exprt is short-circuited, therefore - // target->compatible_expression(*called_target) would not be + // target.generate_compatibility_check(*called_target) would not be // checked on invalid called_targets. current_target_compatible = or_exprt( not_exprt(w_ok_exprt( called_target_ptr, from_integer(0, unsigned_int_type()))), - target->compatible_expression(*called_target)); + target.generate_compatibility_check(called_target)); } else { current_target_compatible = - target->compatible_expression(*called_target); + target.generate_compatibility_check(called_target); } first_iter = false; } @@ -203,7 +186,7 @@ exprt assigns_clauset::compatible_expression( { current_target_compatible = or_exprt( current_target_compatible, - target->compatible_expression(*called_target)); + target.generate_compatibility_check(called_target)); } } if(first_clause) @@ -213,10 +196,7 @@ exprt assigns_clauset::compatible_expression( } else { - exprt::operandst conjuncts; - conjuncts.push_back(result); - conjuncts.push_back(current_target_compatible); - result = conjunction(conjuncts); + result = and_exprt(result, current_target_compatible); } } diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index b5a380ec1ef..1a19ed72f06 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Specify write set in function contracts. +Module: Specify write set in code contracts. Author: Felipe R. Monteiro @@ -18,58 +18,53 @@ Date: July 2021 #include -/// \brief A base class for assigns clause targets -class assigns_clause_targett +/// \brief A class for representing assigns clauses in code contracts +class assigns_clauset { public: - assigns_clause_targett( - const exprt &object, - code_contractst &contract, - messaget &log_parameter, - const irep_idt &function_id); - ~assigns_clause_targett(); - - exprt alias_expression(const exprt &lhs); - exprt compatible_expression(const assigns_clause_targett &called_target); - const exprt &get_target() const; - - static exprt pointer_for(const exprt &object) + /// \brief A class for representing targets for assigns clauses + class targett { - return address_of_exprt(object); - } + public: + targett(const assigns_clauset &, const exprt &); -protected: - const code_contractst &contract; - goto_programt init_block; - messaget &log; - exprt target; - const irep_idt &target_id; -}; + static exprt normalize(const exprt &); -class assigns_clauset -{ -public: - assigns_clauset( - const exprt &assigns, - code_contractst &contract, - const irep_idt function_id, - messaget log_parameter); - ~assigns_clauset(); - - void add_target(exprt target); - goto_programt havoc_code(); - exprt alias_expression(const exprt &lhs); - exprt compatible_expression(const assigns_clauset &called_assigns); + exprt generate_alias_check(const exprt &) const; + exprt generate_compatibility_check(const targett &) const; -protected: - const exprt &assigns; + bool operator==(const targett &other) const + { + return expr == other.expr; + } - std::vector targets; - goto_programt standin_declarations; + struct hasht + { + std::size_t operator()(const targett &target) const + { + return irep_hash{}(target.expr); + } + }; - code_contractst &parent; - const irep_idt function_id; - messaget log; + const exprt expr; + const irep_idt &id; + const assigns_clauset &parent; + }; + + assigns_clauset(const exprt &, const messaget &, const namespacet &); + + void add_target(const exprt &); + + goto_programt generate_havoc_code() const; + exprt generate_alias_check(const exprt &) const; + exprt generate_compatibility_check(const assigns_clauset &) const; + + const exprt &expr; + const messaget &log; + const namespacet &ns; + +protected: + std::unordered_set targets; }; #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6f9a1c35018..462b1404ec0 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -601,8 +601,8 @@ bool code_contractst::apply_function_contract( // in the assigns clause. if(assigns.is_not_nil()) { - assigns_clauset assigns_cause(assigns, *this, function, log); - goto_programt assigns_havoc = assigns_cause.havoc_code(); + assigns_clauset assigns_cause(assigns, log, ns); + auto assigns_havoc = assigns_cause.generate_havoc_code(); // Insert the non-deterministic assignment immediately before the call site. insert_before_swap_and_advance(goto_program, target, assigns_havoc); @@ -699,7 +699,7 @@ void code_contractst::instrument_assign_statement( { goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( - assigns_clause.alias_expression(lhs), + assigns_clause.generate_alias_check(lhs), instruction_iterator->source_location)); alias_assertion.instructions.back().source_location.set_comment( "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); @@ -762,8 +762,8 @@ void code_contractst::instrument_call_statement( to_symbol_expr(instruction_iterator->call_lhs()).get_identifier()) == freely_assignable_symbols.end()) { - exprt alias_expr = - assigns_clause.alias_expression(instruction_iterator->call_lhs()); + const auto alias_expr = + assigns_clause.generate_alias_check(instruction_iterator->call_lhs()); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( @@ -802,13 +802,12 @@ void code_contractst::instrument_call_statement( replace_formal_params(called_assigns); // check compatibility of assigns clause with the called function - assigns_clauset called_assigns_clause( - called_assigns, *this, called_name, log); - exprt compatible = - assigns_clause.compatible_expression(called_assigns_clause); + assigns_clauset called_assigns_clause(called_assigns, log, ns); + const auto compatibility_check = + assigns_clause.generate_compatibility_check(called_assigns_clause); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( - compatible, instruction_iterator->source_location)); + compatibility_check, instruction_iterator->source_location)); alias_assertion.instructions.back().source_location.set_comment( "Check compatibility of assigns clause with the called function"); program.insert_before_swap(instruction_iterator, alias_assertion); @@ -910,7 +909,7 @@ void code_contractst::check_frame_conditions( const auto &type = to_code_with_contract_type(target.type); exprt assigns_expr = type.assigns(); - assigns_clauset assigns(assigns_expr, *this, target.name, log); + assigns_clauset assigns(assigns_expr, log, ns); // Create a list of variables that are okay to assign. std::set freely_assignable_symbols; From 2834e848a42a28228cb8490a7ed5e500619548a7 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 10 Sep 2021 21:27:29 +0000 Subject: [PATCH 2/3] Fix alias checks within assigns clause assigns_clauset was calling `compatible_expression` (not `alias_expression`) on each target, and was thus only comparing the object IDs (not offsets and sizes). We fix this by removing `compatible_expression` entirely and calling `alias_expression` for each from assigns_clauset. --- .../assigns_validity_pointer_04/test.desc | 11 +- .../test_aliasing_ensure_indirect/test.desc | 2 +- src/goto-instrument/contracts/assigns.cpp | 112 ++++++------------ src/goto-instrument/contracts/assigns.h | 10 +- src/goto-instrument/contracts/contracts.cpp | 16 +-- 5 files changed, 61 insertions(+), 90 deletions(-) diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc index 98d5c698b9f..28accca893f 100644 --- a/regression/contracts/assigns_validity_pointer_04/test.desc +++ b/regression/contracts/assigns_validity_pointer_04/test.desc @@ -1,6 +1,6 @@ -CORE +KNOWNBUG main.c ---enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz +--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ @@ -13,8 +13,13 @@ ASSUME .*::tmp_if_expr ASSUME \*z = 7 -- -- -Verification: 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/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 67f44e427c6..3c408d3b146 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -7,7 +7,7 @@ main.c \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS \[bar.\d+\] line \d+ Check that z is assignable: SUCCESS \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.\d+\] line \d+ Check compatibility of assigns clause with the called function: SUCCESS +\[foo.\d+\] line \d+ Check that callee's assigns clause is a subset of caller's: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 1b6fc7a86d5..454b2469179 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -22,7 +22,10 @@ Date: July 2021 assigns_clauset::targett::targett( const assigns_clauset &parent, const exprt &expr) - : expr(address_of_exprt(expr)), id(expr.id()), parent(parent) + : address(address_of_exprt(normalize(expr))), + expr(expr), + id(expr.id()), + parent(parent) { } @@ -38,18 +41,18 @@ exprt assigns_clauset::targett::normalize(const exprt &expr) return to_index_expr(object).array(); } -exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const +exprt assigns_clauset::targett::generate_containment_check( + const address_of_exprt &lhs_address) const { exprt::operandst condition; - const auto lhs_ptr = - (lhs.id() == ID_address_of) ? lhs : address_of_exprt(lhs); // __CPROVER_w_ok(target, sizeof(target)) condition.push_back(w_ok_exprt( - expr, size_of_expr(dereference_exprt(expr).type(), parent.ns).value())); + address, + size_of_expr(dereference_exprt(address).type(), parent.ns).value())); // __CPROVER_same_object(lhs, target) - condition.push_back(same_object(lhs_ptr, expr)); + condition.push_back(same_object(lhs_address, address)); // If assigns target was a dereference, comparing objects is enough if(id == ID_dereference) @@ -57,20 +60,21 @@ exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const return conjunction(condition); } - const auto lhs_offset = pointer_offset(lhs_ptr); - const auto own_offset = pointer_offset(expr); + const auto lhs_offset = pointer_offset(lhs_address); + const auto own_offset = pointer_offset(address); // __CPROVER_offset(lhs) >= __CPROVER_offset(target) condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, own_offset)); const auto lhs_region = plus_exprt( typecast_exprt::conditional_cast( - size_of_expr(lhs.type(), parent.ns).value(), lhs_offset.type()), + size_of_expr(lhs_address.object().type(), parent.ns).value(), + lhs_offset.type()), lhs_offset); const exprt own_region = plus_exprt( typecast_exprt::conditional_cast( - size_of_expr(dereference_exprt(expr).type(), parent.ns).value(), + size_of_expr(address.object().type(), parent.ns).value(), own_offset.type()), own_offset); @@ -81,12 +85,6 @@ exprt assigns_clauset::targett::generate_alias_check(const exprt &lhs) const return conjunction(condition); } -exprt assigns_clauset::targett::generate_compatibility_check( - const assigns_clauset::targett &other_target) const -{ - return same_object(other_target.expr, expr); -} - assigns_clauset::assigns_clauset( const exprt &expr, const messaget &log, @@ -101,8 +99,7 @@ assigns_clauset::assigns_clauset( void assigns_clauset::add_target(const exprt &target_expr) { - auto insertion_succeeded = - targets.emplace(*this, targett::normalize(target_expr)).second; + auto insertion_succeeded = targets.emplace(*this, target_expr).second; if(!insertion_succeeded) { @@ -117,87 +114,56 @@ goto_programt assigns_clauset::generate_havoc_code() const { modifiest modifies; for(const auto &target : targets) - modifies.insert(to_address_of_expr(target.expr).object()); + modifies.insert(target.address.object()); goto_programt havoc_statements; append_havoc_code(expr.source_location(), modifies, havoc_statements); return havoc_statements; } -exprt assigns_clauset::generate_alias_check(const exprt &lhs) const +exprt assigns_clauset::generate_containment_check(const exprt &lhs) const { // If write set is empty, no assignment is allowed. if(targets.empty()) - { return false_exprt(); - } + + const auto lhs_address = address_of_exprt(targett::normalize(lhs)); exprt::operandst condition; for(const auto &target : targets) { - condition.push_back(target.generate_alias_check(lhs)); + condition.push_back(target.generate_containment_check(lhs_address)); } return disjunction(condition); } -exprt assigns_clauset::generate_compatibility_check( - const assigns_clauset &called_assigns) const +exprt assigns_clauset::generate_subset_check( + const assigns_clauset &subassigns) const { - if(called_assigns.targets.empty()) - { + if(subassigns.targets.empty()) return true_exprt(); - } - bool first_clause = true; exprt result = true_exprt(); - for(const auto &called_target : called_assigns.targets) + for(const auto &subtarget : subassigns.targets) { - bool first_iter = true; - exprt current_target_compatible = false_exprt(); + // TODO: Optimize the implication generated due to the validity check. + // In some cases, e.g. when `subtarget` is known to be `NULL`, + // the implication can be skipped entirely. See #6105 for more details. + auto validity_check = + w_ok_exprt(subtarget.address, from_integer(0, unsigned_int_type())); + + exprt::operandst current_subtarget_found_conditions; for(const auto &target : targets) { - if(first_iter) - { - // TODO: Optimize the validation below and remove code duplication - // See GitHub issue #6105 for further details - - // Validating the called target through __CPROVER_w_ok() is - // only useful when the called target is a dereference - const auto &called_target_ptr = called_target.expr; - if( - to_address_of_expr(called_target_ptr).object().id() == ID_dereference) - { - // or_exprt is short-circuited, therefore - // target.generate_compatibility_check(*called_target) would not be - // checked on invalid called_targets. - current_target_compatible = or_exprt( - not_exprt(w_ok_exprt( - called_target_ptr, from_integer(0, unsigned_int_type()))), - target.generate_compatibility_check(called_target)); - } - else - { - current_target_compatible = - target.generate_compatibility_check(called_target); - } - first_iter = false; - } - else - { - current_target_compatible = or_exprt( - current_target_compatible, - target.generate_compatibility_check(called_target)); - } - } - if(first_clause) - { - result = current_target_compatible; - first_clause = false; - } - else - { - result = and_exprt(result, current_target_compatible); + current_subtarget_found_conditions.push_back( + target.generate_containment_check(subtarget.address)); } + + auto current_subtarget_found = or_exprt( + not_exprt(validity_check), + disjunction(current_subtarget_found_conditions)); + + result = and_exprt(result, current_subtarget_found); } return result; diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 1a19ed72f06..82c214aa0bf 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -30,8 +30,7 @@ class assigns_clauset static exprt normalize(const exprt &); - exprt generate_alias_check(const exprt &) const; - exprt generate_compatibility_check(const targett &) const; + exprt generate_containment_check(const address_of_exprt &) const; bool operator==(const targett &other) const { @@ -46,7 +45,8 @@ class assigns_clauset } }; - const exprt expr; + const address_of_exprt address; + const exprt &expr; const irep_idt &id; const assigns_clauset &parent; }; @@ -56,8 +56,8 @@ class assigns_clauset void add_target(const exprt &); goto_programt generate_havoc_code() const; - exprt generate_alias_check(const exprt &) const; - exprt generate_compatibility_check(const assigns_clauset &) const; + exprt generate_containment_check(const exprt &) const; + exprt generate_subset_check(const assigns_clauset &) const; const exprt &expr; const messaget &log; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 462b1404ec0..1e076dced7b 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -699,7 +699,7 @@ void code_contractst::instrument_assign_statement( { goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( - assigns_clause.generate_alias_check(lhs), + 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"); @@ -762,8 +762,8 @@ void code_contractst::instrument_call_statement( to_symbol_expr(instruction_iterator->call_lhs()).get_identifier()) == freely_assignable_symbols.end()) { - const auto alias_expr = - assigns_clause.generate_alias_check(instruction_iterator->call_lhs()); + const auto alias_expr = assigns_clause.generate_containment_check( + instruction_iterator->call_lhs()); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( @@ -801,15 +801,15 @@ void code_contractst::instrument_call_statement( } replace_formal_params(called_assigns); - // check compatibility of assigns clause with the called function + // check subset relationship of assigns clause for called function assigns_clauset called_assigns_clause(called_assigns, log, ns); - const auto compatibility_check = - assigns_clause.generate_compatibility_check(called_assigns_clause); + const auto subset_check = + assigns_clause.generate_subset_check(called_assigns_clause); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( - compatibility_check, instruction_iterator->source_location)); + subset_check, instruction_iterator->source_location)); alias_assertion.instructions.back().source_location.set_comment( - "Check compatibility of assigns clause with the called function"); + "Check that callee's assigns clause is a subset of caller's"); program.insert_before_swap(instruction_iterator, alias_assertion); ++instruction_iterator; } From e1e7235003aca3bbc7568f9687b5f395ca486a55 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Thu, 9 Sep 2021 18:44:09 +0000 Subject: [PATCH 3/3] Remove dead symbols from assignable set --- src/goto-instrument/contracts/assigns.cpp | 5 +++++ src/goto-instrument/contracts/assigns.h | 1 + src/goto-instrument/contracts/contracts.cpp | 7 +++++++ 3 files changed, 13 insertions(+) diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 454b2469179..b033cfa8763 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -110,6 +110,11 @@ void assigns_clauset::add_target(const exprt &target_expr) } } +void assigns_clauset::remove_target(const exprt &target_expr) +{ + targets.erase(targett(*this, targett::normalize(target_expr))); +} + goto_programt assigns_clauset::generate_havoc_code() const { modifiest modifies; diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 82c214aa0bf..5b9d334364d 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -54,6 +54,7 @@ class assigns_clauset assigns_clauset(const exprt &, const messaget &, const namespacet &); void add_target(const exprt &); + void remove_target(const exprt &); goto_programt generate_havoc_code() const; exprt generate_containment_check(const exprt &) const; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 1e076dced7b..4aad2ec3b74 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -944,6 +944,13 @@ void code_contractst::check_frame_conditions( 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()); + } } }