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  const std::string file;
87  const std::string function;
88  const int line;
89  const std::string backtrace;
90  const std::string reason;
91 
93  const std::string &_file,
94  const std::string &_function,
95  int _line,
96  const std::string &_backtrace,
97  const std::string &_reason):
98  logic_error(
100  _file,
101  _function,
102  _line,
103  _backtrace,
104  _reason)),
105  file(_file),
106  function(_function),
107  line(_line),
108  backtrace(_backtrace),
109  reason(_reason)
110  {
111  }
112 };
113 
114 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
115 // Used to allow CPROVER to check itself
116 #define INVARIANT(CONDITION, REASON) \
117  __CPROVER_assert((CONDITION), "Invariant : " REASON)
118 
119 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
120  INVARIANT(CONDITION, "")
121 
122 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
123 // For performance builds, invariants can be ignored
124 // This is *not* recommended as it can result in unpredictable behaviour
125 // including silently reporting incorrect results.
126 // This is also useful for checking side-effect freedom.
127 #define INVARIANT(CONDITION, REASON) do {} while(false)
128 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
129 
130 #elif defined(CPROVER_INVARIANT_ASSERT)
131 // Not recommended but provided for backwards compatability
132 #include <cassert>
133 // NOLINTNEXTLINE(*)
134 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
135 // NOLINTNEXTLINE(*)
136 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
137 #else
138 
139 void print_backtrace(std::ostream &out);
140 
141 std::string get_backtrace();
142 
144 
154 template<class ET, typename ...Params>
155 #ifdef __GNUC__
156 __attribute__((noreturn))
157 #endif
158 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
160  const std::string &file,
161  const std::string &function,
162  const int line,
163  Params &&... params)
164 {
165  std::string backtrace=get_backtrace();
166  ET to_throw(file, function, line, backtrace, std::forward<Params>(params)...);
167  // We now have a structured exception ready to use;
168  // in future this is the place to put a 'throw'.
169  report_exception_to_stderr(to_throw);
170  abort();
171 }
172 
180 #ifdef __GNUC__
181 __attribute__((noreturn))
182 #endif
184  const std::string &file,
185  const std::string &function,
186  const int line,
187  const std::string &reason)
188 {
189  invariant_violated_structured<invariant_failedt>(
190  file,
191  function,
192  line,
193  reason);
194 }
195 
196 // These require a trailing semicolon by the user, such that INVARIANT
197 // behaves syntactically like a function call.
198 // NOLINT as macro definitions confuse the linter it seems.
199 #ifdef _MSC_VER
200 #define __this_function__ __FUNCTION__
201 #else
202 #define __this_function__ __func__
203 #endif
204 
205 #define INVARIANT(CONDITION, REASON) \
206  do /* NOLINT */ \
207  { \
208  if(!(CONDITION)) \
209  invariant_violated_string( \
210  __FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */ \
211  } while(false)
212 
213 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
214  do /* NOLINT */ \
215  { \
216  if(!(CONDITION)) \
217  invariant_violated_structured<TYPENAME>( \
218  __FILE__, __this_function__, __LINE__, __VA_ARGS__); /* NOLINT */ \
219  } while(false)
220 
221 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
222 
223 // Short hand macros. The second variant of each one permits including an
224 // explanation or structured exception, in which case they are synonyms
225 // for INVARIANT.
226 
227 // The condition should only contain (unmodified) arguments to the method.
228 // "The design of the system means that the arguments to this method
229 // will always meet this condition".
230 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
231 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
232  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
233 
234 // The condition should only contain variables that will be returned /
235 // output without further modification.
236 // "The implementation of this method means that the condition will hold".
237 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
238 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
239  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
240 
241 // The condition should only contain (unmodified) values that were
242 // changed by a previous method call.
243 // "The contract of the previous method call means the following
244 // condition holds".
245 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
246 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
247  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
248 
249 // This should be used to mark dead code
250 #define UNREACHABLE INVARIANT(false, "Unreachable")
251 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
252  INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
253 
254 // This condition should be used to document that assumptions that are
255 // made on goto_functions, goto_programs, exprts, etc. being well formed.
256 // "The data structure is corrupt or malformed"
257 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
258 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
259  INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
260 
261 // Legacy annotations
262 
263 // The following should not be used in new code and are only intended
264 // to migrate documentation and "error handling" in older code
265 #define TODO INVARIANT(false, "Todo")
266 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
267 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
268 
269 #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:88
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__))
const std::string reason
Definition: invariant.h:90
const std::string function
Definition: invariant.h:87
const std::string backtrace
Definition: invariant.h:89
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:86
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:183
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:159
invariant_failedt(const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_reason)
Definition: invariant.h:92
Definition: kdev_t.h:19