diff --git a/regression/contracts/invar_check_break_pass/main.c b/regression/contracts/invar_check_break_pass/main.c index c64e2325695..c8eeb27e513 100644 --- a/regression/contracts/invar_check_break_pass/main.c +++ b/regression/contracts/invar_check_break_pass/main.c @@ -6,7 +6,10 @@ int main() __CPROVER_assume(r >= 0); while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on { --r; if(r <= 1) diff --git a/regression/contracts/invar_check_continue/main.c b/regression/contracts/invar_check_continue/main.c index 22440cf5f15..c60b5233082 100644 --- a/regression/contracts/invar_check_continue/main.c +++ b/regression/contracts/invar_check_continue/main.c @@ -6,7 +6,10 @@ int main() __CPROVER_assume(r >= 0); while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on { --r; if(r < 5) diff --git a/regression/contracts/invar_check_large/main.c b/regression/contracts/invar_check_large/main.c index 2dd6507c952..cc67eb7bdc5 100644 --- a/regression/contracts/invar_check_large/main.c +++ b/regression/contracts/invar_check_large/main.c @@ -22,9 +22,9 @@ int main() int l = 0; int r = 1; while(h > l) + // clang-format off __CPROVER_loop_invariant( // Turn off `clang-format` because it breaks the `==>` operator. - /* clang-format off */ h >= l && 0 <= l && l < 5 && 0 <= h && h < 5 && @@ -44,8 +44,9 @@ int main() (2 > h ==> arr2 >= pivot) && (3 > h ==> arr3 >= pivot) && (4 > h ==> arr4 >= pivot) - /* clang-format on */ ) + __CPROVER_decreases(h - l) + // clang-format on { if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) { diff --git a/regression/contracts/invar_check_multiple_loops/main.c b/regression/contracts/invar_check_multiple_loops/main.c index b30322b8258..32386ccd3ef 100644 --- a/regression/contracts/invar_check_multiple_loops/main.c +++ b/regression/contracts/invar_check_multiple_loops/main.c @@ -6,12 +6,18 @@ int main() __CPROVER_assume(n > 0 && x == y); for(r = 0; r < n; ++r) + // clang-format off __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r) + __CPROVER_decreases(n - r) + // clang-format on { x++; } while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r)) + __CPROVER_decreases(r) + // clang-format on { y--; r--; diff --git a/regression/contracts/invar_check_nested_loops/main.c b/regression/contracts/invar_check_nested_loops/main.c index a83aa6a26f6..4c9617fbd26 100644 --- a/regression/contracts/invar_check_nested_loops/main.c +++ b/regression/contracts/invar_check_nested_loops/main.c @@ -6,13 +6,19 @@ int main() __CPROVER_assume(n >= 0); for(int i = 0; i < n; ++i) + // clang-format off __CPROVER_loop_invariant(i <= n && s == i) + __CPROVER_decreases(n - i) + // clang-format on { int a, b; __CPROVER_assume(b >= 0 && a == b); while(a > 0) + // clang-format off __CPROVER_loop_invariant(a >= 0 && s == i + (b - a)) + __CPROVER_decreases(a) + // clang-format on { s++; a--; diff --git a/regression/contracts/invar_check_pointer_modifies-01/main.c b/regression/contracts/invar_check_pointer_modifies-01/main.c index 1c6dc2df5a7..c6034daab31 100644 --- a/regression/contracts/invar_check_pointer_modifies-01/main.c +++ b/regression/contracts/invar_check_pointer_modifies-01/main.c @@ -8,7 +8,10 @@ void main() unsigned i; while(i > 0) + // clang-format off __CPROVER_loop_invariant(*data == 42) + __CPROVER_decreases(i) + // clang-format on { *data = 42; i--; diff --git a/regression/contracts/invar_check_pointer_modifies-02/main.c b/regression/contracts/invar_check_pointer_modifies-02/main.c index 1642d621ed9..03ae679af71 100644 --- a/regression/contracts/invar_check_pointer_modifies-02/main.c +++ b/regression/contracts/invar_check_pointer_modifies-02/main.c @@ -10,7 +10,10 @@ void main() unsigned i; while(i > 0) + // clang-format off __CPROVER_loop_invariant(*data == 42) + __CPROVER_decreases(i) + // clang-format on { *data = 42; i--; diff --git a/regression/contracts/invar_check_sufficiency/main.c b/regression/contracts/invar_check_sufficiency/main.c index b650ef25181..667d3bdfd9e 100644 --- a/regression/contracts/invar_check_sufficiency/main.c +++ b/regression/contracts/invar_check_sufficiency/main.c @@ -6,7 +6,10 @@ int main() __CPROVER_assume(r >= 0); while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on { --r; } diff --git a/regression/contracts/invar_loop_constant_no_modify/main.c b/regression/contracts/invar_loop_constant_no_modify/main.c index b57995c0987..3b03c7777d2 100644 --- a/regression/contracts/invar_loop_constant_no_modify/main.c +++ b/regression/contracts/invar_loop_constant_no_modify/main.c @@ -6,7 +6,10 @@ int main() int s = 1; __CPROVER_assume(r >= 0); while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on { r--; } diff --git a/regression/contracts/invar_loop_constant_pass/main.c b/regression/contracts/invar_loop_constant_pass/main.c index 8e85f3cb140..fbb5cb3d88a 100644 --- a/regression/contracts/invar_loop_constant_pass/main.c +++ b/regression/contracts/invar_loop_constant_pass/main.c @@ -5,7 +5,10 @@ int main() int r, s = 1; __CPROVER_assume(r >= 0); while(r > 0) + // clang-format off __CPROVER_loop_invariant(r >= 0 && s == 1) + __CPROVER_decreases(r) + // clang-format on { s = 1; r--; diff --git a/regression/contracts/invariant_side_effects/main.c b/regression/contracts/invariant_side_effects/main.c index 26d5748c67f..b2000c05c06 100644 --- a/regression/contracts/invariant_side_effects/main.c +++ b/regression/contracts/invariant_side_effects/main.c @@ -7,7 +7,10 @@ int main() *a = 0; while(*a < N) + // clang-format off __CPROVER_loop_invariant((0 <= *a) && (*a <= N)) + __CPROVER_decreases(N - *a) + // clang-format on { ++(*a); } diff --git a/regression/contracts/variant_parsing_statement_fail/main.c b/regression/contracts/variant_parsing_statement_fail/main.c new file mode 100644 index 00000000000..05d24f810c3 --- /dev/null +++ b/regression/contracts/variant_parsing_statement_fail/main.c @@ -0,0 +1,16 @@ + +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(int x = 0) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_parsing_statement_fail/test.desc b/regression/contracts/variant_parsing_statement_fail/test.desc new file mode 100644 index 00000000000..a65b9fc5dae --- /dev/null +++ b/regression/contracts/variant_parsing_statement_fail/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +activate-multi-line-match +^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$ +^PARSING ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test fails because the loop variant is a statement (more precisely, +an assignment) rather than an expression (more precisely, an ACSL binding +expression). diff --git a/regression/contracts/variant_parsing_tuple_fail/main.c b/regression/contracts/variant_parsing_tuple_fail/main.c new file mode 100644 index 00000000000..e0a0f07eb2a --- /dev/null +++ b/regression/contracts/variant_parsing_tuple_fail/main.c @@ -0,0 +1,15 @@ +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(N - i, 42) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts/variant_parsing_tuple_fail/test.desc b/regression/contracts/variant_parsing_tuple_fail/test.desc new file mode 100644 index 00000000000..e47f0b1ee48 --- /dev/null +++ b/regression/contracts/variant_parsing_tuple_fail/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +activate-multi-line-match +^main.c.*error: syntax error before ','\n.*__CPROVER_decreases\(N - i, 42\)$ +^PARSING ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test fails because the loop variant has two arguments instead of just one. +Currently, we only support loop variants of single arguments - we do not +support loop variants of tuples (yet). diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index e37fa666d73..8a17aaabdff 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -144,7 +144,8 @@ class c_typecheck_baset: virtual void typecheck_while(code_whilet &code); virtual void typecheck_dowhile(code_dowhilet &code); virtual void typecheck_start_thread(codet &code); - virtual void typecheck_spec_expr(codet &code, const irep_idt &spec); + virtual void typecheck_spec_loop_invariant(codet &code); + virtual void typecheck_spec_decreases(codet &code); bool break_is_allowed; bool continue_is_allowed; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 6b29f013d9f..5ea85a0462f 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -484,7 +484,8 @@ void c_typecheck_baset::typecheck_for(codet &code) typecheck_code(code); // recursive call } - typecheck_spec_expr(code, ID_C_spec_loop_invariant); + typecheck_spec_loop_invariant(code); + typecheck_spec_decreases(code); } void c_typecheck_baset::typecheck_label(code_labelt &code) @@ -772,7 +773,8 @@ void c_typecheck_baset::typecheck_while(code_whilet &code) break_is_allowed=old_break_is_allowed; continue_is_allowed=old_continue_is_allowed; - typecheck_spec_expr(code, ID_C_spec_loop_invariant); + typecheck_spec_loop_invariant(code); + typecheck_spec_decreases(code); } void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) @@ -805,16 +807,28 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) break_is_allowed=old_break_is_allowed; continue_is_allowed=old_continue_is_allowed; - typecheck_spec_expr(code, ID_C_spec_loop_invariant); + typecheck_spec_loop_invariant(code); + typecheck_spec_decreases(code); } -void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec) +void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) { - if(code.find(spec).is_not_nil()) + if(code.find(ID_C_spec_loop_invariant).is_not_nil()) { - exprt &constraint = static_cast(code.add(spec)); + exprt &invariant = static_cast(code.add(ID_C_spec_loop_invariant)); - typecheck_expr(constraint); - implicit_typecast_bool(constraint); + typecheck_expr(invariant); + implicit_typecast_bool(invariant); + } +} + +void c_typecheck_baset::typecheck_spec_decreases(codet &code) +{ + if(code.find(ID_C_spec_decreases).is_not_nil()) + { + exprt &variant = static_cast(code.add(ID_C_spec_decreases)); + + typecheck_expr(variant); + implicit_typecast_arithmetic(variant); } } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 3dab4f2a856..4115777463b 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -51,7 +51,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr) return; } - // fist do sub-nodes + // first do sub-nodes typecheck_expr_operands(expr); // now do case-split diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 38bcd911c3a..1a86113046c 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -203,6 +203,7 @@ extern char *yyansi_ctext; %token TOK_CPROVER_FINALLY "__CPROVER_finally" %token TOK_CPROVER_ID "__CPROVER_ID" %token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant" +%token TOK_CPROVER_DECREASES "__CPROVER_decreases" %token TOK_CPROVER_REQUIRES "__CPROVER_requires" %token TOK_CPROVER_ENSURES "__CPROVER_ensures" %token TOK_CPROVER_ASSIGNS "__CPROVER_assigns" @@ -497,6 +498,13 @@ loop_invariant_opt: { $$=$3; } ; +cprover_decreases_opt: + /* nothing */ + { init($$); parser_stack($$).make_nil(); } + | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')' + { $$=$3; } + ; + statement_expression: '(' compound_statement ')' { $$=$1; @@ -2418,17 +2426,21 @@ declaration_or_expression_statement: iteration_statement: TOK_WHILE '(' comma_expression_opt ')' - loop_invariant_opt statement + loop_invariant_opt cprover_decreases_opt + statement { $$=$1; statement($$, ID_while); - parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($6))); + parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7))); if(parser_stack($5).is_not_nil()) parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($5)); + + if(parser_stack($6).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6)); } | TOK_DO statement TOK_WHILE '(' comma_expression ')' - loop_invariant_opt ';' + loop_invariant_opt cprover_decreases_opt ';' { $$=$1; statement($$, ID_dowhile); @@ -2436,6 +2448,9 @@ iteration_statement: if(parser_stack($7).is_not_nil()) parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($7)); + + if(parser_stack($8).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8)); } | TOK_FOR { @@ -2449,7 +2464,7 @@ iteration_statement: '(' declaration_or_expression_statement comma_expression_opt ';' comma_expression_opt ')' - loop_invariant_opt + loop_invariant_opt cprover_decreases_opt statement { $$=$1; @@ -2458,11 +2473,14 @@ iteration_statement: mto($$, $4); mto($$, $5); mto($$, $7); - mto($$, $10); + mto($$, $11); if(parser_stack($9).is_not_nil()) parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($9)); + if(parser_stack($10).is_not_nil()) + parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10)); + if(PARSER.for_has_scope) PARSER.pop_scope(); // remove the C99 for-scope } diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index a1afcc773df..92de9458112 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1281,6 +1281,7 @@ __decltype { if(PARSER.cpp98 && {CPROVER_PREFIX}"finally" { loc(); return TOK_CPROVER_FINALLY; } {CPROVER_PREFIX}"ID" { loc(); return TOK_CPROVER_ID; } {CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; } +{CPROVER_PREFIX}"decreases" { loc(); return TOK_CPROVER_DECREASES; } {CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; } {CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; } {CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f405d7f8921..c5f1b9c2008 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -572,6 +572,7 @@ IREP_ID_ONE(is_weak) 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, #spec_requires) IREP_ID_TWO(C_spec_ensures, #spec_ensures) IREP_ID_TWO(C_spec_assigns, #spec_assigns)