diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 9a01fa233ec..0bb68a80439 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -214,9 +215,8 @@ void bmct::get_memory_model() memory_model=util_make_unique(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", "try values of sc, tso, pso"); } } diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 53fbd50f491..3bb617e7bd1 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -219,7 +219,7 @@ bool bmc_covert::operator()() { if(it->is_assert()) { - assert(it->source.pc->is_assert()); + PRECONDITION(it->source.pc->is_assert()); const and_exprt c( literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal)); literalt l_c=solver.convert(c); @@ -239,7 +239,9 @@ bool bmc_covert::operator()() cover_goals.add(l); } - assert(cover_goals.size()==goal_map.size()); + INVARIANT(cover_goals.size() == goal_map.size(), + "we add coverage for each goal"); + status() << "Running " << solver.decision_procedure_text() << eom; diff --git a/src/cbmc/cbmc_main.cpp b/src/cbmc/cbmc_main.cpp index bcf6c764c68..b96923910f3 100644 --- a/src/cbmc/cbmc_main.cpp +++ b/src/cbmc/cbmc_main.cpp @@ -43,7 +43,7 @@ int main(int argc, const char **argv) #endif cbmc_parse_optionst parse_options(argc, argv); - int res=parse_options.main(); + int res = parse_options.main(); #ifdef IREP_HASH_STATS std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n'; diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp index 2cbd8cb1ff5..fe1d40179aa 100644 --- a/src/cbmc/cbmc_solvers.cpp +++ b/src/cbmc/cbmc_solvers.cpp @@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include #include @@ -32,7 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \return An smt2_dect::solvert giving the solver to use. smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const { - assert(options.get_bool_option("smt2")); + // we shouldn't get here if this option isn't set + PRECONDITION(options.get_bool_option("smt2")); smt2_dect::solvert s=smt2_dect::solvert::GENERIC; @@ -163,8 +166,10 @@ std::unique_ptr cbmc_solverst::get_smt2( { if(solver==smt2_dect::solvert::GENERIC) { - error() << "please use --outfile" << eom; - throw 0; + throw invalid_user_input_exceptiont( + "required filename not provided", + "--outfile", + "provide a filename with --outfile"); } auto smt2_dec = util_make_unique( @@ -206,8 +211,8 @@ std::unique_ptr cbmc_solverst::get_smt2( if(!*out) { - error() << "failed to open " << filename << eom; - throw 0; + throw invalid_user_input_exceptiont( + "failed to open file: " + filename, "--outfile"); } auto smt2_conv = util_make_unique( @@ -231,18 +236,32 @@ void cbmc_solverst::no_beautification() { if(options.get_bool_option("beautify")) { - error() << "sorry, this solver does not support beautification" << eom; - throw 0; + throw invalid_user_input_exceptiont( + "the chosen 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")!="") + const bool all_properties = options.get_bool_option("all-properties"); + const bool cover = options.is_set("cover"); + const bool incremental_check = options.is_set("incremental-check"); + + if(all_properties) + { + throw invalid_user_input_exceptiont( + "the chosen solver does not support incremental solving", + "--all_properties"); + } + else if(cover) + { + throw invalid_user_input_exceptiont( + "the chosen 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( + "the chosen solver does not support incremental solving", + "--incremental-check"); } } diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index 5e458b32368..54bf3805e30 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -68,13 +68,13 @@ class cbmc_solverst:public messaget prop_convt &prop_conv() const { - assert(prop_conv_ptr!=nullptr); + PRECONDITION(prop_conv_ptr != nullptr); return *prop_conv_ptr; } propt &prop() const { - assert(prop_ptr!=nullptr); + PRECONDITION(prop_ptr != nullptr); return *prop_ptr; } diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index ec3cbd91250..8df3fcbd61f 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -81,7 +81,7 @@ fault_localizationt::get_failed_property() bool fault_localizationt::check(const lpointst &lpoints, const lpoints_valuet &value) { - assert(value.size()==lpoints.size()); + PRECONDITION(value.size() == lpoints.size()); bvt assumptions; lpoints_valuet::const_iterator v_it=value.begin(); for(const auto &l : lpoints) @@ -142,7 +142,7 @@ void fault_localizationt::run(irep_idt goal_id) { // find failed property failed=get_failed_property(); - assert(failed!=bmc.equation.SSA_steps.end()); + PRECONDITION(failed != bmc.equation.SSA_steps.end()); if(goal_id==ID_nil) goal_id=failed->source.pc->source_location.get_property_id(); diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index ddef86378d9..840f4de5fc1 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -139,15 +139,17 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( const symex_coveraget::coveraget &coverage): coverage_recordt("method") { - assert(gf_it->second.body_available()); + PRECONDITION(gf_it->second.body_available()); // identify the file name, inlined functions aren't properly // accounted for goto_programt::const_targett end_function= --gf_it->second.body.instructions.end(); - assert(end_function->is_end_function()); + DATA_INVARIANT( + end_function->is_end_function(), + "last instruction in a function body is end function"); file_name=end_function->source_location.get_file(); - assert(!file_name.empty()); + DATA_INVARIANT(!file_name.empty(), "should have a valid source location"); // compute the maximum coverage of individual source-code lines coverage_lines_mapt coverage_lines_map; @@ -260,11 +262,15 @@ void goto_program_coverage_recordt::compute_coverage_lines( for(const auto &cov : c_entry->second) std::cerr << cov.second.succ->location_number << '\n'; } - assert(c_entry->second.size()==1 || is_branch); + DATA_INVARIANT( + c_entry->second.size() == 1 || is_branch, + "instructions other than branch instructions have exactly 1 successor"); for(const auto &cov : c_entry->second) { - assert(cov.second.num_executions>0); + DATA_INVARIANT( + cov.second.num_executions > 0, + "coverage entries can only exist with at least one execution"); if(entry.first->second.hits==0) ++lines_covered; @@ -275,7 +281,9 @@ void goto_program_coverage_recordt::compute_coverage_lines( if(is_branch) { auto cond_entry=entry.first->second.conditions.find(it); - assert(cond_entry!=entry.first->second.conditions.end()); + INVARIANT( + cond_entry != entry.first->second.conditions.end(), + "branch should have condition"); if(it->get_target()==cov.second.succ) { @@ -439,7 +447,7 @@ bool symex_coveraget::generate_report( const goto_functionst &goto_functions, const std::string &path) const { - assert(!path.empty()); + PRECONDITION(!path.empty()); if(path=="-") return output_report(goto_functions, std::cout); diff --git a/src/util/Makefile b/src/util/Makefile index c1cb652c959..d19524cd81c 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -13,6 +13,7 @@ SRC = arith_tools.cpp \ expr.cpp \ expr_initializer.cpp \ expr_util.cpp \ + exception_utils.cpp \ file_util.cpp \ find_macros.cpp \ find_symbols.cpp \ diff --git a/src/util/exception_utils.cpp b/src/util/exception_utils.cpp new file mode 100644 index 00000000000..148ddc742cd --- /dev/null +++ b/src/util/exception_utils.cpp @@ -0,0 +1,20 @@ +/*******************************************************************\ + +Module: Exception helper utilities + +Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com + +\*******************************************************************/ + +#include "exception_utils.h" + +std::string invalid_user_input_exceptiont::what() const noexcept +{ + std::string res; + res += "\nInvalid User Input\n"; + res += "Option: " + option + "\n"; + res += "Reason: " + reason; + // Print an optional correct usage message assuming correct input parameters have been passed + res += correct_input + "\n"; + return res; +} diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h new file mode 100644 index 00000000000..4c871b94fbf --- /dev/null +++ b/src/util/exception_utils.h @@ -0,0 +1,36 @@ +/*******************************************************************\ + +Module: Exception helper utilities + +Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_EXCEPTION_UTILS_H +#define CPROVER_UTIL_EXCEPTION_UTILS_H + +#include + +class invalid_user_input_exceptiont +{ + /// The reason this exception was generated. + std::string reason; + /// The full command line option (not the argument) that got + /// erroneous input. + std::string option; + /// In case we have samples of correct input to the 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; +}; + +#endif // CPROVER_UTIL_EXCEPTION_UTILS_H diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 2428c236889..b5a1b7e9b1f 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( @@ -47,23 +49,34 @@ void parse_options_baset::unknown_option_msg() int parse_options_baset::main() { - if(parse_result) + // catch all exceptions here so that this code is not duplicated + // for each tool + try { - usage_error(); - unknown_option_msg(); - return EX_USAGE; + if(parse_result) + { + usage_error(); + unknown_option_msg(); + return EX_USAGE; + } + + if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help")) + { + help(); + return EX_OK; + } + + // install signal catcher + install_signal_catcher(); + + return doit(); } - - if(cmdline.isset('?') || cmdline.isset('h') || cmdline.isset("help")) + catch(invalid_user_input_exceptiont &e) { - help(); - return EX_OK; + std::cerr << e.what() << "\n"; + return CPROVER_EXIT_USAGE_ERROR; } - - // install signal catcher - install_signal_catcher(); - - return doit(); + return CPROVER_EXIT_SUCCESS; } std::string