From 6ce96c7faf5472f193463f67feee51e99d5f86d8 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 23 Apr 2021 19:58:16 +0000 Subject: [PATCH] Adds support for pointer history variables in function contracts This adds support for history variables in function contracts. History variables are (1) declared and (2) assigned to the value that their corresponding variable has at function call time. Currently, only pointers are supported. --- .../contracts/history-pointer-both-01/main.c | 20 +++ .../history-pointer-both-01/test.desc | 17 ++ .../history-pointer-enforce-01/main.c | 13 ++ .../history-pointer-enforce-01/test.desc | 14 ++ .../history-pointer-enforce-02/main.c | 13 ++ .../history-pointer-enforce-02/test.desc | 14 ++ .../history-pointer-enforce-03/main.c | 16 ++ .../history-pointer-enforce-03/test.desc | 14 ++ .../history-pointer-enforce-04/main.c | 15 ++ .../history-pointer-enforce-04/test.desc | 14 ++ .../history-pointer-enforce-05/main.c | 14 ++ .../history-pointer-enforce-05/test.desc | 14 ++ .../history-pointer-enforce-06/main.c | 16 ++ .../history-pointer-enforce-06/test.desc | 12 ++ .../history-pointer-enforce-07/main.c | 13 ++ .../history-pointer-enforce-07/test.desc | 14 ++ .../history-pointer-enforce-08/main.c | 24 +++ .../history-pointer-enforce-08/test.desc | 14 ++ .../history-pointer-replace-01/main.c | 19 +++ .../history-pointer-replace-01/test.desc | 15 ++ .../history-pointer-replace-02/main.c | 17 ++ .../history-pointer-replace-02/test.desc | 15 ++ .../history-pointer-replace-03/main.c | 18 +++ .../history-pointer-replace-03/test.desc | 12 ++ src/ansi-c/c_expr.h | 23 +++ src/ansi-c/c_typecheck_base.cpp | 1 + src/ansi-c/c_typecheck_base.h | 1 + src/ansi-c/c_typecheck_expr.cpp | 31 ++++ src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/library/cprover.h | 1 + src/goto-instrument/code_contracts.cpp | 147 ++++++++++++++++-- src/goto-instrument/code_contracts.h | 20 +++ src/util/irep_ids.def | 1 + 33 files changed, 577 insertions(+), 16 deletions(-) create mode 100644 regression/contracts/history-pointer-both-01/main.c create mode 100644 regression/contracts/history-pointer-both-01/test.desc create mode 100644 regression/contracts/history-pointer-enforce-01/main.c create mode 100644 regression/contracts/history-pointer-enforce-01/test.desc create mode 100644 regression/contracts/history-pointer-enforce-02/main.c create mode 100644 regression/contracts/history-pointer-enforce-02/test.desc create mode 100644 regression/contracts/history-pointer-enforce-03/main.c create mode 100644 regression/contracts/history-pointer-enforce-03/test.desc create mode 100644 regression/contracts/history-pointer-enforce-04/main.c create mode 100644 regression/contracts/history-pointer-enforce-04/test.desc create mode 100644 regression/contracts/history-pointer-enforce-05/main.c create mode 100644 regression/contracts/history-pointer-enforce-05/test.desc create mode 100644 regression/contracts/history-pointer-enforce-06/main.c create mode 100644 regression/contracts/history-pointer-enforce-06/test.desc create mode 100644 regression/contracts/history-pointer-enforce-07/main.c create mode 100644 regression/contracts/history-pointer-enforce-07/test.desc create mode 100644 regression/contracts/history-pointer-enforce-08/main.c create mode 100644 regression/contracts/history-pointer-enforce-08/test.desc create mode 100644 regression/contracts/history-pointer-replace-01/main.c create mode 100644 regression/contracts/history-pointer-replace-01/test.desc create mode 100644 regression/contracts/history-pointer-replace-02/main.c create mode 100644 regression/contracts/history-pointer-replace-02/test.desc create mode 100644 regression/contracts/history-pointer-replace-03/main.c create mode 100644 regression/contracts/history-pointer-replace-03/test.desc 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)