diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 5865f49f154..0a75c2d5d5c 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
#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");
}
}
diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp
index 019982f6fd7..faa0160bc27 100644
--- a/src/cbmc/bv_cbmc.cpp
+++ b/src/cbmc/bv_cbmc.cpp
@@ -9,16 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
#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
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index b5ea4553f17..b52f0001b4c 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -67,7 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com
#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),
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 24204c061b4..326ee7c0319 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/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
{
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 8b216839f92..29ddcea3335 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -14,9 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
#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");
}
}
diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
index 6a5b051cff9..677b33921c4 100644
--- a/src/cbmc/show_vcc.cpp
+++ b/src/cbmc/show_vcc.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
#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;
diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h
new file mode 100644
index 00000000000..73938fe1826
--- /dev/null
+++ b/src/util/exception_utils.h
@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
+
+\*******************************************************************/
+
+#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
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
index 2428c236889..08ddb7c00be 100644
--- a/src/util/parse_options.cpp
+++ b/src/util/parse_options.cpp
@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
#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;
+}
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
index 6b2b982fd51..cb210b96277 100644
--- a/src/util/parse_options.h
+++ b/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,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);