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

diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index bfd482e..eb26ebf 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);