Skip to content

Extra documentation and refactoring of the Invariant definitions #2666

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Aug 9, 2018
Merged

Extra documentation and refactoring of the Invariant definitions #2666

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
bf6dd9e
Added extra use-case hints to the already present invariant definitions.
NlightNFotis Jul 31, 2018
515f050
Pass the condition to the invariant_failedt constructor.
NlightNFotis Aug 1, 2018
efb1c40
Refactor invariant_failedt definition.
NlightNFotis Aug 1, 2018
4782b48
Fix invariant regression tests
NlightNFotis Aug 6, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 11 additions & 9 deletions regression/invariants/driver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,16 +40,18 @@ class structured_error_testt: public invariant_failedt
const std::string &function,
int line,
const std::string &backtrace,
const std::string &condition,
int code,
const std::string &_description):
invariant_failedt(
file,
function,
line,
backtrace,
pretty_print(code, _description)),
error_code(code),
description(_description)
const std::string &_description)
: invariant_failedt(
file,
function,
line,
backtrace,
condition,
pretty_print(code, _description)),
error_code(code),
description(_description)
{
}
};
Expand Down
20 changes: 6 additions & 14 deletions src/util/invariant.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Martin Brain, [email protected]

#include "invariant.h"

#include "util/freer.h"
#include "freer.h"

#include <memory>
#include <string>
Expand Down Expand Up @@ -79,8 +79,6 @@ void print_backtrace(
std::ostream &out)
{
#ifdef __GLIBC__
out << "Backtrace\n" << std::flush;

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Someone has finally noticed that it prints backtrace twice! :-)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or someone has finally bothered to fix it... Usually when you see this you have other worries than this ;)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How very true...

void * stack[50] = {};

std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
Expand Down Expand Up @@ -116,20 +114,14 @@ void report_exception_to_stderr(const invariant_failedt &reason)
std::cerr << "--- end invariant violation report ---\n";
}

std::string invariant_failedt::get_invariant_failed_message(
const std::string &file,
const std::string &function,
int line,
const std::string &backtrace,
const std::string &reason)
std::string invariant_failedt::what() const noexcept
{
std::ostringstream out;
out << "Invariant check failed\n"
<< "File " << file
<< " function " << function
<< " line " << line << '\n'
<< "Reason: " << reason
<< "\nBacktrace:\n"
<< "File: " << file << ":" << line << " function: " << function << '\n'
<< "Condition: " << condition << '\n'
<< "Reason: " << reason << '\n'
<< "Backtrace:" << '\n'
<< backtrace << '\n';
return out.str();
}
87 changes: 54 additions & 33 deletions src/util/invariant.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,41 +72,32 @@ Author: Martin Brain, [email protected]
/// family of macros, allowing constructs like
/// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)`
///
class invariant_failedt: public std::logic_error
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I recall someone being very emphatically passionate that this had to inherit from one of the standard exception handlers. i don't now recall why. Does anyone know? Why is it better to not do so.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The idea behind it is that we don't want a generic exception catcher

catch (exception &e)

to catch these exceptions if they propagate. Now an ellipsis (catch all - catch (...)) will still catch it, which we don't think is a good idea, but since we are not entirely sure of how further up the callstack these exceptions can propagate and where exactly (pathwise) these catchers are, we are going to fix this issue as a later part of this work.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK... at the risk of being a stuck record on this; don't over-estimate what you can do after catching an exception. If an invariant has failed then there is at least one significant, relevant bug in CPROVER. After that data structures should not be trusted and results should especially not be trusted. So... it might be that the only sensible thing to do is the same as the handlers for catch (exception &e) or catch (...). YMMV.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case, it's still my opinion that there should be a special handler that handles this type, even if it duplicates the body of the catch all handlers, even if it's only for documentation purposes - making it clear that this is desired behaviour. As it is right now, the behaviour, even if correct or the only logical one, appears to be accidental.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Up to you. As I said to start with, at one point, I recall someone being very passionate about this but I can't remember why. As long as there is a good reason; it's all good.

class invariant_failedt
{
private:
std::string get_invariant_failed_message(
const std::string &file,
const std::string &function,
int line,
const std::string &backtrace,
const std::string &reason);

public:
const std::string file;
const std::string function;
const int line;
const std::string backtrace;
const std::string condition;
const std::string reason;

public:
std::string what() const noexcept;

invariant_failedt(
const std::string &_file,
const std::string &_function,
int _line,
const std::string &_backtrace,
const std::string &_reason):
logic_error(
get_invariant_failed_message(
_file,
_function,
_line,
_backtrace,
_reason)),
file(_file),
function(_function),
line(_line),
backtrace(_backtrace),
reason(_reason)
const std::string &_condition,
const std::string &_reason)
: file(_file),
function(_function),
line(_line),
backtrace(_backtrace),
condition(_condition),
reason(_reason)
{
}
};
Expand Down Expand Up @@ -149,9 +140,10 @@ void report_exception_to_stderr(const invariant_failedt &);
/// \param file : C string giving the name of the file.
/// \param function : C string giving the name of the function.
/// \param line : The line number of the invariant
/// \param condition : the condition this invariant is checking.
/// \param params : (variadic) parameters to forward to ET's constructor
/// its backtrace member will be set before it is used.
template<class ET, typename ...Params>
template <class ET, typename... Params>
#ifdef __GNUC__
__attribute__((noreturn))
#endif
Expand All @@ -160,10 +152,17 @@ invariant_violated_structured(
const std::string &file,
const std::string &function,
const int line,
const std::string &condition,
Params &&... params)
{
std::string backtrace=get_backtrace();
ET to_throw(file, function, line, backtrace, std::forward<Params>(params)...);
ET to_throw(
file,
function,
line,
backtrace,
condition,
std::forward<Params>(params)...);
// We now have a structured exception ready to use;
// in future this is the place to put a 'throw'.
report_exception_to_stderr(to_throw);
Expand All @@ -177,20 +176,20 @@ invariant_violated_structured(
/// \param function : C string giving the name of the function.
/// \param line : The line number of the invariant
/// \param reason : brief description of the invariant violation.
/// \param condition : the condition this invariant is checking.
#ifdef __GNUC__
__attribute__((noreturn))
#endif
inline void invariant_violated_string(
inline void
invariant_violated_string(
const std::string &file,
const std::string &function,
const int line,
const std::string &reason)
const std::string &reason,
const std::string &condition)
{
invariant_violated_structured<invariant_failedt>(
file,
function,
line,
reason);
file, function, line, condition, reason);
}

// These require a trailing semicolon by the user, such that INVARIANT
Expand All @@ -207,15 +206,23 @@ inline void invariant_violated_string(
{ \
if(!(CONDITION)) \
invariant_violated_string( \
__FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */ \
__FILE__, \
__this_function__, \
__LINE__, \
(REASON), \
#CONDITION); /* NOLINT */ \
} while(false)

#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
do /* NOLINT */ \
{ \
if(!(CONDITION)) \
invariant_violated_structured<TYPENAME>( \
__FILE__, __this_function__, __LINE__, __VA_ARGS__); /* NOLINT */ \
__FILE__, \
__this_function__, \
__LINE__, \
#CONDITION, \
__VA_ARGS__); /* NOLINT */ \
} while(false)

#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
Expand All @@ -225,15 +232,25 @@ inline void invariant_violated_string(
// for INVARIANT.

// The condition should only contain (unmodified) arguments to the method.
// Inputs include arguments passed to the function, as well as member
// variables that the function may read.
// "The design of the system means that the arguments to this method
// will always meet this condition".
//
// The PRECONDITION documents / checks assumptions about the inputs
// that is the caller's responsibility to make happen before the call.
#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

// The condition should only contain variables that will be returned /
// output without further modification.
// "The implementation of this method means that the condition will hold".
//
// A POSTCONDITION documents what the function can guarantee about its
// output when it returns, given that it was called with valid inputs.
// Outputs include the return value of the function, as well as member
// variables that the function may write.
#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
Expand All @@ -242,6 +259,10 @@ inline void invariant_violated_string(
// changed by a previous method call.
// "The contract of the previous method call means the following
// condition holds".
//
// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
// a statement about what the caller expects from a function, whereas a
// POSTCONDITION is a statement about guarantees made by the function itself.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes! This is a subtle point but the key thing, as you have got, is that POSTCONDITION is the callee saying "I will always guarantee that CONDITION holds before I return" while CHECK_RETURN is the caller saying "I will assume that the called function made sure CONDITION holds". Ideally the POSTCONDITION will imply that all CHECK_RETURNs hold but the separation is to make the separation of responsibilities clear.

#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
Expand All @@ -261,7 +282,7 @@ inline void invariant_violated_string(
// Legacy annotations

// The following should not be used in new code and are only intended
// to migrate documentation and "error handling" in older code
// to migrate documentation and "error handling" in older code.
#define TODO INVARIANT(false, "Todo")
#define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
#define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
Expand Down