public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-4014] [Ada] Ada2022: AI12-0195 overriding class-wide pre/postconditions
@ 2021-10-01 6:15 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-10-01 6:15 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:475e1d240086365da3e240fb9199eb1c5ad511f8
commit r12-4014-g475e1d240086365da3e240fb9199eb1c5ad511f8
Author: Javier Miranda <miranda@adacore.com>
Date: Mon Aug 2 09:16:47 2021 -0400
[Ada] Ada2022: AI12-0195 overriding class-wide pre/postconditions
gcc/ada/
* contracts.ads (Make_Class_Precondition_Subps): New subprogram.
(Merge_Class_Conditions): New subprogram.
(Process_Class_Conditions_At_Freeze_Point): New subprogram.
* contracts.adb (Check_Class_Condition): New subprogram.
(Set_Class_Condition): New subprogram.
(Analyze_Contracts): Remove code analyzing class-wide-clone
subprogram since it is no longer built.
(Process_Spec_Postconditions): Avoid processing twice seen
subprograms.
(Process_Preconditions): Simplify its functionality to
non-class-wide preconditions.
(Process_Preconditions_For): No action needed for wrappers and
helpers.
(Make_Class_Precondition_Subps): New subprogram.
(Process_Class_Conditions_At_Freeze_Point): New subprogram.
(Merge_Class_Conditions): New subprogram.
* exp_ch6.ads (Install_Class_Preconditions_Check): New
subprogram.
* exp_ch6.adb (Expand_Call_Helper): Install class-wide
preconditions check on dispatching primitives that have or
inherit class-wide preconditions.
(Freeze_Subprogram): Remove code for null procedures with
preconditions.
(Install_Class_Preconditions_Check): New subprogram.
* exp_util.ads (Build_Class_Wide_Expression): Lower the
complexity of this subprogram; out-mode formal Needs_Wrapper
since this functionality is now provided by a new subprogram.
(Get_Mapped_Entity): New subprogram.
(Map_Formals): New subprogram.
* exp_util.adb (Build_Class_Wide_Expression): Lower the
complexity of this subprogram. Its previous functionality is now
provided by subprograms Needs_Wrapper and Check_Class_Condition.
(Add_Parent_DICs): Map the overridden primitive to the
overriding one.
(Get_Mapped_Entity): New subprogram.
(Map_Formals): New subprogram.
(Update_Primitives_Mapping): Adding assertion.
* freeze.ads (Check_Inherited_Conditions): Subprogram made
public with added formal to support late overriding.
* freeze.adb (Check_Inherited_Conditions): New implementation;
builds the dispatch table wrapper required for class-wide
pre/postconditions; added support for late overriding.
(Needs_Wrapper): New subprogram.
* sem.ads (Inside_Class_Condition_Preanalysis): New global
variable.
* sem_disp.ads (Covered_Interface_Primitives): New subprogram.
* sem_disp.adb (Covered_Interface_Primitives): New subprogram.
(Check_Dispatching_Context): Skip checking context of
dispatching calls during preanalysis of class-wide conditions
since at that stage the expression is not installed yet on its
definite context.
(Check_Dispatching_Call): Skip checking 6.1.1(18.2/5) by
AI12-0412 on helpers and wrappers internally built for
supporting class-wide conditions; for late-overriding
subprograms call Check_Inherited_Conditions to build the
dispatch-table wrapper (if required).
(Propagate_Tag): Adding call to
Install_Class_Preconditions_Check.
* sem_util.ads (Build_Class_Wide_Clone_Body): Removed.
(Build_Class_Wide_Clone_Call): Removed.
(Build_Class_Wide_Clone_Decl): Removed.
(Class_Condition): New subprogram.
(Nearest_Class_Condition_Subprogram): New subprogram.
* sem_util.adb (Build_Class_Wide_Clone_Body): Removed.
(Build_Class_Wide_Clone_Call): Removed.
(Build_Class_Wide_Clone_Decl): Removed.
(Class_Condition): New subprogram.
(Nearest_Class_Condition_Subprogram): New subprogram.
(Eligible_For_Conditional_Evaluation): No need to evaluate
class-wide conditions during preanalysis since the expression is
not installed on its definite context.
* einfo.ads (Class_Wide_Clone): Removed.
(Class_Postconditions): New attribute.
(Class_Preconditions): New attribute.
(Class_Preconditions_Subprogram): New attribute.
(Dynamic_Call_Helper): New attribute.
(Ignored_Class_Postconditions): New attribute.
(Ignored_Class_Preconditions): New attribute.
(Indirect_Call_Wrapper): New attribute.
(Is_Dispatch_Table_Wrapper): New attribute.
(Static_Call_Helper): New attribute.
* exp_attr.adb (Expand_N_Attribute_Reference): When the prefix
is of an access-to-subprogram type that has class-wide
preconditions and an indirect-call wrapper of such subprogram is
available, replace the prefix by the wrapper.
* exp_ch3.adb (Build_Class_Condition_Subprograms): New
subprogram.
(Register_Dispatch_Table_Wrappers): New subprogram.
* exp_disp.adb (Build_Class_Wide_Check): Removed; class-wide
precondition checks now rely on internally built helpers.
* sem_ch13.adb (Analyze_Aspect_Specifications): Set initial
value of attributes Class_Preconditions, Class_Postconditions,
Ignored_Class_Preconditions and Ignored_Class_Postconditions.
These values are later updated with the full pre/postcondition
by Merge_Class_Conditions.
(Freeze_Entity_Checks): Call
Process_Class_Conditions_At_Freeze_Point.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove code
building the body of the class-wide clone subprogram since it is
no longer required.
(Install_Entity): Adding assertion.
* sem_prag.adb (Analyze_Pre_Post_Condition_In_Decl_Part): Remove
code building and analyzing the class-wide clone subprogram; no
longer required.
(Build_Pragma_Check_Equivalent): Adjust call to
Build_Class_Wide_Expression since the formal named Needs_Wrapper
has been removed.
* sem_attr.adb (Analyze_Attribute_Old_Result): Skip processing
these attributes during preanalysis of class-wide conditions
since at that stage the expression is not installed yet on its
definite context.
* sem_res.adb (Resolve_Actuals): Skip applying RM 3.9.2(9/1) and
SPARK RM 6.1.7(3) on actuals of internal helpers and wrappers
built to support class-wide preconditions.
* sem_ch5.adb (Process_Bounds): Do not generate a constant
declaration for the bounds when we are preanalyzing a class-wide
condition.
(Analyze_Loop_Parameter_Specification): Handle preanalysis of
quantified expression placed in the outermost expression of a
class-wide condition.
* ghost.adb (Check_Ghost_Context): No check required during
preanalysis of class-wide conditions.
* gen_il-fields.ads (Opt_Field_Enum): Adding
Class_Postconditions, Class_Preconditions,
Class_Preconditions_Subprogram, Dynamic_Call_Helper,
Ignored_Class_Postconditions, Ignored_Class_Preconditions,
Indirect_Call_Wrapper, Is_Dispatch_Table_Wrapper,
Static_Call_Helper.
* gen_il-gen-gen_entities.adb (Is_Dispatch_Table_Wrapper):
Adding semantic flag Is_Dispatch_Table_Wrapper; removing
semantic field Class_Wide_Clone; adding semantic fields for
Class_Postconditions, Class_Preconditions,
Class_Preconditions_Subprogram, Dynamic_Call_Helper,
Ignored_Class_Postconditions, Indirect_Call_Wrapper,
Ignored_Class_Preconditions, and Static_Call_Helper.
Diff:
---
gcc/ada/contracts.adb | 1641 +++++++++++++++++++++++++++++------
gcc/ada/contracts.ads | 25 +
gcc/ada/einfo.ads | 75 +-
gcc/ada/exp_attr.adb | 14 +
gcc/ada/exp_ch3.adb | 92 ++
gcc/ada/exp_ch6.adb | 387 ++++++++-
gcc/ada/exp_ch6.ads | 3 +
gcc/ada/exp_disp.adb | 225 -----
gcc/ada/exp_util.adb | 183 ++--
gcc/ada/exp_util.ads | 48 +-
gcc/ada/freeze.adb | 573 +++++++++---
gcc/ada/freeze.ads | 9 +
gcc/ada/gen_il-fields.ads | 10 +-
gcc/ada/gen_il-gen-gen_entities.adb | 10 +-
gcc/ada/ghost.adb | 9 +
gcc/ada/sem.ads | 4 +
gcc/ada/sem_attr.adb | 10 +
gcc/ada/sem_ch13.adb | 40 +
gcc/ada/sem_ch5.adb | 10 +
gcc/ada/sem_ch6.adb | 24 +-
gcc/ada/sem_disp.adb | 110 +++
gcc/ada/sem_disp.ads | 4 +
gcc/ada/sem_prag.adb | 38 +-
gcc/ada/sem_res.adb | 9 +
gcc/ada/sem_util.adb | 261 ++----
gcc/ada/sem_util.ads | 42 +-
26 files changed, 2843 insertions(+), 1013 deletions(-)
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 705f197148c..2726486d200 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -47,6 +47,8 @@ with Sem_Ch12; use Sem_Ch12;
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Prag; use Sem_Prag;
+with Sem_Res; use Sem_Res;
+with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
@@ -66,6 +68,16 @@ package body Contracts is
--
-- Part_Of
+ procedure Check_Class_Condition
+ (Cond : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id;
+ Is_Precondition : Boolean);
+ -- Perform checking of class-wide pre/postcondition Cond inherited by Subp
+ -- from Par_Subp. Is_Precondition enables check specific for preconditions.
+ -- In SPARK_Mode, an inherited operation that is not overridden but has
+ -- inherited modified conditions pre/postconditions is illegal.
+
procedure Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id : Entity_Id);
-- Perform checking of external properties pragmas that is common to both
@@ -77,6 +89,12 @@ package body Contracts is
-- well as Contract_Cases, Subprogram_Variant, invariants and predicates.
-- Body_Id denotes the entity of the subprogram body.
+ procedure Set_Class_Condition
+ (Kind : Condition_Kind;
+ Subp : Entity_Id;
+ Cond : Node_Id);
+ -- Set the class-wide Kind condition of Subp
+
-----------------------
-- Add_Contract_Item --
-----------------------
@@ -386,23 +404,7 @@ package body Contracts is
| N_Generic_Subprogram_Declaration
| N_Subprogram_Declaration
then
- declare
- Subp_Id : constant Entity_Id := Defining_Entity (Decl);
-
- begin
- Analyze_Entry_Or_Subprogram_Contract (Subp_Id);
-
- -- If analysis of a class-wide pre/postcondition indicates
- -- that a class-wide clone is needed, analyze its declaration
- -- now. Its body is created when the body of the original
- -- operation is analyzed (and rewritten).
-
- if Is_Subprogram (Subp_Id)
- and then Present (Class_Wide_Clone (Subp_Id))
- then
- Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id)));
- end if;
- end;
+ Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
-- Entry or subprogram bodies
@@ -1491,6 +1493,141 @@ package body Contracts is
(Type_Or_Obj_Id => Type_Id);
end Analyze_Type_Contract;
+ ---------------------------
+ -- Check_Class_Condition --
+ ---------------------------
+
+ procedure Check_Class_Condition
+ (Cond : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id;
+ Is_Precondition : Boolean)
+ is
+ function Check_Entity (N : Node_Id) return Traverse_Result;
+ -- Check reference to formal of inherited operation or to primitive
+ -- operation of root type.
+
+ ------------------
+ -- Check_Entity --
+ ------------------
+
+ function Check_Entity (N : Node_Id) return Traverse_Result is
+ New_E : Entity_Id;
+ Orig_E : Entity_Id;
+
+ begin
+ if Nkind (N) = N_Identifier
+ and then Present (Entity (N))
+ and then
+ (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
+ and then
+ (Nkind (Parent (N)) /= N_Attribute_Reference
+ or else Attribute_Name (Parent (N)) /= Name_Class)
+ then
+ -- These checks do not apply to dispatching calls within the
+ -- condition, but only to calls whose static tag is that of
+ -- the parent type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ and then Present (Controlling_Argument (Parent (N)))
+ then
+ return OK;
+ end if;
+
+ -- Determine whether entity has a renaming
+
+ Orig_E := Entity (N);
+ New_E := Get_Mapped_Entity (Orig_E);
+
+ if Present (New_E) then
+
+ -- AI12-0166: A precondition for a protected operation
+ -- cannot include an internal call to a protected function
+ -- of the type. In the case of an inherited condition for an
+ -- overriding operation, both the operation and the function
+ -- are given by primitive wrappers.
+
+ if Is_Precondition
+ and then Ekind (New_E) = E_Function
+ and then Is_Primitive_Wrapper (New_E)
+ and then Is_Primitive_Wrapper (Subp)
+ and then Scope (Subp) = Scope (New_E)
+ then
+ Error_Msg_Node_2 := Wrapped_Entity (Subp);
+ Error_Msg_NE
+ ("internal call to& cannot appear in inherited "
+ & "precondition of protected operation&",
+ Subp, Wrapped_Entity (New_E));
+ end if;
+ end if;
+
+ -- Check that there are no calls left to abstract operations if
+ -- the current subprogram is not abstract.
+
+ if Present (New_E)
+ and then Nkind (Parent (N)) = N_Function_Call
+ and then N = Name (Parent (N))
+ then
+ if not Is_Abstract_Subprogram (Subp)
+ and then Is_Abstract_Subprogram (New_E)
+ then
+ Error_Msg_Sloc := Sloc (Current_Scope);
+ Error_Msg_Node_2 := Subp;
+
+ if Comes_From_Source (Subp) then
+ Error_Msg_NE
+ ("cannot call abstract subprogram & in inherited "
+ & "condition for&#", Subp, New_E);
+ else
+ Error_Msg_NE
+ ("cannot call abstract subprogram & in inherited "
+ & "condition for inherited&#", Subp, New_E);
+ end if;
+
+ -- In SPARK mode, report error on inherited condition for an
+ -- inherited operation if it contains a call to an overriding
+ -- operation, because this implies that the pre/postconditions
+ -- of the inherited operation have changed silently.
+
+ elsif SPARK_Mode = On
+ and then Warn_On_Suspicious_Contract
+ and then Present (Alias (Subp))
+ and then Present (New_E)
+ and then Comes_From_Source (New_E)
+ then
+ Error_Msg_N
+ ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
+ Parent (Subp));
+ Error_Msg_Sloc := Sloc (New_E);
+ Error_Msg_Node_2 := Subp;
+ Error_Msg_NE
+ ("\overriding of&# forces overriding of&",
+ Parent (Subp), New_E);
+ end if;
+ end if;
+ end if;
+
+ return OK;
+ end Check_Entity;
+
+ procedure Check_Condition_Entities is
+ new Traverse_Proc (Check_Entity);
+
+ -- Start of processing for Check_Class_Condition
+
+ begin
+ -- No check required if the subprograms match
+
+ if Par_Subp = Subp then
+ return;
+ end if;
+
+ Update_Primitives_Mapping (Par_Subp, Subp);
+ Map_Formals (Par_Subp, Subp);
+ Check_Condition_Entities (Cond);
+ end Check_Class_Condition;
+
-----------------------------
-- Create_Generic_Contract --
-----------------------------
@@ -1900,7 +2037,7 @@ package body Contracts is
procedure Add_Stable_Property_Contracts
(Subp_Id : Entity_Id; Class_Present : Boolean)
is
- Loc : constant Source_Ptr := Sloc (Subp_Id);
+ Loc : constant Source_Ptr := Sloc (Subp_Id);
procedure Insert_Stable_Property_Check
(Formal : Entity_Id; Property_Function : Entity_Id);
@@ -2552,13 +2689,38 @@ package body Contracts is
---------------------------------
procedure Process_Spec_Postconditions is
- Subps : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Seen : Subprogram_List (Subps'Range) := (others => Empty);
+
+ function Seen_Subp (Subp_Id : Entity_Id) return Boolean;
+ -- Return True if the contract of subprogram Subp_Id has been
+ -- processed.
+
+ ---------------
+ -- Seen_Subp --
+ ---------------
+
+ function Seen_Subp (Subp_Id : Entity_Id) return Boolean is
+ begin
+ for Index in Seen'Range loop
+ if Seen (Index) = Subp_Id then
+ return True;
+ end if;
+ end loop;
+
+ return False;
+ end Seen_Subp;
+
+ -- Local variables
+
Item : Node_Id;
Items : Node_Id;
Prag : Node_Id;
Subp_Id : Entity_Id;
+ -- Start of processing for Process_Spec_Postconditions
+
begin
-- Process the contract
@@ -2589,7 +2751,7 @@ package body Contracts is
Subp_Id := Ultimate_Alias (Subp_Id);
end if;
- -- Wrappers of class-wide pre/post conditions reference the
+ -- Wrappers of class-wide pre/postconditions reference the
-- parent primitive that has the inherited contract.
if Is_Wrapper (Subp_Id)
@@ -2600,7 +2762,9 @@ package body Contracts is
Items := Contract (Subp_Id);
- if Present (Items) then
+ if not Seen_Subp (Subp_Id) and then Present (Items) then
+ Seen (Index) := Subp_Id;
+
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
if Pragma_Name (Prag) = Name_Postcondition
@@ -2657,10 +2821,6 @@ package body Contracts is
---------------------------
procedure Process_Preconditions is
- Class_Pre : Node_Id := Empty;
- -- The sole [inherited] class-wide precondition pragma that applies
- -- to the subprogram.
-
Insert_Node : Node_Id := Empty;
-- The insertion node after which all pragma Check equivalents are
-- inserted.
@@ -2669,21 +2829,12 @@ package body Contracts is
-- Determine whether arbitrary declaration Decl denotes a renaming of
-- a discriminant or protection field _object.
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
- -- Merge two class-wide preconditions by "or else"-ing them. The
- -- changes are accumulated in parameter Into. Update the error
- -- message of Into.
-
procedure Prepend_To_Decls (Item : Node_Id);
-- Prepend a single item to the declarations of the subprogram body
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
- -- Save a class-wide precondition into Class_Pre, or prepend a normal
- -- precondition to the declarations of the body and analyze it.
-
- procedure Process_Inherited_Preconditions;
- -- Collect all inherited class-wide preconditions and merge them into
- -- one big precondition to be evaluated as pragma Check.
+ procedure Prepend_Pragma_To_Decls (Prag : Node_Id);
+ -- Prepend a normal precondition to the declarations of the body and
+ -- analyze it.
procedure Process_Preconditions_For (Subp_Id : Entity_Id);
-- Collect all preconditions of subprogram Subp_Id and prepend their
@@ -2737,78 +2888,6 @@ package body Contracts is
return False;
end Is_Prologue_Renaming;
- -------------------------
- -- Merge_Preconditions --
- -------------------------
-
- procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
- function Expression_Arg (Prag : Node_Id) return Node_Id;
- -- Return the boolean expression argument of a precondition while
- -- updating its parentheses count for the subsequent merge.
-
- function Message_Arg (Prag : Node_Id) return Node_Id;
- -- Return the message argument of a precondition
-
- --------------------
- -- Expression_Arg --
- --------------------
-
- function Expression_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
-
- begin
- if Paren_Count (Arg) = 0 then
- Set_Paren_Count (Arg, 1);
- end if;
-
- return Arg;
- end Expression_Arg;
-
- -----------------
- -- Message_Arg --
- -----------------
-
- function Message_Arg (Prag : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
- begin
- return Get_Pragma_Arg (Last (Args));
- end Message_Arg;
-
- -- Local variables
-
- From_Expr : constant Node_Id := Expression_Arg (From);
- From_Msg : constant Node_Id := Message_Arg (From);
- Into_Expr : constant Node_Id := Expression_Arg (Into);
- Into_Msg : constant Node_Id := Message_Arg (Into);
- Loc : constant Source_Ptr := Sloc (Into);
-
- -- Start of processing for Merge_Preconditions
-
- begin
- -- Merge the two preconditions by "or else"-ing them
-
- Rewrite (Into_Expr,
- Make_Or_Else (Loc,
- Right_Opnd => Relocate_Node (Into_Expr),
- Left_Opnd => From_Expr));
-
- -- Merge the two error messages to produce a single message of the
- -- form:
-
- -- failed precondition from ...
- -- also failed inherited precondition from ...
-
- if not Exception_Locations_Suppressed then
- Start_String (Strval (Into_Msg));
- Store_String_Char (ASCII.LF);
- Store_String_Chars (" also ");
- Store_String_Chars (Strval (From_Msg));
-
- Set_Strval (Into_Msg, End_String);
- end if;
- end Merge_Preconditions;
-
----------------------
-- Prepend_To_Decls --
----------------------
@@ -2829,28 +2908,27 @@ package body Contracts is
Prepend_To (Decls, Item);
end Prepend_To_Decls;
- ------------------------------
- -- Prepend_To_Decls_Or_Save --
- ------------------------------
+ -----------------------------
+ -- Prepend_Pragma_To_Decls --
+ -----------------------------
- procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
+ procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is
Check_Prag : Node_Id;
begin
- Check_Prag := Build_Pragma_Check_Equivalent (Prag);
-
- -- Save the sole class-wide precondition (if any) for the next
- -- step, where it will be merged with inherited preconditions.
+ -- Skip the sole class-wide precondition (if any) since it is
+ -- processed by Merge_Class_Conditions.
if Class_Present (Prag) then
- pragma Assert (No (Class_Pre));
- Class_Pre := Check_Prag;
+ null;
-- Accumulate the corresponding Check pragmas at the top of the
-- declarations. Prepending the items ensures that they will be
-- evaluated in their original order.
else
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+
if Present (Insert_Node) then
Insert_After (Insert_Node, Check_Prag);
else
@@ -2859,87 +2937,7 @@ package body Contracts is
Analyze (Check_Prag);
end if;
- end Prepend_To_Decls_Or_Save;
-
- -------------------------------------
- -- Process_Inherited_Preconditions --
- -------------------------------------
-
- procedure Process_Inherited_Preconditions is
- Subps : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
-
- Item : Node_Id;
- Items : Node_Id;
- Prag : Node_Id;
- Subp_Id : Entity_Id;
-
- begin
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide preconditions.
-
- for Index in Subps'Range loop
- Subp_Id := Subps (Index);
-
- if Present (Alias (Subp_Id)) then
- Subp_Id := Ultimate_Alias (Subp_Id);
- end if;
-
- -- Wrappers of class-wide pre/post conditions reference the
- -- parent primitive that has the inherited contract.
-
- if Is_Wrapper (Subp_Id)
- and then Present (LSP_Subprogram (Subp_Id))
- then
- Subp_Id := LSP_Subprogram (Subp_Id);
- end if;
-
- Items := Contract (Subp_Id);
-
- if Present (Items) then
- Prag := Pre_Post_Conditions (Items);
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Item :=
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Spec_Id,
- Inher_Id => Subp_Id);
-
- -- The pragma Check equivalent of the class-wide
- -- precondition is still created even though the
- -- pragma may be ignored because the equivalent
- -- performs semantic checks.
-
- if Is_Checked (Prag) then
-
- -- The spec of an inherited subprogram already
- -- yielded a class-wide precondition. Merge the
- -- existing precondition with the current one
- -- using "or else".
-
- if Present (Class_Pre) then
- Merge_Preconditions (Item, Class_Pre);
- else
- Class_Pre := Item;
- end if;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
- end loop;
-
- -- Add the merged class-wide preconditions
-
- if Present (Class_Pre) then
- Prepend_To_Decls (Class_Pre);
- Analyze (Class_Pre);
- end if;
- end Process_Inherited_Preconditions;
+ end Prepend_Pragma_To_Decls;
-------------------------------
-- Process_Preconditions_For --
@@ -2983,7 +2981,7 @@ package body Contracts is
N => Body_Decl);
end if;
- Prepend_To_Decls_Or_Save (Prag);
+ Prepend_Pragma_To_Decls (Prag);
end if;
Prag := Next_Pragma (Prag);
@@ -3008,7 +3006,7 @@ package body Contracts is
if Pragma_Name (Decl) = Name_Precondition
and then Is_Checked (Decl)
then
- Prepend_To_Decls_Or_Save (Decl);
+ Prepend_Pragma_To_Decls (Decl);
end if;
-- Skip internally generated code
@@ -3073,22 +3071,21 @@ package body Contracts is
Next (Decl);
end loop;
- end if;
- -- The processing of preconditions is done in reverse order (body
- -- first), because each pragma Check equivalent is inserted at the
- -- top of the declarations. This ensures that the final order is
- -- consistent with following diagram:
+ -- The processing of preconditions is done in reverse order (body
+ -- first), because each pragma Check equivalent is inserted at the
+ -- top of the declarations. This ensures that the final order is
+ -- consistent with following diagram:
- -- <inherited preconditions>
- -- <preconditions from spec>
- -- <preconditions from body>
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
- Process_Preconditions_For (Body_Id);
+ Process_Preconditions_For (Body_Id);
+ end if;
if Present (Spec_Id) then
Process_Preconditions_For (Spec_Id);
- Process_Inherited_Preconditions;
end if;
end Process_Preconditions;
@@ -3139,6 +3136,12 @@ package body Contracts is
elsif Is_Ignored_Ghost_Entity (Subp_Id) then
return;
+ -- No action needed for helpers and indirect-call wrapper built to
+ -- support class-wide preconditions.
+
+ elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then
+ return;
+
-- Do not re-expand the same contract. This scenario occurs when a
-- construct is rewritten into something else during its analysis
-- (expression functions for instance).
@@ -3605,61 +3608,1191 @@ package body Contracts is
end if;
end Instantiate_Subprogram_Contract;
- ----------------------------------------
- -- Save_Global_References_In_Contract --
- ----------------------------------------
+ -----------------------------------
+ -- Make_Class_Precondition_Subps --
+ -----------------------------------
- procedure Save_Global_References_In_Contract
- (Templ : Node_Id;
- Gen_Id : Entity_Id)
+ procedure Make_Class_Precondition_Subps
+ (Subp_Id : Entity_Id;
+ Late_Overriding : Boolean := False)
is
- procedure Save_Global_References_In_List (First_Prag : Node_Id);
- -- Save all global references in contract-related source pragmas found
- -- in the list, starting with pragma First_Prag.
+ Loc : constant Source_Ptr := Sloc (Subp_Id);
+ Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
- ------------------------------------
- -- Save_Global_References_In_List --
- ------------------------------------
+ procedure Add_Indirect_Call_Wrapper;
+ -- Build the indirect-call wrapper and append it to the freezing actions
+ -- of Tagged_Type.
- procedure Save_Global_References_In_List (First_Prag : Node_Id) is
- Prag : Node_Id;
+ procedure Add_Call_Helper
+ (Helper_Id : Entity_Id;
+ Is_Dynamic : Boolean);
+ -- Factorizes code for building a call helper with the given identifier
+ -- and append it to the freezing actions of Tagged_Type. Is_Dynamic
+ -- controls building the static or dynamic version of the helper.
- begin
- Prag := First_Prag;
- while Present (Prag) loop
- if Is_Generic_Contract_Pragma (Prag) then
- Save_Global_References (Prag);
+ -------------------------------
+ -- Add_Indirect_Call_Wrapper --
+ -------------------------------
+
+ procedure Add_Indirect_Call_Wrapper is
+
+ function Build_ICW_Body return Node_Id;
+ -- Build the body of the indirect call wrapper
+
+ function Build_ICW_Decl return Node_Id;
+ -- Build the declaration of the indirect call wrapper
+
+ --------------------
+ -- Build_ICW_Body --
+ --------------------
+
+ function Build_ICW_Body return Node_Id is
+ ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id);
+ Spec : constant Node_Id := Parent (ICW_Id);
+ Body_Spec : Node_Id;
+ Call : Node_Id;
+ ICW_Body : Node_Id;
+
+ begin
+ Body_Spec := Copy_Subprogram_Spec (Spec);
+
+ -- Build call to wrapped subprogram
+
+ declare
+ Actuals : constant List_Id := Empty_List;
+ Formal_Spec : Entity_Id :=
+ First (Parameter_Specifications (Spec));
+ begin
+ -- Build parameter association & call
+
+ while Present (Formal_Spec) loop
+ Append_To (Actuals,
+ New_Occurrence_Of
+ (Defining_Identifier (Formal_Spec), Loc));
+ Next (Formal_Spec);
+ end loop;
+
+ if Ekind (ICW_Id) = E_Procedure then
+ Call :=
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Subp_Id, Loc),
+ Parameter_Associations => Actuals);
+ else
+ Call :=
+ Make_Simple_Return_Statement (Loc,
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Subp_Id, Loc),
+ Parameter_Associations => Actuals));
+ end if;
+ end;
+
+ ICW_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification => Body_Spec,
+ Declarations => New_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call)));
+
+ -- The new operation is internal and overriding indicators do not
+ -- apply.
+
+ Set_Must_Override (Body_Spec, False);
+
+ return ICW_Body;
+ end Build_ICW_Body;
+
+ --------------------
+ -- Build_ICW_Decl --
+ --------------------
+
+ function Build_ICW_Decl return Node_Id is
+ ICW_Id : constant Entity_Id :=
+ Make_Defining_Identifier (Loc,
+ New_External_Name (Chars (Subp_Id),
+ Suffix => "ICW",
+ Suffix_Index => Source_Offset (Loc)));
+ Decl : Node_Id;
+ Spec : Node_Id;
+
+ begin
+ Spec := Copy_Subprogram_Spec (Parent (Subp_Id));
+ Set_Must_Override (Spec, False);
+ Set_Must_Not_Override (Spec, False);
+ Set_Defining_Unit_Name (Spec, ICW_Id);
+ Mutate_Ekind (ICW_Id, Ekind (Subp_Id));
+ Set_Is_Public (ICW_Id);
+
+ -- The indirect call wrapper is commonly used for indirect calls
+ -- but inlined for direct calls performed from the DTW.
+
+ Set_Is_Inlined (ICW_Id);
+
+ if Nkind (Spec) = N_Procedure_Specification then
+ Set_Null_Present (Spec, False);
end if;
- Prag := Next_Pragma (Prag);
- end loop;
- end Save_Global_References_In_List;
+ Decl := Make_Subprogram_Declaration (Loc, Spec);
- -- Local variables
+ -- Link original subprogram to indirect wrapper and vice versa
- Items : constant Node_Id := Contract (Defining_Entity (Templ));
+ Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id);
+ Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id);
- -- Start of processing for Save_Global_References_In_Contract
+ -- Inherit debug info flag to allow debugging the wrapper
- begin
- -- The entity of the analyzed generic copy must be on the scope stack
- -- to ensure proper detection of global references.
+ if Needs_Debug_Info (Subp_Id) then
+ Set_Debug_Info_Needed (ICW_Id);
+ end if;
- Push_Scope (Gen_Id);
+ return Decl;
+ end Build_ICW_Decl;
- if Permits_Aspect_Specifications (Templ)
- and then Has_Aspects (Templ)
- then
- Save_Global_References_In_Aspects (Templ);
- end if;
+ -- Local Variables
- if Present (Items) then
- Save_Global_References_In_List (Pre_Post_Conditions (Items));
- Save_Global_References_In_List (Contract_Test_Cases (Items));
- Save_Global_References_In_List (Classifications (Items));
- end if;
+ ICW_Body : Node_Id;
+ ICW_Decl : Node_Id;
- Pop_Scope;
- end Save_Global_References_In_Contract;
+ -- Start of processing for Add_Indirect_Call_Wrapper
+
+ begin
+ pragma Assert (No (Indirect_Call_Wrapper (Subp_Id)));
+
+ ICW_Decl := Build_ICW_Decl;
+
+ Ensure_Freeze_Node (Tagged_Type);
+ Append_Freeze_Action (Tagged_Type, ICW_Decl);
+ Analyze (ICW_Decl);
+
+ ICW_Body := Build_ICW_Body;
+ Append_Freeze_Action (Tagged_Type, ICW_Body);
+
+ -- We cannot defer the analysis of this ICW wrapper when it is
+ -- built as a consequence of building its partner DTW wrapper
+ -- at the freezing point of the tagged type.
+
+ if Is_Dispatch_Table_Wrapper (Subp_Id) then
+ Analyze (ICW_Body);
+ end if;
+ end Add_Indirect_Call_Wrapper;
+
+ ---------------------
+ -- Add_Call_Helper --
+ ---------------------
+
+ procedure Add_Call_Helper
+ (Helper_Id : Entity_Id;
+ Is_Dynamic : Boolean)
+ is
+ function Build_Call_Helper_Body return Node_Id;
+ -- Build the body of a call helper
+
+ function Build_Call_Helper_Decl return Node_Id;
+ -- Build the declaration of a call helper
+
+ function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id;
+ -- Build the specification of the helper
+
+ ----------------------------
+ -- Build_Call_Helper_Body --
+ ----------------------------
+
+ function Build_Call_Helper_Body return Node_Id is
+
+ function Copy_And_Update_References
+ (Expr : Node_Id) return Node_Id;
+ -- Copy Expr updating references to formals of Helper_Id; update
+ -- also references to loop identifiers of quantified expressions.
+
+ --------------------------------
+ -- Copy_And_Update_References --
+ --------------------------------
+
+ function Copy_And_Update_References
+ (Expr : Node_Id) return Node_Id
+ is
+ Assoc_List : constant Elist_Id := New_Elmt_List;
+
+ procedure Map_Quantified_Expression_Loop_Identifiers;
+ -- Traverse Expr and append to Assoc_List the mapping of loop
+ -- identifers of quantified expressions with its new copy.
+
+ ------------------------------------------------
+ -- Map_Quantified_Expression_Loop_Identifiers --
+ ------------------------------------------------
+
+ procedure Map_Quantified_Expression_Loop_Identifiers is
+ function Map_Loop_Param (N : Node_Id) return Traverse_Result;
+ -- Append to Assoc_List the mapping of loop identifers of
+ -- quantified expressions with its new copy.
+
+ --------------------
+ -- Map_Loop_Param --
+ --------------------
+
+ function Map_Loop_Param (N : Node_Id) return Traverse_Result
+ is
+ begin
+ if Nkind (N) = N_Loop_Parameter_Specification
+ and then Nkind (Parent (N)) = N_Quantified_Expression
+ then
+ declare
+ Def_Id : constant Entity_Id :=
+ Defining_Identifier (N);
+ begin
+ Append_Elmt (Def_Id, Assoc_List);
+ Append_Elmt (New_Copy (Def_Id), Assoc_List);
+ end;
+ end if;
+
+ return OK;
+ end Map_Loop_Param;
+
+ procedure Map_Quantified_Expressions is
+ new Traverse_Proc (Map_Loop_Param);
+
+ begin
+ Map_Quantified_Expressions (Expr);
+ end Map_Quantified_Expression_Loop_Identifiers;
+
+ -- Local variables
+
+ Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id);
+ Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id);
+
+ -- Start of processing for Copy_And_Update_References
+
+ begin
+ while Present (Subp_Formal_Id) loop
+ Append_Elmt (Subp_Formal_Id, Assoc_List);
+ Append_Elmt (Helper_Formal_Id, Assoc_List);
+
+ Next_Formal (Subp_Formal_Id);
+ Next_Formal (Helper_Formal_Id);
+ end loop;
+
+ Map_Quantified_Expression_Loop_Identifiers;
+
+ return New_Copy_Tree (Expr, Map => Assoc_List);
+ end Copy_And_Update_References;
+
+ -- Local variables
+
+ Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id));
+ Body_Id : Entity_Id;
+ Body_Spec : Node_Id;
+ Body_Stmts : Node_Id;
+ Helper_Body : Node_Id;
+ Return_Expr : Node_Id;
+
+ -- Start of processing for Build_Call_Helper_Body
+
+ begin
+ pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id)));
+ pragma Assert (No (Corresponding_Body (Helper_Decl)));
+
+ Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id));
+ Body_Spec := Build_Call_Helper_Spec (Body_Id);
+
+ Set_Corresponding_Body (Helper_Decl, Body_Id);
+ Set_Must_Override (Body_Spec, False);
+
+ if Present (Class_Preconditions (Subp_Id)) then
+ Return_Expr :=
+ Copy_And_Update_References (Class_Preconditions (Subp_Id));
+
+ -- When the subprogram is compiled with assertions disabled the
+ -- helper just returns True; done to avoid reporting errors at
+ -- link time since a unit may be compiled with assertions disabled
+ -- and another (which depends on it) compiled with assertions
+ -- enabled.
+
+ else
+ pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id)));
+ Return_Expr := New_Occurrence_Of (Standard_True, Loc);
+ end if;
+
+ Body_Stmts :=
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Make_Simple_Return_Statement (Loc, Return_Expr)));
+
+ Helper_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification => Body_Spec,
+ Declarations => New_List,
+ Handled_Statement_Sequence => Body_Stmts);
+
+ return Helper_Body;
+ end Build_Call_Helper_Body;
+
+ ----------------------------
+ -- Build_Call_Helper_Decl --
+ ----------------------------
+
+ function Build_Call_Helper_Decl return Node_Id is
+ Decl : Node_Id;
+ Spec : Node_Id;
+
+ begin
+ Spec := Build_Call_Helper_Spec (Helper_Id);
+ Set_Must_Override (Spec, False);
+ Set_Must_Not_Override (Spec, False);
+ Set_Is_Inlined (Helper_Id);
+ Set_Is_Public (Helper_Id);
+
+ Decl := Make_Subprogram_Declaration (Loc, Spec);
+
+ -- Inherit debug info flag from Subp_Id to Helper_Id to allow
+ -- debugging of the helper subprogram.
+
+ if Needs_Debug_Info (Subp_Id) then
+ Set_Debug_Info_Needed (Helper_Id);
+ end if;
+
+ return Decl;
+ end Build_Call_Helper_Decl;
+
+ ----------------------------
+ -- Build_Call_Helper_Spec --
+ ----------------------------
+
+ function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id
+ is
+ Spec : constant Node_Id := Parent (Subp_Id);
+ Def_Id : constant Node_Id := Defining_Unit_Name (Spec);
+ Formal : Entity_Id;
+ Func_Formals : constant List_Id := New_List;
+ P_Spec : constant List_Id := Parameter_Specifications (Spec);
+ Par_Formal : Node_Id;
+ Param : Node_Id;
+ Param_Type : Node_Id;
+
+ begin
+ -- Create a list of formal parameters with the same types as the
+ -- original subprogram but changing the controlling formal.
+
+ Param := First (P_Spec);
+ Formal := First_Formal (Def_Id);
+ while Present (Formal) loop
+ Par_Formal := Parent (Formal);
+
+ if Is_Dynamic and then Is_Controlling_Formal (Formal) then
+ if Nkind (Parameter_Type (Par_Formal))
+ = N_Access_Definition
+ then
+ Param_Type :=
+ Copy_Separate_Tree (Parameter_Type (Par_Formal));
+ Rewrite (Subtype_Mark (Param_Type),
+ Make_Attribute_Reference (Loc,
+ Prefix => Relocate_Node (Subtype_Mark (Param_Type)),
+ Attribute_Name => Name_Class));
+
+ else
+ Param_Type :=
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Occurrence_Of (Etype (Formal), Loc),
+ Attribute_Name => Name_Class);
+ end if;
+ else
+ Param_Type := New_Occurrence_Of (Etype (Formal), Loc);
+ end if;
+
+ Append_To (Func_Formals,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc, Chars (Formal)),
+ In_Present => In_Present (Par_Formal),
+ Out_Present => Out_Present (Par_Formal),
+ Null_Exclusion_Present => Null_Exclusion_Present
+ (Par_Formal),
+ Parameter_Type => Param_Type));
+
+ Next (Param);
+ Next_Formal (Formal);
+ end loop;
+
+ return
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name => Spec_Id,
+ Parameter_Specifications => Func_Formals,
+ Result_Definition =>
+ New_Occurrence_Of (Standard_Boolean, Loc));
+ end Build_Call_Helper_Spec;
+
+ -- Local variables
+
+ Helper_Body : Node_Id;
+ Helper_Decl : Node_Id;
+
+ -- Start of processing for Add_Call_Helper
+
+ begin
+ Helper_Decl := Build_Call_Helper_Decl;
+ Mutate_Ekind (Helper_Id, Ekind (Subp_Id));
+
+ -- Add the helper to the freezing actions of the tagged type
+
+ Ensure_Freeze_Node (Tagged_Type);
+ Append_Freeze_Action (Tagged_Type, Helper_Decl);
+ Analyze (Helper_Decl);
+
+ Helper_Body := Build_Call_Helper_Body;
+ Append_Freeze_Action (Tagged_Type, Helper_Body);
+
+ -- If this helper is built as part of building the DTW at the
+ -- freezing point of its tagged type then we cannot defer
+ -- its analysis.
+
+ if Late_Overriding then
+ pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id));
+ Analyze (Helper_Body);
+ end if;
+ end Add_Call_Helper;
+
+ -- Local variables
+
+ Helper_Id : Entity_Id;
+
+ -- Start of processing for Make_Class_Precondition_Subps
+
+ begin
+ if Present (Class_Preconditions (Subp_Id))
+ or Present (Ignored_Class_Preconditions (Subp_Id))
+ then
+ pragma Assert
+ (Comes_From_Source (Subp_Id)
+ or else Is_Dispatch_Table_Wrapper (Subp_Id));
+
+ if No (Dynamic_Call_Helper (Subp_Id)) then
+
+ -- Build and add to the freezing actions of Tagged_Type its
+ -- dynamic-call helper.
+
+ Helper_Id :=
+ Make_Defining_Identifier (Loc,
+ New_External_Name (Chars (Subp_Id),
+ Suffix => "DP",
+ Suffix_Index => Source_Offset (Loc)));
+ Add_Call_Helper (Helper_Id, Is_Dynamic => True);
+
+ -- Link original subprogram to helper and vice versa
+
+ Set_Dynamic_Call_Helper (Subp_Id, Helper_Id);
+ Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
+ end if;
+
+ if not Is_Abstract_Subprogram (Subp_Id)
+ and then No (Static_Call_Helper (Subp_Id))
+ then
+ -- Build and add to the freezing actions of Tagged_Type its
+ -- static-call helper.
+
+ Helper_Id :=
+ Make_Defining_Identifier (Loc,
+ New_External_Name (Chars (Subp_Id),
+ Suffix => "SP",
+ Suffix_Index => Source_Offset (Loc)));
+
+ Add_Call_Helper (Helper_Id, Is_Dynamic => False);
+
+ -- Link original subprogram to helper and vice versa
+
+ Set_Static_Call_Helper (Subp_Id, Helper_Id);
+ Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id);
+
+ -- Build and add to the freezing actions of Tagged_Type the
+ -- indirect-call wrapper.
+
+ Add_Indirect_Call_Wrapper;
+ end if;
+ end if;
+ end Make_Class_Precondition_Subps;
+
+ ----------------------------------------------
+ -- Process_Class_Conditions_At_Freeze_Point --
+ ----------------------------------------------
+
+ procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is
+
+ procedure Check_Class_Conditions (Spec_Id : Entity_Id);
+ -- Check class-wide pre/postconditions of Spec_Id
+
+ function Has_Class_Postconditions_Subprogram
+ (Spec_Id : Entity_Id) return Boolean;
+ -- Return True if Spec_Id has (or inherits) a postconditions subprogram.
+
+ function Has_Class_Preconditions_Subprogram
+ (Spec_Id : Entity_Id) return Boolean;
+ -- Return True if Spec_Id has (or inherits) a preconditions subprogram.
+
+ ----------------------------
+ -- Check_Class_Conditions --
+ ----------------------------
+
+ procedure Check_Class_Conditions (Spec_Id : Entity_Id) is
+ Par_Subp : Entity_Id;
+
+ begin
+ for Kind in Condition_Kind loop
+ Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id);
+
+ if Present (Par_Subp) then
+ Check_Class_Condition
+ (Cond => Class_Condition (Kind, Par_Subp),
+ Subp => Spec_Id,
+ Par_Subp => Par_Subp,
+ Is_Precondition => Kind in Ignored_Class_Precondition
+ | Class_Precondition);
+ end if;
+ end loop;
+ end Check_Class_Conditions;
+
+ -----------------------------------------
+ -- Has_Class_Postconditions_Subprogram --
+ -----------------------------------------
+
+ function Has_Class_Postconditions_Subprogram
+ (Spec_Id : Entity_Id) return Boolean is
+ begin
+ return
+ Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Spec_Id,
+ Kind => Class_Postcondition))
+ or else
+ Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Spec_Id,
+ Kind => Ignored_Class_Postcondition));
+ end Has_Class_Postconditions_Subprogram;
+
+ ----------------------------------------
+ -- Has_Class_Preconditions_Subprogram --
+ ----------------------------------------
+
+ function Has_Class_Preconditions_Subprogram
+ (Spec_Id : Entity_Id) return Boolean is
+ begin
+ return
+ Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Spec_Id,
+ Kind => Class_Precondition))
+ or else
+ Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Spec_Id,
+ Kind => Ignored_Class_Precondition));
+ end Has_Class_Preconditions_Subprogram;
+
+ -- Local variables
+
+ Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
+ Prim : Entity_Id;
+
+ -- Start of processing for Process_Class_Conditions_At_Freeze_Point
+
+ begin
+ while Present (Prim_Elmt) loop
+ Prim := Node (Prim_Elmt);
+
+ if Has_Class_Preconditions_Subprogram (Prim)
+ or else Has_Class_Postconditions_Subprogram (Prim)
+ then
+ if Comes_From_Source (Prim) then
+ if Has_Significant_Contract (Prim) then
+ Merge_Class_Conditions (Prim);
+ end if;
+
+ -- Handle wrapper of protected operation
+
+ elsif Is_Primitive_Wrapper (Prim) then
+ Merge_Class_Conditions (Prim);
+
+ -- Check inherited class-wide conditions, excluding internal
+ -- entities built for mapping of interface primitives.
+
+ elsif Is_Derived_Type (Typ)
+ and then Present (Alias (Prim))
+ and then No (Interface_Alias (Prim))
+ then
+ Check_Class_Conditions (Prim);
+ end if;
+ end if;
+
+ Next_Elmt (Prim_Elmt);
+ end loop;
+ end Process_Class_Conditions_At_Freeze_Point;
+
+ ----------------------------
+ -- Merge_Class_Conditions --
+ ----------------------------
+
+ procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is
+
+ procedure Preanalyze_Condition
+ (Subp : Entity_Id;
+ Expr : Node_Id);
+ -- Preanalyze the class-wide condition Expr of Subp
+
+ procedure Process_Inherited_Conditions (Kind : Condition_Kind);
+ -- Collect all inherited class-wide conditions of Spec_Id and merge
+ -- them into one big condition.
+
+ --------------------------
+ -- Preanalyze_Condition --
+ --------------------------
+
+ procedure Preanalyze_Condition
+ (Subp : Entity_Id;
+ Expr : Node_Id)
+ is
+ procedure Clear_Unset_References;
+ -- Clear unset references on formals of Subp since preanalysis
+ -- occurs in a place unrelated to the actual code.
+
+ procedure Remove_Controlling_Arguments;
+ -- Traverse Expr and clear the Controlling_Argument of calls to
+ -- nonabstract functions.
+
+ procedure Remove_Formals (Id : Entity_Id);
+ -- Remove formals from homonym chains and make them not visible
+
+ ----------------------------
+ -- Clear_Unset_References --
+ ----------------------------
+
+ procedure Clear_Unset_References is
+ F : Entity_Id := First_Formal (Subp);
+
+ begin
+ while Present (F) loop
+ Set_Unset_Reference (F, Empty);
+ Next_Formal (F);
+ end loop;
+ end Clear_Unset_References;
+
+ ----------------------------------
+ -- Remove_Controlling_Arguments --
+ ----------------------------------
+
+ procedure Remove_Controlling_Arguments is
+ function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result;
+ -- Reset the Controlling_Argument of calls to nonabstract
+ -- function calls.
+
+ ---------------------
+ -- Remove_Ctrl_Arg --
+ ---------------------
+
+ function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is
+ begin
+ if Nkind (N) = N_Function_Call
+ and then Present (Controlling_Argument (N))
+ and then not Is_Abstract_Subprogram (Entity (Name (N)))
+ then
+ Set_Controlling_Argument (N, Empty);
+ end if;
+
+ return OK;
+ end Remove_Ctrl_Arg;
+
+ procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg);
+ begin
+ Remove_Ctrl_Args (Expr);
+ end Remove_Controlling_Arguments;
+
+ --------------------
+ -- Remove_Formals --
+ --------------------
+
+ procedure Remove_Formals (Id : Entity_Id) is
+ F : Entity_Id := First_Formal (Id);
+
+ begin
+ while Present (F) loop
+ Set_Is_Immediately_Visible (F, False);
+ Remove_Homonym (F);
+ Next_Formal (F);
+ end loop;
+ end Remove_Formals;
+
+ -- Start of processing for Preanalyze_Condition
+
+ begin
+ pragma Assert (Present (Expr));
+ pragma Assert (Inside_Class_Condition_Preanalysis = False);
+
+ Push_Scope (Subp);
+ Install_Formals (Subp);
+ Inside_Class_Condition_Preanalysis := True;
+
+ Preanalyze_And_Resolve (Expr, Standard_Boolean);
+
+ Inside_Class_Condition_Preanalysis := False;
+ Remove_Formals (Subp);
+ Pop_Scope;
+
+ -- Traverse Expr and clear the Controlling_Argument of calls to
+ -- nonabstract functions. Required since the preanalyzed condition
+ -- is not yet installed on its definite context and will be cloned
+ -- and extended in derivations with additional conditions.
+
+ Remove_Controlling_Arguments;
+
+ -- Clear also attribute Unset_Reference; again because preanalysis
+ -- occurs in a place unrelated to the actual code.
+
+ Clear_Unset_References;
+ end Preanalyze_Condition;
+
+ ----------------------------------
+ -- Process_Inherited_Conditions --
+ ----------------------------------
+
+ procedure Process_Inherited_Conditions (Kind : Condition_Kind) is
+ Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
+ Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id);
+ Seen : Subprogram_List (Subps'Range) := (others => Empty);
+
+ function Inherit_Condition
+ (Par_Subp : Entity_Id;
+ Subp : Entity_Id) return Node_Id;
+ -- Inherit the class-wide condition from Par_Subp to Subp and adjust
+ -- all the references to formals in the inherited condition.
+
+ procedure Merge_Conditions (From : Node_Id; Into : Node_Id);
+ -- Merge two class-wide preconditions or postconditions (the former
+ -- are merged using "or else", and the latter are merged using "and-
+ -- then"). The changes are accumulated in parameter Into.
+
+ function Seen_Subp (Id : Entity_Id) return Boolean;
+ -- Return True if the contract of subprogram Id has been processed
+
+ -----------------------
+ -- Inherit_Condition --
+ -----------------------
+
+ function Inherit_Condition
+ (Par_Subp : Entity_Id;
+ Subp : Entity_Id) return Node_Id
+ is
+ Installed_Calls : constant Elist_Id := New_Elmt_List;
+
+ procedure Install_Original_Selected_Component (Expr : Node_Id);
+ -- Traverse the given expression searching for dispatching calls
+ -- to functions whose original nodes was a selected component,
+ -- and replacing them temporarily by a copy of their original
+ -- node. Modified calls are stored in the list Installed_Calls
+ -- (to undo this work later).
+
+ procedure Restore_Dispatching_Calls (Expr : Node_Id);
+ -- Undo the work done by Install_Original_Selected_Component.
+
+ -----------------------------------------
+ -- Install_Original_Selected_Component --
+ -----------------------------------------
+
+ procedure Install_Original_Selected_Component (Expr : Node_Id) is
+ function Install_Node (N : Node_Id) return Traverse_Result;
+ -- Process a single node
+
+ ------------------
+ -- Install_Node --
+ ------------------
+
+ function Install_Node (N : Node_Id) return Traverse_Result is
+ New_N : Node_Id;
+ Orig_Nod : Node_Id;
+
+ begin
+ if Nkind (N) = N_Function_Call
+ and then Nkind (Original_Node (N)) = N_Selected_Component
+ and then Is_Dispatching_Operation (Entity (Name (N)))
+ then
+ Orig_Nod := Original_Node (N);
+
+ -- Temporarily use the original node field to keep the
+ -- reference to this node (to undo this work later!).
+
+ New_N := New_Copy (N);
+ Set_Original_Node (New_N, Orig_Nod);
+ Append_Elmt (New_N, Installed_Calls);
+
+ Rewrite (N, Orig_Nod);
+ Set_Original_Node (N, New_N);
+ end if;
+
+ return OK;
+ end Install_Node;
+
+ procedure Install_Nodes is new Traverse_Proc (Install_Node);
+
+ begin
+ Install_Nodes (Expr);
+ end Install_Original_Selected_Component;
+
+ -------------------------------
+ -- Restore_Dispatching_Calls --
+ -------------------------------
+
+ procedure Restore_Dispatching_Calls (Expr : Node_Id) is
+ function Restore_Node (N : Node_Id) return Traverse_Result;
+ -- Process a single node
+
+ ------------------
+ -- Restore_Node --
+ ------------------
+
+ function Restore_Node (N : Node_Id) return Traverse_Result is
+ Orig_Sel_N : Node_Id;
+
+ begin
+ if Nkind (N) = N_Selected_Component
+ and then Nkind (Original_Node (N)) = N_Function_Call
+ and then Contains (Installed_Calls, Original_Node (N))
+ then
+ Orig_Sel_N := Original_Node (Original_Node (N));
+ pragma Assert (Nkind (Orig_Sel_N) = N_Selected_Component);
+ Rewrite (N, Original_Node (N));
+ Set_Original_Node (N, Orig_Sel_N);
+ end if;
+
+ return OK;
+ end Restore_Node;
+
+ procedure Restore_Nodes is new Traverse_Proc (Restore_Node);
+
+ begin
+ Restore_Nodes (Expr);
+ end Restore_Dispatching_Calls;
+
+ -- Local variables
+
+ Assoc_List : constant Elist_Id := New_Elmt_List;
+ Par_Formal_Id : Entity_Id := First_Formal (Par_Subp);
+ Subp_Formal_Id : Entity_Id := First_Formal (Subp);
+ New_Expr : Node_Id;
+ Class_Cond : Node_Id;
+
+ -- Start of processing for Inherit_Condition
+
+ begin
+ while Present (Par_Formal_Id) loop
+ Append_Elmt (Par_Formal_Id, Assoc_List);
+ Append_Elmt (Subp_Formal_Id, Assoc_List);
+
+ Next_Formal (Par_Formal_Id);
+ Next_Formal (Subp_Formal_Id);
+ end loop;
+
+ -- In order to properly preanalyze an inherited preanalyzed
+ -- condition that has occurrences of the Object.Operation
+ -- notation we must restore the original node; otherwise we
+ -- would report spurious errors.
+
+ Class_Cond := Class_Condition (Kind, Par_Subp);
+
+ Install_Original_Selected_Component (Class_Cond);
+ New_Expr := New_Copy_Tree (Class_Cond);
+ Restore_Dispatching_Calls (Class_Cond);
+
+ return New_Copy_Tree (New_Expr, Map => Assoc_List);
+ end Inherit_Condition;
+
+ ----------------------
+ -- Merge_Conditions --
+ ----------------------
+
+ procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is
+ function Expression_Arg (Expr : Node_Id) return Node_Id;
+ -- Return the boolean expression argument of a condition while
+ -- updating its parentheses count for the subsequent merge.
+
+ --------------------
+ -- Expression_Arg --
+ --------------------
+
+ function Expression_Arg (Expr : Node_Id) return Node_Id is
+ begin
+ if Paren_Count (Expr) = 0 then
+ Set_Paren_Count (Expr, 1);
+ end if;
+
+ return Expr;
+ end Expression_Arg;
+
+ -- Local variables
+
+ From_Expr : constant Node_Id := Expression_Arg (From);
+ Into_Expr : constant Node_Id := Expression_Arg (Into);
+ Loc : constant Source_Ptr := Sloc (Into);
+
+ -- Start of processing for Merge_Conditions
+
+ begin
+ case Kind is
+
+ -- Merge the two preconditions by "or else"-ing them
+
+ when Ignored_Class_Precondition
+ | Class_Precondition
+ =>
+ Rewrite (Into_Expr,
+ Make_Or_Else (Loc,
+ Right_Opnd => Relocate_Node (Into_Expr),
+ Left_Opnd => From_Expr));
+
+ -- Merge the two postconditions by "and then"-ing them
+
+ when Ignored_Class_Postcondition
+ | Class_Postcondition
+ =>
+ Rewrite (Into_Expr,
+ Make_And_Then (Loc,
+ Right_Opnd => Relocate_Node (Into_Expr),
+ Left_Opnd => From_Expr));
+ end case;
+ end Merge_Conditions;
+
+ ---------------
+ -- Seen_Subp --
+ ---------------
+
+ function Seen_Subp (Id : Entity_Id) return Boolean is
+ begin
+ for Index in Seen'Range loop
+ if Seen (Index) = Id then
+ return True;
+ end if;
+ end loop;
+
+ return False;
+ end Seen_Subp;
+
+ -- Local variables
+
+ Class_Cond : Node_Id;
+ Cond : Node_Id;
+ Subp_Id : Entity_Id;
+ Par_Prim : Entity_Id := Empty;
+ Par_Iface_Prims : Elist_Id := No_Elist;
+
+ -- Start of processing for Process_Inherited_Conditions
+
+ begin
+ Class_Cond := Class_Condition (Kind, Spec_Id);
+
+ -- Process parent primitives looking for nearest ancestor with
+ -- class-wide conditions.
+
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+
+ if No (Par_Prim)
+ and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ)
+ then
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Ultimate_Alias (Subp_Id);
+ end if;
+
+ -- Wrappers of class-wide pre/postconditions reference the
+ -- parent primitive that has the inherited contract and help
+ -- us to climb fast.
+
+ if Is_Wrapper (Subp_Id)
+ and then Present (LSP_Subprogram (Subp_Id))
+ then
+ Subp_Id := LSP_Subprogram (Subp_Id);
+ end if;
+
+ if not Seen_Subp (Subp_Id)
+ and then Present (Class_Condition (Kind, Subp_Id))
+ then
+ Seen (Index) := Subp_Id;
+ Par_Prim := Subp_Id;
+ Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim);
+
+ Cond := Inherit_Condition
+ (Subp => Spec_Id,
+ Par_Subp => Subp_Id);
+
+ if Present (Class_Cond) then
+ Merge_Conditions (Cond, Class_Cond);
+ else
+ Class_Cond := Cond;
+ end if;
+
+ Check_Class_Condition
+ (Cond => Class_Cond,
+ Subp => Spec_Id,
+ Par_Subp => Subp_Id,
+ Is_Precondition => Kind in Ignored_Class_Precondition
+ | Class_Precondition);
+ Build_Class_Wide_Expression
+ (Pragma_Or_Expr => Class_Cond,
+ Subp => Spec_Id,
+ Par_Subp => Subp_Id,
+ Adjust_Sloc => False);
+
+ -- We are done as soon as we process the nearest ancestor
+
+ exit;
+ end if;
+ end if;
+ end loop;
+
+ -- Process the contract of interface primitives not covered by
+ -- the nearest ancestor.
+
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+
+ if Is_Interface (Find_Dispatching_Type (Subp_Id)) then
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Ultimate_Alias (Subp_Id);
+ end if;
+
+ if not Seen_Subp (Subp_Id)
+ and then Present (Class_Condition (Kind, Subp_Id))
+ and then not Contains (Par_Iface_Prims, Subp_Id)
+ then
+ Seen (Index) := Subp_Id;
+
+ Cond := Inherit_Condition
+ (Subp => Spec_Id,
+ Par_Subp => Subp_Id);
+
+ Check_Class_Condition
+ (Cond => Cond,
+ Subp => Spec_Id,
+ Par_Subp => Subp_Id,
+ Is_Precondition => Kind in Ignored_Class_Precondition
+ | Class_Precondition);
+ Build_Class_Wide_Expression
+ (Pragma_Or_Expr => Cond,
+ Subp => Spec_Id,
+ Par_Subp => Subp_Id,
+ Adjust_Sloc => False);
+
+ if Present (Class_Cond) then
+ Merge_Conditions (Cond, Class_Cond);
+ else
+ Class_Cond := Cond;
+ end if;
+ end if;
+ end if;
+ end loop;
+
+ Set_Class_Condition (Kind, Spec_Id, Class_Cond);
+ end Process_Inherited_Conditions;
+
+ -- Local variables
+
+ Cond : Node_Id;
+
+ -- Start of processing for Merge_Class_Conditions
+
+ begin
+ for Kind in Condition_Kind loop
+ Cond := Class_Condition (Kind, Spec_Id);
+
+ -- If this subprogram has class-wide conditions then preanalyze
+ -- them before processing inherited conditions since conditions
+ -- are checked and merged from right to left.
+
+ if Present (Cond) then
+ Preanalyze_Condition (Spec_Id, Cond);
+ end if;
+
+ Process_Inherited_Conditions (Kind);
+
+ -- Preanalyze merged inherited conditions
+
+ if Cond /= Class_Condition (Kind, Spec_Id) then
+ Preanalyze_Condition (Spec_Id,
+ Class_Condition (Kind, Spec_Id));
+ end if;
+ end loop;
+ end Merge_Class_Conditions;
+
+ ----------------------------------------
+ -- Save_Global_References_In_Contract --
+ ----------------------------------------
+
+ procedure Save_Global_References_In_Contract
+ (Templ : Node_Id;
+ Gen_Id : Entity_Id)
+ is
+ procedure Save_Global_References_In_List (First_Prag : Node_Id);
+ -- Save all global references in contract-related source pragmas found
+ -- in the list, starting with pragma First_Prag.
+
+ ------------------------------------
+ -- Save_Global_References_In_List --
+ ------------------------------------
+
+ procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+ Prag : Node_Id := First_Prag;
+
+ begin
+ while Present (Prag) loop
+ if Is_Generic_Contract_Pragma (Prag) then
+ Save_Global_References (Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Save_Global_References_In_List;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (Defining_Entity (Templ));
+
+ -- Start of processing for Save_Global_References_In_Contract
+
+ begin
+ -- The entity of the analyzed generic copy must be on the scope stack
+ -- to ensure proper detection of global references.
+
+ Push_Scope (Gen_Id);
+
+ if Permits_Aspect_Specifications (Templ)
+ and then Has_Aspects (Templ)
+ then
+ Save_Global_References_In_Aspects (Templ);
+ end if;
+
+ if Present (Items) then
+ Save_Global_References_In_List (Pre_Post_Conditions (Items));
+ Save_Global_References_In_List (Contract_Test_Cases (Items));
+ Save_Global_References_In_List (Classifications (Items));
+ end if;
+
+ Pop_Scope;
+ end Save_Global_References_In_Contract;
+
+ -------------------------
+ -- Set_Class_Condition --
+ -------------------------
+
+ procedure Set_Class_Condition
+ (Kind : Condition_Kind;
+ Subp : Entity_Id;
+ Cond : Node_Id)
+ is
+ begin
+ case Kind is
+ when Class_Postcondition =>
+ Set_Class_Postconditions (Subp, Cond);
+
+ when Class_Precondition =>
+ Set_Class_Preconditions (Subp, Cond);
+
+ when Ignored_Class_Postcondition =>
+ Set_Ignored_Class_Postconditions (Subp, Cond);
+
+ when Ignored_Class_Precondition =>
+ Set_Ignored_Class_Preconditions (Subp, Cond);
+ end case;
+ end Set_Class_Condition;
end Contracts;
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index bfd482e3053..eb26ebf1332 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -216,6 +216,31 @@ package Contracts is
-- subprogram declaration template denoted by Templ. The instantiated
-- pragmas are added to list L.
+ procedure Make_Class_Precondition_Subps
+ (Subp_Id : Entity_Id;
+ Late_Overriding : Boolean := False);
+ -- Build helpers that at run time evaluate statically and dynamically the
+ -- class-wide preconditions of Subp_Id; build also the indirect-call
+ -- wrapper (ICW) required to check class-wide preconditions when the
+ -- subprogram is invoked through an access-to-subprogram, or when it
+ -- overrides an inherited class-wide precondition (see AI12-0195-1).
+ -- Late_Overriding enables special handling required for late-overriding
+ -- subprograms.
+
+ procedure Merge_Class_Conditions (Spec_Id : Entity_Id);
+ -- Merge and preanalyze all class-wide conditions of Spec_Id (class-wide
+ -- preconditions merged with operator or-else; class-wide postconditions
+ -- merged with operator and-then). Ignored pre/postconditions are also
+ -- merged since, although they are not required to generate code, their
+ -- preanalysis is required to perform semantic checks. Resulting merged
+ -- expressions are later installed by the expander in helper subprograms
+ -- which are invoked from the caller side; they are also used to build
+ -- the dispatch-table wrapper (DTW), if required.
+
+ procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id);
+ -- Merge, preanalyze, and check class-wide pre/postconditions of Typ
+ -- primitives.
+
procedure Save_Global_References_In_Contract
(Templ : Node_Id;
Gen_Id : Entity_Id);
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 94c56624fef..f890fe54230 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -610,12 +610,23 @@ package Einfo is
-- tables must be consulted to determine if there actually is an active
-- Suppress or Unsuppress pragma that applies to the entity.
--- Class_Wide_Clone
--- Defined on subprogram entities. Set if the subprogram has a class-wide
--- pre- or postcondition, and the expression contains calls to other
--- primitive funtions of the type. Used to implement properly the
--- semantics of inherited operations whose class-wide condition may
--- be different from that of the ancestor (See AI012-0195).
+-- Class_Postconditions
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- postconditions. Denotes the (and-then) expression built by merging
+-- inherited class-wide postconditions with its own class-wide
+-- postconditions.
+
+-- Class_Preconditions
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- preconditions. Denotes the (or-else) expression built by merging
+-- inherited class-wide preconditions with its own class-wide
+-- preconditions.
+
+-- Class_Preconditions_Subprogram
+-- Defined on subprogram entities. Set on subprogram helpers and also on
+-- the indirect-call wrapper internally built for subprograms that have
+-- class-wide preconditions. References the subprogram that has the
+-- class-wide preconditions.
-- Class_Wide_Type
-- Defined in all type entities. For a tagged type or subtype, returns
@@ -1029,6 +1040,11 @@ package Einfo is
-- associated with the tagged type. For an untagged record, contains
-- No_Elist.
+-- Dynamic_Call_Helper
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- preconditions. Denotes the helper that evaluates at run time the
+-- class-wide preconditions performing dispatching calls.
+
-- DTC_Entity
-- Defined in function and procedure entities. Set to Empty unless
-- the subprogram is dispatching in which case it references the
@@ -2182,6 +2198,18 @@ package Einfo is
-- "off" and indicates that all SPARK_Mode pragmas found within must
-- be ignored.
+-- Ignored_Class_Postconditions
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- postconditions. Denotes the (and-then) expression built by merging
+-- inherited ignored class-wide postconditions with its own ignored
+-- class-wide postconditions.
+
+-- Ignored_Class_Preconditions
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- preconditions. Denotes the (or-else) expression built by merging
+-- inherited ignored class-wide preconditions with its own ignored
+-- class-wide preconditions.
+
-- Implementation_Base_Type (synthesized)
-- Applies to all entities. For types, similar to Base_Type, but never
-- returns a private type when applied to a non-private type. Instead in
@@ -2216,6 +2244,12 @@ package Einfo is
-- is relocated to the corresponding package body, which must have a
-- corresponding nonlimited with_clause.
+-- Indirect_Call_Wrapper
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- preconditions. Denotes the internal wrapper that checks preconditions
+-- and invokes the subprogram body. Subp'Access points to the indirect
+-- call wrapper if available.
+
-- Initialization_Statements
-- Defined in constants and variables. For a composite object initialized
-- with an aggregate that has been converted to a sequence of
@@ -2507,6 +2541,11 @@ package Einfo is
-- Applies to all entities. Set to indicate to the backend that this
-- entity is associated with a dispatch table.
+-- Is_Dispatch_Table_Wrapper
+-- Applies to all entities. Set on wrappers built when the subprogram has
+-- class-wide preconditions or class-wide postconditions affected by
+-- overriding (AI12-0195).
+
-- Is_Dispatching_Operation
-- Defined in all entities. Set for procedures, functions, generic
-- procedures, and generic functions if the corresponding operation
@@ -4401,6 +4440,11 @@ package Einfo is
-- Default_Scalar_Storage_Order (High_Order_First) was active at the time
-- the record or array was declared and therefore applies to it.
+-- Static_Call_Helper
+-- Defined on subprogram entities. Set if the subprogram has class-wide
+-- preconditions. Denotes the helper that evaluates at runtime the
+-- class-wide preconditions performing static calls.
+
-- Static_Discrete_Predicate
-- Defined in discrete types/subtypes with static predicates (with the
-- two flags Has_Predicates and Has_Static_Predicate set). Set if the
@@ -4878,6 +4922,7 @@ package Einfo is
-- Is_Discrim_SO_Function
-- Is_Discriminant_Check_Function
-- Is_Dispatch_Table_Entity
+ -- Is_Dispatch_Table_Wrapper
-- Is_Dispatching_Operation
-- Is_Entry_Formal
-- Is_Exported
@@ -5484,7 +5529,14 @@ package Einfo is
-- Linker_Section_Pragma
-- Contract
-- Import_Pragma (non-generic case only)
- -- Class_Wide_Clone
+ -- Class_Postconditions
+ -- Class_Preconditions
+ -- Class_Preconditions_Subprogram
+ -- Dynamic_Call_Helper
+ -- Ignored_Class_Preconditions
+ -- Ignored_Class_Postconditions
+ -- Indirect_Call_Wrapper
+ -- Static_Call_Helper
-- Protected_Subprogram (non-generic case only)
-- SPARK_Pragma
-- Original_Protected_Subprogram
@@ -5840,7 +5892,14 @@ package Einfo is
-- Linker_Section_Pragma
-- Contract
-- Import_Pragma (non-generic case only)
- -- Class_Wide_Clone
+ -- Class_Postconditions
+ -- Class_Preconditions
+ -- Class_Preconditions_Subprogram
+ -- Dynamic_Call_Helper
+ -- Ignored_Class_Preconditions
+ -- Ignored_Class_Postconditions
+ -- Indirect_Call_Wrapper
+ -- Static_Call_Helper
-- Protected_Subprogram (non-generic case only)
-- SPARK_Pragma
-- Original_Protected_Subprogram
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index c962c2a8516..3e7bb838118 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -2216,6 +2216,20 @@ package body Exp_Attr is
if Is_Access_Protected_Subprogram_Type (Btyp) then
Expand_Access_To_Protected_Op (N, Pref, Typ);
+ -- If prefix is a subprogram that has class-wide preconditions and
+ -- an indirect-call wrapper (ICW) of such subprogram is available
+ -- then replace the prefix by the ICW.
+
+ elsif Is_Access_Subprogram_Type (Btyp)
+ and then Is_Entity_Name (Pref)
+ and then Present (Class_Preconditions (Entity (Pref)))
+ and then Present (Indirect_Call_Wrapper (Entity (Pref)))
+ then
+ Rewrite (Pref,
+ New_Occurrence_Of
+ (Indirect_Call_Wrapper (Entity (Pref)), Loc));
+ Analyze_And_Resolve (N, Typ);
+
-- If prefix is a type name, this is a reference to the current
-- instance of the type, within its initialization procedure.
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index 45d5baf51b4..418306f3040 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -26,6 +26,7 @@
with Aspects; use Aspects;
with Atree; use Atree;
with Checks; use Checks;
+with Contracts; use Contracts;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
@@ -5352,10 +5353,66 @@ package body Exp_Ch3 is
-------------------------------
procedure Expand_Freeze_Record_Type (N : Node_Id) is
+
+ procedure Build_Class_Condition_Subprograms (Typ : Entity_Id);
+ -- Create internal subprograms of Typ primitives that have class-wide
+ -- preconditions or postconditions; they are invoked by the caller to
+ -- evaluate the conditions.
+
procedure Build_Variant_Record_Equality (Typ : Entity_Id);
-- Create An Equality function for the untagged variant record Typ and
-- attach it to the TSS list.
+ procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id);
+ -- Register dispatch-table wrappers in the dispatch table of Typ
+
+ ---------------------------------------
+ -- Build_Class_Condition_Subprograms --
+ ---------------------------------------
+
+ procedure Build_Class_Condition_Subprograms (Typ : Entity_Id) is
+ Prim_List : constant Elist_Id := Primitive_Operations (Typ);
+ Prim_Elmt : Elmt_Id := First_Elmt (Prim_List);
+ Prim : Entity_Id;
+
+ begin
+ while Present (Prim_Elmt) loop
+ Prim := Node (Prim_Elmt);
+
+ -- Primitive with class-wide preconditions
+
+ if Comes_From_Source (Prim)
+ and then Has_Significant_Contract (Prim)
+ and then
+ (Present (Class_Preconditions (Prim))
+ or else Present (Ignored_Class_Preconditions (Prim)))
+ then
+ if Expander_Active then
+ Make_Class_Precondition_Subps (Prim);
+ end if;
+
+ -- Wrapper of a primitive that has or inherits class-wide
+ -- preconditions.
+
+ elsif Is_Primitive_Wrapper (Prim)
+ and then
+ (Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Prim,
+ Kind => Class_Precondition))
+ or else
+ Present (Nearest_Class_Condition_Subprogram
+ (Spec_Id => Prim,
+ Kind => Ignored_Class_Precondition)))
+ then
+ if Expander_Active then
+ Make_Class_Precondition_Subps (Prim);
+ end if;
+ end if;
+
+ Next_Elmt (Prim_Elmt);
+ end loop;
+ end Build_Class_Condition_Subprograms;
+
-----------------------------------
-- Build_Variant_Record_Equality --
-----------------------------------
@@ -5417,6 +5474,27 @@ package body Exp_Ch3 is
end if;
end Build_Variant_Record_Equality;
+ --------------------------------------
+ -- Register_Dispatch_Table_Wrappers --
+ --------------------------------------
+
+ procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id) is
+ Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ));
+ Subp : Entity_Id;
+
+ begin
+ while Present (Elmt) loop
+ Subp := Node (Elmt);
+
+ if Is_Dispatch_Table_Wrapper (Subp) then
+ Append_Freeze_Actions (Typ,
+ Register_Primitive (Sloc (Subp), Subp));
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+ end Register_Dispatch_Table_Wrappers;
+
-- Local variables
Typ : constant Node_Id := Entity (N);
@@ -5666,6 +5744,13 @@ package body Exp_Ch3 is
if not Building_Static_DT (Typ) then
Append_Freeze_Actions (Typ, Make_DT (Typ));
+
+ -- Register dispatch table wrappers in the dispatch table.
+ -- It could not be done when these wrappers were built
+ -- because, at that stage, the dispatch table was not
+ -- available.
+
+ Register_Dispatch_Table_Wrappers (Typ);
end if;
end if;
@@ -5857,6 +5942,13 @@ package body Exp_Ch3 is
end loop;
end;
end if;
+
+ -- Build internal subprograms of primitives with class-wide
+ -- pre/postconditions.
+
+ if Is_Tagged_Type (Typ) then
+ Build_Class_Condition_Subprograms (Typ);
+ end if;
end Expand_Freeze_Record_Type;
------------------------------------
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 7717fa7c0ab..ffd14759a7f 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -73,8 +73,10 @@ with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
+with Sinput; use Sinput;
with Snames; use Snames;
with Stand; use Stand;
+with Stringt; use Stringt;
with Tbuild; use Tbuild;
with Uintp; use Uintp;
with Validsw; use Validsw;
@@ -4065,7 +4067,7 @@ package body Exp_Ch6 is
end;
end if;
- -- If the formal is class wide and the actual is an aggregate, force
+ -- If the formal is class-wide and the actual is an aggregate, force
-- evaluation so that the back end who does not know about class-wide
-- type, does not generate a temporary of the wrong size.
@@ -4250,6 +4252,16 @@ package body Exp_Ch6 is
Expand_Interface_Actuals (Call_Node);
end if;
+ -- Install class-wide preconditions runtime check when this is a
+ -- dispatching primitive that has or inherits class-wide preconditions;
+ -- otherwise no runtime check is installed.
+
+ if Nkind (Call_Node) in N_Subprogram_Call
+ and then Is_Dispatching_Operation (Subp)
+ then
+ Install_Class_Preconditions_Check (Call_Node);
+ end if;
+
-- Deals with Dispatch_Call if we still have a call, before expanding
-- extra actuals since this will be done on the re-analysis of the
-- dispatching call. Note that we do not try to shorten the actual list
@@ -7855,18 +7867,6 @@ package body Exp_Ch6 is
-- returned type may not be known yet (for private types).
Compute_Returns_By_Ref (Subp);
-
- -- When freezing a null procedure, analyze its delayed aspects now
- -- because we may not have reached the end of the declarative list when
- -- delayed aspects are normally analyzed. This ensures that dispatching
- -- calls are properly rewritten when the generated _Postcondition
- -- procedure is analyzed in the null procedure body.
-
- if Nkind (Parent (Subp)) = N_Procedure_Specification
- and then Null_Present (Parent (Subp))
- then
- Analyze_Entry_Or_Subprogram_Contract (Subp);
- end if;
end Freeze_Subprogram;
--------------------------
@@ -8101,6 +8101,367 @@ package body Exp_Ch6 is
end if;
end Insert_Post_Call_Actions;
+ ---------------------------------------
+ -- Install_Class_Preconditions_Check --
+ ---------------------------------------
+
+ procedure Install_Class_Preconditions_Check (Call_Node : Node_Id) is
+ Loc : constant Source_Ptr := Sloc (Call_Node);
+
+ function Build_Dynamic_Check_Helper_Call return Node_Id;
+ -- Build call to the helper runtime function of the nearest ancestor
+ -- of the target subprogram that dynamically evaluates the merged
+ -- or-else preconditions.
+
+ function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id;
+ -- Build message associated with the class-wide precondition of Subp_Id
+ -- indicating the call that caused it.
+
+ function Build_Static_Check_Helper_Call return Node_Id;
+ -- Build call to the helper runtime function of the nearest ancestor
+ -- of the target subprogram that dynamically evaluates the merged
+ -- or-else preconditions.
+
+ function Class_Preconditions_Subprogram
+ (Spec_Id : Entity_Id;
+ Dynamic : Boolean) return Node_Id;
+ -- Return the nearest ancestor of Spec_Id defining a helper function
+ -- that evaluates a combined or-else expression containing all the
+ -- inherited class-wide preconditions; Dynamic enables searching for
+ -- the helper that dynamically evaluates preconditions using dispatching
+ -- calls; if False it searches for the helper that statically evaluates
+ -- preconditions; return Empty when not available (which means that no
+ -- preconditions check is required).
+
+ -------------------------------------
+ -- Build_Dynamic_Check_Helper_Call --
+ -------------------------------------
+
+ function Build_Dynamic_Check_Helper_Call return Node_Id is
+ Spec_Id : constant Entity_Id := Entity (Name (Call_Node));
+ CW_Subp : constant Entity_Id :=
+ Class_Preconditions_Subprogram (Spec_Id,
+ Dynamic => True);
+ Helper_Id : constant Entity_Id :=
+ Dynamic_Call_Helper (CW_Subp);
+ Actuals : constant List_Id := New_List;
+ A : Node_Id := First_Actual (Call_Node);
+ F : Entity_Id := First_Formal (Helper_Id);
+
+ begin
+ while Present (A) loop
+
+ -- Ensure that the evaluation of the actuals will not produce
+ -- side effects.
+
+ Remove_Side_Effects (A);
+
+ Append_To (Actuals, New_Copy_Tree (A));
+ Next_Formal (F);
+ Next_Actual (A);
+ end loop;
+
+ return
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Helper_Id, Loc),
+ Parameter_Associations => Actuals);
+ end Build_Dynamic_Check_Helper_Call;
+
+ -------------------------
+ -- Build_Error_Message --
+ -------------------------
+
+ function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id is
+
+ procedure Append_Message
+ (Id : Entity_Id;
+ Is_First : in out Boolean);
+ -- Build the fragment of the message associated with subprogram Id;
+ -- Is_First facilitates identifying continuation messages.
+
+ --------------------
+ -- Append_Message --
+ --------------------
+
+ procedure Append_Message
+ (Id : Entity_Id;
+ Is_First : in out Boolean)
+ is
+ Prag : constant Node_Id := Get_Class_Wide_Pragma (Id,
+ Pragma_Precondition);
+ Msg : Node_Id;
+ Str_Id : String_Id;
+
+ begin
+ if No (Prag) or else Is_Ignored (Prag) then
+ return;
+ end if;
+
+ Msg := Expression (Last (Pragma_Argument_Associations (Prag)));
+ Str_Id := Strval (Msg);
+
+ if Is_First then
+ Is_First := False;
+
+ Append (Global_Name_Buffer, Strval (Msg));
+
+ if Id /= Subp_Id
+ and then Name_Buffer (1 .. 19) = "failed precondition"
+ then
+ Insert_Str_In_Name_Buffer ("inherited ", 8);
+ end if;
+
+ else
+ declare
+ Str : constant String := To_String (Str_Id);
+ From_Idx : Integer;
+
+ begin
+ Append (Global_Name_Buffer, ASCII.LF);
+ Append (Global_Name_Buffer, " or ");
+
+ From_Idx := Name_Len;
+ Append (Global_Name_Buffer, Str_Id);
+
+ if Str (1 .. 19) = "failed precondition" then
+ Insert_Str_In_Name_Buffer ("inherited ", From_Idx + 8);
+ end if;
+ end;
+ end if;
+ end Append_Message;
+
+ -- Local variables
+
+ Str_Loc : constant String := Build_Location_String (Loc);
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Subp_Id);
+ Is_First : Boolean := True;
+
+ -- Start of processing for Build_Error_Message
+
+ begin
+ Name_Len := 0;
+ Append_Message (Subp_Id, Is_First);
+
+ for Index in Subps'Range loop
+ Append_Message (Subps (Index), Is_First);
+ end loop;
+
+ if Present (Controlling_Argument (Call_Node)) then
+ Append (Global_Name_Buffer, " in dispatching call at ");
+ else
+ Append (Global_Name_Buffer, " in call at ");
+ end if;
+
+ Append (Global_Name_Buffer, Str_Loc);
+
+ return Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
+ end Build_Error_Message;
+
+ ------------------------------------
+ -- Build_Static_Check_Helper_Call --
+ ------------------------------------
+
+ function Build_Static_Check_Helper_Call return Node_Id is
+ Actuals : constant List_Id := New_List;
+ A : Node_Id;
+ Helper_Id : Entity_Id;
+ F : Entity_Id;
+ CW_Subp : Entity_Id;
+ Spec_Id : constant Entity_Id := Entity (Name (Call_Node));
+
+ begin
+ -- The target is the wrapper built to support inheriting body but
+ -- overriding pre/postconditions (AI12-0195).
+
+ if Is_Dispatch_Table_Wrapper (Spec_Id) then
+ CW_Subp := Spec_Id;
+
+ -- Common case
+
+ else
+ CW_Subp := Class_Preconditions_Subprogram (Spec_Id,
+ Dynamic => False);
+ end if;
+
+ Helper_Id := Static_Call_Helper (CW_Subp);
+
+ F := First_Formal (Helper_Id);
+ A := First_Actual (Call_Node);
+ while Present (A) loop
+
+ -- Ensure that the evaluation of the actuals will not produce
+ -- side effects.
+
+ Remove_Side_Effects (A);
+
+ if Is_Controlling_Actual (A)
+ and then Etype (F) /= Etype (A)
+ then
+ Append_To (Actuals,
+ Make_Unchecked_Type_Conversion (Loc,
+ New_Occurrence_Of (Etype (F), Loc),
+ New_Copy_Tree (A)));
+ else
+ Append_To (Actuals, New_Copy_Tree (A));
+ end if;
+
+ Next_Formal (F);
+ Next_Actual (A);
+ end loop;
+
+ return
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Helper_Id, Loc),
+ Parameter_Associations => Actuals);
+ end Build_Static_Check_Helper_Call;
+
+ ------------------------------------
+ -- Class_Preconditions_Subprogram --
+ ------------------------------------
+
+ function Class_Preconditions_Subprogram
+ (Spec_Id : Entity_Id;
+ Dynamic : Boolean) return Node_Id
+ is
+ Subp_Id : constant Entity_Id := Ultimate_Alias (Spec_Id);
+
+ begin
+ -- Prevent cascaded errors
+
+ if not Is_Dispatching_Operation (Subp_Id) then
+ return Empty;
+
+ -- No need to search if this subprogram has the helper we are
+ -- searching
+
+ elsif Dynamic then
+ if Present (Dynamic_Call_Helper (Subp_Id)) then
+ return Subp_Id;
+ end if;
+ else
+ if Present (Static_Call_Helper (Subp_Id)) then
+ return Subp_Id;
+ end if;
+ end if;
+
+ -- Process inherited subprograms looking for class-wide
+ -- preconditions.
+
+ declare
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Subp_Id);
+ Subp_Id : Entity_Id;
+
+ begin
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Ultimate_Alias (Subp_Id);
+ end if;
+
+ -- Wrappers of class-wide pre/postconditions reference the
+ -- parent primitive that has the inherited contract.
+
+ if Is_Wrapper (Subp_Id)
+ and then Present (LSP_Subprogram (Subp_Id))
+ then
+ Subp_Id := LSP_Subprogram (Subp_Id);
+ end if;
+
+ if Dynamic then
+ if Present (Dynamic_Call_Helper (Subp_Id)) then
+ return Subp_Id;
+ end if;
+ else
+ if Present (Static_Call_Helper (Subp_Id)) then
+ return Subp_Id;
+ end if;
+ end if;
+ end loop;
+ end;
+
+ return Empty;
+ end Class_Preconditions_Subprogram;
+
+ -- Local variables
+
+ Dynamic_Check : constant Boolean :=
+ Present (Controlling_Argument (Call_Node));
+ Class_Subp : Entity_Id;
+ Cond : Node_Id;
+ Subp : Entity_Id;
+
+ -- Start of processing for Install_Class_Preconditions_Check
+
+ begin
+ -- Do not expand the check if we are compiling under restriction
+ -- No_Dispatching_Calls; the semantic analyzer has previously
+ -- notified the violation of this restriction.
+
+ if Dynamic_Check
+ and then Restriction_Active (No_Dispatching_Calls)
+ then
+ return;
+
+ -- Class-wide precondition check not needed in interface thunks since
+ -- they are installed in the dispatching call that caused invoking the
+ -- thunk.
+
+ elsif Is_Thunk (Current_Scope) then
+ return;
+ end if;
+
+ Subp := Entity (Name (Call_Node));
+
+ -- No check needed for this subprogram call if no class-wide
+ -- preconditions apply (or if the unique available preconditions
+ -- are ignored preconditions).
+
+ Class_Subp := Class_Preconditions_Subprogram (Subp, Dynamic_Check);
+
+ if No (Class_Subp)
+ or else No (Class_Preconditions (Class_Subp))
+ then
+ return;
+ end if;
+
+ -- Build and install the check
+
+ if Dynamic_Check then
+ Cond := Build_Dynamic_Check_Helper_Call;
+ else
+ Cond := Build_Static_Check_Helper_Call;
+ end if;
+
+ if Exception_Locations_Suppressed then
+ Insert_Action (Call_Node,
+ Make_If_Statement (Loc,
+ Condition => Make_Op_Not (Loc, Cond),
+ Then_Statements => New_List (
+ Make_Raise_Statement (Loc,
+ Name =>
+ New_Occurrence_Of
+ (RTE (RE_Assert_Failure), Loc)))));
+
+ -- Failed check with message indicating the failed precondition and the
+ -- call that caused it.
+
+ else
+ Insert_Action (Call_Node,
+ Make_If_Statement (Loc,
+ Condition => Make_Op_Not (Loc, Cond),
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of
+ (RTE (RE_Raise_Assert_Failure), Loc),
+ Parameter_Associations =>
+ New_List (Build_Error_Message (Subp))))));
+ end if;
+ end Install_Class_Preconditions_Check;
+
-----------------------------------
-- Is_Build_In_Place_Result_Type --
-----------------------------------
diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads
index 76cec4d4e47..196f7e6d941 100644
--- a/gcc/ada/exp_ch6.ads
+++ b/gcc/ada/exp_ch6.ads
@@ -121,6 +121,9 @@ package Exp_Ch6 is
-- The returned node is the root of the procedure body which will replace
-- the original function body, which is not needed for the C program.
+ procedure Install_Class_Preconditions_Check (Call_Node : Node_Id);
+ -- Install check of class-wide preconditions on the caller.
+
function Is_Build_In_Place_Entity (E : Entity_Id) return Boolean;
-- Ada 2005 (AI-318-02): Returns True if E is a BIP entity.
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 7cce41b234e..72f4e7c90b7 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -63,7 +63,6 @@ with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
-with Sinput; use Sinput;
with Snames; use Snames;
with Stand; use Stand;
with Stringt; use Stringt;
@@ -697,233 +696,11 @@ package body Exp_Disp is
Eq_Prim_Op : Entity_Id := Empty;
Controlling_Tag : Node_Id;
- procedure Build_Class_Wide_Check (E : Entity_Id);
- -- If the denoted subprogram has a class-wide precondition, generate a
- -- check using that precondition before the dispatching call, because
- -- this is the only class-wide precondition that applies to the call;
- -- otherwise climb to the ancestors searching for the enclosing
- -- overridden primitive of E that has a class-wide precondition (and
- -- use it to generate the check).
-
function New_Value (From : Node_Id) return Node_Id;
-- From is the original Expression. New_Value is equivalent to a call
-- to Duplicate_Subexpr with an explicit dereference when From is an
-- access parameter.
- ----------------------------
- -- Build_Class_Wide_Check --
- ----------------------------
-
- procedure Build_Class_Wide_Check (E : Entity_Id) is
- Subp : Entity_Id := E;
-
- function Has_Class_Wide_Precondition
- (Subp : Entity_Id) return Boolean;
- -- Evaluates if the dispatching subprogram Subp has a class-wide
- -- precondition.
-
- function Replace_Formals (N : Node_Id) return Traverse_Result;
- -- Replace occurrences of the formals of the subprogram by the
- -- corresponding actuals in the call, given that this check is
- -- performed outside of the body of the subprogram.
-
- -- If the dispatching call appears in the same scope as the
- -- declaration of the dispatching subprogram (for example in
- -- the expression of a local expression function), the spec
- -- has not been analyzed yet, in which case we use the Chars
- -- field to recognize intended occurrences of the formals.
-
- ---------------------------------
- -- Has_Class_Wide_Precondition --
- ---------------------------------
-
- function Has_Class_Wide_Precondition
- (Subp : Entity_Id) return Boolean
- is
- Prec : Node_Id := Empty;
-
- begin
- if Present (Contract (Subp))
- and then Present (Pre_Post_Conditions (Contract (Subp)))
- then
- Prec := Pre_Post_Conditions (Contract (Subp));
-
- while Present (Prec) loop
- exit when Pragma_Name (Prec) = Name_Precondition
- and then Class_Present (Prec);
- Prec := Next_Pragma (Prec);
- end loop;
- end if;
-
- return Present (Prec)
- and then not Is_Ignored (Prec);
- end Has_Class_Wide_Precondition;
-
- ---------------------
- -- Replace_Formals --
- ---------------------
-
- function Replace_Formals (N : Node_Id) return Traverse_Result is
- A : Node_Id;
- F : Entity_Id;
- begin
- if Is_Entity_Name (N) then
- F := First_Formal (Subp);
- A := First_Actual (Call_Node);
-
- if Present (Entity (N)) and then Is_Formal (Entity (N)) then
- while Present (F) loop
- if F = Entity (N) then
- if not Is_Controlling_Actual (N) then
- Rewrite (N, New_Copy_Tree (A));
-
- -- If the formal is class-wide, and thus not a
- -- controlling argument, preserve its type because
- -- it may appear in a nested call with a class-wide
- -- parameter.
-
- if Is_Class_Wide_Type (Etype (F)) then
- Set_Etype (N, Etype (F));
-
- -- Conversely, if this is a controlling argument
- -- (in a dispatching call in the condition) that
- -- is a dereference, the source is an access-to-
- -- -class-wide type, so preserve the dispatching
- -- nature of the call in the rewritten condition.
-
- elsif Nkind (Parent (N)) = N_Explicit_Dereference
- and then Is_Controlling_Actual (Parent (N))
- then
- Set_Controlling_Argument (Parent (Parent (N)),
- Parent (N));
- end if;
-
- -- Ensure that the type of the controlling actual
- -- matches the type of the controlling formal of the
- -- parent primitive Subp defining the class-wide
- -- precondition.
-
- elsif Is_Class_Wide_Type (Etype (A)) then
- Rewrite (N,
- Convert_To
- (Class_Wide_Type (Etype (F)),
- New_Copy_Tree (A)));
-
- else
- Rewrite (N,
- Convert_To
- (Etype (F),
- New_Copy_Tree (A)));
- end if;
-
- exit;
- end if;
-
- Next_Formal (F);
- Next_Actual (A);
- end loop;
-
- -- If the node is not analyzed, recognize occurrences of a
- -- formal by name, as would be done when resolving the aspect
- -- expression in the context of the subprogram.
-
- elsif not Analyzed (N)
- and then Nkind (N) = N_Identifier
- and then No (Entity (N))
- then
- while Present (F) loop
- if Chars (N) = Chars (F) then
- Rewrite (N, New_Copy_Tree (A));
- return Skip;
- end if;
-
- Next_Formal (F);
- Next_Actual (A);
- end loop;
- end if;
- end if;
-
- return OK;
- end Replace_Formals;
-
- procedure Update is new Traverse_Proc (Replace_Formals);
-
- -- Local variables
-
- Str_Loc : constant String := Build_Location_String (Loc);
-
- A : Node_Id;
- Cond : Node_Id;
- Msg : Node_Id;
- Prec : Node_Id;
-
- -- Start of processing for Build_Class_Wide_Check
-
- begin
- -- Climb searching for the enclosing class-wide precondition
-
- while not Has_Class_Wide_Precondition (Subp)
- and then Present (Overridden_Operation (Subp))
- loop
- Subp := Overridden_Operation (Subp);
- end loop;
-
- -- Locate class-wide precondition, if any
-
- if Present (Contract (Subp))
- and then Present (Pre_Post_Conditions (Contract (Subp)))
- then
- Prec := Pre_Post_Conditions (Contract (Subp));
-
- while Present (Prec) loop
- exit when Pragma_Name (Prec) = Name_Precondition
- and then Class_Present (Prec);
- Prec := Next_Pragma (Prec);
- end loop;
-
- if No (Prec) or else Is_Ignored (Prec) then
- return;
- end if;
-
- -- Ensure that the evaluation of the actuals will not produce side
- -- effects (since the check will use a copy of the actuals).
-
- A := First_Actual (Call_Node);
- while Present (A) loop
- Remove_Side_Effects (A);
- Next_Actual (A);
- end loop;
-
- -- The expression for the precondition is analyzed within the
- -- generated pragma. The message text is the last parameter of
- -- the generated pragma, indicating source of precondition.
-
- Cond :=
- New_Copy_Tree
- (Expression (First (Pragma_Argument_Associations (Prec))));
- Update (Cond);
-
- -- Build message indicating the failed precondition and the
- -- dispatching call that caused it.
-
- Msg := Expression (Last (Pragma_Argument_Associations (Prec)));
- Name_Len := 0;
- Append (Global_Name_Buffer, Strval (Msg));
- Append (Global_Name_Buffer, " in dispatching call at ");
- Append (Global_Name_Buffer, Str_Loc);
- Msg := Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len));
-
- Insert_Action (Call_Node,
- Make_If_Statement (Loc,
- Condition => Make_Op_Not (Loc, Cond),
- Then_Statements => New_List (
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
- Parameter_Associations => New_List (Msg)))));
- end if;
- end Build_Class_Wide_Check;
-
---------------
-- New_Value --
---------------
@@ -984,8 +761,6 @@ package body Exp_Disp is
Subp := Alias (Subp);
end if;
- Build_Class_Wide_Check (Subp);
-
-- Definition of the class-wide type and the tagged type
-- If the controlling argument is itself a tag rather than a tagged
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 807afb2c580..7c366663dcb 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1270,11 +1270,10 @@ package body Exp_Util is
---------------------------------
procedure Build_Class_Wide_Expression
- (Prag : Node_Id;
- Subp : Entity_Id;
- Par_Subp : Entity_Id;
- Adjust_Sloc : Boolean;
- Needs_Wrapper : out Boolean)
+ (Pragma_Or_Expr : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id;
+ Adjust_Sloc : Boolean)
is
function Replace_Entity (N : Node_Id) return Traverse_Result;
-- Replace reference to formal of inherited operation or to primitive
@@ -1319,84 +1318,6 @@ package body Exp_Util is
if Present (New_E) then
Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
-
- -- AI12-0166: a precondition for a protected operation
- -- cannot include an internal call to a protected function
- -- of the type. In the case of an inherited condition for an
- -- overriding operation, both the operation and the function
- -- are given by primitive wrappers.
- -- Move this check to sem???
-
- if Ekind (New_E) = E_Function
- and then Is_Primitive_Wrapper (New_E)
- and then Is_Primitive_Wrapper (Subp)
- and then Scope (Subp) = Scope (New_E)
- and then Chars (Pragma_Identifier (Prag)) = Name_Precondition
- then
- Error_Msg_Node_2 := Wrapped_Entity (Subp);
- Error_Msg_NE
- ("internal call to& cannot appear in inherited "
- & "precondition of protected operation&",
- N, Wrapped_Entity (New_E));
- end if;
-
- -- If the entity is an overridden primitive and we are not
- -- in GNATprove mode, we must build a wrapper for the current
- -- inherited operation. If the reference is the prefix of an
- -- attribute such as 'Result (or others ???) there is no need
- -- for a wrapper: the condition is just rewritten in terms of
- -- the inherited subprogram.
-
- if Is_Subprogram (New_E)
- and then Nkind (Parent (N)) /= N_Attribute_Reference
- and then not GNATprove_Mode
- then
- Needs_Wrapper := True;
- end if;
- end if;
-
- -- Check that there are no calls left to abstract operations if
- -- the current subprogram is not abstract.
- -- Move this check to sem???
-
- if Nkind (Parent (N)) = N_Function_Call
- and then N = Name (Parent (N))
- then
- if not Is_Abstract_Subprogram (Subp)
- and then Is_Abstract_Subprogram (Entity (N))
- then
- Error_Msg_Sloc := Sloc (Current_Scope);
- Error_Msg_Node_2 := Subp;
- if Comes_From_Source (Subp) then
- Error_Msg_NE
- ("cannot call abstract subprogram & in inherited "
- & "condition for&#", Subp, Entity (N));
- else
- Error_Msg_NE
- ("cannot call abstract subprogram & in inherited "
- & "condition for inherited&#", Subp, Entity (N));
- end if;
-
- -- In SPARK mode, reject an inherited condition for an
- -- inherited operation if it contains a call to an overriding
- -- operation, because this implies that the pre/postconditions
- -- of the inherited operation have changed silently.
-
- elsif SPARK_Mode = On
- and then Warn_On_Suspicious_Contract
- and then Present (Alias (Subp))
- and then Present (New_E)
- and then Comes_From_Source (New_E)
- then
- Error_Msg_N
- ("cannot modify inherited condition (SPARK RM 6.1.1(1))",
- Parent (Subp));
- Error_Msg_Sloc := Sloc (New_E);
- Error_Msg_Node_2 := Subp;
- Error_Msg_NE
- ("\overriding of&# forces overriding of&",
- Parent (Subp), New_E);
- end if;
end if;
-- Update type of function call node, which should be the same as
@@ -1422,26 +1343,17 @@ package body Exp_Util is
-- Local variables
- Par_Formal : Entity_Id;
- Subp_Formal : Entity_Id;
+ Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Subp);
+ Subp_Typ : constant Entity_Id := Find_Dispatching_Type (Subp);
-- Start of processing for Build_Class_Wide_Expression
begin
- Needs_Wrapper := False;
-
- -- Add mapping from old formals to new formals
+ pragma Assert (Par_Typ /= Subp_Typ);
- Par_Formal := First_Formal (Par_Subp);
- Subp_Formal := First_Formal (Subp);
-
- while Present (Par_Formal) and then Present (Subp_Formal) loop
- Type_Map.Set (Par_Formal, Subp_Formal);
- Next_Formal (Par_Formal);
- Next_Formal (Subp_Formal);
- end loop;
-
- Replace_Condition_Entities (Prag);
+ Update_Primitives_Mapping (Par_Subp, Subp);
+ Map_Formals (Par_Subp, Subp);
+ Replace_Condition_Entities (Pragma_Or_Expr);
end Build_Class_Wide_Expression;
--------------------
@@ -1895,7 +1807,33 @@ package body Exp_Util is
Priv_Typ : Entity_Id;
-- The partial view of Par_Typ
+ Op_Node : Elmt_Id;
+ Par_Prim : Entity_Id;
+ Prim : Entity_Id;
+
begin
+ -- Map the overridden primitive to the overriding one; required by
+ -- Replace_References (called by Add_Inherited_DICs) to handle calls
+ -- to parent primitives.
+
+ Op_Node := First_Elmt (Primitive_Operations (T));
+ while Present (Op_Node) loop
+ Prim := Node (Op_Node);
+
+ if Present (Overridden_Operation (Prim))
+ and then Comes_From_Source (Prim)
+ then
+ Par_Prim := Overridden_Operation (Prim);
+
+ -- Create a mapping of the form:
+ -- parent type primitive -> derived type primitive
+
+ Type_Map.Set (Par_Prim, Prim);
+ end if;
+
+ Next_Elmt (Op_Node);
+ end loop;
+
-- Climb the parent type chain
Curr_Typ := T;
@@ -7073,6 +7011,15 @@ package body Exp_Util is
return Etype (Indx);
end Get_Index_Subtype;
+ -----------------------
+ -- Get_Mapped_Entity --
+ -----------------------
+
+ function Get_Mapped_Entity (E : Entity_Id) return Entity_Id is
+ begin
+ return Type_Map.Get (E);
+ end Get_Mapped_Entity;
+
---------------------
-- Get_Stream_Size --
---------------------
@@ -10350,6 +10297,36 @@ package body Exp_Util is
end if;
end Make_Variant_Comparison;
+ -----------------
+ -- Map_Formals --
+ -----------------
+
+ procedure Map_Formals
+ (Parent_Subp : Entity_Id;
+ Derived_Subp : Entity_Id;
+ Force_Update : Boolean := False)
+ is
+ Par_Formal : Entity_Id := First_Formal (Parent_Subp);
+ Subp_Formal : Entity_Id := First_Formal (Derived_Subp);
+
+ begin
+ if Force_Update then
+ Type_Map.Set (Parent_Subp, Derived_Subp);
+ end if;
+
+ -- At this stage either we are under regular processing and the caller
+ -- has previously ensured that these primitives are already mapped (by
+ -- means of calling previously to Update_Primitives_Mapping), or we are
+ -- processing a late-overriding primitive and Force_Update updated above
+ -- the mapping of these primitives.
+
+ while Present (Par_Formal) and then Present (Subp_Formal) loop
+ Type_Map.Set (Par_Formal, Subp_Formal);
+ Next_Formal (Par_Formal);
+ Next_Formal (Subp_Formal);
+ end loop;
+ end Map_Formals;
+
---------------
-- Map_Types --
---------------
@@ -10861,7 +10838,7 @@ package body Exp_Util is
-- they relate to the primitives of the parent type. If there is a
-- meaningful relation, create a mapping of the form:
- -- parent type primitive -> perived type primitive
+ -- parent type primitive -> derived type primitive
if Present (Direct_Primitive_Operations (Deriv_Typ)) then
Prim_Elmt := First_Elmt (Direct_Primitive_Operations (Deriv_Typ));
@@ -14123,10 +14100,12 @@ package body Exp_Util is
(Inher_Id : Entity_Id;
Subp_Id : Entity_Id)
is
+ Parent_Type : constant Entity_Id := Find_Dispatching_Type (Inher_Id);
+ Derived_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
+
begin
- Map_Types
- (Parent_Type => Find_Dispatching_Type (Inher_Id),
- Derived_Type => Find_Dispatching_Type (Subp_Id));
+ pragma Assert (Parent_Type /= Derived_Type);
+ Map_Types (Parent_Type, Derived_Type);
end Update_Primitives_Mapping;
----------------------------------
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 56ff61f489b..eddf314c932 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -270,28 +270,16 @@ package Exp_Util is
-- not install a call to Abort_Defer.
procedure Build_Class_Wide_Expression
- (Prag : Node_Id;
- Subp : Entity_Id;
- Par_Subp : Entity_Id;
- Adjust_Sloc : Boolean;
- Needs_Wrapper : out Boolean);
- -- Build the expression for an inherited class-wide condition. Prag is
- -- the pragma constructed from the corresponding aspect of the parent
- -- subprogram, and Subp is the overriding operation, and Par_Subp is
- -- the overridden operation that has the condition. Adjust_Sloc is True
- -- when the sloc of nodes traversed should be adjusted for the inherited
- -- pragma. The routine is also called to check whether an inherited
- -- operation that is not overridden but has inherited conditions needs
- -- a wrapper, because the inherited condition includes calls to other
- -- primitives that have been overridden. In that case the first argument
- -- is the expression of the original class-wide aspect. In SPARK_Mode, such
- -- operation which are just inherited but have modified pre/postconditions
- -- are illegal.
- -- If there are calls to overridden operations in the condition, and the
- -- pragma applies to an inherited operation, a wrapper must be built for
- -- it to capture the new inherited condition. The flag Needs_Wrapper is
- -- set in that case so that the wrapper can be built, when the controlling
- -- type is frozen.
+ (Pragma_Or_Expr : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id;
+ Adjust_Sloc : Boolean);
+ -- Build the expression for an inherited class-wide condition. Pragma_Or_
+ -- _Expr is either the pragma constructed from the corresponding aspect of
+ -- the parent subprogram or the class-wide pre/postcondition built from the
+ -- parent, Subp is the overriding operation, and Par_Subp is the overridden
+ -- operation that has the condition. Adjust_Sloc is True when the sloc of
+ -- nodes traversed should be adjusted for the inherited pragma.
function Build_DIC_Call
(Loc : Source_Ptr;
@@ -612,7 +600,7 @@ package Exp_Util is
function Find_Prim_Op (T : Entity_Id; Name : Name_Id) return Entity_Id;
-- Find the first primitive operation of a tagged type T with name Name.
-- This function allows the use of a primitive operation which is not
- -- directly visible. If T is a class wide type, then the reference is to an
+ -- directly visible. If T is a class-wide type, then the reference is to an
-- operation of the corresponding root type. It is an error if no primitive
-- operation with the given name is found.
@@ -739,6 +727,10 @@ package Exp_Util is
-- Used for First, Last, and Length, when the prefix is an array type.
-- Obtains the corresponding index subtype.
+ function Get_Mapped_Entity (E : Entity_Id) return Entity_Id;
+ -- Return the mapped entity of E; used to check inherited class-wide
+ -- pre/postconditions.
+
function Get_Stream_Size (E : Entity_Id) return Uint;
-- Return the stream size value of the subtype E
@@ -918,6 +910,15 @@ package Exp_Util is
-- Subprogram_Variant. Generate a comparison between Curr_Val and Old_Val
-- depending on the variant mode (Increases / Decreases).
+ procedure Map_Formals
+ (Parent_Subp : Entity_Id;
+ Derived_Subp : Entity_Id;
+ Force_Update : Boolean := False);
+ -- Establish the mapping from the formals of Parent_Subp to the formals
+ -- of Derived_Subp; if Force_Update is True then mapping of Parent_Subp to
+ -- Derived_Subp is also updated; used to update mapping of late-overriding
+ -- primitives of a tagged type.
+
procedure Map_Types (Parent_Type : Entity_Id; Derived_Type : Entity_Id);
-- Establish the following mapping between the attributes of tagged parent
-- type Parent_Type and tagged derived type Derived_Type.
@@ -1205,5 +1206,6 @@ package Exp_Util is
private
pragma Inline (Duplicate_Subexpr);
pragma Inline (Force_Evaluation);
+ pragma Inline (Get_Mapped_Entity);
pragma Inline (Is_Library_Level_Tagged_Type);
end Exp_Util;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 5b7607d051d..5f81d9efbda 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -35,6 +35,7 @@ with Elists; use Elists;
with Errout; use Errout;
with Exp_Ch3; use Exp_Ch3;
with Exp_Ch7; use Exp_Ch7;
+with Exp_Disp; use Exp_Disp;
with Exp_Pakd; use Exp_Pakd;
with Exp_Util; use Exp_Util;
with Exp_Tss; use Exp_Tss;
@@ -56,6 +57,7 @@ with Sem_Ch6; use Sem_Ch6;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch13; use Sem_Ch13;
+with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Mech; use Sem_Mech;
with Sem_Prag; use Sem_Prag;
@@ -132,11 +134,6 @@ package body Freeze is
-- Attribute references to outer types are freeze points for those types;
-- this routine generates the required freeze nodes for them.
- procedure Check_Inherited_Conditions (R : Entity_Id);
- -- For a tagged derived type, create wrappers for inherited operations
- -- that have a class-wide condition, so it can be properly rewritten if
- -- it involves calls to other overriding primitives.
-
procedure Check_Strict_Alignment (E : Entity_Id);
-- E is a base type. If E is tagged or has a component that is aliased
-- or tagged or contains something this is aliased or tagged, set
@@ -160,7 +157,7 @@ package body Freeze is
procedure Freeze_Enumeration_Type (Typ : Entity_Id);
-- Freeze enumeration type. The Esize field is set as processing
-- proceeds (i.e. set by default when the type is declared and then
- -- adjusted by rep clauses. What this procedure does is to make sure
+ -- adjusted by rep clauses). What this procedure does is to make sure
-- that if a foreign convention is specified, and no specific size
-- is given, then the size must be at least Integer'Size.
@@ -1483,90 +1480,322 @@ package body Freeze is
-- Check_Inherited_Conditions --
--------------------------------
- procedure Check_Inherited_Conditions (R : Entity_Id) is
- Prim_Ops : constant Elist_Id := Primitive_Operations (R);
- Decls : List_Id;
- Needs_Wrapper : Boolean;
- Op_Node : Elmt_Id;
- Par_Prim : Entity_Id;
- Prim : Entity_Id;
-
- procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id);
+ procedure Check_Inherited_Conditions
+ (R : Entity_Id;
+ Late_Overriding : Boolean := False)
+ is
+ Prim_Ops : constant Elist_Id := Primitive_Operations (R);
+ Decls : List_Id;
+ Op_Node : Elmt_Id;
+ Par_Prim : Entity_Id;
+ Prim : Entity_Id;
+ Wrapper_Needed : Boolean;
+
+ function Build_DTW_Body
+ (Loc : Source_Ptr;
+ DTW_Spec : Node_Id;
+ DTW_Decls : List_Id;
+ Par_Prim : Entity_Id;
+ Wrapped_Subp : Entity_Id) return Node_Id;
+ -- Build the body of the dispatch table wrapper containing the given
+ -- spec and declarations; the call to the wrapped subprogram includes
+ -- the proper type conversion.
+
+ function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id;
+ -- Build the spec of the dispatch table wrapper
+
+ procedure Build_Inherited_Condition_Pragmas
+ (Subp : Entity_Id;
+ Wrapper_Needed : out Boolean);
-- Build corresponding pragmas for an operation whose ancestor has
- -- class-wide pre/postconditions. If the operation is inherited, the
- -- pragmas force the creation of a wrapper for the inherited operation.
- -- If the ancestor is being overridden, the pragmas are constructed only
- -- to verify their legality, in case they contain calls to other
- -- primitives that may have been overridden.
+ -- class-wide pre/postconditions. If the operation is inherited then
+ -- Wrapper_Needed is returned True to force the creation of a wrapper
+ -- for the inherited operation. If the ancestor is being overridden,
+ -- the pragmas are constructed only to verify their legality, in case
+ -- they contain calls to other primitives that may have been overridden.
+
+ function Needs_Wrapper
+ (Class_Cond : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id) return Boolean;
+ -- Checks whether the dispatch-table wrapper (DTW) for Subp must be
+ -- built to evaluate the given class-wide condition.
+
+ --------------------
+ -- Build_DTW_Body --
+ --------------------
+
+ function Build_DTW_Body
+ (Loc : Source_Ptr;
+ DTW_Spec : Node_Id;
+ DTW_Decls : List_Id;
+ Par_Prim : Entity_Id;
+ Wrapped_Subp : Entity_Id) return Node_Id
+ is
+ Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Prim);
+ Actuals : constant List_Id := Empty_List;
+ Call : Node_Id;
+ Formal : Entity_Id := First_Formal (Par_Prim);
+ New_F_Spec : Entity_Id := First (Parameter_Specifications (DTW_Spec));
+ New_Formal : Entity_Id;
+
+ begin
+ -- Build parameter association for call to wrapped subprogram
+
+ while Present (Formal) loop
+ New_Formal := Defining_Identifier (New_F_Spec);
+
+ -- If the controlling argument is inherited, add conversion to
+ -- parent type for the call.
+
+ if Etype (Formal) = Par_Typ
+ and then Is_Controlling_Formal (Formal)
+ then
+ Append_To (Actuals,
+ Make_Type_Conversion (Loc,
+ New_Occurrence_Of (Par_Typ, Loc),
+ New_Occurrence_Of (New_Formal, Loc)));
+ else
+ Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
+ end if;
+
+ Next_Formal (Formal);
+ Next (New_F_Spec);
+ end loop;
+
+ if Ekind (Wrapped_Subp) = E_Procedure then
+ Call :=
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Wrapped_Subp, Loc),
+ Parameter_Associations => Actuals);
+ else
+ Call :=
+ Make_Simple_Return_Statement (Loc,
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Wrapped_Subp, Loc),
+ Parameter_Associations => Actuals));
+ end if;
+
+ return
+ Make_Subprogram_Body (Loc,
+ Specification => Copy_Subprogram_Spec (DTW_Spec),
+ Declarations => DTW_Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call),
+ End_Label => Make_Identifier (Loc,
+ Chars (Defining_Entity (DTW_Spec)))));
+ end Build_DTW_Body;
+
+ --------------------
+ -- Build_DTW_Spec --
+ --------------------
+
+ function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id is
+ DTW_Id : Entity_Id;
+ DTW_Spec : Node_Id;
+
+ begin
+ DTW_Spec := Build_Overriding_Spec (Par_Prim, R);
+ DTW_Id := Defining_Entity (DTW_Spec);
+
+ -- Add minimal decoration of fields
+
+ Mutate_Ekind (DTW_Id, Ekind (Par_Prim));
+ Set_LSP_Subprogram (DTW_Id, Par_Prim);
+ Set_Is_Dispatch_Table_Wrapper (DTW_Id);
+ Set_Is_Wrapper (DTW_Id);
+
+ -- The DTW wrapper is never a null procedure
+
+ if Nkind (DTW_Spec) = N_Procedure_Specification then
+ Set_Null_Present (DTW_Spec, False);
+ end if;
+
+ return DTW_Spec;
+ end Build_DTW_Spec;
---------------------------------------
-- Build_Inherited_Condition_Pragmas --
---------------------------------------
- procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is
- A_Post : Node_Id;
- A_Pre : Node_Id;
- New_Prag : Node_Id;
+ procedure Build_Inherited_Condition_Pragmas
+ (Subp : Entity_Id;
+ Wrapper_Needed : out Boolean)
+ is
+ Class_Pre : constant Node_Id :=
+ Class_Preconditions (Ultimate_Alias (Subp));
+ Class_Post : Node_Id := Class_Postconditions (Par_Prim);
+ A_Post : Node_Id;
+ New_Prag : Node_Id;
begin
- A_Pre := Get_Class_Wide_Pragma (Par_Prim, Pragma_Precondition);
+ Wrapper_Needed := False;
- if Present (A_Pre) then
- New_Prag := New_Copy_Tree (A_Pre);
- Build_Class_Wide_Expression
- (Prag => New_Prag,
- Subp => Prim,
- Par_Subp => Par_Prim,
- Adjust_Sloc => False,
- Needs_Wrapper => Needs_Wrapper);
-
- if Needs_Wrapper
- and then not Comes_From_Source (Subp)
- and then Expander_Active
- then
- Append (New_Prag, Decls);
- end if;
+ if No (Class_Pre) and then No (Class_Post) then
+ return;
end if;
- A_Post := Get_Class_Wide_Pragma (Par_Prim, Pragma_Postcondition);
+ -- For class-wide preconditions we just evaluate whether the wrapper
+ -- is needed; there is no need to build the pragma since the check
+ -- is performed on the caller side.
- if Present (A_Post) then
- New_Prag := New_Copy_Tree (A_Post);
+ if Present (Class_Pre)
+ and then Needs_Wrapper (Class_Pre, Subp, Par_Prim)
+ then
+ Wrapper_Needed := True;
+ end if;
+
+ -- For class-wide postconditions we evaluate whether the wrapper is
+ -- needed and we build the class-wide postcondition pragma to install
+ -- it in the wrapper.
+
+ if Present (Class_Post)
+ and then Needs_Wrapper (Class_Post, Subp, Par_Prim)
+ then
+ Wrapper_Needed := True;
+
+ -- Update the class-wide postcondition
+
+ Class_Post := New_Copy_Tree (Class_Post);
Build_Class_Wide_Expression
- (Prag => New_Prag,
- Subp => Prim,
+ (Pragma_Or_Expr => Class_Post,
+ Subp => Subp,
Par_Subp => Par_Prim,
- Adjust_Sloc => False,
- Needs_Wrapper => Needs_Wrapper);
+ Adjust_Sloc => False);
- if Needs_Wrapper
- and then not Comes_From_Source (Subp)
- and then Expander_Active
- then
- Append (New_Prag, Decls);
+ -- Install the updated class-wide postcondition in a copy of the
+ -- pragma postcondition defined for the nearest ancestor.
+
+ A_Post := Get_Class_Wide_Pragma (Par_Prim,
+ Pragma_Postcondition);
+
+ if No (A_Post) then
+ declare
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Subp);
+ begin
+ for Index in Subps'Range loop
+ A_Post := Get_Class_Wide_Pragma (Subps (Index),
+ Pragma_Postcondition);
+ exit when Present (A_Post);
+ end loop;
+ end;
end if;
+
+ New_Prag := New_Copy_Tree (A_Post);
+ Rewrite
+ (Expression (First (Pragma_Argument_Associations (New_Prag))),
+ Class_Post);
+ Append (New_Prag, Decls);
end if;
end Build_Inherited_Condition_Pragmas;
+ -------------------
+ -- Needs_Wrapper --
+ -------------------
+
+ function Needs_Wrapper
+ (Class_Cond : Node_Id;
+ Subp : Entity_Id;
+ Par_Subp : Entity_Id) return Boolean
+ is
+ Result : Boolean := False;
+
+ function Check_Entity (N : Node_Id) return Traverse_Result;
+ -- Check calls to overridden primitives
+
+ --------------------
+ -- Replace_Entity --
+ --------------------
+
+ function Check_Entity (N : Node_Id) return Traverse_Result is
+ New_E : Entity_Id;
+
+ begin
+ if Nkind (N) = N_Identifier
+ and then Present (Entity (N))
+ and then
+ (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
+ and then
+ (Nkind (Parent (N)) /= N_Attribute_Reference
+ or else Attribute_Name (Parent (N)) /= Name_Class)
+ then
+ -- The check does not apply to dispatching calls within the
+ -- condition, but only to calls whose static tag is that of
+ -- the parent type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ and then Present (Controlling_Argument (Parent (N)))
+ then
+ return OK;
+ end if;
+
+ -- Determine whether entity has a renaming
+
+ New_E := Get_Mapped_Entity (Entity (N));
+
+ -- If the entity is an overridden primitive and we are not
+ -- in GNATprove mode, we must build a wrapper for the current
+ -- inherited operation. If the reference is the prefix of an
+ -- attribute such as 'Result (or others ???) there is no need
+ -- for a wrapper: the condition is just rewritten in terms of
+ -- the inherited subprogram.
+
+ if Present (New_E)
+ and then Comes_From_Source (New_E)
+ and then Is_Subprogram (New_E)
+ and then Nkind (Parent (N)) /= N_Attribute_Reference
+ and then not GNATprove_Mode
+ then
+ Result := True;
+ return Abandon;
+ end if;
+ end if;
+
+ return OK;
+ end Check_Entity;
+
+ procedure Check_Condition_Entities is
+ new Traverse_Proc (Check_Entity);
+
+ -- Start of processing for Needs_Wrapper
+
+ begin
+ Update_Primitives_Mapping (Par_Subp, Subp);
+
+ Map_Formals (Par_Subp, Subp);
+ Check_Condition_Entities (Class_Cond);
+
+ return Result;
+ end Needs_Wrapper;
+
-- Start of processing for Check_Inherited_Conditions
begin
- Op_Node := First_Elmt (Prim_Ops);
- while Present (Op_Node) loop
- Prim := Node (Op_Node);
+ if Late_Overriding then
+ Op_Node := First_Elmt (Prim_Ops);
+ while Present (Op_Node) loop
+ Prim := Node (Op_Node);
- -- Map the overridden primitive to the overriding one. This takes
- -- care of all overridings and is done only once.
+ -- Map the overridden primitive to the overriding one
- if Present (Overridden_Operation (Prim))
- and then Comes_From_Source (Prim)
- then
- Par_Prim := Overridden_Operation (Prim);
- Update_Primitives_Mapping (Par_Prim, Prim);
- end if;
+ if Present (Overridden_Operation (Prim))
+ and then Comes_From_Source (Prim)
+ then
+ Par_Prim := Overridden_Operation (Prim);
+ Update_Primitives_Mapping (Par_Prim, Prim);
- Next_Elmt (Op_Node);
- end loop;
+ -- Force discarding previous mappings of its formals
+
+ Map_Formals (Par_Prim, Prim, Force_Update => True);
+ end if;
+
+ Next_Elmt (Op_Node);
+ end loop;
+ end if;
-- Perform validity checks on the inherited conditions of overriding
-- operations, for conformance with LSP, and apply SPARK-specific
@@ -1602,12 +1831,6 @@ package body Freeze is
if GNATprove_Mode then
Collect_Inherited_Class_Wide_Conditions (Prim);
-
- -- Otherwise build the corresponding pragmas to check for legality
- -- of the inherited condition.
-
- else
- Build_Inherited_Condition_Pragmas (Prim);
end if;
end if;
@@ -1621,12 +1844,17 @@ package body Freeze is
Op_Node := First_Elmt (Prim_Ops);
while Present (Op_Node) loop
- Decls := Empty_List;
- Prim := Node (Op_Node);
- Needs_Wrapper := False;
+ Decls := Empty_List;
+ Prim := Node (Op_Node);
+ Wrapper_Needed := False;
+
+ -- Skip internal entities built for mapping interface primitives
- if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then
- Par_Prim := Alias (Prim);
+ if not Comes_From_Source (Prim)
+ and then Present (Alias (Prim))
+ and then No (Interface_Alias (Prim))
+ then
+ Par_Prim := Ultimate_Alias (Prim);
-- When the primitive is an LSP wrapper we climb to the parent
-- primitive that has the inherited contract.
@@ -1644,39 +1872,39 @@ package body Freeze is
-- in the loop above.
Analyze_Entry_Or_Subprogram_Contract (Par_Prim);
- Build_Inherited_Condition_Pragmas (Prim);
+ Build_Inherited_Condition_Pragmas (Prim, Wrapper_Needed);
end if;
- if Needs_Wrapper
+ if Wrapper_Needed
and then not Is_Abstract_Subprogram (Par_Prim)
and then Expander_Active
then
- -- We need to build a new primitive that overrides the inherited
- -- one, and whose inherited expression has been updated above.
- -- These expressions are the arguments of pragmas that are part
- -- of the declarations of the wrapper. The wrapper holds a single
- -- statement that is a call to the class-wide clone, where the
- -- controlling actuals are conversions to the corresponding type
- -- in the parent primitive:
-
- -- procedure New_Prim (F1 : T1; ...);
- -- procedure New_Prim (F1 : T1; ...) is
- -- pragma Check (Precondition, Expr);
- -- begin
- -- Par_Prim_Clone (Par_Type (F1), ...);
- -- end;
-
- -- If the primitive is a function the statement is a return
- -- statement with a call.
+ -- Build the dispatch-table wrapper (DTW). The support for
+ -- AI12-0195 relies on two kind of wrappers: one for indirect
+ -- calls (also used for AI12-0220), and one for putting in the
+ -- dispatch table:
+ --
+ -- 1) "indirect-call wrapper" (ICW) is needed anytime there are
+ -- class-wide preconditions. Prim'Access will point directly
+ -- at the ICW if any, or at the "pristine" body if Prim has
+ -- no class-wide preconditions.
+ --
+ -- 2) "dispatch-table wrapper" (DTW) is needed anytime the class
+ -- wide preconditions *or* the class-wide postconditions are
+ -- affected by overriding.
+ --
+ -- The DTW holds a single statement that is a single call where
+ -- the controlling actuals are conversions to the corresponding
+ -- type in the parent primitive. If the primitive is a function
+ -- the statement is a return statement with a call.
declare
Alias_Id : constant Entity_Id := Ultimate_Alias (Prim);
Loc : constant Source_Ptr := Sloc (R);
- Par_R : constant Node_Id := Parent (R);
- New_Body : Node_Id;
- New_Decl : Node_Id;
- New_Id : Entity_Id;
- New_Spec : Node_Id;
+ DTW_Body : Node_Id;
+ DTW_Decl : Node_Id;
+ DTW_Id : Entity_Id;
+ DTW_Spec : Node_Id;
begin
-- The wrapper must be analyzed in the scope of its wrapped
@@ -1684,47 +1912,130 @@ package body Freeze is
Push_Scope (Scope (Prim));
- New_Spec := Build_Overriding_Spec (Par_Prim, R);
- New_Id := Defining_Entity (New_Spec);
- New_Decl :=
- Make_Subprogram_Declaration (Loc,
- Specification => New_Spec);
+ DTW_Spec := Build_DTW_Spec (Par_Prim);
+ DTW_Id := Defining_Entity (DTW_Spec);
+ DTW_Decl := Make_Subprogram_Declaration (Loc,
+ Specification => DTW_Spec);
+
+ -- For inherited class-wide preconditions the DTW wrapper
+ -- reuses the ICW of the parent (which checks the parent
+ -- interpretation of the class-wide preconditions); the
+ -- interpretation of the class-wide preconditions for the
+ -- inherited subprogram is checked at the caller side.
+
+ -- When the subprogram inherits class-wide postconditions
+ -- the DTW also checks the interpretation of the class-wide
+ -- postconditions for the inherited subprogram, and the body
+ -- of the parent checks its interpretation of the parent for
+ -- the class-wide postconditions.
+
+ -- procedure Prim (F1 : T1; ...) is
+ -- [ pragma Check (Postcondition, Expr); ]
+ -- begin
+ -- Par_Prim_ICW (Par_Type (F1), ...);
+ -- end;
+
+ if Present (Indirect_Call_Wrapper (Par_Prim)) then
+ DTW_Body :=
+ Build_DTW_Body (Loc,
+ DTW_Spec => DTW_Spec,
+ DTW_Decls => Decls,
+ Par_Prim => Par_Prim,
+ Wrapped_Subp => Indirect_Call_Wrapper (Par_Prim));
+
+ -- For subprograms that only inherit class-wide postconditions
+ -- the DTW wrapper calls the parent primitive (which on its
+ -- body checks the interpretation of the class-wide post-
+ -- conditions for the parent subprogram), and the DTW checks
+ -- the interpretation of the class-wide postconditions for the
+ -- inherited subprogram.
+
+ -- procedure Prim (F1 : T1; ...) is
+ -- pragma Check (Postcondition, Expr);
+ -- begin
+ -- Par_Prim (Par_Type (F1), ...);
+ -- end;
- -- Insert the declaration and the body of the wrapper after
- -- type declaration that generates inherited operation. For
- -- a null procedure, the declaration implies a null body.
-
- -- Before insertion, do some minimal decoration of fields
+ else
+ DTW_Body :=
+ Build_DTW_Body (Loc,
+ DTW_Spec => DTW_Spec,
+ DTW_Decls => Decls,
+ Par_Prim => Par_Prim,
+ Wrapped_Subp => Par_Prim);
+ end if;
- Mutate_Ekind (New_Id, Ekind (Par_Prim));
- Set_LSP_Subprogram (New_Id, Par_Prim);
- Set_Is_Wrapper (New_Id);
+ -- Insert the declaration of the wrapper before the freezing
+ -- node of the record type declaration to ensure that it will
+ -- override the internal primitive built by Derive_Subprogram.
- if Nkind (New_Spec) = N_Procedure_Specification
- and then Null_Present (New_Spec)
- then
- Insert_After_And_Analyze (Par_R, New_Decl);
+ Ensure_Freeze_Node (R);
+ if Late_Overriding then
+ Insert_Before_And_Analyze (Freeze_Node (R), DTW_Decl);
else
- -- Build body as wrapper to a call to the already built
- -- class-wide clone.
+ Append_Freeze_Action (R, DTW_Decl);
+ end if;
+
+ Analyze (DTW_Decl);
+
+ -- Insert the body of the wrapper in the freeze actions of
+ -- its record type declaration to ensure that it is placed
+ -- in the scope of its declaration but not too early to cause
+ -- premature freezing of other entities.
+
+ Append_Freeze_Action (R, DTW_Body);
+ Analyze (DTW_Body);
+
+ -- Ensure correct decoration
+
+ pragma Assert (Is_Dispatching_Operation (DTW_Id));
+ pragma Assert (Present (Overridden_Operation (DTW_Id)));
+ pragma Assert (Overridden_Operation (DTW_Id) = Alias_Id);
- New_Body :=
- Build_Class_Wide_Clone_Call
- (Loc, Decls, Par_Prim, New_Spec);
+ -- Inherit dispatch table slot
- Insert_List_After_And_Analyze
- (Par_R, New_List (New_Decl, New_Body));
+ Set_DTC_Entity_Value (R, DTW_Id);
+ Set_DT_Position (DTW_Id, DT_Position (Alias_Id));
- -- Ensure correct decoration
+ -- Register the wrapper in the dispatch table
- pragma Assert (Present (Alias (Prim)));
- pragma Assert (Present (Overridden_Operation (New_Id)));
- pragma Assert (Overridden_Operation (New_Id) = Alias_Id);
+ if Late_Overriding
+ and then not Building_Static_DT (R)
+ then
+ Insert_List_After_And_Analyze (Freeze_Node (R),
+ Register_Primitive (Loc, DTW_Id));
end if;
- pragma Assert (Is_Dispatching_Operation (Prim));
- pragma Assert (Is_Dispatching_Operation (New_Id));
+ -- Build the helper and ICW for the DTW
+
+ if Present (Indirect_Call_Wrapper (Par_Prim)) then
+ declare
+ CW_Subp : Entity_Id;
+ Decl_N : Node_Id;
+ Body_N : Node_Id;
+
+ begin
+ Merge_Class_Conditions (DTW_Id);
+ Make_Class_Precondition_Subps (DTW_Id,
+ Late_Overriding => Late_Overriding);
+
+ CW_Subp := Static_Call_Helper (DTW_Id);
+ Decl_N := Unit_Declaration_Node (CW_Subp);
+ Analyze (Decl_N);
+
+ -- If the DTW was built for a late-overriding primitive
+ -- its body must be analyzed now (since the tagged type
+ -- is already frozen).
+
+ if Late_Overriding then
+ Body_N :=
+ Unit_Declaration_Node
+ (Corresponding_Body (Decl_N));
+ Analyze (Body_N);
+ end if;
+ end;
+ end if;
Pop_Scope;
end;
@@ -7417,7 +7728,7 @@ package body Freeze is
if Is_Type (E) then
Freeze_And_Append (First_Subtype (E), N, Result);
- -- If we just froze a tagged non-class wide record, then freeze the
+ -- If we just froze a tagged non-class-wide record, then freeze the
-- corresponding class-wide type. This must be done after the tagged
-- type itself is frozen, because the class-wide type refers to the
-- tagged type which generates the class.
diff --git a/gcc/ada/freeze.ads b/gcc/ada/freeze.ads
index 6f4fecaea72..01747562b20 100644
--- a/gcc/ada/freeze.ads
+++ b/gcc/ada/freeze.ads
@@ -174,6 +174,15 @@ package Freeze is
-- do not allow a size clause if the size would not otherwise be known at
-- compile time in any case.
+ procedure Check_Inherited_Conditions
+ (R : Entity_Id;
+ Late_Overriding : Boolean := False);
+ -- For a tagged derived type R, create wrappers for inherited operations
+ -- that have class-wide conditions, so it can be properly rewritten if
+ -- it involves calls to other overriding primitives. Late_Overriding is
+ -- True when we are processing the body of a primitive with no previous
+ -- spec defined after R is frozen (see Check_Dispatching_Operation).
+
function Is_Full_Access_Aggregate (N : Node_Id) return Boolean;
-- If a full access object is initialized with an aggregate or is assigned
-- an aggregate, we have to prevent a piecemeal access or assignment to the
diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads
index 360e2e1e0eb..24f57b4b241 100644
--- a/gcc/ada/gen_il-fields.ads
+++ b/gcc/ada/gen_il-fields.ads
@@ -461,7 +461,9 @@ package Gen_IL.Fields is
Can_Never_Be_Null,
Can_Use_Internal_Rep,
Checks_May_Be_Suppressed,
- Class_Wide_Clone,
+ Class_Postconditions,
+ Class_Preconditions,
+ Class_Preconditions_Subprogram,
Class_Wide_Type,
Cloned_Subtype,
Component_Alignment,
@@ -509,6 +511,7 @@ package Gen_IL.Fields is
Discriminant_Default_Value,
Discriminant_Number,
Dispatch_Table_Wrappers,
+ Dynamic_Call_Helper,
DT_Entry_Count,
DT_Offset_To_Top_Func,
DT_Position,
@@ -649,9 +652,12 @@ package Gen_IL.Fields is
Hiding_Loop_Variable,
Hidden_In_Formal_Instance,
Homonym,
+ Ignored_Class_Postconditions,
+ Ignored_Class_Preconditions,
Ignore_SPARK_Mode_Pragmas,
Import_Pragma,
Incomplete_Actuals,
+ Indirect_Call_Wrapper,
In_Package_Body,
In_Private_Part,
In_Use,
@@ -693,6 +699,7 @@ package Gen_IL.Fields is
Is_Discrim_SO_Function,
Is_Discriminant_Check_Function,
Is_Dispatch_Table_Entity,
+ Is_Dispatch_Table_Wrapper,
Is_Dispatching_Operation,
Is_Elaboration_Checks_OK_Id,
Is_Elaboration_Warnings_OK_Id,
@@ -892,6 +899,7 @@ package Gen_IL.Fields is
Spec_Entity,
SSO_Set_High_By_Default,
SSO_Set_Low_By_Default,
+ Static_Call_Helper,
Static_Discrete_Predicate,
Static_Elaboration_Desired,
Static_Initialization,
diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb
index 0b70dae6c2f..bf0997e795d 100644
--- a/gcc/ada/gen_il-gen-gen_entities.adb
+++ b/gcc/ada/gen_il-gen-gen_entities.adb
@@ -139,6 +139,7 @@ begin -- Gen_IL.Gen.Gen_Entities
Sm (Is_Discrim_SO_Function, Flag),
Sm (Is_Discriminant_Check_Function, Flag),
Sm (Is_Dispatch_Table_Entity, Flag),
+ Sm (Is_Dispatch_Table_Wrapper, Flag),
Sm (Is_Dispatching_Operation, Flag),
Sm (Is_Eliminated, Flag),
Sm (Is_Entry_Formal, Flag),
@@ -977,8 +978,11 @@ begin -- Gen_IL.Gen.Gen_Entities
Ab (Subprogram_Kind, Overloadable_Kind,
(Sm (Body_Needed_For_SAL, Flag),
- Sm (Class_Wide_Clone, Node_Id),
+ Sm (Class_Postconditions, Node_Id),
+ Sm (Class_Preconditions, Node_Id),
+ Sm (Class_Preconditions_Subprogram, Node_Id),
Sm (Contract, Node_Id),
+ Sm (Dynamic_Call_Helper, Node_Id),
Sm (Elaboration_Entity, Node_Id),
Sm (Elaboration_Entity_Required, Flag),
Sm (First_Entity, Node_Id),
@@ -986,8 +990,11 @@ begin -- Gen_IL.Gen.Gen_Entities
Sm (Has_Nested_Subprogram, Flag),
Sm (Has_Out_Or_In_Out_Parameter, Flag),
Sm (Has_Recursive_Call, Flag),
+ Sm (Ignored_Class_Postconditions, Node_Id),
+ Sm (Ignored_Class_Preconditions, Node_Id),
Sm (Ignore_SPARK_Mode_Pragmas, Flag),
Sm (Import_Pragma, Node_Id),
+ Sm (Indirect_Call_Wrapper, Node_Id),
Sm (Interface_Alias, Node_Id),
Sm (Interface_Name, Node_Id),
Sm (Is_Elaboration_Checks_OK_Id, Flag),
@@ -998,6 +1005,7 @@ begin -- Gen_IL.Gen.Gen_Entities
Sm (Overridden_Operation, Node_Id),
Sm (Protected_Body_Subprogram, Node_Id),
Sm (Scope_Depth_Value, Uint),
+ Sm (Static_Call_Helper, Node_Id),
Sm (SPARK_Pragma, Node_Id),
Sm (SPARK_Pragma_Inherited, Flag),
Sm (Subps_Index, Uint)));
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 42ea0f52cf3..1720fe01cb8 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -584,6 +584,15 @@ package body Ghost is
-- Start of processing for Check_Ghost_Context
begin
+ -- Class-wide pre/postconditions of ignored pragmas are preanalyzed
+ -- to report errors on wrong conditions; however, ignored pragmas may
+ -- also have references to ghost entities and we must disable checking
+ -- their context to avoid reporting spurious errors.
+
+ if Inside_Class_Condition_Preanalysis then
+ return;
+ end if;
+
-- Once it has been established that the reference to the Ghost entity
-- is within a suitable context, ensure that the policy at the point of
-- declaration and at the point of use match.
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index 2fdccf756a6..699f68520ba 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -291,6 +291,10 @@ package Sem is
-- freezing nodes can modify the status of this flag, any other client
-- should regard it as read-only.
+ Inside_Class_Condition_Preanalysis : Boolean := False;
+ -- Flag indicating whether we are preanalyzing a class-wide precondition
+ -- or postcondition.
+
Inside_Preanalysis_Without_Freezing : Nat := 0;
-- Flag indicating whether we are preanalyzing an expression performing no
-- freezing. Non-zero means we are inside (it is actually a level counter
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index d954d46aaad..7b6dc21b6f0 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1339,6 +1339,16 @@ package body Sem_Attr is
Legal := False;
Spec_Id := Empty;
+ -- Skip processing during preanalysis of class-wide preconditions and
+ -- postconditions since at this stage the expression is not installed
+ -- yet on its definite context.
+
+ if Inside_Class_Condition_Preanalysis then
+ Legal := True;
+ Spec_Id := Current_Scope;
+ return;
+ end if;
+
-- Traverse the parent chain to find the aspect or pragma where the
-- attribute resides.
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 595a741346f..15b3c444125 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -26,6 +26,7 @@
with Aspects; use Aspects;
with Atree; use Atree;
with Checks; use Checks;
+with Contracts; use Contracts;
with Debug; use Debug;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
@@ -4446,6 +4447,38 @@ package body Sem_Ch13 is
goto Continue;
end if;
+ -- Remember class-wide conditions; they will be merged
+ -- with inherited conditions.
+
+ if Class_Present (Aspect)
+ and then A_Id in Aspect_Pre | Aspect_Post
+ and then Is_Subprogram (E)
+ and then not Is_Ignored_Ghost_Entity (E)
+ then
+ if A_Id = Aspect_Pre then
+ if Is_Ignored (Aspect) then
+ Set_Ignored_Class_Preconditions (E,
+ New_Copy_Tree (Expr));
+ else
+ Set_Class_Preconditions (E, New_Copy_Tree (Expr));
+ end if;
+
+ -- Postconditions may split into separate aspects, and we
+ -- remember the expression before such split (i.e. when
+ -- the first postcondition is processed).
+
+ elsif No (Class_Postconditions (E))
+ and then No (Ignored_Class_Postconditions (E))
+ then
+ if Is_Ignored (Aspect) then
+ Set_Ignored_Class_Postconditions (E,
+ New_Copy_Tree (Expr));
+ else
+ Set_Class_Postconditions (E, New_Copy_Tree (Expr));
+ end if;
+ end if;
+ end if;
+
-- If the expressions is of the form A and then B, then
-- we generate separate Pre/Post aspects for the separate
-- clauses. Since we allow multiple pragmas, there is no
@@ -13169,6 +13202,13 @@ package body Sem_Ch13 is
end if;
end Check_Variant_Part;
end if;
+
+ if not In_Generic_Scope (E)
+ and then Ekind (E) = E_Record_Type
+ and then Is_Tagged_Type (E)
+ then
+ Process_Class_Conditions_At_Freeze_Point (E);
+ end if;
end Freeze_Entity_Checks;
-------------------------
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 7a8d0cc7f1d..63bb80c1291 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -3028,6 +3028,10 @@ package body Sem_Ch5 is
then
Analyze_And_Resolve (Original_Bound, Typ);
return Original_Bound;
+
+ elsif Inside_Class_Condition_Preanalysis then
+ Analyze_And_Resolve (Original_Bound, Typ);
+ return Original_Bound;
end if;
-- Normally, the best approach is simply to generate a constant
@@ -3333,11 +3337,17 @@ package body Sem_Ch5 is
-- or post-condition has been expanded. Update the type of the loop
-- variable to reflect the proper itype at each stage of analysis.
+ -- Loop_Nod might not be present when we are preanalyzing a class-wide
+ -- pre/postcondition since preanalysis occurs in a place unrelated to
+ -- the actual code and the quantified expression may be the outermost
+ -- expression of the class-wide condition.
+
if No (Etype (Id))
or else Etype (Id) = Any_Type
or else
(Present (Etype (Id))
and then Is_Itype (Etype (Id))
+ and then Present (Loop_Nod)
and then Nkind (Parent (Loop_Nod)) = N_Expression_With_Actions
and then Nkind (Original_Node (Parent (Loop_Nod))) =
N_Quantified_Expression)
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 02928342744..1fcbdfbf918 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -4498,29 +4498,6 @@ package body Sem_Ch6 is
end if;
end if;
- -- If the subprogram has a class-wide clone, build its body as a copy
- -- of the original body, and rewrite body of original subprogram as a
- -- wrapper that calls the clone. If N is a stub, this construction will
- -- take place when the proper body is analyzed. No action needed if this
- -- subprogram has been eliminated.
-
- if Present (Spec_Id)
- and then Present (Class_Wide_Clone (Spec_Id))
- and then (Comes_From_Source (N) or else Was_Expression_Function (N))
- and then Nkind (N) /= N_Subprogram_Body_Stub
- and then not (Expander_Active and then Is_Eliminated (Spec_Id))
- then
- Build_Class_Wide_Clone_Body (Spec_Id, N);
-
- -- This is the new body for the existing primitive operation
-
- Rewrite (N, Build_Class_Wide_Clone_Call
- (Sloc (N), New_List, Spec_Id, Parent (Spec_Id)));
- Set_Has_Completion (Spec_Id, False);
- Analyze (N);
- return;
- end if;
-
-- Place subprogram on scope stack, and make formals visible. If there
-- is a spec, the visible entity remains that of the spec.
@@ -10413,6 +10390,7 @@ package body Sem_Ch6 is
begin
Set_Is_Immediately_Visible (E);
Set_Current_Entity (E);
+ pragma Assert (Prev /= E);
Set_Homonym (E, Prev);
end Install_Entity;
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index cc612db9f1b..cba3c9dbb0d 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -32,9 +32,11 @@ with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
with Exp_Disp; use Exp_Disp;
with Exp_Util; use Exp_Util;
+with Exp_Ch6; use Exp_Ch6;
with Exp_Ch7; use Exp_Ch7;
with Exp_Tss; use Exp_Tss;
with Errout; use Errout;
+with Freeze; use Freeze;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
with Nlists; use Nlists;
@@ -197,6 +199,91 @@ package body Sem_Disp is
return Empty;
end Covered_Interface_Op;
+ ----------------------------------
+ -- Covered_Interface_Primitives --
+ ----------------------------------
+
+ function Covered_Interface_Primitives (Prim : Entity_Id) return Elist_Id is
+ Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Prim);
+ Elmt : Elmt_Id;
+ E : Entity_Id;
+ Result : Elist_Id := No_Elist;
+
+ begin
+ pragma Assert (Is_Dispatching_Operation (Prim));
+
+ -- Although this is a dispatching primitive we must check if its
+ -- dispatching type is available because it may be the primitive
+ -- of a private type not defined as tagged in its partial view.
+
+ if Present (Tagged_Type) and then Has_Interfaces (Tagged_Type) then
+
+ -- If the tagged type is frozen then the internal entities associated
+ -- with interfaces are available in the list of primitives of the
+ -- tagged type and can be used to speed up this search.
+
+ if Is_Frozen (Tagged_Type) then
+ Elmt := First_Elmt (Primitive_Operations (Tagged_Type));
+ while Present (Elmt) loop
+ E := Node (Elmt);
+
+ if Present (Interface_Alias (E))
+ and then Alias (E) = Prim
+ then
+ if No (Result) then
+ Result := New_Elmt_List;
+ end if;
+
+ Append_Elmt (Interface_Alias (E), Result);
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+
+ -- Otherwise we must collect all the interface primitives and check
+ -- whether the Prim overrides (implements) some interface primitive.
+
+ else
+ declare
+ Ifaces_List : Elist_Id;
+ Iface_Elmt : Elmt_Id;
+ Iface : Entity_Id;
+ Iface_Prim : Entity_Id;
+
+ begin
+ Collect_Interfaces (Tagged_Type, Ifaces_List);
+
+ Iface_Elmt := First_Elmt (Ifaces_List);
+ while Present (Iface_Elmt) loop
+ Iface := Node (Iface_Elmt);
+
+ Elmt := First_Elmt (Primitive_Operations (Iface));
+ while Present (Elmt) loop
+ Iface_Prim := Node (Elmt);
+
+ if Chars (Iface_Prim) = Chars (Prim)
+ and then Is_Interface_Conformant
+ (Tagged_Type, Iface_Prim, Prim)
+ then
+ if No (Result) then
+ Result := New_Elmt_List;
+ end if;
+
+ Append_Elmt (Iface_Prim, Result);
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+
+ Next_Elmt (Iface_Elmt);
+ end loop;
+ end;
+ end if;
+ end if;
+
+ return Result;
+ end Covered_Interface_Primitives;
+
-------------------------------
-- Check_Controlling_Formals --
-------------------------------
@@ -592,6 +679,14 @@ package body Sem_Disp is
-- Start of processing for Check_Dispatching_Context
begin
+ -- Skip checking context of dispatching calls during preanalysis of
+ -- class-wide conditions since at that stage the expression is not
+ -- installed yet on its definite context.
+
+ if Inside_Class_Condition_Preanalysis then
+ return;
+ end if;
+
-- If the called subprogram is a private overriding, replace it
-- with its alias, which has the correct body. Verify that the
-- two subprograms have the same controlling type (this is not the
@@ -992,10 +1087,17 @@ package body Sem_Disp is
-- nonstatic values, then report an error. This is specified by
-- RM 6.1.1(18.2/5) (by AI12-0412).
+ -- Skip reporting this error on helpers and indirect-call wrappers
+ -- built to support class-wide preconditions.
+
if No (Control)
and then not Is_Abstract_Subprogram (Subp_Entity)
and then
Is_Prim_Of_Abst_Type_With_Nonstatic_CW_Pre_Post (Subp_Entity)
+ and then not
+ (Is_Subprogram (Current_Scope)
+ and then
+ Present (Class_Preconditions_Subprogram (Current_Scope)))
then
Error_Msg_N
("nondispatching call to nonabstract subprogram of "
@@ -1463,6 +1565,9 @@ package body Sem_Disp is
end;
end if;
end if;
+
+ Check_Inherited_Conditions (Tagged_Type,
+ Late_Overriding => True);
end if;
end if;
end;
@@ -2925,6 +3030,11 @@ package body Sem_Disp is
Next_Actual (Arg);
end loop;
+ -- Add class-wide precondition check if the target of this dispatching
+ -- call has or inherits class-wide preconditions.
+
+ Install_Class_Preconditions_Check (Call_Node);
+
-- Expansion of dispatching calls is suppressed on VM targets, because
-- the VM back-ends directly handle the generation of dispatching calls
-- and would have to undo any expansion to an indirect call.
diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads
index 7b42cf54d12..f37391b6307 100644
--- a/gcc/ada/sem_disp.ads
+++ b/gcc/ada/sem_disp.ads
@@ -74,6 +74,10 @@ package Sem_Disp is
-- The Alias of Old_Subp is adjusted to point to the inherited procedure
-- of the full view because it is always this one which has to be called.
+ function Covered_Interface_Primitives (Prim : Entity_Id) return Elist_Id;
+ -- Returns all the interface primitives covered by Prim, when its
+ -- controlling type has progenitors.
+
function Covered_Interface_Op (Prim : Entity_Id) return Entity_Id;
-- Returns the interface primitive that Prim covers, when its controlling
-- type has progenitors.
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0228717d707..7386ecc1b93 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -25896,23 +25896,6 @@ package body Sem_Prag is
("operation in class-wide condition must be primitive "
& "of &", Nod, Disp_Typ);
end if;
-
- -- Otherwise we have a call to an overridden primitive, and we
- -- will create a common class-wide clone for the body of
- -- original operation and its eventual inherited versions. If
- -- the original operation dispatches on result it is never
- -- inherited and there is no need for a clone. There is not
- -- need for a clone either in GNATprove mode, as cases that
- -- would require it are rejected (when an inherited primitive
- -- calls an overridden operation in a class-wide contract), and
- -- the clone would make proof impossible in some cases.
-
- elsif not Is_Abstract_Subprogram (Spec_Id)
- and then No (Class_Wide_Clone (Spec_Id))
- and then not Has_Controlling_Result (Spec_Id)
- and then not GNATprove_Mode
- then
- Build_Class_Wide_Clone_Decl (Spec_Id);
end if;
end;
@@ -26033,15 +26016,6 @@ package body Sem_Prag is
End_Scope;
end if;
- -- If analysis of the condition indicates that a class-wide clone
- -- has been created, build and analyze its declaration.
-
- if Is_Subprogram (Spec_Id)
- and then Present (Class_Wide_Clone (Spec_Id))
- then
- Analyze (Unit_Declaration_Node (Class_Wide_Clone (Spec_Id)));
- end if;
-
-- Currently it is not possible to inline pre/postconditions on a
-- subprogram subject to pragma Inline_Always.
@@ -29528,9 +29502,6 @@ package body Sem_Prag is
Msg_Arg : Node_Id;
Nam : Name_Id;
- Needs_Wrapper : Boolean;
- pragma Unreferenced (Needs_Wrapper);
-
-- Start of processing for Build_Pragma_Check_Equivalent
begin
@@ -29557,11 +29528,10 @@ package body Sem_Prag is
-- Build the inherited class-wide condition
Build_Class_Wide_Expression
- (Prag => Check_Prag,
- Subp => Subp_Id,
- Par_Subp => Inher_Id,
- Adjust_Sloc => True,
- Needs_Wrapper => Needs_Wrapper);
+ (Pragma_Or_Expr => Check_Prag,
+ Subp => Subp_Id,
+ Par_Subp => Inher_Id,
+ Adjust_Sloc => True);
-- If not an inherited condition simply copy the original pragma
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7b9f8ab48d8..0d013ba7ec1 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4891,10 +4891,15 @@ package body Sem_Res is
-- Apply legality rule 3.9.2 (9/1)
+ -- Skip this check on helpers and indirect-call wrappers built to
+ -- support class-wide preconditions.
+
if (Is_Class_Wide_Type (A_Typ) or else Is_Dynamically_Tagged (A))
and then not Is_Class_Wide_Type (F_Typ)
and then not Is_Controlling_Formal (F)
and then not In_Instance
+ and then (not Is_Subprogram (Nam)
+ or else No (Class_Preconditions_Subprogram (Nam)))
then
Error_Msg_N ("class-wide argument not allowed here!", A);
@@ -4992,9 +4997,13 @@ package body Sem_Res is
-- "False" cannot act as an actual in a subprogram with value
-- "True" (SPARK RM 6.1.7(3)).
+ -- No check needed for helpers and indirect-call wrappers built to
+ -- support class-wide preconditions.
+
if Is_EVF_Expression (A)
and then Extensions_Visible_Status (Nam) =
Extensions_Visible_True
+ and then No (Class_Preconditions_Subprogram (Current_Scope))
then
Error_Msg_N
("formal parameter cannot act as actual parameter when "
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 816fb451fd0..98e68779107 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2212,180 +2212,6 @@ package body Sem_Util is
return Empty;
end Build_Actual_Subtype_Of_Component;
- ---------------------------------
- -- Build_Class_Wide_Clone_Body --
- ---------------------------------
-
- procedure Build_Class_Wide_Clone_Body
- (Spec_Id : Entity_Id;
- Bod : Node_Id)
- is
- Loc : constant Source_Ptr := Sloc (Bod);
- Clone_Id : constant Entity_Id := Class_Wide_Clone (Spec_Id);
- Clone_Body : Node_Id;
- Assoc_List : constant Elist_Id := New_Elmt_List;
-
- begin
- -- The declaration of the class-wide clone was created when the
- -- corresponding class-wide condition was analyzed.
-
- -- The body of the original condition may contain references to
- -- the formals of Spec_Id. In the body of the class-wide clone,
- -- these must be replaced with the corresponding formals of
- -- the clone.
-
- declare
- Spec_Formal_Id : Entity_Id := First_Formal (Spec_Id);
- Clone_Formal_Id : Entity_Id := First_Formal (Clone_Id);
- begin
- while Present (Spec_Formal_Id) loop
- Append_Elmt (Spec_Formal_Id, Assoc_List);
- Append_Elmt (Clone_Formal_Id, Assoc_List);
-
- Next_Formal (Spec_Formal_Id);
- Next_Formal (Clone_Formal_Id);
- end loop;
- end;
-
- Clone_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Subprogram_Spec (Parent (Clone_Id)),
- Declarations => Declarations (Bod),
- Handled_Statement_Sequence =>
- New_Copy_Tree (Handled_Statement_Sequence (Bod),
- Map => Assoc_List));
-
- -- The new operation is internal and overriding indicators do not apply
- -- (the original primitive may have carried one).
-
- Set_Must_Override (Specification (Clone_Body), False);
-
- -- If the subprogram body is the proper body of a stub, insert the
- -- subprogram after the stub, i.e. the same declarative region as
- -- the original sugprogram.
-
- if Nkind (Parent (Bod)) = N_Subunit then
- Insert_After (Corresponding_Stub (Parent (Bod)), Clone_Body);
-
- else
- Insert_Before (Bod, Clone_Body);
- end if;
-
- Analyze (Clone_Body);
- end Build_Class_Wide_Clone_Body;
-
- ---------------------------------
- -- Build_Class_Wide_Clone_Call --
- ---------------------------------
-
- function Build_Class_Wide_Clone_Call
- (Loc : Source_Ptr;
- Decls : List_Id;
- Spec_Id : Entity_Id;
- Spec : Node_Id) return Node_Id
- is
- Clone_Id : constant Entity_Id := Class_Wide_Clone (Spec_Id);
- Par_Type : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
-
- Actuals : List_Id;
- Call : Node_Id;
- Formal : Entity_Id;
- New_Body : Node_Id;
- New_F_Spec : Entity_Id;
- New_Formal : Entity_Id;
-
- begin
- Actuals := Empty_List;
- Formal := First_Formal (Spec_Id);
- New_F_Spec := First (Parameter_Specifications (Spec));
-
- -- Build parameter association for call to class-wide clone.
-
- while Present (Formal) loop
- New_Formal := Defining_Identifier (New_F_Spec);
-
- -- If controlling argument and operation is inherited, add conversion
- -- to parent type for the call.
-
- if Etype (Formal) = Par_Type
- and then not Is_Empty_List (Decls)
- then
- Append_To (Actuals,
- Make_Type_Conversion (Loc,
- New_Occurrence_Of (Par_Type, Loc),
- New_Occurrence_Of (New_Formal, Loc)));
-
- else
- Append_To (Actuals, New_Occurrence_Of (New_Formal, Loc));
- end if;
-
- Next_Formal (Formal);
- Next (New_F_Spec);
- end loop;
-
- if Ekind (Spec_Id) = E_Procedure then
- Call :=
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Clone_Id, Loc),
- Parameter_Associations => Actuals);
- else
- Call :=
- Make_Simple_Return_Statement (Loc,
- Expression =>
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (Clone_Id, Loc),
- Parameter_Associations => Actuals));
- end if;
-
- New_Body :=
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Subprogram_Spec (Spec),
- Declarations => Decls,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Call),
- End_Label => Make_Identifier (Loc, Chars (Spec_Id))));
-
- return New_Body;
- end Build_Class_Wide_Clone_Call;
-
- ---------------------------------
- -- Build_Class_Wide_Clone_Decl --
- ---------------------------------
-
- procedure Build_Class_Wide_Clone_Decl (Spec_Id : Entity_Id) is
- Loc : constant Source_Ptr := Sloc (Spec_Id);
- Clone_Id : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- New_External_Name (Chars (Spec_Id), Suffix => "CL"));
-
- Decl : Node_Id;
- Spec : Node_Id;
-
- begin
- Spec := Copy_Subprogram_Spec (Parent (Spec_Id));
- Set_Must_Override (Spec, False);
- Set_Must_Not_Override (Spec, False);
- Set_Defining_Unit_Name (Spec, Clone_Id);
-
- Decl := Make_Subprogram_Declaration (Loc, Spec);
- Append (Decl, List_Containing (Unit_Declaration_Node (Spec_Id)));
-
- -- Link clone to original subprogram, for use when building body and
- -- wrapper call to inherited operation.
-
- Set_Class_Wide_Clone (Spec_Id, Clone_Id);
-
- -- Inherit debug info flag from Spec_Id to Clone_Id to allow debugging
- -- of the class-wide clone subprogram.
-
- if Needs_Debug_Info (Spec_Id) then
- Set_Debug_Info_Needed (Clone_Id);
- end if;
- end Build_Class_Wide_Clone_Decl;
-
-----------------------------
-- Build_Component_Subtype --
-----------------------------
@@ -5878,6 +5704,30 @@ package body Sem_Util is
end if;
end Choice_List;
+ ---------------------
+ -- Class_Condition --
+ ---------------------
+
+ function Class_Condition
+ (Kind : Condition_Kind;
+ Subp : Entity_Id) return Node_Id is
+
+ begin
+ case Kind is
+ when Class_Postcondition =>
+ return Class_Postconditions (Subp);
+
+ when Class_Precondition =>
+ return Class_Preconditions (Subp);
+
+ when Ignored_Class_Postcondition =>
+ return Ignored_Class_Postconditions (Subp);
+
+ when Ignored_Class_Precondition =>
+ return Ignored_Class_Preconditions (Subp);
+ end case;
+ end Class_Condition;
+
-------------------------
-- Collect_Body_States --
-------------------------
@@ -22789,6 +22639,61 @@ package body Sem_Util is
return Result;
end Might_Raise;
+ ----------------------------------------
+ -- Nearest_Class_Condition_Subprogram --
+ ----------------------------------------
+
+ function Nearest_Class_Condition_Subprogram
+ (Kind : Condition_Kind;
+ Spec_Id : Entity_Id) return Entity_Id
+ is
+ Subp_Id : constant Entity_Id := Ultimate_Alias (Spec_Id);
+
+ begin
+ -- Prevent cascaded errors
+
+ if not Is_Dispatching_Operation (Subp_Id) then
+ return Empty;
+
+ -- No need to search if this subprogram has class-wide postconditions
+
+ elsif Present (Class_Condition (Kind, Subp_Id)) then
+ return Subp_Id;
+ end if;
+
+ -- Process the contracts of inherited subprograms, looking for
+ -- class-wide pre/postconditions.
+
+ declare
+ Subps : constant Subprogram_List := Inherited_Subprograms (Subp_Id);
+ Subp_Id : Entity_Id;
+
+ begin
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+
+ if Present (Alias (Subp_Id)) then
+ Subp_Id := Ultimate_Alias (Subp_Id);
+ end if;
+
+ -- Wrappers of class-wide pre/postconditions reference the
+ -- parent primitive that has the inherited contract.
+
+ if Is_Wrapper (Subp_Id)
+ and then Present (LSP_Subprogram (Subp_Id))
+ then
+ Subp_Id := LSP_Subprogram (Subp_Id);
+ end if;
+
+ if Present (Class_Condition (Kind, Subp_Id)) then
+ return Subp_Id;
+ end if;
+ end loop;
+ end;
+
+ return Empty;
+ end Nearest_Class_Condition_Subprogram;
+
--------------------------------
-- Nearest_Enclosing_Instance --
--------------------------------
@@ -31535,8 +31440,16 @@ package body Sem_Util is
-- type case correctly, so we avoid that problem by
-- returning True here.
return True;
+
elsif Ada_Version < Ada_2022 then
return False;
+
+ elsif Inside_Class_Condition_Preanalysis then
+ -- No need to evaluate it during preanalysis of a class-wide
+ -- pre/postcondition since the expression is not installed yet
+ -- on its definite context.
+ return False;
+
elsif not Is_Conditionally_Evaluated (Expr) then
return False;
else
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 4e896a3599f..7a7771562c6 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -283,30 +283,6 @@ package Sem_Util is
-- take care of constructing declaration and body of the clone, and
-- building the calls to it within the appropriate wrappers.
- procedure Build_Class_Wide_Clone_Body
- (Spec_Id : Entity_Id;
- Bod : Node_Id);
- -- Build body of subprogram that has a class-wide condition that contains
- -- calls to other primitives. Spec_Id is the Id of the subprogram, and B
- -- is its source body, which becomes the body of the clone.
-
- function Build_Class_Wide_Clone_Call
- (Loc : Source_Ptr;
- Decls : List_Id;
- Spec_Id : Entity_Id;
- Spec : Node_Id) return Node_Id;
- -- Build a call to the common class-wide clone of a subprogram with
- -- class-wide conditions. The body of the subprogram becomes a wrapper
- -- for a call to the clone. The inherited operation becomes a similar
- -- wrapper to which modified conditions apply, and the call to the
- -- clone includes the proper conversion in a call the parent operation.
-
- procedure Build_Class_Wide_Clone_Decl (Spec_Id : Entity_Id);
- -- For a subprogram that has a class-wide condition that contains calls
- -- to other primitives, build an internal subprogram that is invoked
- -- through a type-specific wrapper for all inherited subprograms that
- -- may have a modified condition.
-
procedure Build_Constrained_Itype
(N : Node_Id;
Typ : Entity_Id;
@@ -527,6 +503,18 @@ package Sem_Util is
-- reasons these nodes have a different structure even though they play
-- similar roles in array aggregates.
+ type Condition_Kind is
+ (Ignored_Class_Precondition,
+ Ignored_Class_Postcondition,
+ Class_Precondition,
+ Class_Postcondition);
+ -- Kind of class-wide conditions
+
+ function Class_Condition
+ (Kind : Condition_Kind;
+ Subp : Entity_Id) return Node_Id;
+ -- Class-wide Kind condition of Subp
+
function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
-- Gather the entities of all abstract states and objects declared in the
-- body state space of package body Body_Id.
@@ -2621,6 +2609,12 @@ package Sem_Util is
-- if we're not sure, we return True. If N is a subprogram body, this is
-- about whether execution of that body can raise.
+ function Nearest_Class_Condition_Subprogram
+ (Kind : Condition_Kind;
+ Spec_Id : Entity_Id) return Entity_Id;
+ -- Return the nearest ancestor containing the merged class-wide conditions
+ -- that statically apply to Spec_Id; return Empty otherwise.
+
function Nearest_Enclosing_Instance (E : Entity_Id) return Entity_Id;
-- Return the entity of the nearest enclosing instance which encapsulates
-- entity E. If no such instance exits, return Empty.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-10-01 6:15 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-10-01 6:15 [gcc r12-4014] [Ada] Ada2022: AI12-0195 overriding class-wide pre/postconditions Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).