diff --git a/regression/contracts/named-contracts/main-contract-after-declaration.c b/regression/contracts/named-contracts/main-contract-after-declaration.c new file mode 100644 index 00000000000..af7174a40e6 --- /dev/null +++ b/regression/contracts/named-contracts/main-contract-after-declaration.c @@ -0,0 +1,28 @@ +int foo(int *arr, int size); + +int foo(int *arr, int size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns( + arr[0], arr[size-1]; + size >= 10: arr[5]; +) +__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0) +__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value) + // clang-format on + ; + +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + return size < 10 ? 0 : arr[5]; +} + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/contracts/named-contracts/main-contract-after-definition.c b/regression/contracts/named-contracts/main-contract-after-definition.c new file mode 100644 index 00000000000..639f4a95678 --- /dev/null +++ b/regression/contracts/named-contracts/main-contract-after-definition.c @@ -0,0 +1,26 @@ +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + return size < 10 ? 0 : arr[5]; +} + +int foo(int *arr, int size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns( + arr[0], arr[size-1]; + size >= 10: arr[5]; +) +__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0) +__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value) + // clang-format on + ; + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/contracts/named-contracts/main-contract-incomplete.c b/regression/contracts/named-contracts/main-contract-incomplete.c new file mode 100644 index 00000000000..e91bdbf340e --- /dev/null +++ b/regression/contracts/named-contracts/main-contract-incomplete.c @@ -0,0 +1,22 @@ +int foo(int *arr, int size); + +int foo() + // clang-format off +__CPROVER_ensures(__CPROVER_return_value != 0) + // clang-format on + ; + +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + return size < 10 ? 0 : arr[5]; +} + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/contracts/named-contracts/main-contract-signature-conflict.c b/regression/contracts/named-contracts/main-contract-signature-conflict.c new file mode 100644 index 00000000000..b0d1fe6838a --- /dev/null +++ b/regression/contracts/named-contracts/main-contract-signature-conflict.c @@ -0,0 +1,30 @@ +int foo(int *arr, int size); + +#if 0 +int foo() + // clang-format off +__CPROVER_ensures(__CPROVER_return_value != 0) + // clang-format on + ; +#endif + +void foo(int *arr, int size) + // clang-format off +__CPROVER_requires(size > 0) + // clang-format on + ; + +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + return size < 10 ? 0 : arr[5]; +} + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/contracts/named-contracts/main-definition-after-contract.c b/regression/contracts/named-contracts/main-definition-after-contract.c new file mode 100644 index 00000000000..b8c458cb05e --- /dev/null +++ b/regression/contracts/named-contracts/main-definition-after-contract.c @@ -0,0 +1,26 @@ +int foo(int *arr, int size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns( + arr[0], arr[size-1]; + size >= 10: arr[5]; +) +__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0) +__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value) + // clang-format on + ; + +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + return size < 10 ? 0 : arr[5]; +} + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/contracts/named-contracts/main-no-definition.c b/regression/contracts/named-contracts/main-no-definition.c new file mode 100644 index 00000000000..c28e2f188c5 --- /dev/null +++ b/regression/contracts/named-contracts/main-no-definition.c @@ -0,0 +1,28 @@ +int foo(int *arr, int size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns( + arr[0], arr[size-1]; + size >= 10: arr[5]; +) +__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0) +__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value) + // clang-format on + ; + +int main() +{ + int arr[10] = {10, 9, 8, 7, 6, 5, 4, 3, 2, 1}; + int retval = foo(arr, 10); + assert(arr[0] == 0); + assert(arr[1] == 9); + assert(arr[2] == 8); + assert(arr[3] == 7); + assert(arr[4] == 6); + assert(arr[5] == retval); + assert(arr[6] == 4); + assert(arr[7] == 3); + assert(arr[8] == 2); + assert(arr[9] == 0); + return 0; +} diff --git a/regression/contracts/named-contracts/test-contract-after-declaration.desc b/regression/contracts/named-contracts/test-contract-after-declaration.desc new file mode 100644 index 00000000000..3533275f3f4 --- /dev/null +++ b/regression/contracts/named-contracts/test-contract-after-declaration.desc @@ -0,0 +1,10 @@ +CORE +main-contract-after-declaration.c +--replace-call-with-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that we can have a function declaration with a contract after +having seen an earlier declaration of that same function. diff --git a/regression/contracts/named-contracts/test-contract-after-definition.desc b/regression/contracts/named-contracts/test-contract-after-definition.desc new file mode 100644 index 00000000000..bbfeda27862 --- /dev/null +++ b/regression/contracts/named-contracts/test-contract-after-definition.desc @@ -0,0 +1,10 @@ +CORE +main-contract-after-definition.c +--replace-call-with-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that we can have a function declaration with a contract after +having seen that function's definition. diff --git a/regression/contracts/named-contracts/test-contract-incomplete.desc b/regression/contracts/named-contracts/test-contract-incomplete.desc new file mode 100644 index 00000000000..95fd11fea25 --- /dev/null +++ b/regression/contracts/named-contracts/test-contract-incomplete.desc @@ -0,0 +1,10 @@ +CORE +main-contract-incomplete.c + +error: code contract on incomplete function re-declaration +CONVERSION ERROR +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that contracts on incomplete re-declarations are rejected. diff --git a/regression/contracts/named-contracts/test-contract-signature-conflict.desc b/regression/contracts/named-contracts/test-contract-signature-conflict.desc new file mode 100644 index 00000000000..48f78bc5a6b --- /dev/null +++ b/regression/contracts/named-contracts/test-contract-signature-conflict.desc @@ -0,0 +1,10 @@ +CORE +main-contract-signature-conflict.c +--enforce-contract foo +^Contract of 'foo' has different signature\.$ +^EXIT=6$ +^SIGNAL=0$ +-- +-- +This test checks that contracts on function declarations with a matching name +but different type are rejected. diff --git a/regression/contracts/named-contracts/test-definition-after-contract.desc b/regression/contracts/named-contracts/test-definition-after-contract.desc new file mode 100644 index 00000000000..c4122381f08 --- /dev/null +++ b/regression/contracts/named-contracts/test-definition-after-contract.desc @@ -0,0 +1,11 @@ +CORE +main-definition-after-contract.c +--replace-call-with-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that we can have a function declaration with a contract and +without body, then the function definition, and successfully replace a call to +the function by the contract. diff --git a/regression/contracts/named-contracts/test-no-definition.desc b/regression/contracts/named-contracts/test-no-definition.desc new file mode 100644 index 00000000000..b7c21d92b16 --- /dev/null +++ b/regression/contracts/named-contracts/test-no-definition.desc @@ -0,0 +1,10 @@ +CORE +main-no-definition.c +--replace-call-with-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that we can have a function declaration with a contract and +without body and replace a call to the function by the contract. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index bc609740bb5..287c9f0e13f 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include "ansi_c_declaration.h" @@ -153,7 +154,9 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol) { typecheck_function_body(symbol); } - else + else if( + symbol.is_macro || + !to_code_with_contract_type(symbol.type).has_contract()) { // we don't need the identifiers for(auto ¶meter : to_code_type(symbol.type).parameters()) @@ -370,7 +373,15 @@ void c_typecheck_baset::typecheck_redefinition_non_type( if(old_ct.has_ellipsis() && !new_ct.has_ellipsis()) old_ct=new_ct; else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis()) + { + if(to_code_with_contract_type(new_ct).has_contract()) + { + error().source_location = new_symbol.location; + error() << "code contract on incomplete function re-declaration" << eom; + throw 0; + } new_ct=old_ct; + } if(inlined) { @@ -443,6 +454,22 @@ void c_typecheck_baset::typecheck_redefinition_non_type( // overwrite type (because of parameter names) old_symbol.type=new_symbol.type; } + else if(to_code_with_contract_type(new_ct).has_contract()) + { + // overwrite type to add contract, but keep the old parameter identifiers + // (if any) + auto new_parameters_it = new_ct.parameters().begin(); + for(auto &p : old_ct.parameters()) + { + if(new_parameters_it != new_ct.parameters().end()) + { + new_parameters_it->set_identifier(p.get_identifier()); + ++new_parameters_it; + } + } + + old_symbol.type = new_symbol.type; + } return; } @@ -752,17 +779,53 @@ void c_typecheck_baset::typecheck_declaration( // check the contract, if any symbolt &new_symbol = symbol_table.get_writeable_ref(identifier); - if(new_symbol.type.id() == ID_code) + if( + new_symbol.type.id() == ID_code && + to_code_with_contract_type(new_symbol.type).has_contract()) { - // We typecheck this after the - // function body done above, so as to have parameter symbols - // available - auto &code_type = to_code_with_contract_type(new_symbol.type); + code_with_contract_typet code_type = + to_code_with_contract_type(new_symbol.type); + + // ensure parameter declarations are available for type checking to + // succeed + binding_exprt::variablest temporary_parameter_symbols; + + const auto &return_type = code_type.return_type(); + if(return_type.id() != ID_empty) + { + parameter_map[CPROVER_PREFIX "return_value"] = return_type; + temporary_parameter_symbols.emplace_back( + CPROVER_PREFIX "return_value", return_type); + } + + std::size_t anon_counter = 0; + for(auto &p : code_type.parameters()) + { + // may be anonymous + if(p.get_base_name().empty()) + p.set_base_name("#anon" + std::to_string(anon_counter++)); + + // produce identifier + const irep_idt &base_name = p.get_base_name(); + irep_idt parameter_identifier = + id2string(identifier) + "::" + id2string(base_name); + + p.set_identifier(parameter_identifier); + + PRECONDITION( + parameter_map.find(parameter_identifier) == parameter_map.end()); + parameter_map[parameter_identifier] = p.type(); + temporary_parameter_symbols.emplace_back( + parameter_identifier, p.type()); + } for(auto &expr : code_type.requires_contract()) { typecheck_spec_function_pointer_obeys_contract(expr); check_history_expr(expr); + lambda_exprt lambda{temporary_parameter_symbols, expr}; + lambda.add_source_location() = expr.source_location(); + expr.swap(lambda); } for(auto &requires : code_type.requires()) @@ -770,13 +833,18 @@ void c_typecheck_baset::typecheck_declaration( typecheck_expr(requires); implicit_typecast_bool(requires); check_history_expr(requires); + lambda_exprt lambda{temporary_parameter_symbols, requires}; + lambda.add_source_location() = requires.source_location(); + requires.swap(lambda); } typecheck_spec_assigns(code_type.assigns()); - - const auto &return_type = code_type.return_type(); - if(return_type.id() != ID_empty) - parameter_map[CPROVER_PREFIX "return_value"] = return_type; + for(auto &assigns : code_type.assigns()) + { + lambda_exprt lambda{temporary_parameter_symbols, assigns}; + lambda.add_source_location() = assigns.source_location(); + assigns.swap(lambda); + } for(auto &expr : code_type.ensures_contract()) { @@ -785,23 +853,55 @@ void c_typecheck_baset::typecheck_declaration( expr, ID_loop_entry, CPROVER_PREFIX "loop_entry is not allowed in postconditions."); + lambda_exprt lambda{temporary_parameter_symbols, expr}; + lambda.add_source_location() = expr.source_location(); + expr.swap(lambda); } - if(!as_const(code_type).ensures().empty()) + for(auto &ensures : code_type.ensures()) { - for(auto &ensures : code_type.ensures()) - { - typecheck_expr(ensures); - implicit_typecast_bool(ensures); - disallow_subexpr_by_id( - ensures, - ID_loop_entry, - CPROVER_PREFIX "loop_entry is not allowed in postconditions."); - } + typecheck_expr(ensures); + implicit_typecast_bool(ensures); + disallow_subexpr_by_id( + ensures, + ID_loop_entry, + CPROVER_PREFIX "loop_entry is not allowed in postconditions."); + lambda_exprt lambda{temporary_parameter_symbols, ensures}; + lambda.add_source_location() = ensures.source_location(); + ensures.swap(lambda); } - if(return_type.id() != ID_empty) - parameter_map.erase(CPROVER_PREFIX "return_value"); + for(const auto ¶meter_sym : temporary_parameter_symbols) + parameter_map.erase(parameter_sym.get_identifier()); + + // create a contract symbol + symbolt contract; + contract.name = "contract::" + id2string(new_symbol.name); + contract.base_name = new_symbol.name; + contract.pretty_name = new_symbol.name; + contract.is_property = true; + contract.type = code_type; + contract.mode = new_symbol.mode; + contract.module = module; + contract.location = new_symbol.location; + + auto entry = symbol_table.insert(std::move(contract)); + if(!entry.second) + { + error().source_location = new_symbol.location; + error() << "contract '" << new_symbol.display_name() + << "' already set at " << entry.first.location.as_string() + << eom; + throw 0; + } + + // Remove the contract from the original symbol as we have created a + // dedicated contract symbol. + new_symbol.type.remove(ID_C_spec_assigns); + new_symbol.type.remove(ID_C_spec_ensures); + new_symbol.type.remove(ID_C_spec_ensures_contract); + new_symbol.type.remove(ID_C_spec_requires); + new_symbol.type.remove(ID_C_spec_requires_contract); } } } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 108a902d1d4..c3fb7fc9bc1 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -25,7 +25,6 @@ Date: February 2016 #include #include #include -#include #include #include @@ -740,6 +739,29 @@ code_contractst::create_ensures_instruction( return std::make_pair(std::move(ensures_program), std::move(history)); } +static const code_with_contract_typet & +get_contract(const irep_idt &function, const namespacet &ns) +{ + const std::string &function_str = id2string(function); + const auto &function_symbol = ns.lookup(function); + + const symbolt *contract_sym; + if(ns.lookup("contract::" + function_str, contract_sym)) + { + // no contract provided in the source or just an empty assigns clause + return to_code_with_contract_type(function_symbol.type); + } + + const auto &type = to_code_with_contract_type(contract_sym->type); + if(type != function_symbol.type) + { + throw invalid_input_exceptiont( + "Contract of '" + function_str + "' has different signature."); + } + + return type; +} + void code_contractst::apply_function_contract( const irep_idt &function, const source_locationt &location, @@ -752,24 +774,20 @@ void code_contractst::apply_function_contract( // function pointers. PRECONDITION(const_target->call_function().id() == ID_symbol); - // Retrieve the function type, which is needed to extract the contract - // components. const irep_idt &target_function = to_symbol_expr(const_target->call_function()).get_identifier(); const symbolt &function_symbol = ns.lookup(target_function); - const auto &type = to_code_with_contract_type(function_symbol.type); + const code_typet &function_type = to_code_type(function_symbol.type); // Isolate each component of the contract. + const auto &type = get_contract(target_function, ns); auto assigns_clause = type.assigns(); - auto requires = conjunction(type.requires()); - auto ensures = conjunction(type.ensures()); auto requires_contract = type.requires_contract(); auto ensures_contract = type.ensures_contract(); - // Create a replace_symbolt object, for replacing expressions in the callee + // Prepare to instantiate expressions in the callee // with expressions from the call site (e.g. the return value). - // This object tracks replacements that are common to ENSURES and REQUIRES. - replace_symbolt common_replace; + exprt::operandst instantiation_values; // keep track of the call's return expression to make it nondet later optionalt call_ret_opt = {}; @@ -777,7 +795,7 @@ void code_contractst::apply_function_contract( // if true, the call return variable variable was created during replacement bool call_ret_is_fresh_var = false; - if(type.return_type() != empty_typet()) + if(function_type.return_type() != empty_typet()) { // Check whether the function's return value is not disregarded. if(target->call_lhs().is_not_nil()) @@ -788,50 +806,46 @@ void code_contractst::apply_function_contract( // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5) auto &lhs_expr = const_target->call_lhs(); call_ret_opt = lhs_expr; - symbol_exprt ret_val(CPROVER_PREFIX "return_value", lhs_expr.type()); - common_replace.insert(ret_val, lhs_expr); + instantiation_values.push_back(lhs_expr); } else { // If the function does return a value, but the return value is // disregarded, check if the postcondition includes the return value. - if(has_subexpr(ensures, [](const exprt &e) { - return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == - CPROVER_PREFIX "return_value"; - })) + if(std::any_of( + type.ensures().begin(), type.ensures().end(), [](const exprt &e) { + return has_symbol_expr( + to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true); + })) { // The postcondition does mention __CPROVER_return_value, so mint a // fresh variable to replace __CPROVER_return_value with. call_ret_is_fresh_var = true; const symbolt &fresh = get_fresh_aux_symbol( - type.return_type(), + function_type.return_type(), id2string(target_function), "ignored_return_value", const_target->source_location(), symbol_table.lookup_ref(target_function).mode, ns, symbol_table); - symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type()); auto fresh_sym_expr = fresh.symbol_expr(); - common_replace.insert(ret_val, fresh_sym_expr); call_ret_opt = fresh_sym_expr; + instantiation_values.push_back(fresh_sym_expr); + } + else + { + // unused, add a dummy with the right type + instantiation_values.push_back( + exprt{ID_nil, function_type.return_type()}); } } } // Replace formal parameters const auto &arguments = const_target->call_arguments(); - auto a_it = arguments.begin(); - for(auto p_it = type.parameters().begin(); - p_it != type.parameters().end() && a_it != arguments.end(); - ++p_it, ++a_it) - { - if(!p_it->get_identifier().empty()) - { - symbol_exprt p(p_it->get_identifier(), p_it->type()); - common_replace.insert(p, *a_it); - } - } + instantiation_values.insert( + instantiation_values.end(), arguments.begin(), arguments.end()); const auto &mode = function_symbol.mode; @@ -843,11 +857,20 @@ void code_contractst::apply_function_contract( is_fresh.add_memory_map_decl(new_program); // Insert assertion of the precondition immediately before the call site. + exprt::operandst requires_conjuncts; + for(const auto &r : type.requires()) + { + requires_conjuncts.push_back( + to_lambda_expr(r).application(instantiation_values)); + } + auto requires = conjunction(requires_conjuncts); + requires.add_source_location() = + requires_conjuncts.empty() ? type.source_location() + : type.requires().front().source_location(); if(!requires.is_true()) { if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall)) add_quantified_variable(requires, mode); - common_replace(requires); goto_programt assertion; converter.goto_convert(code_assertt(requires), assertion, mode); @@ -865,21 +888,30 @@ void code_contractst::apply_function_contract( for(auto &expr : requires_contract) { assert_function_pointer_obeys_contract( - to_function_pointer_obeys_contract_expr(expr), + to_function_pointer_obeys_contract_expr( + to_lambda_expr(expr).application(instantiation_values)), ID_precondition, - common_replace, mode, new_program); } // Gather all the instructions required to handle history variables // as well as the ensures clause + exprt::operandst ensures_conjuncts; + for(const auto &r : type.ensures()) + { + ensures_conjuncts.push_back( + to_lambda_expr(r).application(instantiation_values)); + } + auto ensures = conjunction(ensures_conjuncts); + ensures.add_source_location() = ensures_conjuncts.empty() + ? type.source_location() + : type.ensures().front().source_location(); std::pair ensures_pair; if(!ensures.is_false()) { if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall)) add_quantified_variable(ensures, mode); - common_replace(ensures); auto assumption = code_assumet(ensures); ensures_pair = @@ -891,10 +923,9 @@ void code_contractst::apply_function_contract( // ASSIGNS clause should not refer to any quantified variables, // and only refer to the common symbols to be replaced. - exprt targets; + exprt::operandst targets; for(auto &target : assigns_clause) - targets.add_to_operands(std::move(target)); - common_replace(targets); + targets.push_back(to_lambda_expr(target).application(instantiation_values)); // Create a sequence of non-deterministic assignments ... @@ -903,7 +934,7 @@ void code_contractst::apply_function_contract( function_cfg_infot cfg_info({}); havoc_assigns_clause_targetst havocker( target_function, - targets.operands(), + targets, goto_functions, cfg_info, location, @@ -945,8 +976,8 @@ void code_contractst::apply_function_contract( for(auto &expr : ensures_contract) { assume_function_pointer_obeys_contract( - to_function_pointer_obeys_contract_expr(expr), - common_replace, + to_function_pointer_obeys_contract_expr( + to_lambda_expr(expr).application(instantiation_values)), mode, new_program); } @@ -1249,11 +1280,6 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function) const auto &goto_function = function_obj->second; auto &function_body = function_obj->second.body; - // Get assigns clause for function - const symbolt &function_symbol = ns.lookup(function); - const auto &function_with_contract = - to_code_with_contract_type(function_symbol.type); - function_cfg_infot cfg_info(goto_function); instrument_spec_assignst instrument_spec_assigns( @@ -1296,17 +1322,30 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function) insert_before_swap_and_advance( function_body, instruction_it, snapshot_static_locals); - // Track targets mentionned in the specification - for(auto &target : function_with_contract.assigns()) + // Track targets mentioned in the specification + const symbolt &function_symbol = ns.lookup(function); + const code_typet &function_type = to_code_type(function_symbol.type); + exprt::operandst instantiation_values; + // assigns clauses cannot refer to the return value, but we still need an + // element in there to apply the lambda function consistently + if(function_type.return_type() != empty_typet()) + instantiation_values.push_back(exprt{ID_nil, function_type.return_type()}); + for(const auto ¶m : function_type.parameters()) + { + instantiation_values.push_back( + ns.lookup(param.get_identifier()).symbol_expr()); + } + for(auto &target : get_contract(function, ns).assigns()) { goto_programt payload; - instrument_spec_assigns.track_spec_target(target, payload); + instrument_spec_assigns.track_spec_target( + to_lambda_expr(target).application(instantiation_values), payload); insert_before_swap_and_advance(function_body, instruction_it, payload); } // Track formal parameters goto_programt snapshot_function_parameters; - for(const auto ¶m : to_code_type(function_symbol.type).parameters()) + for(const auto ¶m : function_type.parameters()) { goto_programt payload; instrument_spec_assigns.track_stack_allocated( @@ -1382,7 +1421,6 @@ void code_contractst::enforce_contract(const irep_idt &function) void code_contractst::assert_function_pointer_obeys_contract( const function_pointer_obeys_contract_exprt &expr, const irep_idt &property_class, - const replace_symbolt &replace, const irep_idt &mode, goto_programt &dest) { @@ -1394,9 +1432,8 @@ void code_contractst::assert_function_pointer_obeys_contract( << "' obeys contract '" << from_expr_using_mode(ns, mode, expr.contract()) << "'"; loc.set_comment(comment.str()); - exprt function_pointer(expr.function_pointer()); - replace(function_pointer); - code_assertt assert_expr(equal_exprt{function_pointer, expr.contract()}); + code_assertt assert_expr( + equal_exprt{expr.function_pointer(), expr.contract()}); assert_expr.add_source_location() = loc; goto_programt instructions; converter.goto_convert(assert_expr, instructions, mode); @@ -1405,7 +1442,6 @@ void code_contractst::assert_function_pointer_obeys_contract( void code_contractst::assume_function_pointer_obeys_contract( const function_pointer_obeys_contract_exprt &expr, - const replace_symbolt &replace, const irep_idt &mode, goto_programt &dest) { @@ -1416,10 +1452,8 @@ void code_contractst::assume_function_pointer_obeys_contract( << "' obeys contract '" << from_expr_using_mode(ns, mode, expr.contract()) << "'"; loc.set_comment(comment.str()); - exprt function_pointer(expr.function_pointer()); - replace(function_pointer); - dest.add( - goto_programt::make_assignment(function_pointer, expr.contract(), loc)); + dest.add(goto_programt::make_assignment( + expr.function_pointer(), expr.contract(), loc)); } void code_contractst::add_contract_check( @@ -1429,38 +1463,29 @@ void code_contractst::add_contract_check( { PRECONDITION(!dest.instructions.empty()); - const symbolt &function_symbol = ns.lookup(mangled_function); - const auto &code_type = to_code_with_contract_type(function_symbol.type); - + const auto &code_type = get_contract(wrapper_function, ns); auto assigns = code_type.assigns(); - auto requires = conjunction(code_type.requires()); - auto ensures = conjunction(code_type.ensures()); auto requires_contract = code_type.requires_contract(); auto ensures_contract = code_type.ensures_contract(); // build: - // if(nondet) - // decl ret - // decl parameter1 ... - // decl history_parameter1 ... [optional] - // assume(requires) [optional] - // ret=function(parameter1, ...) - // assert(ensures) - // skip: ... - - // build skip so that if(nondet) can refer to it - goto_programt tmp_skip; - goto_programt::targett skip = - tmp_skip.add(goto_programt::make_skip(ensures.source_location())); + // decl ret + // decl parameter1 ... + // decl history_parameter1 ... [optional] + // assume(requires) [optional] + // ret=function(parameter1, ...) + // assert(ensures) goto_programt check; // prepare function call including all declarations + const symbolt &function_symbol = ns.lookup(mangled_function); code_function_callt call(function_symbol.symbol_expr()); - // Create a replace_symbolt object, for replacing expressions in the callee + // Prepare to instantiate expressions in the callee // with expressions from the call site (e.g. the return value). - // This object tracks replacements that are common to ENSURES and REQUIRES. - replace_symbolt common_replace; + exprt::operandst instantiation_values; + + const auto &source_location = function_symbol.location; // decl ret optionalt return_stmt; @@ -1468,17 +1493,16 @@ void code_contractst::add_contract_check( { symbol_exprt r = new_tmp_symbol( code_type.return_type(), - skip->source_location(), + source_location, function_symbol.mode, symbol_table) .symbol_expr(); - check.add(goto_programt::make_decl(r, skip->source_location())); + check.add(goto_programt::make_decl(r, source_location)); call.lhs() = r; return_stmt = code_returnt(r); - symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); - common_replace.insert(ret_val, r); + instantiation_values.push_back(r); } // decl parameter1 ... @@ -1493,28 +1517,37 @@ void code_contractst::add_contract_check( const symbolt ¶meter_symbol = ns.lookup(parameter); symbol_exprt p = new_tmp_symbol( parameter_symbol.type, - skip->source_location(), + source_location, parameter_symbol.mode, symbol_table) .symbol_expr(); - check.add(goto_programt::make_decl(p, skip->source_location())); + check.add(goto_programt::make_decl(p, source_location)); check.add(goto_programt::make_assignment( - p, parameter_symbol.symbol_expr(), skip->source_location())); + p, parameter_symbol.symbol_expr(), source_location)); call.arguments().push_back(p); - common_replace.insert(parameter_symbol.symbol_expr(), p); + instantiation_values.push_back(p); } is_fresh_enforcet visitor(*this, log, wrapper_function); visitor.create_declarations(); visitor.add_memory_map_decl(check); // Generate: assume(requires) + exprt::operandst requires_conjuncts; + for(const auto &r : code_type.requires()) + { + requires_conjuncts.push_back( + to_lambda_expr(r).application(instantiation_values)); + } + auto requires = conjunction(requires_conjuncts); + requires.add_source_location() = + requires_conjuncts.empty() ? code_type.source_location() + : code_type.requires().front().source_location(); if(!requires.is_false()) { if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall)) add_quantified_variable(requires, function_symbol.mode); - common_replace(requires); goto_programt assumption; converter.goto_convert( @@ -1527,11 +1560,20 @@ void code_contractst::add_contract_check( std::pair ensures_pair; // Generate: copies for history variables + exprt::operandst ensures_conjuncts; + for(const auto &r : code_type.ensures()) + { + ensures_conjuncts.push_back( + to_lambda_expr(r).application(instantiation_values)); + } + auto ensures = conjunction(ensures_conjuncts); + ensures.add_source_location() = + ensures_conjuncts.empty() ? code_type.source_location() + : code_type.ensures().front().source_location(); if(!ensures.is_true()) { if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall)) add_quantified_variable(ensures, function_symbol.mode); - common_replace(ensures); // get all the relevant instructions related to history variables auto assertion = code_assertt(ensures); @@ -1554,14 +1596,14 @@ void code_contractst::add_contract_check( for(auto &expr : requires_contract) { assume_function_pointer_obeys_contract( - to_function_pointer_obeys_contract_expr(expr), - common_replace, + to_function_pointer_obeys_contract_expr( + to_lambda_expr(expr).application(instantiation_values)), function_symbol.mode, check); } // ret=mangled_function(parameter1, ...) - check.add(goto_programt::make_function_call(call, skip->source_location())); + check.add(goto_programt::make_function_call(call, source_location)); // Generate: assert(ensures) if(ensures.is_not_nil()) @@ -1573,24 +1615,21 @@ void code_contractst::add_contract_check( for(auto &expr : ensures_contract) { assert_function_pointer_obeys_contract( - to_function_pointer_obeys_contract_expr(expr), + to_function_pointer_obeys_contract_expr( + to_lambda_expr(expr).application(instantiation_values)), ID_postcondition, - common_replace, function_symbol.mode, check); } if(code_type.return_type() != empty_typet()) { check.add(goto_programt::make_set_return_value( - return_stmt.value().return_value(), skip->source_location())); + return_stmt.value().return_value(), source_location)); } // kill the is_fresh memory map visitor.add_memory_map_dead(check); - // add final instruction - check.destructive_append(tmp_skip); - // prepend the new code to dest dest.destructive_insert(dest.instructions.begin(), check); diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 32b10baaa22..ba8b2a2bd25 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -48,7 +48,6 @@ Date: February 2016 " --enforce-contract wrap fun with an assertion of its contract\n" class local_may_aliast; -class replace_symbolt; class instrument_spec_assignst; class cfg_infot; class function_pointer_obeys_contract_exprt; @@ -148,14 +147,11 @@ class code_contractst /// ``` /// \param expr expression to translate /// \param property_class property class to use for the generated assertions - /// \param replace symbol substitution to use in the context where the - /// expression is translated /// \param mode language mode to use for goto_conversion and prints /// \param dest goto_program where generated instructions are appended void assert_function_pointer_obeys_contract( const function_pointer_obeys_contract_exprt &expr, const irep_idt &property_class, - const replace_symbolt &replace, const irep_idt &mode, goto_programt &dest); @@ -164,13 +160,10 @@ class code_contractst /// ASSIGN function_pointer = contract; /// ``` /// \param expr expression to translate - /// \param replace symbol substitution to use in the context where the - /// expression is translated /// \param mode language mode to use for goto_conversion and prints /// \param dest goto_program where generated instructions are appended void assume_function_pointer_obeys_contract( const function_pointer_obeys_contract_exprt &expr, - const replace_symbolt &replace, const irep_idt &mode, goto_programt &dest); diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp index af1ba14e9ab..e3cd1c11daa 100644 --- a/src/goto-instrument/horn_encoding.cpp +++ b/src/goto-instrument/horn_encoding.cpp @@ -699,12 +699,6 @@ static exprt simplifying_not(exprt src) return not_exprt(src); } -static bool has_contract(const code_with_contract_typet &contract) -{ - return !contract.assigns().empty() || !contract.requires().empty() || - !contract.ensures().empty(); -} - void state_encodingt::function_call_symbol( goto_programt::const_targett loc, encoding_targett &dest) @@ -1007,7 +1001,7 @@ void state_encoding( const auto &symbol = ns.lookup(f->first); if( f->first == goto_functionst::entry_point() || - has_contract(to_code_with_contract_type(symbol.type))) + to_code_with_contract_type(symbol.type).has_contract()) { dest.annotation(""); dest.annotation("function " + id2string(f->first)); diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index b4186f4c9f7..834c098a982 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -1101,6 +1101,11 @@ void linkingt::duplicate_non_type_symbol( symbolt &old_symbol, symbolt &new_symbol) { + // we do not permit multiple contracts to be defined, or cases where only one + // of the symbols is a contract + if(old_symbol.is_property || new_symbol.is_property) + link_error(old_symbol, new_symbol, "conflict on code contract"); + // see if it is a function or a variable bool is_code_old_symbol=old_symbol.type.id()==ID_code; diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 118be47b5c2..5563b1b835c 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -67,12 +67,16 @@ static void get_symbols( to_code_with_contract_type(code_type); find_symbols_sett new_symbols; + for(const exprt &a : maybe_contract.assigns()) + find_type_and_expr_symbols(a, new_symbols); for(const exprt &e : maybe_contract.ensures()) find_type_and_expr_symbols(e, new_symbols); + for(const exprt &e : maybe_contract.ensures_contract()) + find_type_and_expr_symbols(e, new_symbols); for(const exprt &r : maybe_contract.requires()) find_type_and_expr_symbols(r, new_symbols); - for(const exprt &a : maybe_contract.assigns()) - find_type_and_expr_symbols(a, new_symbols); + for(const exprt &r : maybe_contract.requires_contract()) + find_type_and_expr_symbols(r, new_symbols); for(const auto &s : new_symbols) { @@ -180,6 +184,7 @@ void remove_internal_symbols( bool is_type=symbol.is_type; bool has_body=symbol.value.is_not_nil(); bool has_initializer = symbol.value.is_not_nil(); + bool is_contract = is_function && symbol.is_property; // __attribute__((constructor)), __attribute__((destructor)) if(symbol.mode==ID_C && is_function && is_file_local) @@ -208,6 +213,8 @@ void remove_internal_symbols( { get_symbols(ns, symbol, exported); } + else if(is_contract) + get_symbols(ns, symbol, exported); } else { diff --git a/src/util/c_types.h b/src/util/c_types.h index ab1a614eacf..e9b922a709f 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -366,6 +366,13 @@ class code_with_contract_typet : public code_typet { } + bool has_contract() const + { + return !ensures().empty() || !ensures_contract().empty() || + !requires().empty() || !requires_contract().empty() || + !assigns().empty(); + } + const exprt::operandst &assigns() const { return static_cast(find(ID_C_spec_assigns)).operands(); diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp index a44369fbc34..2c1cfebf36d 100644 --- a/src/util/rename_symbol.cpp +++ b/src/util/rename_symbol.cpp @@ -162,6 +162,50 @@ bool rename_symbolt::rename(typet &dest) const result=false; } } + + const exprt &spec_assigns = + static_cast(dest.find(ID_C_spec_assigns)); + if(spec_assigns.is_not_nil() && have_to_rename(spec_assigns)) + { + rename(static_cast(dest.add(ID_C_spec_assigns))); + result = false; + } + + const exprt &spec_ensures = + static_cast(dest.find(ID_C_spec_ensures)); + if(spec_ensures.is_not_nil() && have_to_rename(spec_ensures)) + { + rename(static_cast(dest.add(ID_C_spec_ensures))); + result = false; + } + + const exprt &spec_ensures_contract = + static_cast(dest.find(ID_C_spec_ensures_contract)); + if( + spec_ensures_contract.is_not_nil() && + have_to_rename(spec_ensures_contract)) + { + rename(static_cast(dest.add(ID_C_spec_ensures_contract))); + result = false; + } + + const exprt &spec_requires = + static_cast(dest.find(ID_C_spec_requires)); + if(spec_requires.is_not_nil() && have_to_rename(spec_requires)) + { + rename(static_cast(dest.add(ID_C_spec_requires))); + result = false; + } + + const exprt &spec_requires_contract = + static_cast(dest.find(ID_C_spec_requires_contract)); + if( + spec_requires_contract.is_not_nil() && + have_to_rename(spec_requires_contract)) + { + rename(static_cast(dest.add(ID_C_spec_requires_contract))); + result = false; + } } else if(dest.id()==ID_c_enum_tag || dest.id()==ID_struct_tag || @@ -225,6 +269,39 @@ bool rename_symbolt::have_to_rename(const typet &dest) const if(expr_map.find(p.get_identifier()) != expr_map.end()) return true; } + + const exprt &spec_assigns = + static_cast(dest.find(ID_C_spec_assigns)); + if(spec_assigns.is_not_nil() && have_to_rename(spec_assigns)) + return true; + + const exprt &spec_ensures = + static_cast(dest.find(ID_C_spec_ensures)); + if(spec_ensures.is_not_nil() && have_to_rename(spec_ensures)) + return true; + + const exprt &spec_ensures_contract = + static_cast(dest.find(ID_C_spec_ensures_contract)); + if( + spec_ensures_contract.is_not_nil() && + have_to_rename(spec_ensures_contract)) + { + return true; + } + + const exprt &spec_requires = + static_cast(dest.find(ID_C_spec_requires)); + if(spec_requires.is_not_nil() && have_to_rename(spec_requires)) + return true; + + const exprt &spec_requires_contract = + static_cast(dest.find(ID_C_spec_requires_contract)); + if( + spec_requires_contract.is_not_nil() && + have_to_rename(spec_requires_contract)) + { + return true; + } } else if(dest.id()==ID_c_enum_tag || dest.id()==ID_struct_tag || diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 3e74096abbf..71cc2da13ed 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -231,6 +231,41 @@ bool replace_symbolt::replace(typet &dest) const for(auto &p : code_type.parameters()) if(!replace(p)) result=false; + + const exprt &spec_assigns = + static_cast(dest.find(ID_C_spec_assigns)); + if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns)) + result &= replace(static_cast(dest.add(ID_C_spec_assigns))); + + const exprt &spec_ensures = + static_cast(dest.find(ID_C_spec_ensures)); + if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures)) + result &= replace(static_cast(dest.add(ID_C_spec_ensures))); + + const exprt &spec_ensures_contract = + static_cast(dest.find(ID_C_spec_ensures_contract)); + if( + spec_ensures_contract.is_not_nil() && + have_to_replace(spec_ensures_contract)) + { + result &= + replace(static_cast(dest.add(ID_C_spec_ensures_contract))); + } + + const exprt &spec_requires = + static_cast(dest.find(ID_C_spec_requires)); + if(spec_requires.is_not_nil() && have_to_replace(spec_requires)) + result &= replace(static_cast(dest.add(ID_C_spec_requires))); + + const exprt &spec_requires_contract = + static_cast(dest.find(ID_C_spec_requires_contract)); + if( + spec_requires_contract.is_not_nil() && + have_to_replace(spec_requires_contract)) + { + result &= + replace(static_cast(dest.add(ID_C_spec_requires_contract))); + } } else if(dest.id()==ID_array) { @@ -276,6 +311,39 @@ bool replace_symbolt::have_to_replace(const typet &dest) const for(const auto &p : code_type.parameters()) if(have_to_replace(p)) return true; + + const exprt &spec_assigns = + static_cast(dest.find(ID_C_spec_assigns)); + if(spec_assigns.is_not_nil() && have_to_replace(spec_assigns)) + return true; + + const exprt &spec_ensures = + static_cast(dest.find(ID_C_spec_ensures)); + if(spec_ensures.is_not_nil() && have_to_replace(spec_ensures)) + return true; + + const exprt &spec_ensures_contract = + static_cast(dest.find(ID_C_spec_ensures_contract)); + if( + spec_ensures_contract.is_not_nil() && + have_to_replace(spec_ensures_contract)) + { + return true; + } + + const exprt &spec_requires = + static_cast(dest.find(ID_C_spec_requires)); + if(spec_requires.is_not_nil() && have_to_replace(spec_requires)) + return true; + + const exprt &spec_requires_contract = + static_cast(dest.find(ID_C_spec_requires_contract)); + if( + spec_requires_contract.is_not_nil() && + have_to_replace(spec_requires_contract)) + { + return true; + } } else if(dest.id()==ID_array) return have_to_replace(to_array_type(dest).size());