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

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 595a741..15b3c44 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;
 
    -------------------------