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 
76 {
77  private:
78  const std::string file;
79  const std::string function;
80  const int line;
81  const std::string backtrace;
82  const std::string condition;
83  const std::string reason;
84 
85 public:
86  std::string what() const noexcept;
87 
89  const std::string &_file,
90  const std::string &_function,
91  int _line,
92  const std::string &_backtrace,
93  const std::string &_condition,
94  const std::string &_reason)
95  : file(_file),
96  function(_function),
97  line(_line),
98  backtrace(_backtrace),
99  condition(_condition),
100  reason(_reason)
101  {
102  }
103 };
104 
105 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
106 // Used to allow CPROVER to check itself
107 #define INVARIANT(CONDITION, REASON) \
108  __CPROVER_assert((CONDITION), "Invariant : " REASON)
109 
110 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
111  INVARIANT(CONDITION, "")
112 
113 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
114 // For performance builds, invariants can be ignored
115 // This is *not* recommended as it can result in unpredictable behaviour
116 // including silently reporting incorrect results.
117 // This is also useful for checking side-effect freedom.
118 #define INVARIANT(CONDITION, REASON) do {} while(false)
119 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
120 
121 #elif defined(CPROVER_INVARIANT_ASSERT)
122 // Not recommended but provided for backwards compatability
123 #include <cassert>
124 // NOLINTNEXTLINE(*)
125 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
126 // NOLINTNEXTLINE(*)
127 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
128 #else
129 
130 void print_backtrace(std::ostream &out);
131 
132 std::string get_backtrace();
133 
135 
146 template <class ET, typename... Params>
147 #ifdef __GNUC__
148 __attribute__((noreturn))
149 #endif
150 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
152  const std::string &file,
153  const std::string &function,
154  const int line,
155  const std::string &condition,
156  Params &&... params)
157 {
158  std::string backtrace=get_backtrace();
159  ET to_throw(
160  file,
161  function,
162  line,
163  backtrace,
164  condition,
165  std::forward<Params>(params)...);
166  // We now have a structured exception ready to use;
167  // in future this is the place to put a 'throw'.
168  report_exception_to_stderr(to_throw);
169  abort();
170 }
171 
180 #ifdef __GNUC__
181 __attribute__((noreturn))
182 #endif
183 inline void
185  const std::string &file,
186  const std::string &function,
187  const int line,
188  const std::string &reason,
189  const std::string &condition)
190 {
191  invariant_violated_structured<invariant_failedt>(
192  file, function, line, condition, reason);
193 }
194 
195 // These require a trailing semicolon by the user, such that INVARIANT
196 // behaves syntactically like a function call.
197 // NOLINT as macro definitions confuse the linter it seems.
198 #ifdef _MSC_VER
199 #define __this_function__ __FUNCTION__
200 #else
201 #define __this_function__ __func__
202 #endif
203 
204 #define INVARIANT(CONDITION, REASON) \
205  do /* NOLINT */ \
206  { \
207  if(!(CONDITION)) \
208  invariant_violated_string( \
209  __FILE__, \
210  __this_function__, \
211  __LINE__, \
212  (REASON), \
213  #CONDITION); /* NOLINT */ \
214  } while(false)
215 
216 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
217  do /* NOLINT */ \
218  { \
219  if(!(CONDITION)) \
220  invariant_violated_structured<TYPENAME>( \
221  __FILE__, \
222  __this_function__, \
223  __LINE__, \
224  #CONDITION, \
225  __VA_ARGS__); /* NOLINT */ \
226  } while(false)
227 
228 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
229 
230 // Short hand macros. The second variant of each one permits including an
231 // explanation or structured exception, in which case they are synonyms
232 // for INVARIANT.
233 
234 // The condition should only contain (unmodified) arguments to the method.
235 // Inputs include arguments passed to the function, as well as member
236 // variables that the function may read.
237 // "The design of the system means that the arguments to this method
238 // will always meet this condition".
239 //
240 // The PRECONDITION documents / checks assumptions about the inputs
241 // that is the caller's responsibility to make happen before the call.
242 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
243 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
244  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
245 
246 // The condition should only contain variables that will be returned /
247 // output without further modification.
248 // "The implementation of this method means that the condition will hold".
249 //
250 // A POSTCONDITION documents what the function can guarantee about its
251 // output when it returns, given that it was called with valid inputs.
252 // Outputs include the return value of the function, as well as member
253 // variables that the function may write.
254 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
255 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
256  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
257 
258 // The condition should only contain (unmodified) values that were
259 // changed by a previous method call.
260 // "The contract of the previous method call means the following
261 // condition holds".
262 //
263 // A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
264 // a statement about what the caller expects from a function, whereas a
265 // POSTCONDITION is a statement about guarantees made by the function itself.
266 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
267 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
268  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
269 
270 // This should be used to mark dead code
271 #define UNREACHABLE INVARIANT(false, "Unreachable")
272 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
273  INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
274 
275 // This condition should be used to document that assumptions that are
276 // made on goto_functions, goto_programs, exprts, etc. being well formed.
277 // "The data structure is corrupt or malformed"
278 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
279 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
280  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
281 
282 // Legacy annotations
283 
284 // The following should not be used in new code and are only intended
285 // to migrate documentation and "error handling" in older code.
286 #define TODO INVARIANT(false, "Todo")
287 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
288 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
289 
290 #endif // CPROVER_UTIL_INVARIANT_H
std::string what() const noexcept
Definition: invariant.cpp:117
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:75
const int line
Definition: invariant.h:80
STL namespace.
const std::string condition
Definition: invariant.h:82
void print_backtrace(std::ostream &out)
Prints a back trace to &#39;out&#39;.
Definition: invariant.cpp:78
int __gcc_m64 __attribute__((__vector_size__(8), __may_alias__))
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &reason, const std::string &condition)
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant&#39;s description.
Definition: invariant.h:184
const std::string reason
Definition: invariant.h:83
const std::string function
Definition: invariant.h:79
const std::string backtrace
Definition: invariant.h:81
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:102
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
Definition: invariant.cpp:110
const std::string file
Definition: invariant.h:78
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)
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace).
Definition: invariant.h:151
Definition: kdev_t.h:19