Implementation of invalid user input exception

src/cbmc/bmc.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 #include <iostream>
 
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 
 #include <langapi/language_util.h>
@@ -296,9 +297,8 @@ void bmct::get_memory_model()
     memory_model=util_make_unique<memory_model_psot>(ns);
   else
   {
-    error() << "Invalid memory model " << mm
-            << " -- use one of sc, tso, pso" << eom;
-    throw "invalid memory model";
+    throw invalid_user_input_exceptiont(
+      "Invalid parameter " + mm, "--mm", "values of sc, tso, pso");
   }
 }
 

src/cbmc/bv_cbmc.cpp

@@ -9,16 +9,13 @@ Author: Daniel Kroening, [email protected]
 #include "bv_cbmc.h"
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/replace_expr.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;
-  }
+  DATA_INVARIANT(expr.operands().size() != 4,
+  	"waitfor expression is expected to have four operands");
 
   const exprt &old_cycle=expr.op0();
   const exprt &cycle_var=expr.op1();
@@ -27,12 +24,8 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
   const exprt new_cycle = make_free_bv_expr(expr.type());
 
   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;
-  }
+  bool successful_cast = to_integer(bound, bound_value);
+  INVARIANT(successful_cast, "waitfor bound must be a constant");
 
   {
     // constraint: new_cycle>=old_cycle

src/cbmc/cbmc_parse_options.cpp

@@ -67,7 +67,7 @@ Author: Daniel Kroening, [email protected]
 #include "version.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),
   messaget(ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION),
@@ -79,7 +79,7 @@ ::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),
   messaget(ui_message_handler),
   ui_message_handler(cmdline, "CBMC " CBMC_VERSION),

src/cbmc/cbmc_parse_options.h

@@ -78,7 +78,7 @@ class optionst;
 // clang-format on
 
 class cbmc_parse_optionst:
-  public parse_options_baset,
+  public parse_optionst,
   public xml_interfacet,
   public messaget
 {

src/cbmc/cbmc_solvers.cpp

@@ -14,9 +14,11 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 #include <memory>
+#include <string>
 
-#include <util/unicode.h>
+#include <util/exception_utils.h>
 #include <util/make_unique.h>
+#include <util/unicode.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
@@ -168,8 +170,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
   {
     if(solver==smt2_dect::solvert::GENERIC)
     {
-      error() << "please use --outfile" << eom;
-      throw 0;
+      throw invalid_user_input_exceptiont(
+        "Failed to provide a filename",
+        "--outfile",
+        "provide a filename with --outfile");
     }
 
     auto smt2_dec=
@@ -213,8 +217,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
 
     if(!*out)
     {
-      error() << "failed to open " << filename << eom;
-      throw 0;
+      throw invalid_user_input_exceptiont(
+        "Failed to open suggested file: " + filename, "--outfile");
     }
 
     auto smt2_conv=
@@ -237,20 +241,38 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
 
 void cbmc_solverst::no_beautification()
 {
-  if(options.get_bool_option("beautify"))
+  bool beautify = options.get_bool_option("beautify");
+
+  if(beautify)
   {
-    error() << "sorry, this solver does not support beautification" << eom;
-    throw 0;
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support beautification",
+      "--beautify");
   }
 }
 
 void cbmc_solverst::no_incremental_check()
 {
-  if(options.get_bool_option("all-properties") ||
-     options.get_option("cover")!="" ||
-     options.get_option("incremental-check")!="")
+  bool all_properties = options.get_bool_option("all-properties");
+  bool cover = options.get_option("cover") != "";
+  bool incremental_check = options.get_option("incremental-check") != "";
+
+  if(all_properties)
+  {
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support incremental solving",
+      "--all_properties");
+  }
+  else if(cover)
+  {
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support incremental solving",
+      "--cover");
+  }
+  else if(incremental_check)
   {
-    error() << "sorry, this solver does not support incremental solving" << eom;
-    throw 0;
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support incremental solving",
+      "--incremental-check");
   }
 }

src/cbmc/show_vcc.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/mode.h>
 #include <langapi/language_util.h>
 
+#include <util/exception_utils.h>
 #include <util/json.h>
 #include <util/json_expr.h>
 
@@ -143,7 +144,8 @@ void bmct::show_vcc()
   {
     of.open(filename);
     if(!of)
-      throw "failed to open file "+filename;
+      throw invalid_user_input_exceptiont(
+        "Failed to open file: " + filename, "--outfile");
   }
 
   std::ostream &out=have_file?of:std::cout;

src/util/exception_utils.h

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Fotis Koutoulakis, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_EXCEPTION_UTILS_H
+#define CPROVER_UTIL_EXCEPTION_UTILS_H
+
+#include <string>
+
+class invalid_user_input_exceptiont
+{
+  std::string reason;
+  std::string option;
+  std::string correct_input;
+
+public:
+  invalid_user_input_exceptiont(
+    std::string reason,
+    std::string option,
+    std::string correct_input = "")
+    : reason(reason), option(option), correct_input(correct_input)
+  {
+  }
+
+  std::string what() const noexcept
+  {
+    std::string res;
+    res += "\nInvalid User Input Exception\n";
+    res += "Option: " + option + "\n";
+    res += "Reason: " + reason;
+    // Print an optional correct usage message assuming correct input parameters have been passed
+    res += correct_input.empty() ? "\n" : " Try: " + correct_input + "\n";
+    return res;
+  }
+};
+
+#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

src/util/parse_options.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #include "cmdline.h"
+#include "exception_utils.h"
+#include "exit_codes.h"
 #include "signal_catcher.h"
 
 parse_options_baset::parse_options_baset(
@@ -82,3 +84,19 @@ banner_string(const std::string &front_end, const std::string &version)
   return "* *" + std::string(left_padding, ' ') + version_str +
          std::string(right_padding, ' ') + "* *";
 }
+
+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(invalid_user_input_exceptiont &e)
+  {
+  	message.error() << e.what() << messaget::eom;
+  	return CPROVER_EXIT_EXCEPTION;
+  }
+  return CPROVER_EXIT_SUCCESS;
+}

src/util/parse_options.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include "cmdline.h"
+#include "message.h"
 
 class parse_options_baset
 {
@@ -35,6 +36,25 @@ 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;
+};
+
 std::string
 banner_string(const std::string &front_end, const std::string &version);