type checking & conversion of loop assigns clauses

Author: SaswatPadhi

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())
         {

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);
 

src/ansi-c/c_typecheck_code.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/range.h>
 #include <util/string_constant.h>
 
@@ -486,6 +487,10 @@ 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)
@@ -775,6 +780,10 @@ 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)
@@ -809,6 +818,41 @@ 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" << 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;
+    }
+  }
 }
 
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)

src/goto-programs/goto_convert.cpp

@@ -863,11 +863,16 @@ 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 +885,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 +979,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 +1037,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 +1106,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);