SystemVerilog: declarations in named blocks in tasks/functions

This fixes the identifier generated for declarations in named blocks in
tasks and functions.

Author: kroening

regression/verilog/functioncall/named_block1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 named_block1.sv
 
 ^\[.*\] always main\.foo\(\) == 123: PROVED$

src/verilog/verilog_typecheck.cpp

@@ -273,9 +273,11 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl)
 {
   irep_idt decl_class=decl.get_class();
 
-  const std::string identifier=
-    id2string(module_identifier)+"."+
-    id2string(decl.get_identifier());
+  // the base name of the function/task
+  auto base_name = decl.get_identifier();
+
+  const std::string identifier =
+    id2string(module_identifier) + "." + id2string(base_name);
 
   auto result=symbol_table.get_writeable(identifier);
 
@@ -292,11 +294,18 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl)
 
   function_or_task_name = symbol.name;
 
+  // function/tasks have an implicit named block with the name
+  // of the function
+
+  named_blocks.push_back(id2string(base_name) + ".");
+
   for(auto &inner_decl : decl.declarations())
     convert_decl(inner_decl);
 
   convert_statement(decl.body());
 
+  named_blocks.pop_back();
+
   function_or_task_name="";
 
   symbol.value=decl.body();
@@ -336,6 +345,11 @@ exprt verilog_typecheckt::elaborate_constant_function_call(
 
   function_or_task_name = function_symbol.name;
 
+  // function/tasks have an implicit named block with the name
+  // of the function
+
+  named_blocks.push_back(id2string(function_symbol.base_name) + ".");
+
   for(auto &inner_decl : decl.declarations())
     convert_decl(inner_decl);
 
@@ -380,6 +394,8 @@ exprt verilog_typecheckt::elaborate_constant_function_call(
   // interpret it
   verilog_interpreter(decl.body());
 
+  named_blocks.pop_back();
+
   function_or_task_name="";
 
   // get return value
@@ -429,16 +445,9 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl)
       named_block = named_blocks.back();
 
     // fix the type and identifier
-    irep_idt full_identifier;
-
-    if(!function_or_task_name.empty())
-      full_identifier = id2string(function_or_task_name) + "." +
-                        id2string(named_block) +
-                        id2string(declarator.base_name());
-    else
-      full_identifier = id2string(module_identifier) + "." +
-                        id2string(named_block) +
-                        id2string(declarator.base_name());
+    auto full_identifier = id2string(module_identifier) + "." +
+                           id2string(named_block) +
+                           id2string(declarator.base_name());
 
     symbolt &symbol = symbol_table_lookup(full_identifier);
     declarator.type() = symbol.type;

src/verilog/verilog_typecheck_expr.cpp

@@ -1149,24 +1149,10 @@ exprt verilog_typecheck_exprt::convert_symbol(
 {
   const irep_idt &identifier = expr.get_identifier();
 
-  std::string full_identifier;
-
-  // in a task or function? Try local ones first
   if(function_or_task_name!="")
-  {
-    full_identifier=
-      id2string(function_or_task_name)+
-      "."+id2string(identifier);
-    
-    const symbolt *symbol;
-    if(!ns.lookup(full_identifier, symbol))
-    { // found!
-      expr.type()=symbol->type;
-      expr.set_identifier(full_identifier);
-      return std::move(expr);
-    }
-  }
-  
+    DATA_INVARIANT(!named_blocks.empty(), "must have named block");
+
+  std::string full_identifier;
   std::string named_block;
 
   // try named blocks, beginning with inner one