Merge pull request #371 from diffblue/strong-enum-typing

Verilog: strong typing for enums

regression/verilog/data-types/enum2.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 enum2.sv
 
-^EXIT=10$
+^file .* line 4: assignment to enum requires enum of the same type$
+^EXIT=2$
 ^SIGNAL=0$
 --
---
-enum constants must be strongly typed.

regression/verilog/data-types/enum4.desc

@@ -1,9 +1,7 @@
-KNOWNBUG
+CORE
 enum4.sv
 --bound 0
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^\[main\.property\.p1\] always main\.my_light != 0 \+ 1 \+ 1 \+ 1: PROVED up to bound 0$
+^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
 --
---
-Type conversion not working

regression/verilog/data-types/enum_base_type1.desc

@@ -0,0 +1,7 @@
+CORE
+enum_base_type1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[.*\] always 8 == 8: PROVED up to bound 0$
+--

regression/verilog/data-types/enum_base_type1.sv

@@ -0,0 +1,8 @@
+module main;
+
+  typedef enum bit [7:0] { A } enum_t;
+
+  // expected to pass
+  p1: assert property ($bits(A) == 8);
+
+endmodule

regression/verilog/data-types/enum_cast1.desc

@@ -0,0 +1,8 @@
+CORE
+enum_cast1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$
+^\[main\.property\.p2\] always 2 == 2: PROVED up to bound 0$
+--

regression/verilog/data-types/enum_cast1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  typedef enum { A = 1, B = 2 } enum_t;
+
+  // expected to pass
+  p1: assert property (A == enum_t'(1));
+  p2: assert property (B == enum_t'(2));
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -106,6 +106,7 @@ IREP_ID_ONE(uwire)
 IREP_ID_ONE(wand)
 IREP_ID_ONE(automatic)
 IREP_ID_ONE(verilog_enum)
+IREP_ID_TWO(C_verilog_type, #verilog_type)
 IREP_ID_ONE(verilog_type_reference)
 IREP_ID_ONE(enum_names)
 IREP_ID_ONE(var)

src/verilog/parser.y

@@ -1253,6 +1253,11 @@ data_type:
 	          init($$, ID_verilog_enum);
 	          stack_type($$).add_subtype() = std::move(stack_type($2));
 	          stack_type($$).set(ID_enum_names, stack_type($4));
+
+	          // We attach a dummy id to distinguish two syntactically
+	          // identical enum types.
+	          auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id();
+	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
 	        { init($$, ID_string); }
@@ -1328,7 +1333,9 @@ enum_base_type_opt:
 		{ init($$, ID_nil); }
 	| integer_atom_type signing_opt
 	| integer_vector_type signing_opt packed_dimension_opt
+		{ $$ = $3; add_as_subtype(stack_type($$), stack_type($1)); }
 	| type_identifier packed_dimension_opt
+		{ $$ = $2; add_as_subtype(stack_type($$), stack_type($1)); }
 	;
 
 non_integer_type:
@@ -2125,7 +2132,7 @@ gate_instance:
 
 name_of_gate_instance_opt:
 	  /* Optional */ 
-	        { init($$, "$_&#ANON" + PARSER.get_dummy_id()); }
+	        { init($$, "$_&#ANON" + PARSER.get_next_id()); }
 	| name_of_gate_instance
 	;
 
@@ -2192,7 +2199,7 @@ module_instance:
 	;
 
 name_of_instance:
-	  { init($$, "$_&#ANON" + PARSER.get_dummy_id());}
+	  { init($$, "$_&#ANON" + PARSER.get_next_id());}
 	| TOK_NON_TYPE_IDENTIFIER
 	;
 

src/verilog/verilog_elaborate.cpp

@@ -102,9 +102,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
     if(enum_type.has_base_type())
       collect_symbols(enum_type.base_type());
 
-    // The default base type is 'int'.
-    auto base_type =
-      enum_type.has_base_type() ? enum_type.base_type() : signedbv_typet(32);
+    // convert the type now
+    auto converted_type = convert_type(enum_type);
 
     // Add the enum names to the symbol table for subsequent elaboration.
     // Values are given, or the previous plus one, starting with value '0'.
@@ -113,13 +112,17 @@ void verilog_typecheckt::collect_symbols(const typet &type)
     for(auto &enum_name : enum_type.enum_names())
     {
       if(enum_name.value().is_not_nil())
-        initializer = enum_name.value();
+      {
+        exprt tmp = enum_name.value();
+        convert_expr(tmp);
+        initializer = std::move(tmp);
+      }
 
-      exprt value = typecast_exprt(initializer, base_type);
+      exprt value = typecast_exprt(initializer, converted_type);
 
       const auto base_name = enum_name.base_name();
       const auto identifier = hierarchical_identifier(base_name);
-      symbolt enum_name_symbol(identifier, base_type, mode);
+      symbolt enum_name_symbol(identifier, converted_type, mode);
       enum_name_symbol.module = module_identifier;
       enum_name_symbol.base_name = base_name;
       enum_name_symbol.value = std::move(value);
@@ -128,8 +131,8 @@ void verilog_typecheckt::collect_symbols(const typet &type)
       add_symbol(std::move(enum_name_symbol));
 
       initializer = plus_exprt(
-        typecast_exprt(initializer, base_type),
-        typecast_exprt(from_integer(1, integer_typet()), base_type));
+        typecast_exprt(initializer, converted_type),
+        typecast_exprt(from_integer(1, integer_typet()), converted_type));
     }
   }
 }

src/verilog/verilog_parser.h

@@ -46,7 +46,6 @@ class verilog_parsert:public parsert
 
   verilog_parsert():mode(VIS_VERILOG)
   {
-    dummy_id=0;
   }
 
   // parser scopes and identifiers
@@ -118,12 +117,14 @@ class verilog_parsert:public parsert
     return scope_ptr == nullptr ? false : scope_ptr->is_type;
   }
 
-  unsigned dummy_id;
+  // These are used for anonymous gate instances
+  // and to create a unique identifier for enum types.
+  std::size_t next_id_counter = 0;
 
-  std::string get_dummy_id()
+  std::string get_next_id()
   {
-    dummy_id++;
-    return integer2string(dummy_id-1);
+    next_id_counter++;
+    return integer2string(next_id_counter - 1);
   }
 };
 

src/verilog/verilog_typecheck_expr.cpp

@@ -94,6 +94,21 @@ void verilog_typecheck_exprt::propagate_type(
   exprt &expr,
   const typet &type)
 {
+  auto &verilog_dest_type = 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))
+    {
+      throw errort().with_location(expr.source_location())
+        << "assignment to enum requires enum of the same type";
+    }
+  }
+
   if(expr.type()==type)
     return;
 
@@ -193,7 +208,7 @@ void verilog_typecheck_exprt::propagate_type(
     }
   }
 
-  typecast(expr, type);
+  implicit_typecast(expr, type);
 }
 
 /*******************************************************************\
@@ -1436,7 +1451,7 @@ bool verilog_typecheck_exprt::is_constant_expression(
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::typecast
+Function: verilog_typecheck_exprt::implicit_typecast
 
   Inputs:
 
@@ -1446,13 +1461,28 @@ Function: verilog_typecheck_exprt::typecast
 
 \*******************************************************************/
 
-void verilog_typecheck_exprt::typecast(
+void verilog_typecheck_exprt::implicit_typecast(
   exprt &expr,
   const typet &dest_type)
 {
   if(dest_type.id()==irep_idt())
     return;
 
+  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"
+    if(
+      expr.type().get(ID_C_verilog_type) != ID_verilog_enum ||
+      expr.type().get(ID_C_identifier) != dest_type.get(ID_C_identifier))
+    {
+      throw errort().with_location(expr.source_location())
+        << "assignment to enum requires enum of the same type";
+    }
+  }
+
   if(expr.type()==dest_type)
     return;
 
@@ -1800,7 +1830,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   }
   else if(expr.id() == ID_typecast)
   {
-    // System Verilog has got type'(expr).
+    // System Verilog has got type'(expr). This is an explicit
+    // type cast.
     expr.type() = convert_type(expr.type());
     convert_expr(expr.op());
   }

src/verilog/verilog_typecheck_expr.h

@@ -130,7 +130,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_extractbit_expr(extractbit_exprt);
   [[nodiscard]] exprt convert_replication_expr(replication_exprt);
   [[nodiscard]] exprt convert_shl_expr(shl_exprt);
-  void typecast(exprt &, const typet &type);
+  void implicit_typecast(exprt &, const typet &type);
   void tc_binary_expr(exprt &);
   void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
   void no_bool_ops(exprt &);

src/verilog/verilog_typecheck_type.cpp

@@ -105,11 +105,14 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
   }
   else if(src.id() == ID_verilog_enum)
   {
-    // Replace by base type.
+    // Replace by base type, but annotate the original type.
     // The default base type is 'int'.
     auto &enum_type = to_verilog_enum_type(src);
-    auto result =
-      enum_type.has_base_type() ? enum_type.base_type() : signedbv_typet(32);
+    auto result = enum_type.has_base_type()
+                    ? convert_type(enum_type.base_type())
+                    : signedbv_typet(32);
+    result.set(ID_C_verilog_type, ID_verilog_enum);
+    result.set(ID_C_identifier, enum_type.identifier());
     return result.with_source_location(source_location);
   }
   else if(src.id() == ID_array)
@@ -130,9 +133,10 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
         ? static_cast<const type_with_subtypet &>(src).subtype()
         : typet(ID_nil);
 
-    if(subtype.is_nil() ||
-       subtype.id()==ID_signed ||
-       subtype.id()==ID_unsigned)
+    if(
+      subtype.is_nil() || subtype.id() == ID_signed ||
+      subtype.id() == ID_unsigned || subtype.id() == ID_verilog_bit ||
+      subtype.id() == ID_verilog_logic)
     {
       // we have a bit-vector type, not an array