gcc/cp/contracts.h

   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 */