Merge pull request #7238 from tautschnig/bugfixes/7057-entry-point

C/C++ entry-point: resolve full symbol names

Author: tautschnig

regression/cbmc-cpp/entry_point1/main.cpp

@@ -0,0 +1,4 @@
+void mymain()
+{
+  __CPROVER_assert(false, "expected to fail");
+}

regression/cbmc-cpp/entry_point1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+--function 'mymain()'
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/message.h>
 #include <util/pointer_expr.h>
-#include <util/range.h>
 #include <util/symbol_table_base.h>
 
 #include <goto-programs/goto_functions.h>
@@ -118,20 +117,14 @@ bool ansi_c_entry_point(
   // find main symbol, if any is given
   if(config.main.has_value())
   {
-    std::list<irep_idt> matches;
+    auto matches = symbol_table.match_name_or_base_name(*config.main);
 
-    for(const auto &symbol_name_entry :
-        equal_range(symbol_table.symbol_base_map, config.main.value()))
+    for(auto it = matches.begin(); it != matches.end();) // no ++it
     {
-      // look it up
-      symbol_table_baset::symbolst::const_iterator s_it =
-        symbol_table.symbols.find(symbol_name_entry.second);
-
-      if(s_it==symbol_table.symbols.end())
-        continue;
-
-      if(s_it->second.type.id() == ID_code && !s_it->second.is_property)
-        matches.push_back(symbol_name_entry.second);
+      if((*it)->second.type.id() != ID_code || (*it)->second.is_property)
+        it = matches.erase(it);
+      else
+        ++it;
     }
 
     if(matches.empty())
@@ -150,7 +143,7 @@ bool ansi_c_entry_point(
       return true;
     }
 
-    main_symbol=matches.front();
+    main_symbol = matches.front()->first;
   }
   else
     main_symbol=ID_main;

src/goto-programs/initialize_goto_model.cpp

@@ -40,17 +40,20 @@ static bool generate_entry_point_for_function(
 {
   const irep_idt &entry_function_name = options.get_option("function");
   CHECK_RETURN(!entry_function_name.empty());
-  auto const entry_function_sym = symbol_table.lookup(entry_function_name);
-  if(entry_function_sym == nullptr)
+  auto matches = symbol_table.match_name_or_base_name(entry_function_name);
+  // it's ok if this is ambiguous at this point, we just need to get a mode, the
+  // actual entry point generator will take care of resolving (or rejecting)
+  // ambiguity
+  if(matches.empty())
   {
     throw invalid_command_line_argument_exceptiont{
-      // NOLINTNEXTLINE(whitespace/braces)
-      std::string{"couldn't find function with name '"} +
+      std::string("couldn't find entry with name '") +
         id2string(entry_function_name) + "' in symbol table",
       "--function"};
   }
-  PRECONDITION(!entry_function_sym->mode.empty());
-  auto const entry_language = get_language_from_mode(entry_function_sym->mode);
+  const auto &entry_point_mode = matches.front()->second.mode;
+  PRECONDITION(!entry_point_mode.empty());
+  auto const entry_language = get_language_from_mode(entry_point_mode);
   CHECK_RETURN(entry_language != nullptr);
   entry_language->set_message_handler(message_handler);
   entry_language->set_language_options(options);

src/util/symbol_table_base.h

@@ -109,6 +109,33 @@ class symbol_table_baset
     return *symbol;
   }
 
+  /// Collect all symbols the name of which matches \p id or the base name of
+  /// which matches \p id.
+  std::list<symbolst::const_iterator>
+  match_name_or_base_name(const irep_idt &id) const
+  {
+    std::list<symbolst::const_iterator> results;
+
+    auto name_it = symbols.find(id);
+    if(name_it != symbols.end())
+      results.push_back(name_it);
+
+    auto base_name_it_pair = symbol_base_map.equal_range(id);
+    for(auto base_name_it = base_name_it_pair.first;
+        base_name_it != base_name_it_pair.second;
+        ++base_name_it)
+    {
+      name_it = symbols.find(base_name_it->second);
+      CHECK_RETURN(name_it != symbols.end());
+      // don't add entries where name and base name match as this amounts to the
+      // case already covered above
+      if(base_name_it->first != base_name_it->second)
+        results.push_back(name_it);
+    }
+
+    return results;
+  }
+
   /// Find a symbol in the symbol table for read-write access.
   /// \param name: The name of the symbol to look for
   /// \return A pointer to the found symbol if it exists, nullptr otherwise.