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-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 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 132 : checked_contract_p (contract_semantic cs)
58 : {
59 132 : 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 784 : contract_mode (contract_level level, contract_role *role = NULL)
95 784 : : kind(cm_dynamic)
96 : {
97 784 : contract_configuration cc;
98 784 : cc.level = level;
99 784 : cc.role = role;
100 784 : u.config = cc;
101 784 : }
102 40 : contract_mode (contract_semantic semantic) : kind(cm_explicit)
103 : {
104 40 : u.semantic = semantic;
105 40 : }
106 :
107 781 : contract_level get_level () const
108 : {
109 781 : gcc_assert (kind == cm_dynamic);
110 781 : return u.config.level;
111 : }
112 :
113 781 : contract_role *get_role () const
114 : {
115 781 : gcc_assert (kind == cm_dynamic);
116 781 : return u.config.role;
117 : }
118 :
119 40 : contract_semantic get_semantic () const
120 : {
121 40 : gcc_assert (kind == cm_explicit);
122 40 : 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 760 : get_default_contract_role ()
156 : {
157 760 : 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 */
|
