Fixing the method to work with java_bytecode

The java bytecode entry point relied on things working a little
differently.

Firstly, the function name is transformed to allow simpler function
names to be passed in. As such the rebuild_entry_point cannot be
responsible for looking up the symbol. This in turn involved a new way
of identifying the mode to use (using the existing entry points mode)

Secondly, as the lanuages are destroyed after the parsing phase, we must
re-provide the message handler as this is used by the entry point
generation.

Finally, the java_bytecode_entry_point adds a new symbol to the symbol
table, so we remove all symbols that are in the scope of the original
entry point.

Author: thk123

src/ansi-c/ansi_c_language.cpp

@@ -43,11 +43,11 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
 ///   function symbol will be added to this table
 /// \return Returns false if the _start method was generated correctly
 bool ansi_c_languaget::generate_start_function(
-  const symbolt &entry_function_symbol,
+  const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
   return generate_ansi_c_start_function(
-    entry_function_symbol,
+    symbol_table.symbols.at(entry_function_symbol_id),
     symbol_table,
     *message_handler);
 }

src/ansi-c/ansi_c_language.h

@@ -74,7 +74,7 @@ class ansi_c_languaget:public languaget
   void modules_provided(std::set<std::string> &modules) override;
 
   virtual bool generate_start_function(
-    const class symbolt &entry_function_symbol,
+    const irep_idt &entry_function_symbol_id,
     class symbol_tablet &symbol_table) override;
 
 protected:

src/cpp/cpp_language.cpp

@@ -60,11 +60,11 @@ void cpp_languaget::modules_provided(std::set<std::string> &modules)
 ///   function symbol will be added to this table
 /// \return Returns false if the _start method was generated correctly
 bool cpp_languaget::generate_start_function(
-  const symbolt &entry_function_symbol,
+  const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
   return generate_ansi_c_start_function(
-    entry_function_symbol,
+    symbol_table.lookup(entry_function_symbol_id),
     symbol_table,
     *message_handler);
 }

src/cpp/cpp_language.h

@@ -86,7 +86,7 @@ class cpp_languaget:public languaget
   void modules_provided(std::set<std::string> &modules) override;
 
   virtual bool generate_start_function(
-    const class symbolt &entry_function_symbol,
+    const irep_idt &entry_function_symbol_id,
     class symbol_tablet &symbol_table) override;
 
 protected:

src/goto-programs/rebuild_goto_start_function.cpp

@@ -12,6 +12,7 @@
 #include <util/language.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
+#include <util/prefix.h>
 #include <langapi/mode.h>
 #include <memory>
 
@@ -43,30 +44,18 @@ rebuild_goto_start_functiont::rebuild_goto_start_functiont(
 bool rebuild_goto_start_functiont::operator()(
   const irep_idt &entry_function)
 {
-  const auto &desired_entry_function=
-    symbol_table.symbols.find(entry_function);
+  const irep_idt &mode=get_entry_point_mode();
 
-  // Check the specified entry function is a function in the symbol table
-  if(desired_entry_function==symbol_table.symbols.end())
-  {
-    error() << "main symbol `" << entry_function
-            << "' not found" << eom;
-    return true;
-  }
+  // Get the relevant languaget to generate the new entry point with
+  std::unique_ptr<languaget> language=get_language_from_mode(mode);
+  INVARIANT(language, "No language found for mode: "+id2string(mode));
+  language->set_message_handler(get_message_handler());
 
-  // Remove the existing _start function so we can create a new one
-  symbol_table.remove(goto_functionst::entry_point());
-
-  auto language=
-    std::unique_ptr<languaget>(
-      get_language_from_mode(
-        desired_entry_function->second.mode));
-  assert(language);
+  // To create a new entry point we must first remove the old one
+  remove_existing_entry_point();
 
   bool return_code=
-    language->generate_start_function(
-      desired_entry_function->second,
-      symbol_table);
+    language->generate_start_function(entry_function, symbol_table);
 
   // Remove the function from the goto_functions so it is copied back in
   // from the symbol table during goto_convert
@@ -82,3 +71,39 @@ bool rebuild_goto_start_functiont::operator()(
 
   return return_code;
 }
+
+/// Find out the mode of the current entry point to determine the mode of the
+/// replacement entry point
+/// \return A mode string saying which language to use
+irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const
+{
+  const symbolt &current_entry_point=
+    symbol_table.lookup(goto_functionst::entry_point());
+  return current_entry_point.mode;
+}
+
+/// Eliminate the existing entry point function symbol and any symbols created
+/// in that scope from the symbol table.
+void rebuild_goto_start_functiont::remove_existing_entry_point()
+{
+  // Remove the function itself
+  symbol_table.remove(goto_functionst::entry_point());
+
+  // And any symbols created in the scope of the entry point
+  std::vector<irep_idt> entry_point_symbols;
+  for(const auto &symbol_entry : symbol_table.symbols)
+  {
+    const bool is_entry_point_symbol=
+      has_prefix(
+        id2string(symbol_entry.first),
+        id2string(goto_functionst::entry_point()));
+
+    if(is_entry_point_symbol)
+      entry_point_symbols.push_back(symbol_entry.first);
+  }
+
+  for(const irep_idt &entry_point_symbol : entry_point_symbols)
+  {
+    symbol_table.remove(entry_point_symbol);
+  }
+}

src/goto-programs/rebuild_goto_start_function.h

@@ -31,6 +31,10 @@ class rebuild_goto_start_functiont: public messaget
   bool operator()(const irep_idt &entry_function);
 
 private:
+  irep_idt get_entry_point_mode() const;
+
+  void remove_existing_entry_point();
+
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 };

src/java_bytecode/java_bytecode_language.cpp

@@ -113,11 +113,15 @@ void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
 ///   function symbol will be added to this table
 /// \return Returns false if the _start method was generated correctly
 bool java_bytecode_languaget::generate_start_function(
-  const symbolt &entry_function_symbol,
+  const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
+  const auto res=
+    get_main_symbol(
+      symbol_table, entry_function_symbol_id, get_message_handler());
+
   return generate_java_start_function(
-    entry_function_symbol,
+    res.main_function,
     symbol_table,
     get_message_handler(),
     assume_inputs_non_null,

src/java_bytecode/java_bytecode_language.h

@@ -138,7 +138,7 @@ class java_bytecode_languaget:public languaget
     const irep_idt &id, symbol_tablet &) override;
 
   virtual bool generate_start_function(
-    const class symbolt &entry_function_symbol,
+    const irep_idt &entry_function_symbol_id,
     class symbol_tablet &symbol_table) override;
 
 protected:

src/jsil/jsil_language.cpp

@@ -48,7 +48,7 @@ bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
 ///   function symbol will be added to this table
 /// \return Returns false if the _start method was generated correctly
 bool jsil_languaget::generate_start_function(
-  const symbolt &entry_function_symbol,
+  const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
   // TODO(tkiley): This should be implemented if this language

src/jsil/jsil_language.h

@@ -70,7 +70,7 @@ class jsil_languaget:public languaget
   virtual bool interfaces(symbol_tablet &symbol_table) override;
 
   virtual bool generate_start_function(
-    const class symbolt &entry_function_symbol,
+    const irep_idt &entry_function_symbol_id,
     class symbol_tablet &symbol_table) override;
 
 protected:

src/util/language.h

@@ -120,7 +120,7 @@ class languaget:public messaget
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
   virtual bool generate_start_function(
-    const class symbolt &entry_function_symbol,
+    const irep_idt &entry_function_symbol_id,
     class symbol_tablet &symbol_table)=0;
 
   // constructor / destructor