Verilog: enum constants may depend on elaboration-time constants

This postpones the conversion of enum base types and enum initializers to
enable them to depend on other elaboration-time constants.

Author: kroening

Diff for: regression/verilog/enums/enum1.desc

@@ -3,5 +3,5 @@ enum1.sv
 --bound 3
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.property\.p1\] always main\.my_light != 0 \+ 1 \+ 1 \+ 1: REFUTED$
+^\[main\.property\.p1\] always main\.my_light != 3: REFUTED$
 --

Diff for: regression/verilog/enums/enum2.desc

@@ -1,7 +1,7 @@
 CORE
 enum2.sv
 
-^file .* line 4: assignment to enum requires enum of the same type$
+^file .* line 4: assignment to enum requires enum of the same type, but got signed \[0:31\]$
 ^EXIT=2$
 ^SIGNAL=0$
 --

Diff for: regression/verilog/enums/enum_base_type2.desc

@@ -1,9 +1,7 @@
-KNOWNBUG
+CORE
 enum_base_type2.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*\] always 8 == 8: PROVED up to bound 0$
 --
---
-The base type of an enum may depend on an elaboration-time constant.

Diff for: regression/verilog/enums/enum_initializers1.desc

@@ -2,7 +2,7 @@ CORE
 enum_initializers1.sv
 --bound 0
 ^\[main\.property\.pA\] always 1 == 1: PROVED up to bound 0$
-^\[main\.property\.pB\] always 1 \+ 10 == 11: PROVED up to bound 0$
+^\[main\.property\.pB\] always 11 == 11: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

Diff for: regression/verilog/enums/enum_initializers2.desc

@@ -1,9 +1,6 @@
-KNOWNBUG
+CORE
 enum_initializers2.sv
 
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
 --
---
-Crashes with missing identifier
-

Diff for: regression/verilog/enums/enum_initializers2.sv

@@ -2,11 +2,11 @@ module main;
 
   parameter B = A + 1;
 
-  enum { A = 1, C = my_parameter + 1 } my_enum;
+  enum { A = 1, C = B + 1 } my_enum;
 
   // expected to pass
   pA: assert property (A == 1);
   pB: assert property (B == 2);
-  pC: assert property (B == 3);
+  pC: assert property (C == 3);
 
 endmodule

Diff for: regression/verilog/enums/enum_initializers3.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 enum_initializers3.sv
 
-^EXIT=10$
+^file .* line 4: cyclic dependency when elaborating main\.B$
+^EXIT=2$
 ^SIGNAL=0$
 --
---
-Cycle not detected.

Diff for: src/verilog/verilog_elaborate.cpp

@@ -102,37 +102,37 @@ void verilog_typecheckt::collect_symbols(const typet &type)
     if(enum_type.has_base_type())
       collect_symbols(enum_type.base_type());
 
-    // convert the type now
-    auto converted_type = convert_type(enum_type);
+    // The type needs to be converted later, as it may
+    // depend on other elaboration-time constants.
+    auto tbd_type = to_be_elaborated_typet(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'.
     exprt initializer = from_integer(0, integer_typet());
 
     for(auto &enum_name : enum_type.enum_names())
     {
+      // The initializer will also be converted later.
       if(enum_name.value().is_not_nil())
-      {
-        exprt tmp = enum_name.value();
-        convert_expr(tmp);
-        initializer = std::move(tmp);
-      }
+        initializer = enum_name.value();
 
-      exprt value = typecast_exprt(initializer, converted_type);
+      exprt value = typecast_exprt(initializer, tbd_type);
+      value.add_source_location() = enum_name.source_location();
 
       const auto base_name = enum_name.base_name();
       const auto identifier = hierarchical_identifier(base_name);
-      symbolt enum_name_symbol(identifier, converted_type, mode);
+      symbolt enum_name_symbol(identifier, tbd_type, mode);
       enum_name_symbol.module = module_identifier;
       enum_name_symbol.base_name = base_name;
       enum_name_symbol.value = std::move(value);
       enum_name_symbol.is_macro = true;
       enum_name_symbol.is_file_local = true;
+      enum_name_symbol.location = enum_name.source_location();
       add_symbol(std::move(enum_name_symbol));
 
       initializer = plus_exprt(
-        typecast_exprt(initializer, converted_type),
-        typecast_exprt(from_integer(1, integer_typet()), converted_type));
+        typecast_exprt(initializer, tbd_type),
+        typecast_exprt(from_integer(1, integer_typet()), tbd_type));
     }
   }
 }
@@ -831,8 +831,10 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
       // Now elaborate the value, possibly recursively, if any.
       if(symbol.value.is_not_nil())
       {
+        auto location = symbol.value.source_location();
         convert_expr(symbol.value);
         symbol.value = elaborate_constant_expression(symbol.value);
+        symbol.value.add_source_location() = location;
 
         // Cast to the given type.
         propagate_type(symbol.value, symbol.type);

Diff for: src/verilog/verilog_typecheck_expr.cpp

@@ -105,7 +105,8 @@ void verilog_typecheck_exprt::propagate_type(
       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";
+        << "assignment to enum requires enum of the same type, but got "
+        << to_string(expr.type());
     }
   }
 
@@ -1319,6 +1320,10 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
   }
   else
   {
+    // Remember the Verilog type.
+    auto expr_verilog_type = expr.type().get(ID_C_verilog_type);
+    auto expr_identifier = expr.type().get(ID_C_identifier);
+
     // Do any operands first.
     bool operands_are_constant = true;
 
@@ -1344,7 +1349,16 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
 
     // We fall back to the simplifier to approximate
     // the standard's definition of 'constant expression'.
-    return simplify_expr(expr, ns);
+    auto simplified_expr = simplify_expr(expr, ns);
+
+    // Restore the Verilog type, if any.
+    if(expr_verilog_type != irep_idt())
+      simplified_expr.type().set(ID_C_verilog_type, expr_verilog_type);
+
+    if(expr_identifier != irep_idt())
+      simplified_expr.type().set(ID_C_identifier, expr_identifier);
+
+    return simplified_expr;
   }
 }
 
@@ -1479,7 +1493,8 @@ void verilog_typecheck_exprt::implicit_typecast(
       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";
+        << "assignment to enum requires enum of the same type, but got "
+        << to_string(expr.type());
     }
   }
 

Diff for: src/verilog/verilog_typecheck_type.cpp

@@ -175,6 +175,11 @@ typet verilog_typecheck_exprt::convert_type(const typet &src)
     else
       return convert_type(type_reference.type_op());
   }
+  else if(src.id() == ID_to_be_elaborated)
+  {
+    // recursive call
+    return convert_type(to_to_be_elaborated_type(src).subtype());
+  }
   else
   {
     error().source_location = source_location;

Diff for: src/verilog/verilog_types.h

@@ -22,6 +22,31 @@ class to_be_elaborated_typet : public type_with_subtypet
   }
 };
 
+/*! \brief Cast a generic typet to a \ref to_be_elaborated_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * to_be_elaborated_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref to_be_elaborated_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const to_be_elaborated_typet &to_to_be_elaborated_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_to_be_elaborated);
+  return static_cast<const to_be_elaborated_typet &>(type);
+}
+
+/*! \copydoc to_to_be_elaborated_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline to_be_elaborated_typet &to_to_be_elaborated_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_to_be_elaborated);
+  return static_cast<to_be_elaborated_typet &>(type);
+}
+
 /// Used during elaboration only,
 /// to signal that the type of the symbol is going to be the
 /// type of the value (default for parameters).
@@ -336,6 +361,11 @@ class verilog_enum_typet : public type_with_subtypet
     {
       set(ID_base_name, _base_name);
     }
+
+    const source_locationt &source_location() const
+    {
+      return static_cast<const source_locationt &>(find(ID_C_source_location));
+    }
   };
 
   using enum_namest = std::vector<enum_namet>;