Change the unstructured asserts to invalid_user_input_exceptions and preconditions/invariants.

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>
@@ -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", "Try values of sc, tso, pso");
   }
 }
 

src/cbmc/bmc_cover.cpp

@@ -241,8 +241,8 @@ bool bmc_covert::operator()()
     cover_goals.add(l);
   }
 
-  INVARIANT(
-    cover_goals.size() == goal_map.size(), "we add coverage for each goal");
+  INVARIANT(cover_goals.size() == goal_map.size(),
+    "we add coverage for each goal");
 
 
   status() << "Running " << solver.decision_procedure_text() << eom;

src/cbmc/bv_cbmc.cpp

@@ -9,16 +9,14 @@ 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 +25,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_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>
@@ -169,8 +171,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>(
@@ -212,8 +216,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>(
@@ -237,18 +241,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

@@ -70,13 +70,13 @@ class cbmc_solverst:public messaget
 
     prop_convt &prop_conv() const
     {
-      PRECONDITION(prop_conv_ptr!=nullptr);
+      PRECONDITION(prop_conv_ptr != nullptr);
       return *prop_conv_ptr;
     }
 
     propt &prop() const
     {
-      PRECONDITION(prop_ptr!=nullptr);
+      PRECONDITION(prop_ptr != nullptr);
       return *prop_ptr;
     }
 

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.cpp

@@ -15,6 +15,6 @@ std::string invalid_user_input_exceptiont::what() const noexcept
   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";
+  res += correct_input.empty() ? "\n" : correct_input + "\n";
   return res;
 }

src/util/exception_utils.h

@@ -13,8 +13,12 @@ Author: Fotis Koutoulakis, [email protected]
 
 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: