Change the unstructured asserts to invalid_user_input_exceptions and preconditions/invariants.

NlightNFotis · NlightNFotis · commit 2e6d6a0eb910 · 2018-09-04T14:45:31.000+01:00
diff --git 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>
@@ -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");
   }
 }
 
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -239,8 +239,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;
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
@@ -14,7 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #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>
@@ -164,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>(
@@ -207,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>(
@@ -232,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
@@ -68,13 +68,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;
     }
 
diff --git a/src/util/exception_utils.h b/src/util/exception_utils.h
@@ -13,8 +13,12 @@ Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
 
 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:

Original file line number	Diff line number	Diff line change
`@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]`
`14`	`14`	`#include <chrono>`
`15`	`15`	`#include <iostream>`
`16`	`16`
	`17`	`+#include <util/exception_utils.h>`
`17`	`18`	`#include <util/exit_codes.h>`
`18`	`19`
`19`	`20`	`#include <langapi/language_util.h>`
`@@ -214,9 +215,8 @@ void bmct::get_memory_model()`
`214`	`215`	`memory_model=util_make_unique<memory_model_psot>(ns);`
`215`	`216`	`else`
`216`	`217`	`{`
`217`		`- error() << "Invalid memory model " << mm`
`218`		`- << " -- use one of sc, tso, pso" << eom;`
`219`		`- throw "invalid memory model";`
	`218`	`+ throw invalid_user_input_exceptiont(`
	`219`	`+ "invalid parameter " + mm, "--mm", "try values of sc, tso, pso");`
`220`	`220`	`}`
`221`	`221`	`}`
`222`	`222`
Original file line number	Diff line number	Diff line change
`@@ -239,8 +239,8 @@ bool bmc_covert::operator()()`
`239`	`239`	`cover_goals.add(l);`
`240`	`240`	`}`
`241`	`241`
`242`		`- INVARIANT(`
`243`		`- cover_goals.size() == goal_map.size(), "we add coverage for each goal");`
	`242`	`+ INVARIANT(cover_goals.size() == goal_map.size(),`
	`243`	`+ "we add coverage for each goal");`
`244`	`244`
`245`	`245`
`246`	`246`	`status() << "Running " << solver.decision_procedure_text() << eom;`
Original file line number	Diff line number	Diff line change
`@@ -14,7 +14,9 @@ Author: Daniel Kroening, [email protected]`
`14`	`14`	`#include <fstream>`
`15`	`15`	`#include <iostream>`
`16`	`16`	`#include <memory>`
	`17`	`+#include <string>`
`17`	`18`
	`19`	`+#include <util/exception_utils.h>`
`18`	`20`	`#include <util/make_unique.h>`
`19`	`21`	`#include <util/unicode.h>`
`20`	`22`	`#include <util/version.h>`
`@@ -164,8 +166,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`164`	`166`	`{`
`165`	`167`	`if(solver==smt2_dect::solvert::GENERIC)`
`166`	`168`	`{`
`167`		`- error() << "please use --outfile" << eom;`
`168`		`- throw 0;`
	`169`	`+ throw invalid_user_input_exceptiont(`
	`170`	`+ "required filename not provided",`
	`171`	`+ "--outfile",`
	`172`	`+ "provide a filename with --outfile");`
`169`	`173`	`}`
`170`	`174`
`171`	`175`	`auto smt2_dec = util_make_unique<smt2_dect>(`
`@@ -207,8 +211,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(`
`207`	`211`
`208`	`212`	`if(!*out)`
`209`	`213`	`{`
`210`		`- error() << "failed to open " << filename << eom;`
`211`		`- throw 0;`
	`214`	`+ throw invalid_user_input_exceptiont(`
	`215`	`+ "failed to open file: " + filename, "--outfile");`
`212`	`216`	`}`
`213`	`217`
`214`	`218`	`auto smt2_conv = util_make_unique<smt2_convt>(`
`@@ -232,18 +236,32 @@ void cbmc_solverst::no_beautification()`
`232`	`236`	`{`
`233`	`237`	`if(options.get_bool_option("beautify"))`
`234`	`238`	`{`
`235`		`- error() << "sorry, this solver does not support beautification" << eom;`
`236`		`- throw 0;`
	`239`	`+ throw invalid_user_input_exceptiont(`
	`240`	`+ "the chosen solver does not support beautification", "--beautify");`
`237`	`241`	`}`
`238`	`242`	`}`
`239`	`243`
`240`	`244`	`void cbmc_solverst::no_incremental_check()`
`241`	`245`	`{`
`242`		`- if(options.get_bool_option("all-properties") \|\|`
`243`		`- options.get_option("cover")!="" \|\|`
`244`		`- options.get_option("incremental-check")!="")`
	`246`	`+ const bool all_properties = options.get_bool_option("all-properties");`
	`247`	`+ const bool cover = options.is_set("cover");`
	`248`	`+ const bool incremental_check = options.is_set("incremental-check");`
	`249`	`+`
	`250`	`+ if(all_properties)`
	`251`	`+ {`
	`252`	`+ throw invalid_user_input_exceptiont(`
	`253`	`+ "the chosen solver does not support incremental solving",`
	`254`	`+ "--all_properties");`
	`255`	`+ }`
	`256`	`+ else if(cover)`
	`257`	`+ {`
	`258`	`+ throw invalid_user_input_exceptiont(`
	`259`	`+ "the chosen solver does not support incremental solving", "--cover");`
	`260`	`+ }`
	`261`	`+ else if(incremental_check)`
`245`	`262`	`{`
`246`		`- error() << "sorry, this solver does not support incremental solving" << eom;`
`247`		`- throw 0;`
	`263`	`+ throw invalid_user_input_exceptiont(`
	`264`	`+ "the chosen solver does not support incremental solving",`
	`265`	`+ "--incremental-check");`
`248`	`266`	`}`
`249`	`267`	`}`
Original file line number	Diff line number	Diff line change
`@@ -68,13 +68,13 @@ class cbmc_solverst:public messaget`
`68`	`68`
`69`	`69`	`prop_convt &prop_conv() const`
`70`	`70`	`{`
`71`		`- PRECONDITION(prop_conv_ptr!=nullptr);`
	`71`	`+ PRECONDITION(prop_conv_ptr != nullptr);`
`72`	`72`	`return *prop_conv_ptr;`
`73`	`73`	`}`
`74`	`74`
`75`	`75`	`propt &prop() const`
`76`	`76`	`{`
`77`		`- PRECONDITION(prop_ptr!=nullptr);`
	`77`	`+ PRECONDITION(prop_ptr != nullptr);`
`78`	`78`	`return *prop_ptr;`
`79`	`79`	`}`
`80`	`80`