diff --git a/regression/contracts/history-pointer-both-01/main.c b/regression/contracts/history-pointer-both-01/main.c new file mode 100644 index 00000000000..e562ea1af5e --- /dev/null +++ b/regression/contracts/history-pointer-both-01/main.c @@ -0,0 +1,20 @@ +#include + +void bar(int *l) __CPROVER_assigns(*l) __CPROVER_requires(l != NULL) + __CPROVER_ensures(__CPROVER_old(*l) == *l) +{ +} + +void foo(int *n) __CPROVER_assigns(*n) __CPROVER_requires(n != NULL) + __CPROVER_ensures(__CPROVER_old(*n) == *n) +{ + bar(n); +} + +int main() +{ + int m; + foo(&m); + + return 0; +} diff --git a/regression/contracts/history-pointer-both-01/test.desc b/regression/contracts/history-pointer-both-01/test.desc new file mode 100644 index 00000000000..76377d45f8a --- /dev/null +++ b/regression/contracts/history-pointer-both-01/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--enforce-contract foo --replace-call-with-contract bar +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSUME tmp_cc\$\d != \(\(signed int \*\)NULL\) +ASSERT n != \(\(signed int \*\)NULL\) +ASSUME tmp_cc == \*n +ASSERT tmp_cc\$\d == \*tmp_cc\$\d +-- +-- +Verification: +This test checks that history variables are supported for parameters of the +the function under test. By using the --enforce-all-contracts flag, +the post-condition (which contains the history variable) is asserted. +In this case, this assertion should pass. diff --git a/regression/contracts/history-pointer-enforce-01/main.c b/regression/contracts/history-pointer-enforce-01/main.c new file mode 100644 index 00000000000..07cba9ccd7a --- /dev/null +++ b/regression/contracts/history-pointer-enforce-01/main.c @@ -0,0 +1,13 @@ +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(*x == __CPROVER_old(*x) + 5) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-01/test.desc b/regression/contracts/history-pointer-enforce-01/test.desc new file mode 100644 index 00000000000..d3300daed5c --- /dev/null +++ b/regression/contracts/history-pointer-enforce-01/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT \*tmp_cc\$\d == tmp_cc\$\d \+ 5 +-- +-- +Verification: +This test checks that history variables are supported for parameters of the +the function under test. By using the --enforce-all-contracts flag, +the post-condition (which contains the history variable) is asserted. +In this case, this assertion should pass. diff --git a/regression/contracts/history-pointer-enforce-02/main.c b/regression/contracts/history-pointer-enforce-02/main.c new file mode 100644 index 00000000000..36f2ce3c80c --- /dev/null +++ b/regression/contracts/history-pointer-enforce-02/main.c @@ -0,0 +1,13 @@ +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(*x < __CPROVER_old(*x) + 5) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-02/test.desc b/regression/contracts/history-pointer-enforce-02/test.desc new file mode 100644 index 00000000000..960b0eb4aaf --- /dev/null +++ b/regression/contracts/history-pointer-enforce-02/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +ASSERT \*tmp_cc\$\d < tmp_cc\$\d \+ 5 +-- +-- +Verification: +This test checks that history variables are supported for parameters of the +the function under test. By using the --enforce-all-contracts flag, +the post-condition (which contains the history variable) is asserted. +In this case, this assertion should fail. diff --git a/regression/contracts/history-pointer-enforce-03/main.c b/regression/contracts/history-pointer-enforce-03/main.c new file mode 100644 index 00000000000..69eb8f972cc --- /dev/null +++ b/regression/contracts/history-pointer-enforce-03/main.c @@ -0,0 +1,16 @@ +#include + +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_requires(*x > 0 && *x < INT_MAX - 5) __CPROVER_ensures( + *x >= __CPROVER_old(*x) + 4 && *x <= __CPROVER_old(*x) + 6) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-03/test.desc b/regression/contracts/history-pointer-enforce-03/test.desc new file mode 100644 index 00000000000..9938b262b58 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-03/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT tmp_if_expr\$\d +-- +-- +Verification: +This test checks that history variables are supported in the case where a +history variable is referred to multiple times within an ensures clause. +By using the --enforce-all-contracts flag, the post-condition (which contains +the history variable) is asserted. In this case, this assertion should pass. diff --git a/regression/contracts/history-pointer-enforce-04/main.c b/regression/contracts/history-pointer-enforce-04/main.c new file mode 100644 index 00000000000..87da56243ee --- /dev/null +++ b/regression/contracts/history-pointer-enforce-04/main.c @@ -0,0 +1,15 @@ +void foo(int *x, int *y) __CPROVER_assigns(*x, *y) + __CPROVER_ensures(*x == __CPROVER_old(*y) + 1 && *y == __CPROVER_old(*x) + 2) +{ + int x_initial = *x; + *x = *y + 1; + *y = x_initial + 2; +} + +int main() +{ + int x, y; + foo(&x, &y); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-04/test.desc b/regression/contracts/history-pointer-enforce-04/test.desc new file mode 100644 index 00000000000..21bab515511 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-04/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT tmp_if_expr +-- +-- +Verification: +This test checks that history variables are supported in the case where the +function under test has multiple parameters. By using the +--enforce-all-contracts flag, the post-condition (which contains the history +variables) is asserted. In this case, this assertion should pass. diff --git a/regression/contracts/history-pointer-enforce-05/main.c b/regression/contracts/history-pointer-enforce-05/main.c new file mode 100644 index 00000000000..33783befa60 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-05/main.c @@ -0,0 +1,14 @@ +void foo(int *x, int *y) __CPROVER_assigns(*x, *y) + __CPROVER_ensures(*x == __CPROVER_old(*x) + 2 || *y == __CPROVER_old(*y) + 3) +{ + *x = *x + 1; + *y = *y + 2; +} + +int main() +{ + int x, y; + foo(&x, &y); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-05/test.desc b/regression/contracts/history-pointer-enforce-05/test.desc new file mode 100644 index 00000000000..493944290e8 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-05/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +ASSERT tmp_if_expr +-- +-- +Verification: +This test checks that history variables are supported in the case where the +function under test has multiple parameters. By using the +--enforce-all-contracts flag, the post-condition (which contains the history +variables) is asserted. In this case, this assertion should fail. diff --git a/regression/contracts/history-pointer-enforce-06/main.c b/regression/contracts/history-pointer-enforce-06/main.c new file mode 100644 index 00000000000..b8c7bef2b03 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-06/main.c @@ -0,0 +1,16 @@ +#include + +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(*x == __CPROVER_old(*x) + 5) +{ + assert(__CPROVER_old(*x) == *x); + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-06/test.desc b/regression/contracts/history-pointer-enforce-06/test.desc new file mode 100644 index 00000000000..c610475b5cc --- /dev/null +++ b/regression/contracts/history-pointer-enforce-06/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +warning: ignoring old +-- +-- +Verification: +This test checks that history variables are not supported when referred to from +a function body. In such a case, verification should fail. diff --git a/regression/contracts/history-pointer-enforce-07/main.c b/regression/contracts/history-pointer-enforce-07/main.c new file mode 100644 index 00000000000..13c04214e73 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-07/main.c @@ -0,0 +1,13 @@ +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(*x == __CPROVER_old(*y) + 5) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-07/test.desc b/regression/contracts/history-pointer-enforce-07/test.desc new file mode 100644 index 00000000000..62caa14ea81 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-07/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=(1|64)$ +^SIGNAL=0$ +^CONVERSION ERROR$ +error: failed to find symbol 'y' +-- +-- +Verification: +This test checks that history variables may only be used with existing +symbols. In other words, including a new symbol as part of __CPROVER_old() +is not alowed. In such a case, the program should not parse and there +should be a conversion error. diff --git a/regression/contracts/history-pointer-enforce-08/main.c b/regression/contracts/history-pointer-enforce-08/main.c new file mode 100644 index 00000000000..49e3e74ce70 --- /dev/null +++ b/regression/contracts/history-pointer-enforce-08/main.c @@ -0,0 +1,24 @@ +#include + +struct pair +{ + int *x; + int *y; +}; + +void foo(struct pair p) __CPROVER_assigns(*(p.y)) + __CPROVER_ensures(*(p.y) == __CPROVER_old(*(p.y)) + 5) +{ + *(p.y) = *(p.y) + 5; +} + +int main() +{ + struct pair p; + p.x = malloc(sizeof(int)); + p.y = malloc(sizeof(int)); + + foo(p); + + return 0; +} diff --git a/regression/contracts/history-pointer-enforce-08/test.desc b/regression/contracts/history-pointer-enforce-08/test.desc new file mode 100644 index 00000000000..951fff65c6f --- /dev/null +++ b/regression/contracts/history-pointer-enforce-08/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT \*tmp_cc\$\d\.y == tmp_cc\$\d \+ 5 +-- +-- +Verification: +This test checks that history variables are supported for dereferences over +pointers to struct members. By using the --enforce-all-contracts flag, the +post-condition (which contains the history variable) is asserted. In this +case, this assertion should pass. diff --git a/regression/contracts/history-pointer-replace-01/main.c b/regression/contracts/history-pointer-replace-01/main.c new file mode 100644 index 00000000000..861d78448b0 --- /dev/null +++ b/regression/contracts/history-pointer-replace-01/main.c @@ -0,0 +1,19 @@ +#include +#include + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0) + __CPROVER_ensures(*x == __CPROVER_old(*x) + 2) +{ + *x = *x + 2; +} + +int main() +{ + int n; + __CPROVER_assume(n > 0 && n < INT_MAX - 2); + foo(&n); + + assert(n > 2); + + return 0; +} diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc new file mode 100644 index 00000000000..3c047fc5975 --- /dev/null +++ b/regression/contracts/history-pointer-replace-01/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT \*\(&n\) > 0 +ASSUME \*\(&n\) == tmp_cc[\$\d]? \+ 2 +-- +-- +Verification: +This test checks that history variables are supported with the use of the +--replace-all-calls-with-contracts flag. In this case, the pre-condition +becomes an assertion and the post-condition (which contains the history +variable) becomes an assumption. diff --git a/regression/contracts/history-pointer-replace-02/main.c b/regression/contracts/history-pointer-replace-02/main.c new file mode 100644 index 00000000000..5c4e72fa1c2 --- /dev/null +++ b/regression/contracts/history-pointer-replace-02/main.c @@ -0,0 +1,17 @@ +#include + +void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x == 0) + __CPROVER_ensures(*x >= __CPROVER_old(*x) + 2) +{ + *x = *x + 2; +} + +int main() +{ + int n = 0; + foo(&n); + + assert(n >= 2); + + return 0; +} diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc new file mode 100644 index 00000000000..3903c0aa6ff --- /dev/null +++ b/regression/contracts/history-pointer-replace-02/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +ASSERT \*\(&n\) == 0 +ASSUME \*\(&n\) >= tmp_cc[\$\d]? \+ 2 +-- +-- +Verification: +This test checks that history variables are supported with the use of the +--replace-all-calls-with-contracts flag. In this case, the pre-condition +becomes an assertion and the post-condition (which contains the history +variable) becomes an assumption. diff --git a/regression/contracts/history-pointer-replace-03/main.c b/regression/contracts/history-pointer-replace-03/main.c new file mode 100644 index 00000000000..ccefee72fd4 --- /dev/null +++ b/regression/contracts/history-pointer-replace-03/main.c @@ -0,0 +1,18 @@ +#include + +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_requires(*x == __CPROVER_old(*x)) + __CPROVER_ensures(*x == __CPROVER_old(*x) + 2) +{ + *x = *x + 2; +} + +int main() +{ + int n = 0; + foo(&n); + + assert(n == 2); + + return 0; +} diff --git a/regression/contracts/history-pointer-replace-03/test.desc b/regression/contracts/history-pointer-replace-03/test.desc new file mode 100644 index 00000000000..a49bbb6f868 --- /dev/null +++ b/regression/contracts/history-pointer-replace-03/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=(1|64)$ +^SIGNAL=0$ +^CONVERSION ERROR$ +error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses +-- +-- +Verification: +This test checks that history variables cannot be used as part of the +pre-condition contract. In this case, verification should fail. diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 5061d8fccf8..13b965ec6e7 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -200,4 +200,27 @@ inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &expr) return static_cast(side_effect_expr); } +/// \brief A class for an expression that indicates the pre-function-call +/// value of an expression passed as a parameter to a function +class old_exprt : public unary_exprt +{ +public: + explicit old_exprt(exprt variable) : unary_exprt(ID_old, std::move(variable)) + { + } + + const exprt &expression() const + { + return op0(); + } +}; + +inline const old_exprt &to_old_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_old); + 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 257ca817540..42658898fd1 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -729,6 +729,7 @@ void c_typecheck_baset::typecheck_declaration( auto &requires = code_type.requires(); typecheck_expr(requires); implicit_typecast_bool(requires); + disallow_history_variables(requires); } if(as_const(code_type).assigns().is_not_nil()) diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 06fb78fd299..e37fa666d73 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -205,6 +205,7 @@ class c_typecheck_baset: const symbol_exprt &function_symbol); virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr); + void disallow_history_variables(const exprt &) const; virtual void make_index_type(exprt &expr); virtual void make_constant(exprt &expr); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 429911cfeff..ebe1fd9a7fd 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2621,6 +2621,20 @@ exprt c_typecheck_baset::do_special_functions( return std::move(ok_expr); } + else if(identifier == CPROVER_PREFIX "old") + { + if(expr.arguments().size() != 1) + { + error().source_location = f_op.source_location(); + error() << identifier << " expects one operand" << eom; + throw 0; + } + + old_exprt old_expr(expr.arguments()[0]); + old_expr.add_source_location() = source_location; + + return std::move(old_expr); + } else if(identifier==CPROVER_PREFIX "isinff" || identifier==CPROVER_PREFIX "isinfd" || identifier==CPROVER_PREFIX "isinfld" || @@ -3862,3 +3876,20 @@ void c_typecheck_baset::make_constant_index(exprt &expr) throw 0; } } + +void c_typecheck_baset::disallow_history_variables(const exprt &expr) const +{ + for(auto &op : expr.operands()) + { + disallow_history_variables(op); + } + + if(expr.id() == ID_old) + { + error().source_location = expr.source_location(); + error() << CPROVER_PREFIX + "old expressions are not allowed in " CPROVER_PREFIX "requires clauses" + << eom; + throw 0; + } +} diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index bf9a34b19c0..250b5ba06c0 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -13,6 +13,7 @@ __CPROVER_size_t __CPROVER_buffer_size(const void *); __CPROVER_bool __CPROVER_r_ok(); __CPROVER_bool __CPROVER_w_ok(); __CPROVER_bool __CPROVER_rw_ok(); +void __CPROVER_old(const void *); // bitvector analysis __CPROVER_bool __CPROVER_get_flag(const void *, const char *); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index f646f55e8ee..c4e3427393a 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -36,6 +36,7 @@ __CPROVER_size_t __CPROVER_buffer_size(const void *); __CPROVER_bool __CPROVER_r_ok(); __CPROVER_bool __CPROVER_w_ok(); __CPROVER_bool __CPROVER_rw_ok(); +void __CPROVER_old(); #if 0 __CPROVER_bool __CPROVER_equal(); diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 90b23b9866a..47df57471a8 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -14,9 +14,12 @@ Date: February 2016 #include "code_contracts.h" #include +#include #include +#include + #include #include @@ -241,6 +244,92 @@ void code_contractst::add_quantified_variable( } } +void code_contractst::replace_old_parameter( + exprt &expr, + std::map ¶meter2history, + source_locationt location, + const irep_idt &function, + const irep_idt &mode, + goto_programt &history) +{ + for(auto &op : expr.operands()) + { + replace_old_parameter( + op, parameter2history, location, function, mode, history); + } + + if(expr.id() == ID_old) + { + DATA_INVARIANT( + expr.operands().size() == 1, CPROVER_PREFIX "old must have one operand"); + + const auto ¶meter = to_old_expr(expr).expression(); + + // TODO: generalize below + if(parameter.id() == ID_dereference) + { + const auto &dereference_expr = to_dereference_expr(parameter); + + auto it = parameter2history.find(dereference_expr); + + if(it == parameter2history.end()) + { + // 1. Create a temporary symbol expression that represents the + // history variable + symbol_exprt tmp_symbol = + new_tmp_symbol(dereference_expr.type(), location, function, mode) + .symbol_expr(); + + // 2. Associate the above temporary variable to it's corresponding + // expression + parameter2history[dereference_expr] = tmp_symbol; + + // 3. Add the required instructions to the instructions list + // 3.1 Declare the newly created temporary variable + history.add(goto_programt::make_decl(tmp_symbol, location)); + + // 3.2 Add an assignment such that the value pointed to by the new + // temporary variable is equal to the value of the corresponding + // parameter + history.add(goto_programt::make_assignment( + tmp_symbol, dereference_expr, location)); + } + + expr = parameter2history[dereference_expr]; + } + else + { + log.error() << CPROVER_PREFIX "old does not currently support " + << parameter.id() << " expressions." << messaget::eom; + throw 0; + } + } +} + +std::pair +code_contractst::create_ensures_instruction( + codet &expression, + source_locationt location, + const irep_idt &function, + const irep_idt &mode) +{ + std::map parameter2history; + goto_programt history; + + // Find and replace "old" expression in the "expression" variable + replace_old_parameter( + expression, parameter2history, location, function, mode, history); + + // Create instructions corresponding to the ensures clause + goto_programt ensures_program; + convert_to_goto(expression, mode, ensures_program); + + // return a pair containing: + // 1. instructions corresponding to the ensures clause + // 2. instructions related to initializing the history variables + return std::make_pair(std::move(ensures_program), std::move(history)); +} + bool code_contractst::apply_function_contract( const irep_idt &function_id, goto_programt &goto_program, @@ -344,6 +433,25 @@ bool code_contractst::apply_function_contract( std::advance(target, lines_to_iterate); } + // Gather all the instructions required to handle history variables + // as well as the ensures clause + std::pair ensures_pair; + if(ensures.is_not_nil()) + { + auto assumption = code_assumet(ensures); + ensures_pair = create_ensures_instruction( + assumption, + ensures.source_location(), + function, + symbol_table.lookup_ref(function).mode); + + // add all the history variable initialization instructions + // to the goto program + auto lines_to_iterate = ensures_pair.second.instructions.size(); + goto_program.insert_before_swap(target, ensures_pair.second); + std::advance(target, lines_to_iterate); + } + // Create a series of non-deterministic assignments to havoc the variables // in the assigns clause. if(assigns.is_not_nil()) @@ -363,13 +471,8 @@ bool code_contractst::apply_function_contract( // function call with a SKIP statement. if(ensures.is_not_nil()) { - goto_programt assumption; - convert_to_goto( - code_assumet(ensures), - symbol_table.lookup_ref(function).mode, - assumption); - auto lines_to_iterate = assumption.instructions.size(); - goto_program.insert_before_swap(target, assumption); + auto lines_to_iterate = ensures_pair.first.instructions.size(); + goto_program.insert_before_swap(target, ensures_pair.first); std::advance(target, lines_to_iterate); } *target = goto_programt::make_skip(); @@ -784,6 +887,7 @@ void code_contractst::add_contract_check( // if(nondet) // decl ret // decl parameter1 ... + // decl history_parameter1 ... [optional] // assume(requires) [optional] // ret=function(parameter1, ...) // assert(ensures) @@ -812,7 +916,7 @@ void code_contractst::add_contract_check( .symbol_expr(); check.add(goto_programt::make_decl(r, skip->source_location)); - call.lhs()=r; + call.lhs() = r; return_stmt = code_returnt(r); symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); @@ -850,6 +954,10 @@ void code_contractst::add_contract_check( code_contractst::add_quantified_variable( requires, replace, function_symbol.mode); + // rewrite any use of __CPROVER_return_value + exprt ensures_cond = ensures; + replace(ensures_cond); + // assume(requires) if(requires.is_not_nil()) { @@ -863,20 +971,27 @@ void code_contractst::add_contract_check( check.destructive_append(assumption); } + // Prepare the history variables handling + std::pair ensures_pair; + + if(ensures.is_not_nil()) + { + // get all the relevant instructions related to history variables + auto assertion = code_assertt(ensures_cond); + ensures_pair = create_ensures_instruction( + assertion, ensures.source_location(), wrapper_fun, function_symbol.mode); + + // add all the history variable initializations + check.destructive_append(ensures_pair.second); + } + // ret=mangled_fun(parameter1, ...) check.add(goto_programt::make_function_call(call, skip->source_location)); - // rewrite any use of __CPROVER_return_value - exprt ensures_cond = ensures; - replace(ensures_cond); - // assert(ensures) if(ensures.is_not_nil()) { - goto_programt assertion; - convert_to_goto( - code_assertt(ensures_cond), function_symbol.mode, assertion); - check.destructive_append(assertion); + check.destructive_append(ensures_pair.first); } if(code_type.return_type() != empty_typet()) diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 11651a513aa..e4e18d588fb 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -14,6 +14,7 @@ Date: February 2016 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H +#include #include #include #include @@ -179,6 +180,25 @@ class code_contractst exprt expression, replace_symbolt &replace, irep_idt mode); + + /// This function recursively identifies the "old" expressions within expr + /// and replaces them with correspoding history variables. + void replace_old_parameter( + exprt &expr, + std::map ¶meter2history, + source_locationt location, + const irep_idt &function, + const irep_idt &mode, + goto_programt &history); + + /// This function creates and returns an instruction that corresponds to the + /// ensures clause. It also returns a list of instructions related to + /// initializing history variables, if required. + std::pair create_ensures_instruction( + codet &expression, + source_locationt location, + const irep_idt &function, + const irep_idt &mode); }; #define FLAG_REPLACE_CALL "replace-call-with-contract" diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 86a13313ba8..ac1aae45683 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -688,6 +688,7 @@ IREP_ID_TWO(C_array_ini, #array_ini) IREP_ID_ONE(r_ok) IREP_ID_ONE(w_ok) IREP_ID_ONE(rw_ok) +IREP_ID_ONE(old) IREP_ID_ONE(super_class) IREP_ID_ONE(exceptions_thrown_list) IREP_ID_TWO(C_java_method_type, #java_method_type)