Skip to content

Commit 4ffc2a4

Browse files
danpoedanpoe
authored
Merge pull request diffblue#2744 from danpoe/feature/invariants-with-diagnostic-information
Invariant macros with diagnostic information
2 parents d0be385 + 1e2fda3 commit 4ffc2a4

File tree

8 files changed

+223
-34
lines changed

8 files changed

+223
-34
lines changed

‎regression/invariants/driver.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,22 @@ int main(int argc, char** argv)
9191
DATA_INVARIANT(false, "Test invariant failure");
9292
else if(arg=="irep")
9393
INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet()));
94+
else if(arg == "invariant-diagnostics")
95+
INVARIANT(
96+
false,
97+
"invariant with diagnostics failure",
98+
"invariant diagnostics information");
99+
else if(arg == "precondition-diagnostics")
100+
PRECONDITION(false, "precondition diagnostics information");
101+
else if(arg == "postcondition-diagnostics")
102+
POSTCONDITION(false, "postcondition diagnostics information");
103+
else if(arg == "check-return-diagnostics")
104+
CHECK_RETURN(false, "check return diagnostics information");
105+
else if(arg == "data-invariant-diagnostics")
106+
DATA_INVARIANT(
107+
false,
108+
"data invariant with diagnostics failure",
109+
"data invariant diagnostics information");
94110
else
95111
return 1;
96112
}

‎regression/invariants/invariant-failure14/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
dummy_parameter.c
3+
invariant-diagnostics
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
invariant with diagnostics failure
8+
invariant diagnostics information
9+
^(Backtrace)|(Backtraces not supported)$
10+
--
11+
^warning: ignoring
12+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure15/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
dummy_parameter.c
3+
precondition-diagnostics
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
precondition diagnostics information
8+
^(Backtrace)|(Backtraces not supported)$
9+
--
10+
^warning: ignoring
11+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure16/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
dummy_parameter.c
3+
postcondition-diagnostics
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
postcondition diagnostics information
8+
^(Backtrace)|(Backtraces not supported)$
9+
--
10+
^warning: ignoring
11+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure17/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
dummy_parameter.c
3+
check-return-diagnostics
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
check return diagnostics information
8+
^(Backtrace)|(Backtraces not supported)$
9+
--
10+
^warning: ignoring
11+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure18/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
dummy_parameter.c
3+
data-invariant-diagnostics
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
data invariant diagnostics information
8+
^(Backtrace)|(Backtraces not supported)$
9+
--
10+
^warning: ignoring
11+
^VERIFICATION SUCCESSFUL$

‎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: 141 additions & 34 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,54 @@ invariant_violated_string(
201249
#define __this_function__ __func__
202250
#endif
203251

204-
#define INVARIANT(CONDITION, REASON) \
252+
// We wrap macros that take __VA_ARGS__ as an argument with EXPAND_MACRO(). This
253+
// is to account for the behaviour of msvc, which otherwise would not expand
254+
// __VA_ARGS__ to multiple arguments in the outermost macro invocation.
255+
#define EXPAND_MACRO(x) x
256+
257+
#define GET_MACRO(X1, X2, X3, X4, X5, X6, MACRO, ...) MACRO
258+
259+
// This macro dispatches to the macros MACRO<n> (with 1 <= n <= 6) and calls
260+
// them with the arguments in __VA_ARGS__. The invocation of GET_MACRO() selects
261+
// MACRO<n> when __VA_ARGS__ consists of n arguments.
262+
#define REDIRECT(MACRO, ...) \
263+
do \
264+
{ \
265+
EXPAND_MACRO( \
266+
GET_MACRO( \
267+
__VA_ARGS__, \
268+
MACRO##6, \
269+
MACRO##5, \
270+
MACRO##4, \
271+
MACRO##3, \
272+
MACRO##2, \
273+
MACRO##1, \
274+
DUMMY_MACRO_ARG)(__VA_ARGS__)); \
275+
} while(false)
276+
277+
#define INVARIANT2(CONDITION, REASON) \
205278
do /* NOLINT */ \
206279
{ \
207280
if(!(CONDITION)) \
208281
invariant_violated_string( \
209282
__FILE__, \
210283
__this_function__, \
211284
__LINE__, \
285+
#CONDITION, \
286+
(REASON)); /* NOLINT */ \
287+
} while(false)
288+
289+
#define INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
290+
do /* NOLINT */ \
291+
{ \
292+
if(!(CONDITION)) \
293+
invariant_violated_structured<invariant_with_diagnostics_failedt>( \
294+
__FILE__, \
295+
__this_function__, \
296+
__LINE__, \
297+
#CONDITION, \
212298
(REASON), \
213-
#CONDITION); /* NOLINT */ \
299+
(DIAGNOSTICS)); /* NOLINT */ \
214300
} while(false)
215301

216302
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
@@ -227,21 +313,27 @@ invariant_violated_string(
227313

228314
#endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
229315

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.
316+
// Short hand macros. The variants *_STRUCTURED below allow to specify a custom
317+
// exception, and are equivalent to INVARIANT_STRUCTURED.
233318

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.
319+
#define INVARIANT(...) EXPAND_MACRO(REDIRECT(INVARIANT, __VA_ARGS__))
320+
321+
// The condition should only contain (unmodified) inputs to the method. Inputs
322+
// include arguments passed to the function, as well as member variables that
323+
// the function may read.
237324
// "The design of the system means that the arguments to this method
238325
// will always meet this condition".
239326
//
240327
// The PRECONDITION documents / checks assumptions about the inputs
241328
// 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__)
329+
#define PRECONDITION1(CONDITION) INVARIANT2(CONDITION, "Precondition")
330+
#define PRECONDITION2(CONDITION, DIAGNOSTICS) \
331+
INVARIANT3(CONDITION, "Precondition", DIAGNOSTICS)
332+
333+
#define PRECONDITION(...) EXPAND_MACRO(REDIRECT(PRECONDITION, __VA_ARGS__))
334+
335+
#define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
336+
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
245337

246338
// The condition should only contain variables that will be returned /
247339
// output without further modification.
@@ -251,9 +343,14 @@ invariant_violated_string(
251343
// output when it returns, given that it was called with valid inputs.
252344
// Outputs include the return value of the function, as well as member
253345
// 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__)
346+
#define POSTCONDITION1(CONDITION) INVARIANT2(CONDITION, "Postcondition")
347+
#define POSTCONDITION2(CONDITION, DIAGNOSTICS) \
348+
INVARIANT3(CONDITION, "Postcondition", DIAGNOSTICS)
349+
350+
#define POSTCONDITION(...) EXPAND_MACRO(REDIRECT(POSTCONDITION, __VA_ARGS__))
351+
352+
#define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
353+
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
257354

258355
// The condition should only contain (unmodified) values that were
259356
// changed by a previous method call.
@@ -263,28 +360,38 @@ invariant_violated_string(
263360
// A difference between CHECK_RETURN and POSTCONDITION is that CHECK_RETURN is
264361
// a statement about what the caller expects from a function, whereas a
265362
// 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__)
363+
#define CHECK_RETURN1(CONDITION) INVARIANT2(CONDITION, "Check return value")
364+
#define CHECK_RETURN2(CONDITION, DIAGNOSTICS) \
365+
INVARIANT3(CONDITION, "Check return value", DIAGNOSTICS)
366+
367+
#define CHECK_RETURN(...) EXPAND_MACRO(REDIRECT(CHECK_RETURN, __VA_ARGS__))
368+
369+
#define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
370+
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
269371

270372
// 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__)
373+
#define UNREACHABLE INVARIANT2(false, "Unreachable")
374+
#define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
375+
EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
274376

275377
// This condition should be used to document that assumptions that are
276378
// made on goto_functions, goto_programs, exprts, etc. being well formed.
277379
// "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__)
380+
#define DATA_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON)
381+
#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS) \
382+
INVARIANT3(CONDITION, REASON, DIAGNOSTICS)
383+
384+
#define DATA_INVARIANT(...) EXPAND_MACRO(REDIRECT(DATA_INVARIANT, __VA_ARGS__))
385+
386+
#define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
387+
EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
281388

282389
// Legacy annotations
283390

284391
// The following should not be used in new code and are only intended
285392
// 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")
393+
#define TODO INVARIANT2(false, "Todo")
394+
#define UNIMPLEMENTED INVARIANT2(false, "Unimplemented")
395+
#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case")
289396

290397
#endif // CPROVER_UTIL_INVARIANT_H

0 commit comments

Comments
 (0)