diff --git a/regression/contracts/function-pointer-contracts-enforce/main.c b/regression/contracts/function-pointer-contracts-enforce/main.c new file mode 100644 index 00000000000..2ec46d402c0 --- /dev/null +++ b/regression/contracts/function-pointer-contracts-enforce/main.c @@ -0,0 +1,62 @@ +#include +#include + +bool nondet_bool(); + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +// requires a fresh array and positive size +// resets the first element to zero +void contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size))) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +// clang-format on +{ +} + +arr_fun_t bar() + // clang-format off + __CPROVER_ensures_contract(__CPROVER_return_value, contract) +// clang-format on +{ + return contract; +} + +// Testing pre-conditions constructs +// Takes a function pointer as input, uses it if its preconditions are met +int foo(char *arr, size_t size, arr_fun_t fun) + // clang-format off +__CPROVER_requires_contract(fun, contract) +__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr && size > 0: arr[0]) +__CPROVER_ensures(arr && size > 0 ==> (arr[0] == 0 && __CPROVER_return_value == 0)) +__CPROVER_ensures(!(arr && size > 0) ==> __CPROVER_return_value == -1) +// clang-format on +{ + if(nondet_bool()) + fun = bar(); // non-deterministically get a function pointer from bar() + + int retval = -1; + if(arr && size > 0) + { + // calls the function pointer to do update the array + fun(arr, size); + retval = 0; + } + return retval; +} + +void main() +{ + size_t size; + char *arr; + arr_fun_t fun; + // The precondition that `fun` obeys `contract` + // and that bar returns a function that obeys `contract` + // are used establish the post-conditions of `foo` + foo(arr, size, fun); +} diff --git a/regression/contracts/function-pointer-contracts-enforce/test.desc b/regression/contracts/function-pointer-contracts-enforce/test.desc new file mode 100644 index 00000000000..818d9befb81 --- /dev/null +++ b/regression/contracts/function-pointer-contracts-enforce/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that we can require that a function pointer satisfies some named +contract when verifying another function, and successfully replace a call to this +function pointer by the contract. diff --git a/regression/contracts/function-pointer-contracts-replace/main.c b/regression/contracts/function-pointer-contracts-replace/main.c new file mode 100644 index 00000000000..0f8f8f83395 --- /dev/null +++ b/regression/contracts/function-pointer-contracts-replace/main.c @@ -0,0 +1,39 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size))) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +// clang-format on +{ +} + +arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun) + // clang-format off +__CPROVER_requires_contract(infun, contract) +__CPROVER_ensures_contract(*outfun, contract) +__CPROVER_ensures_contract(__CPROVER_return_value, contract) +// clang-format on +{ + *outfun = contract; + return infun; +} + +void main() +{ + // establish pre-conditions before replacement + arr_fun_t infun = contract; + + arr_fun_t outfun1 = NULL; + arr_fun_t outfun2 = foo(infun, &outfun1); + + // checking post-conditions after replacement + assert(outfun1 == contract); + assert(outfun2 == contract); +} diff --git a/regression/contracts/function-pointer-contracts-replace/test.desc b/regression/contracts/function-pointer-contracts-replace/test.desc new file mode 100644 index 00000000000..57d14757bba --- /dev/null +++ b/regression/contracts/function-pointer-contracts-replace/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--replace-call-with-contract foo +^\[precondition.\d+] Assert function pointer 'infun' obeys contract 'contract': SUCCESS$ +^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$ +^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that, when replacing a call by its contract, +requires_contract clauses are translated to equality checks +and that ensures_contract are translated to assignments. diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 76a20b8b66c..425d30113f3 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -259,6 +259,12 @@ void ansi_c_convert_typet::read_rec(const typet &type) static_cast(static_cast(type)); requires.push_back(to_unary_expr(as_expr).op()); } + else if(type.id() == ID_C_spec_requires_contract) + { + const exprt &as_expr = + static_cast(static_cast(type)); + requires_contract.push_back(to_unary_expr(as_expr).op()); + } else if(type.id() == ID_C_spec_assigns) { const exprt &as_expr = @@ -273,6 +279,12 @@ void ansi_c_convert_typet::read_rec(const typet &type) static_cast(static_cast(type)); ensures.push_back(to_unary_expr(as_expr).op()); } + else if(type.id() == ID_C_spec_ensures_contract) + { + const exprt &as_expr = + static_cast(static_cast(type)); + ensures_contract.push_back(to_unary_expr(as_expr).op()); + } else other.push_back(type); } @@ -322,12 +334,20 @@ void ansi_c_convert_typet::write(typet &type) if(!requires.empty()) to_code_with_contract_type(type).requires() = std::move(requires); + if(!requires_contract.empty()) + to_code_with_contract_type(type).requires_contract() = + std::move(requires_contract); + if(!assigns.empty()) to_code_with_contract_type(type).assigns() = std::move(assigns); if(!ensures.empty()) to_code_with_contract_type(type).ensures() = std::move(ensures); + if(!ensures_contract.empty()) + to_code_with_contract_type(type).ensures_contract() = + std::move(ensures_contract); + if(constructor || destructor) { if(constructor && destructor) diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 47166506409..83f65ffe3ff 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -47,7 +47,8 @@ class ansi_c_convert_typet:public messaget bool constructor, destructor; // contracts - exprt::operandst assigns, ensures, requires; + exprt::operandst assigns, ensures, requires, ensures_contract, + requires_contract; // storage spec c_storage_spect c_storage_spec; diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index c58c4e41716..4e383b02ce3 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -320,4 +320,96 @@ to_conditional_target_group_expr(exprt &expr) return ret; } +/// \brief A class for expressions representing a +/// `requires_contract(fptr, contract)` clause +/// or an `ensures_contract(fptr, contract)` clause +/// in a function contract. +class function_pointer_obeys_contract_exprt : public exprt +{ +public: + explicit function_pointer_obeys_contract_exprt( + exprt _function_pointer, + exprt _contract) + : exprt(ID_function_pointer_obeys_contract, empty_typet{}) + { + add_to_operands(std::move(_function_pointer)); + add_to_operands(std::move(_contract)); + } + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, + expr.operands().size() == 2, + "function pointer obeys contract expression must have two operands"); + } + + static void validate( + const exprt &expr, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + + const exprt &function_pointer() const + { + return op0(); + } + + exprt &function_pointer() + { + return op0(); + } + + const exprt &contract() const + { + return op1(); + } + + exprt &contract() + { + return op1(); + } +}; + +inline void validate_expr(const function_pointer_obeys_contract_exprt &value) +{ + function_pointer_obeys_contract_exprt::check(value); +} + +template <> +inline bool +can_cast_expr(const exprt &base) +{ + return base.id() == ID_function_pointer_obeys_contract; +} + +/// \brief Cast an exprt to a \ref function_pointer_obeys_contract_exprt +/// +/// \a expr must be known to be \ref function_pointer_obeys_contract_exprt +/// +/// \param expr: Source expression +/// \return Object of type \ref function_pointer_obeys_contract_exprt +inline const function_pointer_obeys_contract_exprt & +to_function_pointer_obeys_contract_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_function_pointer_obeys_contract); + auto &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_function_pointer_obeys_contract_expr(const exprt &expr) +inline function_pointer_obeys_contract_exprt & +to_function_pointer_obeys_contract_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_function_pointer_obeys_contract); + auto &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_ANSI_C_C_EXPR_H diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index efc5cbd787f..b8889276dc8 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -699,6 +699,15 @@ void c_typecheck_baset::typecheck_declaration( typecheck_symbol(symbol); + auto check_history_expr = [&](const exprt expr) { + disallow_subexpr_by_id( + expr, ID_old, CPROVER_PREFIX "old is not allowed in preconditions."); + disallow_subexpr_by_id( + expr, + ID_loop_entry, + CPROVER_PREFIX "loop_entry is not allowed in preconditions."); + }; + // check the contract, if any symbolt &new_symbol = symbol_table.get_writeable_ref(identifier); if(new_symbol.type.id() == ID_code) @@ -708,29 +717,36 @@ void c_typecheck_baset::typecheck_declaration( // available auto &code_type = to_code_with_contract_type(new_symbol.type); + for(auto &expr : code_type.requires_contract()) + { + typecheck_spec_function_pointer_obeys_contract(expr); + check_history_expr(expr); + } + for(auto &requires : code_type.requires()) { typecheck_expr(requires); implicit_typecast_bool(requires); - disallow_subexpr_by_id( - requires, - ID_old, - CPROVER_PREFIX "old is not allowed in preconditions."); - disallow_subexpr_by_id( - requires, - ID_loop_entry, - CPROVER_PREFIX "loop_entry is not allowed in preconditions."); + check_history_expr(requires); } typecheck_spec_assigns(code_type.assigns()); - if(!as_const(code_type).ensures().empty()) - { - const auto &return_type = code_type.return_type(); + const auto &return_type = code_type.return_type(); + if(return_type.id() != ID_empty) + parameter_map[CPROVER_PREFIX "return_value"] = return_type; - if(return_type.id() != ID_empty) - parameter_map[CPROVER_PREFIX "return_value"] = return_type; + for(auto &expr : code_type.ensures_contract()) + { + typecheck_spec_function_pointer_obeys_contract(expr); + disallow_subexpr_by_id( + expr, + ID_loop_entry, + CPROVER_PREFIX "loop_entry is not allowed in postconditions."); + } + if(!as_const(code_type).ensures().empty()) + { for(auto &ensures : code_type.ensures()) { typecheck_expr(ensures); @@ -740,10 +756,10 @@ void c_typecheck_baset::typecheck_declaration( ID_loop_entry, CPROVER_PREFIX "loop_entry is not allowed in postconditions."); } - - if(return_type.id() != ID_empty) - parameter_map.erase(CPROVER_PREFIX "return_value"); } + + if(return_type.id() != ID_empty) + parameter_map.erase(CPROVER_PREFIX "return_value"); } } } diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index bc13f60b943..10dbb1f8196 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -146,6 +146,7 @@ class c_typecheck_baset: virtual void typecheck_start_thread(codet &code); // contracts + virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr); virtual void typecheck_spec_assigns(exprt::operandst &targets); virtual void typecheck_spec_assigns_condition(exprt &condition); virtual void typecheck_spec_assigns_target(exprt &target); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index ff0d9666057..e2924c811d3 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -985,6 +985,88 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) } } +void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( + exprt &expr) +{ + if(!can_cast_expr(expr)) + { + error().source_location = expr.source_location(); + error() << "expected ID_function_pointer_obeys_contract expression in " + "requires_contract/ensures_contract clause, found " + << expr.id() << eom; + throw 0; + } + + auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr); + + validate_expr(obeys_expr); + + // the first parameter must be a function pointer typed assignable path + // expression, without side effects or ternary operator + auto &function_pointer = obeys_expr.function_pointer(); + typecheck_expr(function_pointer); + + if( + function_pointer.type().id() != ID_pointer || + to_pointer_type(function_pointer.type()).subtype().id() != ID_code) + { + error().source_location = expr.source_location(); + error() << "the first parameter of the clause must be a function pointer " + "expression" + << eom; + throw 0; + } + + if(!function_pointer.get_bool(ID_C_lvalue)) + { + error().source_location = function_pointer.source_location(); + error() << "first parameter of the clause must be an lvalue" << eom; + throw 0; + } + + if(has_subexpr(function_pointer, ID_side_effect)) + { + error().source_location = function_pointer.source_location(); + error() << "first parameter of the clause must have no side-effects" << eom; + throw 0; + } + + if(has_subexpr(function_pointer, ID_if)) + { + error().source_location = function_pointer.source_location(); + error() << "first parameter of the clause must have no ternary operator" + << eom; + throw 0; + } + + // second parameter must be the address of a function symbol + auto &contract = obeys_expr.contract(); + typecheck_expr(contract); + + if( + contract.id() != ID_address_of || + to_address_of_expr(contract).object().id() != ID_symbol || + contract.type().id() != ID_pointer || + to_pointer_type(contract.type()).subtype().id() != ID_code) + { + error().source_location = expr.source_location(); + error() << "the second parameter of the requires_contract/ensures_contract " + "clause must be a function symbol" + << eom; + throw 0; + } + + if(function_pointer.type() != contract.type()) + { + error().source_location = expr.source_location(); + error() << "the first and second parameter of the " + "requires_contract/ensures_contract clause must have the same " + "function pointer type " + << eom; + throw 0; + } +} + void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) { exprt::operandst tmp; diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 9b551e196d4..7cd594b68d6 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -204,7 +204,9 @@ extern char *yyansi_ctext; %token TOK_CPROVER_ID "__CPROVER_ID" %token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant" %token TOK_CPROVER_DECREASES "__CPROVER_decreases" +%token TOK_CPROVER_REQUIRES_CONTRACT "__CPROVER_requires_contract" %token TOK_CPROVER_REQUIRES "__CPROVER_requires" +%token TOK_CPROVER_ENSURES_CONTRACT "__CPROVER_ensures_contract" %token TOK_CPROVER_ENSURES "__CPROVER_ensures" %token TOK_CPROVER_ASSIGNS "__CPROVER_assigns" %token TOK_IMPLIES "==>" @@ -3294,6 +3296,24 @@ cprover_function_contract: set($$, ID_C_spec_requires); mto($$, $3); } + | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression ')' + { + $$=$1; + set($$, ID_C_spec_ensures_contract); + exprt tmp(ID_function_pointer_obeys_contract); + tmp.add_to_operands(std::move(parser_stack($3))); + tmp.add_to_operands(std::move(parser_stack($5))); + parser_stack($$).add_to_operands(std::move(tmp)); + } + | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')' + { + $$=$1; + set($$, ID_C_spec_requires_contract); + exprt tmp(ID_function_pointer_obeys_contract); + tmp.add_to_operands(std::move(parser_stack($3))); + tmp.add_to_operands(std::move(parser_stack($5))); + parser_stack($$).add_to_operands(std::move(tmp)); + } | cprover_contract_assigns ; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index a2e48e9f566..884549091fb 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1292,6 +1292,8 @@ __decltype { if(PARSER.cpp98 && {CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; } {CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; } {CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; } +{CPROVER_PREFIX}"requires_contract" { loc(); return TOK_CPROVER_REQUIRES_CONTRACT; } +{CPROVER_PREFIX}"ensures_contract" { loc(); return TOK_CPROVER_ENSURES_CONTRACT; } "\xe2\x88\x80" | "\\forall" { /* Non-standard, obviously. Found in ACSL syntax. */ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index d6638749f4a..14be16bfd2d 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -756,6 +756,8 @@ void code_contractst::apply_function_contract( 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 // with expressions from the call site (e.g. the return value). @@ -852,6 +854,17 @@ void code_contractst::apply_function_contract( new_program.destructive_append(assertion); } + // Translate requires_contract(ptr, contract) clauses to assertions + for(auto &expr : requires_contract) + { + assert_function_pointer_obeys_contract( + to_function_pointer_obeys_contract_expr(expr), + ID_precondition, + common_replace, + mode, + new_program); + } + // Gather all the instructions required to handle history variables // as well as the ensures clause std::pair ensures_pair; @@ -920,6 +933,16 @@ void code_contractst::apply_function_contract( new_program.destructive_append(ensures_pair.first); } + // Translate ensures_contract(ptr, contract) clauses to assumptions + for(auto &expr : ensures_contract) + { + assume_function_pointer_obeys_contract( + to_function_pointer_obeys_contract_expr(expr), + common_replace, + mode, + new_program); + } + // Kill return value variable if fresh if(call_ret_is_fresh_var) { @@ -1346,6 +1369,49 @@ void code_contractst::enforce_contract(const irep_idt &function) add_contract_check(original, mangled, wrapper.body); } +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) +{ + source_locationt loc(expr.source_location()); + loc.set_property_class(property_class); + std::stringstream comment; + comment << "Assert function pointer '" + << from_expr_using_mode(ns, mode, expr.function_pointer()) + << "' 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()}); + assert_expr.add_source_location() = loc; + goto_programt instructions; + converter.goto_convert(assert_expr, instructions, mode); + dest.destructive_append(instructions); +} + +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) +{ + source_locationt loc(expr.source_location()); + std::stringstream comment; + comment << "Assume function pointer '" + << from_expr_using_mode(ns, mode, expr.function_pointer()) + << "' 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)); +} + void code_contractst::add_contract_check( const irep_idt &wrapper_function, const irep_idt &mangled_function, @@ -1359,7 +1425,8 @@ void code_contractst::add_contract_check( 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 @@ -1473,6 +1540,16 @@ void code_contractst::add_contract_check( check.destructive_append(ensures_pair.second); } + // Translate requires_contract(ptr, contract) clauses to assumptions + for(auto &expr : requires_contract) + { + assume_function_pointer_obeys_contract( + to_function_pointer_obeys_contract_expr(expr), + common_replace, + function_symbol.mode, + check); + } + // ret=mangled_function(parameter1, ...) check.add(goto_programt::make_function_call(call, skip->source_location())); @@ -1482,6 +1559,16 @@ void code_contractst::add_contract_check( check.destructive_append(ensures_pair.first); } + // Translate ensures_contract(ptr, contract) clauses to assertions + for(auto &expr : ensures_contract) + { + assert_function_pointer_obeys_contract( + to_function_pointer_obeys_contract_expr(expr), + ID_postcondition, + common_replace, + function_symbol.mode, + check); + } if(code_type.return_type() != empty_typet()) { check.add(goto_programt::make_set_return_value( diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ed989be27c9..04d5078e4b3 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -49,6 +49,7 @@ class local_may_aliast; class replace_symbolt; class instrument_spec_assignst; class cfg_infot; +class function_pointer_obeys_contract_exprt; class code_contractst { @@ -128,6 +129,38 @@ class code_contractst std::unordered_set summarized; + /// Translates a function_pointer_obeys_contract_exprt into an assertion + /// ``` + /// ASSERT function_pointer == contract; + /// ``` + /// \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); + + /// Translates a function_pointer_obeys_contract_exprt into an assignment + /// ``` + /// 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); + /// \brief Enforce contract of a single function void enforce_contract(const irep_idt &function); diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index a471cd5c652..5e058af5176 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -8,15 +8,33 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "language_util.h" -#include - -#include +#include #include #include +#include #include "language.h" #include "mode.h" +#include + +std::string from_expr_using_mode( + const namespacet &ns, + const irep_idt &mode, + const exprt &expr) +{ + std::unique_ptr language = (mode == ID_unknown) + ? get_default_language() + : get_language_from_mode(mode); + INVARIANT( + language, "could not retrieve language for mode '" + id2string(mode) + "'"); + + std::string result; + language->from_expr(expr, result, ns); + + return result; +} + std::string from_expr( const namespacet &ns, const irep_idt &identifier, diff --git a/src/langapi/language_util.h b/src/langapi/language_util.h index 9893aea4b68..9e7f87466af 100644 --- a/src/langapi/language_util.h +++ b/src/langapi/language_util.h @@ -16,6 +16,13 @@ class exprt; class namespacet; class typet; +/// Formats an expression using the given namespace, +/// using the given mode to retrieve the language printer. +std::string from_expr_using_mode( + const namespacet &ns, + const irep_idt &mode, + const exprt &expr); + std::string from_expr( const namespacet &ns, const irep_idt &identifier, diff --git a/src/util/c_types.h b/src/util/c_types.h index ed67a5edfe2..ab1a614eacf 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -376,6 +376,17 @@ class code_with_contract_typet : public code_typet return static_cast(add(ID_C_spec_assigns)).operands(); } + const exprt::operandst &requires_contract() const + { + return static_cast(find(ID_C_spec_requires_contract)) + .operands(); + } + + exprt::operandst &requires_contract() + { + return static_cast(add(ID_C_spec_requires_contract)).operands(); + } + const exprt::operandst &requires() const { return static_cast(find(ID_C_spec_requires)).operands(); @@ -386,6 +397,17 @@ class code_with_contract_typet : public code_typet return static_cast(add(ID_C_spec_requires)).operands(); } + const exprt::operandst &ensures_contract() const + { + return static_cast(find(ID_C_spec_ensures_contract)) + .operands(); + } + + exprt::operandst &ensures_contract() + { + return static_cast(add(ID_C_spec_ensures_contract)).operands(); + } + const exprt::operandst &ensures() const { return static_cast(find(ID_C_spec_ensures)).operands(); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 7d004168fa6..9fe71eb1d7c 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -573,11 +573,14 @@ IREP_ID_ONE(used) IREP_ID_ONE(is_used) IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant) IREP_ID_TWO(C_spec_decreases, #spec_decreases) +IREP_ID_TWO(C_spec_requires_contract, #spec_requires_contract) IREP_ID_TWO(C_spec_requires, #spec_requires) +IREP_ID_TWO(C_spec_ensures_contract, #spec_ensures_contract) IREP_ID_TWO(C_spec_ensures, #spec_ensures) IREP_ID_TWO(C_spec_assigns, #spec_assigns) IREP_ID_ONE(target_list) IREP_ID_ONE(conditional_target_group) +IREP_ID_ONE(function_pointer_obeys_contract) IREP_ID_ONE(virtual_function) IREP_ID_TWO(element_type, element_type) IREP_ID_ONE(working_directory)