[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.

1 files changed, 87 insertions, 174 deletions

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 816fb45..98e68779 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