Implementation of invalid user input exception #5

NlightNFotis · 2018-07-02T12:36:16Z

This PR contains an implementation of an erroneous user input exception, and changes the unstructured throw 0s in the cbmc/ folder into structured exceptions and preconditions/invariants.

hannes-steffenhagen-diffblue

LGTM for the most part

hannes-steffenhagen-diffblue · 2018-07-02T14:00:05Z

src/cbmc/cbmc_solvers.cpp

+    throw invalid_user_input_exceptiont(
+      "Reason: sorry, this solver does not support incremental solving",
+      "--incremental-check",
+      "");


This is quite a big improvement over the previous version that didn't tell you what option it didn't like, 👍

hannes-steffenhagen-diffblue · 2018-07-02T14:02:22Z

src/util/exception_utils.h

+    std::string res;
+    res += "\nInvalid User Input Exception\n";
+    res += "Option: " + option + "\n";
+    res += reason;


I think it's fine to have the "Reason: " part here, I just didn't like forcing the form of the part after the reason.
Sorry for being unclear with this

danpoe · 2018-07-03T10:20:46Z

src/cbmc/bv_cbmc.cpp

-    error() << "waitfor expected to have four operands" << eom;
-    throw 0;
-  }
+  PRECONDITION(expr.operands().size() != 4);


We could use DATA_INVARIANT here which is for checking whether goto programs, exprts, etc. are well-formed. Then we can also keep the error message.

I won't implement this. It's easily implementable, but the error message is just redundant IMO. It doesn't convey any information that the precondition expression doesn't convey already. It just duplicates semantic information about the behaviour of the code.

Hm the error message had the additional information that expr is a wait-for expression (i.e., expr.id() is "waitfor"). From the condition we only see that it is some expression with four operands.

Good spot, didn't notice that. I guess I can rewrite that a little bit as well.

danpoe · 2018-07-03T10:57:21Z

src/cbmc/show_vcc.cpp

@@ -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 suggested file", "--outfile", "");


We can drop "suggested", and append the filename to the first argument.

danpoe · 2018-07-03T10:58:24Z

src/util/exception_utils.h

+  invalid_user_input_exceptiont(
+    std::string reason,
+    std::string option,
+    std::string correct_input)


Can we have an empty string default argument for correct_input?

danpoe · 2018-07-03T10:59:30Z

src/util/exception_utils.h

+    res += "Option: " + option + "\n";
+    res += "Reason: " + reason;
+    // Print an optional correct usage message assuming correct input parameters have been passed
+    correct_input.empty() ? "\n" : res += " Try: " + correct_input + "\n";


I think we need to add a newline before " Try".

I'd rather it be kept on the same line.

Should we add a separator character then? Maybe a comma.

danpoe · 2018-07-03T11:02:30Z

src/cbmc/cbmc_main.cpp

@@ -52,4 +58,9 @@ int main(int argc, const char **argv)
  #endif

  return res;
+  }
+  catch(invalid_user_input_exceptiont &e)


Currently if an exception is caught here the program still exits with a zero exit code. We should change this to exit with an error code.

I think we can also move the exception catching code to parse_options_baset::main() (wrapping the call to doit()). Then the tools that inherit from it don't need to repeat the exception handlers.

This is very interesting. It's a great suggestion, but this needs a little bit thinking about how to properly implement this (I haven't thought it through yet, might be easier than I realise)

NlightNFotis · 2018-07-03T15:43:57Z

@hannes-steffenhagen-diffblue @danpoe Can I request a new review from both of you? Made some substantial changes on where we handle exceptions in the latest commit.

danpoe · 2018-07-04T15:04:42Z

src/cbmc/cbmc_main.cpp

@@ -25,6 +25,10 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif

+#include <iostream>
+
+#include <util/exception_utils.h>


I think those two includes are now not needed anymore.

danpoe · 2018-07-04T15:05:55Z

src/cbmc/show_vcc.cpp

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


... file" -> ...file "

…preconditions/invariants.

danpoe

Looks good to me!

hannes-steffenhagen-diffblue · 2018-07-04T15:21:26Z

src/cbmc/show_vcc.cpp

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


Thinking about it, I don't really like this being an invalid user input exception (I suppose you can justify it being subject to user input as they control the filename, but technically whether or not we're able to open the file isn't necessarily up to the user).

Not a blocker for sure, but in general I'd have a preference for IO related exceptions to have their own place.

hannes-steffenhagen-diffblue

Still looks OK to me

…tion

hannes-steffenhagen-diffblue approved these changes Jul 2, 2018

View reviewed changes

NlightNFotis force-pushed the custom_exception branch from 4ffe61a to 5a1d8b6 Compare July 3, 2018 08:51

danpoe suggested changes Jul 3, 2018

View reviewed changes

NlightNFotis force-pushed the custom_exception branch from 5a1d8b6 to b8bb108 Compare July 3, 2018 15:43

NlightNFotis force-pushed the custom_exception branch from b8bb108 to c952a8a Compare July 4, 2018 10:14

danpoe reviewed Jul 4, 2018

View reviewed changes

NlightNFotis added 2 commits July 4, 2018 16:14

Implementation of a erroneous user input exception class.

4fb727c

Change the unstructured commits to invalid_user_input_exceptions and …

662f90a

…preconditions/invariants.

NlightNFotis force-pushed the custom_exception branch from c952a8a to 6f3f888 Compare July 4, 2018 15:14

danpoe approved these changes Jul 4, 2018

View reviewed changes

hannes-steffenhagen-diffblue reviewed Jul 4, 2018

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Jul 4, 2018

View reviewed changes

Add a parse_options class for a better suited exception handling loca…

0248d40

…tion

NlightNFotis force-pushed the custom_exception branch from 6f3f888 to 0248d40 Compare July 6, 2018 09:09

chrisr-diffblue approved these changes Jul 17, 2018

View reviewed changes

chrisr-diffblue merged commit 8c4eb38 into chrisr-diffblue:cbmc-bookworm Jul 17, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implementation of invalid user input exception #5

Implementation of invalid user input exception #5

NlightNFotis commented Jul 2, 2018

hannes-steffenhagen-diffblue left a comment

hannes-steffenhagen-diffblue Jul 2, 2018

hannes-steffenhagen-diffblue Jul 2, 2018

danpoe Jul 3, 2018

NlightNFotis Jul 3, 2018 •

edited

Loading

danpoe Jul 3, 2018 •

edited

Loading

NlightNFotis Jul 3, 2018

danpoe Jul 3, 2018

danpoe Jul 3, 2018

danpoe Jul 3, 2018

NlightNFotis Jul 3, 2018

danpoe Jul 3, 2018

danpoe Jul 3, 2018

NlightNFotis Jul 3, 2018

NlightNFotis commented Jul 3, 2018

danpoe Jul 4, 2018 •

edited

Loading

danpoe Jul 4, 2018

danpoe left a comment

hannes-steffenhagen-diffblue Jul 4, 2018

hannes-steffenhagen-diffblue left a comment

Implementation of invalid user input exception #5

Implementation of invalid user input exception #5

Conversation

NlightNFotis commented Jul 2, 2018

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis Jul 3, 2018 • edited Loading

Choose a reason for hiding this comment

danpoe Jul 3, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented Jul 3, 2018

danpoe Jul 4, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

NlightNFotis Jul 3, 2018 •

edited

Loading

danpoe Jul 3, 2018 •

edited

Loading

danpoe Jul 4, 2018 •

edited

Loading