parsing, type checking & conversion of loop assigns clauses

SaswatPadhi · SaswatPadhi · commit e0da7e79c461 · 2021-11-23T17:00:41.000Z
In this commit we implement the parsing actions, type checking and conversion routines for assigns clauses on loops. The syntax rules along with regressions tests were introduced in an earlier PR: #6196.
diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_elvis_4/test.desc b/regression/contracts/assigns_enforce_elvis_4/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: void-typed targets not permitted$
+^.*error: void-typed targets not permitted in assigns clause$
 --
 --
 Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected.
diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: void-typed targets not permitted$
+^.*error: void-typed targets not permitted in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --
diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-error: illegal target in assigns clause
+error: non-lvalue target in assigns clause
 --
 Checks whether type checking reports illegal target in assigns clause.
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
@@ -739,33 +739,7 @@ void c_typecheck_baset::typecheck_declaration(
             CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
         }
 
-        for(auto &target : code_type.assigns())
-        {
-          typecheck_expr(target);
-
-          if(target.type().id() == ID_empty)
-          {
-            error().source_location = target.source_location();
-            error() << "void-typed targets not permitted" << eom;
-            throw 0;
-          }
-          else if(target.id() == ID_pointer_object)
-          {
-            // skip
-          }
-          else if(!target.get_bool(ID_C_lvalue))
-          {
-            error().source_location = target.source_location();
-            error() << "illegal target in assigns clause" << eom;
-            throw 0;
-          }
-          else if(has_subexpr(target, ID_side_effect))
-          {
-            error().source_location = target.source_location();
-            error() << "assigns clause is not side-effect free" << eom;
-            throw 0;
-          }
-        }
+        typecheck_spec_assigns(code_type.assigns());
 
         if(!as_const(code_type).ensures().empty())
         {
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -144,6 +144,9 @@ 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);
+
+  // contracts
+  virtual void typecheck_spec_assigns(exprt::operandst &targets);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/range.h>
 #include <util/string_constant.h>
 
@@ -493,6 +494,12 @@ void c_typecheck_baset::typecheck_for(codet &code)
 
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
+
+  if(code.find(ID_C_spec_assigns).is_not_nil())
+  {
+    typecheck_spec_assigns(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
+  }
 }
 
 void c_typecheck_baset::typecheck_label(code_labelt &code)
@@ -782,6 +789,12 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
 
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
+
+  if(code.find(ID_C_spec_assigns).is_not_nil())
+  {
+    typecheck_spec_assigns(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
+  }
 }
 
 void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
@@ -816,6 +829,43 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
 
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
+
+  if(code.find(ID_C_spec_assigns).is_not_nil())
+  {
+    typecheck_spec_assigns(
+      static_cast<unary_exprt &>(code.add(ID_C_spec_assigns)).op().operands());
+  }
+}
+
+void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets)
+{
+  for(auto &target : targets)
+  {
+    typecheck_expr(target);
+
+    if(target.type().id() == ID_empty)
+    {
+      error().source_location = target.source_location();
+      error() << "void-typed targets not permitted in assigns clause" << eom;
+      throw 0;
+    }
+    else if(target.id() == ID_pointer_object)
+    {
+      // skip
+    }
+    else if(!target.get_bool(ID_C_lvalue))
+    {
+      error().source_location = target.source_location();
+      error() << "non-lvalue target in assigns clause" << eom;
+      throw 0;
+    }
+    else if(has_subexpr(target, ID_side_effect))
+    {
+      error().source_location = target.source_location();
+      error() << "assigns clause is not side-effect free" << eom;
+      throw 0;
+    }
+  }
 }
 
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
@@ -2453,6 +2453,9 @@ iteration_statement:
           statement($$, ID_while);
           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_assigns)).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());
 
@@ -2468,6 +2471,9 @@ iteration_statement:
           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_assigns)).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());
 
@@ -2499,6 +2505,9 @@ iteration_statement:
           mto($$, $7);
           mto($$, $12);
 
+          if(!parser_stack($9).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).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());
 
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -863,11 +863,15 @@ void goto_convertt::convert_loop_contracts(
   goto_programt::targett loop,
   const irep_idt &mode)
 {
-  exprt invariant =
-    static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
-  exprt decreases_clause =
-    static_cast<const exprt &>(code.find(ID_C_spec_decreases));
+  auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
+  if(assigns.is_not_nil())
+  {
+    PRECONDITION(loop->is_goto());
+    loop->guard.add(ID_C_spec_assigns).swap(assigns.op());
+  }
 
+  auto invariant =
+    static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
   if(!invariant.is_nil())
   {
     if(has_subexpr(invariant, ID_side_effect))
@@ -880,6 +884,8 @@ void goto_convertt::convert_loop_contracts(
     loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
   }
 
+  auto decreases_clause =
+    static_cast<const exprt &>(code.find(ID_C_spec_decreases));
   if(!decreases_clause.is_nil())
   {
     if(has_subexpr(decreases_clause, ID_side_effect))
@@ -972,7 +978,7 @@ void goto_convertt::convert_for(
   goto_programt::targett y = tmp_y.add(
     goto_programt::make_goto(u, true_exprt(), code.source_location()));
 
-  // loop invariant and decreases clause
+  // assigns clause, loop invariant and decreases clause
   convert_loop_contracts(code, y, mode);
 
   dest.destructive_append(sideeffects);
@@ -1030,7 +1036,7 @@ void goto_convertt::convert_while(
   goto_programt tmp_x;
   convert(code.body(), tmp_x, mode);
 
-  // loop invariant and decreases clause
+  // assigns clause, loop invariant and decreases clause
   convert_loop_contracts(code, y, mode);
 
   dest.destructive_append(tmp_branch);
@@ -1099,7 +1105,7 @@ void goto_convertt::convert_dowhile(
   // y: if(c) goto w;
   y->complete_goto(w);
 
-  // loop invariant and decreases clause
+  // assigns_clause, loop invariant and decreases clause
   convert_loop_contracts(code, y, mode);
 
   dest.destructive_append(tmp_w);
