RFC: handling of fatal errors

src/cbmc/bv_cbmc.cpp

@@ -10,15 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/replace_expr.h>
+#include <util/exception_utils.h>
 
 bvt bv_cbmct::convert_waitfor(const exprt &expr)
 {
   if(expr.operands().size()!=4)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor expected to have four operands" << eom;
-    throw 0;
-  }
+    throw input_src_exceptiont(
+      expr.find_source_location(),
+      "waitfor expected to have four operands");
 
   exprt new_cycle;
   const exprt &old_cycle=expr.op0();
@@ -30,11 +29,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
 
   mp_integer bound_value;
   if(to_integer(bound, bound_value))
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor bound must be a constant" << eom;
-    throw 0;
-  }
+    throw input_src_exceptiont(
+      expr.find_source_location(),
+      "waitfor bound must be a constant");
 
   {
     // constraint: new_cycle>=old_cycle
@@ -135,11 +132,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
 bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr)
 {
   if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor_symbol expected to have one operand" << eom;
-    throw 0;
-  }
+    throw input_src_exceptiont(
+      expr.find_source_location(),
+      "waitfor_symbol expected to have one operand");
 
   exprt result;
   const exprt &bound=expr.op0();

src/cbmc/cbmc_parse_options.cpp

@@ -69,7 +69,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "xml_interface.h"
 
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
-  parse_options_baset(CBMC_OPTIONS, argc, argv),
+  parse_optionst(CBMC_OPTIONS, argc, argv, ui_message_handler),
   xml_interfacet(cmdline),
   language_uit(cmdline, ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION)
@@ -80,7 +80,8 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
   int argc,
   const char **argv,
   const std::string &extra_options):
-  parse_options_baset(CBMC_OPTIONS+extra_options, argc, argv),
+  parse_optionst(
+    CBMC_OPTIONS+extra_options, argc, argv, ui_message_handler),
   xml_interfacet(cmdline),
   language_uit(cmdline, ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION)

src/cbmc/cbmc_parse_options.h

@@ -72,7 +72,7 @@ class optionst;
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst:
-  public parse_options_baset,
+  public parse_optionst,
   public xml_interfacet,
   public language_uit
 {

src/cbmc/cbmc_solvers.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 
 #include <util/unicode.h>
+#include <util/exception_utils.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
@@ -205,10 +206,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
   if(filename=="")
   {
     if(solver==smt1_dect::solvert::GENERIC)
-    {
-      error() << "please use --outfile" << eom;
-      throw 0;
-    }
+      throw ui_exceptiont("please use --outfile");
 
     smt1_dect *smt1_dec=
       new smt1_dect(
@@ -244,10 +242,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt1(smt1_dect::solvert solver)
     #endif
 
     if(!out)
-    {
-      error() << "failed to open " << filename << eom;
-      throw 0;
-    }
+      throw system_exceptiont("failed to open "+filename);
 
     smt1_convt *smt1_conv=
       new smt1_convt(
@@ -273,10 +268,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
   if(filename=="")
   {
     if(solver==smt2_dect::solvert::GENERIC)
-    {
-      error() << "please use --outfile" << eom;
-      throw 0;
-    }
+      throw ui_exceptiont("please use --outfile");
 
     smt2_dect *smt2_dec=
       new smt2_dect(
@@ -318,10 +310,7 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
     #endif
 
     if(!*out)
-    {
-      error() << "failed to open " << filename << eom;
-      throw 0;
-    }
+      throw system_exceptiont("failed to open " +filename);
 
     smt2_convt *smt2_conv=
       new smt2_convt(
@@ -344,19 +333,14 @@ cbmc_solverst::solvert* cbmc_solverst::get_smt2(smt2_dect::solvert solver)
 void cbmc_solverst::no_beautification()
 {
   if(options.get_bool_option("beautify"))
-  {
-    error() << "sorry, this solver does not support beautification" << eom;
-    throw 0;
-  }
+    throw ui_exceptiont("sorry, this solver does not support beautification");
 }
 
 void cbmc_solverst::no_incremental_check()
 {
   if(options.get_bool_option("all-properties") ||
      options.get_option("cover")!="" ||
      options.get_option("incremental-check")!="")
-  {
-    error() << "sorry, this solver does not support incremental solving" << eom;
-    throw 0;
-  }
+    throw ui_exceptiont(
+      "sorry, this solver does not support incremental solving");
 }

src/cbmc/show_vcc.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/json.h>
 #include <util/json_expr.h>
+#include <util/exception_utils.h>
 
 void bmct::show_vcc_plain(std::ostream &out)
 {
@@ -150,7 +151,7 @@ void bmct::show_vcc()
   {
     of.open(filename);
     if(!of)
-      throw "failed to open file "+filename;
+      throw system_exceptiont("failed to open file "+filename);
   }
 
   std::ostream &out=have_file?of:std::cout;

src/util/exception_utils.h

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Peter Schrammel, peter.schrammel@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_EXCEPTION_UTILS_H
+#define CPROVER_UTIL_EXCEPTION_UTILS_H
+
+#include "invariant.h"
+
+/// A logic error to be used for OS-related errors (I/O etc)
+class system_exceptiont: public std::logic_error
+{
+public:
+  system_exceptiont(
+    const std::string &_reason):
+    std::logic_error(_reason)
+  {
+  }
+};
+
+/// A logic error to be used for user interface errors
+class ui_exceptiont: public std::logic_error
+{
+public:
+  ui_exceptiont(
+    const std::string &_reason):
+    std::logic_error(_reason)
+  {
+  }
+};
+
+/// A user interface exception with source locations
+class input_src_exceptiont: public ui_exceptiont
+{
+public:
+  input_src_exceptiont(
+    const source_locationt &_source_location,
+    const std::string &_reason):
+    ui_exceptiont(_reason),
+    source_location(_source_location)
+  {
+  }
+
+  source_locationt source_location;
+};
+
+#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

src/util/invariant_utils.h

@@ -6,8 +6,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 \*******************************************************************/
 
-#ifndef CPROVER_UTIL_INVARIANT_TYPES_H
-#define CPROVER_UTIL_INVARIANT_TYPES_H
+#ifndef CPROVER_UTIL_INVARIANT_UTILS_H
+#define CPROVER_UTIL_INVARIANT_UTILS_H
 
 #include "invariant.h"
 
@@ -45,4 +45,4 @@ std::string pretty_print_invariant_with_irep(
 #define DATA_INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP) \
   INVARIANT_WITH_IREP((CONDITION), (DESCRIPTION), (IREP))
 
-#endif
+#endif // CPROVER_UTIL_INVARIANT_UTILS_H

src/util/parse_options.cpp

@@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "parse_options.h"
+#include "exception_utils.h"
 
 #include <iostream>
 
@@ -65,3 +66,31 @@ int parse_options_baset::main()
 
   return doit();
 }
+
+int parse_optionst::main()
+{
+  // catch all exceptions here so that this code is not duplicated
+  // for each tool
+  try
+  {
+    return parse_options_baset::main();
+  }
+  catch(const system_exceptiont &e)
+  {
+    message.error() << e.what() << messaget::eom;
+  }
+  catch(const input_src_exceptiont &e)
+  {
+    message.error().source_location=e.source_location;
+    message.error() << e.what() << messaget::eom;
+  }
+  catch(const ui_exceptiont &e)
+  {
+    message.error() << e.what() << messaget::eom;
+  }
+  catch(const invariant_failedt &e)
+  {
+    message.error() << e.what() << messaget::eom;
+  }
+  return 6;
+}

src/util/parse_options.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 #include "cmdline.h"
+#include "message.h"
 
 class parse_options_baset
 {
@@ -35,4 +36,23 @@ class parse_options_baset
   bool parse_result;
 };
 
+class parse_optionst: public parse_options_baset
+{
+public:
+  parse_optionst(
+    const std::string &optstring,
+    int argc,
+    const char **argv,
+    message_handlert &message_handler):
+    parse_options_baset(optstring, argc, argv),
+    message(message_handler)
+  {
+  }
+
+  int main() override;
+
+protected:
+  messaget message;
+};
+
 #endif // CPROVER_UTIL_PARSE_OPTIONS_H