[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, 23 deletions

diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 56ff61f..eddf314 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;