Properly track assigns clause targets in goto converter

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

src/ansi-c/ansi_c_convert_type.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/std_types.h>
 #include <util/string_constant.h>
 
@@ -253,26 +254,22 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
 
-    for(const exprt &operand : to_unary_expr(as_expr).op().operands())
+    for(const exprt &target : to_unary_expr(as_expr).op().operands())
     {
-      if(
-        operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
-        operand.id() != ID_member && operand.id() != ID_dereference)
+      if(!is_lvalue(target))
       {
-        error().source_location = source_location;
+        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;
+      }
+      assigns.push_back(target);
     }
-
-    if(assigns.is_nil())
-      assigns = to_unary_expr(as_expr).op();
-    else
-    {
-      for(auto &assignment : to_unary_expr(as_expr).op().operands())
-        assigns.add_to_operands(std::move(assignment));
-    }
-    assigns.add_source_location() = as_expr.source_location();
   }
   else if(type.id() == ID_C_spec_ensures)
   {
@@ -329,7 +326,7 @@ void ansi_c_convert_typet::write(typet &type)
     if(!requires.empty())
       to_code_with_contract_type(type).requires() = std::move(requires);
 
-    if(assigns.is_not_nil())
+    if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
     if(!ensures.empty())

src/ansi-c/ansi_c_convert_type.h

@@ -47,8 +47,7 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt assigns;
-  exprt::operandst requires, ensures;
+  exprt::operandst assigns, ensures, requires;
 
   // storage spec
   c_storage_spect c_storage_spec;
@@ -87,7 +86,7 @@ class ansi_c_convert_typet:public messaget
     msc_based.make_nil();
     gcc_attribute_mode.make_nil();
 
-    assigns.make_nil();
+    assigns.clear();
     requires.clear();
     ensures.clear();
 

src/ansi-c/c_typecheck_base.cpp

@@ -741,10 +741,10 @@ void c_typecheck_baset::typecheck_declaration(
           }
         }
 
-        if(as_const(code_type).assigns().is_not_nil())
+        if(!as_const(code_type).assigns().empty())
         {
-          for(auto &op : code_type.assigns().operands())
-            typecheck_expr(op);
+          for(auto &target : code_type.assigns())
+            typecheck_expr(target);
         }
 
         if(!as_const(code_type).ensures().empty())

src/ansi-c/expr2c.cpp

@@ -583,10 +583,9 @@ std::string expr2ct::convert_rec(
       dest += " [[requires " + convert(requires) + "]]";
     }
 
-    if(!to_code_with_contract_type(src).assigns().operands().empty())
+    for(auto &assigns : to_code_with_contract_type(src).assigns())
     {
-      dest += " [[assigns " +
-              convert(to_code_with_contract_type(src).assigns()) + "]]";
+      dest += " [[assigns " + convert(assigns) + "]]";
     }
 
     for(auto &ensures : to_code_with_contract_type(src).ensures())

src/util/c_types.h

@@ -339,22 +339,14 @@ class code_with_contract_typet : public code_typet
   {
   }
 
-  bool has_contract() const
+  const exprt::operandst &assigns() const
   {
-    return assigns().is_not_nil() || !requires().empty() || !ensures().empty();
+    return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
   }
 
-  const exprt &assigns() const
+  exprt::operandst &assigns()
   {
-    return static_cast<const exprt &>(find(ID_C_spec_assigns));
-  }
-
-  exprt &assigns()
-  {
-    auto &result = static_cast<exprt &>(add(ID_C_spec_assigns));
-    if(result.id().empty()) // not initialized?
-      result.make_nil();
-    return result;
+    return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
   }
 
   const exprt::operandst &requires() const