Verilog system tasks and functions are always base names

Verilog system tasks and functions are never qualified or decorated, hence
use verilog_identifier_exprt for their name.

Author: kroening

src/verilog/expr2verilog.cpp

@@ -1178,6 +1178,24 @@ expr2verilogt::resultt expr2verilogt::convert_symbol(const exprt &src)
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_verilog_identifier
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt
+expr2verilogt::convert_verilog_identifier(const verilog_identifier_exprt &src)
+{
+  return {verilog_precedencet::MAX, id2string(src.base_name())};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_nondet_symbol
 
   Inputs:
@@ -1809,6 +1827,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id()==ID_symbol)
     return convert_symbol(src);
 
+  else if(src.id() == ID_verilog_identifier)
+    return convert_symbol(to_verilog_identifier_expr(src));
+
   else if(src.id()==ID_nondet_symbol)
     return convert_nondet_symbol(src);
 

src/verilog/expr2verilog_class.h

@@ -19,6 +19,7 @@ class sva_cycle_delay_exprt;
 class sva_sequence_first_match_exprt;
 class sva_sequence_property_instance_exprt;
 class sva_sequence_repetition_exprt;
+class verilog_identifier_exprt;
 
 // Precedences (higher means binds more strongly).
 // Follows Table 11-2 in IEEE 1800-2017.
@@ -98,6 +99,8 @@ class expr2verilogt
 
   resultt convert_symbol(const exprt &);
 
+  resultt convert_verilog_identifier(const verilog_identifier_exprt &);
+
   resultt
   convert_hierarchical_identifier(const class hierarchical_identifier_exprt &);
 

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

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

src/verilog/verilog_lowering.cpp

@@ -176,68 +176,68 @@ exprt to_bitvector(const exprt &src)
 
 exprt verilog_lowering_system_function(const function_call_exprt &call)
 {
-  auto identifier = to_symbol_expr(call.function()).get_identifier();
+  auto base_name = to_verilog_identifier_expr(call.function()).base_name();
   auto &arguments = call.arguments();
 
-  if(identifier == "$signed" || identifier == "$unsigned")
+  if(base_name == "$signed" || base_name == "$unsigned")
   {
     // lower to typecast
     DATA_INVARIANT(
-      arguments.size() == 1, id2string(identifier) + " takes one argument");
+      arguments.size() == 1, id2string(base_name) + " takes one argument");
     return typecast_exprt{arguments[0], call.type()};
   }
-  else if(identifier == "$rtoi")
+  else if(base_name == "$rtoi")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // These truncate, and do not round.
     return floatbv_typecast_exprt{
       arguments[0],
       ieee_floatt::rounding_mode_expr(
         ieee_floatt::rounding_modet::ROUND_TO_ZERO),
       verilog_lowering(call.type())};
   }
-  else if(identifier == "$itor")
+  else if(base_name == "$itor")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // No rounding required, any 32-bit integer will fit into double.
     return floatbv_typecast_exprt{
       arguments[0],
       ieee_floatt::rounding_mode_expr(
         ieee_floatt::rounding_modet::ROUND_TO_ZERO),
       verilog_lowering(call.type())};
   }
-  else if(identifier == "$bitstoreal")
+  else if(base_name == "$bitstoreal")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // not a conversion -- this returns the given bit-pattern as a real
     return typecast_exprt{
       zero_extend_exprt{arguments[0], bv_typet{64}},
       verilog_lowering(call.type())};
   }
-  else if(identifier == "$bitstoshortreal")
+  else if(base_name == "$bitstoshortreal")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // not a conversion -- this returns the given bit-pattern as a real
     return typecast_exprt{
       zero_extend_exprt{arguments[0], bv_typet{32}},
       verilog_lowering(call.type())};
   }
-  else if(identifier == "$realtobits")
+  else if(base_name == "$realtobits")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // not a conversion -- this returns the given floating-point bit-pattern as [63:0]
     return zero_extend_exprt{
       typecast_exprt{arguments[0], bv_typet{64}}, call.type()};
   }
-  else if(identifier == "$shortrealtobits")
+  else if(base_name == "$shortrealtobits")
   {
     DATA_INVARIANT(
-      arguments.size(), id2string(identifier) + " takes one argument");
+      arguments.size(), id2string(base_name) + " takes one argument");
     // not a conversion -- this returns the given floating-point bit-pattern as [31:0]
     return zero_extend_exprt{
       typecast_exprt{arguments[0], bv_typet{32}}, call.type()};
@@ -350,8 +350,8 @@ exprt verilog_lowering(exprt expr)
     auto &call = to_function_call_expr(expr);
     if(call.is_system_function_call())
     {
-      auto identifier = to_symbol_expr(call.function()).get_identifier();
-      if(identifier == "$typename")
+      auto base_name = to_verilog_identifier_expr(call.function()).base_name();
+      if(base_name == "$typename")
       {
         // Don't touch.
         // Will be expanded by elaborate_constant_system_function_call,

src/verilog/verilog_synthesis.cpp

@@ -342,8 +342,8 @@ exprt verilog_synthesist::expand_function_call(
   // Is it a 'system function call'?
   if(call.is_system_function_call())
   {
-    auto identifier = to_symbol_expr(call.function()).get_identifier();
-    if(identifier == "$ND")
+    auto base_name = to_verilog_identifier_expr(call.function()).base_name();
+    if(base_name == "$ND")
     {
       std::string identifier =
         id2string(module) + "::nondet::" + std::to_string(nondet_count++);
@@ -354,7 +354,7 @@ exprt verilog_synthesist::expand_function_call(
       select_one.set(ID_identifier, identifier);
       return select_one.with_source_location(call);
     }
-    else if(identifier == "$past")
+    else if(base_name == "$past")
     {
       auto what = call.arguments()[0];
       auto ticks = call.arguments().size() < 2
@@ -363,8 +363,8 @@ exprt verilog_synthesist::expand_function_call(
       return verilog_past_exprt{what, ticks}.with_source_location(call);
     }
     else if(
-      identifier == "$stable" || identifier == "$rose" ||
-      identifier == "$fell" || identifier == "$changed")
+      base_name == "$stable" || base_name == "$rose" || base_name == "$fell" ||
+      base_name == "$changed")
     {
       DATA_INVARIANT(call.arguments().size() >= 1, "must have argument");
       auto what = call.arguments()[0];
@@ -376,18 +376,18 @@ exprt verilog_synthesist::expand_function_call(
           std::move(expr), from_integer(0, integer_typet{})};
       };
 
-      if(identifier == "$stable")
+      if(base_name == "$stable")
         return equal_exprt{what, past};
-      else if(identifier == "$changed")
+      else if(base_name == "$changed")
         return notequal_exprt{what, past};
-      else if(identifier == "$rose")
+      else if(base_name == "$rose")
         return and_exprt{not_exprt{lsb(past)}, lsb(what)};
-      else if(identifier == "$fell")
+      else if(base_name == "$fell")
         return and_exprt{lsb(past), not_exprt{lsb(what)}};
       else
         DATA_INVARIANT(false, "all cases covered");
     }
-    else if(identifier == "$countones")
+    else if(base_name == "$countones")
     {
       // lower to popcount
       DATA_INVARIANT(
@@ -3094,21 +3094,15 @@ Function: verilog_synthesist::synth_function_call_or_task_enable
 void verilog_synthesist::synth_function_call_or_task_enable(
   const verilog_function_callt &statement)
 {
-  // this is essentially inlined
-  const symbol_exprt &function=to_symbol_expr(statement.function());
-  
-  irep_idt identifier=function.get_identifier();
-  
-  // We ignore everyting that starts with a '$',
-  // e.g., $display etc
-    
-  if(!identifier.empty() && identifier[0]=='$')       
+  if(statement.is_system_function_call())
   {
-    // ignore
+    // ignore system functions
   }
   else
   {
-    const symbolt &symbol=ns.lookup(identifier);
+    // this is essentially inlined
+    const symbol_exprt &function = to_symbol_expr(statement.function());
+    const symbolt &symbol = ns.lookup(function);
 
     if(symbol.type.id()!=ID_code)
     {