Cleanup error handling of cbmc/ folder #2703

NlightNFotis · 2018-08-09T16:02:01Z

Perform various cleanups of the error handling mechanisms in the src/cbmc/ folder. These include turning asserts into INVARIANTs and PRECONDITIONs as well as a new custom exception class.

martin-cs

Approve subject to addressing the comments.

martin-cs · 2018-08-09T16:22:49Z

src/cbmc/symex_coverage.cpp

  goto_programt::const_targett end_function=
    --gf_it->second.body.instructions.end();
-  assert(end_function->is_end_function());
+  INVARIANT(end_function->is_end_function(),


DATA_INVARIANT I think.

martin-cs · 2018-08-09T16:23:17Z

src/cbmc/symex_coverage.cpp

+    "Last instruction in a function body is end function");
  file_name=end_function->source_location.get_file();
-  assert(!file_name.empty());
+  INVARIANT(!file_name.empty(),


DATA_INVARIANT

src/cbmc/symex_coverage.cpp

martin-cs · 2018-08-09T16:28:30Z

src/util/parse_options.cpp

+  catch(invalid_user_input_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";
+    return CPROVER_EXIT_EXCEPTION;


CPROVER_EXIT_USAGE_ERROR ?

peterschrammel · 2018-08-09T21:45:21Z

src/cbmc/bmc_cover.cpp

  }

-  assert(cover_goals.size()==goal_map.size());
+  INVARIANT(cover_goals.size()==goal_map.size(),


apply clang-format

peterschrammel · 2018-08-09T21:45:50Z

src/cbmc/cbmc_main.cpp

+    int res = parse_options.main();

  #ifdef IREP_HASH_STATS
  std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n';


indentation

peterschrammel · 2018-08-09T21:47:13Z

src/util/exception_utils.h

+  std::string what() const noexcept
+  {
+    std::string res;
+    res += "\nInvalid User Input Exception\n";


I'd remove the word Exception.

peterschrammel · 2018-08-09T21:48:32Z

src/cbmc/cbmc_solvers.cpp

-    error() << "sorry, this solver does not support beautification" << eom;
-    throw 0;
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support beautification",


maybe this solver -> the chosen solver ? (same below)

And drop "sorry" - we don't apologise elsewhere either.

peterschrammel · 2018-08-09T21:51:49Z

src/util/parse_options.cpp

+  }
+  catch(invalid_user_input_exceptiont &e)
+  {
+    std::cerr << e.what() << "\n";


No. This must go into a message stream.

It was like this in the original design, but then I saw during rebasing on develop, that recently a similar change was eliminated, so I thought that it must have been that this is more appropriate. If I am also to do that now, I will need to add a messaget into parse_options_baset, which will require changes in various places

I found exactly what I was referring to. So parse_options_baset doesn't seem to inherit from messaget and doesn't contain a reference to a messaget. If I do this, then I get loads of compilation errors regarding ambiguous calls to things like status(), get_message_handler(), etc.

It's also consistent with the rest of the file. parse_options_baset::usage_error(), parse_options_baset::unknown_options_msg() seem to be following the same pattern of using std::cerr

At the risk of contradicting @peterschrammel: I don't think a message stream can be used here, because setting up the desired one requires successful parsing of command-line options (picking, e.g., JSON output with a verbosity of 5). Hence I'm with @NlightNFotis that using std::cerr is correct here.

peterschrammel · 2018-08-09T21:52:22Z

src/cbmc/cbmc_main.cpp

 int main(int argc, const char **argv)
 {
 #endif
-  try


Please squash this with the first commit that introduce the change that you undo here.

tautschnig

This looks like a good direction of work to me, but I'd suggest to make this as clean as possible unless there is a need to rush it in? If so, please break it apart into separate pull requests as the need for further discussion varies widely among the commits.

tautschnig · 2018-08-10T08:47:12Z

src/cbmc/bmc_cover.cpp


-  assert(cover_goals.size()==goal_map.size());
+  INVARIANT(cover_goals.size()==goal_map.size(),
+    "We add coverage for each goal");


The coding standard says that error messages start with a lower-case letter.

tautschnig · 2018-08-10T08:50:12Z

src/cbmc/symex_coverage.cpp

-        assert(cov.second.num_executions>0);
+        INVARIANT(cov.second.num_executions>0,
+          // FIXME I don't know what this means
+          "Number of executions most be positive");


Should be a PRECONDITION. A coverage entry can only exist when a location has actually been covered in at least one execution.

There's a problem with that, in that the PRECONDITION according to documentation should only contain unmodified arguments to a function, but I can change it, since it makes it easier to drop the message which appears incorrect as well.

You might use a DATA_INVARIANT, paraphrasing in the message what I said above (coverage entries can only exist with at least one execution).

tautschnig · 2018-08-10T08:53:10Z

src/cbmc/cbmc_main.cpp

+  catch(invalid_user_input_exceptiont &e)
+  {
+    std::cerr << e.what() << std::endl;
+  }


Design note: I don't think such an exception should propagate out of parse_options for the key task of parse_options is to parse options? If anything goes wrong it should and does return an error code. Having both error codes and exceptions seems wrong to me.

This is a comment on outdated code. The error handling is now being contained in parse_optionst::main(), and doesn't escape that context. parse_optionst::main() will indeed return an error code, that is is being handled in cbmc_main

Btw, it also appears that parse_optionst was mainly useful during the evolution of the code, but now that has been rebased, its usefulness has diminished, so I am trying to eliminate it.

tautschnig · 2018-08-10T08:55:02Z

src/util/exception_utils.h

+  {
+  }
+
+  std::string what() const noexcept


I don't think this should be a header-only class. Add a cpp file and move the implementation of at least this function over there. No need to inline it everywhere, will just unnecessarily increase the size of the binary.

src/cbmc/bmc.cpp

tautschnig · 2018-08-10T09:05:37Z

src/cbmc/cbmc_solvers.cpp

 void cbmc_solverst::no_beautification()
 {
-  if(options.get_bool_option("beautify"))
+  bool beautify = options.get_bool_option("beautify");


Why is this temporary introduced?

I remember I had a reason in the beginning but I may have refactored it enough that it's now unneeded.

tautschnig · 2018-08-10T09:06:12Z

src/cbmc/cbmc_solvers.cpp

-    error() << "sorry, this solver does not support beautification" << eom;
-    throw 0;
+    throw invalid_user_input_exceptiont(
+      "Sorry, this solver does not support beautification",


And drop "sorry" - we don't apologise elsewhere either.

tautschnig · 2018-08-10T09:06:36Z

src/cbmc/cbmc_solvers.cpp

-  if(options.get_bool_option("all-properties") ||
-     options.get_option("cover")!="" ||
-     options.get_option("incremental-check")!="")
+  bool all_properties = options.get_bool_option("all-properties");


const (here and below)

tautschnig · 2018-08-10T09:08:20Z

src/cbmc/cbmc_solvers.cpp

-     options.get_option("cover")!="" ||
-     options.get_option("incremental-check")!="")
+  bool all_properties = options.get_bool_option("all-properties");
+  bool cover = options.get_option("cover") != "";


While you're cleaning this up: use .is_set instead of get_option(...) != ""

tautschnig · 2018-08-10T09:11:46Z

src/util/parse_options.h

  bool parse_result;
 };

+class parse_optionst : public parse_options_baset


I'm not sure we need this derived class: can't it just be changed in parse_options_baset and make everyone benefit without changes?

This is not needed anymore. I have eliminated it.

danpoe · 2018-08-13T15:02:32Z

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
+    res += correct_input.empty() ? "\n" : " Try: " + correct_input + "\n";


The "Try: ..." portion should better be on a new line.

@tautschnig Suggested to drop the Try altogether, and just add in the various constructor callsites so that it reads more like a sentence.

NlightNFotis · 2018-08-24T10:41:19Z

@peterschrammel You have a red (blocker) cross applied to this. All your points have now been addressed. Can you take a look now and tell me if there's anything more you would want explained or changed?

NlightNFotis · 2018-08-24T10:42:27Z

@tautschnig Hi, can you also take a look to see if it's closer to what you expect? It's the same as before, but cleaned up and the changes suggested applied. The only extra is the last commit, which I thought makes sense to not be squashed, as it is a good atomic change (it replaces to_integer with numeric_cast).

src/cbmc/cbmc_parse_options.h

peterschrammel · 2018-08-28T09:48:53Z

src/cbmc/cbmc_main.cpp

 #endif
-  cbmc_parse_optionst parse_options(argc, argv);
+  try
+  {


This change is undone two commits later. Why is this change made at all?

peterschrammel · 2018-08-28T09:55:37Z

src/util/exception_utils.cpp

+
+#include "exception_utils.h"
+
+std::string invalid_user_input_exceptiont::what() const noexcept


Ideally, there should also be a version hat can serialise into json and XML in a more structure way (in a future PR).

peterschrammel · 2018-08-28T09:57:29Z

src/cbmc/bv_cbmc.cpp

-  }
+  DATA_INVARIANT(
+    expr.operands().size() != 4,
+    "waitfor expression is expected to have four operands");


@chrisr-diffblue, @martin-cs, the source location is lost here. Would it be possible to have variants of the INVARIANT macros that take a source location explicitly so that it can be output in a structured way?

peterschrammel · 2018-08-28T09:59:40Z

@NlightNFotis, the changes in f257667 that are later undone in 017c1b0 need to be removed.

tautschnig · 2018-09-04T10:13:41Z

Could this one please be rebased and cleaned up with regard to the comments raised by @peterschrammel - then it might be good to go.

NlightNFotis · 2018-09-04T10:20:16Z

@tautschnig Yes, this is waiting for us to decide on a clean way to create a more structured, "variadic" invariant, that can take a source_locationt and anything else we might want to decide to pass to it in the future - it's the last comment Peter made on his last review.

tautschnig · 2018-09-04T10:24:55Z

Yes, this is waiting for us to decide on a clean way to create a more structured, "variadic" invariant, that can take a source_locationt and anything else we might want to decide to pass to it in the future - it's the last comment Peter made on his last review.

Apart from the fact that the specific bit of code that @peterschrammel commented on is now gone from the repository: can't we just solve this by doing source_location.as_string()? I'm sure there are more beautiful ways of doing this, but perfection is the enemy of good. And here such decision-taking might just be blocking progress?

NlightNFotis · 2018-09-04T10:56:56Z

@tautschnig I have now rebased the PR and I'm waiting for CI to pass. Then it should be good to go. We decided to go ahead with this now and we can implement the structured invariants later.

tautschnig

There are still changes in the individual commits that just modify what was added in one of the other commits in this series. Some soft reset and the use of git add -p seems to be due.

src/cbmc/symex_coverage.cpp

tautschnig · 2018-09-04T10:58:51Z

src/cbmc/cbmc_solvers.h

    prop_convt &prop_conv() const
    {
-      assert(prop_conv_ptr!=nullptr);
+      PRECONDITION(prop_conv_ptr!=nullptr);


Nit pick: clang-format.

src/cbmc/symex_coverage.cpp

src/cbmc/cbmc_solvers.cpp

src/cbmc/cbmc_solvers.h

src/util/exception_utils.cpp

src/cbmc/cbmc_parse_options.h

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 3bd4322).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

…preconditions/invariants.

NlightNFotis · 2018-09-04T14:06:35Z

@tautschnig I have implemented all of the changes suggested in your comments, and Peter's comments (bar the structured invariant). I have also pinged Peter for a re-review. Can you take a look at it and green-light it if you think it's good to go?

tautschnig · 2018-09-04T14:13:32Z

src/cbmc/cbmc_solvers.h

    propt &prop() const
    {
-      PRECONDITION(prop_ptr!=nullptr);
+      PRECONDITION(prop_ptr != nullptr);


This is still in the wrong commit, fixing up a change from an earlier commit.

tautschnig · 2018-09-04T14:13:56Z

src/cbmc/cbmc_main.cpp

  cbmc_parse_optionst parse_options(argc, argv);

-  int res=parse_options.main();
+  int res = parse_options.main();


Unnecessary change?

tautschnig · 2018-09-04T14:14:57Z

src/util/exception_utils.cpp

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


Wishlist: please add a test for this, i.e., intentionally use CBMC with incorrect options.

Do you need this as part of this PR, or can it go in as part of a follow up PR for example?

Up to you, as long as it happens at some point :-)

We plan to make some further improvements to user error handling, so we'll definitely be adding suitable test cases as part of that work, so I'd be happy for this PR to go in, with tests following as part of the later improvements.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2e6d6a0).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

NlightNFotis self-assigned this Aug 9, 2018

NlightNFotis requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners August 9, 2018 16:02

martin-cs approved these changes Aug 9, 2018

View reviewed changes

peterschrammel requested changes Aug 9, 2018

View reviewed changes

tautschnig reviewed Aug 10, 2018

View reviewed changes

danpoe mentioned this pull request Aug 10, 2018

Replace function calls with calls to other functions #2705

Merged

danpoe reviewed Aug 13, 2018

View reviewed changes

danpoe mentioned this pull request Aug 20, 2018

Error handling cleanup in src/util (files starting with a-g) #2762

Merged

NlightNFotis force-pushed the develop_cbmc_cleanup_rebase branch 2 times, most recently from 3c9225c to f06cbea Compare August 24, 2018 10:39

peterschrammel requested changes Aug 28, 2018

View reviewed changes

NlightNFotis added the do not merge label Sep 4, 2018

NlightNFotis force-pushed the develop_cbmc_cleanup_rebase branch from f06cbea to 3bd4322 Compare September 4, 2018 10:51

tautschnig reviewed Sep 4, 2018

View reviewed changes

allredj reviewed Sep 4, 2018

View reviewed changes

hannes-steffenhagen-diffblue and others added 3 commits September 4, 2018 14:45

Convert assert calls to INVARIANTs

3372c22

Implementation of a erroneous user input exception class.

1b95a94

Change the unstructured asserts to invalid_user_input_exceptions and …

2e6d6a0

…preconditions/invariants.

NlightNFotis force-pushed the develop_cbmc_cleanup_rebase branch from 3bd4322 to 2e6d6a0 Compare September 4, 2018 13:45

peterschrammel approved these changes Sep 4, 2018

View reviewed changes

tautschnig approved these changes Sep 4, 2018

View reviewed changes

NlightNFotis merged commit b01d603 into diffblue:develop Sep 4, 2018

NlightNFotis removed the do not merge label Sep 4, 2018

allredj reviewed Sep 4, 2018

View reviewed changes

NlightNFotis mentioned this pull request Sep 5, 2018

Cleanup of asserts and throws under the goto-symex directory #2902

Merged


		#include "exception_utils.h"

		std::string invalid_user_input_exceptiont::what() const noexcept

Cleanup error handling of cbmc/ folder #2703

Cleanup error handling of cbmc/ folder #2703

Uh oh!

Conversation

NlightNFotis commented Aug 9, 2018

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Aug 24, 2018

Uh oh!

NlightNFotis commented Aug 24, 2018

Uh oh!

Uh oh!

Choose a reason for hiding this comment