Feature/internal invariant #911

martin-cs · 2017-05-11T19:49:10Z

A proposal to resolve issue #182 . Assertions (and things like throw 0) should be replaced with INVARIANT, PRECONDITION, POSTCONDITION, DATA_INVARIANT, CHECK_RETURN and UNREACHABLE. These macros can be configured to throw a std::exception with a backtrace (the default), assert, __CPROVER_assert (so we can examine our own source code), be ignored (for performance or checking they are side-effect free) or print out the backtrace and then terminate.

To get backtraces you need to build against glibc. To get function names in the backtrace you must have built with LINKFLAGS="-rdynamic".

peterschrammel · 2017-05-11T21:10:17Z

src/util/invariant.cpp

+
+\*******************************************************************/
+
+static bool output_demangled_name (std::ostream &out, const char * const stack_entry)


http://cbmc-linter.diffblue.com.s3-website-us-east-1.amazonaws.com/linter-b8324cc9655b75e58100e3989b2d3ab7aa790ff3.txt

Lint errors fixed.

peterschrammel · 2017-05-11T21:11:15Z

src/util/invariant.cpp

+{
+  if (condition)
+    return;
+  else


no else after return

peterschrammel · 2017-05-11T21:16:04Z

src/util/invariant.h

+// Not recommended but provided for backwards compatability
+#include <cassert>
+
+#define INVARIANT(CONDITION, REASON) assert((CONDITION))


could use (CONDITION) && (REASON)

Yes; good idea. Fixed.

peterschrammel · 2017-05-11T21:16:51Z

src/util/invariant.h

+// This is *not* recommended as it can result in unpredictable behaviour
+// including silently reporting incorrect results.
+// This is also useful for checking side-effect freedom.
+#define INVARIANT(CONDITION, REASON) do {} while(0)


ok, ; would do as well

I put do/while to swallow the semi-colon at the end.

To add to this: it's important to ensure that no expansion of those macros can yield ;; as that may trigger compiler warnings.

Good point.

peterschrammel · 2017-05-11T21:18:38Z

src/util/invariant.h

+// to migrate documentation and "error handling" in older code
+#define TODO           INVARIANT(0, "Todo");
+#define UNIMPLEMENTED  INVARIANT(0, "Unimplemented");
+#define UNHANDLED_CASE INVARIANT(0, "Unhandled case");


What's the difference between these?

Documentation value?

peterschrammel · 2017-05-11T21:19:36Z

src/util/irep.cpp

@@ -203,7 +204,8 @@ void irept::nonrecursive_destructor(dt *old_data)
    if(d==&empty_d)
      continue;

-    assert(d->ref_count!=0);
+    INVARIANT(d->ref_count!=0,


break after ( (several occurrences)

Unnecessary line break removed. Is that what you meant?

peterschrammel · 2017-05-11T21:24:08Z

src/solvers/smt2/smt2_conv.cpp

@@ -42,7 +41,7 @@ Author: Daniel Kroening, [email protected]
 #define UNEXPECTEDCASE(S) throw "Unexpected case: " S

 // General todos
-#define TODO(S) throw "TODO: " S
+#define SMT2_TODO(S) throw "TODO: " S


Why is this not a TODO or UNIMPLEMENTED?

I wanted this commit to be as minimal as possible and to be clearly not changing functionality (the whole set should be very low risk / minimal impact). To replace with the new TODO I'd have to move the more complex error messages to use error(), which would mean a bigger change.

Ok, this can be done separately.

peterschrammel · 2017-05-11T21:25:14Z

src/util/std_expr.h

@@ -1914,6 +2001,34 @@ class bitnot_exprt:public unary_exprt
  }
 };

+/*! \brief Cast a generic exprt to a \ref bitnot_exprt


These two functions seem to be new. Maybe put into a separate commit.

peterschrammel · 2017-05-11T21:31:59Z

src/util/invariant.cpp

+
+// Backtraces compiler and C library specific
+#include <assert.h>
+#ifdef __GLIBC__


This doesn't work for mac and alpine:
https://travis-ci.org/diffblue/cbmc/jobs/231294968#L140

Oops; fixed.

peterschrammel · 2017-05-11T21:32:38Z

src/util/invariant.h

+                     const bool condition, const char * const reason);
+
+#define INVARIANT(CONDITION, REASON) \
+  check_invariant(__FILE__, __func__, __LINE__, (CONDITION), (REASON))


This doesn't work for msvc:
https://ci.appveyor.com/project/diffblue/cbmc/build/1.0.1155#L90

It's in C99! But, ofcourse, Microsoft can't ship a standard compliant C compiler...
Fixed.

martin-cs · 2017-05-11T23:38:57Z

The one linter failure is unavoidable; it is a regression test for the linter to find asserts.

martin-cs · 2017-05-12T01:08:23Z

AppVeyor failure is a bit harder and help from someone who knows windows / has access to a windows machine would be appreciated.

tautschnig

Very nice work! My comments are all about whitespace... I'd suggest that @reuk takes a look at this.

tautschnig · 2017-05-12T07:15:16Z

src/util/invariant.cpp

+
+#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
+#include <iostream>
+#include <stdlib.h>


Use cstdlib

tautschnig · 2017-05-12T07:15:39Z

src/util/invariant.cpp

+#include <string>
+#include <sstream>
+
+


A lot of blank lines here, I'd opt for single blank lines

tautschnig · 2017-05-12T07:15:59Z

src/util/invariant.cpp

+#endif
+
+// Backtraces compiler and C library specific
+#include <assert.h>


Should be cassert, I'd say

That won't do what I'm after. I'm including a C header so that I get GLIBC defined if that C library is GLibc. Thus I want something that is definitely and always a C header, regardless of how the stdc++ library is implemented.

Ah! Would you mind adding this as a comment to the code so that no one ever changes this in a naive cleanup attempt? Thanks!

tautschnig · 2017-05-12T07:16:31Z

src/util/invariant.cpp

+
+\*******************************************************************/
+
+static bool output_demangled_name(std::ostream &out,


Newline after (

Ah; that's what Peter wanted. Sorry, not checked by lint.

tautschnig · 2017-05-12T07:16:41Z

src/util/invariant.cpp

+static bool output_demangled_name(std::ostream &out,
+                                  const char * const stack_entry)
+{
+  bool return_value = false;


No whitespace around =

Fixed. Again, I thought lint was catching these so when it wasn't caught I figured we weren't doing it.

tautschnig · 2017-05-12T07:17:26Z

src/util/invariant.cpp

+
+  std::string working(stack_entry);
+
+  size_t start = working.rfind('(');  // Path may contain '(' !


We seem to be widely using std::size_t, even though in this case I'd even lean towards std::string::size_type

tautschnig · 2017-05-12T07:17:37Z

src/util/invariant.cpp

+  size_t start = working.rfind('(');  // Path may contain '(' !
+  size_t end = working.find('+', start);
+
+  if(start != std::string::npos &&


No whitespace around !=

tautschnig · 2017-05-12T07:17:50Z

src/util/invariant.cpp

+     end != std::string::npos &&
+     start + 1 <= end - 1)
+  {
+    size_t length = end - (start + 1);


No whitespace around -, +

tautschnig · 2017-05-12T07:18:46Z

src/util/invariant.cpp

+    std::string mangled(working.substr(start + 1, length));
+
+    int demangle_success = 1;
+    char *demangled =


std::unique_ptr maybe?

I'd rather keep these as free as the documentation says that they are explicitly malloc'd.

peterschrammel · 2017-05-12T08:58:20Z

@martin-cs, you can put // NOLINT(build/depreciated) to silence the linter for this specific case.

tautschnig · 2017-05-12T08:59:35Z

@peterschrammel Wouldn't that defy the purpose of the regression test?

reuk · 2017-05-12T09:01:06Z

My main concern is this:

These macros can be configured to throw a std::exception with a backtrace (the default), assert, __CPROVER_assert (so we can examine our own source code), be ignored (for performance or checking they are side-effect free) or print out the backtrace and then terminate.

The exceptions that may be thrown from a function are an important part of its interface. Lets say that, during normal development, we build with invariants set to throw exceptions. Somewhere in the code, we discover that something that was designed to be an invariant actually may trigger during normal operation, so we use a try/catch to retry this method with different arguments if it fails. Now, if we swap exceptions for asserts, we get a hard crash. Worse, if we remove them, we open the program up to memory corruption errors, because the program attempts to continue. Being able to swap out error reporting mechanisms means that the program might exhibit markedly different behaviour depending on the compile flags, which in turn means that we would need (at minimum) every error reporting mechanism to be enabled and tested during CI.

One response to this might be "instead of try/catch on an exception triggered by an assertion, the invariant should be replaced by a true (non-invariant) exception", but part of the reason this is an issue in the first place is because we're hitting assertions in production. We haven't been able to guarantee that the things we think are invariants really are. If we just used banned assert and used exceptions by default, we wouldn't have to worry about putting side-effects in assert statements, we'd always have the option to recover from errors (the caller should be allowed to decide whether or not an error from higher up the stack is really fatal or not), and we'd only have a single build configuration to test.

tautschnig · 2017-05-12T09:25:31Z

The exceptions that may be thrown from a function are an important part of its interface. Lets say that, during normal development, we build with invariants set to throw exceptions. Somewhere in the code, we discover that something that was designed to be an invariant actually may trigger during normal operation, so we use a try/catch to retry this method with different arguments if it fails.

That's abuse of exceptions, isn't it? If I read this correctly, this would suggest that exceptions are considered part of normal behaviour. But I may be misinterpreting what you've said.

reuk · 2017-05-12T09:43:09Z

Exceptions aren't normal behaviour, but they are foreseeable program states. In the situation described in this comment, we might want to try loading other classes, even if one class is ill-formed - we might be able to use the default stubbing behaviour for classes which couldn't be loaded (for example). Using try/catch to handle errors and continue with execution isn't an abuse, but rather the motivating case for exceptions.

tautschnig · 2017-05-12T09:53:46Z

Agreed, but then we should be throwing very specific types/classes of exceptions in all forseen cases. We can then catch those, and only those.

reuk · 2017-05-12T09:55:34Z

Yes, that's my proposal. But I'm saying that currently, everywhere we're using assertions, we could make the decision to replace these with exceptions, as this gives us a chance to recover from logic errors. Inner functions shouldn't have the ability to halt the program with no warnings, because there's always a chance that the caller may have forseen the failure case and have a contingency plan.

martin-cs · 2017-05-12T12:10:29Z

The exceptions that may be thrown from a function are an important part of its interface. Lets say that, during normal development, we build with invariants set to throw exceptions. Somewhere in the code, we discover that something that was designed to be an invariant actually may trigger during normal operation, so we use a `try/catch` to retry this method with different arguments if it fails.

Please never do this; it is an incredibly bad idea. If we discover something we thought was an invariant but fails under normal operation then something is *SERIOUSLY* wrong. This is a huge red flag and attempting to 'just hack around it' is the *worst* thing we can do and that is *exactly* why we need a way of building the software that doesn't throw and exception -- so I can still debug the system remotely, via e-mail, even when people have done this. Allow me to clarify some of the terminology: Invariant --------- An expression that is true at the given location, regardless of input. These must hold for *all* inputs. In some deep sense they are a logical consequence of the structure (and design) of the program. Their failure is not a "forseeable event"; it's the opposite, it is the programmer saying "I believe this to be impossible". Although these are (theoretically) logically redundant, they are of immense value to formal verification tools ( hence CPROVER_INVARIANT_CPROVER_ASSERT ) but more importantly they are of immense value to programmers as they formally document "why is it OK to assume that" / the intent of the design. So why bother checking them if they are always true? Well, we don't have to ( CPROVER_INVARIANT_DO_NOT_CHECK ) and as the invariants become more complex ( "this goto-program is correctly structured" #751 ), we made want to ignore them for specific use-cases where we are already checking for known reference results ( https://sv-comp.sosy-lab.org/ ). However checking them is useful because it can catch programmer misunderstandings of the design of the system. This is why they default to being checked. The point is that there is no one right thing to do once you're reached a state in which, by definition, the program is wrong. At the moment invariants are checked / their failure is handled by a mix of different methods, assert, throw, abort, etc. We should be consistent on marking them as what they are and separate the /annotation/ from the /mechanism/. Assertions ---------- Assertions are one /mechanism/ for handling invariants. They have the problem that when they fail they are not very informative (this is why I started working on this) and they aren't particularly useful as documentation because although they give the condition they don't say why. Although they aren't great for backwards compatability we should still offer them ( CPROVER_INVARIANT_ASSERT ). Exceptions ---------- Exceptions are a /mechanism/ for handling a range of different errors. This may include handling the failure of invariants. They are a good mechanism as they allow flexible error handling (this is why they are the default) but they are not the *only* method for handling errors, nor are they the most desirable in all circumstances; doubly for handling invariant failures. From a support perspective, exceptions can be a nightmare. What I ideally want is that the program informs me as soon as one of the design invariants of the system has been broken, ideally statically but dynamically would do as well. Unfortunately we don't have the tech to do that (yet). So I'll settle for the next best thing, notification as soon as the program notices, i.e. as soon as an invariant fails. This is what CPROVER_INVARIANT_PRINT_STACK_TRACE does, and will give me a core dump to boot, so I can remotely debug problems on sites I don't have any interactive access to / interactive access only via e-mail and someone else. If you only handle invariant failure by an exception then there is a risk that someone will catch it, think they know better, do something else and so on... leaving me staring at an incorrect answer with no real idea where, when or why the program is wrong. Debugging via e-mail is hard enough, chasing throws and catches is likely largely impossible. Thus there needs to be a way of "stop on the first error" that *cannot* be disabled regardless of what other well-meaning programmers do. Just saying "we'll tell people not to catch exceptions of type ..." will not work; we are, by definition, dealing with cases when there are mistakes during development. Conclusion ---------- If you believe the design (and correct) implementation of the system ensures that something holds ---> INVARIANT. If it is a forseeable error given the correct implementation of the system ---> throw an exception. 1. I am not saying "don't use exceptions" I am saying "do not *only* use exceptions to handle failed invariants". 2. This patch is intended to be the start of a long clear-up which removes asserts and some of the exceptions that are being used to handle failed invariants ("throw 0" will be my first target). This is part of a move to not only have documentation on various key data-structure but to automatically check it. 3. You do not have to use invariants, you can always throw an exception if it makes you happy. You will make my job harder but if that's the price for having the tools we need ... so be it.

reuk · 2017-05-12T13:18:02Z

So I'll settle for the next best thing, notification as soon as the program notices, i.e. as soon as an invariant fails.

Sure, but there's a difference between 'notification' and 'terminate the program'. This could be achieved equally well using an exception that logs, on construction, the current backtrace into a logfile or to stderr. Good debuggers allow you to set exception breakpoints, which is another option for immediate notification.

If you only handle invariant failure by an exception then there is a risk that someone will catch it, think they know better, do something else and so on... leaving me staring at an incorrect answer with no real
idea where, when or why the program is wrong.

Maybe the caller really does know better. As the writer of a library function, you have no way of knowing all the contexts in which your function will be called. As I see it, all the arguments for assertions could equally well be addressed with better logging, as the main problem seems to be a lack of information when invariants are broken.

Going back to my original point, allowing the error notification mechanism to be changed at compile time may cause breakage if callers come to depend on the behaviour of a particular mechanism. The only way to combat this is to build and test all the options on CI. Therefore, I believe that this should not be a point of customisation. Instead, we should decide and document how each class of error should be reported, in order to minimise the number of build configurations.

tautschnig · 2017-05-12T13:22:23Z

Going back to my original point, allowing the error notification mechanism to be changed at compile time may cause breakage if callers come to depend on the behaviour of a particular mechanism. The only way to combat this is to build and test all the options on CI. Therefore, I believe that this should not be a point of customisation. Instead, we should decide and document how each class of error should be reported, in order to minimise the number of build configurations.

I think I no longer know what the problem is here. Let's just build all the config options in CI and get over it?

martin-cs · 2017-05-12T13:44:08Z

On Fri, 2017-05-12 at 06:18 -0700, Reuben Thomas wrote: > So I'll settle for the next best thing, notification as soon as the program notices, i.e. as soon as an invariant fails. Sure, but there's a difference between 'notification' and 'terminate the program'.

There is but in this case I want a hard stop.

This could be achieved equally well using an exception that logs, on construction, the current backtrace into a logfile or to stderr.

This is what messaget is for and why it is suggested that more comprehensive information goes there.

Good debuggers allow you to set exception breakpoints, which is another option for immediate notification.

In many of the cases where this will be active it is not possible to run a debugger, good or otherwise.

> If you only handle invariant failure by an exception then there is a risk that someone will catch it, think they know better, do something else and so on... leaving me staring at an incorrect answer with no real idea where, when or why the program is wrong. Maybe the caller really does know better. As the writer of a library function, you have no way of knowing all the contexts in which your function will be called.

We aren't writing a general purpose library and there are many things in CPROVER that are just plain wrong. We don't have code that attempts to recover from invalid / corrupted data structure and there are *many* higher priority things to write. Yeah, in theory, maybe, one day, we might want this but let's solve that problem when we come to it and we know what the actual requirements are. We will have the invariants clearly marked and separated from the 'normal' exceptions so we can just drop in the support we need.

As I see it, all the arguments for assertions could equally well be addressed with better logging, as the main problem seems to be a lack of information when invariants are broken.

No amount of logging will allow me to swap the invariants out for CPROVER_asserts or ignore them entirely. The specific problem I referred to was around the normalisation of error and people making mistakes about exception handling; logging does not fix those either.

Going back to my original point, allowing the error notification mechanism to be changed at compile time may cause breakage if callers come to depend on the behaviour of a particular mechanism.

Would it help if I changed the (informal) contract to "if this fails then it is undefined behaviour"?

The only way to combat this is to build and test all the options on CI.

Sure; let's do it.

Therefore, I believe that this should not be a point of customisation. Instead, we should decide and document how each class of error should be reported, in order to minimise the number of build configurations.

As I said before, there isn't one right thing to do. It depends on the real world context of how the system is being deployed. The policy is pretty clear : write to messaget, then INVARIANT if it is an invariant, throw an exception if it is a feasible error.

martin-cs · 2017-05-17T22:50:34Z

This is now as fixed as it can be. There is one linter failure, from a regression test for the linter to check for exactly that kind of failure.

@kroening : is this what you wanted when you told me an assertion based solution?
@peterschrammel @tautschnig : any more review comments?

tautschnig

From my point of view this looks good, even though I think 14118e5 would better be placed in a separate (trivial) PR. But that's just me doing my usual nit picking.

reuk · 2017-05-18T08:45:38Z

regression/cpp-linter/assert/test.desc

+CORE
+main.cpp
+
+^main\.cpp:8:  assert is depreciated, use INVARIANT instead  \[build/depreciated\] \[4\]


depreciated -> deprecated

Fixed; good catch.

reuk · 2017-05-18T08:45:50Z

scripts/cpplint.py

+            'assert is depreciated, use UNREACHABLE instead')
+    else:
+      error(filename, linenum, 'build/depreciated', 4,
+            'assert is depreciated, use INVARIANT, PRECONDITION, CHECK_RETURN, etc. instead')


depreciated -> deprecated

Fixed; good catch.

reuk · 2017-05-18T08:47:42Z

src/util/invariant.cpp

+#ifdef CPROVER_INVARIANT_PRINT_STACK_TRACE
+    abort();
+#else
+    throw std::logic_error(out.str());


Throw something more descriptive than logic_error, probably a custom exception derived from logic_error specifically for logic errors in CBMC code.

Yeah; probably makes sense.

reuk · 2017-05-18T08:51:29Z

src/util/invariant.cpp

+    std::size_t i;
+
+    entries=backtrace(stack, sizeof(stack) / sizeof(void *));
+    description=backtrace_symbols(stack, entries);


Use unique_ptr with a custom deleter. This deleter is a general-purpose component that should probably live in util:

struct freert final { template <typename T> void operator()(T t) const { free(t); } };

reuk · 2017-05-18T08:52:29Z

src/util/invariant.cpp

+    void * stack[50];
+    std::size_t entries;
+    char **description;
+    std::size_t i;


All of these should be initialised, and moved as close to where they are used as possible.

Refactored all but stack so that the are declared and initialised together. stack is initialised on the line below it's declaration.

void *stack[50]={};?

reuk · 2017-05-18T08:55:46Z

src/util/invariant.h

+
+void check_invariant(const char * const file,
+                     const char * const function, const int line,
+                     const bool condition, const char * const reason);


Marking passed-by-value arguments const in the interface has no effect.

Having them const stops me accidentally changing them in the implementation.

Yes, but it's unnecessary noise on the interface. This post explains it pretty well.

It's valid to have void check_invariant(bool); in your interface and void check_invariant(const bool) {} in your implementation. The declaration will still correspond to the expected definition.

I think it's worth keeping the signatures the same in declaration and implementation. If the cost of getting people to add consts is that we get too many -- so be it. I really doubt the consts are used minimally in the rest of the code base.

Plus; this is not a developer facing function. If there was a way of hiding the declaration entirely; then I'd do it.

reuk · 2017-05-18T09:10:23Z

src/util/invariant.cpp

+    std::string mangled(working.substr(start+1, length));
+
+    int demangle_success=1;
+    char *demangled=


Use unique_ptr with custom freer.

reuk · 2017-05-18T09:24:13Z

src/util/invariant.cpp

+
+    if(demangle_success==0)
+    {
+      out << working.substr(0, start+1)


If the ostream has exceptions enabled, << may throw an exception, in which case we would leak demangled.

martin-cs · 2017-05-18T11:37:13Z

The memory stuff... I think I'd rather keep the code obvious and straight forward. As I see it, the only possibility of a leak would requires the following sequence:

an invariant fails.
writing to a std::ostringstream throws an exception

That sounds pretty terminally unrecoverable to me and at that point I'm not sure that leaking a small number of bytes is really a problem? I mean, I could try/catch around the writing so that we still get a meaningful error message even if it goes catastrophically wrong. Would that help?

reuk · 2017-05-18T12:02:02Z

unique_ptr is designed to automatically free resources when they go out of scope. I don't really understand what the problem is here.

martin-cs · 2017-05-18T12:37:10Z

On Thu, 2017-05-18 at 05:02 -0700, Reuben Thomas wrote: `unique_ptr` is designed to automatically free resources when they go out of scope. I don't really understand what the problem is here.

I just don't want to make the code any more complicated than it needs to be; especially not to deal with cases that really don't matter given the context of the application. I can see an argument for "what happens if an exception is thrown during the construction of the exception for the fatal error". I guess that could happen and maybe we would need a meaningful answer for that but... There are many more pressing things we could spend our time on.

martin-cs · 2017-06-08T14:12:59Z

@kroening A version of this patch has been used to locate an issue that was not otherwise possible to diagnose ( https://github.com/diffblue/platform/issues/603 ).

tautschnig · 2017-06-08T15:45:49Z

Would it make sense to have that "version" of the patch in this PR? Also a rebase is due.

martin-cs · 2017-06-09T10:53:42Z

Have rebased.

The version of this patch... I'd rather not because 1. it patches a different version to trunk (older plus some things that are not in master) and 2. it contains a hasty, automatic conversion of most of the asserts and some of the throws to invariants. I don't think automatic conversion is the way to go as part of the point of this exercise is to tidy up what are actually invariants, what are possible error cases that should be thrown, etc.

peterschrammel · 2017-06-09T15:39:47Z

src/util/invariant.h

+** CPROVER_INVARIANT_* macros.
+*/
+
+class invariant_failed : public std::logic_error


The linter wants you to remove the space before the colon. Same in 57 and 58.

The class name should end in "t".

Fixed; could have sworn I'd got all of the linting errors.

peterschrammel · 2017-06-09T15:41:56Z

src/util/invariant.h

+
+class invariant_failed : public std::logic_error
+{
+ public :


No space before colon. Do not indent public.

peterschrammel · 2017-06-09T15:42:26Z

src/util/invariant.h

+class invariant_failed : public std::logic_error
+{
+ public :
+  explicit invariant_failed (const std::string& what) : logic_error(what) {}


No space before (. Same in the next line.

peterschrammel · 2017-06-09T15:42:42Z

src/util/invariant.h

+// This is *not* recommended as it can result in unpredictable behaviour
+// including silently reporting incorrect results.
+// This is also useful for checking side-effect freedom.
+#define INVARIANT(CONDITION, REASON) do {} while(0)


Good point.

peterschrammel · 2017-06-09T15:46:06Z

src/util/invariant.h

+#define INVARIANT(CONDITION, REASON) \
+  __CPROVER_assert((CONDITION), "Invariant : " REASON)
+
+


Reduce the number of blank lines in this file.

peterschrammel · 2017-06-09T15:52:41Z

src/util/invariant.cpp

+
+/*******************************************************************\
+
+Function: check_invariant


Should be adapted do doxygen now.

peterschrammel · 2017-06-09T15:53:03Z

src/util/invariant.cpp

+     end!=std::string::npos &&
+     start+1<=end-1)
+  {
+    std::string::size_type length=end - (start+1);


no spaces around -

peterschrammel · 2017-06-09T15:55:24Z

scripts/cpplint.py

+  line = clean_lines.elided[linenum]
+  match = Match(r'.*\s+assert\(.*\).*', line)
+  if match:
+    if Match(r'.*\s+assert\(0\).*', line):


also assert(false)

peterschrammel · 2017-06-09T15:56:53Z

src/util/std_expr.h

@@ -59,7 +58,9 @@ class transt:public exprt
 */
 inline const transt &to_trans_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_trans && expr.operands().size()==3);
+  PRECONDITION(expr.id()==ID_trans);
+  DATA_INVARIANT(expr.operands().size()==3,


Put both arguments on a separate line if they don't fit (similar cases below)

peterschrammel · 2017-06-09T16:00:15Z

src/util/expr.cpp

@@ -245,7 +245,7 @@ bool exprt::is_zero() const
    {
      rationalt rat_value;
      if(to_rational(*this, rat_value))
-        assert(false);
+        CHECK_RETURN(false);


It would actually be even more convenient if we could write CHECK_RETURN(to_rational(*this, rat_value));. However, we must guarantee that the implementation of CHECK_RETURN always evaluates its argument.

Yes... this patch set is intended to replace assert but there are a few other invariant handling patterns that could benefit from some kind of support. This is one of them, another is:

if (invariant) { debug() << "Actually helpful message with " << variables << " in it " << "maybe even " << e.pretty(); assert(0); }

We should do something about these but I don't think we should do so in this patch set. I this will come out of trying to convert things to this way of doing things. We will get a better idea of what patterns there are and how they could be improved.

This allows us to have tests that are intended to abort. Given that tests can (and mostly do) check the exit code this should not reduce the utility of the test system.

martin-cs · 2017-06-13T11:00:19Z

Have addressed all of @peterschrammel 's comments, rebased and repushed.

… fails.

Many of these are split into two invariants are there is the specific precondition (before calling to_div_expr it is your responsibility to check you have an exprt with id() == ID_div) and a general data structure invariant (all ID_div exprts should have exactly two operands). A few invariants are commented out as I believe they hold but they are not currently enforced. This commit should not change the functionality of the code.

These also serve as examples of which annotations to use.

martin-cs mentioned this pull request May 11, 2017

replace assert() #182

Closed

peterschrammel reviewed May 11, 2017

View reviewed changes

martin-cs force-pushed the feature/internal-invariant branch 2 times, most recently from 85d2a39 to 5c0a0a0 Compare May 11, 2017 23:35

martin-cs force-pushed the feature/internal-invariant branch 2 times, most recently from fcea86b to 3296931 Compare May 12, 2017 00:47

martin-cs force-pushed the feature/internal-invariant branch from 3296931 to 4676af7 Compare May 12, 2017 01:18

tautschnig reviewed May 12, 2017

View reviewed changes

martin-cs force-pushed the feature/internal-invariant branch 2 times, most recently from e0ca64c to 143ab80 Compare May 12, 2017 12:44

martin-cs force-pushed the feature/internal-invariant branch 3 times, most recently from 5eb96c2 to 265e143 Compare May 17, 2017 22:26

tautschnig approved these changes May 18, 2017

View reviewed changes

reuk reviewed May 18, 2017

View reviewed changes

martin-cs force-pushed the feature/internal-invariant branch from 265e143 to ab9dd02 Compare May 18, 2017 10:48

tautschnig mentioned this pull request Jun 5, 2017

Fix endless loop bug #979

Closed

martin-cs force-pushed the feature/internal-invariant branch from ab9dd02 to f328e08 Compare June 9, 2017 10:47

peterschrammel reviewed Jun 9, 2017

View reviewed changes

martin added 2 commits June 13, 2017 10:51

A new macro based replacement for assert().

b290a9e

Abnormal termination is no longer an automatic test failure.

668dbfa

This allows us to have tests that are intended to abort. Given that tests can (and mostly do) check the exit code this should not reduce the utility of the test system.

martin-cs force-pushed the feature/internal-invariant branch from f328e08 to f16c3d8 Compare June 13, 2017 10:59

martin added 6 commits June 13, 2017 16:11

Add an (undocumented) option to test out what happens if an invariant…

720e0f8

… fails.

Get the linter to check for assertions and give a deprecated warning.

975b5a3

Remove clashing parts of my previous implementation.

0a60788

Add conversion functions for ID_bitnot.

f77b843

Replace assertions in some core libraries.

cbe7de3

These also serve as examples of which annotations to use.

martin-cs force-pushed the feature/internal-invariant branch from f16c3d8 to cbe7de3 Compare June 13, 2017 15:12

kroening merged commit ae74767 into diffblue:master Jun 13, 2017


		\*******************************************************************/

		static bool output_demangled_name (std::ostream &out, const char * const stack_entry)


		\*******************************************************************/

		static bool output_demangled_name(std::ostream &out,


		std::string working(stack_entry);

		size_t start = working.rfind('('); // Path may contain '(' !

		#define INVARIANT(CONDITION, REASON) \
		__CPROVER_assert((CONDITION), "Invariant : " REASON)


		/*******************************************************************\

		Function: check_invariant

		#include <string>
		#include <sstream>

Feature/internal invariant #911

Feature/internal invariant #911

Conversation

martin-cs commented May 11, 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

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

martin-cs commented May 11, 2017 • edited Loading

martin-cs commented May 12, 2017

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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 12, 2017

tautschnig commented May 12, 2017

reuk commented May 12, 2017 • edited Loading

tautschnig commented May 12, 2017

reuk commented May 12, 2017

tautschnig commented May 12, 2017

reuk commented May 12, 2017 • edited Loading

martin-cs commented May 12, 2017 via email

reuk commented May 12, 2017

tautschnig commented May 12, 2017

martin-cs commented May 12, 2017 via email

martin-cs commented May 17, 2017

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk May 18, 2017 • edited Loading

Choose a reason for hiding this comment

reuk May 18, 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

martin-cs commented May 11, 2017 •

edited

Loading

reuk commented May 12, 2017 •

edited

Loading

reuk commented May 12, 2017 •

edited

Loading

reuk May 18, 2017 •

edited

Loading

reuk May 18, 2017 •

edited

Loading