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 
73 
76 {
77  bool old_state;
79  {
81  }
82 
84  {
86  }
87 };
88 
111 {
112  private:
113  const std::string file;
114  const std::string function;
115  const int line;
116  const std::string backtrace;
117  const std::string condition;
118  const std::string reason;
119 
120 public:
121  virtual ~invariant_failedt() = default;
122 
123  virtual std::string what() const noexcept;
124 
126  const std::string &_file,
127  const std::string &_function,
128  int _line,
129  const std::string &_backtrace,
130  const std::string &_condition,
131  const std::string &_reason)
132  : file(_file),
133  function(_function),
134  line(_line),
135  backtrace(_backtrace),
136  condition(_condition),
137  reason(_reason)
138  {
139  }
140 };
141 
145 {
146 private:
147  const std::string diagnostics;
148 
149 public:
150  virtual std::string what() const noexcept;
151 
153  const std::string &_file,
154  const std::string &_function,
155  int _line,
156  const std::string &_backtrace,
157  const std::string &_condition,
158  const std::string &_reason,
159  const std::string &_diagnostics)
161  _file,
162  _function,
163  _line,
164  _backtrace,
165  _condition,
166  _reason),
167  diagnostics(_diagnostics)
168  {
169  }
170 };
171 
172 #ifdef __GNUC__
173 #define CBMC_NORETURN __attribute((noreturn))
174 #elif defined(_MSC_VER)
175 #define CBMC_NORETURN __declspec(noreturn)
176 #elif __cplusplus >= 201703L
177 #define CBMC_NORETURN [[noreturn]]
178 #else
179 #define CBMC_NORETURN
180 #endif
181 
182 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
183 // Used to allow CPROVER to check itself
184 #define INVARIANT(CONDITION, REASON) \
185  __CPROVER_assert((CONDITION), "Invariant : " REASON)
186 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
187  __CPROVER_assert((CONDITION), "Invariant : " REASON)
188 
189 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
190  INVARIANT(CONDITION, "")
191 
192 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
193 // For performance builds, invariants can be ignored
194 // This is *not* recommended as it can result in unpredictable behaviour
195 // including silently reporting incorrect results.
196 // This is also useful for checking side-effect freedom.
197 #define INVARIANT(CONDITION, REASON) \
198  do \
199  { \
200  } while(false)
201 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
202  do \
203  { \
204  } while(false)
205 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
206 
207 #elif defined(CPROVER_INVARIANT_ASSERT)
208 // Not recommended but provided for backwards compatability
209 #include <cassert>
210 // NOLINTNEXTLINE(*)
211 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
212 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
213  assert((CONDITION) && ((REASON), true)) /* NOLINT */
214 // NOLINTNEXTLINE(*)
215 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
216 #else
217 
218 void print_backtrace(std::ostream &out);
219 
220 std::string get_backtrace();
221 
223 
237 template <class ET, typename... Params>
239  typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
241  const std::string &file,
242  const std::string &function,
243  const int line,
244  const std::string &condition,
245  Params &&... params)
246 {
247  std::string backtrace=get_backtrace();
248  ET to_throw(
249  file,
250  function,
251  line,
252  backtrace,
253  condition,
254  std::forward<Params>(params)...);
255 
257  throw to_throw;
258  else
259  {
260  report_exception_to_stderr(to_throw);
261  abort();
262  }
263 }
264 
275 inline void
277  const std::string &file,
278  const std::string &function,
279  const int line,
280  const std::string &condition,
281  const std::string &reason)
282 {
283  invariant_violated_structured<invariant_failedt>(
284  file, function, line, condition, reason);
285 }
286 
287 namespace detail
288 {
289 template <typename T>
290 struct always_falset : public std::false_type
291 {
292 };
293 } // namespace detail
294 
298 template <typename T>
300 {
301  // silly construct because C++ won't let us write static_assert(false,...)
302  static_assert(
304  "to avoid unintended strangeness, diagnostics_helpert needs to be "
305  "specialised for each diagnostic type");
306  static std::string diagnostics_as_string(const T &);
307 };
308 
309 // Standard string specialisations for diagnostics_helper
310 // (character arrays, character pointers and std::string)
311 
312 template <std::size_t N>
313 struct diagnostics_helpert<char[N]>
314 {
315  static std::string diagnostics_as_string(const char (&string)[N])
316  {
317  return string;
318  }
319 };
320 template <>
321 struct diagnostics_helpert<char *>
322 {
323  static std::string diagnostics_as_string(const char *string)
324  {
325  return string;
326  }
327 };
328 
329 template <>
330 struct diagnostics_helpert<std::string>
331 {
332  // This is deliberately taking a copy instead of a reference
333  // to avoid making an extra copy when passing a temporary string
334  // as a diagnostic
335  static std::string diagnostics_as_string(std::string string)
336  {
337  return string;
338  }
339 };
340 
341 namespace detail
342 {
343 inline std::string assemble_diagnostics()
344 {
345  return "";
346 }
347 
348 template <typename T>
349 std::string diagnostic_as_string(T &&val)
350 {
351  return diagnostics_helpert<
352  typename std::remove_cv<typename std::remove_reference<T>::type>::type>::
353  diagnostics_as_string(std::forward<T>(val));
354 }
355 
356 inline void write_rest_diagnostics(std::ostream &)
357 {
358 }
359 
360 template <typename T, typename... Ts>
361 void write_rest_diagnostics(std::ostream &out, T &&next, Ts &&... rest)
362 {
363  out << "\n" << diagnostic_as_string(std::forward<T>(next));
364  write_rest_diagnostics(out, std::forward<Ts>(rest)...);
365 }
366 
367 template <typename... Diagnostics>
368 std::string assemble_diagnostics(Diagnostics &&... args)
369 {
370  std::ostringstream out;
371  out << "\n<< EXTRA DIAGNOSTICS >>";
372  write_rest_diagnostics(out, std::forward<Diagnostics>(args)...);
373  out << "\n<< END EXTRA DIAGNOSTICS >>";
374  return out.str();
375 }
376 } // namespace detail
377 
379 template <typename... Diagnostics>
381  const std::string &file,
382  const std::string &function,
383  int line,
384  std::string reason,
385  std::string condition,
386  Diagnostics &&... diagnostics)
387 {
388  invariant_violated_structured<invariant_with_diagnostics_failedt>(
389  file,
390  function,
391  line,
392  reason,
393  condition,
394  detail::assemble_diagnostics(std::forward<Diagnostics>(diagnostics)...));
395 }
396 
397 #define EXPAND_MACRO(x) x
398 
399 // These require a trailing semicolon by the user, such that INVARIANT
400 // behaves syntactically like a function call.
401 // NOLINT as macro definitions confuse the linter it seems.
402 #ifdef _MSC_VER
403 #define CURRENT_FUNCTION_NAME __FUNCTION__
404 #else
405 #define CURRENT_FUNCTION_NAME __func__
406 #endif
407 
408 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
409  do /* NOLINT */ \
410  { \
411  if(!(CONDITION)) \
412  invariant_violated_structured<TYPENAME>( \
413  __FILE__, \
414  CURRENT_FUNCTION_NAME, \
415  __LINE__, \
416  #CONDITION, \
417  __VA_ARGS__); /* NOLINT */ \
418  } while(false)
419 
420 // Short hand macros. The variants *_STRUCTURED below allow to specify a custom
421 // exception, and are equivalent to INVARIANT_STRUCTURED.
422 
424 #define INVARIANT(CONDITION, REASON) \
425  do \
426  { \
427  if(!(CONDITION)) \
428  { \
429  invariant_violated_string( \
430  __FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON); \
431  } \
432  } while(false)
433 
438 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
439  do \
440  { \
441  if(!(CONDITION)) \
442  { \
443  report_invariant_failure( \
444  __FILE__, \
445  CURRENT_FUNCTION_NAME, \
446  __LINE__, \
447  REASON, \
448  #CONDITION, \
449  __VA_ARGS__); \
450  } \
451  } while(false)
452 
453 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
454 
455 // The condition should only contain (unmodified) inputs to the method. Inputs
456 // include arguments passed to the function, as well as member variables that
457 // the function may read.
458 // "The design of the system means that the arguments to this method
459 // will always meet this condition".
460 //
461 // The PRECONDITION documents / checks assumptions about the inputs
462 // that is the caller's responsibility to make happen before the call.
463 
464 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
465 #define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
466  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)
467 
468 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
469  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
470 
471 // The condition should only contain variables that will be returned /
472 // output without further modification.
473 // "The implementation of this method means that the condition will hold".
474 //
475 // A POSTCONDITION documents what the function can guarantee about its
476 // output when it returns, given that it was called with valid inputs.
477 // Outputs include the return value of the function, as well as member
478 // variables that the function may write.
479 
480 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
481 #define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
482  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)
483 
484 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
485  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
486 
487 // The condition should only contain (unmodified) values that were
488 // changed by a previous method call.
489 // "The contract of the previous method call means the following
490 // condition holds".
491 //
492 // A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
493 // a statement about what the caller expects from a function, whereas a
494 // POSTCONDITION is a statement about guarantees made by the function itself.
495 
496 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
497 #define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) \
498  INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)
499 
500 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
501  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
502 
504 #define UNREACHABLE INVARIANT(false, "Unreachable")
505 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
506  EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
507 
511 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
512 #define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
513  INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
514 
515 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
516  EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
517 
518 // Legacy annotations
519 
520 // The following should not be used in new code and are only intended
521 // to migrate documentation and "error handling" in older code.
522 #define TODO INVARIANT(false, "Todo")
523 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
524 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
525 
526 #endif // CPROVER_UTIL_INVARIANT_H
bool cbmc_invariants_should_throw
Set this to true to cause invariants to throw a C++ exception rather than abort the program...
Definition: invariant.cpp:19
virtual std::string what() const noexcept
Definition: invariant.cpp:118
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:110
A class that includes diagnostic information related to an invariant violation.
Definition: invariant.h:144
static std::string diagnostics_as_string(std::string string)
Definition: invariant.h:335
void write_rest_diagnostics(std::ostream &)
Definition: invariant.h:356
const int line
Definition: invariant.h:115
virtual std::string what() const noexcept
Definition: invariant.cpp:130
STL namespace.
const std::string condition
Definition: invariant.h:117
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:276
void print_backtrace(std::ostream &out)
Prints a back trace to &#39;out&#39;.
Definition: invariant.cpp:79
Helper to enable invariant throwing as above bounded to an object lifetime:
Definition: invariant.h:75
virtual ~invariant_failedt()=default
#define CBMC_NORETURN
Definition: invariant.h:179
Helper to give us some diagnostic in a usable form on assertion failure.
Definition: invariant.h:299
const std::string reason
Definition: invariant.h:118
const std::string function
Definition: invariant.h:114
static std::string diagnostics_as_string(const T &)
const std::string backtrace
Definition: invariant.h:116
std::string assemble_diagnostics()
Definition: invariant.h:343
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:103
static std::string diagnostics_as_string(const char(&string)[N])
Definition: invariant.h:315
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
Definition: invariant.cpp:111
const std::string file
Definition: invariant.h:113
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:240
std::string diagnostic_as_string(T &&val)
Definition: invariant.h:349
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:380
static std::string diagnostics_as_string(const char *string)
Definition: invariant.h:323
Definition: kdev_t.h:19