Merge pull request #1063 from diffblue/verilog-const

SystemVerilog: `const`

Author: kroening

regression/verilog/const/const2.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 const2.sv
 
-^EXIT=10$
+^file .* line 9: assignment to const$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Should be rejected owing to assignment to const variable.

src/hw_cbmc_irep_ids.h

@@ -94,6 +94,7 @@ IREP_ID_ONE(sva_implies)
 IREP_ID_ONE(sva_not)
 IREP_ID_ONE(sva_or)
 IREP_ID_ONE(module_instance)
+IREP_ID_TWO(C_const, #const)
 IREP_ID_TWO(C_offset, #offset)
 IREP_ID_TWO(C_increasing, #increasing)
 IREP_ID_ONE(ports)

src/verilog/parser.y

@@ -1381,20 +1381,24 @@ data_declaration:
 	  const_opt TOK_VAR lifetime_opt data_type_or_implicit list_of_variable_decl_assignments ';'
 	  	{ init($$, ID_decl);
 		  stack_expr($$).set(ID_class, ID_var);
-		  addswap($$, ID_type, $4);
+		  add_as_subtype(stack_type($1), stack_type($4));
+		  addswap($$, ID_type, $1);
 		  swapop($$, $5); }
 	| const_opt lifetime_opt data_type list_of_variable_decl_assignments ';'
 		{ init($$, ID_decl);
 		  stack_expr($$).set(ID_class, ID_reg);
-		  addswap($$, ID_type, $3);
+		  add_as_subtype(stack_type($1), stack_type($3));
+		  addswap($$, ID_type, $1);
 		  swapop($$, $4); }
 	| type_declaration
 	| package_import_declaration
 	;
 
 const_opt:
 	  /* Optional */
+		{ init($$, ID_nil); }
 	| TOK_CONST
+		{ init($$, ID_const); stack_type($$).add_subtype().make_nil(); }
 	;
 
 package_import_declaration_brace:

src/verilog/verilog_elaborate_type.cpp

@@ -468,6 +468,13 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     tmp.subtype() = elaborate_type(tmp.subtype());
     return std::move(tmp);
   }
+  else if(src.id() == ID_const)
+  {
+    auto tmp = to_type_with_subtype(src).subtype();
+    tmp = elaborate_type(tmp);
+    tmp.set(ID_C_const, true);
+    return tmp;
+  }
   else
   {
     throw errort().with_location(source_location)

src/verilog/verilog_typecheck.cpp

@@ -728,6 +728,13 @@ void verilog_typecheckt::check_lhs(
   {
     const symbolt &symbol=ns.lookup(to_symbol_expr(lhs));
 
+    // check for 'const'
+    if(symbol.type.get_bool(ID_C_const))
+    {
+      throw errort().with_location(lhs.source_location())
+        << "assignment to const";
+    }
+
     switch(vassign)
     {
     case A_CONTINUOUS:

src/verilog/verilog_typecheck_expr.h

@@ -66,7 +66,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 
   void propagate_type(exprt &expr, const typet &type);
 
-  typet elaborate_type(const typet &);
+  [[nodiscard]] typet elaborate_type(const typet &);
   typet elaborate_package_scope_typedef(const verilog_package_scope_typet &);
   typet convert_enum(const class verilog_enum_typet &);
   array_typet convert_unpacked_array_type(const type_with_subtypet &);