Skip to content

Commit 8a37a2d

Browse files
danpoedanpoe
committed
Invariant macros with diagnostic information
This overloads the invariant macros to take an additional optional argument to include diagnostic information. This can e.g. be useful when debugging an invariant violation without having access to the goto binary on which cbmc was run on. For example, one can now do both of DATA_INVARIANT(expr.operands().size() == 2, "binary expression") DATA_INVARIANT(expr.operands().size() == 2, "binary expression", expr.pretty())
1 parent bcb7c76 commit 8a37a2d

File tree

2 files changed

+136
-24
lines changed

2 files changed

+136
-24
lines changed

‎src/util/invariant.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,3 +125,13 @@ std::string invariant_failedt::what() const noexcept
125125
<< backtrace << '\n';
126126
return out.str();
127127
}
128+
129+
std::string invariant_with_diagnostics_failedt::what() const noexcept
130+
{
131+
std::string s(invariant_failedt::what());
132+
133+
if(!s.empty() && s.back() != '\n')
134+
s += '\n';
135+
136+
return s + "Diagnostics: " + diagnostics + '\n';
137+
}

‎src/util/invariant.h

Lines changed: 126 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,11 @@ Author: Martin Brain, [email protected]
99
#ifndef CPROVER_UTIL_INVARIANT_H
1010
#define CPROVER_UTIL_INVARIANT_H
1111

12+
#include <cstdlib>
1213
#include <stdexcept>
13-
#include <type_traits>
1414
#include <string>
15-
#include <cstdlib>
15+
#include <tuple>
16+
#include <type_traits>
1617

1718
/*
1819
** Invariants document conditions that the programmer believes to
@@ -83,7 +84,7 @@ class invariant_failedt
8384
const std::string reason;
8485

8586
public:
86-
std::string what() const noexcept;
87+
virtual std::string what() const noexcept;
8788

8889
invariant_failedt(
8990
const std::string &_file,
@@ -102,9 +103,47 @@ class invariant_failedt
102103
}
103104
};
104105

106+
/// A class that includes diagnostic information related to an invariant
107+
/// violation.
108+
class invariant_with_diagnostics_failedt : public invariant_failedt
109+
{
110+
private:
111+
const std::string diagnostics;
112+
113+
public:
114+
virtual std::string what() const noexcept;
115+
116+
invariant_with_diagnostics_failedt(
117+
const std::string &_file,
118+
const std::string &_function,
119+
int _line,
120+
const std::string &_backtrace,
121+
const std::string &_condition,
122+
const std::string &_reason,
123+
const std::string &_diagnostics)
124+
: invariant_failedt(
125+
_file,
126+
_function,
127+
_line,
128+
_backtrace,
129+
_condition,
130+
_reason),
131+
diagnostics(_diagnostics)
132+
{
133+
}
134+
};
135+
136+
// The macros MACRO<n> (e.g., INVARIANT2) are for internal use in this file
137+
// only. The corresponding macros that take a variable number of arguments (see
138+
// further below) should be used instead, which in turn call those with a fixed
139+
// number of arguments. For example, if INVARIANT(...) is called with two
140+
// arguments, it calls INVARIANT2().
141+
105142
#if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
106143
// Used to allow CPROVER to check itself
107-
#define INVARIANT(CONDITION, REASON) \
144+
#define INVARIANT2(CONDITION, REASON) \
145+
__CPROVER_assert((CONDITION), "Invariant : " REASON)
146+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
108147
__CPROVER_assert((CONDITION), "Invariant : " REASON)
109148

110149
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
@@ -115,14 +154,23 @@ class invariant_failedt
115154
// This is *not* recommended as it can result in unpredictable behaviour
116155
// including silently reporting incorrect results.
117156
// This is also useful for checking side-effect freedom.
118-
#define INVARIANT(CONDITION, REASON) do {} while(false)
157+
#define INVARIANT2(CONDITION, REASON) \
158+
do \
159+
{ \
160+
} while(false)
161+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
162+
do \
163+
{ \
164+
} while(false)
119165
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
120166

121167
#elif defined(CPROVER_INVARIANT_ASSERT)
122168
// Not recommended but provided for backwards compatability
123169
#include <cassert>
124170
// NOLINTNEXTLINE(*)
125-
#define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
171+
#define INVARIANT2(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
172+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
173+
assert((CONDITION) && ((REASON), true)) /* NOLINT */
126174
// NOLINTNEXTLINE(*)
127175
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
128176
#else
@@ -185,8 +233,8 @@ invariant_violated_string(
185233
const std::string &file,
186234
const std::string &function,
187235
const int line,
188-
const std::string &reason,
189-
const std::string &condition)
236+
const std::string &condition,
237+
const std::string &reason)
190238
{
191239
invariant_violated_structured<invariant_failedt>(
192240
file, function, line, condition, reason);
@@ -201,16 +249,49 @@ invariant_violated_string(
201249
#define __this_function__ __func__
202250
#endif
203251

204-
#define INVARIANT(CONDITION, REASON) \
252+
#define GET_MACRO(X1, X2, X3, X4, X5, X6, MACRO, ...) MACRO
253+
254+
// This macro dispatches to the macros MACRO<n> (with 1 <= n <= 6) and calls
255+
// them with the arguments in __VA_ARGS__. The invocation of GET_MACRO() selects
256+
// MACRO<n> when __VA_ARGS__ consists of n arguments.
257+
#define REDIRECT(MACRO, ...) \
258+
do \
259+
{ \
260+
GET_MACRO( \
261+
__VA_ARGS__, \
262+
MACRO##6, \
263+
MACRO##5, \
264+
MACRO##4, \
265+
MACRO##3, \
266+
MACRO##2, \
267+
MACRO##1, \
268+
DUMMY_MACRO_ARG) \
269+
(__VA_ARGS__); \
270+
} while(false)
271+
272+
#define INVARIANT2(CONDITION, REASON) \
205273
do /* NOLINT */ \
206274
{ \
207275
if(!(CONDITION)) \
208276
invariant_violated_string( \
209277
__FILE__, \
210278
__this_function__, \
211279
__LINE__, \
280+
#CONDITION, \
281+
(REASON)); /* NOLINT */ \
282+
} while(false)
283+
284+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
285+
do /* NOLINT */ \
286+
{ \
287+
if(!(CONDITION)) \
288+
invariant_violated_structured<invariant_with_diagnostics_failedt>( \
289+
__FILE__, \
290+
__this_function__, \
291+
__LINE__, \
292+
#CONDITION, \
212293
(REASON), \
213-
#CONDITION); /* NOLINT */ \
294+
(DIAGNOSTICS)); /* NOLINT */ \
214295
} while(false)
215296

216297
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
@@ -227,19 +308,25 @@ invariant_violated_string(
227308

228309
#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
229310

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.
311+
// Short hand macros. The variants *_STRUCTURED below allow to specify a custom
312+
// exception, and are equivalent to INVARIANT_STRUCTURED.
313+
314+
#define INVARIANT(...) REDIRECT(INVARIANT, __VA_ARGS__)
233315

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.
316+
// The condition should only contain (unmodified) inputs to the method. Inputs
317+
// include arguments passed to the function, as well as member variables that
318+
// the function may read.
237319
// "The design of the system means that the arguments to this method
238320
// will always meet this condition".
239321
//
240322
// The PRECONDITION documents / checks assumptions about the inputs
241323
// that is the caller's responsibility to make happen before the call.
242-
#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
324+
#define PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition")
325+
#define PRECONDITION2(CONDITION, DIAGNOSTICS) \
326+
INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS)
327+
328+
#define PRECONDITION(...) REDIRECT(PRECONDITION, __VA_ARGS__)
329+
243330
#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
244331
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
245332

@@ -251,7 +338,12 @@ invariant_violated_string(
251338
// output when it returns, given that it was called with valid inputs.
252339
// Outputs include the return value of the function, as well as member
253340
// variables that the function may write.
254-
#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
341+
#define POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition")
342+
#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \
343+
INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS)
344+
345+
#define POSTCONDITION(...) REDIRECT(POSTCONDITION, __VA_ARGS__)
346+
255347
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
256348
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
257349

@@ -263,28 +355,38 @@ invariant_violated_string(
263355
// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
264356
// a statement about what the caller expects from a function, whereas a
265357
// POSTCONDITION is a statement about guarantees made by the function itself.
266-
#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
358+
#define CHECK_RETURN1(CONDITION) INVARIANT2(CONDITION, "Check return value")
359+
#define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \
360+
INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS)
361+
362+
#define CHECK_RETURN(...) REDIRECT(CHECK_RETURN, __VA_ARGS__)
363+
267364
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
268365
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
269366

270367
// This should be used to mark dead code
271-
#define UNREACHABLE INVARIANT(false, "Unreachable")
368+
#define UNREACHABLE INVARIANT2(false, "Unreachable")
272369
#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
273370
INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
274371

275372
// This condition should be used to document that assumptions that are
276373
// made on goto_functions, goto_programs, exprts, etc. being well formed.
277374
// "The data structure is corrupt or malformed"
278-
#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
375+
#define DATA_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON)
376+
#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
377+
INVARIANT3(CONDITION, REASON, DIAGNOSTICS)
378+
379+
#define DATA_INVARIANT(...) REDIRECT(DATA_INVARIANT, __VA_ARGS__)
380+
279381
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
280382
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
281383

282384
// Legacy annotations
283385

284386
// The following should not be used in new code and are only intended
285387
// 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")
388+
#define TODO INVARIANT2(false, "Todo")
389+
#define UNIMPLEMENTED INVARIANT2(false, "Unimplemented")
390+
#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case")
289391

290392
#endif // CPROVER_UTIL_INVARIANT_H

0 commit comments

Comments
 (0)