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