Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage

SEC-58: Split the entry-point-generation phase into two parts

Author: smowton

cbmc/regression/cbmc/mixed-c-library-goto-main/lib.c

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

cbmc/regression/cbmc/mixed-c-library-goto-main/main.c

@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}

cbmc/regression/cbmc/mixed-c-library-goto-main/main.gb

@@ -0,0 +1,8 @@
+CORE
+main.gb
+lib.c --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

cbmc/regression/cbmc/mixed-c-library-goto-main/with_function.desc

@@ -0,0 +1,8 @@
+CORE
+main.gb
+lib.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

cbmc/regression/cbmc/mixed-c-library-goto-main/without_function.desc

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

cbmc/regression/cbmc/mixed-goto-library-c-main/lib.c

@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}

cbmc/regression/cbmc/mixed-goto-library-c-main/lib.gb

@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.gb --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

cbmc/regression/cbmc/mixed-goto-library-c-main/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.gb
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

cbmc/regression/cbmc/mixed-goto-library-c-main/with_function.desc

@@ -37,22 +37,6 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
-/// Generate a _start function for a specific function
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   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 irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  return generate_ansi_c_start_function(
-    symbol_table.symbols.at(entry_function_symbol_id),
-    symbol_table,
-    *message_handler);
-}
-
 /// ANSI-C preprocessing
 bool ansi_c_languaget::preprocess(
   std::istream &instream,
@@ -141,19 +125,19 @@ bool ansi_c_languaget::typecheck(
   return false;
 }
 
-bool ansi_c_languaget::final(
-  symbol_tablet &symbol_table,
-  bool create_start_function)
+bool ansi_c_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
 {
+  // Note this can happen here because C doesn't currently
+  // support lazy loading at the symbol-table level, and therefore
+  // function bodies have already been populated and external stub
+  // symbols created during the typecheck() phase. If it gains lazy
+  // loading support then stubs will need to be created during
+  // function body parsing, or else generate-stubs moved to the
+  // final phase.
   generate_opaque_method_stubs(symbol_table);
-
-  if(create_start_function)
-  {
-    if(ansi_c_entry_point(symbol_table, get_message_handler()))
-      return true;
-  }
-
-  return false;
+  // This creates __CPROVER_start and __CPROVER_initialize:
+  return ansi_c_entry_point(symbol_table, get_message_handler());
 }
 
 void ansi_c_languaget::show_parse(std::ostream &out)

cbmc/regression/cbmc/mixed-goto-library-c-main/without_function.desc

@@ -31,14 +31,13 @@ class ansi_c_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module) override;
 
-  bool final(
-    symbol_tablet &symbol_table,
-    bool create_start_function) override;
-
   void show_parse(std::ostream &out) override;
 
   ~ansi_c_languaget() override;
@@ -77,10 +76,6 @@ class ansi_c_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;

cbmc/src/ansi-c/ansi_c_language.cpp

@@ -51,7 +51,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -629,20 +628,6 @@ int cbmc_parse_optionst::get_goto_program(
     // are already compiled
       return 6;
 
-    if(cmdline.isset("function"))
-    {
-      const std::string &function_id=cmdline.get_value("function");
-      rebuild_goto_start_functiont start_function_rebuilder(
-        get_message_handler(),
-        goto_model.symbol_table,
-        goto_model.goto_functions);
-
-      if(start_function_rebuilder(function_id))
-      {
-        return 6;
-      }
-    }
-
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table(goto_model, ui_message_handler.get_ui());

cbmc/src/ansi-c/ansi_c_language.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
-#include <goto-programs/rebuild_goto_start_function.h>
+#include <util/language.h>
 
 #include <analyses/goto_check.h>
 

cbmc/src/cbmc/cbmc_parse_options.cpp

@@ -54,22 +54,6 @@ void cpp_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
-/// Generate a _start function for a specific function
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   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 irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  return generate_ansi_c_start_function(
-    symbol_table.lookup(entry_function_symbol_id),
-    symbol_table,
-    *message_handler);
-}
-
 /// ANSI-C preprocessing
 bool cpp_languaget::preprocess(
   std::istream &instream,
@@ -151,17 +135,10 @@ bool cpp_languaget::typecheck(
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }
 
-bool cpp_languaget::final(
-  symbol_tablet &symbol_table,
-  bool create_start_function)
+bool cpp_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
 {
-  if(create_start_function)
-  {
-    if(ansi_c_entry_point(symbol_table, get_message_handler()))
-      return true;
-  }
-
-  return false;
+  return ansi_c_entry_point(symbol_table, get_message_handler());
 }
 
 void cpp_languaget::show_parse(std::ostream &out)

cbmc/src/cbmc/cbmc_parse_options.h

@@ -33,6 +33,9 @@ class cpp_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module) override;
@@ -43,10 +46,6 @@ class cpp_languaget:public languaget
     const std::string &module,
     class replace_symbolt &replace_symbol) const;
 
-  bool final(
-    symbol_tablet &symbol_table,
-    bool create_start_function) override;
-
   void show_parse(std::ostream &out) override;
 
   // constructor, destructor
@@ -89,10 +88,6 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;

cbmc/src/cpp/cpp_language.cpp

@@ -14,10 +14,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/language.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 

cbmc/src/cpp/cpp_language.h

@@ -29,7 +29,6 @@ Author: Daniel Kroening, [email protected]
 bool initialize_goto_model(
   goto_modelt &goto_model,
   const cmdlinet &cmdline,
-  bool generate_start_function,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);
@@ -54,12 +53,11 @@ bool initialize_goto_model(
         sources.push_back(file);
     }
 
+    language_filest language_files;
+    language_files.set_message_handler(message_handler);
+
     if(!sources.empty())
     {
-      language_filest language_files;
-
-      language_files.set_message_handler(message_handler);
-
       for(const auto &filename : sources)
       {
         #ifdef _MSC_VER
@@ -115,17 +113,6 @@ bool initialize_goto_model(
         msg.error() << "CONVERSION ERROR" << messaget::eom;
         return true;
       }
-
-      if(binaries.empty())
-      {
-        if(language_files.final(
-          goto_model.symbol_table,
-          generate_start_function))
-        {
-          msg.error() << "CONVERSION ERROR" << messaget::eom;
-          return true;
-        }
-      }
     }
 
     for(const auto &file : binaries)
@@ -136,18 +123,39 @@ bool initialize_goto_model(
         return true;
     }
 
-    if(cmdline.isset("function"))
+    bool binaries_provided_start=
+      goto_model.symbol_table.has_symbol(goto_functionst::entry_point());
+
+    bool entry_point_generation_failed=false;
+
+    if(binaries_provided_start && cmdline.isset("function"))
     {
-      const std::string &function_id=cmdline.get_value("function");
-      rebuild_goto_start_functiont start_function_rebuilder(
+      // Rebuild the entry-point, using the language annotation of the
+      // existing __CPROVER_start function:
+      rebuild_goto_start_functiont rebuild_existing_start(
         msg.get_message_handler(),
         goto_model.symbol_table,
         goto_model.goto_functions);
+      entry_point_generation_failed=rebuild_existing_start();
+    }
+    else if(!binaries_provided_start)
+    {
+      // Allow all language front-ends to try to provide the user-specified
+      // (--function) entry-point, or some language-specific default:
+      entry_point_generation_failed=
+        language_files.generate_support_functions(goto_model.symbol_table);
+    }
 
-      if(start_function_rebuilder(function_id))
-      {
-        return 6;
-      }
+    if(entry_point_generation_failed)
+    {
+      msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
+      return true;
+    }
+
+    if(language_files.final(goto_model.symbol_table))
+    {
+      msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
+      return true;
     }
 
     msg.status() << "Generating GOTO Program" << messaget::eom;

cbmc/src/goto-analyzer/goto_analyzer_parse_options.h

@@ -21,16 +21,6 @@ Author: Daniel Kroening, [email protected]
 bool initialize_goto_model(
   goto_modelt &goto_model,
   const cmdlinet & cmdline,
-  bool generate_start_function,
   message_handlert &message_handler);
 
-inline bool initialize_goto_model(
-  goto_modelt &goto_model,
-  const cmdlinet &cmdline,
-  message_handlert &message_handler)
-{
-  return initialize_goto_model(goto_model, cmdline, true, message_handler);
-}
-
-
 #endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H