Branch data Line data Source code
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-2025 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 : 28 : unchecked_contract_p (contract_semantic cs)
50 : : {
51 : 28 : 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 : 805 : contract_mode (contract_level level, contract_role *role = NULL)
95 : 805 : : kind(cm_dynamic)
96 : : {
97 : 805 : contract_configuration cc;
98 : 805 : cc.level = level;
99 : 805 : cc.role = role;
100 : 805 : u.config = cc;
101 : 805 : }
102 : 42 : contract_mode (contract_semantic semantic) : kind(cm_explicit)
103 : : {
104 : 42 : u.semantic = semantic;
105 : 42 : }
106 : :
107 : 802 : contract_level get_level () const
108 : : {
109 : 802 : gcc_assert (kind == cm_dynamic);
110 : 802 : return u.config.level;
111 : : }
112 : :
113 : 802 : contract_role *get_role () const
114 : : {
115 : 802 : gcc_assert (kind == cm_dynamic);
116 : 802 : return u.config.role;
117 : : }
118 : :
119 : 42 : contract_semantic get_semantic () const
120 : : {
121 : 42 : gcc_assert (kind == cm_explicit);
122 : 42 : 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 : : /* Map a source level semantic or level name to its value, or invalid. */
135 : : extern contract_semantic map_contract_semantic (const char *);
136 : : extern contract_level map_contract_level (const char *);
137 : :
138 : : /* Check if an attribute is a cxx contract attribute. */
139 : : extern bool cxx_contract_attribute_p (const_tree);
140 : : extern bool cp_contract_assertion_p (const_tree);
141 : :
142 : : /* Handle various command line arguments related to semantic mapping. */
143 : : extern void handle_OPT_fcontract_build_level_ (const char *);
144 : : extern void handle_OPT_fcontract_assumption_mode_ (const char *);
145 : : extern void handle_OPT_fcontract_continuation_mode_ (const char *);
146 : : extern void handle_OPT_fcontract_role_ (const char *);
147 : : extern void handle_OPT_fcontract_semantic_ (const char *);
148 : :
149 : : enum contract_matching_context
150 : : {
151 : : cmc_declaration,
152 : : cmc_override
153 : : };
154 : :
155 : : /* True if NODE is any kind of contract. */
156 : : #define CONTRACT_P(NODE) \
157 : : (TREE_CODE (NODE) == ASSERTION_STMT \
158 : : || TREE_CODE (NODE) == PRECONDITION_STMT \
159 : : || TREE_CODE (NODE) == POSTCONDITION_STMT)
160 : :
161 : : /* True if NODE is a contract condition. */
162 : : #define CONTRACT_CONDITION_P(NODE) \
163 : : (TREE_CODE (NODE) == PRECONDITION_STMT \
164 : : || TREE_CODE (NODE) == POSTCONDITION_STMT)
165 : :
166 : : /* True if NODE is a precondition. */
167 : : #define PRECONDITION_P(NODE) \
168 : : (TREE_CODE (NODE) == PRECONDITION_STMT)
169 : :
170 : : /* True if NODE is a postcondition. */
171 : : #define POSTCONDITION_P(NODE) \
172 : : (TREE_CODE (NODE) == POSTCONDITION_STMT)
173 : :
174 : : #define CONTRACT_CHECK(NODE) \
175 : : (TREE_CHECK3 (NODE, ASSERTION_STMT, PRECONDITION_STMT, POSTCONDITION_STMT))
176 : :
177 : : /* True iff the FUNCTION_DECL NODE currently has any contracts. */
178 : : #define DECL_HAS_CONTRACTS_P(NODE) \
179 : : (DECL_CONTRACTS (NODE) != NULL_TREE)
180 : :
181 : : /* For a FUNCTION_DECL of a guarded function, this points to a list of the pre
182 : : and post contracts of the first decl of NODE in original order. */
183 : : #define DECL_CONTRACTS(NODE) \
184 : : (find_contract (DECL_ATTRIBUTES (NODE)))
185 : :
186 : : /* The next contract (if any) after this one in an attribute list. */
187 : : #define CONTRACT_CHAIN(NODE) \
188 : : (find_contract (TREE_CHAIN (NODE)))
189 : :
190 : : /* The wrapper of the original source location of a list of contracts. */
191 : : #define CONTRACT_SOURCE_LOCATION_WRAPPER(NODE) \
192 : : (TREE_PURPOSE (TREE_VALUE (NODE)))
193 : :
194 : : /* The original source location of a list of contracts. */
195 : : #define CONTRACT_SOURCE_LOCATION(NODE) \
196 : : (EXPR_LOCATION (CONTRACT_SOURCE_LOCATION_WRAPPER (NODE)))
197 : :
198 : : /* The actual code _STMT for a contract attribute. */
199 : : #define CONTRACT_STATEMENT(NODE) \
200 : : (TREE_VALUE (TREE_VALUE (NODE)))
201 : :
202 : : /* True if the contract semantic was specified literally. If true, the
203 : : contract mode is an identifier containing the semantic. Otherwise,
204 : : it is a TREE_LIST whose TREE_VALUE is the level and whose TREE_PURPOSE
205 : : is the role. */
206 : : #define CONTRACT_LITERAL_MODE_P(NODE) \
207 : : (CONTRACT_MODE (NODE) != NULL_TREE \
208 : : && TREE_CODE (CONTRACT_MODE (NODE)) == IDENTIFIER_NODE)
209 : :
210 : : /* The identifier denoting the literal semantic of the contract. */
211 : : #define CONTRACT_LITERAL_SEMANTIC(NODE) \
212 : : (TREE_OPERAND (NODE, 0))
213 : :
214 : : /* The written "mode" of the contract. Either an IDENTIFIER with the
215 : : literal semantic or a TREE_LIST containing the level and role. */
216 : : #define CONTRACT_MODE(NODE) \
217 : : (TREE_OPERAND (CONTRACT_CHECK (NODE), 0))
218 : :
219 : : /* The identifier denoting the build level of the contract. */
220 : : #define CONTRACT_LEVEL(NODE) \
221 : : (TREE_VALUE (CONTRACT_MODE (NODE)))
222 : :
223 : : /* The identifier denoting the role of the contract */
224 : : #define CONTRACT_ROLE(NODE) \
225 : : (TREE_PURPOSE (CONTRACT_MODE (NODE)))
226 : :
227 : : /* The parsed condition of the contract. */
228 : : #define CONTRACT_CONDITION(NODE) \
229 : : (TREE_OPERAND (CONTRACT_CHECK (NODE), 1))
230 : :
231 : : /* True iff the condition of the contract NODE is not yet parsed. */
232 : : #define CONTRACT_CONDITION_DEFERRED_P(NODE) \
233 : : (TREE_CODE (CONTRACT_CONDITION (NODE)) == DEFERRED_PARSE)
234 : :
235 : : /* The raw comment of the contract. */
236 : : #define CONTRACT_COMMENT(NODE) \
237 : : (TREE_OPERAND (CONTRACT_CHECK (NODE), 2))
238 : :
239 : : /* The VAR_DECL of a postcondition result. For deferred contracts, this
240 : : is an IDENTIFIER. */
241 : : #define POSTCONDITION_IDENTIFIER(NODE) \
242 : : (TREE_OPERAND (POSTCONDITION_STMT_CHECK (NODE), 3))
243 : :
244 : : /* For a FUNCTION_DECL of a guarded function, this holds the function decl
245 : : where pre contract checks are emitted. */
246 : : #define DECL_PRE_FN(NODE) \
247 : : (get_precondition_function ((NODE)))
248 : :
249 : : /* For a FUNCTION_DECL of a guarded function, this holds the function decl
250 : : where post contract checks are emitted. */
251 : : #define DECL_POST_FN(NODE) \
252 : : (get_postcondition_function ((NODE)))
253 : :
254 : : /* True iff the FUNCTION_DECL is the pre function for a guarded function. */
255 : : #define DECL_IS_PRE_FN_P(NODE) \
256 : : (DECL_ABSTRACT_ORIGIN (NODE) && DECL_PRE_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)
257 : :
258 : : /* True iff the FUNCTION_DECL is the post function for a guarded function. */
259 : : #define DECL_IS_POST_FN_P(NODE) \
260 : : (DECL_ABSTRACT_ORIGIN (NODE) && DECL_POST_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)
261 : :
262 : : /* contracts.cc */
263 : : extern void emit_assertion (tree);
264 : :
265 : : extern void remove_contract_attributes (tree);
266 : : extern bool all_attributes_are_contracts_p (tree);
267 : : extern tree finish_contract_attribute (tree, tree);
268 : : extern void copy_contract_attributes (tree, tree);
269 : : extern bool diagnose_misapplied_contracts (tree);
270 : : extern void remap_contracts (tree, tree, tree, bool);
271 : : extern tree splice_out_contracts (tree);
272 : : extern void inherit_base_contracts (tree, tree);
273 : :
274 : : extern tree make_postcondition_variable (cp_expr);
275 : : extern tree make_postcondition_variable (cp_expr, tree);
276 : : extern void maybe_update_postconditions (tree);
277 : : extern void rebuild_postconditions (tree);
278 : : extern bool check_postcondition_result (tree, tree, location_t);
279 : :
280 : : extern tree grok_contract (tree, tree, tree, cp_expr,
281 : : location_t);
282 : : extern tree finish_contract_condition (cp_expr);
283 : : extern void update_late_contract (tree, tree, tree);
284 : : extern tree invalidate_contract (tree);
285 : : extern void duplicate_contracts (tree, tree);
286 : :
287 : : extern void match_deferred_contracts (tree);
288 : : extern void defer_guarded_contract_match (tree, tree, tree);
289 : :
290 : : extern tree get_precondition_function (tree);
291 : : extern tree get_postcondition_function (tree);
292 : : extern void start_function_contracts (tree);
293 : : extern void maybe_apply_function_contracts (tree);
294 : : extern void finish_function_contracts (tree);
295 : : extern void set_contract_functions (tree, tree, tree);
296 : :
297 : : extern tree build_contract_check (tree);
298 : :
299 : : /* Return the first contract in ATTRS, or NULL_TREE if there are none. */
300 : :
301 : : inline tree
302 : 1413684056 : find_contract (tree attrs)
303 : : {
304 : 1525224761 : while (attrs && !cxx_contract_attribute_p (attrs))
305 : 111540705 : attrs = TREE_CHAIN (attrs);
306 : 1413684056 : return attrs;
307 : : }
308 : :
309 : : inline void
310 : 12 : set_decl_contracts (tree decl, tree contract_attrs)
311 : : {
312 : 12 : remove_contract_attributes (decl);
313 : 12 : DECL_ATTRIBUTES (decl) = chainon (DECL_ATTRIBUTES (decl), contract_attrs);
314 : 12 : }
315 : :
316 : : /* Returns the computed semantic of the node. */
317 : :
318 : : inline contract_semantic
319 : 3876 : get_contract_semantic (const_tree t)
320 : : {
321 : 3876 : return (contract_semantic) (TREE_LANG_FLAG_3 (CONTRACT_CHECK (t))
322 : 3876 : | (TREE_LANG_FLAG_2 (t) << 1)
323 : 3876 : | (TREE_LANG_FLAG_0 ((t)) << 2));
324 : : }
325 : :
326 : : /* Sets the computed semantic of the node. */
327 : :
328 : : inline void
329 : 847 : set_contract_semantic (tree t, contract_semantic semantic)
330 : : {
331 : 847 : TREE_LANG_FLAG_3 (CONTRACT_CHECK (t)) = semantic & 0x01;
332 : 847 : TREE_LANG_FLAG_2 (t) = (semantic & 0x02) >> 1;
333 : 847 : TREE_LANG_FLAG_0 (t) = (semantic & 0x04) >> 2;
334 : 847 : }
335 : :
336 : :
337 : : /* Will this contract be ignored. */
338 : :
339 : : inline bool
340 : 103 : contract_ignored_p (const_tree contract)
341 : : {
342 : 103 : return (get_contract_semantic (contract) <= CCS_IGNORE);
343 : : }
344 : :
345 : : /* Will this contract be evaluated? */
346 : :
347 : : inline bool
348 : 87 : contract_evaluated_p (const_tree contract)
349 : : {
350 : 87 : return (get_contract_semantic (contract) >= CCS_NEVER);
351 : : }
352 : : #endif /* ! GCC_CP_CONTRACT_H */
|
