aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/contracts.ads
diff options
context:
space:
mode:
authorJustin Squirek <squirek@adacore.com>2022-08-31 14:52:11 +0000
committerMarc Poulhiès <poulhies@adacore.com>2022-09-12 10:16:51 +0200
commita968d80d0e89e847a1928842b7de166a6d42c92e (patch)
tree4190c36a86a777293a7ca1be5847c291b1eacd8a /gcc/ada/contracts.ads
parent46ba7ae3c6eea45cc03de5fb00c8084cdc760d64 (diff)
downloadgcc-a968d80d0e89e847a1928842b7de166a6d42c92e.zip
gcc-a968d80d0e89e847a1928842b7de166a6d42c92e.tar.gz
gcc-a968d80d0e89e847a1928842b7de166a6d42c92e.tar.bz2
[Ada] Tech debt: Expansion of contracts
This patch modifies the expansion of contracts such that the statements and declarations of a subprogram with post-execution checks get moved to a local internally generated subprogram which the original subprogram calls directly followed by the required post-execution checks. This differs from the current implementation which requires delicate machinary which coordinates with the finalization process to emulate the desired behavior within the "at end" procedure. gcc/ada/ * contracts.adb, contracts.ads (Analyze_Pragmas_In_Declarations): Added to aid in the new expansion model so that pragmas relating to contracts can get processed early before the rest of the subprogram containing them. (Build_Subprogram_Contract_Wrapper): Created to do the majority of expansion for postconditions. It builds a local wrapper with the statements and declarations within a given subprogram. (Is_Prologue_Renaming): Moved out from Process_Preconditions to be used generally within the contracts package. (Build_Entry_Contract_Wrapper): Moved from exp_ch7. (Expand_Subprogram_Contract): Add new local variable Decls to store expanded declarations needed for evaluation of contracts. Call new wrapper building procedure and modify comments to match new expansion model. (Get_Postcond_Enabled): Deleted. (Get_Result_Object_For_Postcond): Deleted. (Get_Return_Success_For_Postcond): Deleted. (Process_Contract_Cases): Add new parameter to store declarations. (Process_Postconditions): Add new parameter to store declarations. (Process_Preconditions): Add new parameter to store declarations. Add code to move entry-call prologue renamings * einfo.ads: Document new field Wrapped_Statements and modify comment for Postconditions_Proc. * exp_attr.adb (Analyze_Attribute): Modify expansion of the 'Old attribute to recognize new expansion model and use Wrapped_Statements instead of Postconditions_Proc. * exp_ch6.adb (Add_Return): Remove special expansion for postconditions. (Expand_Call): Modify condition checking for calls to access subprogram wrappers to handle new expansion models. (Expand_Call_Helper): Remove special expansion for postconditions. (Expand_Non_Function_Return): Remove special expansion for postconditions. (Expand_Simple_Function_Return): Remove special expansion for postconditions. * exp_ch7.adb (Build_Finalizer): Deleted, but replaced by code in Build_Finalizer_Helper (Build_Finalizer_Helper): Renamed to Build_Finalizer, and special handling of 'Old objects removed. * exp_ch9.adb (Build_Contract_Wrapper): Renamed and moved to contracts package. * exp_prag.adb (Expand_Pragma_Contract_Cases): Delay analysis of contracts since they now instead get analyzed as part of the wrapper generation instead of after analysis of their corresponding subprogram's body. (Expand_Pragma_Check): Label expanded if-statements which come from the expansion of assertion statements as Comes_From_Check_Or_Contract. * freeze.adb (Freeze_Entity): Add special case to avoid freezing when a freeze node gets generated as part of the expansion of a postcondition check. * gen_il-gen-gen_nodes.adb: Add new flag Comes_From_Check_Or_Contract. * gen_il-fields.ads: Add new field Wrapped_Statements. Add new flag Comes_From_Check_Or_Contract. * gen_il-gen-gen_entities.adb: Add new field Wrapped_Statements. * ghost.adb (Is_OK_Declaration): Replace Name_uPostconditions with Name_uWrapped_Statements. (Is_OK_Statement): Simplify condition due to the loss of Original_Node as a result of the new expansion model of contracts and use new flag Comes_From_Check_Or_Contract in its place. * inline.adb (Declare_Postconditions_Result): Replace Name_uPostconditions with Name_uWrapped_Statements. (Expand_Inlined_Call): Replace Name_uPostconditions with Name_uWrapped_Statements. * lib.adb, lib.ads (ipu): Created to aid in debugging. * lib-xref.adb (Generate_References): Remove special handling for postcondition procedures. * sem_attr.adb (Analyze_Attribute_Old_Result): Add new context in which 'Old can appear due to the changes in expansion. Replace Name_uPostconditions with Name_uWrapped_Statements. (Result): Replace Name_uPostconditions with Name_uWrapped_Statements. * sem_ch11.adb (Analyze_Handled_Statements): Remove check to exclude warnings on useless assignments within postcondition procedures since postconditions no longer get isolated into separate subprograms. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Modify expansion of generic subprogram bodies so that contracts (and their associated pragmas) get analyzed first. (Analyze_Subprogram_Body_Helper): Remove global HSS variable due to the HSS of the body potentially changing during the expansion of contracts. In cases where it was used instead directly call Handled_Statement_Sequence. Modify expansion of subprogram bodies so that contracts (and their associated pragmas) get analyzed first. (Check_Missing_Return): Create local HSS variable instead of using a global one. (Move_Pragmas): Use new pragma table instead of an explicit list. * sem_elab.adb (Is_Postconditions_Proc): Deleted since the new scheme of expansion no longer divides postcondition checks to a separate subprogram and so cannot be easily identified (similar to pre-condition checks). (Info_Call): Remove info printing for _Postconditions subprograms. (Is_Assertion_Pragma_Target): Remove check for postconditions procedure (Is_Bridge_Target): Remove check for postconditions procedure. (Get_Invocation_Attributes): Remove unneeded local variables and check for postconditions procedure. (Output_Call): Remove info printing for _Postconditions subprograms. * sem_prag.adb, sem_prag.ads: Add new Pragma table for pragmas significant to subprograms, along with tech-debt comment. (Check_Arg_Is_Local_Name): Modified to recognize the new _Wrapped_Statements internal subprogram and the new expansion model. (Relocate_Pragmas_To_Body): Replace Name_uPostconditions with Name_uWrapped_Statements. * sem_res.adb (Resolve_Entry_Call): Add conditional to detect both contract based wrappers of entries, but also wrappers generated as part of general contract expansion (e.g. local postconditions subprograms). * sem_util.adb (Accessibility_Level): Verify 'Access is not taken based on a component of a function result. (Has_Significant_Contracts): Replace Name_uPostconditions with Name_uWrapped_Statements. (Same_Or_Aliased_Subprogram): Add conditional to detect and obtain the original subprogram based on the new concept of "postcondition" wrappers. * sinfo.ads: Add documentation for new flag Comes_From_Check_Or_Contract. * snames.ads-tmpl: Remove Name_uPostconditions and add Name_uWrapped_Statements
Diffstat (limited to 'gcc/ada/contracts.ads')
-rw-r--r--gcc/ada/contracts.ads36
1 files changed, 21 insertions, 15 deletions
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 5178373..bde32ff 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -64,6 +64,16 @@ package Contracts is
procedure Analyze_Contracts (L : List_Id);
-- Analyze the contracts of all eligible constructs found in list L
+ procedure Analyze_Pragmas_In_Declarations (Body_Id : Entity_Id);
+ -- Perform early analysis of pragmas at the top of a given subprogram's
+ -- declarations.
+ --
+ -- The purpose of this is to analyze contract-related pragmas for later
+ -- processing, but also to handle other such pragmas before these
+ -- declarations get moved to an internal wrapper as part of contract
+ -- expansion. For example, pragmas Inline, Ghost, Volatile all need to
+ -- apply directly to the subprogram and not be moved to a wrapper.
+
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of entry or
-- subprogram body Body_Id as if they appeared at the end of a declarative
@@ -177,6 +187,17 @@ package Contracts is
-- Depends
-- Global
+ procedure Build_Entry_Contract_Wrapper (E : Entity_Id; Decl : Node_Id);
+ -- Build the body of a wrapper procedure for an entry or entry family that
+ -- has contract cases, preconditions, or postconditions, and add it to the
+ -- freeze actions of the related synchronized type.
+ --
+ -- The body first verifies the preconditions and case guards of the
+ -- contract cases, then invokes the entry [family], and finally verifies
+ -- the postconditions and the consequences of the contract cases. E denotes
+ -- the entry family. Decl denotes the declaration of the enclosing
+ -- synchronized type.
+
procedure Create_Generic_Contract (Unit : Node_Id);
-- Create a contract node for a generic package, generic subprogram, or a
-- generic body denoted by Unit by collecting all source contract-related
@@ -188,21 +209,6 @@ package Contracts is
-- denoted by Body_Decl. In addition, freeze the contract of the nearest
-- enclosing package body.
- function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's Postcond_Enabled
- -- object created during the expansion of the subprogram's postconditions.
-
- function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's
- -- Result_Object_For_Postcond object created during the expansion of the
- -- subprogram's postconditions.
-
- function Get_Return_Success_For_Postcond
- (Subp : Entity_Id) return Entity_Id;
- -- Get the defining identifier for a subprogram's
- -- Return_Success_For_Postcond object created during the expansion of the
- -- subprogram's postconditions.
-
procedure Inherit_Subprogram_Contract
(Subp : Entity_Id;
From_Subp : Entity_Id);