Use structured exceptions in initialize_goto_model

Author: hannes-steffenhagen-diffblue

src/goto-programs/initialize_goto_model.cpp

@@ -1,3 +1,5 @@
+#include <utility>
+
 /*******************************************************************\
 
 Module: Get a Goto Program
@@ -21,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include <goto-programs/rebuild_goto_start_function.h>
+#include <util/exception_utils.h>
 
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
@@ -33,8 +36,9 @@ goto_modelt initialize_goto_model(
   const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    msg.error() << "Please provide a program" << messaget::eom;
-    throw 0;
+    throw invalid_user_input_exceptiont("missing program argument",
+      "",
+      "one or more paths to program files");
   }
 
   std::vector<std::string> binaries, sources;
@@ -66,21 +70,18 @@ goto_modelt initialize_goto_model(
 
       if(!infile)
       {
-        msg.error() << "failed to open input file `" << filename
-          << '\'' << messaget::eom;
-        throw 0;
+        throw io_exceptiont("Failed to open input file `" + filename + '\'');
       }
 
       language_filet &lf=language_files.add_file(filename);
       lf.language=get_language_from_filename(filename);
 
       if(lf.language==nullptr)
       {
+
         source_locationt location;
         location.set_file(filename);
-        msg.error().source_location=location;
-        msg.error() << "failed to figure out type of file" << messaget::eom;
-        throw 0;
+        throw goto_model_initialization_errort("Failed to figure out type of file", location);
       }
 
       languaget &language=*lf.language;
@@ -91,8 +92,8 @@ goto_modelt initialize_goto_model(
 
       if(language.parse(infile, filename))
       {
-        msg.error() << "PARSING ERROR" << messaget::eom;
-        throw 0;
+        // FIXME not a super helpful message
+        throw goto_model_initialization_errort("PARSING ERROR");
       }
 
       lf.get_modules();
@@ -102,17 +103,17 @@ goto_modelt initialize_goto_model(
 
     if(language_files.typecheck(goto_model.symbol_table))
     {
-      msg.error() << "CONVERSION ERROR" << messaget::eom;
-      throw 0;
+      throw goto_model_initialization_errort("CONVERSION ERROR");
     }
   }
 
   for(const auto &file : binaries)
   {
     msg.status() << "Reading GOTO program from file" << messaget::eom;
 
-    if(read_object_and_link(file, goto_model, message_handler))
-      throw 0;
+    if(read_object_and_link(file, goto_model, message_handler)) {
+      throw goto_model_initialization_errort("failed to read object or link in file `" + file + '\'');
+    }
   }
 
   bool binaries_provided_start=
@@ -149,14 +150,13 @@ goto_modelt initialize_goto_model(
 
   if(entry_point_generation_failed)
   {
-    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
-    throw 0;
+    // FIXME more helpful error message?
+    throw goto_model_initialization_errort("SUPPORT FUNCTION GENERATION ERROR");
   }
 
   if(language_files.final(goto_model.symbol_table))
   {
-    msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
-    throw 0;
+    throw goto_model_initialization_errort("FINAL STAGE CONVERSION ERROR");
   }
 
   msg.status() << "Generating GOTO Program" << messaget::eom;
@@ -172,3 +172,22 @@ goto_modelt initialize_goto_model(
 
   return goto_model;
 }
+
+goto_model_initialization_errort::goto_model_initialization_errort(std::string message)
+  : goto_model_initialization_errort(std::move(message), source_locationt())
+{}
+
+std::string goto_model_initialization_errort::what() const noexcept {
+  std::string what_msg = message;
+  if(source_location.is_not_nil())
+  {
+    what_msg += "\nsource location: " + source_location.as_string();
+  }
+  return what_msg;
+}
+
+goto_model_initialization_errort::goto_model_initialization_errort(std::string message, source_locationt source_location)
+  : message(std::move(message)), source_location(std::move(source_location))
+{
+
+}

src/goto-programs/initialize_goto_model.h

@@ -16,6 +16,19 @@ Author: Daniel Kroening, [email protected]
 #include <util/cmdline.h>
 
 #include "goto_model.h"
+#include <string>
+#include <util/exception_utils.h>
+
+class goto_model_initialization_errort : public cprover_exceptiont
+{
+public:
+  explicit goto_model_initialization_errort(std::string message);
+  goto_model_initialization_errort(std::string message, source_locationt source_location);
+  std::string what() const noexcept override;
+private:
+  std::string message;
+  source_locationt source_location;
+};
 
 goto_modelt initialize_goto_model(
   const cmdlinet &cmdline,