enable JAR file support for goto-diff

src/cbmc/cbmc_parse_options.cpp

@@ -71,7 +71,9 @@ Function: cbmc_parse_optionst::cbmc_parse_optionst
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),
-  language_uit("CBMC " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                       "CBMC " CBMC_VERSION)
 {
 }
 
@@ -93,7 +95,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   const std::string &extra_options):
   parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
   xml_interfacet(cmdline),
-  language_uit("CBMC " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                       "CBMC " CBMC_VERSION)
 {
 }
 

src/cbmc/cbmc_parse_options.h

@@ -72,6 +72,7 @@ class cbmc_parse_optionst:
     const std::string &extra_options);
 
 protected:
+  ui_message_handlert ui_message_handler;
   virtual void register_languages();
 
   virtual void get_command_line_options(optionst &options);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -62,7 +62,9 @@ Function: goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv),
-  language_uit("GOTO-ANALYSER " CBMC_VERSION, cmdline)
+  language_uit(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline),
+                     "GOTO-ANALYZER " CBMC_VERSION)
 {
 }
 

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -49,6 +49,7 @@ class goto_analyzer_parse_optionst:
   goto_analyzer_parse_optionst(int argc, const char **argv);
 
 protected:
+  ui_message_handlert ui_message_handler;
   get_goto_modelt goto_model;
 
   virtual void register_languages();

src/goto-cc/compile.cpp

@@ -736,7 +736,9 @@ Function: compilet::compilet
 \*******************************************************************/
 
 compilet::compilet(cmdlinet &_cmdline):
-  language_uit("goto-cc " CBMC_VERSION, _cmdline),
+  language_uit(_cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(_cmdline),
+                     "goto-cc " CBMC_VERSION),
   ns(symbol_table),
   cmdline(_cmdline)
 {

src/goto-cc/compile.h

@@ -20,6 +20,7 @@ Date: June 2006
 class compilet:public language_uit
 {
 public:
+  ui_message_handlert ui_message_handler;
   namespacet ns;
   goto_functionst compiled_functions;
   bool echo_file_name;

src/goto-cc/goto_cc_mode.cpp

@@ -34,7 +34,9 @@ Function: goto_cc_modet::goto_cc_modet
 \*******************************************************************/
 
 goto_cc_modet::goto_cc_modet(goto_cc_cmdlinet &_cmdline):
-  language_uit("goto-cc " CBMC_VERSION, _cmdline),
+  language_uit(_cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(_cmdline),
+                     "goto-cc " CBMC_VERSION),
   cmdline(_cmdline)
 {
   register_languages();

src/goto-cc/goto_cc_mode.h

@@ -30,6 +30,7 @@ class goto_cc_modet:public language_uit
   ~goto_cc_modet();
 
 protected:
+  ui_message_handlert ui_message_handler;
   void register_languages();
   goto_cc_cmdlinet &cmdline;
 };

src/goto-diff/goto_diff_base.cpp

@@ -7,6 +7,7 @@ Author: Peter Schrammel
 \*******************************************************************/
 
 #include <util/i2string.h>
+#include <util/json_expr.h>
 
 #include "goto_diff.h"
 
@@ -126,7 +127,10 @@ void goto_difft::convert_function(
 {
   const goto_programt &program=
     goto_model2.goto_functions.function_map.at(function_name).body;
-  result["file"]=json_stringt(
-    id2string(program.instructions.begin()->source_location.get_file()));
+  if(!program.instructions.empty())
+  {
+    result["sourceLocation"]=
+      json(program.instructions.begin()->source_location);
+  }
   result["name"]=json_stringt(id2string(function_name));
 }

src/goto-diff/goto_diff_languages.cpp

@@ -19,11 +19,11 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/java_bytecode_language.h>
 #endif
 
-#include "goto_diff_parse_options.h"
+#include "goto_diff_languages.h"
 
 /*******************************************************************\
 
-Function: goto_diff_parse_optionst::register_languages
+Function: goto_diff_languagest::register_languages
 
   Inputs:
 
@@ -33,7 +33,7 @@ Function: goto_diff_parse_optionst::register_languages
 
 \*******************************************************************/
 
-void goto_diff_parse_optionst::register_languages()
+void goto_diff_languagest::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);

src/goto-diff/goto_diff_languages.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: GOTO-DIFF Languages
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_DIFF_LANGUAGES_H
+#define CPROVER_GOTO_DIFF_LANGUAGES_H
+
+#include <langapi/language_ui.h>
+#include <goto-programs/goto_model.h>
+
+class goto_diff_languagest :
+  public language_uit
+{
+public:
+  explicit goto_diff_languagest(
+    const cmdlinet& cmdline,
+    ui_message_handlert &ui_message_handler) :
+  language_uit(cmdline, ui_message_handler)
+  {
+    register_languages();
+  }
+
+protected:
+  virtual void register_languages();
+
+};
+
+#endif

src/goto-diff/goto_diff_parse_options.cpp

@@ -62,7 +62,10 @@ Function: goto_diff_parse_optionst::goto_diff_parse_optionst
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),
-  language_uit("GOTO_DIFF " CBMC_VERSION, cmdline)
+  goto_diff_languagest(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline), 
+    "GOTO-DIFF " CBMC_VERSION),
+  languages2(cmdline, ui_message_handler)
 {
 }
 
@@ -83,7 +86,10 @@ ::goto_diff_parse_optionst::goto_diff_parse_optionst(
   const char **argv,
   const std::string &extra_options):
   parse_options_baset(GOTO_DIFF_OPTIONS+extra_options, argc, argv),
-  language_uit("GOTO_DIFF " CBMC_VERSION, cmdline)
+  goto_diff_languagest(cmdline, ui_message_handler),
+  ui_message_handler(language_uit::get_ui_cmdline(cmdline), 
+    "GOTO-DIFF " CBMC_VERSION),
+  languages2(cmdline, ui_message_handler)
 {
 }
 
@@ -309,20 +315,27 @@ int goto_diff_parse_optionst::doit()
   //
   // Print a banner
   //
-  status() << "GOTO_DIFF version " CBMC_VERSION " "
+  status() << "GOTO-DIFF version " CBMC_VERSION " "
            << sizeof(void *)*8 << "-bit "
            << config.this_architecture() << " "
            << config.this_operating_system() << eom;
 
-  register_languages();
+  if(cmdline.args.size()!=2)
+  {
+    error() << "Please provide two programs to compare" << eom;
+    return 6;
+  }
 
   goto_modelt goto_model1, goto_model2;
 
-  int get_goto_programs_ret=
-    get_goto_programs(options, goto_model1, goto_model2);
-
-  if(get_goto_programs_ret!=-1)
-    return get_goto_programs_ret;
+  int get_goto_program_ret=
+    get_goto_program(options, *this, goto_model1);
+  if(get_goto_program_ret!=-1)
+    return get_goto_program_ret;
+  get_goto_program_ret=
+    get_goto_program(options, languages2, goto_model2);
+  if(get_goto_program_ret!=-1)
+    return get_goto_program_ret;
 
   if(cmdline.isset("show-goto-functions"))
   {
@@ -376,7 +389,7 @@ int goto_diff_parse_optionst::doit()
 
 /*******************************************************************\
 
-Function: goto_diff_parse_optionst::get_goto_programs
+Function: goto_diff_parse_optionst::get_goto_program
 
   Inputs:
 
@@ -386,33 +399,54 @@ Function: goto_diff_parse_optionst::get_goto_programs
 
 \*******************************************************************/
 
-int goto_diff_parse_optionst::get_goto_programs(
+int goto_diff_parse_optionst::get_goto_program(
   const optionst &options,
-  goto_modelt &goto_model1,
-  goto_modelt &goto_model2)
+  goto_diff_languagest &languages,
+  goto_modelt &goto_model)
 {
-  if(cmdline.args.size()!=2)
+  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
+
+  if(is_goto_binary(cmdline.args[0]))
   {
-    error() << "Please provide two programs to compare" << eom;
-    return 6;
+    if(read_goto_binary(cmdline.args[0],
+                        goto_model.symbol_table, goto_model.goto_functions,
+                        languages.get_message_handler()))
+      return 6;
+
+    config.set(cmdline);
+    config.set_from_symbol_table(goto_model.symbol_table);
+
+    // This one is done.
+    cmdline.args.erase(cmdline.args.begin());
   }
+  else
+  {
+    // This is a a workaround to make parse() think that there is only 
+    // one source file.
+    std::string arg2("");
+    if(cmdline.args.size()==2)
+    {
+      arg2 = cmdline.args[1];
+      cmdline.args.erase(--cmdline.args.end());
+    }
 
-  status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;
+    if(languages.parse()) return 6;
+    if(languages.typecheck()) return 6;
+    if(languages.final()) return 6;
 
-  if(read_goto_binary(cmdline.args[0],
-                      goto_model1.symbol_table, goto_model1.goto_functions,
-                      get_message_handler()))
-    throw 0;
+    // we no longer need any parse trees or language files
+    languages.clear_parse();
 
-  status() << "Reading GOTO program from `" << cmdline.args[1] << "'" << eom;
+    status() << "Generating GOTO Program" << eom;
 
-  if(read_goto_binary(cmdline.args[1],
-                      goto_model2.symbol_table, goto_model2.goto_functions,
-                      get_message_handler()))
-    throw 0;
+    goto_model.symbol_table=languages.symbol_table;
+    goto_convert(goto_model.symbol_table, goto_model.goto_functions,
+                 ui_message_handler);
 
-  config.set(cmdline);
-  config.set_from_symbol_table(goto_model2.symbol_table);
+    // if we had a second argument then we will handle it next
+    if(arg2!="")
+      cmdline.args[0]=arg2;
+  }
 
   return -1; // no error, continue
 }

src/goto-diff/goto_diff_parse_options.h

@@ -16,6 +16,8 @@ Author: Peter Schrammel
 
 #include <goto-programs/goto_model.h>
 
+#include "goto_diff_languages.h"
+
 class goto_modelt;
 class optionst;
 
@@ -28,7 +30,7 @@ class optionst;
 
 class goto_diff_parse_optionst:
   public parse_options_baset,
-  public language_uit
+  public goto_diff_languagest
 {
 public:
   virtual int doit();
@@ -41,14 +43,15 @@ class goto_diff_parse_optionst:
     const std::string &extra_options);
 
 protected:
-  virtual void register_languages();
+  ui_message_handlert ui_message_handler;
+  goto_diff_languagest languages2;
 
   virtual void get_command_line_options(optionst &options);
 
-  virtual int get_goto_programs(
+  virtual int get_goto_program(
     const optionst &options,
-    goto_modelt &goto_model1,
-    goto_modelt &goto_model2);
+    goto_diff_languagest &languages,
+    goto_modelt &goto_model);
 
   virtual bool process_goto_program(
     const optionst &options,

src/goto-instrument/goto_instrument_parse_options.h

@@ -73,14 +73,16 @@ class goto_instrument_parse_optionst:
 
   goto_instrument_parse_optionst(int argc, const char **argv):
     parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv),
-    language_uit("goto-instrument", cmdline),
+    language_uit(cmdline, ui_message_handler),
+    ui_message_handler(language_uit::get_ui_cmdline(cmdline),"goto-instrument"),
     function_pointer_removal_done(false),
     partial_inlining_done(false),
     remove_returns_done(false)
   {
   }
 
 protected:
+  ui_message_handlert ui_message_handler;
   virtual void register_languages();
 
   void get_goto_program();

src/langapi/language_ui.cpp

@@ -31,7 +31,7 @@ Function: get_ui_cmdline
 
 \*******************************************************************/
 
-static ui_message_handlert::uit get_ui_cmdline(const cmdlinet &cmdline)
+ui_message_handlert::uit language_uit::get_ui_cmdline(const cmdlinet &cmdline)
 {
   if(cmdline.isset("xml-ui"))
     return ui_message_handlert::XML_UI;
@@ -55,9 +55,9 @@ Function: language_uit::language_uit
 \*******************************************************************/
 
 language_uit::language_uit(
-  const std::string &program,
-  const cmdlinet &__cmdline):
-  ui_message_handler(get_ui_cmdline(__cmdline), program),
+  const cmdlinet &__cmdline,
+  ui_message_handlert &_ui_message_handler):
+  ui_message_handler(_ui_message_handler),
   _cmdline(__cmdline)
 {
   set_message_handler(ui_message_handler);