diff --git a/doc/cprover-manual/contracts-functions.md b/doc/cprover-manual/contracts-functions.md index 6e0b4c0a07e..d95775719b6 100644 --- a/doc/cprover-manual/contracts-functions.md +++ b/doc/cprover-manual/contracts-functions.md @@ -143,6 +143,27 @@ instruments the code to use the function contract in place of the function implementation wherever is invoked, and the third one runs CBMC to check the program using contracts. +## Pure contracts + +A pure contract is a function definition equipped with a contract and +for which the body consists of a single call to the function +`__CPROVER_pure_contract`: + +```C +ret_t foo(param_t params) +__CPROVER_requires(R) +__CPROVER_assigns(A) +__CPROVER_ensures(E) +{ + __CPROVER_pure_contract(); +} +``` +Using `__CPROVER_pure_contract();` in any other way results in a failed +assertion. + +Calls to pure contracts are globally replaced by goto-instrument when the +flag `--replace-pure-contracts` is specified on the command line. + ## Additional Resources - [Requires \& Ensures Clauses](contracts-requires-and-ensures.md) diff --git a/regression/contracts/pure-contracts/main-fail.c b/regression/contracts/pure-contracts/main-fail.c new file mode 100644 index 00000000000..0444ad45e64 --- /dev/null +++ b/regression/contracts/pure-contracts/main-fail.c @@ -0,0 +1,41 @@ +#include + +char nondet_char(); + +char foo(char *arr, size_t size) + // clang-format off +__CPROVER_requires( + 0 < size && size < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0], arr[size-1]) +__CPROVER_ensures( + arr[0] == __CPROVER_return_value && arr[size-1] == __CPROVER_return_value) +// clang-format on +{ + char retval = nondet_char(); + arr[0] = retval; + arr[size - 1] = retval; + __CPROVER_pure_contract(); + return retval; +} + +char bar(char *arr, size_t size) + // clang-format off +__CPROVER_requires( + 0 < size && size < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0], arr[size-1]) +__CPROVER_ensures( + arr[0] == __CPROVER_return_value && arr[size-1] == __CPROVER_return_value) +// clang-format on +{ + return foo(arr, size); +} + +int main() +{ + size_t size; + char *arr; + bar(arr, size); + return 0; +} diff --git a/regression/contracts/pure-contracts/main.c b/regression/contracts/pure-contracts/main.c new file mode 100644 index 00000000000..6ae1d609772 --- /dev/null +++ b/regression/contracts/pure-contracts/main.c @@ -0,0 +1,36 @@ +#include + +char foo(char *arr, size_t size) + // clang-format off +__CPROVER_requires( + 0 < size && size < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0], arr[size - 1]) +__CPROVER_ensures( + arr[0] == __CPROVER_return_value && arr[size - 1] == __CPROVER_return_value) +// clang-format on +{ + __CPROVER_pure_contract(); +} + +char bar(char *arr, size_t size) + // clang-format off +__CPROVER_requires( + 0 < size && size < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0], arr[size - 1]) +__CPROVER_ensures( + arr[0] == __CPROVER_return_value && arr[size - 1] == __CPROVER_return_value) +// clang-format on + +{ + return foo(arr, size); +} + +int main() +{ + size_t size; + char *arr; + bar(arr, size); + return 0; +} diff --git a/regression/contracts/pure-contracts/test-fail.desc b/regression/contracts/pure-contracts/test-fail.desc new file mode 100644 index 00000000000..b91c78954f8 --- /dev/null +++ b/regression/contracts/pure-contracts/test-fail.desc @@ -0,0 +1,11 @@ +CORE +main-fail.c +--replace-pure-contracts --enforce-contract bar +^main-fail.c.* error: incorrect use of __CPROVER_pure_contract, function contains other instructions$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test demonstrates that an improper use of __CPROVER_pure_contract +is detected and causes a conversion error. diff --git a/regression/contracts/pure-contracts/test.desc b/regression/contracts/pure-contracts/test.desc new file mode 100644 index 00000000000..0901435c53c --- /dev/null +++ b/regression/contracts/pure-contracts/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--replace-pure-contracts --enforce-contract bar +^\[foo.pure_contract.\d+\] line \d+ all calls replaced: (UNREACHABLE|SUCCESS)$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test demonstrates that calls to functions tagged as pure contracts +replaced by the contract when the command line switch --replace-pure-contracts +is used. foo is a pure contract, bar has the same contract and calls foo. +foo gets replaced in bar, and bar satisfies its contract. +The assertion `foo.pure_contract` is UNREACHABLE or SUCCESS when +all calls to foo have actually been replaced by foo's contract. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 104da3a02a0..68096227537 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -499,6 +499,48 @@ void c_typecheck_baset::typecheck_redefinition_non_type( // mismatch. } +/// Tries to match `symbol.value` as a code block containing a +/// single call to `__CPROVER_pure_contract`. +/// Adds a pragma "pure_contract" to the symbol and the +/// `__CPROVER_pure_contract` call when successfull. +void c_typecheck_baset::typecheck_pure_contract(symbolt &symbol) +{ + codet &code = to_code(symbol.value); + if(!can_cast_expr(code)) + return; + + auto &statements = to_code_block(code).statements(); + + if(statements.size() != 1) + return; + + auto &statement = statements.front(); + + if(!can_cast_expr(statement)) + return; + + auto &statement_expr = to_code_expression(statement).expression(); + + if(!can_cast_expr(statement_expr)) + return; + + auto &call_expr = to_side_effect_expr_function_call(statement_expr); + + if(call_expr.arguments().size() != 0) + return; + + auto &function = call_expr.function(); + + if(!can_cast_expr(function)) + return; + auto &symbol_expr = to_symbol_expr(function); + if(symbol_expr.get_identifier() == CPROVER_PREFIX "pure_contract") + { + symbol.location.add_pragma("pure_contract"); + symbol_expr.add_source_location().add_pragma("pure_contract"); + } +} + void c_typecheck_baset::typecheck_function_body(symbolt &symbol) { if(symbol.value.id() != ID_code) @@ -550,7 +592,8 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol) move_symbol(p_symbol, new_p_symbol); } - // typecheck the body code + typecheck_pure_contract(symbol); + typecheck_code(to_code(symbol.value)); // check the labels diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 4ee55c2cde9..a8127462671 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -268,6 +268,8 @@ class c_typecheck_baset: symbolt &old_symbol, symbolt &new_symbol); void typecheck_function_body(symbolt &symbol); + void typecheck_pure_contract(symbolt &symbol); + virtual void do_initializer(symbolt &symbol); static bool is_numeric_type(const typet &src) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 63bfaa3fff0..b2e5f924cd6 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1940,6 +1940,28 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(entry!=asm_label_map.end()) identifier=entry->second; + if(identifier == CPROVER_PREFIX "pure_contract") + { + const auto &loc = f_op.find_source_location(); + bool usage_ok = false; + + for(const auto &pragma : loc.get_pragmas()) + { + const auto s = id2string(pragma.first); + if(!s.compare(0, 13, "pure_contract")) + usage_ok = true; + } + + if(!usage_ok) + { + // throw an error otherwise + error().source_location = loc; + error() << "incorrect use of " << identifier + << ", function contains other instructions" << eom; + throw 0; + } + } + if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { // This is an undeclared function. diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 51de0f7bbfb..7878ef28faa 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -4,6 +4,7 @@ void __VERIFIER_assume(__CPROVER_bool assumption); void __CPROVER_assert(__CPROVER_bool assertion, const char *description); void __CPROVER_precondition(__CPROVER_bool precondition, const char *description); void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description); +void __CPROVER_pure_contract(); void __CPROVER_havoc_object(void *); void __CPROVER_havoc_slice(void *, __CPROVER_size_t); __CPROVER_bool __CPROVER_equal(); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 430535b3b32..11767cbc091 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -133,6 +133,18 @@ class inlining_decoratort : public message_handlert } }; +bool code_contractst::is_pure_contract(const irep_idt &function_id) +{ + for(const auto &pragma : ns.lookup(function_id).location.get_pragmas()) + { + const auto s = id2string(pragma.first); + if(!s.compare(0, 13, "pure_contract")) + return true; + } + + return false; +} + void code_contractst::check_apply_loop_contracts( const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, @@ -1537,6 +1549,17 @@ void code_contractst::check_all_functions_found( } } +void code_contractst::replace_pure_contracts() +{ + std::set to_replace; + for(const auto &it : goto_functions.function_map) + { + if(is_pure_contract(it.first)) + to_replace.insert(id2string(it.first)); + } + replace_calls(to_replace); +} + void code_contractst::replace_calls(const std::set &to_replace) { if(to_replace.empty()) diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 6e3526f187c..d92fe2f58fc 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -36,6 +36,12 @@ Date: February 2016 " --apply-loop-contracts\n" \ " check and use loop contracts when provided\n" +#define FLAG_REPLACE_PURE_CONTRACTS "replace-pure-contracts" +#define HELP_REPLACE_PURE_CONTRACTS \ + " --replace-pure-contracts\n" \ + " replace calls to all functions defined as " \ + " pure contracts with their contracts\n" + #define FLAG_REPLACE_CALL "replace-call-with-contract" #define HELP_REPLACE_CALL \ " --replace-call-with-contract \n" \ @@ -62,6 +68,10 @@ class code_contractst { } + /// \brief Replace all calls to functions defined pure contracts by their + /// contracts + void replace_pure_contracts(); + /// Throws an exception if some function `functions` is found in the program. void check_all_functions_found(const std::set &functions) const; @@ -128,6 +138,10 @@ class code_contractst std::unordered_set summarized; + /// \brief Returns true iff a function is a pure contract and must + /// automatically be replaced by its contract + bool is_pure_contract(const irep_idt &function_id); + /// \brief Enforce contract of a single function void enforce_contract(const irep_idt &function); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efea60220bd..1e33b0812c1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1133,7 +1133,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() if( cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) || - cmdline.isset(FLAG_ENFORCE_CONTRACT)) + cmdline.isset(FLAG_ENFORCE_CONTRACT) || + cmdline.isset(FLAG_REPLACE_PURE_CONTRACTS)) { do_indirect_call_and_rtti_removal(); code_contractst contracts(goto_model, log); @@ -1150,6 +1151,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() // first replacement then enforcement. We rely on contract replacement // and inlining of sub-function calls to properly annotate all // assignments. + + if(cmdline.isset(FLAG_REPLACE_PURE_CONTRACTS)) + contracts.replace_pure_contracts(); + contracts.replace_calls(to_replace); contracts.enforce_contracts(to_enforce); @@ -1844,6 +1849,7 @@ void goto_instrument_parse_optionst::help() "Code contracts:\n" HELP_LOOP_CONTRACTS HELP_REPLACE_CALL + HELP_REPLACE_PURE_CONTRACTS HELP_ENFORCE_CONTRACT "\n" "Other options:\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 1f79d593a7b..98f65ad0f14 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -96,6 +96,7 @@ Author: Daniel Kroening, kroening@kroening.com "(horn)(skip-loops):(model-argc-argv):" \ "(" FLAG_LOOP_CONTRACTS ")" \ "(" FLAG_REPLACE_CALL "):" \ + "(" FLAG_REPLACE_PURE_CONTRACTS ")" \ "(" FLAG_ENFORCE_CONTRACT "):" \ "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 6847ab93345..d877a8978cf 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -767,7 +767,16 @@ void goto_convertt::do_function_call_symbol( return; } - if(identifier == CPROVER_PREFIX "havoc_slice") + if(identifier == CPROVER_PREFIX "pure_contract") + { + const auto &loc = function.find_source_location(); + goto_programt::targett t = + dest.add(goto_programt::make_assertion(false_exprt(), loc)); + t->source_location_nonconst().set("user-provided", false); + t->source_location_nonconst().set_property_class(ID_pure_contract); + t->source_location_nonconst().set_comment("all calls replaced"); + } + else if(identifier == CPROVER_PREFIX "havoc_slice") { do_havoc_slice(lhs, function, arguments, dest, mode); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f70b9132c43..f1b1598f3b0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -88,6 +88,7 @@ IREP_ID_ONE(assign_bitor) IREP_ID_ONE(assume) IREP_ID_ONE(assert) IREP_ID_ONE(assertion) +IREP_ID_ONE(pure_contract) IREP_ID_ONE(precondition) IREP_ID_ONE(postcondition) IREP_ID_ONE(precondition_instance)