diff --git a/regression/contracts/function_loop_history_ensures_fail/main.c b/regression/contracts/function_loop_history_ensures_fail/main.c new file mode 100644 index 00000000000..8ff92262bf0 --- /dev/null +++ b/regression/contracts/function_loop_history_ensures_fail/main.c @@ -0,0 +1,13 @@ +void foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(*x == __CPROVER_loop_entry(*x) + 5) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/function_loop_history_ensures_fail/test.desc b/regression/contracts/function_loop_history_ensures_fail/test.desc new file mode 100644 index 00000000000..542b13720dd --- /dev/null +++ b/regression/contracts/function_loop_history_ensures_fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^main.c.* error: __CPROVER_loop_entry is not allowed in postconditions.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test ensures that __CPROVER_loop_entry cannot be used within ensures clause. diff --git a/regression/contracts/function_loop_history_requires_fail/main.c b/regression/contracts/function_loop_history_requires_fail/main.c new file mode 100644 index 00000000000..f0f4aeeba22 --- /dev/null +++ b/regression/contracts/function_loop_history_requires_fail/main.c @@ -0,0 +1,13 @@ +void bar(int *x) __CPROVER_assigns(*x) + __CPROVER_requires(*x == __CPROVER_loop_entry(*x) + 5) +{ + *x = *x + 5; +} + +int main() +{ + int n; + foo(&n); + + return 0; +} diff --git a/regression/contracts/function_loop_history_requires_fail/test.desc b/regression/contracts/function_loop_history_requires_fail/test.desc new file mode 100644 index 00000000000..52670fd8778 --- /dev/null +++ b/regression/contracts/function_loop_history_requires_fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^main.c.* error: __CPROVER_loop_entry is not allowed in preconditions.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test ensures that __CPROVER_loop_entry cannot be used within requires clause. diff --git a/regression/contracts/history-pointer-replace-03/test.desc b/regression/contracts/history-pointer-replace-03/test.desc index a49bbb6f868..0c26792ec94 100644 --- a/regression/contracts/history-pointer-replace-03/test.desc +++ b/regression/contracts/history-pointer-replace-03/test.desc @@ -1,12 +1,11 @@ CORE main.c --replace-all-calls-with-contracts +^main.c.* error: __CPROVER_old is not allowed in preconditions.$ +^CONVERSION ERROR$ ^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. +pre-condition (requires) contract. diff --git a/regression/contracts/invar_function-old_fail/main.c b/regression/contracts/invar_function-old_fail/main.c new file mode 100644 index 00000000000..1be7b6b15ed --- /dev/null +++ b/regression/contracts/invar_function-old_fail/main.c @@ -0,0 +1,17 @@ +#include + +void main() +{ + int *x, y, z; + + x = &z; + + while(y > 0) + __CPROVER_loop_invariant(*x == __CPROVER_old(*x)) + { + --y; + *x = *x + 1; + *x = *x - 1; + } + assert(*x == z); +} diff --git a/regression/contracts/invar_function-old_fail/test.desc b/regression/contracts/invar_function-old_fail/test.desc new file mode 100644 index 00000000000..07f2ce0de84 --- /dev/null +++ b/regression/contracts/invar_function-old_fail/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts +^main.c.* error: __CPROVER_old is not allowed in loop invariants.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test ensures that __CPROVER_old cannot be used within loop contracts. diff --git a/regression/contracts/invar_loop-entry_check/main.c b/regression/contracts/invar_loop-entry_check/main.c new file mode 100644 index 00000000000..c89606e0886 --- /dev/null +++ b/regression/contracts/invar_loop-entry_check/main.c @@ -0,0 +1,49 @@ +#include +#include + +typedef struct +{ + int *n; +} s; + +void main() +{ + int *x1, y1, z1; + x1 = &z1; + + while(y1 > 0) + __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1)) + { + --y1; + *x1 = *x1 + 1; + *x1 = *x1 - 1; + } + assert(*x1 == z1); + + int x2, y2, z2; + x2 = z2; + + while(y2 > 0) + __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2)) + { + --y2; + x2 = x2 + 1; + x2 = x2 - 1; + } + assert(x2 == z2); + + int y3; + s *s1, *s2; + s2->n = malloc(sizeof(int)); + s1->n = s2->n; + + while(y3 > 0) + __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n)) + { + --y3; + s1->n = s1->n + 1; + s1->n = s1->n - 1; + } + + assert(*(s1->n) == *(s2->n)); +} diff --git a/regression/contracts/invar_loop-entry_check/test.desc b/regression/contracts/invar_loop-entry_check/test.desc new file mode 100644 index 00000000000..e563175416b --- /dev/null +++ b/regression/contracts/invar_loop-entry_check/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion \*x1 == z1: SUCCESS$ +^\[main.3\] .* Check loop invariant before entry: SUCCESS$ +^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$ +^\[main.5\] .* Check loop invariant before entry: SUCCESS$ +^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that __CPROVER_loop_entry is supported. diff --git a/regression/contracts/invar_loop-entry_fail/main.c b/regression/contracts/invar_loop-entry_fail/main.c new file mode 100644 index 00000000000..e902c8ab841 --- /dev/null +++ b/regression/contracts/invar_loop-entry_fail/main.c @@ -0,0 +1,15 @@ +#include + +void main() +{ + int x, y, z; + x = z; + + while(y > 0) + __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x)) + { + --y; + x = x + 1; + x = x - 2; + } +} diff --git a/regression/contracts/invar_loop-entry_fail/test.desc b/regression/contracts/invar_loop-entry_fail/test.desc new file mode 100644 index 00000000000..1bfb43d60b7 --- /dev/null +++ b/regression/contracts/invar_loop-entry_fail/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=(10|6)$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test ensures that __CPROVER_loop_entry violations are checked. diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 13b965ec6e7..9ef4902010c 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -200,12 +200,12 @@ 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 +/// \brief A class for an expression that indicates a history variable +class history_exprt : public unary_exprt { public: - explicit old_exprt(exprt variable) : unary_exprt(ID_old, std::move(variable)) + explicit history_exprt(exprt variable, const irep_idt &id) + : unary_exprt(id, std::move(variable)) { } @@ -215,10 +215,12 @@ class old_exprt : public unary_exprt } }; -inline const old_exprt &to_old_expr(const exprt &expr) +inline const history_exprt & +to_history_expr(const exprt &expr, const irep_idt &id) { - PRECONDITION(expr.id() == ID_old); - auto &ret = static_cast(expr); + PRECONDITION(id == ID_old || id == ID_loop_entry); + PRECONDITION(expr.id() == id); + auto &ret = static_cast(expr); validate_expr(ret); return ret; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 1b42a62a24c..0dc7eae5401 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -730,7 +730,14 @@ void c_typecheck_baset::typecheck_declaration( { typecheck_expr(requires); implicit_typecast_bool(requires); - disallow_history_variables(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."); } } @@ -751,6 +758,10 @@ void c_typecheck_baset::typecheck_declaration( { typecheck_expr(ensures); implicit_typecast_bool(ensures); + disallow_subexpr_by_id( + ensures, + ID_loop_entry, + CPROVER_PREFIX "loop_entry is not allowed in postconditions."); } if(return_type.id() != ID_empty) diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 8a17aaabdff..a79aedae124 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -206,7 +206,10 @@ 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; + void disallow_subexpr_by_id( + const exprt &, + const irep_idt &, + const std::string &) const; virtual void make_index_type(exprt &expr); virtual void make_constant(exprt &expr); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 5cfbdd45bc4..013362406aa 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -820,6 +820,10 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) { typecheck_expr(invariant); implicit_typecast_bool(invariant); + disallow_subexpr_by_id( + invariant, + ID_old, + CPROVER_PREFIX "old is not allowed in loop invariants."); } } } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 76036ecea78..ad9a2dc2701 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2695,7 +2695,9 @@ exprt c_typecheck_baset::do_special_functions( return std::move(ok_expr); } - else if(identifier == CPROVER_PREFIX "old") + else if( + (identifier == CPROVER_PREFIX "old") || + (identifier == CPROVER_PREFIX "loop_entry")) { if(expr.arguments().size() != 1) { @@ -2704,7 +2706,9 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - old_exprt old_expr(expr.arguments()[0]); + irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry; + + history_exprt old_expr(expr.arguments()[0], id); old_expr.add_source_location() = source_location; return std::move(old_expr); @@ -3957,19 +3961,15 @@ void c_typecheck_baset::make_constant_index(exprt &expr) } } -void c_typecheck_baset::disallow_history_variables(const exprt &expr) const +void c_typecheck_baset::disallow_subexpr_by_id( + const exprt &expr, + const irep_idt &id, + const std::string &message) const { - for(auto &op : expr.operands()) - { - disallow_history_variables(op); - } + if(!has_subexpr(expr, id)) + return; - 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; - } + error().source_location = expr.source_location(); + error() << message << eom; + throw 0; } diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 7a63afb74d3..b75c633824f 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -37,6 +37,7 @@ void __CPROVER_fence(const char *kind, ...); // contract-related functions __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); void __CPROVER_old(const void *); +void __CPROVER_loop_entry(const void *); // pointers __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 49caccfa4fe..2991855f781 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -147,6 +147,7 @@ void code_contractst::check_apply_loop_contracts( // H: loop; // E: ... // to + // initialize loop_entry variables; // H: assert(invariant); // havoc; // assume(invariant); @@ -176,6 +177,20 @@ void code_contractst::check_apply_loop_contracts( return invariant_copy; }; + // Process "loop_entry" history variables + // Find and replace "loop_entry" expression in the "invariant" expression. + std::map parameter2history; + replace_history_parameter( + invariant, + parameter2history, + loop_head->source_location, + mode, + havoc_code, + ID_loop_entry); + + // Create 'loop_entry' history variables + insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code); + // Generate: assert(invariant) just before the loop // We use a block scope to create a temporary assertion, // and immediately convert it to goto instructions. @@ -377,24 +392,23 @@ void code_contractst::add_quantified_variable( } } -void code_contractst::replace_old_parameter( +void code_contractst::replace_history_parameter( exprt &expr, std::map ¶meter2history, source_locationt location, const irep_idt &mode, - goto_programt &history) + goto_programt &history, + const irep_idt &id) { for(auto &op : expr.operands()) { - replace_old_parameter(op, parameter2history, location, mode, history); + replace_history_parameter( + op, parameter2history, location, mode, history, id); } - if(expr.id() == ID_old) + if(expr.id() == ID_old || expr.id() == ID_loop_entry) { - DATA_INVARIANT( - expr.operands().size() == 1, CPROVER_PREFIX "old must have one operand"); - - const auto ¶meter = to_old_expr(expr).expression(); + const auto ¶meter = to_history_expr(expr, id).expression(); if( parameter.id() == ID_dereference || parameter.id() == ID_member || @@ -428,8 +442,8 @@ void code_contractst::replace_old_parameter( } else { - log.error() << CPROVER_PREFIX "old does not currently support " - << parameter.id() << " expressions." << messaget::eom; + log.error() << "Tracking history of " << parameter.id() + << " expressions is not supported yet." << messaget::eom; throw 0; } } @@ -445,7 +459,8 @@ code_contractst::create_ensures_instruction( goto_programt history; // Find and replace "old" expression in the "expression" variable - replace_old_parameter(expression, parameter2history, location, mode, history); + replace_history_parameter( + expression, parameter2history, location, mode, history, ID_old); // Create instructions corresponding to the ensures clause goto_programt ensures_program; diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index cca800aec58..97da9806748 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -219,12 +219,13 @@ class code_contractst /// This function recursively identifies the "old" expressions within expr /// and replaces them with correspoding history variables. - void replace_old_parameter( + void replace_history_parameter( exprt &expr, std::map ¶meter2history, source_locationt location, const irep_idt &mode, - goto_programt &history); + goto_programt &history, + const irep_idt &id); /// This function creates and returns an instruction that corresponds to the /// ensures clause. It also returns a list of instructions related to diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 49835963492..d85676fedea 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -691,6 +691,7 @@ IREP_ID_ONE(r_ok) IREP_ID_ONE(w_ok) IREP_ID_ONE(rw_ok) IREP_ID_ONE(old) +IREP_ID_ONE(loop_entry) IREP_ID_ONE(super_class) IREP_ID_ONE(exceptions_thrown_list) IREP_ID_TWO(C_java_method_type, #java_method_type)