Skip to content

Commit afe8731

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 85a81ea commit afe8731

File tree

2 files changed

+133
-24
lines changed

2 files changed

+133
-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: 123 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,11 @@ Author: Martin Brain, martin.brain@diffblue.com
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,46 @@ 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+
#define REDIRECT(MACRO, ...) \
255+
do \
256+
{ \
257+
GET_MACRO( \
258+
__VA_ARGS__, \
259+
MACRO##6, \
260+
MACRO##5, \
261+
MACRO##4, \
262+
MACRO##3, \
263+
MACRO##2, \
264+
MACRO##1, \
265+
DUMMY_MACRO_ARG) \
266+
(__VA_ARGS__); \
267+
} while(false)
268+
269+
#define INVARIANT2(CONDITION, REASON) \
205270
do /* NOLINT */ \
206271
{ \
207272
if(!(CONDITION)) \
208273
invariant_violated_string( \
209274
__FILE__, \
210275
__this_function__, \
211276
__LINE__, \
277+
#CONDITION, \
278+
(REASON)); /* NOLINT */ \
279+
} while(false)
280+
281+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
282+
do /* NOLINT */ \
283+
{ \
284+
if(!(CONDITION)) \
285+
invariant_violated_structured<invariant_with_diagnostics_failedt>( \
286+
__FILE__, \
287+
__this_function__, \
288+
__LINE__, \
289+
#CONDITION, \
212290
(REASON), \
213-
#CONDITION); /* NOLINT */ \
291+
(DIAGNOSTICS)); /* NOLINT */ \
214292
} while(false)
215293

216294
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
@@ -227,19 +305,25 @@ invariant_violated_string(
227305

228306
#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
229307

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

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.
313+
// The condition should only contain (unmodified) inputs to the method. Inputs
314+
// include arguments passed to the function, as well as member variables that
315+
// the function may read.
237316
// "The design of the system means that the arguments to this method
238317
// will always meet this condition".
239318
//
240319
// The PRECONDITION documents / checks assumptions about the inputs
241320
// that is the caller's responsibility to make happen before the call.
242-
#define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
321+
#define PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition")
322+
#define PRECONDITION2(CONDITION, DIAGNOSTICS) \
323+
INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS)
324+
325+
#define PRECONDITION(...) REDIRECT(PRECONDITION, __VA_ARGS__)
326+
243327
#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
244328
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
245329

@@ -251,7 +335,12 @@ invariant_violated_string(
251335
// output when it returns, given that it was called with valid inputs.
252336
// Outputs include the return value of the function, as well as member
253337
// variables that the function may write.
254-
#define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
338+
#define POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition")
339+
#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \
340+
INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS)
341+
342+
#define POSTCONDITION(...) REDIRECT(POSTCONDITION, __VA_ARGS__)
343+
255344
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
256345
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
257346

@@ -263,28 +352,38 @@ invariant_violated_string(
263352
// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
264353
// a statement about what the caller expects from a function, whereas a
265354
// POSTCONDITION is a statement about guarantees made by the function itself.
266-
#define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
355+
#define CHECK_RETURN1(CONDITION) INVARIANT2(CONDITION, "Check return value")
356+
#define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \
357+
INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS)
358+
359+
#define CHECK_RETURN(...) REDIRECT(CHECK_RETURN, __VA_ARGS__)
360+
267361
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
268362
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
269363

270364
// This should be used to mark dead code
271-
#define UNREACHABLE INVARIANT(false, "Unreachable")
365+
#define UNREACHABLE INVARIANT2(false, "Unreachable")
272366
#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
273367
INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)
274368

275369
// This condition should be used to document that assumptions that are
276370
// made on goto_functions, goto_programs, exprts, etc. being well formed.
277371
// "The data structure is corrupt or malformed"
278-
#define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
372+
#define DATA_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON)
373+
#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
374+
INVARIANT3(CONDITION, REASON, DIAGNOSTICS)
375+
376+
#define DATA_INVARIANT(...) REDIRECT(DATA_INVARIANT, __VA_ARGS__)
377+
279378
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
280379
INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)
281380

282381
// Legacy annotations
283382

284383
// The following should not be used in new code and are only intended
285384
// 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")
385+
#define TODO INVARIANT2(false, "Todo")
386+
#define UNIMPLEMENTED INVARIANT2(false, "Unimplemented")
387+
#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case")
289388

290389
#endif // CPROVER_UTIL_INVARIANT_H

0 commit comments

Comments
 (0)