Merge pull request #2703 from NlightNFotis/develop_cbmc_cleanup_rebase

Cleanup error handling of cbmc/ folder

Author: NlightNFotis

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>
@@ -214,9 +215,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", "try values of sc, tso, pso");
   }
 }
 

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;
 

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';

src/cbmc/cbmc_solvers.cpp

@@ -14,7 +14,9 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 #include <memory>
+#include <string>
 
+#include <util/exception_utils.h>
 #include <util/make_unique.h>
 #include <util/unicode.h>
 #include <util/version.h>
@@ -32,7 +34,8 @@ Author: Daniel Kroening, [email protected]
 /// \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::solvert> 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<smt2_dect>(
@@ -206,8 +211,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 file: " + filename, "--outfile");
     }
 
     auto smt2_conv = util_make_unique<smt2_convt>(
@@ -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");
   }
 }

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;
     }
 

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();

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);

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 \

src/util/exception_utils.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Exception helper utilities
+
+Author: Fotis Koutoulakis, [email protected]
+
+\*******************************************************************/
+
+#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;
+}

src/util/exception_utils.h

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+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
+{
+  /// 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

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(
@@ -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