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-2023 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 CONTRACT_COMMENT(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 */