Merge pull request #1318 from diffblue/move-assignment-conversion

Verilog: move assignment conversion code

Author: tautschnig

src/verilog/verilog_typecheck.cpp

@@ -1420,7 +1420,7 @@ void verilog_typecheckt::convert_case_values(
 
     // This works like a relational operator, not like an assignment
     typet t=max_type(it->type(), case_operand.type());
-    propagate_type(*it, t);
+    downwards_type_propagation(*it, t);
   }
 }
 

src/verilog/verilog_typecheck_expr.cpp

@@ -89,7 +89,7 @@ void verilog_typecheck_exprt::enter_named_block(const irep_idt &name)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::propagate_type
+Function: verilog_typecheck_exprt::assignment_conversion
 
   Inputs:
 
@@ -99,125 +99,205 @@ Function: verilog_typecheck_exprt::propagate_type
 
 \*******************************************************************/
 
-void verilog_typecheck_exprt::propagate_type(
-  exprt &expr,
-  const typet &type)
+void verilog_typecheck_exprt::assignment_conversion(
+  exprt &rhs,
+  const typet &lhs_type)
 {
-  auto &verilog_dest_type = type.get(ID_C_verilog_type);
+  // 1800-2017 10.9
+  if(rhs.type().id() == ID_verilog_assignment_pattern)
+  {
+    DATA_INVARIANT(
+      rhs.id() == ID_verilog_assignment_pattern,
+      "verilog_assignment_pattern expression expected");
+
+    if(lhs_type.id() == ID_struct)
+    {
+      auto &struct_type = to_struct_type(lhs_type);
+      auto &components = struct_type.components();
+
+      if(
+        !rhs.operands().empty() &&
+        rhs.operands().front().id() == ID_member_initializer)
+      {
+        exprt::operandst initializers{components.size(), nil_exprt{}};
+
+        for(auto &op : rhs.operands())
+        {
+          PRECONDITION(op.id() == ID_member_initializer);
+          auto member_name = op.get(ID_member_name);
+          if(!struct_type.has_component(member_name))
+          {
+            throw errort().with_location(op.source_location())
+              << "struct does not have a member `" << member_name << "'";
+          }
+          auto nr = struct_type.component_number(member_name);
+          auto value = to_unary_expr(op).op();
+          // rec. call
+          assignment_conversion(value, components[nr].type());
+          initializers[nr] = std::move(value);
+        }
+
+        // Is every member covered?
+        for(std::size_t i = 0; i < components.size(); i++)
+          if(initializers[i].is_nil())
+          {
+            throw errort().with_location(rhs.source_location())
+              << "assignment pattern does not assign member `"
+              << components[i].get_name() << "'";
+          }
+
+        rhs = struct_exprt{std::move(initializers), struct_type}
+                .with_source_location(rhs.source_location());
+      }
+      else
+      {
+        if(rhs.operands().size() != components.size())
+        {
+          throw errort().with_location(rhs.source_location())
+            << "number of expressions does not match number of struct members";
+        }
+
+        for(std::size_t i = 0; i < components.size(); i++)
+        {
+          // rec. call
+          assignment_conversion(rhs.operands()[i], components[i].type());
+        }
+
+        // turn into struct expression
+        rhs.id(ID_struct);
+        rhs.type() = lhs_type;
+      }
+
+      return;
+    }
+    else if(lhs_type.id() == ID_array)
+    {
+      auto &array_type = to_array_type(lhs_type);
+      auto &element_type = array_type.element_type();
+      auto array_size =
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+
+      if(array_size != rhs.operands().size())
+      {
+        throw errort().with_location(rhs.source_location())
+          << "number of expressions does not match number of array elements";
+      }
+
+      for(std::size_t i = 0; i < array_size; i++)
+      {
+        // rec. call
+        assignment_conversion(rhs.operands()[i], element_type);
+      }
+
+      // turn into array expression
+      rhs.id(ID_array);
+      rhs.type() = lhs_type;
+      return;
+    }
+    else
+    {
+      throw errort().with_location(rhs.source_location())
+        << "cannot convert assignment pattern to '" << to_string(lhs_type)
+        << '\'';
+    }
+  }
+
+  auto original_rhs_type = rhs.type(); // copy
+
+  auto &verilog_dest_type = lhs_type.get(ID_C_verilog_type);
   if(verilog_dest_type == ID_verilog_enum)
   {
     // IEEE 1800-2017 6.19.3: "a variable of type enum cannot be directly
     // assigned a value that lies outside the enumeration set unless an
     // explicit cast is used"
     if(
-      expr.type().get(ID_C_verilog_type) != ID_verilog_enum ||
-      expr.type().get(ID_C_identifier) != type.get(ID_C_identifier))
+      rhs.type().get(ID_C_verilog_type) != ID_verilog_enum ||
+      rhs.type().get(ID_C_identifier) != lhs_type.get(ID_C_identifier))
     {
-      throw errort().with_location(expr.source_location())
+      throw errort().with_location(rhs.source_location())
         << "assignment to enum requires enum of the same type, but got "
-        << to_string(expr.type());
+        << to_string(rhs.type());
     }
   }
 
-  if(expr.type()==type)
+  if(lhs_type == rhs.type())
     return;
 
-  if(expr.type().id() == ID_verilog_sva_sequence)
-  {
-    throw errort{}.with_location(expr.source_location())
-      << "cannot use SVA sequence as an expression";
-  }
-  else if(expr.type().id() == ID_verilog_sva_property)
+  // do enum, union and struct decay
+  enum_decay(rhs);
+  struct_decay(rhs);
+  union_decay(rhs);
+
+  if(rhs.type().id() == ID_struct || rhs.type().id() == ID_union)
   {
-    throw errort{}.with_location(expr.source_location())
-      << "cannot use SVA property as an expression";
+    // not decayed, not equal
+    throw errort().with_location(rhs.source_location())
+      << "failed to convert `" << to_string(original_rhs_type) << "' to `"
+      << to_string(lhs_type) << "'";
   }
 
-  vtypet vt_from=vtypet(expr.type());
-  vtypet vt_to  =vtypet(type);
+  // Implements 1800-2017 10.7 and 1800-2017 11.8.3.
 
-  if(!vt_from.is_other() && !vt_to.is_other() &&
-     expr.has_operands())
+  if(
+    lhs_type.id() == ID_verilog_real || lhs_type.id() == ID_verilog_shortreal ||
+    lhs_type.id() == ID_verilog_realtime ||
+    rhs.type().id() == ID_verilog_real ||
+    rhs.type().id() == ID_verilog_shortreal)
   {
-    // arithmetic
+    // from/to real is just a cast
+    rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
+    return;
+  }
 
+  if(rhs.type().id() == ID_verilog_null)
+  {
     if(
-      expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
-      expr.id() == ID_div || expr.id() == ID_unary_minus ||
-      expr.id() == ID_unary_plus)
+      lhs_type.id() == ID_verilog_chandle ||
+      lhs_type.id() == ID_verilog_class_type ||
+      lhs_type.id() == ID_verilog_event)
     {
-      if(type.id()!=ID_bool)
-      {
-        Forall_operands(it, expr)
-          propagate_type(*it, type);
-
-        expr.type()=type;
-
-        return;
-      }
+      rhs = typecast_exprt{rhs, lhs_type};
+      return;
     }
-    else if(expr.id()==ID_bitand  ||
-            expr.id()==ID_bitor   ||
-            expr.id()==ID_bitnand ||
-            expr.id()==ID_bitnor  ||
-            expr.id()==ID_bitxor  ||
-            expr.id()==ID_bitxnor ||
-            expr.id()==ID_bitnot)
-    {
-      Forall_operands(it, expr)
-        propagate_type(*it, type);
+  }
 
-      expr.type()=type;
+  // "The size of the left-hand side of an assignment forms
+  // the context for the right-hand expression."
 
-      if(type.id()==ID_bool)
-      {
-        if(expr.id()==ID_bitand)
-          expr.id(ID_and);
-        else if(expr.id()==ID_bitor)
-          expr.id(ID_or);
-        else if(expr.id()==ID_bitnand)
-          expr.id(ID_nand);
-        else if(expr.id()==ID_bitnor)
-          expr.id(ID_nor);
-        else if(expr.id()==ID_bitxor)
-          expr.id(ID_xor);
-        else if(expr.id()==ID_bitxnor)
-          expr.id(ID_xnor);
-        else if(expr.id()==ID_bitnot)
-          expr.id(ID_not);
-      }
+  // Get the width of LHS and RHS
+  auto lhs_width = get_width(lhs_type);
+  auto rhs_width = get_width(rhs.type());
 
-      return;
-    }
-    else if(expr.id()==ID_if)
+  if(lhs_width > rhs_width)
+  {
+    // Need to enlarge the RHS.
+    //
+    // "If needed, extend the size of the right-hand side,
+    // performing sign extension if, and only if, the type
+    // of the right-hand side is signed.
+    if(
+      (rhs.type().id() == ID_signedbv ||
+       rhs.type().id() == ID_verilog_signedbv) &&
+      (lhs_type.id() == ID_unsignedbv ||
+       lhs_type.id() == ID_verilog_unsignedbv))
     {
-      if(expr.operands().size()==3)
-      {
-        propagate_type(to_if_expr(expr).true_case(), type);
-        propagate_type(to_if_expr(expr).false_case(), type);
+      // LHS is unsigned, RHS is signed. Must sign-extend.
+      auto new_rhs_type = to_bitvector_type(rhs.type());
+      new_rhs_type.set_width(numeric_cast_v<std::size_t>(lhs_width));
 
-        expr.type()=type;
-        return;
-      }
-    }
-    else if(expr.id()==ID_shl) // does not work with shr
-    {
-      // does not work with boolean
-      if(type.id()!=ID_bool)
-      {
-        if(expr.operands().size()==2)
-        {
-          propagate_type(to_binary_expr(expr).op0(), type);
-          // not applicable to second operand
+      downwards_type_propagation(rhs, new_rhs_type);
 
-          expr.type()=type;
-          return;
-        }
-      }
+      // then cast
+      rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
     }
+    else
+      downwards_type_propagation(rhs, lhs_type);
+  }
+  else
+  {
+    // no need to enlarge
+    rhs = typecast_exprt::conditional_cast(rhs, lhs_type);
   }
-
-  implicit_typecast(expr, type);
 }
 
 /*******************************************************************\
@@ -612,7 +692,7 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
   }
 
   for(unsigned i=0; i<arguments.size(); i++)
-    propagate_type(arguments[i], parameter_types[i].type());
+    assignment_conversion(arguments[i], parameter_types[i].type());
 
   return std::move(expr);
 }

src/verilog/verilog_typecheck_expr.h

@@ -65,7 +65,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   void make_boolean(exprt &expr);
 
-  void propagate_type(exprt &expr, const typet &type);
+  void assignment_conversion(exprt &expr, const typet &type);
   void downwards_type_propagation(exprt &, const typet &);
 
   [[nodiscard]] typet elaborate_type(const typet &);

src/verilog/verilog_typecheck_sva.cpp

@@ -295,7 +295,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr)
       {
         convert_expr(pattern);
         typet t = max_type(pattern.type(), case_expr.case_op().type());
-        propagate_type(pattern, t);
+        downwards_type_propagation(pattern, t);
       }
 
       convert_sva(case_item.result());