Improved invariants #1063

smowton · 2017-06-27T10:03:14Z

Based on recent discussions about the shortcomings of the INVARIANT family of macros, here are some improvements:

Most importantly, invariants can now be structured. INVARIANT(false, "Hello world") still works and produces an invariant_failedt as before, but one can also derive from invariant_failedt, add fields to describe an error in a more useful way, and override pretty_print to render them into a human-readable error message. This means that even before catching invariants becomes allowed practice we can be producing structured invariants ready for if and when that changes. The update to tests demonstrates this feature in use.
For consistency, the throw / abort behaviour of invariants is no longer dependent on compile-time conditional definitions; it will now function one way and do that dependably on both development and production builds, hopefully reducing the chance of a surprise in production. Currently it always aborts owing to @martin-cs concerns that a catch(...) may accidentally swallow in invariant it didn't mean to.
(Incidental) the reason expression, whether structured or a simple string, is now lazily evaluated (e.g. INVARIANT(x==y, str1+str2) will only perform the string concatenation if the test fails).

Please get in there now with your design concerns rather than objecting to down-the-line PRs that use these features!

smowton · 2017-06-27T10:04:57Z

@NathanJPhillips requested review also (can't do it formally for some reason)

thk123 · 2017-06-27T10:09:49Z

src/util/invariant.cpp

-/// \param reason : C string giving the reason why the invariant should be true.
-void check_invariant(
+/// \param out: Stream to print backtrace
+void print_backtrace(


I appreciate this should have gone in a previous review - but I notice the backtrace only happens under glibc. Given that we currently run the DB platform on musl based platform this seems like not a good limitation

afaik, all images have been moved to debian in the meantime

This solution works on gcc and Windows: http://stacktrace.sourceforge.net/
Even if you don't use it it might be worth adding a comment mentioning it in the #else section below.

The eternal question of external deps. I'll leave this for subsequent work.

peterschrammel · 2017-06-27T12:30:32Z

src/cbmc/cbmc_parse_options.cpp

@@ -97,6 +97,31 @@ void cbmc_parse_optionst::eval_verbosity()
  ui_message_handler.set_verbosity(v);
 }

+/// An example of structured invariants-- this contains fields to


I'd suggest to put these tests into a unit test instead of cluttering the tool.

Was just copying the existing clutter :) but I agree will move

peterschrammel · 2017-06-27T12:32:22Z

src/util/invariant.cpp

-/// \param reason : C string giving the reason why the invariant should be true.
-void check_invariant(
+/// \param out: Stream to print backtrace
+void print_backtrace(


afaik, all images have been moved to debian in the meantime

peterschrammel · 2017-06-27T12:33:45Z

src/util/invariant.h

-  explicit invariant_failedt(const std::string& what) : logic_error(what) {}
-  explicit invariant_failedt(const char* what) : logic_error(what) {}
+  invariant_failedt(
+    const std::string& what):


peterschrammel · 2017-06-27T12:34:05Z

src/util/invariant.h

-  explicit invariant_failedt(const char* what) : logic_error(what) {}
+  invariant_failedt(
+    const std::string& what):
+  logic_error(what),


peterschrammel · 2017-06-27T12:35:14Z

src/util/invariant.h

+  }
+
+  /// Stores the backtrace set by `invariant_violated`.
+  std::string backtrace;


maybe make protected?

peterschrammel · 2017-06-27T12:37:14Z

src/util/invariant.h

+  }
+
+  /// Temporary storage for `what`'s return value
+  mutable std::string what_str;


why can't this be declared locally?

The string needs to live beyond the lifespan of what(). It's a bad interface; the docs for std::logic_error admit as much, but I'd rather produce this on demand than inevitably have some derived class mutator forget to update it.

Ah. I see. exception::what returns a pointer.

peterschrammel · 2017-06-27T12:40:43Z

src/util/invariant.h

@@ -10,6 +10,8 @@ Author: Martin Brain, [email protected]
 #define CPROVER_UTIL_INVARIANT_H

 #include <stdexcept>
+#include <type_traits>
+#include <iostream>

 /*
 ** Invariants document conditions that the programmer believes to


/* */ should not be used

smowton · 2017-06-27T15:41:16Z

Applied @peterschrammel changes except for moving the tests, which needs me to understand how unit tests are being done...

thk123 · 2017-06-28T09:10:17Z

@smowton as discussed, since you want to check the output of stderr you probably are best using a driver program inside the regressions folder.

However, if you would also like to write a unit test (e.g. to check that under default builds, INVARIANT(false, "hello") throws an exception):

Example unit tests from variable sensitivity domain
Documentation from coding standards
Catch (the unit testing framework) documentation

thk123 · 2017-06-28T09:15:33Z

src/util/invariant.h

+/// \param reason : (derived from invariant_failedt) error report structure;
+///  its backtrace member will be set before it is used.
+template<class T>
+typename std::enable_if<std::is_base_of<invariant_failedt, T>::value>::type


Is there a reason to use templates here rather than just const invariant_failedt & Unless I'm not understanding something, this will only compile with children of invariant_failedt

Oh I see - there is some magic to make different methods exist if the type is a string or a invariant_failedt. Can this not be done through regular method overloading, one that takes an const invariant_failedt & and one that takes const std::string &?

Actually I think it probably could work like that in this case. Either taking a const invariant_failedt & and then copying it to a temporary or else taking an invariant_failedt & and having it in the contract that it will be updated with the stacktrace.

I took the true type because when we throw them we'll want to throw the actual type. If I throw an invariant_failedt & then I will attempt to copy-construct an invariant_failedt at the throw site (throws are by value). Such a copy constructor would discard information.

Oh I see - I didn't know that. I suppose this is cleaner than a virtual clone method on invariant_failedt

NathanJPhillips · 2017-06-28T09:22:53Z

src/util/invariant.cpp

-/// \param reason : C string giving the reason why the invariant should be true.
-void check_invariant(
+/// \param out: Stream to print backtrace
+void print_backtrace(


This solution works on gcc and Windows: http://stacktrace.sourceforge.net/
Even if you don't use it it might be worth adding a comment mentioning it in the #else section below.

NathanJPhillips · 2017-06-28T09:24:19Z

src/util/invariant.h

 class invariant_failedt: public std::logic_error
 {
+  /// Stores the backtrace set by `invariant_violated`.


Normally I would explicitly write private: rather than relying on the default in case someone adds something public above.

NathanJPhillips · 2017-06-28T09:25:02Z

src/util/invariant.h

+  invariant_failedt(
+    const std::string &what):
+    logic_error(what),
+    backtrace()


Unnecessary call to default constructor.

NathanJPhillips · 2017-06-28T09:33:28Z

src/util/invariant.h

+  { \
+  if(!(CONDITION)) \
+    invariant_violated(__FILE__, __FUNCTION__, __LINE__, (REASON)); \
+  } while(0)


Presumably this is to make a statement that requires a trailing semicolon to make INVARIANT behave syntactically as much like a normal function as possible. If so, a comment saying so would be helpful.

NathanJPhillips · 2017-06-28T09:41:06Z

src/util/invariant.h

+/// \param reason : (derived from invariant_failedt) error report structure;
+///  its backtrace member will be set before it is used.
+template<class T>
+typename std::enable_if<std::is_base_of<invariant_failedt, T>::value>::type


Actually I think it probably could work like that in this case. Either taking a const invariant_failedt & and then copying it to a temporary or else taking an invariant_failedt & and having it in the contract that it will be updated with the stacktrace.

NathanJPhillips · 2017-06-28T09:42:06Z

src/util/invariant.h

+  /// Set the backtrace stored against this error report.
+  /// This is overwritten by `invariant_violated`, which is called
+  /// from the `INVARIANT` family of macros.
+  void set_backtrace(const std::string &_backtrace)


I would consider having this private (probably actually directly accessing the private field) and making invariant_violated a friend or a static member of this class.

smowton · 2017-06-28T10:04:46Z

@thk123 under every build they abort with this patch, but if we change that I will use Catch as you recommend

smowton · 2017-06-28T10:42:58Z

@NathanJPhillips @peterschrammel all changes applied except as noted

smowton · 2017-06-28T11:12:26Z

All changes applied, including moving the tests. @thk123 @peterschrammel @NathanJPhillips ready for re-review.

thk123 · 2017-06-28T11:24:42Z

regression/invariants/Makefile

+include ../../src/common
+
+test: driver$(EXEEXT)
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \


How does this work? Don't you need some shell script that compiles and runs driver.cpp rather than running cbmc?

tautschnig

I can no longer claim I understand what's going on here. Files being compiled but seemingly never used (driver.cpp), options seemingly nowhere handled (test-invariant-failure). Can we keep it simple, please?

tautschnig · 2017-06-28T11:48:06Z

regression/invariants/driver.cpp

+
+/// Causes an invariant failure dependent on first argument value.
+/// Returns 1 on unexpected arguments.
+int main(int argc, char** argv) {


Nit picking: Place { on next line

tautschnig · 2017-06-28T11:49:37Z

src/cbmc/cbmc_parse_options.cpp

@@ -106,26 +106,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
  }

  // Test only; do not use for input validation


I believe that comment should be removed as well

tautschnig · 2017-06-28T11:52:38Z

src/cbmc/cbmc_parse_options.h

@@ -63,7 +63,7 @@ class optionst;
  "(java-cp-include-files):" \
  "(localize-faults)(localize-faults-method):" \
  "(lazy-methods)" \
-  "(test-invariant-failure)" \
+  "(test-invariant-failure):" \


I admit I have no idea how this works: all code handling "test-invariant-failure" has been removed. So where is it being processed?

smowton · 2017-06-28T12:16:27Z

@thk123 @tautschnig oops I had not committed some changes but was getting away with it due to a stale cbmc. Changed now, but in summary:

Makefile builds driver as a dependency of the test target
driver passed to test.pl as the program under test.

smowton · 2017-06-28T12:19:25Z

@tautschnig that option should have been removed; all your changes now applied.

tautschnig · 2017-06-28T12:33:39Z

src/util/invariant.cpp

+/// \return backtrace with a file / function / line header.
+std::string get_backtrace(
+  const char * const file,
+  const char * const function,


Why are C strings being used here instead of std::string?

Constant strings introduced by the preprocessor I guess.

But then the compiler would happily build const std::string objects from those?

Sure, I was just saying I guess @martin-cs presumably did that cos he knew they were always plain old string constants. I can make them std::string if you prefer.

I am aware that this implies further changes; but given the effort by @reuk to get rid of plain pointers we should stick with that direction.

tautschnig · 2017-06-28T12:35:01Z

src/util/invariant.h

@@ -10,6 +10,8 @@ Author: Martin Brain, [email protected]
 #define CPROVER_UTIL_INVARIANT_H

 #include <stdexcept>
+#include <type_traits>
+#include <iostream>


We must avoid #include <iostream> in a widely used header file to keep compilation times reasonable.

If it's just for forward declarations #include <iosfwd> might be acceptable?

Just to follow-up on that: the implementation of the function using std::cerr would thus have to go in the cpp file.

I've moved the std::cerr stuff into the cpp file

peterschrammel · 2017-06-30T09:45:36Z

Last fix required: http://cbmc-linter.diffblue.com.s3-website-us-east-1.amazonaws.com/linter-b1a89d91dd4441085f467f642e3c449ddf718f1c.txt
then this should be ready to go.

smowton · 2017-07-03T08:45:44Z

(fix applied)

peterschrammel · 2017-07-03T14:05:12Z

@kroening, this is ready to go.

reuk

I have a couple of issues with the structure of invariant_failedt, sorry to revive this PR after so long.

reuk · 2017-07-10T10:09:37Z

src/util/invariant.h

+
+  /// Describes this error using `backtrace` and `pretty_print`.
+  /// Cannot be overridden; override `pretty_print` instead.
+#ifdef _MSC_VER


We should have a macro in util called CBMC_NOEXCEPT or similar which expands to noexcept on platforms which support it, and nothing on those which don't. We could do the same thing with constexpr too.
That way, this function declaration would become

const char *what() const CBMC_NOEXCEPT final

which is a bit cleaner.

reuk · 2017-07-10T10:24:04Z

src/util/invariant.h

+  /// structured error description. `std::logic_error::what` is
+  /// overridden to use this and the backtrace to describe the
+  /// error.
+  virtual std::string pretty_print() const


Exceptions already have a virtual const function which returns a string, so I'm not convinced there's a need for another. I would restructure this code like so:

class invariant_failedt : public std::logic_error { // We don't need a mutable string holding the return of `what`, so the // object is smaller *and* more const-safe std::string backtrace; public: // This is not virtual! It will call `what` and add a stack trace std::string pretty_print() const { try { std::ostringstream ss; ss << what() << '\n' + backtrace; return ss.str(); } catch (...) { return "Exception describing invariant failure"; } } // We don't even need to override `what` here, but derived classes are free // to do so if they need more structured info. };

A possible downfall of this approach is that clients need to know to call pretty_print when they catch the exception, rather than what, but I believe this is a reasonable trade-off, as the invariant_failedt no longer needs to store the what_str member, making it smaller and more const-safe.

I believe various standard things do call what() - in fact isn't the standard behaviour on uncaught exceptions to print what() and terminate?

tautschnig · 2017-07-20T07:27:40Z

@smowton Could you please rebase and poke @kroening to get it merged? With current master, it's seemingly very cumbersome to pass a non-constant reason to INVARIANT (because it uses char* instead of std::string).

smowton · 2017-07-20T08:02:16Z

I've also got reuk's comments to account for, will do this tomorrow morning (on the road today)

tautschnig · 2017-07-20T08:19:07Z

Great, thanks!

kroening · 2017-07-20T13:38:14Z

Looks ready to go after rebase.

reuk

LGTM

reuk · 2017-07-21T15:00:48Z

src/util/invariant.h

-#define INVARIANT(CONDITION, REASON) do {} while(0)
-
+#define INVARIANT(CONDITION, REASON, ...) do {} while(0)
+#define INVARIANT(CONDITION, REASON, ...) do {} while(0)


Is this duplication deliberate?

reuk · 2017-07-21T15:11:17Z

src/util/invariant.h

+  const std::string reason;
+
+  invariant_failedt(
+    const std::string &_file,


Very minor point: names starting with an underscore are reserved in the global namespace, and names starting with _[A-Z] are reserved everywhere. Although the usage here is not in violation, I'd prefer to avoid underscore prefixes in general.

smowton · 2017-07-21T15:27:06Z

@kroening ready when you are

[depends: #1063] Use nullptr to represent null pointers (targets master)

…ets master)"

Revert "[depends: #1063] Use nullptr to represent null pointers (targets master)"

Corrected simplify lhs in ai_domain_baset The boolean flag was the wrong way round for ai_simplify_lhs - this corrects this. Added unit tests to validate the return meaning of ai_simplify_lhs These tests use a mock implementation of the `ai_domain_baset` interface just to validate that true means no simplification. Fix nullptr Fix linter errors, ignoring big-int and miniz Allow invariants with structured exceptions Revert "[depends: diffblue#1063] Use nullptr to represent null pointers (targets master)" goto-symex^2: goto-symex for symbolic execution Goto merged before jumping out the goto-symex operator loop, for handling GOTO and ASSERT

smowton requested review from peterschrammel, tautschnig and thk123 June 27, 2017 10:03

smowton requested review from reuk and martin-cs June 27, 2017 10:05

smowton force-pushed the smowton/feature/improved_invariants branch from c0fea89 to f199e65 Compare June 27, 2017 10:08

thk123 reviewed Jun 27, 2017

View reviewed changes

peterschrammel reviewed Jun 27, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch from f199e65 to 1352369 Compare June 27, 2017 15:40

thk123 reviewed Jun 28, 2017

View reviewed changes

NathanJPhillips suggested changes Jun 28, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch from 1352369 to ad188a1 Compare June 28, 2017 10:42

smowton force-pushed the smowton/feature/improved_invariants branch from ad188a1 to e449526 Compare June 28, 2017 11:11

thk123 reviewed Jun 28, 2017

View reviewed changes

tautschnig requested changes Jun 28, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch from e449526 to a7f31e2 Compare June 28, 2017 12:13

smowton force-pushed the smowton/feature/improved_invariants branch from a7f31e2 to a61e740 Compare June 28, 2017 12:19

smowton force-pushed the smowton/feature/improved_invariants branch from a61e740 to 3871f8f Compare June 28, 2017 12:23

tautschnig reviewed Jun 28, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch 2 times, most recently from 80944ef to 9c8a2be Compare June 28, 2017 12:44

peterschrammel added the enhancement label Jun 29, 2017

NathanJPhillips approved these changes Jun 29, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch from b1a89d9 to 83d9b04 Compare June 30, 2017 10:11

reuk suggested changes Jul 10, 2017

View reviewed changes

jasigal mentioned this pull request Jul 12, 2017

Refactor/update refinement solver asserts #1110

Merged

tautschnig mentioned this pull request Jul 20, 2017

Support out-of-bounds checks on arrays of dynamic size #1158

Merged

reuk mentioned this pull request Jul 20, 2017

[depends: #1063] Use nullptr to represent null pointers (targets master) #1159

Merged

smowton force-pushed the smowton/feature/improved_invariants branch 2 times, most recently from a4df2b3 to 0c29208 Compare July 21, 2017 14:56

reuk approved these changes Jul 21, 2017

View reviewed changes

smowton force-pushed the smowton/feature/improved_invariants branch 2 times, most recently from 48781ac to 06f758e Compare July 21, 2017 15:26

Allow invariants with structured exceptions

493e9be

smowton force-pushed the smowton/feature/improved_invariants branch from 06f758e to 493e9be Compare July 23, 2017 11:07

kroening pushed a commit that referenced this pull request Jul 24, 2017

Merge pull request #1159 from reuk/use-nullptr-master

80e4214

[depends: #1063] Use nullptr to represent null pointers (targets master)

kroening pushed a commit that referenced this pull request Jul 24, 2017

Revert "[depends: #1063] Use nullptr to represent null pointers (targ…

6fea4fa

…ets master)"

kroening merged commit 747db78 into diffblue:master Jul 24, 2017

kroening mentioned this pull request Jul 24, 2017

Revert "Improved invariants" #1171

Closed

tautschnig mentioned this pull request Jul 24, 2017

Revert "[depends: #1063] Use nullptr to represent null pointers (targets master)" #1172

Merged

tautschnig added a commit that referenced this pull request Jul 24, 2017

Merge pull request #1172 from diffblue/revert-1159-use-nullptr-master

49bceb2

Revert "[depends: #1063] Use nullptr to represent null pointers (targets master)"

		@@ -106,26 +106,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
		}

		// Test only; do not use for input validation

Improved invariants #1063

Improved invariants #1063

Conversation

smowton commented Jun 27, 2017

smowton commented Jun 27, 2017

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

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

smowton commented Jun 27, 2017

thk123 commented Jun 28, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton Jun 28, 2017 • 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

NathanJPhillips Jun 28, 2017 • edited Loading

Choose a reason for hiding this comment

smowton commented Jun 28, 2017 • edited Loading

smowton commented Jun 28, 2017

smowton commented Jun 28, 2017

Choose a reason for hiding this comment

tautschnig 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

smowton commented Jun 28, 2017

smowton commented Jun 28, 2017

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

peterschrammel commented Jun 30, 2017

smowton commented Jul 3, 2017

peterschrammel commented Jul 3, 2017

reuk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk Jul 10, 2017 • edited Loading

Choose a reason for hiding this comment

NathanJPhillips Jul 11, 2017 • edited Loading

Choose a reason for hiding this comment

tautschnig commented Jul 20, 2017

smowton commented Jul 20, 2017

tautschnig commented Jul 20, 2017

kroening commented Jul 20, 2017

reuk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Jul 21, 2017

smowton Jun 28, 2017 •

edited

Loading

NathanJPhillips Jun 28, 2017 •

edited

Loading

smowton commented Jun 28, 2017 •

edited

Loading

reuk Jul 10, 2017 •

edited

Loading

NathanJPhillips Jul 11, 2017 •

edited

Loading