cprover
invariant.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Martin Brain, martin.brain@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_INVARIANT_H
10 #define CPROVER_UTIL_INVARIANT_H
11 
12 #include <stdexcept>
13 #include <type_traits>
14 #include <string>
15 #include <cstdlib>
16 
17 /*
18 ** Invariants document conditions that the programmer believes to
19 ** be always true as a consequence of the system architecture and / or
20 ** preceeding code. In principle it should be possible to (machine
21 ** checked) verify them. The condition should be side-effect free and
22 ** evaluate to a boolean.
23 **
24 ** As well as the condition they have a text argument that should be
25 ** used to say why they are true. The reason should be a string literals.
26 ** Longer diagnostics should be output to error(). For example:
27 **
28 ** INVARIANT(x > 0, "x negative and zero case handled by other branches");
29 **
30 ** To help classify different kinds of invariants, various short-hand
31 ** macros are provided.
32 **
33 ** Invariants are used to document and check design / implementation
34 ** knowledge. They should *not* be used:
35 ** - to validate user input or options
36 ** (throw an exception or handle more gracefully)
37 ** - to log information (use debug(), progress(), etc.)
38 ** - as TODO notes (acceptable in private repositories but fix before PR)
39 ** - to handle cases that are unlikely, tedious or expensive (ditto)
40 ** - to modify the state of the system (i.e. no side effects)
41 **
42 ** Invariants provide the following guarantee:
43 ** IF the condition is false
44 ** THEN an invariant_failed exception will be thrown
45 ** OR there will be undefined behaviour
46 **
47 ** Consequentally, programmers may assume that the condition of an
48 ** invariant is true after it has been executed. Applications are
49 ** encouraged to (at least) catch exceptions at the top level and
50 ** output them.
51 **
52 ** Various different approaches to checking (or not) the invariants
53 ** and handling their failure are supported and can be configured with
54 ** CPROVER_INVARIANT_* macros.
55 */
56 
75 class invariant_failedt: public std::logic_error
76 {
77  private:
78  std::string get_invariant_failed_message(
79  const std::string &file,
80  const std::string &function,
81  int line,
82  const std::string &backtrace,
83  const std::string &reason);
84 
85  public:
86 
87  const std::string file;
88  const std::string function;
89  const int line;
90  const std::string backtrace;
91  const std::string reason;
92 
94  const std::string &_file,
95  const std::string &_function,
96  int _line,
97  const std::string &_backtrace,
98  const std::string &_reason):
99  logic_error(
100  get_invariant_failed_message(
101  _file,
102  _function,
103  _line,
104  _backtrace,
105  _reason)),
106  file(_file),
107  function(_function),
108  line(_line),
109  backtrace(_backtrace),
110  reason(_reason)
111  {
112  }
113 };
114 
115 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
116 // Used to allow CPROVER to check itself
117 #define INVARIANT(CONDITION, REASON) \
118  __CPROVER_assert((CONDITION), "Invariant : " REASON)
119 
120 
121 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
122 // For performance builds, invariants can be ignored
123 // This is *not* recommended as it can result in unpredictable behaviour
124 // including silently reporting incorrect results.
125 // This is also useful for checking side-effect freedom.
126 #define INVARIANT(CONDITION, REASON, ...) do {} while(0)
127 
128 #elif defined(CPROVER_INVARIANT_ASSERT)
129 // Not recommended but provided for backwards compatability
130 #include <cassert>
131 // NOLINTNEXTLINE(*)
132 #define INVARIANT(CONDITION, REASON, ...) assert((CONDITION) && ((REASON), true))
133 
134 #else
135 
136 void print_backtrace(std::ostream &out);
137 
138 std::string get_backtrace();
139 
141 
151 template<class ET, typename ...Params>
152 #ifdef __GNUC__
153 __attribute__((noreturn))
154 #endif
155 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
157  const std::string &file,
158  const std::string &function,
159  const int line,
160  Params &&... params)
161 {
162  std::string backtrace=get_backtrace();
163  ET to_throw(file, function, line, backtrace, std::forward<Params>(params)...);
164  // We now have a structured exception ready to use;
165  // in future this is the place to put a 'throw'.
166  report_exception_to_stderr(to_throw);
167  abort();
168 }
169 
177 #ifdef __GNUC__
178 __attribute__((noreturn))
179 #endif
181  const std::string &file,
182  const std::string &function,
183  const int line,
184  const std::string &reason)
185 {
186  invariant_violated_structured<invariant_failedt>(
187  file,
188  function,
189  line,
190  reason);
191 }
192 
193 // These require a trailing semicolon by the user, such that INVARIANT
194 // behaves syntactically like a function call.
195 // NOLINT as macro definitions confuse the linter it seems.
196 #ifdef _MSC_VER
197 #define __this_function__ __FUNCTION__
198 #else
199 #define __this_function__ __func__
200 #endif
201 
202 #define INVARIANT(CONDITION, REASON) \
203  do /* NOLINT */ \
204  { \
205  if(!(CONDITION)) \
206  invariant_violated_string(__FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */ \
207  } while(0)
208 
209 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
210  do /* NOLINT */ \
211  { \
212  if(!(CONDITION)) \
213  invariant_violated_structured<TYPENAME>(__FILE__, __this_function__, __LINE__, __VA_ARGS__); /* NOLINT */ \
214  } while(0)
215 
216 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
217 
218 // Short hand macros. The second variant of each one permits including an
219 // explanation or structured exception, in which case they are synonyms
220 // for INVARIANT.
221 
222 // The condition should only contain (unmodified) arguments to the method.
223 // "The design of the system means that the arguments to this method
224 // will always meet this condition".
225 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
226 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
227  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
228 
229 // The condition should only contain variables that will be returned /
230 // output without further modification.
231 // "The implementation of this method means that the condition will hold".
232 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
233 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
234  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
235 
236 // The condition should only contain (unmodified) values that were
237 // changed by a previous method call.
238 // "The contract of the previous method call means the following
239 // condition holds".
240 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
241 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
242  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
243 
244 // This should be used to mark dead code
245 #define UNREACHABLE INVARIANT(false, "Unreachable")
246 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
247  INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
248 
249 // This condition should be used to document that assumptions that are
250 // made on goto_functions, goto_programs, exprts, etc. being well formed.
251 // "The data structure is corrupt or malformed"
252 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
253 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
254  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
255 
256 // Legacy annotations
257 
258 // The following should not be used in new code and are only intended
259 // to migrate documentation and "error handling" in older code
260 #define TODO INVARIANT(0, "Todo")
261 #define UNIMPLEMENTED INVARIANT(0, "Unimplemented")
262 #define UNHANDLED_CASE INVARIANT(0, "Unhandled case")
263 
264 #endif // CPROVER_UTIL_INVARIANT_H
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:75
std::string get_invariant_failed_message(const std::string &file, const std::string &function, int line, const std::string &backtrace, const std::string &reason)
Definition: invariant.cpp:119
const int line
Definition: invariant.h:89
void print_backtrace(std::ostream &out)
Prints a back trace to &#39;out&#39;.
Definition: invariant.cpp:77
float __gcc_v4sf __attribute__((__vector_size__(16)))
const std::string reason
Definition: invariant.h:91
const std::string function
Definition: invariant.h:88
const std::string backtrace
Definition: invariant.h:90
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:104
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
Definition: invariant.cpp:112
const std::string file
Definition: invariant.h:87
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &reason)
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant&#39;s description.
Definition: invariant.h:180
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)
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace).
Definition: invariant.h:156
invariant_failedt(const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_reason)
Definition: invariant.h:93
Definition: kdev_t.h:19