Merge pull request #6214 from diffblue/multiple_invariants

Allow multiple loop invariants

Author: feliperodri

regression/contracts/invar_check_multiple_loops/main.c

@@ -7,7 +7,8 @@ int main()
 
   for(r = 0; r < n; ++r)
     // clang-format off
-    __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r)
+    __CPROVER_loop_invariant(0 <= r && r <= n)
+    __CPROVER_loop_invariant(x == y + r)
     __CPROVER_decreases(n - r)
     // clang-format on
     {

src/ansi-c/c_typecheck_code.cpp

@@ -815,10 +815,12 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())
   {
-    exprt &invariant = static_cast<exprt &>(code.add(ID_C_spec_loop_invariant));
-
-    typecheck_expr(invariant);
-    implicit_typecast_bool(invariant);
+    for(auto &invariant :
+        (static_cast<exprt &>(code.add(ID_C_spec_loop_invariant)).operands()))
+    {
+      typecheck_expr(invariant);
+      implicit_typecast_bool(invariant);
+    }
   }
 }
 

src/ansi-c/parser.y

@@ -491,11 +491,22 @@ quantifier_expression:
         }
         ;
 
-loop_invariant_opt:
+loop_invariant:
+          TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
+        { $$=$3; }
+        ;
+
+loop_invariant_list:
+          loop_invariant
+        { init($$); mto($$, $1); }
+        | loop_invariant_list loop_invariant
+        { $$=$1; mto($$, $2); }
+        ;
+
+loop_invariant_list_opt:
         /* nothing */
         { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_LOOP_INVARIANT '(' ACSL_binding_expression ')'
-        { $$=$3; }
+        | loop_invariant_list
         ;
 
 cprover_decreases_opt:
@@ -2426,28 +2437,28 @@ declaration_or_expression_statement:
 
 iteration_statement:
         TOK_WHILE '(' comma_expression_opt ')'
-          loop_invariant_opt cprover_decreases_opt 
+          loop_invariant_list_opt cprover_decreases_opt
           statement
         {
           $$=$1;
           statement($$, ID_while);
           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($5).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($5).operands());
 
           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 cprover_decreases_opt ';'
+          loop_invariant_list_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($7).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($7).operands());
 
           if(parser_stack($8).is_not_nil())
             parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($8));
@@ -2464,7 +2475,7 @@ iteration_statement:
           '(' declaration_or_expression_statement
               comma_expression_opt ';'
               comma_expression_opt ')'
-              loop_invariant_opt cprover_decreases_opt
+              loop_invariant_list_opt cprover_decreases_opt
           statement
         {
           $$=$1;
@@ -2475,8 +2486,8 @@ iteration_statement:
           mto($$, $7);
           mto($$, $11);
 
-          if(parser_stack($9).is_not_nil())
-            parser_stack($$).add(ID_C_spec_loop_invariant).swap(parser_stack($9));
+          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).is_not_nil())
             parser_stack($$).add(ID_C_spec_decreases).swap(parser_stack($10));

src/goto-instrument/code_contracts.cpp

@@ -149,6 +149,11 @@ void code_contractst::check_apply_loop_contracts(
         << messaget::eom;
     }
   }
+  else
+  {
+    // form the conjunction
+    invariant = conjunction(invariant.operands());
+  }
 
   // change
   //   H: loop;