1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
|
/* Definitions for C++ contract levels. Implements functionality described in
the N4820 working draft version of contracts, P1290, P1332, and P1429.
Copyright (C) 2020-2023 Free Software Foundation, Inc.
Contributed by Jeff Chapman II (jchapman@lock3software.com)
This file is part of GCC.
GCC is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3, or (at your option)
any later version.
GCC is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with GCC; see the file COPYING3. If not see
<http://www.gnu.org/licenses/>. */
#ifndef GCC_CP_CONTRACT_H
#define GCC_CP_CONTRACT_H
/* Contract levels approximate the complexity of the expression. */
enum contract_level
{
CONTRACT_INVALID,
CONTRACT_DEFAULT,
CONTRACT_AUDIT,
CONTRACT_AXIOM
};
/* The concrete semantics determine the behavior of a contract. */
enum contract_semantic
{
CCS_INVALID,
CCS_IGNORE,
CCS_ASSUME,
CCS_NEVER,
CCS_MAYBE
};
/* True if the contract is unchecked. */
inline bool
unchecked_contract_p (contract_semantic cs)
{
return cs == CCS_IGNORE || cs == CCS_ASSUME;
}
/* True if the contract is checked. */
inline bool
checked_contract_p (contract_semantic cs)
{
return cs >= CCS_NEVER;
}
/* Must match std::contract_violation_continuation_mode in <contract>. */
enum contract_continuation
{
NEVER_CONTINUE,
MAYBE_CONTINUE
};
/* Assertion role info. */
struct contract_role
{
const char *name;
contract_semantic default_semantic;
contract_semantic audit_semantic;
contract_semantic axiom_semantic;
};
/* Information for configured contract semantics. */
struct contract_configuration
{
contract_level level;
contract_role* role;
};
/* A contract mode contains information used to derive the checking
and assumption semantics of a contract. This is either a dynamic
configuration, meaning it derives from the build mode, or it is
explicitly specified. */
struct contract_mode
{
contract_mode () : kind(cm_invalid) {}
contract_mode (contract_level level, contract_role *role = NULL)
: kind(cm_dynamic)
{
contract_configuration cc;
cc.level = level;
cc.role = role;
u.config = cc;
}
contract_mode (contract_semantic semantic) : kind(cm_explicit)
{
u.semantic = semantic;
}
contract_level get_level () const
{
gcc_assert (kind == cm_dynamic);
return u.config.level;
}
contract_role *get_role () const
{
gcc_assert (kind == cm_dynamic);
return u.config.role;
}
contract_semantic get_semantic () const
{
gcc_assert (kind == cm_explicit);
return u.semantic;
}
enum { cm_invalid, cm_dynamic, cm_explicit } kind;
union
{
contract_configuration config;
contract_semantic semantic;
} u;
};
extern contract_role *get_contract_role (const char *);
extern contract_role *add_contract_role (const char *,
contract_semantic,
contract_semantic,
contract_semantic,
bool = true);
extern void validate_contract_role (contract_role *);
extern void setup_default_contract_role (bool = true);
extern contract_semantic lookup_concrete_semantic (const char *);
/* Map a source level semantic or level name to its value, or invalid. */
extern contract_semantic map_contract_semantic (const char *);
extern contract_level map_contract_level (const char *);
/* Check if an attribute is a cxx contract attribute. */
extern bool cxx_contract_attribute_p (const_tree);
extern bool cp_contract_assertion_p (const_tree);
/* Returns the default role. */
inline contract_role *
get_default_contract_role ()
{
return get_contract_role ("default");
}
/* Handle various command line arguments related to semantic mapping. */
extern void handle_OPT_fcontract_build_level_ (const char *);
extern void handle_OPT_fcontract_assumption_mode_ (const char *);
extern void handle_OPT_fcontract_continuation_mode_ (const char *);
extern void handle_OPT_fcontract_role_ (const char *);
extern void handle_OPT_fcontract_semantic_ (const char *);
enum contract_matching_context
{
cmc_declaration,
cmc_override
};
/* True if NODE is any kind of contract. */
#define CONTRACT_P(NODE) \
(TREE_CODE (NODE) == ASSERTION_STMT \
|| TREE_CODE (NODE) == PRECONDITION_STMT \
|| TREE_CODE (NODE) == POSTCONDITION_STMT)
/* True if NODE is a contract condition. */
#define CONTRACT_CONDITION_P(NODE) \
(TREE_CODE (NODE) == PRECONDITION_STMT \
|| TREE_CODE (NODE) == POSTCONDITION_STMT)
/* True if NODE is a precondition. */
#define PRECONDITION_P(NODE) \
(TREE_CODE (NODE) == PRECONDITION_STMT)
/* True if NODE is a postcondition. */
#define POSTCONDITION_P(NODE) \
(TREE_CODE (NODE) == POSTCONDITION_STMT)
#define CONTRACT_CHECK(NODE) \
(TREE_CHECK3 (NODE, ASSERTION_STMT, PRECONDITION_STMT, POSTCONDITION_STMT))
/* True iff the FUNCTION_DECL NODE currently has any contracts. */
#define DECL_HAS_CONTRACTS_P(NODE) \
(DECL_CONTRACTS (NODE) != NULL_TREE)
/* For a FUNCTION_DECL of a guarded function, this points to a list of the pre
and post contracts of the first decl of NODE in original order. */
#define DECL_CONTRACTS(NODE) \
(find_contract (DECL_ATTRIBUTES (NODE)))
/* The next contract (if any) after this one in an attribute list. */
#define CONTRACT_CHAIN(NODE) \
(find_contract (TREE_CHAIN (NODE)))
/* The wrapper of the original source location of a list of contracts. */
#define CONTRACT_SOURCE_LOCATION_WRAPPER(NODE) \
(TREE_PURPOSE (TREE_VALUE (NODE)))
/* The original source location of a list of contracts. */
#define CONTRACT_SOURCE_LOCATION(NODE) \
(EXPR_LOCATION (CONTRACT_SOURCE_LOCATION_WRAPPER (NODE)))
/* The actual code _STMT for a contract attribute. */
#define CONTRACT_STATEMENT(NODE) \
(TREE_VALUE (TREE_VALUE (NODE)))
/* True if the contract semantic was specified literally. If true, the
contract mode is an identifier containing the semantic. Otherwise,
it is a TREE_LIST whose TREE_VALUE is the level and whose TREE_PURPOSE
is the role. */
#define CONTRACT_LITERAL_MODE_P(NODE) \
(CONTRACT_MODE (NODE) != NULL_TREE \
&& TREE_CODE (CONTRACT_MODE (NODE)) == IDENTIFIER_NODE)
/* The identifier denoting the literal semantic of the contract. */
#define CONTRACT_LITERAL_SEMANTIC(NODE) \
(TREE_OPERAND (NODE, 0))
/* The written "mode" of the contract. Either an IDENTIFIER with the
literal semantic or a TREE_LIST containing the level and role. */
#define CONTRACT_MODE(NODE) \
(TREE_OPERAND (CONTRACT_CHECK (NODE), 0))
/* The identifier denoting the build level of the contract. */
#define CONTRACT_LEVEL(NODE) \
(TREE_VALUE (CONTRACT_MODE (NODE)))
/* The identifier denoting the role of the contract */
#define CONTRACT_ROLE(NODE) \
(TREE_PURPOSE (CONTRACT_MODE (NODE)))
/* The parsed condition of the contract. */
#define CONTRACT_CONDITION(NODE) \
(TREE_OPERAND (CONTRACT_CHECK (NODE), 1))
/* True iff the condition of the contract NODE is not yet parsed. */
#define CONTRACT_CONDITION_DEFERRED_P(NODE) \
(TREE_CODE (CONTRACT_CONDITION (NODE)) == DEFERRED_PARSE)
/* The raw comment of the contract. */
#define CONTRACT_COMMENT(NODE) \
(TREE_OPERAND (CONTRACT_CHECK (NODE), 2))
/* The VAR_DECL of a postcondition result. For deferred contracts, this
is an IDENTIFIER. */
#define POSTCONDITION_IDENTIFIER(NODE) \
(TREE_OPERAND (POSTCONDITION_STMT_CHECK (NODE), 3))
/* For a FUNCTION_DECL of a guarded function, this holds the function decl
where pre contract checks are emitted. */
#define DECL_PRE_FN(NODE) \
(get_precondition_function ((NODE)))
/* For a FUNCTION_DECL of a guarded function, this holds the function decl
where post contract checks are emitted. */
#define DECL_POST_FN(NODE) \
(get_postcondition_function ((NODE)))
/* True iff the FUNCTION_DECL is the pre function for a guarded function. */
#define DECL_IS_PRE_FN_P(NODE) \
(DECL_ABSTRACT_ORIGIN (NODE) && DECL_PRE_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)
/* True iff the FUNCTION_DECL is the post function for a guarded function. */
#define DECL_IS_POST_FN_P(NODE) \
(DECL_ABSTRACT_ORIGIN (NODE) && DECL_POST_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)
extern void remove_contract_attributes (tree);
extern void copy_contract_attributes (tree, tree);
extern void remap_contracts (tree, tree, tree, bool);
extern void maybe_update_postconditions (tree);
extern void rebuild_postconditions (tree);
extern bool check_postcondition_result (tree, tree, location_t);
extern tree get_precondition_function (tree);
extern tree get_postcondition_function (tree);
extern void duplicate_contracts (tree, tree);
extern void match_deferred_contracts (tree);
extern void defer_guarded_contract_match (tree, tree, tree);
extern bool diagnose_misapplied_contracts (tree);
extern tree finish_contract_attribute (tree, tree);
extern tree invalidate_contract (tree);
extern void update_late_contract (tree, tree, tree);
extern tree splice_out_contracts (tree);
extern bool all_attributes_are_contracts_p (tree);
extern void inherit_base_contracts (tree, tree);
extern tree apply_postcondition_to_return (tree);
extern void start_function_contracts (tree);
extern void finish_function_contracts (tree);
extern void set_contract_functions (tree, tree, tree);
extern tree build_contract_check (tree);
extern void emit_assertion (tree);
#endif /* ! GCC_CP_CONTRACT_H */
|
