Parser support for assigns contracts on loops

1. Renamed cprover_contract_assigns_opt to cprover_contract_assigns.
2. Created cprover_contract_assigns_opt which has a unit production and cprover_contract_assigns.
3. Renamed cprover_decreases_opt to cprover_contract_decreases_opt.
4. Renamed loop_invariant to cprover_contract_loop_invariant.
5. Renamed loop_invariant_list to cprover_contract_loop_invariant_list.
6. Renamed loop_invariant_list_opt to cprover_contract_loop_invariant_list_opt.
7. Added cprover_contract_assigns_opt to iteration statement.
8. Created the regression test invar_assigns_alias_analysis (KNOWNBUG).
9. Created the regression test invar_assigns_opt (CORE).
10. Created the regression test invar_assigns_empty (CORE).

This adds parser support for assigns contracts on loops.

Author: Aalok Thakkar

regression/contracts/invar_assigns_alias_analysis/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob { char *data; };
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for (unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(b->data)
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+  {
+    b->data[i] = 1;
+  }
+
+  assert(b->data[5] == 0);
+}

regression/contracts/invar_assigns_alias_analysis/test.desc

@@ -0,0 +1,14 @@
+KNOWNBUG
+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 b->data[5] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test shows that the current implementation only supports
+parsing and still uses alias analysis. Fixing this is a part 
+of future work.

regression/contracts/invar_assigns_empty/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    __CPROVER_assigns()
+    __CPROVER_loop_invariant(r >= 0)
+    {
+      r--;
+    }
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts/invar_assigns_empty/test.desc

@@ -0,0 +1,12 @@
+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 r == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that empty assigns clause is supported.

regression/contracts/invar_assigns_opt/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main()
+{
+  int r1, s1 = 1;
+  __CPROVER_assume(r1 >= 0);
+  while(r1 > 0)
+    __CPROVER_loop_invariant(r1 >= 0 && s1 == 1)
+    __CPROVER_decreases(r1)
+    {
+      s1 = 1;
+      r1--;
+    }
+  assert(r1 == 0);
+  assert(s1 == 1);
+
+  int r2, s2 = 1;
+  __CPROVER_assume(r2 >= 0);
+  while(r2 > 0)
+    __CPROVER_assigns(r2, s2)
+    __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)
+    __CPROVER_decreases(r2)
+    {
+      s2 = 1;
+      r2--;
+    }
+  assert(r2 == 0);
+  assert(s2 == 1);
+  return 0;
+}

regression/contracts/invar_assigns_opt/test.desc

@@ -0,0 +1,20 @@
+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.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$
+^\[main.4\] .* Check loop invariant before entry: SUCCESS$
+^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.2\] .* assertion r2 == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that adding assigns clause is optional
+and that if a proof does not require it, then adding an
+appropriate assigns clause does not lead to any 
+unexpected behavior. 

regression/contracts/invar_check_multiple_loops/main.c

@@ -27,4 +27,4 @@ int main()
   assert(x == y + 2 * n);
 
   return 0;
-}
+}

regression/contracts/invar_check_nested_loops/main.c

@@ -16,6 +16,7 @@ int main()
 
       while(a > 0)
         // clang-format off
+        __CPROVER_assigns(s, a)
         __CPROVER_loop_invariant(a >= 0 && s == i + (b - a))
         __CPROVER_decreases(a)
         // clang-format on

regression/contracts/invar_dynamic_struct_member/main.c

@@ -9,7 +9,7 @@ void main()
   t->x = 0;
 
   unsigned n;
-  for(unsigned i = 0; i < n; ++i)
+  for(unsigned i = 0; i < n; ++i)  
     __CPROVER_loop_invariant(i <= n)
     {
       switch(i % 4)

regression/contracts/invar_loop_constant_pass/test.desc

@@ -10,4 +10,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that the invariant is correctly used to satisfy
-all assertions that follow a loop.
+all assertions that follow a loop.

src/ansi-c/parser.y

@@ -491,25 +491,25 @@ quantifier_expression:
         }
         ;
 
-loop_invariant:
+cprover_contract_loop_invariant:
           TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
         { $$=$3; }
         ;
 
-loop_invariant_list:
-          loop_invariant
+cprover_contract_loop_invariant_list:
+          cprover_contract_loop_invariant
         { init($$); mto($$, $1); }
-        | loop_invariant_list loop_invariant
+        | cprover_contract_loop_invariant_list cprover_contract_loop_invariant
         { $$=$1; mto($$, $2); }
         ;
 
-loop_invariant_list_opt:
+cprover_contract_loop_invariant_list_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | loop_invariant_list
+        | cprover_contract_loop_invariant_list
         ;
 
-cprover_decreases_opt:
+cprover_contract_decreases_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
         | TOK_CPROVER_DECREASES '(' ACSL_binding_expression ')'
@@ -2437,31 +2437,35 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          loop_invariant_list_opt cprover_decreases_opt
+          cprover_contract_assigns_opt
+          cprover_contract_loop_invariant_list_opt 
+          cprover_contract_decreases_opt
           statement
         {
           $$=$1;
           statement($$, ID_while);
-          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($7)));
+          parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
 
-          if(!parser_stack($5).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($5).operands());
+          if(!parser_stack($6).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
 
-          if(parser_stack($6).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($6));
+          if(parser_stack($7).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($7));
         }
         | TOK_DO statement TOK_WHILE '(' comma_expression ')'
-          loop_invariant_list_opt cprover_decreases_opt ';'
+          cprover_contract_assigns_opt
+          cprover_contract_loop_invariant_list_opt 
+          cprover_contract_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).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
+          if(!parser_stack($8).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
 
-          if(parser_stack($8).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
+          if(parser_stack($9).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($9));
         }
         | TOK_FOR
           {
@@ -2475,7 +2479,9 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              loop_invariant_list_opt cprover_decreases_opt
+              cprover_contract_assigns_opt
+              cprover_contract_loop_invariant_list_opt 
+              cprover_contract_decreases_opt
           statement
         {
           $$=$1;
@@ -2484,13 +2490,13 @@ iteration_statement:
           mto($$, $4);
           mto($$, $5);
           mto($$, $7);
-          mto($$, $11);
+          mto($$, $12);
 
-          if(!parser_stack($9).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($9).operands());
+          if(!parser_stack($10).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
 
-          if(parser_stack($10).is_not_nil())
-            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));
+          if(parser_stack($11).is_not_nil())
+            parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($11));
 
           if(PARSER.for_has_scope)
             PARSER.pop_scope(); // remove the C99 for-scope
@@ -3272,10 +3278,10 @@ cprover_function_contract:
           set($$, ID_C_spec_requires);
           mto($$, $3);
         }
-        | cprover_contract_assigns_opt
+        | cprover_contract_assigns
         ;
 
-cprover_contract_assigns_opt:
+cprover_contract_assigns:
          TOK_CPROVER_ASSIGNS '(' argument_expression_list ')'
         {
           $$=$1;
@@ -3291,6 +3297,12 @@ cprover_contract_assigns_opt:
         }
         ;
 
+cprover_contract_assigns_opt:
+        /* nothing */
+        { init($$); parser_stack($$).make_nil(); }
+        | cprover_contract_assigns
+        ;
+
 cprover_function_contract_sequence:
           cprover_function_contract
         | cprover_function_contract_sequence cprover_function_contract