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