diff --git a/regression/contracts-dfcc/function-contract-mapping/main.c b/regression/contracts-dfcc/function-contract-mapping/main.c new file mode 100644 index 00000000000..49fe3fce9af --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/main.c @@ -0,0 +1,40 @@ +#include +#include + +bool my_contract(char *arr, size_t size, char *out) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(arr, size)) +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +__CPROVER_assigns((size > 0) : arr[0], *out) +__CPROVER_ensures( + (size > 0) ==> __CPROVER_return_value && + (arr[0] == 0) && + (*out == __CPROVER_old(arr[0]))) +__CPROVER_ensures( + (size == 0) ==> !__CPROVER_return_value) + // clang-format on + ; + +bool bar(char *arr, size_t size, char *out) +{ + if(size > 0) + { + *out = arr[0]; + arr[0] = 0; + return true; + } + return false; +} + +bool foo(char *arr, size_t size, char *out) +{ + return bar(arr, size, out); +} + +void main() +{ + char *arr; + size_t size; + char *out; + foo(arr, size, out); +} diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-contract.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-contract.desc new file mode 100644 index 00000000000..c82e9c424db --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-contract.desc @@ -0,0 +1,10 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/ _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^Invalid function-contract mapping$ +^Reason: couldn't find contract name after '/' in 'foo/'$ +^EXIT=(10|6)$ +^SIGNAL=0$ +-- +-- +Checks that when the contract name is missing an error is triggered. diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-function.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-function.desc new file mode 100644 index 00000000000..a1d3bc852b2 --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-function.desc @@ -0,0 +1,10 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract /my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^Invalid function-contract mapping$ +^Reason: couldn't find function name before '/' in '/my_contract'$ +^EXIT=(10|6)$ +^SIGNAL=0$ +-- +-- +Checks that when the function name is missing an error is triggered. diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-too-many.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-too-many.desc new file mode 100644 index 00000000000..33b06ec2b68 --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-too-many.desc @@ -0,0 +1,10 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^Invalid function-contract mapping$ +^Reason: couldn't parse 'foo/bar/my_contract'$ +^EXIT=(10|6)$ +^SIGNAL=0$ +-- +-- +Checks that when the function name is missing an error is triggered. diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-pass.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-pass.desc new file mode 100644 index 00000000000..fadb4e9409c --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-pass.desc @@ -0,0 +1,10 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test demonstrates the ability to specify a function_name/contract_name +mapping for contract checking. diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-replace-pass.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-replace-pass.desc new file mode 100644 index 00000000000..73d6feb243a --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-replace-pass.desc @@ -0,0 +1,13 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract --replace-call-with-contract bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test demonstrates the ability to check specify a function_name/contract_name +mapping for contract checking and contract replacement. + +The same contract `my_contract` is used for both `foo` and `bar` functions in +checking and replacement mode, respectively. diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc new file mode 100644 index 00000000000..a90b06d7b80 --- /dev/null +++ b/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc @@ -0,0 +1,11 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contractt _ --pointer-check --pointer-primitive-check --pointer-overflow-check +^Contract 'my_contractt' not found, deriving empty pure contract 'contract::my_contractt' from function 'foo'$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that we get a warning that a default contract is derived from the +signature of the function being checked when specifying a non-existing contract. diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index a6024782fc5..37b835d64e2 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -29,6 +29,7 @@ Date: February 2016 #include #include +// clang-format off #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" #define HELP_LOOP_CONTRACTS \ " --apply-loop-contracts\n" \ @@ -36,12 +37,14 @@ Date: February 2016 #define FLAG_REPLACE_CALL "replace-call-with-contract" #define HELP_REPLACE_CALL \ - " --replace-call-with-contract \n" \ - " replace calls to fun with fun's contract\n" + " --replace-call-with-contract [/contract]\n" \ + " replace calls to function with contract\n" #define FLAG_ENFORCE_CONTRACT "enforce-contract" #define HELP_ENFORCE_CONTRACT \ - " --enforce-contract wrap fun with an assertion of its contract\n" + " --enforce-contract [/contract]" \ + " wrap function with an assertion of contract\n" +// clang-format on class local_may_aliast; diff --git a/src/goto-instrument/contracts/doc/user/contracts-cli.md b/src/goto-instrument/contracts/doc/user/contracts-cli.md index f283851d389..262a48134e5 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-cli.md +++ b/src/goto-instrument/contracts/doc/user/contracts-cli.md @@ -5,24 +5,27 @@ The program transformation takes the following parameters: ``` -goto-instrument [--apply-loop-contracts] [--enforce-contract f] (--replace-call-with-contract g)* in.gb out.gb +goto-instrument [--apply-loop-contracts] [--enforce-contract ] (--replace-call-with-contract )* in.gb out.gb ``` Where: - `--apply-loop-contracts` is optional and specifies to apply loop contracts globally; -- `--enforce-contract f` is optional and specifies that `f` must be checked against its contract. -- `--replace-call-with-contract g` is optional and specifies that all calls to `g` must be replaced with its contract; +- `--enforce-contract ` is optional and specifies that `function` must be checked against its contract. +- `--replace-call-with-contract ` is optional and specifies that all calls to `function` must be replaced with its contract; ## Applying the function contracts transformation (with the dynamic frames method) The program transformation takes the following parameters: ``` -goto-instrument --dfcc harness [--enforce-contract f] (--replace-call-with-contract g)* [--apply-loop-contracts] in.gb out.gb +goto-instrument --dfcc harness [--enforce-contract [/]] (--replace-call-with-contract [/])* in.gb out.gb ``` Where: - `--dfcc harness` specifies the proof harness (i.e. the entry point of the analysis); -- `--enforce-contract f` is optional and specifies that `f` must be checked against its contract. -- `--replace-call-with-contract g` is optional and specifies that all calls to `g` must be replaced with its contract; +- `--enforce-contract [/]` is optional and specifies that `function` must be checked against `contract`. + When `contract` is not specfied, the contract is assumed to be carried by the `function` itself. +- `--replace-call-with-contract [/]` is optional and specifies that all calls to `function` must be replaced with `contract`. + When `contract` is not specfied, the contract is assumed to be carried by the `function` itself. + diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 4a2307809bf..a523067d19e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -22,6 +22,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include +#include #include #include @@ -47,6 +48,72 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_lift_memory_predicates.h" +invalid_function_contract_pair_exceptiont:: + invalid_function_contract_pair_exceptiont( + std::string reason, + std::string correct_format) + : cprover_exception_baset(std::move(reason)), + correct_format(std::move(correct_format)) +{ +} + +std::string invalid_function_contract_pair_exceptiont::what() const +{ + std::string res; + + res += "Invalid function-contract mapping"; + res += "\nReason: " + reason; + + if(!correct_format.empty()) + { + res += "\nFormat: " + correct_format; + } + + return res; +} + +#include + +static std::pair +parse_function_contract_pair(const irep_idt &cli_flag) +{ + auto const correct_format_message = + "the format for function and contract pairs is " + "`[/]`"; + + std::string cli_flag_str = id2string(cli_flag); + + auto split = split_string(cli_flag_str, '/', true, false); + + if(split.size() == 1) + { + return std::make_pair(cli_flag, cli_flag); + } + else if(split.size() == 2) + { + auto function_name = split[0]; + if(function_name.size() == 0) + { + throw invalid_function_contract_pair_exceptiont{ + "couldn't find function name before '/' in '" + cli_flag_str + "'", + correct_format_message}; + } + auto contract_name = split[1]; + if(contract_name.size() == 0) + { + throw invalid_function_contract_pair_exceptiont{ + "couldn't find contract name after '/' in '" + cli_flag_str + "'", + correct_format_message}; + } + return std::make_pair(function_name, contract_name); + } + else + { + throw invalid_function_contract_pair_exceptiont{ + "couldn't parse '" + cli_flag_str + "'", correct_format_message}; + } +} + void dfcc( const optionst &options, goto_modelt &goto_model, @@ -59,17 +126,15 @@ void dfcc( message_handlert &message_handler) { std::map to_replace_map; - for(const auto &function_id : to_replace) - to_replace_map.insert({function_id, function_id}); + for(const auto &cli_flag : to_replace) + to_replace_map.insert(parse_function_contract_pair(cli_flag)); dfcc( options, goto_model, harness_id, - to_check.has_value() - ? optionalt>( - std::pair(to_check.value(), to_check.value())) - : optionalt>{}, + to_check.has_value() ? parse_function_contract_pair(to_check.value()) + : optionalt>{}, allow_recursive_calls, to_replace_map, apply_loop_contracts, @@ -164,7 +229,7 @@ void dfcct::check_transform_goto_model_preconditions() "' either not found or has no body"); // triggers signature compatibility checking - contract_handler.get_pure_contract_symbol(pair.second); + contract_handler.get_pure_contract_symbol(pair.second, pair.first); PRECONDITION_WITH_DIAGNOSTICS( pair.first != harness_id, @@ -196,7 +261,7 @@ void dfcct::check_transform_goto_model_preconditions() "Function to replace '" + id2string(pair.first) + "' not found"); // triggers signature compatibility checking - contract_handler.get_pure_contract_symbol(pair.second); + contract_handler.get_pure_contract_symbol(pair.second, pair.first); PRECONDITION_WITH_DIAGNOSTICS( pair.first != harness_id, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index fa0d04f67e4..400439c5c0b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -29,6 +29,7 @@ Author: Remi Delmas, delmasrd@amazon.com #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_H +#include #include #include @@ -56,19 +57,32 @@ class optionst; // clang-format off #define HELP_DFCC \ - "--dfcc activate dynamic frame condition checking for function\n"\ - " contracts using given function as entry point" -// clang-format on + "--dfcc activate dynamic frame condition checking for function\n"\ + " contracts using the given harness as entry point" -// clang-format off #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec" #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):" #define HELP_ENFORCE_CONTRACT_REC \ - " --enforce-contract-rec wrap fun with an assertion of its contract\n"\ + " --enforce-contract-rec [/]" \ + " wrap fun with an assertion of the contract\n"\ " and assume recursive calls to fun satisfy \n"\ " the contract" // clang-format on +/// Exception thrown for bad function/contract specification pairs passed on +/// the CLI. +class invalid_function_contract_pair_exceptiont : public cprover_exception_baset +{ +public: + explicit invalid_function_contract_pair_exceptiont( + std::string reason, + std::string correct_format = ""); + + std::string what() const override; + + std::string correct_format; +}; + /// \ingroup dfcc-module /// \brief Applies function contracts transformation to GOTO model, /// using the dynamic frame condition checking approach. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index 9d45026fcc2..b638692a73e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -110,39 +110,56 @@ void dfcc_contract_handlert::add_contract_instructions( .add_to_dest(dest, function_pointer_contracts); } -const symbolt & -dfcc_contract_handlert::get_pure_contract_symbol(const irep_idt &contract_id) +const symbolt &dfcc_contract_handlert::get_pure_contract_symbol( + const irep_idt &contract_id, + const optionalt function_id_opt) { - const auto &contract_symbol = utils.get_function_symbol(contract_id); auto pure_contract_id = "contract::" + id2string(contract_id); const symbolt *pure_contract_symbol = nullptr; if(!ns.lookup(pure_contract_id, pure_contract_symbol)) { - check_signature_compat( - contract_id, - to_code_type(contract_symbol.type), - pure_contract_id, - to_code_type(pure_contract_symbol->type)); + if(function_id_opt.has_value()) + { + auto function_id = function_id_opt.value(); + const auto &function_symbol = utils.get_function_symbol(function_id); + check_signature_compat( + function_id, + to_code_type(function_symbol.type), + pure_contract_id, + to_code_type(pure_contract_symbol->type)); + } return *pure_contract_symbol; } else { // The contract symbol might not have been created if the function had // no contract or a contract with all empty clauses (which is equivalent). - // in that case we create a fresh symbol again with empty clauses - symbolt new_symbol; - new_symbol.name = pure_contract_id; + // in that case we create a fresh symbol again with empty clauses. + PRECONDITION_WITH_DIAGNOSTICS( + function_id_opt.has_value(), + "Contract '" + pure_contract_id + + "' not found, the identifier of an existing function must be provided " + "to derive a default contract"); + + auto function_id = function_id_opt.value(); + const auto &function_symbol = utils.get_function_symbol(function_id); + + log.warning() << "Contract '" << contract_id + << "' not found, deriving empty pure contract '" + << pure_contract_id << "' from function '" << function_id + << "'" << messaget::eom; + + symbolt new_symbol{ + pure_contract_id, function_symbol.type, function_symbol.mode}; new_symbol.base_name = pure_contract_id; new_symbol.pretty_name = pure_contract_id; new_symbol.is_property = true; - new_symbol.type = contract_symbol.type; - new_symbol.mode = contract_symbol.mode; - new_symbol.module = contract_symbol.module; - new_symbol.location = contract_symbol.location; + new_symbol.module = function_symbol.module; + new_symbol.location = function_symbol.location; auto entry = goto_model.symbol_table.insert(std::move(new_symbol)); INVARIANT( entry.second, - "contract '" + id2string(contract_symbol.display_name()) + + "contract '" + id2string(function_symbol.display_name()) + "' already set at " + id2string(entry.first.location.as_string())); // this lookup will work and set the pointer // no need to check for signature compatibility diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index 2cfdc28aabf..e8c55660908 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -101,18 +101,17 @@ class dfcc_contract_handlert const std::size_t get_assigns_clause_size(const irep_idt &contract_id); /// Searches for a symbol named "contract::contract_id" in the symbol table. - /// - /// If a symbol "contract::contract_id" was found and its type signature is - /// compatible with that of "contract_id" a reference to the symbol is - /// returned. - /// - /// If a symbol "contract::contract_id" was found but its type signature is - /// not compatible with that of "contract_id" an exception is thrown. - /// - /// If a symbol "contract::contract_id" was found, a fresh symbol representing - /// a contract with empty clauses is inserted in the symbol table and a - /// reference to that symbol is returned. - const symbolt &get_pure_contract_symbol(const irep_idt &contract_id); + /// If the "contract::contract_id" is found and \p function_id_opt is present, + /// type signature compatibility is checked between the contract and + /// the function, and an exception is thrown if they are incompatible. + /// If the symbol was not found and \p function_id_opt was provided, + /// the function is used as a template to derive a new default contract with + /// empty requires, empty assigns, empty frees, empty ensures clauses. + /// If the symbol was not found and \p function_id_opt was not provided, a + /// PRECONDITION is triggered. + const symbolt &get_pure_contract_symbol( + const irep_idt &contract_id, + const optionalt function_id_opt = {}); protected: goto_modelt &goto_model;