Verilog: reject non-constant parameters

Module parameters, local parameters and enums must be elaboration time
constants.  This adds an error when they are not.

Author: kroening

regression/verilog/enums/enum5.desc

@@ -0,0 +1,7 @@
+CORE
+enum5.sv
+--bound 0
+^file .* line 6: expected constant expression, but got `main\.some_wire'$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/verilog/enums/enum5.sv

@@ -0,0 +1,8 @@
+module main;
+
+  wire some_wire;
+
+  // some_wire is not a constant
+  typedef enum bit [7:0] { A = some_wire } enum_t;
+
+endmodule

src/verilog/verilog_elaborate.cpp

@@ -614,6 +614,8 @@ void verilog_typecheckt::collect_symbols(const verilog_lett &let)
   new_symbol.base_name = base_name;
   new_symbol.pretty_name = strip_verilog_prefix(new_symbol.name);
 
+  let_symbols.insert(new_symbol.name);
+
   add_symbol(std::move(new_symbol));
 }
 
@@ -929,12 +931,17 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
     // mark as "elaborating" to detect cycles
     symbol.type.id(ID_elaborating);
 
+    bool is_let = let_symbols.find(symbol.name) != let_symbols.end();
+
     // Is the type derived from the value (e.g., parameters)?
     if(to_type_with_subtype(symbol.type).subtype().id() == ID_derive_from_value)
     {
       // First elaborate the value, possibly recursively.
       convert_expr(symbol.value);
-      symbol.value = elaborate_constant_expression(symbol.value);
+
+      if(!is_let)
+        symbol.value = elaborate_constant_expression_check(symbol.value);
+
       symbol.type = symbol.value.type();
     }
     else
@@ -948,7 +955,9 @@ void verilog_typecheckt::elaborate_symbol_rec(irep_idt identifier)
       if(symbol.value.is_not_nil())
       {
         convert_expr(symbol.value);
-        symbol.value = elaborate_constant_expression(symbol.value);
+
+        if(!is_let)
+          symbol.value = elaborate_constant_expression_check(symbol.value);
 
         // Cast to the given type.
         propagate_type(symbol.value, symbol.type);

src/verilog/verilog_typecheck.h

@@ -97,6 +97,7 @@ class verilog_typecheckt:
   collect_symbols(const typet &, const verilog_parameter_declt::declaratort &);
   void collect_port_symbols(const verilog_declt &);
   std::vector<irep_idt> symbols_added;
+  std::set<irep_idt> let_symbols;
 
   // instances
   irep_idt parameterize_module(

src/verilog/verilog_typecheck_expr.cpp

@@ -844,13 +844,8 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     if(arguments.size() >= 2)
     {
-      auto tmp = elaborate_constant_expression(arguments[1]);
-      if(!tmp.is_constant())
-      {
-        throw errort().with_location(arguments[1].source_location())
-          << "expected elaboration-time constant, but got `" << to_string(tmp)
-          << '\'';
-      }
+      auto tmp = elaborate_constant_expression_check(arguments[1]);
+      arguments[1] = tmp;
     }
 
     expr.type() = arguments.front().type();
@@ -1454,12 +1449,12 @@ verilog_typecheck_exprt::convert_integer_constant_expression(exprt expr)
   // this could be large
   propagate_type(expr, integer_typet());
 
-  exprt tmp = elaborate_constant_expression(expr);
+  exprt tmp = elaborate_constant_expression_check(expr);
 
-  if(!tmp.is_constant())
+  if(tmp.id() == ID_infinity)
   {
     throw errort().with_location(source_location)
-      << "expected constant expression, but got `" << to_string(tmp) << '\'';
+      << "expected integer constant, but got $";
   }
 
   const auto &tmp_constant = to_constant_expr(tmp);
@@ -1515,6 +1510,9 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
 
     if(symbol.is_macro)
     {
+      // Elaborate recursively
+      elaborate_symbol_rec(symbol.name);
+
       // A parameter or local parameter. Replace by its value.
       return symbol.value;
     }
@@ -1524,12 +1522,12 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
     #if 0
     status() << "READ " << identifier << " = " << to_string(value) << eom;
     #endif
-      
+
     if(value.is_not_nil())
     {
-      source_locationt source_location=expr.source_location();
-      exprt tmp=value;
-      tmp.add_source_location()=source_location;
+      source_locationt source_location = expr.source_location();
+      exprt tmp = value;
+      tmp.add_source_location() = source_location;
       return tmp;
     }
     else
@@ -1671,6 +1669,34 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::elaborate_constant_expression_check
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt verilog_typecheck_exprt::elaborate_constant_expression_check(exprt expr)
+{
+  source_locationt source_location = expr.find_source_location();
+
+  exprt tmp = elaborate_constant_expression(std::move(expr));
+
+  // $ counts as a constant
+  if(!tmp.is_constant() && tmp.id() != ID_infinity)
+  {
+    throw errort().with_location(source_location)
+      << "expected constant expression, but got `" << to_string(tmp) << '\'';
+  }
+
+  return tmp;
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::elaborate_constant_system_function_call
 
   Inputs:

src/verilog/verilog_typecheck_expr.h

@@ -148,6 +148,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   bool is_constant_expression(const exprt &, mp_integer &value);
   std::optional<mp_integer> is_constant_integer_post_convert(const exprt &);
   exprt elaborate_constant_expression(exprt);
+  exprt elaborate_constant_expression_check(exprt);
 
   // To be overridden, requires a Verilog interpreter.
   virtual exprt elaborate_constant_function_call(const function_call_exprt &)