diff options
author | Justin Squirek <squirek@adacore.com> | 2022-08-31 14:52:11 +0000 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-12 10:16:51 +0200 |
commit | a968d80d0e89e847a1928842b7de166a6d42c92e (patch) | |
tree | 4190c36a86a777293a7ca1be5847c291b1eacd8a /gcc/ada/contracts.ads | |
parent | 46ba7ae3c6eea45cc03de5fb00c8084cdc760d64 (diff) | |
download | gcc-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.ads | 36 |
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); |