Implemented parsing and type checking for loop variants

Long Pham · Long Pham · commit c4b2bbb573fb · 2021-06-21T23:47:12.000Z
diff --git a/regression/contracts/invar_check_break_pass/main.c b/regression/contracts/invar_check_break_pass/main.c
@@ -7,6 +7,7 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
     {
       --r;
       if(r <= 1)
diff --git a/regression/contracts/invar_check_continue/main.c b/regression/contracts/invar_check_continue/main.c
@@ -7,6 +7,7 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
     {
       --r;
       if(r < 5)
diff --git a/regression/contracts/invar_check_multiple_loops/main.c b/regression/contracts/invar_check_multiple_loops/main.c
@@ -7,11 +7,13 @@ int main()
 
   for(r = 0; r < n; ++r)
     __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
+    __CPROVER_decreases(n - r)
     {
       x++;
     }
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
+    __CPROVER_decreases(r)
     {
       y--;
       r--;
diff --git a/regression/contracts/invar_check_nested_loops/main.c b/regression/contracts/invar_check_nested_loops/main.c
@@ -7,12 +7,14 @@ int main()
 
   for(int i = 0; i < n; ++i)
     __CPROVER_loop_invariant(i <= n && s == i)
+    __CPROVER_decreases(n - i)
     {
       int a, b;
       __CPROVER_assume(b >= 0 && a == b);
 
       while(a > 0)
         __CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
+        __CPROVER_decreases(a)
         {
           s++;
           a--;
diff --git a/regression/contracts/invar_check_pointer_modifies-01/main.c b/regression/contracts/invar_check_pointer_modifies-01/main.c
@@ -9,6 +9,7 @@ void main()
   unsigned i;
   while(i > 0)
     __CPROVER_loop_invariant(*data == 42)
+    __CPROVER_decreases(i)
     {
       *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
@@ -11,6 +11,7 @@ void main()
   unsigned i;
   while(i > 0)
     __CPROVER_loop_invariant(*data == 42)
+    __CPROVER_decreases(i)
     {
       *data = 42;
       i--;
diff --git a/regression/contracts/invar_check_sufficiency/main.c b/regression/contracts/invar_check_sufficiency/main.c
@@ -7,6 +7,7 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
     {
       --r;
     }
diff --git a/regression/contracts/invar_loop_constant_no_modify/main.c b/regression/contracts/invar_loop_constant_no_modify/main.c
@@ -7,6 +7,7 @@ int main()
   __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
     {
       r--;
     }
diff --git a/regression/contracts/invar_loop_constant_pass/main.c b/regression/contracts/invar_loop_constant_pass/main.c
@@ -6,6 +6,7 @@ int main()
   __CPROVER_assume(r >= 0);
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0 && s == 1)
+    __CPROVER_decreases(r)
     {
       s = 1;
       r--;
diff --git a/regression/contracts/invariant_side_effects/main.c b/regression/contracts/invariant_side_effects/main.c
@@ -8,6 +8,7 @@ int main()
   *a = 0;
   while(*a < N)
     __CPROVER_loop_invariant((0 <= *a) && (*a <= N))
+    __CPROVER_decreases(N - *a)
     {
       ++(*a);
     }
diff --git a/regression/contracts/variant_parsing_statement_fail/main.c b/regression/contracts/variant_parsing_statement_fail/main.c
@@ -0,0 +1,14 @@
+
+int main()
+{
+  int i = 0; 
+  int N = 10;
+  while (i != N)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(int x = 0)
+  {
+    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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c: In function 'main':$
+^main.c:8:1: error: syntax error before 'int'$
+^     __CPROVER_decreases\(int x = 0\)$
+^PARSING ERROR$
+^EXIT=1$
+^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,13 @@
+int main() 
+{
+  int i = 0; 
+  int N = 10;
+  while (i != N)
+    __CPROVER_loop_invariant(0 <= i && i <= N)
+    __CPROVER_decreases(N - i, 42)
+  {
+    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,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c: In function 'main':$
+^main.c:7:1: error: syntax error before ','$
+^     __CPROVER_decreases\(N - i, 42\)$
+^PARSING ERROR$
+^EXIT=1$
+^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_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_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_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_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_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
`@@ -7,6 +7,7 @@ int main()`
`7`	`7`
`8`	`8`	`while(r > 0)`
`9`	`9`	`__CPROVER_loop_invariant(r >= 0)`
	`10`	`+ __CPROVER_decreases(r)`
`10`	`11`	`{`
`11`	`12`	`--r;`
`12`	`13`	`if(r <= 1)`
Original file line number	Diff line number	Diff line change
`@@ -7,11 +7,13 @@ int main()`
`7`	`7`
`8`	`8`	`for(r = 0; r < n; ++r)`
`9`	`9`	`__CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)`
	`10`	`+ __CPROVER_decreases(n - r)`
`10`	`11`	`{`
`11`	`12`	`x++;`
`12`	`13`	`}`
`13`	`14`	`while(r > 0)`
`14`	`15`	`__CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))`
	`16`	`+ __CPROVER_decreases(r)`
`15`	`17`	`{`
`16`	`18`	`y--;`
`17`	`19`	`r--;`
Original file line number	Diff line number	Diff line change
`@@ -7,12 +7,14 @@ int main()`
`7`	`7`
`8`	`8`	`for(int i = 0; i < n; ++i)`
`9`	`9`	`__CPROVER_loop_invariant(i <= n && s == i)`
	`10`	`+ __CPROVER_decreases(n - i)`
`10`	`11`	`{`
`11`	`12`	`int a, b;`
`12`	`13`	`__CPROVER_assume(b >= 0 && a == b);`
`13`	`14`
`14`	`15`	`while(a > 0)`
`15`	`16`	`__CPROVER_loop_invariant(a >= 0 && s == i + (b - a))`
	`17`	`+ __CPROVER_decreases(a)`
`16`	`18`	`{`
`17`	`19`	`s++;`
`18`	`20`	`a--;`
Original file line number	Diff line number	Diff line change
`@@ -9,6 +9,7 @@ void main()`
`9`	`9`	`unsigned i;`
`10`	`10`	`while(i > 0)`
`11`	`11`	`__CPROVER_loop_invariant(*data == 42)`
	`12`	`+ __CPROVER_decreases(i)`
`12`	`13`	`{`
`13`	`14`	`*data = 42;`
`14`	`15`	`i--;`
Original file line number	Diff line number	Diff line change
`@@ -11,6 +11,7 @@ void main()`
`11`	`11`	`unsigned i;`
`12`	`12`	`while(i > 0)`
`13`	`13`	`__CPROVER_loop_invariant(*data == 42)`
	`14`	`+ __CPROVER_decreases(i)`
`14`	`15`	`{`
`15`	`16`	`*data = 42;`
`16`	`17`	`i--;`
Original file line number	Diff line number	Diff line change
`@@ -7,6 +7,7 @@ int main()`
`7`	`7`	`__CPROVER_assume(r >= 0);`
`8`	`8`	`while(r > 0)`
`9`	`9`	`__CPROVER_loop_invariant(r >= 0)`
	`10`	`+ __CPROVER_decreases(r)`
`10`	`11`	`{`
`11`	`12`	`r--;`
`12`	`13`	`}`
Original file line number	Diff line number	Diff line change
`@@ -6,6 +6,7 @@ int main()`
`6`	`6`	`__CPROVER_assume(r >= 0);`
`7`	`7`	`while(r > 0)`
`8`	`8`	`__CPROVER_loop_invariant(r >= 0 && s == 1)`
	`9`	`+ __CPROVER_decreases(r)`
`9`	`10`	`{`
`10`	`11`	`s = 1;`
`11`	`12`	`r--;`
Original file line number	Diff line number	Diff line change
`@@ -8,6 +8,7 @@ int main()`
`8`	`8`	`*a = 0;`
`9`	`9`	`while(*a < N)`
`10`	`10`	`__CPROVER_loop_invariant((0 <= a) && (a <= N))`
	`11`	`+ __CPROVER_decreases(N - *a)`
`11`	`12`	`{`
`12`	`13`	`++(*a);`
`13`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -51,7 +51,7 @@ void c_typecheck_baset::typecheck_expr(exprt &expr)`
`51`	`51`	`return;`
`52`	`52`	`}`
`53`	`53`
`54`		`- // fist do sub-nodes`
	`54`	`+ // first do sub-nodes`
`55`	`55`	`typecheck_expr_operands(expr);`
`56`	`56`
`57`	`57`	`// now do case-split`