Verilog: use verilog_identifier_exprt

kroening · kroening · commit 6f70c94ede14 · 2025-12-06T15:11:21.000-08:00
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -112,7 +112,7 @@ inline static void init(YYSTYPE &expr, const irep_idt &id)
 
 /*******************************************************************\
 
-Function: new_symbol
+Function: new_identifier
 
   Inputs:
 
@@ -123,9 +123,9 @@ Function: new_symbol
 
 \*******************************************************************/
 
-inline static void new_symbol(YYSTYPE &dest, YYSTYPE &src)
+inline static void new_identifier(YYSTYPE &dest, YYSTYPE &src)
 {
-  init(dest, ID_symbol);
+  init(dest, ID_verilog_identifier);
   const auto base_name = stack_expr(src).id();
   stack_expr(dest).set(ID_identifier, base_name);
   stack_expr(dest).set(ID_base_name, base_name);
@@ -3718,7 +3718,7 @@ function_statement: statement
 	;
 
 system_task_name: TOK_SYSIDENT
-                { new_symbol($$, $1); stack_expr($$).id(ID_verilog_identifier); }
+                { new_identifier($$, $1); }
         ;
 
 // System Verilog standard 1800-2017
@@ -4647,12 +4647,12 @@ attr_name: identifier
 // in a higher scope.
 any_identifier:
 	  TOK_TYPE_IDENTIFIER
-		{ new_symbol($$, $1); }
+		{ new_identifier($$, $1); }
 	| non_type_identifier
 	;
 
 non_type_identifier: TOK_NON_TYPE_IDENTIFIER
-		{ new_symbol($$, $1); }
+		{ new_identifier($$, $1); }
 	;
 
 block_identifier: TOK_NON_TYPE_IDENTIFIER;
@@ -4768,7 +4768,6 @@ hierarchical_identifier:
         | hierarchical_identifier '.' identifier
 		{ init($$, ID_hierarchical_identifier);
 		  stack_expr($$).reserve_operands(2);
-		  stack_expr($3).id(ID_verilog_identifier);
 		  mto($$, $1);
 		  mto($$, $3);
 		}
diff --git a/src/verilog/verilog_generate.cpp b/src/verilog/verilog_generate.cpp
@@ -170,13 +170,14 @@ void verilog_typecheckt::elaborate_generate_assign(
   const verilog_generate_assignt &statement,
   module_itemst &dest)
 {
-  if(statement.lhs().id() != ID_symbol)
+  if(statement.lhs().id() != ID_verilog_identifier)
   {
     throw errort().with_location(statement.lhs().source_location())
       << "expected symbol on left hand side of assignment";
   }
 
-  const irep_idt &identifier = to_symbol_expr(statement.lhs()).get_identifier();
+  const irep_idt &identifier =
+    to_verilog_identifier_expr(statement.lhs()).base_name();
 
   genvarst::iterator it=genvars.find(identifier);
   
diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp
@@ -60,11 +60,12 @@ void verilog_typecheckt::typecheck_port_connection(
   {
     // IEEE 1800 2017 6.10 allows implicit declarations of nets when
     // used in a port connection.
-    if(op.id() == ID_symbol)
+    if(op.id() == ID_verilog_identifier)
     {
       // The type of the implicit net is _not_ the type of the port,
       // but an "implicit scalar net of default net type".
-      op = convert_symbol(to_symbol_expr(op), bool_typet{});
+      op = convert_verilog_identifier(
+        to_verilog_identifier_expr(op), bool_typet{});
     }
     else
     {
@@ -134,15 +135,16 @@ void verilog_typecheckt::typecheck_port_connections(
 
       exprt &value = named_port_connection.value();
       const irep_idt &base_name =
-        to_symbol_expr(named_port_connection.port()).get_identifier();
+        to_verilog_identifier_expr(named_port_connection.port()).base_name();
 
       bool found=false;
 
       std::string full_identifier =
         id2string(symbol.module) + "." + id2string(base_name);
 
-      to_symbol_expr(named_port_connection.port())
-        .set_identifier(full_identifier);
+      named_port_connection.port() =
+        symbol_exprt{full_identifier, typet{}}.with_source_location(
+          named_port_connection.port());
 
       if(assigned_ports.find(base_name) != assigned_ports.end())
       {
@@ -232,11 +234,12 @@ void verilog_typecheckt::typecheck_builtin_port_connections(
   {
     // IEEE 1800 2017 6.10 allows implicit declarations of nets when
     // used in a port connection.
-    if(connection.id() == ID_symbol)
+    if(connection.id() == ID_verilog_identifier)
     {
       // The type of the implicit net is _not_ the type of the port,
       // but an "implicit scalar net of default net type".
-      connection = convert_symbol(to_symbol_expr(connection), bool_typet{});
+      connection = convert_verilog_identifier(
+        to_verilog_identifier_expr(connection), bool_typet{});
     }
     else
     {
@@ -844,8 +847,9 @@ void verilog_typecheckt::convert_continuous_assign(
     // from the RHS, and hence, we convert that first.
     convert_expr(rhs);
 
-    if(lhs.id() == ID_symbol)
-      lhs = convert_symbol(to_symbol_expr(lhs), rhs.type());
+    if(lhs.id() == ID_verilog_identifier)
+      lhs =
+        convert_verilog_identifier(to_verilog_identifier_expr(lhs), rhs.type());
     else
       convert_expr(lhs);
 
@@ -876,7 +880,8 @@ void verilog_typecheckt::convert_function_call_or_task_enable(
   }
   else
   {
-    irep_idt base_name = to_symbol_expr(statement.function()).get_identifier();
+    irep_idt base_name =
+      to_verilog_identifier_expr(statement.function()).base_name();
 
     // look it up
     const irep_idt full_identifier =
@@ -913,8 +918,8 @@ void verilog_typecheckt::convert_function_call_or_task_enable(
       assignment_conversion(arguments[i], parameter_types[i].type());
     }
 
-    statement.function().type() = symbol->type;
-    statement.function().set(ID_identifier, symbol->name);
+    statement.function() =
+      symbol->symbol_expr().with_source_location(statement.function());
   }
 }
 
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -629,24 +629,24 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
   if(expr.is_system_function_call())
     return convert_system_function(expr);
 
-  if(expr.function().id()!=ID_symbol)
+  if(expr.function().id() != ID_verilog_identifier)
   {
     throw errort().with_location(expr.source_location())
-      << "expected symbol as function argument";
+      << "expected identifier as function";
   }
 
-  symbol_exprt &f_op=to_symbol_expr(expr.function());
+  exprt &f_op = expr.function();
 
-  const irep_idt &identifier = f_op.get_identifier();
+  const irep_idt &base_name = to_verilog_identifier_expr(f_op).base_name();
 
-  std::string full_identifier=
-    id2string(module_identifier)+"."+id2string(identifier);
+  std::string full_identifier =
+    id2string(module_identifier) + "." + id2string(base_name);
 
   const symbolt *symbol;
   if(ns.lookup(full_identifier, symbol))
   {
     throw errort().with_location(f_op.source_location())
-      << "unknown function `" << identifier << "'";
+      << "unknown function `" << base_name << "'";
   }
 
   if(symbol->type.id()!=ID_code)
@@ -656,9 +656,8 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
   }
 
   const code_typet &code_type=to_code_type(symbol->type);
-  
-  f_op.type()=code_type;
-  f_op.set(ID_identifier, full_identifier);
+
+  f_op = symbol->symbol_expr().with_source_location(f_op);
   expr.type()=code_type.return_type();
   
   if(code_type.return_type().id()==ID_empty)
@@ -1220,9 +1219,10 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
   {
     return convert_constant(to_constant_expr(std::move(expr)));
   }
-  else if(expr.id()==ID_symbol)
+  else if(expr.id() == ID_verilog_identifier)
   {
-    return convert_symbol(to_symbol_expr(std::move(expr)), {});
+    return convert_verilog_identifier(
+      to_verilog_identifier_expr(std::move(expr)), {});
   }
   else if(expr.id()==ID_verilog_star_event)
   {
@@ -1270,9 +1270,10 @@ Function: verilog_typecheck_exprt::resolve
 
 \*******************************************************************/
 
-const symbolt *verilog_typecheck_exprt::resolve(const symbol_exprt &expr)
+const symbolt *
+verilog_typecheck_exprt::resolve(const verilog_identifier_exprt &expr)
 {
-  const irep_idt &base_name = expr.get_identifier();
+  const irep_idt &base_name = expr.base_name();
 
   // in a task or function? Try local ones first
   if(function_or_task_name!="")
@@ -1322,12 +1323,12 @@ Function: verilog_typecheck_exprt::convert_symbol
 
 \*******************************************************************/
 
-exprt verilog_typecheck_exprt::convert_symbol(
-  symbol_exprt expr,
+exprt verilog_typecheck_exprt::convert_verilog_identifier(
+  verilog_identifier_exprt expr,
   const std::optional<typet> &implicit_net_type)
 {
   auto symbol = resolve(expr);
-  auto base_name = expr.get_identifier();
+  auto base_name = expr.base_name();
 
   if(symbol != nullptr)
   { 
@@ -2959,12 +2960,13 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     auto location = expr.source_location();
     auto &package_scope = to_verilog_package_scope_expr(expr);
 
-    if(package_scope.identifier().id() != ID_symbol)
+    if(package_scope.identifier().id() != ID_verilog_identifier)
       throw errort().with_location(location)
-        << expr.id() << " expects symbol on the rhs";
+        << expr.id() << " expects verilog_identifier on the rhs";
 
     auto package_base = package_scope.package_base_name();
-    auto rhs_base = package_scope.identifier().get(ID_base_name);
+    auto rhs_base =
+      to_verilog_identifier_expr(package_scope.identifier()).base_name();
 
     // stitch together
     irep_idt full_identifier =
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
@@ -174,9 +174,10 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
 protected:
   [[nodiscard]] exprt convert_expr_rec(exprt expr);
   [[nodiscard]] exprt convert_constant(constant_exprt);
-  [[nodiscard]] const symbolt *resolve(const symbol_exprt &);
-  [[nodiscard]] exprt
-  convert_symbol(symbol_exprt, const std::optional<typet> &implicit_net_type);
+  [[nodiscard]] const symbolt *resolve(const verilog_identifier_exprt &);
+  [[nodiscard]] exprt convert_verilog_identifier(
+    verilog_identifier_exprt,
+    const std::optional<typet> &implicit_net_type);
   [[nodiscard]] exprt
     convert_hierarchical_identifier(class hierarchical_identifier_exprt);
   [[nodiscard]] exprt convert_nullary_expr(nullary_exprt);

Original file line number	Diff line number	Diff line change
`@@ -170,13 +170,14 @@ void verilog_typecheckt::elaborate_generate_assign(`
`170`	`170`	`const verilog_generate_assignt &statement,`
`171`	`171`	`module_itemst &dest)`
`172`	`172`	`{`
`173`		`- if(statement.lhs().id() != ID_symbol)`
	`173`	`+ if(statement.lhs().id() != ID_verilog_identifier)`
`174`	`174`	`{`
`175`	`175`	`throw errort().with_location(statement.lhs().source_location())`
`176`	`176`	`<< "expected symbol on left hand side of assignment";`
`177`	`177`	`}`
`178`	`178`
`179`		`- const irep_idt &identifier = to_symbol_expr(statement.lhs()).get_identifier();`
	`179`	`+ const irep_idt &identifier =`
	`180`	`+ to_verilog_identifier_expr(statement.lhs()).base_name();`
`180`	`181`
`181`	`182`	`genvarst::iterator it=genvars.find(identifier);`
`182`	`183`
Original file line number	Diff line number	Diff line change
`@@ -60,11 +60,12 @@ void verilog_typecheckt::typecheck_port_connection(`
`60`	`60`	`{`
`61`	`61`	`// IEEE 1800 2017 6.10 allows implicit declarations of nets when`
`62`	`62`	`// used in a port connection.`
`63`		`- if(op.id() == ID_symbol)`
	`63`	`+ if(op.id() == ID_verilog_identifier)`
`64`	`64`	`{`
`65`	`65`	`// The type of the implicit net is _not_ the type of the port,`
`66`	`66`	`// but an "implicit scalar net of default net type".`
`67`		`- op = convert_symbol(to_symbol_expr(op), bool_typet{});`
	`67`	`+ op = convert_verilog_identifier(`
	`68`	`+ to_verilog_identifier_expr(op), bool_typet{});`
`68`	`69`	`}`
`69`	`70`	`else`
`70`	`71`	`{`
`@@ -134,15 +135,16 @@ void verilog_typecheckt::typecheck_port_connections(`
`134`	`135`
`135`	`136`	`exprt &value = named_port_connection.value();`
`136`	`137`	`const irep_idt &base_name =`
`137`		`- to_symbol_expr(named_port_connection.port()).get_identifier();`
	`138`	`+ to_verilog_identifier_expr(named_port_connection.port()).base_name();`
`138`	`139`
`139`	`140`	`bool found=false;`
`140`	`141`
`141`	`142`	`std::string full_identifier =`
`142`	`143`	`id2string(symbol.module) + "." + id2string(base_name);`
`143`	`144`
`144`		`- to_symbol_expr(named_port_connection.port())`
`145`		`- .set_identifier(full_identifier);`
	`145`	`+ named_port_connection.port() =`
	`146`	`+ symbol_exprt{full_identifier, typet{}}.with_source_location(`
	`147`	`+ named_port_connection.port());`
`146`	`148`
`147`	`149`	`if(assigned_ports.find(base_name) != assigned_ports.end())`
`148`	`150`	`{`
`@@ -232,11 +234,12 @@ void verilog_typecheckt::typecheck_builtin_port_connections(`
`232`	`234`	`{`
`233`	`235`	`// IEEE 1800 2017 6.10 allows implicit declarations of nets when`
`234`	`236`	`// used in a port connection.`
`235`		`- if(connection.id() == ID_symbol)`
	`237`	`+ if(connection.id() == ID_verilog_identifier)`
`236`	`238`	`{`
`237`	`239`	`// The type of the implicit net is _not_ the type of the port,`
`238`	`240`	`// but an "implicit scalar net of default net type".`
`239`		`- connection = convert_symbol(to_symbol_expr(connection), bool_typet{});`
	`241`	`+ connection = convert_verilog_identifier(`
	`242`	`+ to_verilog_identifier_expr(connection), bool_typet{});`
`240`	`243`	`}`
`241`	`244`	`else`
`242`	`245`	`{`
`@@ -844,8 +847,9 @@ void verilog_typecheckt::convert_continuous_assign(`
`844`	`847`	`// from the RHS, and hence, we convert that first.`
`845`	`848`	`convert_expr(rhs);`
`846`	`849`
`847`		`- if(lhs.id() == ID_symbol)`
`848`		`- lhs = convert_symbol(to_symbol_expr(lhs), rhs.type());`
	`850`	`+ if(lhs.id() == ID_verilog_identifier)`
	`851`	`+ lhs =`
	`852`	`+ convert_verilog_identifier(to_verilog_identifier_expr(lhs), rhs.type());`
`849`	`853`	`else`
`850`	`854`	`convert_expr(lhs);`
`851`	`855`
`@@ -876,7 +880,8 @@ void verilog_typecheckt::convert_function_call_or_task_enable(`
`876`	`880`	`}`
`877`	`881`	`else`
`878`	`882`	`{`
`879`		`- irep_idt base_name = to_symbol_expr(statement.function()).get_identifier();`
	`883`	`+ irep_idt base_name =`
	`884`	`+ to_verilog_identifier_expr(statement.function()).base_name();`
`880`	`885`
`881`	`886`	`// look it up`
`882`	`887`	`const irep_idt full_identifier =`
`@@ -913,8 +918,8 @@ void verilog_typecheckt::convert_function_call_or_task_enable(`
`913`	`918`	`assignment_conversion(arguments[i], parameter_types[i].type());`
`914`	`919`	`}`
`915`	`920`
`916`		`- statement.function().type() = symbol->type;`
`917`		`- statement.function().set(ID_identifier, symbol->name);`
	`921`	`+ statement.function() =`
	`922`	`+ symbol->symbol_expr().with_source_location(statement.function());`
`918`	`923`	`}`
`919`	`924`	`}`
`920`	`925`