/* Definitions for C++ contract levels.  Implements functionality described in
   the N4820 working draft version of contracts, P1290, P1332, and P1429.
   Copyright (C) 2020-2023 Free Software Foundation, Inc.
   Contributed by Jeff Chapman II (jchapman@lock3software.com)

This file is part of GCC.

GCC is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3, or (at your option)
any later version.

GCC is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with GCC; see the file COPYING3.  If not see
<http://www.gnu.org/licenses/>.  */

#ifndef GCC_CP_CONTRACT_H
#define GCC_CP_CONTRACT_H

/* Contract levels approximate the complexity of the expression.  */

enum contract_level
{
  CONTRACT_INVALID,
  CONTRACT_DEFAULT,
  CONTRACT_AUDIT,
  CONTRACT_AXIOM
};

/* The concrete semantics determine the behavior of a contract.  */

enum contract_semantic
{
  CCS_INVALID,
  CCS_IGNORE,
  CCS_ASSUME,
  CCS_NEVER,
  CCS_MAYBE
};

/* True if the contract is unchecked.  */

inline bool
unchecked_contract_p (contract_semantic cs)
{
  return cs == CCS_IGNORE || cs == CCS_ASSUME;
}

/* True if the contract is checked.  */

inline bool
checked_contract_p (contract_semantic cs)
{
  return cs >= CCS_NEVER;
}

/* Must match std::contract_violation_continuation_mode in <contract>.  */
enum contract_continuation
{
  NEVER_CONTINUE,
  MAYBE_CONTINUE
};

/* Assertion role info.  */
struct contract_role
{
  const char *name;
  contract_semantic default_semantic;
  contract_semantic audit_semantic;
  contract_semantic axiom_semantic;
};

/* Information for configured contract semantics.  */

struct contract_configuration
{
  contract_level level;
  contract_role* role;
};

/* A contract mode contains information used to derive the checking
   and assumption semantics of a contract. This is either a dynamic
   configuration, meaning it derives from the build mode, or it is
   explicitly specified.  */

struct contract_mode
{
  contract_mode () : kind(cm_invalid) {}
  contract_mode (contract_level level, contract_role *role = NULL)
    : kind(cm_dynamic)
  {
    contract_configuration cc;
    cc.level = level;
    cc.role = role;
    u.config = cc;
  }
  contract_mode (contract_semantic semantic) : kind(cm_explicit)
  {
    u.semantic = semantic;
  }

  contract_level get_level () const
  {
    gcc_assert (kind == cm_dynamic);
    return u.config.level;
  }

  contract_role *get_role () const
  {
    gcc_assert (kind == cm_dynamic);
    return u.config.role;
  }

  contract_semantic get_semantic () const
  {
    gcc_assert (kind == cm_explicit);
    return u.semantic;
  }

  enum { cm_invalid, cm_dynamic, cm_explicit } kind;

  union
  {
    contract_configuration config;
    contract_semantic semantic;
  } u;
};

extern contract_role *get_contract_role	(const char *);
extern contract_role *add_contract_role	(const char *,
					 contract_semantic,
					 contract_semantic,
					 contract_semantic,
					 bool = true);
extern void validate_contract_role	(contract_role *);
extern void setup_default_contract_role	(bool = true);
extern contract_semantic lookup_concrete_semantic (const char *);

/* Map a source level semantic or level name to its value, or invalid.  */
extern contract_semantic map_contract_semantic	(const char *);
extern contract_level map_contract_level	(const char *);

/* Check if an attribute is a cxx contract attribute.  */
extern bool cxx_contract_attribute_p (const_tree);
extern bool cp_contract_assertion_p (const_tree);

/* Returns the default role.  */

inline contract_role *
get_default_contract_role ()
{
  return get_contract_role ("default");
}

/* Handle various command line arguments related to semantic mapping.  */
extern void handle_OPT_fcontract_build_level_ (const char *);
extern void handle_OPT_fcontract_assumption_mode_ (const char *);
extern void handle_OPT_fcontract_continuation_mode_ (const char *);
extern void handle_OPT_fcontract_role_ (const char *);
extern void handle_OPT_fcontract_semantic_ (const char *);

enum contract_matching_context
{
  cmc_declaration,
  cmc_override
};

/* True if NODE is any kind of contract.  */
#define CONTRACT_P(NODE)			\
  (TREE_CODE (NODE) == ASSERTION_STMT		\
   || TREE_CODE (NODE) == PRECONDITION_STMT	\
   || TREE_CODE (NODE) == POSTCONDITION_STMT)

/* True if NODE is a contract condition.  */
#define CONTRACT_CONDITION_P(NODE)		\
  (TREE_CODE (NODE) == PRECONDITION_STMT	\
   || TREE_CODE (NODE) == POSTCONDITION_STMT)

/* True if NODE is a precondition.  */
#define PRECONDITION_P(NODE)           \
  (TREE_CODE (NODE) == PRECONDITION_STMT)

/* True if NODE is a postcondition.  */
#define POSTCONDITION_P(NODE)          \
  (TREE_CODE (NODE) == POSTCONDITION_STMT)

#define CONTRACT_CHECK(NODE) \
  (TREE_CHECK3 (NODE, ASSERTION_STMT, PRECONDITION_STMT, POSTCONDITION_STMT))

/* True iff the FUNCTION_DECL NODE currently has any contracts.  */
#define DECL_HAS_CONTRACTS_P(NODE) \
  (DECL_CONTRACTS (NODE) != NULL_TREE)

/* For a FUNCTION_DECL of a guarded function, this points to a list of the pre
   and post contracts of the first decl of NODE in original order. */
#define DECL_CONTRACTS(NODE) \
  (find_contract (DECL_ATTRIBUTES (NODE)))

/* The next contract (if any) after this one in an attribute list.  */
#define CONTRACT_CHAIN(NODE) \
  (find_contract (TREE_CHAIN (NODE)))

/* The wrapper of the original source location of a list of contracts.  */
#define CONTRACT_SOURCE_LOCATION_WRAPPER(NODE) \
  (TREE_PURPOSE (TREE_VALUE (NODE)))

/* The original source location of a list of contracts.  */
#define CONTRACT_SOURCE_LOCATION(NODE) \
  (EXPR_LOCATION (CONTRACT_SOURCE_LOCATION_WRAPPER (NODE)))

/* The actual code _STMT for a contract attribute.  */
#define CONTRACT_STATEMENT(NODE) \
  (TREE_VALUE (TREE_VALUE (NODE)))

/* True if the contract semantic was specified literally. If true, the
   contract mode is an identifier containing the semantic. Otherwise,
   it is a TREE_LIST whose TREE_VALUE is the level and whose TREE_PURPOSE
   is the role.  */
#define CONTRACT_LITERAL_MODE_P(NODE) \
  (CONTRACT_MODE (NODE) != NULL_TREE \
   && TREE_CODE (CONTRACT_MODE (NODE)) == IDENTIFIER_NODE)

/* The identifier denoting the literal semantic of the contract.  */
#define CONTRACT_LITERAL_SEMANTIC(NODE) \
  (TREE_OPERAND (NODE, 0))

/* The written "mode" of the contract. Either an IDENTIFIER with the
   literal semantic or a TREE_LIST containing the level and role.  */
#define CONTRACT_MODE(NODE) \
  (TREE_OPERAND (CONTRACT_CHECK (NODE), 0))

/* The identifier denoting the build level of the contract. */
#define CONTRACT_LEVEL(NODE)		\
  (TREE_VALUE (CONTRACT_MODE (NODE)))

/* The identifier denoting the role of the contract */
#define CONTRACT_ROLE(NODE)		\
  (TREE_PURPOSE (CONTRACT_MODE (NODE)))

/* The parsed condition of the contract.  */
#define CONTRACT_CONDITION(NODE) \
  (TREE_OPERAND (CONTRACT_CHECK (NODE), 1))

/* True iff the condition of the contract NODE is not yet parsed.  */
#define CONTRACT_CONDITION_DEFERRED_P(NODE) \
  (TREE_CODE (CONTRACT_CONDITION (NODE)) == DEFERRED_PARSE)

/* The raw comment of the contract.  */
#define CONTRACT_COMMENT(NODE) \
  (TREE_OPERAND (CONTRACT_CHECK (NODE), 2))

/* The VAR_DECL of a postcondition result. For deferred contracts, this
   is an IDENTIFIER.  */
#define POSTCONDITION_IDENTIFIER(NODE) \
  (TREE_OPERAND (POSTCONDITION_STMT_CHECK (NODE), 3))

/* For a FUNCTION_DECL of a guarded function, this holds the function decl
   where pre contract checks are emitted.  */
#define DECL_PRE_FN(NODE) \
  (get_precondition_function ((NODE)))

/* For a FUNCTION_DECL of a guarded function, this holds the function decl
   where post contract checks are emitted.  */
#define DECL_POST_FN(NODE) \
  (get_postcondition_function ((NODE)))

/* True iff the FUNCTION_DECL is the pre function for a guarded function.  */
#define DECL_IS_PRE_FN_P(NODE) \
  (DECL_ABSTRACT_ORIGIN (NODE) && DECL_PRE_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)

/* True iff the FUNCTION_DECL is the post function for a guarded function.  */
#define DECL_IS_POST_FN_P(NODE) \
  (DECL_ABSTRACT_ORIGIN (NODE) && DECL_POST_FN (DECL_ABSTRACT_ORIGIN (NODE)) == NODE)

extern void remove_contract_attributes		(tree);
extern void copy_contract_attributes		(tree, tree);
extern void remap_contracts			(tree, tree, tree, bool);
extern void maybe_update_postconditions		(tree);
extern void rebuild_postconditions		(tree);
extern bool check_postcondition_result		(tree, tree, location_t);
extern tree get_precondition_function		(tree);
extern tree get_postcondition_function		(tree);
extern void duplicate_contracts			(tree, tree);
extern void match_deferred_contracts		(tree);
extern void defer_guarded_contract_match	(tree, tree, tree);
extern bool diagnose_misapplied_contracts	(tree);
extern tree finish_contract_attribute		(tree, tree);
extern tree invalidate_contract			(tree);
extern void update_late_contract		(tree, tree, tree);
extern tree splice_out_contracts		(tree);
extern bool all_attributes_are_contracts_p	(tree);
extern void inherit_base_contracts		(tree, tree);
extern tree apply_postcondition_to_return	(tree);
extern void start_function_contracts		(tree);
extern void finish_function_contracts		(tree);
extern void set_contract_functions		(tree, tree, tree);
extern tree build_contract_check		(tree);
extern void emit_assertion			(tree);

#endif /* ! GCC_CP_CONTRACT_H */