Implemented parsing and type checking for loop variants

Long Pham · Long Pham · commit 72f943128fde · 2021-06-23T21:44:04.000Z
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<exprt &>(code.add(spec));
+    exprt &invariant = static_cast<exprt &>(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<exprt &>(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
@@ -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
@@ -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,24 +2426,31 @@ 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);
           parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
 
           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
@@ -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
@@ -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)

Original file line number	Diff line number	Diff line change
`@@ -6,12 +6,18 @@ int main()`
`6`	`6`	`__CPROVER_assume(n > 0 && x == y);`
`7`	`7`
`8`	`8`	`for(r = 0; r < n; ++r)`
	`9`	`+ // clang-format off`
`9`	`10`	`__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)`
	`11`	`+ __CPROVER_decreases(n - r)`
	`12`	`+ // clang-format on`
`10`	`13`	`{`
`11`	`14`	`x++;`
`12`	`15`	`}`
`13`	`16`	`while(r > 0)`
	`17`	`+ // clang-format off`
`14`	`18`	`__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))`
	`19`	`+ __CPROVER_decreases(r)`
	`20`	`+ // clang-format on`
`15`	`21`	`{`
`16`	`22`	`y--;`
`17`	`23`	`r--;`
Original file line number	Diff line number	Diff line change
`@@ -6,7 +6,10 @@ int main()`
`6`	`6`	`__CPROVER_assume(r >= 0);`
`7`	`7`
`8`	`8`	`while(r > 0)`
	`9`	`+ // clang-format off`
`9`	`10`	`__CPROVER_loop_invariant(r >= 0)`
	`11`	`+ __CPROVER_decreases(r)`
	`12`	`+ // clang-format on`
`10`	`13`	`{`
`11`	`14`	`--r;`
`12`	`15`	`}`
Original file line number	Diff line number	Diff line change
`@@ -6,7 +6,10 @@ int main()`
`6`	`6`	`int s = 1;`
`7`	`7`	`__CPROVER_assume(r >= 0);`
`8`	`8`	`while(r > 0)`
	`9`	`+ // clang-format off`
`9`	`10`	`__CPROVER_loop_invariant(r >= 0)`
	`11`	`+ __CPROVER_decreases(r)`
	`12`	`+ // clang-format on`
`10`	`13`	`{`
`11`	`14`	`r--;`
`12`	`15`	`}`