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 <cstdlib>
13 #include <sstream>
14 #include <stdexcept>
15 #include <string>
16 #include <type_traits>
17 
18 /*
19 ** Invariants document conditions that the programmer believes to
20 ** be always true as a consequence of the system architecture and / or
21 ** preceeding code. In principle it should be possible to (machine
22 ** checked) verify them. The condition should be side-effect free and
23 ** evaluate to a boolean.
24 **
25 ** As well as the condition they have a text argument that should be
26 ** used to say why they are true. The reason should be a string literal
27 ** starting with a lower case character.
28 ** Longer diagnostics should be output to error(). For example:
29 **
30 ** INVARIANT(
31 ** x > 0,
32 ** "x should have a positive value as others are handled by other branches");
33 **
34 ** Use "should" style statements for messages in invariants (also see
35 ** CODING_STANDARD.md). An example would be "array should have a non-zero size")
36 ** to make both the violation and the expected behavior clear. (As opposed to
37 ** "no zero size arrays" where it isn't clear if the zero-size array is the
38 ** problem, or the lack of it).
39 **
40 ** To help classify different kinds of invariants, various short-hand
41 ** macros are provided.
42 **
43 ** Invariants are used to document and check design / implementation
44 ** knowledge. They should *not* be used:
45 ** - to validate user input or options
46 ** (throw an exception or handle more gracefully)
47 ** - to log information (use debug(), progress(), etc.)
48 ** - as TODO notes (acceptable in private repositories but fix before PR)
49 ** - to handle cases that are unlikely, tedious or expensive (ditto)
50 ** - to modify the state of the system (i.e. no side effects)
51 **
52 ** Invariants provide the following guarantee:
53 ** IF the condition is false
54 ** THEN an invariant_failed exception will be thrown
55 ** OR there will be undefined behaviour
56 **
57 ** Consequentally, programmers may assume that the condition of an
58 ** invariant is true after it has been executed. Applications are
59 ** encouraged to (at least) catch exceptions at the top level and
60 ** output them.
61 **
62 ** Various different approaches to checking (or not) the invariants
63 ** and handling their failure are supported and can be configured with
64 ** CPROVER_INVARIANT_* macros.
65 */
66 
89 {
90  private:
91  const std::string file;
92  const std::string function;
93  const int line;
94  const std::string backtrace;
95  const std::string condition;
96  const std::string reason;
97 
98 public:
99  virtual ~invariant_failedt() = default;
100 
101  virtual std::string what() const noexcept;
102 
104  const std::string &_file,
105  const std::string &_function,
106  int _line,
107  const std::string &_backtrace,
108  const std::string &_condition,
109  const std::string &_reason)
110  : file(_file),
111  function(_function),
112  line(_line),
113  backtrace(_backtrace),
114  condition(_condition),
115  reason(_reason)
116  {
117  }
118 };
119 
123 {
124 private:
125  const std::string diagnostics;
126 
127 public:
128  virtual std::string what() const noexcept;
129 
131  const std::string &_file,
132  const std::string &_function,
133  int _line,
134  const std::string &_backtrace,
135  const std::string &_condition,
136  const std::string &_reason,
137  const std::string &_diagnostics)
139  _file,
140  _function,
141  _line,
142  _backtrace,
143  _condition,
144  _reason),
145  diagnostics(_diagnostics)
146  {
147  }
148 };
149 
150 #ifdef __GNUC__
151 #define CBMC_NORETURN __attribute((noreturn))
152 #elif defined(_MSC_VER)
153 #define CBMC_NORETURN __declspec(noreturn)
154 #elif __cplusplus >= 201703L
155 #define CBMC_NORETURN [[noreturn]]
156 #else
157 #define CBMC_NORETURN
158 #endif
159 
160 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
161 // Used to allow CPROVER to check itself
162 #define INVARIANT(CONDITION, REASON) \
163  __CPROVER_assert((CONDITION), "Invariant : " REASON)
164 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
165  __CPROVER_assert((CONDITION), "Invariant : " REASON)
166 
167 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
168  INVARIANT(CONDITION, "")
169 
170 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
171 // For performance builds, invariants can be ignored
172 // This is *not* recommended as it can result in unpredictable behaviour
173 // including silently reporting incorrect results.
174 // This is also useful for checking side-effect freedom.
175 #define INVARIANT(CONDITION, REASON) \
176  do \
177  { \
178  } while(false)
179 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
180  do \
181  { \
182  } while(false)
183 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
184 
185 #elif defined(CPROVER_INVARIANT_ASSERT)
186 // Not recommended but provided for backwards compatability
187 #include <cassert>
188 // NOLINTNEXTLINE(*)
189 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
190 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
191  assert((CONDITION) && ((REASON), true)) /* NOLINT */
192 // NOLINTNEXTLINE(*)
193 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
194 #else
195 
196 void print_backtrace(std::ostream &out);
197 
198 std::string get_backtrace();
199 
201 
215 template <class ET, typename... Params>
217  typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
219  const std::string &file,
220  const std::string &function,
221  const int line,
222  const std::string &condition,
223  Params &&... params)
224 {
225  std::string backtrace=get_backtrace();
226  ET to_throw(
227  file,
228  function,
229  line,
230  backtrace,
231  condition,
232  std::forward<Params>(params)...);
233  // We now have a structured exception ready to use;
234  // in future this is the place to put a 'throw'.
235  report_exception_to_stderr(to_throw);
236  abort();
237 }
238 
249 inline void
251  const std::string &file,
252  const std::string &function,
253  const int line,
254  const std::string &condition,
255  const std::string &reason)
256 {
257  invariant_violated_structured<invariant_failedt>(
258  file, function, line, condition, reason);
259 }
260 
261 namespace detail
262 {
263 template <typename T>
264 struct always_falset : public std::false_type
265 {
266 };
267 } // namespace detail
268 
272 template <typename T>
274 {
275  // silly construct because C++ won't let us write static_assert(false,...)
276  static_assert(
278  "to avoid unintended strangeness, diagnostics_helpert needs to be "
279  "specialised for each diagnostic type");
280  static std::string diagnostics_as_string(const T &);
281 };
282 
283 // Standard string specialisations for diagnostics_helper
284 // (character arrays, character pointers and std::string)
285 
286 template <std::size_t N>
287 struct diagnostics_helpert<char[N]>
288 {
289  static std::string diagnostics_as_string(const char (&string)[N])
290  {
291  return string;
292  }
293 };
294 template <>
295 struct diagnostics_helpert<char *>
296 {
297  static std::string diagnostics_as_string(const char *string)
298  {
299  return string;
300  }
301 };
302 
303 template <>
304 struct diagnostics_helpert<std::string>
305 {
306  // This is deliberately taking a copy instead of a reference
307  // to avoid making an extra copy when passing a temporary string
308  // as a diagnostic
309  static std::string diagnostics_as_string(std::string string)
310  {
311  return string;
312  }
313 };
314 
315 namespace detail
316 {
317 inline std::string assemble_diagnostics()
318 {
319  return "";
320 }
321 
322 template <typename T>
323 std::string diagnostic_as_string(T &&val)
324 {
325  return diagnostics_helpert<
326  typename std::remove_cv<typename std::remove_reference<T>::type>::type>::
327  diagnostics_as_string(std::forward<T>(val));
328 }
329 
330 inline void write_rest_diagnostics(std::ostream &)
331 {
332 }
333 
334 template <typename T, typename... Ts>
335 void write_rest_diagnostics(std::ostream &out, T &&next, Ts &&... rest)
336 {
337  out << "\n" << diagnostic_as_string(std::forward<T>(next));
338  write_rest_diagnostics(out, std::forward<Ts>(rest)...);
339 }
340 
341 template <typename... Diagnostics>
342 std::string assemble_diagnostics(Diagnostics &&... args)
343 {
344  std::ostringstream out;
345  out << "\n<< EXTRA DIAGNOSTICS >>";
346  write_rest_diagnostics(out, std::forward<Diagnostics>(args)...);
347  out << "\n<< END EXTRA DIAGNOSTICS >>";
348  return out.str();
349 }
350 } // namespace detail
351 
353 template <typename... Diagnostics>
355  const std::string &file,
356  const std::string &function,
357  int line,
358  std::string reason,
359  std::string condition,
360  Diagnostics &&... diagnostics)
361 {
362  invariant_violated_structured<invariant_with_diagnostics_failedt>(
363  file,
364  function,
365  line,
366  reason,
367  condition,
368  detail::assemble_diagnostics(std::forward<Diagnostics>(diagnostics)...));
369 }
370 
371 #define EXPAND_MACRO(x) x
372 
373 // These require a trailing semicolon by the user, such that INVARIANT
374 // behaves syntactically like a function call.
375 // NOLINT as macro definitions confuse the linter it seems.
376 #ifdef _MSC_VER
377 #define CURRENT_FUNCTION_NAME __FUNCTION__
378 #else
379 #define CURRENT_FUNCTION_NAME __func__
380 #endif
381 
382 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
383  do /* NOLINT */ \
384  { \
385  if(!(CONDITION)) \
386  invariant_violated_structured<TYPENAME>( \
387  __FILE__, \
388  CURRENT_FUNCTION_NAME, \
389  __LINE__, \
390  #CONDITION, \
391  __VA_ARGS__); /* NOLINT */ \
392  } while(false)
393 
394 // Short hand macros. The variants *_STRUCTURED below allow to specify a custom
395 // exception, and are equivalent to INVARIANT_STRUCTURED.
396 
398 #define INVARIANT(CONDITION, REASON) \
399  do \
400  { \
401  if(!(CONDITION)) \
402  { \
403  invariant_violated_string( \
404  __FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON); \
405  } \
406  } while(false)
407 
412 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
413  do \
414  { \
415  if(!(CONDITION)) \
416  { \
417  report_invariant_failure( \
418  __FILE__, \
419  CURRENT_FUNCTION_NAME, \
420  __LINE__, \
421  REASON, \
422  #CONDITION, \
423  __VA_ARGS__); \
424  } \
425  } while(false)
426 
427 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
428 
429 // The condition should only contain (unmodified) inputs to the method. Inputs
430 // include arguments passed to the function, as well as member variables that
431 // the function may read.
432 // "The design of the system means that the arguments to this method
433 // will always meet this condition".
434 //
435 // The PRECONDITION documents / checks assumptions about the inputs
436 // that is the caller's responsibility to make happen before the call.
437 
438 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
439 #define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
440  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)
441 
442 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
443  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
444 
445 // The condition should only contain variables that will be returned /
446 // output without further modification.
447 // "The implementation of this method means that the condition will hold".
448 //
449 // A POSTCONDITION documents what the function can guarantee about its
450 // output when it returns, given that it was called with valid inputs.
451 // Outputs include the return value of the function, as well as member
452 // variables that the function may write.
453 
454 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
455 #define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
456  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)
457 
458 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
459  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
460 
461 // The condition should only contain (unmodified) values that were
462 // changed by a previous method call.
463 // "The contract of the previous method call means the following
464 // condition holds".
465 //
466 // A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
467 // a statement about what the caller expects from a function, whereas a
468 // POSTCONDITION is a statement about guarantees made by the function itself.
469 
470 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
471 #define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) \
472  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)
473 
474 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
475  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
476 
478 #define UNREACHABLE INVARIANT(false, "Unreachable")
479 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
480  EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
481 
485 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
486 #define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
487  INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
488 
489 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
490  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
491 
492 // Legacy annotations
493 
494 // The following should not be used in new code and are only intended
495 // to migrate documentation and "error handling" in older code.
496 #define TODO INVARIANT(false, "Todo")
497 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
498 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
499 
500 #endif // CPROVER_UTIL_INVARIANT_H
virtual std::string what() const noexcept
Definition: invariant.cpp:117
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:88
A class that includes diagnostic information related to an invariant violation.
Definition: invariant.h:122
static std::string diagnostics_as_string(std::string string)
Definition: invariant.h:309
void write_rest_diagnostics(std::ostream &)
Definition: invariant.h:330
const int line
Definition: invariant.h:93
virtual std::string what() const noexcept
Definition: invariant.cpp:129
STL namespace.
const std::string condition
Definition: invariant.h:95
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &condition, const std::string &reason)
This is a wrapper function used by the macro &#39;INVARIANT(CONDITION, REASON)&#39;.
Definition: invariant.h:250
void print_backtrace(std::ostream &out)
Prints a back trace to &#39;out&#39;.
Definition: invariant.cpp:78
virtual ~invariant_failedt()=default
#define CBMC_NORETURN
Definition: invariant.h:157
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:273
const std::string reason
Definition: invariant.h:96
const std::string function
Definition: invariant.h:92
static std::string diagnostics_as_string(const T &)
const std::string backtrace
Definition: invariant.h:94
std::string assemble_diagnostics()
Definition: invariant.h:317
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:102
static std::string diagnostics_as_string(const char(&string)[N])
Definition: invariant.h:289
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
Definition: invariant.cpp:110
const std::string file
Definition: invariant.h:91
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, const std::string &condition, Params &&... params)
This function is the backbone of all the invariant types.
Definition: invariant.h:218
std::string diagnostic_as_string(T &&val)
Definition: invariant.h:323
void report_invariant_failure(const std::string &file, const std::string &function, int line, std::string reason, std::string condition, Diagnostics &&... diagnostics)
This is a wrapper function, used by the macro &#39;INVARIANT_WITH_DIAGNOSTICS&#39;.
Definition: invariant.h:354
static std::string diagnostics_as_string(const char *string)
Definition: invariant.h:297
Definition: kdev_t.h:19