invariant.h

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

Module:

Author: Martin Brain, martin.brain@diffblue.com

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

#ifndef CPROVER_UTIL_INVARIANT_H
#define CPROVER_UTIL_INVARIANT_H

#include <stdexcept>
#include <type_traits>
#include <string>
#include <cstdlib>

/*
** Invariants document conditions that the programmer believes to
** be always true as a consequence of the system architecture and / or
** preceeding code.  In principle it should be possible to (machine
** checked) verify them.  The condition should be side-effect free and
** evaluate to a boolean.
**
** As well as the condition they have a text argument that should be
** used to say why they are true.  The reason should be a string literals.
** Longer diagnostics should be output to error(). For example:
**
** INVARIANT(x > 0, "x negative and zero case handled by other branches");
**
** To help classify different kinds of invariants, various short-hand
** macros are provided.
**
** Invariants are used to document and check design / implementation
** knowledge.  They should *not* be used:
**  - to validate user input or options
**    (throw an exception or handle more gracefully)
**  - to log information (use debug(), progress(), etc.)
**  - as TODO notes (acceptable in private repositories but fix before PR)
**  - to handle cases that are unlikely, tedious or expensive (ditto)
**  - to modify the state of the system (i.e. no side effects)
**
** Invariants provide the following guarantee:
**  IF the condition is false
**  THEN an invariant_failed exception will be thrown
**       OR there will be undefined behaviour
**
** Consequentally, programmers may assume that the condition of an
** invariant is true after it has been executed.  Applications are
** encouraged to (at least) catch exceptions at the top level and
** output them.
**
** Various different approaches to checking (or not) the invariants
** and handling their failure are supported and can be configured with
** CPROVER_INVARIANT_* macros.
*/

/// A logic error, augmented with a distinguished field to hold a backtrace.
/// Classes that extend this one should share the same initial constructor
/// parameters: their constructor signature should be of the form:
/// my_invariantt::my_invariantt(
///   const std::string &file,
///   const std::string &function,
///   int line,
///   const std::string &backtrace,
///   T1 arg1,
///   T2 arg2 ...
///   Tn argn)
/// It should pretty-print the T1 ... Tn arguments and pass it as `reason` to
/// invariant_failedt's constructor, or else simply pass a reason string
/// through.
/// Conforming to this pattern allows the class to be used with the INVARIANT
/// family of macros, allowing constructs like
/// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)`
///
class invariant_failedt: public std::logic_error
{
 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 reason;

  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)
  {
  }
};

#if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
// Used to allow CPROVER to check itself
#define INVARIANT(CONDITION, REASON) \
  __CPROVER_assert((CONDITION), "Invariant : " REASON)


#elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
// For performance builds, invariants can be ignored
// 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)

#elif defined(CPROVER_INVARIANT_ASSERT)
// Not recommended but provided for backwards compatability
#include <cassert>
// NOLINTNEXTLINE(*)
#define INVARIANT(CONDITION, REASON, ...) assert((CONDITION) && ((REASON), true))

#else

void print_backtrace(std::ostream &out);

std::string get_backtrace();

void report_exception_to_stderr(const invariant_failedt &);

/// Takes a backtrace, gives it to the reason structure, then aborts, printing
/// reason.what() (which therefore includes the backtrace).
/// In future this may throw `reason` instead of aborting.
/// Template parameter ET: type of exception to construct
/// \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 params : (variadic) parameters to forward to ET's constructor
///  its backtrace member will be set before it is used.
template<class ET, typename ...Params>
#ifdef __GNUC__
__attribute__((noreturn))
#endif
typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
invariant_violated_structured(
  const std::string &file,
  const std::string &function,
  const int line,
  Params &&... params)
{
  std::string backtrace=get_backtrace();
  ET to_throw(file, function, line, backtrace, 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);
  abort();
}

/// Takes a backtrace, constructs an invariant_violatedt from reason and the
/// backtrace, aborts printing the invariant's description.
/// In future this may throw rather than aborting.
/// \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 reason : brief description of the invariant violation.
#ifdef __GNUC__
__attribute__((noreturn))
#endif
inline void invariant_violated_string(
  const std::string &file,
  const std::string &function,
  const int line,
  const std::string &reason)
{
  invariant_violated_structured<invariant_failedt>(
    file,
    function,
    line,
    reason);
}

// These require a trailing semicolon by the user, such that INVARIANT
// behaves syntactically like a function call.
// NOLINT as macro definitions confuse the linter it seems.
#ifdef _MSC_VER
#define __this_function__ __FUNCTION__
#else
#define __this_function__ __func__
#endif

#define INVARIANT(CONDITION, REASON) \
  do /* NOLINT */ \
  { \
  if(!(CONDITION)) \
    invariant_violated_string(__FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */  \
  } while(0)

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

#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block

// Short hand macros. The second variant of each one permits including an
// explanation or structured exception, in which case they are synonyms
// for INVARIANT.

// The condition should only contain (unmodified) arguments to the method.
// "The design of the system means that the arguments to this method
//  will always meet this condition".
#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".
#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

// The condition should only contain (unmodified) values that were
// changed by a previous method call.
// "The contract of the previous method call means the following
//  condition holds".
#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...)  \
  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

// This should be used to mark dead code
#define UNREACHABLE INVARIANT(false, "Unreachable")
#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
  INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)

// This condition should be used to document that assumptions that are
// made on goto_functions, goto_programs, exprts, etc. being well formed.
// "The data structure is corrupt or malformed"
#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)

// Legacy annotations

// The following should not be used in new code and are only intended
// 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")

#endif // CPROVER_UTIL_INVARIANT_H