Merge pull request #6220 from martin-cs/refactor/virtual_register_languages

martin-cs · web-flow · commit 06afe802d647 · 2021-08-04T00:50:44.000+01:00
Refactor/virtual register languages
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h
@@ -154,8 +154,8 @@ class optionst;
 class janalyzer_parse_optionst : public parse_options_baset
 {
 public:
-  virtual int doit() override;
-  virtual void help() override;
+  int doit() override;
+  void help() override;
 
   janalyzer_parse_optionst(int argc, const char **argv);
 
@@ -177,7 +177,7 @@ class janalyzer_parse_optionst : public parse_options_baset
 protected:
   std::unique_ptr<class_hierarchyt> class_hierarchy;
 
-  void register_languages();
+  void register_languages() override;
 
   void get_command_line_options(optionst &options);
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -42,13 +42,13 @@ class goto_modelt;
 class jdiff_parse_optionst : public parse_options_baset
 {
 public:
-  virtual int doit();
-  virtual void help();
+  int doit() override;
+  void help() override;
 
   jdiff_parse_optionst(int argc, const char **argv);
 
 protected:
-  void register_languages();
+  void register_languages() override;
 
   void get_command_line_options(optionst &options);
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -114,7 +114,7 @@ class cbmc_parse_optionst : public parse_options_baset
 protected:
   goto_modelt goto_model;
 
-  void register_languages();
+  void register_languages() override;
   void get_command_line_options(optionst &);
   void preprocessing(const optionst &);
   bool set_properties();
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
@@ -1,4 +1,5 @@
-SRC = goto_analyzer_main.cpp \
+SRC = goto_analyzer_languages.cpp \
+      goto_analyzer_main.cpp \
       goto_analyzer_parse_options.cpp \
       taint_analysis.cpp \
       taint_parser.cpp \
diff --git a/src/goto-analyzer/goto_analyzer_languages.cpp b/src/goto-analyzer/goto_analyzer_languages.cpp
@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: Language Registration
+
+Author: Martin Brain, martin.brain@cs.ox.ac.uk
+
+\*******************************************************************/
+
+/// \file
+/// Language Registration
+
+#include "goto_analyzer_parse_options.h"
+
+#include <langapi/mode.h>
+
+#include <ansi-c/ansi_c_language.h>
+#include <cpp/cpp_language.h>
+
+#ifdef HAVE_JSIL
+#  include <jsil/jsil_language.h>
+#endif
+
+void goto_analyzer_parse_optionst::register_languages()
+{
+  register_language(new_ansi_c_language);
+  register_language(new_cpp_language);
+
+#ifdef HAVE_JSIL
+  register_language(new_jsil_language);
+#endif
+}
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -16,16 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
-#include <ansi-c/ansi_c_language.h>
 #include <ansi-c/cprover_library.h>
 
 #include <assembler/remove_asm.h>
 
-#include <cpp/cpp_language.h>
 #include <cpp/cprover_library.h>
 
-#include <jsil/jsil_language.h>
-
 #include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
@@ -37,9 +33,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/ai.h>
 #include <analyses/local_may_alias.h>
 
-#include <langapi/mode.h>
-#include <langapi/language.h>
-
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/exit_codes.h>
@@ -65,13 +58,6 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
 {
 }
 
-void goto_analyzer_parse_optionst::register_languages()
-{
-  register_language(new_ansi_c_language);
-  register_language(new_cpp_language);
-  register_language(new_jsil_language);
-}
-
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -183,7 +183,7 @@ class goto_analyzer_parse_optionst: public parse_options_baset
 protected:
   goto_modelt goto_model;
 
-  virtual void register_languages();
+  void register_languages() override;
 
   virtual void get_command_line_options(optionst &options);
 
diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp
@@ -15,11 +15,17 @@ Author: CM Wintersteiger
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
-#include <jsil/jsil_language.h>
+
+#ifdef HAVE_JSIL
+#  include <jsil/jsil_language.h>
+#endif
 
 void goto_cc_modet::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
+
+#ifdef HAVE_JSIL
   register_language(new_jsil_language);
+#endif
 }
diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h
@@ -43,13 +43,13 @@ class optionst;
 class goto_diff_parse_optionst : public parse_options_baset
 {
 public:
-  virtual int doit();
-  virtual void help();
+  int doit() override;
+  void help() override;
 
   goto_diff_parse_optionst(int argc, const char **argv);
 
 protected:
-  void register_languages();
+  void register_languages() override;
 
   void get_command_line_options(optionst &options);
 
diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp
@@ -108,6 +108,9 @@ int goto_harness_parse_optionst::doit()
   // This just sets up the defaults (and would interpret options such as --32).
   config.set(cmdline);
 
+  // Normally we would register language front-ends here but as goto-harness
+  // only works on goto binaries, we don't need to
+
   // Read goto binary into goto-model
   auto read_goto_binary_result =
     read_goto_binary(got_harness_config.in_file, ui_message_handler);
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
@@ -129,8 +129,8 @@ Author: Daniel Kroening, kroening@kroening.com
 class goto_instrument_parse_optionst : public parse_options_baset
 {
 public:
-  virtual int doit();
-  virtual void help();
+  int doit() override;
+  void help() override;
 
   goto_instrument_parse_optionst(int argc, const char **argv)
     : parse_options_baset(
@@ -145,7 +145,7 @@ class goto_instrument_parse_optionst : public parse_options_baset
   }
 
 protected:
-  void register_languages();
+  void register_languages() override;
 
   void get_goto_program();
   void instrument_goto_program();
diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp
@@ -42,6 +42,13 @@ memory_analyzer_parse_optionst::memory_analyzer_parse_optionst(
 {
 }
 
+void memory_analyzer_parse_optionst::register_languages()
+{
+  // For now only C is supported due to the additional challenges of
+  // mapping source code to debugging symbols in other languages.
+  register_language(new_ansi_c_language);
+}
+
 int memory_analyzer_parse_optionst::doit()
 {
   if(cmdline.isset("version"))
@@ -91,7 +98,7 @@ int memory_analyzer_parse_optionst::doit()
       "--symtab-snapshot");
   }
 
-  register_language(new_ansi_c_language);
+  register_languages();
 
   std::string binary = cmdline.args.front();
 
diff --git a/src/memory-analyzer/memory_analyzer_parse_options.h b/src/memory-analyzer/memory_analyzer_parse_options.h
@@ -37,6 +37,8 @@ class memory_analyzer_parse_optionst : public parse_options_baset
 
 protected:
   messaget message;
+
+  void register_languages() override;
 };
 
 #endif // CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H
diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp
@@ -96,6 +96,15 @@ static void run_symtab2gb(
   }
 }
 
+void symtab2gb_parse_optionst::register_languages()
+{
+  // As this is a converter and linker it only really needs to support
+  // the JSON symtab front-end.
+  register_language(new_json_symtab_language);
+  // Workaround to allow external front-ends to use "C" mode
+  register_language(new_ansi_c_language);
+}
+
 int symtab2gb_parse_optionst::doit()
 {
   if(cmdline.isset("version"))
@@ -114,9 +123,7 @@ int symtab2gb_parse_optionst::doit()
   {
     gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
   }
-  register_language(new_json_symtab_language);
-  // Workaround to allow external front-ends to use "C" mode
-  register_language(new_ansi_c_language);
+  register_languages();
   config.set(cmdline);
   run_symtab2gb(symtab_filenames, gb_filename);
   return CPROVER_EXIT_SUCCESS;
diff --git a/src/symtab2gb/symtab2gb_parse_options.h b/src/symtab2gb/symtab2gb_parse_options.h
@@ -27,6 +27,9 @@ class symtab2gb_parse_optionst : public parse_options_baset
   symtab2gb_parse_optionst(int argc, const char *argv[]);
   void help() override;
   int doit() override;
+
+protected:
+  void register_languages() override;
 };
 
 #endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
@@ -45,6 +45,10 @@ class parse_options_baset
   ui_message_handlert ui_message_handler;
   messaget log;
 
+  virtual void register_languages()
+  {
+  }
+
 private:
   void unknown_option_msg();
 };
