Verilog system tasks and functions are always base names

kroening · kroening · commit 3281369f8175 · 2025-12-03T08:32:45.000-08:00
Verilog system tasks and functions are never qualified or decorated, hence
use verilog_identifier_exprt for their name.
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -3718,7 +3718,7 @@ function_statement: statement
 	;
 
 system_task_name: TOK_SYSIDENT
-                { new_symbol($$, $1); }
+                { new_symbol($$, $1); stack_expr($$).id(ID_verilog_identifier); }
         ;
 
 // System Verilog standard 1800-2017
diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
@@ -52,8 +52,9 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const
 
 static bool is_system_function_identifier(const exprt &function)
 {
-  return function.id() == ID_symbol &&
-         has_prefix(id2string(to_symbol_expr(function).get_identifier()), "$");
+  return function.id() == ID_verilog_identifier &&
+         has_prefix(
+           id2string(to_verilog_identifier_expr(function).base_name()), "$");
 }
 
 bool function_call_exprt::is_system_function_call() const
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
@@ -632,12 +632,12 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(
   }
     
   // built-in functions
-  symbol_exprt &f_op=to_symbol_expr(expr.function());
-  
-  const irep_idt &identifier=f_op.get_identifier();
-  
   if(expr.is_system_function_call())
-    return convert_system_function(identifier, expr);
+    return convert_system_function(expr);
+
+  symbol_exprt &f_op=to_symbol_expr(expr.function());
+
+  const irep_idt &identifier = f_op.get_identifier();
 
   std::string full_identifier=
     id2string(module_identifier)+"."+id2string(identifier);
@@ -901,13 +901,13 @@ Function: verilog_typecheck_exprt::convert_system_function
 
 \*******************************************************************/
 
-exprt verilog_typecheck_exprt::convert_system_function(
-  const irep_idt &identifier,
-  function_call_exprt expr)
+exprt verilog_typecheck_exprt::convert_system_function(function_call_exprt expr)
 {
+  auto base_name = to_verilog_identifier_expr(expr.function()).base_name();
+
   exprt::operandst &arguments=expr.arguments();
 
-  if(identifier=="$signed")
+  if(base_name == "$signed")
   {
     // this is an explicit type cast
     if(arguments.size()!=1)
@@ -942,7 +942,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
         << to_string(argument.type()) << '\'';
     }
   }
-  else if(identifier=="$unsigned")
+  else if(base_name == "$unsigned")
   {
     // this is an explicit type cast
     if(arguments.size()!=1)
@@ -977,7 +977,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
         << to_string(argument.type()) << '\'';
     }
   }
-  else if(identifier=="$ND")
+  else if(base_name == "$ND")
   {
     // this is something from VIS
     
@@ -991,21 +991,21 @@ exprt verilog_typecheck_exprt::convert_system_function(
     return std::move(expr);
   }
   else if(
-    identifier == "$bits" || identifier == "$left" || identifier == "$right" ||
-    identifier == "$increment" || identifier == "$low" || identifier == "$high")
+    base_name == "$bits" || base_name == "$left" || base_name == "$right" ||
+    base_name == "$increment" || base_name == "$low" || base_name == "$high")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     // The return type is integer.
     expr.type() = integer_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$countones") // SystemVerilog
+  else if(base_name == "$countones") // SystemVerilog
   {
     if(arguments.size() != 1)
     {
@@ -1018,7 +1018,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
-  else if(identifier=="$onehot") // SystemVerilog
+  else if(base_name == "$onehot") // SystemVerilog
   {
     if(arguments.size()!=1)
     {
@@ -1032,7 +1032,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(onehot);
   }
-  else if(identifier=="$onehot0") // SystemVerilog
+  else if(base_name == "$onehot0") // SystemVerilog
   {
     if(arguments.size()!=1)
     {
@@ -1046,7 +1046,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(onehot0);
   }
-  else if(identifier == "$clog2") // Verilog-2005
+  else if(base_name == "$clog2") // Verilog-2005
   {
     if(arguments.size() != 1)
     {
@@ -1058,7 +1058,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
-  else if(identifier == "$isunknown")
+  else if(base_name == "$isunknown")
   {
     if(arguments.size() != 1)
     {
@@ -1070,7 +1070,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
-  else if(identifier == "$past")
+  else if(base_name == "$past")
   {
     if(arguments.size() == 0 || arguments.size() >= 4)
     {
@@ -1089,73 +1089,73 @@ exprt verilog_typecheck_exprt::convert_system_function(
     return std::move(expr);
   }
   else if(
-    identifier == "$stable" || identifier == "$rose" || identifier == "$fell" ||
-    identifier == "$changed")
+    base_name == "$stable" || base_name == "$rose" || base_name == "$fell" ||
+    base_name == "$changed")
   {
     if(arguments.size() != 1 && arguments.size() != 2)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one or two arguments";
+        << base_name << " takes one or two arguments";
     }
 
     expr.type() = bool_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$rtoi")
+  else if(base_name == "$rtoi")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     expr.type() = verilog_integer_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$itor")
+  else if(base_name == "$itor")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     expr.type() = verilog_real_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$bitstoreal")
+  else if(base_name == "$bitstoreal")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     expr.type() = verilog_real_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$bitstoshortreal")
+  else if(base_name == "$bitstoshortreal")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     expr.type() = verilog_shortreal_typet();
 
     return std::move(expr);
   }
-  else if(identifier == "$realtobits")
+  else if(base_name == "$realtobits")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     arguments[0] =
@@ -1165,12 +1165,12 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
-  else if(identifier == "$shortrealtobits")
+  else if(base_name == "$shortrealtobits")
   {
     if(arguments.size() != 1)
     {
       throw errort().with_location(expr.source_location())
-        << identifier << " takes one argument";
+        << base_name << " takes one argument";
     }
 
     arguments[0] =
@@ -1180,7 +1180,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
 
     return std::move(expr);
   }
-  else if(identifier == "$typename")
+  else if(base_name == "$typename")
   {
     if(arguments.size() != 1)
     {
@@ -1198,7 +1198,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
   else
   {
     throw errort().with_location(expr.function().source_location())
-      << "unknown system function `" << identifier << "'";
+      << "unknown system function `" << base_name << "'";
   }
 }
 
diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h
@@ -185,8 +185,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_trinary_expr(ternary_exprt);
   [[nodiscard]] exprt convert_expr_concatenation(concatenation_exprt);
   [[nodiscard]] exprt convert_expr_function_call(function_call_exprt);
-  [[nodiscard]] exprt
-  convert_system_function(const irep_idt &identifier, function_call_exprt);
+  [[nodiscard]] exprt convert_system_function(function_call_exprt);
   [[nodiscard]] exprt convert_bit_select_expr(binary_exprt);
   [[nodiscard]] exprt convert_replication_expr(replication_exprt);
   [[nodiscard]] exprt convert_power_expr(power_exprt);

Original file line number	Diff line number	Diff line change
`@@ -3718,7 +3718,7 @@ function_statement: statement`
`3718`	`3718`	`;`
`3719`	`3719`
`3720`	`3720`	`system_task_name: TOK_SYSIDENT`
`3721`		`- { new_symbol($$, $1); }`
	`3721`	`+ { new_symbol($$, $1); stack_expr($$).id(ID_verilog_identifier); }`
`3722`	`3722`	`;`
`3723`	`3723`
`3724`	`3724`	`// System Verilog standard 1800-2017`
Original file line number	Diff line number	Diff line change
`@@ -52,8 +52,9 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const`
`52`	`52`
`53`	`53`	`static bool is_system_function_identifier(const exprt &function)`
`54`	`54`	`{`
`55`		`- return function.id() == ID_symbol &&`
`56`		`- has_prefix(id2string(to_symbol_expr(function).get_identifier()), "$");`
	`55`	`+ return function.id() == ID_verilog_identifier &&`
	`56`	`+ has_prefix(`
	`57`	`+ id2string(to_verilog_identifier_expr(function).base_name()), "$");`
`57`	`58`	`}`
`58`	`59`
`59`	`60`	`bool function_call_exprt::is_system_function_call() const`
Original file line number	Diff line number	Diff line change
`@@ -632,12 +632,12 @@ exprt verilog_typecheck_exprt::convert_expr_function_call(`
`632`	`632`	`}`
`633`	`633`
`634`	`634`	`// built-in functions`
`635`		`- symbol_exprt &f_op=to_symbol_expr(expr.function());`
`636`		`-`
`637`		`- const irep_idt &identifier=f_op.get_identifier();`
`638`		`-`
`639`	`635`	`if(expr.is_system_function_call())`
`640`		`- return convert_system_function(identifier, expr);`
	`636`	`+ return convert_system_function(expr);`
	`637`	`+`
	`638`	`+ symbol_exprt &f_op=to_symbol_expr(expr.function());`
	`639`	`+`
	`640`	`+ const irep_idt &identifier = f_op.get_identifier();`
`641`	`641`
`642`	`642`	`std::string full_identifier=`
`643`	`643`	`id2string(module_identifier)+"."+id2string(identifier);`
`@@ -901,13 +901,13 @@ Function: verilog_typecheck_exprt::convert_system_function`
`901`	`901`
`902`	`902`	`\*******************************************************************/`
`903`	`903`
`904`		`-exprt verilog_typecheck_exprt::convert_system_function(`
`905`		`- const irep_idt &identifier,`
`906`		`- function_call_exprt expr)`
	`904`	`+exprt verilog_typecheck_exprt::convert_system_function(function_call_exprt expr)`
`907`	`905`	`{`
	`906`	`+ auto base_name = to_verilog_identifier_expr(expr.function()).base_name();`
	`907`	`+`
`908`	`908`	`exprt::operandst &arguments=expr.arguments();`
`909`	`909`
`910`		`- if(identifier=="$signed")`
	`910`	`+ if(base_name == "$signed")`
`911`	`911`	`{`
`912`	`912`	`// this is an explicit type cast`
`913`	`913`	`if(arguments.size()!=1)`
`@@ -942,7 +942,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`942`	`942`	`<< to_string(argument.type()) << '\'';`
`943`	`943`	`}`
`944`	`944`	`}`
`945`		`- else if(identifier=="$unsigned")`
	`945`	`+ else if(base_name == "$unsigned")`
`946`	`946`	`{`
`947`	`947`	`// this is an explicit type cast`
`948`	`948`	`if(arguments.size()!=1)`
`@@ -977,7 +977,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`977`	`977`	`<< to_string(argument.type()) << '\'';`
`978`	`978`	`}`
`979`	`979`	`}`
`980`		`- else if(identifier=="$ND")`
	`980`	`+ else if(base_name == "$ND")`
`981`	`981`	`{`
`982`	`982`	`// this is something from VIS`
`983`	`983`
`@@ -991,21 +991,21 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`991`	`991`	`return std::move(expr);`
`992`	`992`	`}`
`993`	`993`	`else if(`
`994`		`- identifier == "$bits" \|\| identifier == "$left" \|\| identifier == "$right" \|\|`
`995`		`- identifier == "$increment" \|\| identifier == "$low" \|\| identifier == "$high")`
	`994`	`+ base_name == "$bits" \|\| base_name == "$left" \|\| base_name == "$right" \|\|`
	`995`	`+ base_name == "$increment" \|\| base_name == "$low" \|\| base_name == "$high")`
`996`	`996`	`{`
`997`	`997`	`if(arguments.size() != 1)`
`998`	`998`	`{`
`999`	`999`	`throw errort().with_location(expr.source_location())`
`1000`		`- << identifier << " takes one argument";`
	`1000`	`+ << base_name << " takes one argument";`
`1001`	`1001`	`}`
`1002`	`1002`
`1003`	`1003`	`// The return type is integer.`
`1004`	`1004`	`expr.type() = integer_typet();`
`1005`	`1005`
`1006`	`1006`	`return std::move(expr);`
`1007`	`1007`	`}`
`1008`		`- else if(identifier == "$countones") // SystemVerilog`
	`1008`	`+ else if(base_name == "$countones") // SystemVerilog`
`1009`	`1009`	`{`
`1010`	`1010`	`if(arguments.size() != 1)`
`1011`	`1011`	`{`
`@@ -1018,7 +1018,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1018`	`1018`
`1019`	`1019`	`return std::move(expr);`
`1020`	`1020`	`}`
`1021`		`- else if(identifier=="$onehot") // SystemVerilog`
	`1021`	`+ else if(base_name == "$onehot") // SystemVerilog`
`1022`	`1022`	`{`
`1023`	`1023`	`if(arguments.size()!=1)`
`1024`	`1024`	`{`
`@@ -1032,7 +1032,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1032`	`1032`
`1033`	`1033`	`return std::move(onehot);`
`1034`	`1034`	`}`
`1035`		`- else if(identifier=="$onehot0") // SystemVerilog`
	`1035`	`+ else if(base_name == "$onehot0") // SystemVerilog`
`1036`	`1036`	`{`
`1037`	`1037`	`if(arguments.size()!=1)`
`1038`	`1038`	`{`
`@@ -1046,7 +1046,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1046`	`1046`
`1047`	`1047`	`return std::move(onehot0);`
`1048`	`1048`	`}`
`1049`		`- else if(identifier == "$clog2") // Verilog-2005`
	`1049`	`+ else if(base_name == "$clog2") // Verilog-2005`
`1050`	`1050`	`{`
`1051`	`1051`	`if(arguments.size() != 1)`
`1052`	`1052`	`{`
`@@ -1058,7 +1058,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1058`	`1058`
`1059`	`1059`	`return std::move(expr);`
`1060`	`1060`	`}`
`1061`		`- else if(identifier == "$isunknown")`
	`1061`	`+ else if(base_name == "$isunknown")`
`1062`	`1062`	`{`
`1063`	`1063`	`if(arguments.size() != 1)`
`1064`	`1064`	`{`
`@@ -1070,7 +1070,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1070`	`1070`
`1071`	`1071`	`return std::move(expr);`
`1072`	`1072`	`}`
`1073`		`- else if(identifier == "$past")`
	`1073`	`+ else if(base_name == "$past")`
`1074`	`1074`	`{`
`1075`	`1075`	`if(arguments.size() == 0 \|\| arguments.size() >= 4)`
`1076`	`1076`	`{`
`@@ -1089,73 +1089,73 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1089`	`1089`	`return std::move(expr);`
`1090`	`1090`	`}`
`1091`	`1091`	`else if(`
`1092`		`- identifier == "$stable" \|\| identifier == "$rose" \|\| identifier == "$fell" \|\|`
`1093`		`- identifier == "$changed")`
	`1092`	`+ base_name == "$stable" \|\| base_name == "$rose" \|\| base_name == "$fell" \|\|`
	`1093`	`+ base_name == "$changed")`
`1094`	`1094`	`{`
`1095`	`1095`	`if(arguments.size() != 1 && arguments.size() != 2)`
`1096`	`1096`	`{`
`1097`	`1097`	`throw errort().with_location(expr.source_location())`
`1098`		`- << identifier << " takes one or two arguments";`
	`1098`	`+ << base_name << " takes one or two arguments";`
`1099`	`1099`	`}`
`1100`	`1100`
`1101`	`1101`	`expr.type() = bool_typet();`
`1102`	`1102`
`1103`	`1103`	`return std::move(expr);`
`1104`	`1104`	`}`
`1105`		`- else if(identifier == "$rtoi")`
	`1105`	`+ else if(base_name == "$rtoi")`
`1106`	`1106`	`{`
`1107`	`1107`	`if(arguments.size() != 1)`
`1108`	`1108`	`{`
`1109`	`1109`	`throw errort().with_location(expr.source_location())`
`1110`		`- << identifier << " takes one argument";`
	`1110`	`+ << base_name << " takes one argument";`
`1111`	`1111`	`}`
`1112`	`1112`
`1113`	`1113`	`expr.type() = verilog_integer_typet();`
`1114`	`1114`
`1115`	`1115`	`return std::move(expr);`
`1116`	`1116`	`}`
`1117`		`- else if(identifier == "$itor")`
	`1117`	`+ else if(base_name == "$itor")`
`1118`	`1118`	`{`
`1119`	`1119`	`if(arguments.size() != 1)`
`1120`	`1120`	`{`
`1121`	`1121`	`throw errort().with_location(expr.source_location())`
`1122`		`- << identifier << " takes one argument";`
	`1122`	`+ << base_name << " takes one argument";`
`1123`	`1123`	`}`
`1124`	`1124`
`1125`	`1125`	`expr.type() = verilog_real_typet();`
`1126`	`1126`
`1127`	`1127`	`return std::move(expr);`
`1128`	`1128`	`}`
`1129`		`- else if(identifier == "$bitstoreal")`
	`1129`	`+ else if(base_name == "$bitstoreal")`
`1130`	`1130`	`{`
`1131`	`1131`	`if(arguments.size() != 1)`
`1132`	`1132`	`{`
`1133`	`1133`	`throw errort().with_location(expr.source_location())`
`1134`		`- << identifier << " takes one argument";`
	`1134`	`+ << base_name << " takes one argument";`
`1135`	`1135`	`}`
`1136`	`1136`
`1137`	`1137`	`expr.type() = verilog_real_typet();`
`1138`	`1138`
`1139`	`1139`	`return std::move(expr);`
`1140`	`1140`	`}`
`1141`		`- else if(identifier == "$bitstoshortreal")`
	`1141`	`+ else if(base_name == "$bitstoshortreal")`
`1142`	`1142`	`{`
`1143`	`1143`	`if(arguments.size() != 1)`
`1144`	`1144`	`{`
`1145`	`1145`	`throw errort().with_location(expr.source_location())`
`1146`		`- << identifier << " takes one argument";`
	`1146`	`+ << base_name << " takes one argument";`
`1147`	`1147`	`}`
`1148`	`1148`
`1149`	`1149`	`expr.type() = verilog_shortreal_typet();`
`1150`	`1150`
`1151`	`1151`	`return std::move(expr);`
`1152`	`1152`	`}`
`1153`		`- else if(identifier == "$realtobits")`
	`1153`	`+ else if(base_name == "$realtobits")`
`1154`	`1154`	`{`
`1155`	`1155`	`if(arguments.size() != 1)`
`1156`	`1156`	`{`
`1157`	`1157`	`throw errort().with_location(expr.source_location())`
`1158`		`- << identifier << " takes one argument";`
	`1158`	`+ << base_name << " takes one argument";`
`1159`	`1159`	`}`
`1160`	`1160`
`1161`	`1161`	`arguments[0] =`
`@@ -1165,12 +1165,12 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1165`	`1165`
`1166`	`1166`	`return std::move(expr);`
`1167`	`1167`	`}`
`1168`		`- else if(identifier == "$shortrealtobits")`
	`1168`	`+ else if(base_name == "$shortrealtobits")`
`1169`	`1169`	`{`
`1170`	`1170`	`if(arguments.size() != 1)`
`1171`	`1171`	`{`
`1172`	`1172`	`throw errort().with_location(expr.source_location())`
`1173`		`- << identifier << " takes one argument";`
	`1173`	`+ << base_name << " takes one argument";`
`1174`	`1174`	`}`
`1175`	`1175`
`1176`	`1176`	`arguments[0] =`
`@@ -1180,7 +1180,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1180`	`1180`
`1181`	`1181`	`return std::move(expr);`
`1182`	`1182`	`}`
`1183`		`- else if(identifier == "$typename")`
	`1183`	`+ else if(base_name == "$typename")`
`1184`	`1184`	`{`
`1185`	`1185`	`if(arguments.size() != 1)`
`1186`	`1186`	`{`
`@@ -1198,7 +1198,7 @@ exprt verilog_typecheck_exprt::convert_system_function(`
`1198`	`1198`	`else`
`1199`	`1199`	`{`
`1200`	`1200`	`throw errort().with_location(expr.function().source_location())`
`1201`		- << "unknown system function `" << identifier << "'";
	`1201`	+ << "unknown system function `" << base_name << "'";
`1202`	`1202`	`}`
`1203`	`1203`	`}`
`1204`	`1204`