Merge pull request #1282 from diffblue/struct_decay

Verilog: introduce struct_decay and enum_decay methods

Author: tautschnig

src/verilog/verilog_typecheck_expr.cpp

@@ -1928,14 +1928,14 @@ void verilog_typecheck_exprt::implicit_typecast(
   if(dest_type.id()==irep_idt())
     return;
 
-  const typet &src_type = expr.type();
-
   auto &verilog_dest_type = dest_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"
+    const typet &src_type = expr.type();
+
     if(
       src_type.get(ID_C_verilog_type) != ID_verilog_enum ||
       src_type.get(ID_C_identifier) != dest_type.get(ID_C_identifier))
@@ -1946,9 +1946,16 @@ void verilog_typecheck_exprt::implicit_typecast(
     }
   }
 
-  if(src_type == dest_type)
+  if(expr.type() == dest_type)
     return;
 
+  // do enum, union and struct decay
+  enum_decay(expr);
+  struct_decay(expr);
+  union_decay(expr);
+
+  const typet &src_type = expr.type();
+
   if(dest_type.id() == ID_integer)
   {
     if(expr.is_constant())
@@ -2072,19 +2079,6 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
-  else if(src_type.id() == ID_struct || src_type.id() == ID_union)
-  {
-    // packed structs and packed unions can be converted to bits
-    if(
-      dest_type.id() == ID_bool || dest_type.id() == ID_unsignedbv ||
-      dest_type.id() == ID_signedbv ||
-      dest_type.id() == ID_verilog_unsignedbv ||
-      dest_type.id() == ID_verilog_signedbv)
-    {
-      expr = typecast_exprt{expr, dest_type};
-      return;
-    }
-  }
   else if(src_type.id() == ID_verilog_assignment_pattern)
   {
     DATA_INVARIANT(
@@ -2312,6 +2306,28 @@ typet verilog_typecheck_exprt::enum_decay(const typet &type)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::enum_decay
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheck_exprt::enum_decay(exprt &expr) const
+{
+  // Verilog enum types decay to their base type when used in relational
+  // or arithmetic expressions.
+  if(expr.type().get(ID_C_verilog_type) == ID_verilog_enum)
+  {
+    expr = typecast_exprt{expr, enum_decay(expr.type())};
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::union_decay
 
   Inputs:
@@ -2340,6 +2356,32 @@ void verilog_typecheck_exprt::union_decay(exprt &expr) const
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::struct_decay
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheck_exprt::struct_decay(exprt &expr) const
+{
+  // 1800-2017 7.2.1
+  // Verilog packed struct types decay to a vector type [$bits(t)-1:0]
+  // when used in relational or arithmetic expressions.
+  auto &type = expr.type();
+  if(type.id() == ID_struct)
+  {
+    auto new_type =
+      unsignedbv_typet{numeric_cast_v<std::size_t>(get_width(type))};
+    expr = typecast_exprt{expr, new_type};
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::tc_binary_expr
 
   Inputs:

src/verilog/verilog_typecheck_expr.h

@@ -146,7 +146,9 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   }
 
   static typet enum_decay(const typet &);
+  void enum_decay(exprt &) const;
   void union_decay(exprt &) const;
+  void struct_decay(exprt &) const;
   typet max_type(const typet &t1, const typet &t2);
 
   // named blocks