[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, 110 insertions, 0 deletions

diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index cc612db..cba3c9d 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.