From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 3D5873858434; Fri, 1 Oct 2021 06:15:17 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 3D5873858434 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-4014] [Ada] Ada2022: AI12-0195 overriding class-wide pre/postconditions X-Act-Checkin: gcc X-Git-Author: Javier Miranda X-Git-Refname: refs/heads/master X-Git-Oldrev: fa465c1b609c0d9c5ad426cea803204c74dc277a X-Git-Newrev: 475e1d240086365da3e240fb9199eb1c5ad511f8 Message-Id: <20211001061517.3D5873858434@sourceware.org> Date: Fri, 1 Oct 2021 06:15:17 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 01 Oct 2021 06:15:17 -0000 https://gcc.gnu.org/g:475e1d240086365da3e240fb9199eb1c5ad511f8 commit r12-4014-g475e1d240086365da3e240fb9199eb1c5ad511f8 Author: Javier Miranda Date: Mon Aug 2 09:16:47 2021 -0400 [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. Diff: --- gcc/ada/contracts.adb | 1641 +++++++++++++++++++++++++++++------ gcc/ada/contracts.ads | 25 + gcc/ada/einfo.ads | 75 +- gcc/ada/exp_attr.adb | 14 + gcc/ada/exp_ch3.adb | 92 ++ gcc/ada/exp_ch6.adb | 387 ++++++++- gcc/ada/exp_ch6.ads | 3 + gcc/ada/exp_disp.adb | 225 ----- gcc/ada/exp_util.adb | 183 ++-- gcc/ada/exp_util.ads | 48 +- gcc/ada/freeze.adb | 573 +++++++++--- gcc/ada/freeze.ads | 9 + gcc/ada/gen_il-fields.ads | 10 +- gcc/ada/gen_il-gen-gen_entities.adb | 10 +- gcc/ada/ghost.adb | 9 + gcc/ada/sem.ads | 4 + gcc/ada/sem_attr.adb | 10 + gcc/ada/sem_ch13.adb | 40 + gcc/ada/sem_ch5.adb | 10 + gcc/ada/sem_ch6.adb | 24 +- gcc/ada/sem_disp.adb | 110 +++ gcc/ada/sem_disp.ads | 4 + gcc/ada/sem_prag.adb | 38 +- gcc/ada/sem_res.adb | 9 + gcc/ada/sem_util.adb | 261 ++---- gcc/ada/sem_util.ads | 42 +- 26 files changed, 2843 insertions(+), 1013 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 705f197148c..2726486d200 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -47,6 +47,8 @@ with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; with Sem_Disp; use Sem_Disp; with Sem_Prag; use Sem_Prag; +with Sem_Res; use Sem_Res; +with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; @@ -66,6 +68,16 @@ package body Contracts is -- -- Part_Of + procedure Check_Class_Condition + (Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Is_Precondition : Boolean); + -- Perform checking of class-wide pre/postcondition Cond inherited by Subp + -- from Par_Subp. Is_Precondition enables check specific for preconditions. + -- In SPARK_Mode, an inherited operation that is not overridden but has + -- inherited modified conditions pre/postconditions is illegal. + procedure Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id : Entity_Id); -- Perform checking of external properties pragmas that is common to both @@ -77,6 +89,12 @@ package body Contracts is -- well as Contract_Cases, Subprogram_Variant, invariants and predicates. -- Body_Id denotes the entity of the subprogram body. + procedure Set_Class_Condition + (Kind : Condition_Kind; + Subp : Entity_Id; + Cond : Node_Id); + -- Set the class-wide Kind condition of Subp + ----------------------- -- Add_Contract_Item -- ----------------------- @@ -386,23 +404,7 @@ package body Contracts is | N_Generic_Subprogram_Declaration | N_Subprogram_Declaration then - declare - Subp_Id : constant Entity_Id := Defining_Entity (Decl); - - begin - Analyze_Entry_Or_Subprogram_Contract (Subp_Id); - - -- If analysis of a class-wide pre/postcondition indicates - -- that a class-wide clone is needed, analyze its declaration - -- now. Its body is created when the body of the original - -- operation is analyzed (and rewritten). - - if Is_Subprogram (Subp_Id) - and then Present (Class_Wide_Clone (Subp_Id)) - then - Analyze (Unit_Declaration_Node (Class_Wide_Clone (Subp_Id))); - end if; - end; + Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl)); -- Entry or subprogram bodies @@ -1491,6 +1493,141 @@ package body Contracts is (Type_Or_Obj_Id => Type_Id); end Analyze_Type_Contract; + --------------------------- + -- Check_Class_Condition -- + --------------------------- + + procedure Check_Class_Condition + (Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Is_Precondition : Boolean) + is + function Check_Entity (N : Node_Id) return Traverse_Result; + -- Check reference to formal of inherited operation or to primitive + -- operation of root type. + + ------------------ + -- Check_Entity -- + ------------------ + + function Check_Entity (N : Node_Id) return Traverse_Result is + New_E : Entity_Id; + Orig_E : Entity_Id; + + begin + if Nkind (N) = N_Identifier + and then Present (Entity (N)) + and then + (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) + and then + (Nkind (Parent (N)) /= N_Attribute_Reference + or else Attribute_Name (Parent (N)) /= Name_Class) + then + -- These checks do not apply to dispatching calls within the + -- condition, but only to calls whose static tag is that of + -- the parent type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + and then Present (Controlling_Argument (Parent (N))) + then + return OK; + end if; + + -- Determine whether entity has a renaming + + Orig_E := Entity (N); + New_E := Get_Mapped_Entity (Orig_E); + + if Present (New_E) then + + -- AI12-0166: A precondition for a protected operation + -- cannot include an internal call to a protected function + -- of the type. In the case of an inherited condition for an + -- overriding operation, both the operation and the function + -- are given by primitive wrappers. + + if Is_Precondition + and then Ekind (New_E) = E_Function + and then Is_Primitive_Wrapper (New_E) + and then Is_Primitive_Wrapper (Subp) + and then Scope (Subp) = Scope (New_E) + then + Error_Msg_Node_2 := Wrapped_Entity (Subp); + Error_Msg_NE + ("internal call to& cannot appear in inherited " + & "precondition of protected operation&", + Subp, Wrapped_Entity (New_E)); + end if; + end if; + + -- Check that there are no calls left to abstract operations if + -- the current subprogram is not abstract. + + if Present (New_E) + and then Nkind (Parent (N)) = N_Function_Call + and then N = Name (Parent (N)) + then + if not Is_Abstract_Subprogram (Subp) + and then Is_Abstract_Subprogram (New_E) + then + Error_Msg_Sloc := Sloc (Current_Scope); + Error_Msg_Node_2 := Subp; + + if Comes_From_Source (Subp) then + Error_Msg_NE + ("cannot call abstract subprogram & in inherited " + & "condition for&#", Subp, New_E); + else + Error_Msg_NE + ("cannot call abstract subprogram & in inherited " + & "condition for inherited&#", Subp, New_E); + end if; + + -- In SPARK mode, report error on inherited condition for an + -- inherited operation if it contains a call to an overriding + -- operation, because this implies that the pre/postconditions + -- of the inherited operation have changed silently. + + elsif SPARK_Mode = On + and then Warn_On_Suspicious_Contract + and then Present (Alias (Subp)) + and then Present (New_E) + and then Comes_From_Source (New_E) + then + Error_Msg_N + ("cannot modify inherited condition (SPARK RM 6.1.1(1))", + Parent (Subp)); + Error_Msg_Sloc := Sloc (New_E); + Error_Msg_Node_2 := Subp; + Error_Msg_NE + ("\overriding of&# forces overriding of&", + Parent (Subp), New_E); + end if; + end if; + end if; + + return OK; + end Check_Entity; + + procedure Check_Condition_Entities is + new Traverse_Proc (Check_Entity); + + -- Start of processing for Check_Class_Condition + + begin + -- No check required if the subprograms match + + if Par_Subp = Subp then + return; + end if; + + Update_Primitives_Mapping (Par_Subp, Subp); + Map_Formals (Par_Subp, Subp); + Check_Condition_Entities (Cond); + end Check_Class_Condition; + ----------------------------- -- Create_Generic_Contract -- ----------------------------- @@ -1900,7 +2037,7 @@ package body Contracts is procedure Add_Stable_Property_Contracts (Subp_Id : Entity_Id; Class_Present : Boolean) is - Loc : constant Source_Ptr := Sloc (Subp_Id); + Loc : constant Source_Ptr := Sloc (Subp_Id); procedure Insert_Stable_Property_Check (Formal : Entity_Id; Property_Function : Entity_Id); @@ -2552,13 +2689,38 @@ package body Contracts is --------------------------------- procedure Process_Spec_Postconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Seen : Subprogram_List (Subps'Range) := (others => Empty); + + function Seen_Subp (Subp_Id : Entity_Id) return Boolean; + -- Return True if the contract of subprogram Subp_Id has been + -- processed. + + --------------- + -- Seen_Subp -- + --------------- + + function Seen_Subp (Subp_Id : Entity_Id) return Boolean is + begin + for Index in Seen'Range loop + if Seen (Index) = Subp_Id then + return True; + end if; + end loop; + + return False; + end Seen_Subp; + + -- Local variables + Item : Node_Id; Items : Node_Id; Prag : Node_Id; Subp_Id : Entity_Id; + -- Start of processing for Process_Spec_Postconditions + begin -- Process the contract @@ -2589,7 +2751,7 @@ package body Contracts is Subp_Id := Ultimate_Alias (Subp_Id); end if; - -- Wrappers of class-wide pre/post conditions reference the + -- Wrappers of class-wide pre/postconditions reference the -- parent primitive that has the inherited contract. if Is_Wrapper (Subp_Id) @@ -2600,7 +2762,9 @@ package body Contracts is Items := Contract (Subp_Id); - if Present (Items) then + if not Seen_Subp (Subp_Id) and then Present (Items) then + Seen (Index) := Subp_Id; + Prag := Pre_Post_Conditions (Items); while Present (Prag) loop if Pragma_Name (Prag) = Name_Postcondition @@ -2657,10 +2821,6 @@ package body Contracts is --------------------------- procedure Process_Preconditions is - Class_Pre : Node_Id := Empty; - -- The sole [inherited] class-wide precondition pragma that applies - -- to the subprogram. - Insert_Node : Node_Id := Empty; -- The insertion node after which all pragma Check equivalents are -- inserted. @@ -2669,21 +2829,12 @@ package body Contracts is -- Determine whether arbitrary declaration Decl denotes a renaming of -- a discriminant or protection field _object. - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); - -- Merge two class-wide preconditions by "or else"-ing them. The - -- changes are accumulated in parameter Into. Update the error - -- message of Into. - procedure Prepend_To_Decls (Item : Node_Id); -- Prepend a single item to the declarations of the subprogram body - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); - -- Save a class-wide precondition into Class_Pre, or prepend a normal - -- precondition to the declarations of the body and analyze it. - - procedure Process_Inherited_Preconditions; - -- Collect all inherited class-wide preconditions and merge them into - -- one big precondition to be evaluated as pragma Check. + procedure Prepend_Pragma_To_Decls (Prag : Node_Id); + -- Prepend a normal precondition to the declarations of the body and + -- analyze it. procedure Process_Preconditions_For (Subp_Id : Entity_Id); -- Collect all preconditions of subprogram Subp_Id and prepend their @@ -2737,78 +2888,6 @@ package body Contracts is return False; end Is_Prologue_Renaming; - ------------------------- - -- Merge_Preconditions -- - ------------------------- - - procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is - function Expression_Arg (Prag : Node_Id) return Node_Id; - -- Return the boolean expression argument of a precondition while - -- updating its parentheses count for the subsequent merge. - - function Message_Arg (Prag : Node_Id) return Node_Id; - -- Return the message argument of a precondition - - -------------------- - -- Expression_Arg -- - -------------------- - - function Expression_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args))); - - begin - if Paren_Count (Arg) = 0 then - Set_Paren_Count (Arg, 1); - end if; - - return Arg; - end Expression_Arg; - - ----------------- - -- Message_Arg -- - ----------------- - - function Message_Arg (Prag : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (Prag); - begin - return Get_Pragma_Arg (Last (Args)); - end Message_Arg; - - -- Local variables - - From_Expr : constant Node_Id := Expression_Arg (From); - From_Msg : constant Node_Id := Message_Arg (From); - Into_Expr : constant Node_Id := Expression_Arg (Into); - Into_Msg : constant Node_Id := Message_Arg (Into); - Loc : constant Source_Ptr := Sloc (Into); - - -- Start of processing for Merge_Preconditions - - begin - -- Merge the two preconditions by "or else"-ing them - - Rewrite (Into_Expr, - Make_Or_Else (Loc, - Right_Opnd => Relocate_Node (Into_Expr), - Left_Opnd => From_Expr)); - - -- Merge the two error messages to produce a single message of the - -- form: - - -- failed precondition from ... - -- also failed inherited precondition from ... - - if not Exception_Locations_Suppressed then - Start_String (Strval (Into_Msg)); - Store_String_Char (ASCII.LF); - Store_String_Chars (" also "); - Store_String_Chars (Strval (From_Msg)); - - Set_Strval (Into_Msg, End_String); - end if; - end Merge_Preconditions; - ---------------------- -- Prepend_To_Decls -- ---------------------- @@ -2829,28 +2908,27 @@ package body Contracts is Prepend_To (Decls, Item); end Prepend_To_Decls; - ------------------------------ - -- Prepend_To_Decls_Or_Save -- - ------------------------------ + ----------------------------- + -- Prepend_Pragma_To_Decls -- + ----------------------------- - procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is + procedure Prepend_Pragma_To_Decls (Prag : Node_Id) is Check_Prag : Node_Id; begin - Check_Prag := Build_Pragma_Check_Equivalent (Prag); - - -- Save the sole class-wide precondition (if any) for the next - -- step, where it will be merged with inherited preconditions. + -- Skip the sole class-wide precondition (if any) since it is + -- processed by Merge_Class_Conditions. if Class_Present (Prag) then - pragma Assert (No (Class_Pre)); - Class_Pre := Check_Prag; + null; -- Accumulate the corresponding Check pragmas at the top of the -- declarations. Prepending the items ensures that they will be -- evaluated in their original order. else + Check_Prag := Build_Pragma_Check_Equivalent (Prag); + if Present (Insert_Node) then Insert_After (Insert_Node, Check_Prag); else @@ -2859,87 +2937,7 @@ package body Contracts is Analyze (Check_Prag); end if; - end Prepend_To_Decls_Or_Save; - - ------------------------------------- - -- Process_Inherited_Preconditions -- - ------------------------------------- - - procedure Process_Inherited_Preconditions is - Subps : constant Subprogram_List := - Inherited_Subprograms (Spec_Id); - - Item : Node_Id; - Items : Node_Id; - Prag : Node_Id; - Subp_Id : Entity_Id; - - begin - -- Process the contracts of all inherited subprograms, looking for - -- class-wide preconditions. - - 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/post conditions 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; - - Items := Contract (Subp_Id); - - if Present (Items) then - Prag := Pre_Post_Conditions (Items); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Item := - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Spec_Id, - Inher_Id => Subp_Id); - - -- The pragma Check equivalent of the class-wide - -- precondition is still created even though the - -- pragma may be ignored because the equivalent - -- performs semantic checks. - - if Is_Checked (Prag) then - - -- The spec of an inherited subprogram already - -- yielded a class-wide precondition. Merge the - -- existing precondition with the current one - -- using "or else". - - if Present (Class_Pre) then - Merge_Preconditions (Item, Class_Pre); - else - Class_Pre := Item; - end if; - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - end if; - end loop; - - -- Add the merged class-wide preconditions - - if Present (Class_Pre) then - Prepend_To_Decls (Class_Pre); - Analyze (Class_Pre); - end if; - end Process_Inherited_Preconditions; + end Prepend_Pragma_To_Decls; ------------------------------- -- Process_Preconditions_For -- @@ -2983,7 +2981,7 @@ package body Contracts is N => Body_Decl); end if; - Prepend_To_Decls_Or_Save (Prag); + Prepend_Pragma_To_Decls (Prag); end if; Prag := Next_Pragma (Prag); @@ -3008,7 +3006,7 @@ package body Contracts is if Pragma_Name (Decl) = Name_Precondition and then Is_Checked (Decl) then - Prepend_To_Decls_Or_Save (Decl); + Prepend_Pragma_To_Decls (Decl); end if; -- Skip internally generated code @@ -3073,22 +3071,21 @@ package body Contracts is Next (Decl); end loop; - end if; - -- The processing of preconditions is done in reverse order (body - -- first), because each pragma Check equivalent is inserted at the - -- top of the declarations. This ensures that the final order is - -- consistent with following diagram: + -- The processing of preconditions is done in reverse order (body + -- first), because each pragma Check equivalent is inserted at the + -- top of the declarations. This ensures that the final order is + -- consistent with following diagram: - -- - -- - -- + -- + -- + -- - Process_Preconditions_For (Body_Id); + Process_Preconditions_For (Body_Id); + end if; if Present (Spec_Id) then Process_Preconditions_For (Spec_Id); - Process_Inherited_Preconditions; end if; end Process_Preconditions; @@ -3139,6 +3136,12 @@ package body Contracts is elsif Is_Ignored_Ghost_Entity (Subp_Id) then return; + -- No action needed for helpers and indirect-call wrapper built to + -- support class-wide preconditions. + + elsif Present (Class_Preconditions_Subprogram (Subp_Id)) then + return; + -- Do not re-expand the same contract. This scenario occurs when a -- construct is rewritten into something else during its analysis -- (expression functions for instance). @@ -3605,61 +3608,1191 @@ package body Contracts is end if; end Instantiate_Subprogram_Contract; - ---------------------------------------- - -- Save_Global_References_In_Contract -- - ---------------------------------------- + ----------------------------------- + -- Make_Class_Precondition_Subps -- + ----------------------------------- - procedure Save_Global_References_In_Contract - (Templ : Node_Id; - Gen_Id : Entity_Id) + procedure Make_Class_Precondition_Subps + (Subp_Id : Entity_Id; + Late_Overriding : Boolean := False) is - procedure Save_Global_References_In_List (First_Prag : Node_Id); - -- Save all global references in contract-related source pragmas found - -- in the list, starting with pragma First_Prag. + Loc : constant Source_Ptr := Sloc (Subp_Id); + Tagged_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id); - ------------------------------------ - -- Save_Global_References_In_List -- - ------------------------------------ + procedure Add_Indirect_Call_Wrapper; + -- Build the indirect-call wrapper and append it to the freezing actions + -- of Tagged_Type. - procedure Save_Global_References_In_List (First_Prag : Node_Id) is - Prag : Node_Id; + procedure Add_Call_Helper + (Helper_Id : Entity_Id; + Is_Dynamic : Boolean); + -- Factorizes code for building a call helper with the given identifier + -- and append it to the freezing actions of Tagged_Type. Is_Dynamic + -- controls building the static or dynamic version of the helper. - begin - Prag := First_Prag; - while Present (Prag) loop - if Is_Generic_Contract_Pragma (Prag) then - Save_Global_References (Prag); + ------------------------------- + -- Add_Indirect_Call_Wrapper -- + ------------------------------- + + procedure Add_Indirect_Call_Wrapper is + + function Build_ICW_Body return Node_Id; + -- Build the body of the indirect call wrapper + + function Build_ICW_Decl return Node_Id; + -- Build the declaration of the indirect call wrapper + + -------------------- + -- Build_ICW_Body -- + -------------------- + + function Build_ICW_Body return Node_Id is + ICW_Id : constant Entity_Id := Indirect_Call_Wrapper (Subp_Id); + Spec : constant Node_Id := Parent (ICW_Id); + Body_Spec : Node_Id; + Call : Node_Id; + ICW_Body : Node_Id; + + begin + Body_Spec := Copy_Subprogram_Spec (Spec); + + -- Build call to wrapped subprogram + + declare + Actuals : constant List_Id := Empty_List; + Formal_Spec : Entity_Id := + First (Parameter_Specifications (Spec)); + begin + -- Build parameter association & call + + while Present (Formal_Spec) loop + Append_To (Actuals, + New_Occurrence_Of + (Defining_Identifier (Formal_Spec), Loc)); + Next (Formal_Spec); + end loop; + + if Ekind (ICW_Id) = E_Procedure then + Call := + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Subp_Id, Loc), + Parameter_Associations => Actuals); + else + Call := + Make_Simple_Return_Statement (Loc, + Expression => + Make_Function_Call (Loc, + Name => New_Occurrence_Of (Subp_Id, Loc), + Parameter_Associations => Actuals)); + end if; + end; + + ICW_Body := + Make_Subprogram_Body (Loc, + Specification => Body_Spec, + Declarations => New_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List (Call))); + + -- The new operation is internal and overriding indicators do not + -- apply. + + Set_Must_Override (Body_Spec, False); + + return ICW_Body; + end Build_ICW_Body; + + -------------------- + -- Build_ICW_Decl -- + -------------------- + + function Build_ICW_Decl return Node_Id is + ICW_Id : constant Entity_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "ICW", + Suffix_Index => Source_Offset (Loc))); + Decl : Node_Id; + Spec : Node_Id; + + begin + Spec := Copy_Subprogram_Spec (Parent (Subp_Id)); + Set_Must_Override (Spec, False); + Set_Must_Not_Override (Spec, False); + Set_Defining_Unit_Name (Spec, ICW_Id); + Mutate_Ekind (ICW_Id, Ekind (Subp_Id)); + Set_Is_Public (ICW_Id); + + -- The indirect call wrapper is commonly used for indirect calls + -- but inlined for direct calls performed from the DTW. + + Set_Is_Inlined (ICW_Id); + + if Nkind (Spec) = N_Procedure_Specification then + Set_Null_Present (Spec, False); end if; - Prag := Next_Pragma (Prag); - end loop; - end Save_Global_References_In_List; + Decl := Make_Subprogram_Declaration (Loc, Spec); - -- Local variables + -- Link original subprogram to indirect wrapper and vice versa - Items : constant Node_Id := Contract (Defining_Entity (Templ)); + Set_Indirect_Call_Wrapper (Subp_Id, ICW_Id); + Set_Class_Preconditions_Subprogram (ICW_Id, Subp_Id); - -- Start of processing for Save_Global_References_In_Contract + -- Inherit debug info flag to allow debugging the wrapper - begin - -- The entity of the analyzed generic copy must be on the scope stack - -- to ensure proper detection of global references. + if Needs_Debug_Info (Subp_Id) then + Set_Debug_Info_Needed (ICW_Id); + end if; - Push_Scope (Gen_Id); + return Decl; + end Build_ICW_Decl; - if Permits_Aspect_Specifications (Templ) - and then Has_Aspects (Templ) - then - Save_Global_References_In_Aspects (Templ); - end if; + -- Local Variables - if Present (Items) then - Save_Global_References_In_List (Pre_Post_Conditions (Items)); - Save_Global_References_In_List (Contract_Test_Cases (Items)); - Save_Global_References_In_List (Classifications (Items)); - end if; + ICW_Body : Node_Id; + ICW_Decl : Node_Id; - Pop_Scope; - end Save_Global_References_In_Contract; + -- Start of processing for Add_Indirect_Call_Wrapper + + begin + pragma Assert (No (Indirect_Call_Wrapper (Subp_Id))); + + ICW_Decl := Build_ICW_Decl; + + Ensure_Freeze_Node (Tagged_Type); + Append_Freeze_Action (Tagged_Type, ICW_Decl); + Analyze (ICW_Decl); + + ICW_Body := Build_ICW_Body; + Append_Freeze_Action (Tagged_Type, ICW_Body); + + -- We cannot defer the analysis of this ICW wrapper when it is + -- built as a consequence of building its partner DTW wrapper + -- at the freezing point of the tagged type. + + if Is_Dispatch_Table_Wrapper (Subp_Id) then + Analyze (ICW_Body); + end if; + end Add_Indirect_Call_Wrapper; + + --------------------- + -- Add_Call_Helper -- + --------------------- + + procedure Add_Call_Helper + (Helper_Id : Entity_Id; + Is_Dynamic : Boolean) + is + function Build_Call_Helper_Body return Node_Id; + -- Build the body of a call helper + + function Build_Call_Helper_Decl return Node_Id; + -- Build the declaration of a call helper + + function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id; + -- Build the specification of the helper + + ---------------------------- + -- Build_Call_Helper_Body -- + ---------------------------- + + function Build_Call_Helper_Body return Node_Id is + + function Copy_And_Update_References + (Expr : Node_Id) return Node_Id; + -- Copy Expr updating references to formals of Helper_Id; update + -- also references to loop identifiers of quantified expressions. + + -------------------------------- + -- Copy_And_Update_References -- + -------------------------------- + + function Copy_And_Update_References + (Expr : Node_Id) return Node_Id + is + Assoc_List : constant Elist_Id := New_Elmt_List; + + procedure Map_Quantified_Expression_Loop_Identifiers; + -- Traverse Expr and append to Assoc_List the mapping of loop + -- identifers of quantified expressions with its new copy. + + ------------------------------------------------ + -- Map_Quantified_Expression_Loop_Identifiers -- + ------------------------------------------------ + + procedure Map_Quantified_Expression_Loop_Identifiers is + function Map_Loop_Param (N : Node_Id) return Traverse_Result; + -- Append to Assoc_List the mapping of loop identifers of + -- quantified expressions with its new copy. + + -------------------- + -- Map_Loop_Param -- + -------------------- + + function Map_Loop_Param (N : Node_Id) return Traverse_Result + is + begin + if Nkind (N) = N_Loop_Parameter_Specification + and then Nkind (Parent (N)) = N_Quantified_Expression + then + declare + Def_Id : constant Entity_Id := + Defining_Identifier (N); + begin + Append_Elmt (Def_Id, Assoc_List); + Append_Elmt (New_Copy (Def_Id), Assoc_List); + end; + end if; + + return OK; + end Map_Loop_Param; + + procedure Map_Quantified_Expressions is + new Traverse_Proc (Map_Loop_Param); + + begin + Map_Quantified_Expressions (Expr); + end Map_Quantified_Expression_Loop_Identifiers; + + -- Local variables + + Subp_Formal_Id : Entity_Id := First_Formal (Subp_Id); + Helper_Formal_Id : Entity_Id := First_Formal (Helper_Id); + + -- Start of processing for Copy_And_Update_References + + begin + while Present (Subp_Formal_Id) loop + Append_Elmt (Subp_Formal_Id, Assoc_List); + Append_Elmt (Helper_Formal_Id, Assoc_List); + + Next_Formal (Subp_Formal_Id); + Next_Formal (Helper_Formal_Id); + end loop; + + Map_Quantified_Expression_Loop_Identifiers; + + return New_Copy_Tree (Expr, Map => Assoc_List); + end Copy_And_Update_References; + + -- Local variables + + Helper_Decl : constant Node_Id := Parent (Parent (Helper_Id)); + Body_Id : Entity_Id; + Body_Spec : Node_Id; + Body_Stmts : Node_Id; + Helper_Body : Node_Id; + Return_Expr : Node_Id; + + -- Start of processing for Build_Call_Helper_Body + + begin + pragma Assert (Analyzed (Unit_Declaration_Node (Helper_Id))); + pragma Assert (No (Corresponding_Body (Helper_Decl))); + + Body_Id := Make_Defining_Identifier (Loc, Chars (Helper_Id)); + Body_Spec := Build_Call_Helper_Spec (Body_Id); + + Set_Corresponding_Body (Helper_Decl, Body_Id); + Set_Must_Override (Body_Spec, False); + + if Present (Class_Preconditions (Subp_Id)) then + Return_Expr := + Copy_And_Update_References (Class_Preconditions (Subp_Id)); + + -- When the subprogram is compiled with assertions disabled the + -- helper just returns True; done to avoid reporting errors at + -- link time since a unit may be compiled with assertions disabled + -- and another (which depends on it) compiled with assertions + -- enabled. + + else + pragma Assert (Present (Ignored_Class_Preconditions (Subp_Id))); + Return_Expr := New_Occurrence_Of (Standard_True, Loc); + end if; + + Body_Stmts := + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List ( + Make_Simple_Return_Statement (Loc, Return_Expr))); + + Helper_Body := + Make_Subprogram_Body (Loc, + Specification => Body_Spec, + Declarations => New_List, + Handled_Statement_Sequence => Body_Stmts); + + return Helper_Body; + end Build_Call_Helper_Body; + + ---------------------------- + -- Build_Call_Helper_Decl -- + ---------------------------- + + function Build_Call_Helper_Decl return Node_Id is + Decl : Node_Id; + Spec : Node_Id; + + begin + Spec := Build_Call_Helper_Spec (Helper_Id); + Set_Must_Override (Spec, False); + Set_Must_Not_Override (Spec, False); + Set_Is_Inlined (Helper_Id); + Set_Is_Public (Helper_Id); + + Decl := Make_Subprogram_Declaration (Loc, Spec); + + -- Inherit debug info flag from Subp_Id to Helper_Id to allow + -- debugging of the helper subprogram. + + if Needs_Debug_Info (Subp_Id) then + Set_Debug_Info_Needed (Helper_Id); + end if; + + return Decl; + end Build_Call_Helper_Decl; + + ---------------------------- + -- Build_Call_Helper_Spec -- + ---------------------------- + + function Build_Call_Helper_Spec (Spec_Id : Entity_Id) return Node_Id + is + Spec : constant Node_Id := Parent (Subp_Id); + Def_Id : constant Node_Id := Defining_Unit_Name (Spec); + Formal : Entity_Id; + Func_Formals : constant List_Id := New_List; + P_Spec : constant List_Id := Parameter_Specifications (Spec); + Par_Formal : Node_Id; + Param : Node_Id; + Param_Type : Node_Id; + + begin + -- Create a list of formal parameters with the same types as the + -- original subprogram but changing the controlling formal. + + Param := First (P_Spec); + Formal := First_Formal (Def_Id); + while Present (Formal) loop + Par_Formal := Parent (Formal); + + if Is_Dynamic and then Is_Controlling_Formal (Formal) then + if Nkind (Parameter_Type (Par_Formal)) + = N_Access_Definition + then + Param_Type := + Copy_Separate_Tree (Parameter_Type (Par_Formal)); + Rewrite (Subtype_Mark (Param_Type), + Make_Attribute_Reference (Loc, + Prefix => Relocate_Node (Subtype_Mark (Param_Type)), + Attribute_Name => Name_Class)); + + else + Param_Type := + Make_Attribute_Reference (Loc, + Prefix => New_Occurrence_Of (Etype (Formal), Loc), + Attribute_Name => Name_Class); + end if; + else + Param_Type := New_Occurrence_Of (Etype (Formal), Loc); + end if; + + Append_To (Func_Formals, + Make_Parameter_Specification (Loc, + Defining_Identifier => + Make_Defining_Identifier (Loc, Chars (Formal)), + In_Present => In_Present (Par_Formal), + Out_Present => Out_Present (Par_Formal), + Null_Exclusion_Present => Null_Exclusion_Present + (Par_Formal), + Parameter_Type => Param_Type)); + + Next (Param); + Next_Formal (Formal); + end loop; + + return + Make_Function_Specification (Loc, + Defining_Unit_Name => Spec_Id, + Parameter_Specifications => Func_Formals, + Result_Definition => + New_Occurrence_Of (Standard_Boolean, Loc)); + end Build_Call_Helper_Spec; + + -- Local variables + + Helper_Body : Node_Id; + Helper_Decl : Node_Id; + + -- Start of processing for Add_Call_Helper + + begin + Helper_Decl := Build_Call_Helper_Decl; + Mutate_Ekind (Helper_Id, Ekind (Subp_Id)); + + -- Add the helper to the freezing actions of the tagged type + + Ensure_Freeze_Node (Tagged_Type); + Append_Freeze_Action (Tagged_Type, Helper_Decl); + Analyze (Helper_Decl); + + Helper_Body := Build_Call_Helper_Body; + Append_Freeze_Action (Tagged_Type, Helper_Body); + + -- If this helper is built as part of building the DTW at the + -- freezing point of its tagged type then we cannot defer + -- its analysis. + + if Late_Overriding then + pragma Assert (Is_Dispatch_Table_Wrapper (Subp_Id)); + Analyze (Helper_Body); + end if; + end Add_Call_Helper; + + -- Local variables + + Helper_Id : Entity_Id; + + -- Start of processing for Make_Class_Precondition_Subps + + begin + if Present (Class_Preconditions (Subp_Id)) + or Present (Ignored_Class_Preconditions (Subp_Id)) + then + pragma Assert + (Comes_From_Source (Subp_Id) + or else Is_Dispatch_Table_Wrapper (Subp_Id)); + + if No (Dynamic_Call_Helper (Subp_Id)) then + + -- Build and add to the freezing actions of Tagged_Type its + -- dynamic-call helper. + + Helper_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "DP", + Suffix_Index => Source_Offset (Loc))); + Add_Call_Helper (Helper_Id, Is_Dynamic => True); + + -- Link original subprogram to helper and vice versa + + Set_Dynamic_Call_Helper (Subp_Id, Helper_Id); + Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); + end if; + + if not Is_Abstract_Subprogram (Subp_Id) + and then No (Static_Call_Helper (Subp_Id)) + then + -- Build and add to the freezing actions of Tagged_Type its + -- static-call helper. + + Helper_Id := + Make_Defining_Identifier (Loc, + New_External_Name (Chars (Subp_Id), + Suffix => "SP", + Suffix_Index => Source_Offset (Loc))); + + Add_Call_Helper (Helper_Id, Is_Dynamic => False); + + -- Link original subprogram to helper and vice versa + + Set_Static_Call_Helper (Subp_Id, Helper_Id); + Set_Class_Preconditions_Subprogram (Helper_Id, Subp_Id); + + -- Build and add to the freezing actions of Tagged_Type the + -- indirect-call wrapper. + + Add_Indirect_Call_Wrapper; + end if; + end if; + end Make_Class_Precondition_Subps; + + ---------------------------------------------- + -- Process_Class_Conditions_At_Freeze_Point -- + ---------------------------------------------- + + procedure Process_Class_Conditions_At_Freeze_Point (Typ : Entity_Id) is + + procedure Check_Class_Conditions (Spec_Id : Entity_Id); + -- Check class-wide pre/postconditions of Spec_Id + + function Has_Class_Postconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean; + -- Return True if Spec_Id has (or inherits) a postconditions subprogram. + + function Has_Class_Preconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean; + -- Return True if Spec_Id has (or inherits) a preconditions subprogram. + + ---------------------------- + -- Check_Class_Conditions -- + ---------------------------- + + procedure Check_Class_Conditions (Spec_Id : Entity_Id) is + Par_Subp : Entity_Id; + + begin + for Kind in Condition_Kind loop + Par_Subp := Nearest_Class_Condition_Subprogram (Kind, Spec_Id); + + if Present (Par_Subp) then + Check_Class_Condition + (Cond => Class_Condition (Kind, Par_Subp), + Subp => Spec_Id, + Par_Subp => Par_Subp, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + end if; + end loop; + end Check_Class_Conditions; + + ----------------------------------------- + -- Has_Class_Postconditions_Subprogram -- + ----------------------------------------- + + function Has_Class_Postconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean is + begin + return + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Class_Postcondition)) + or else + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Ignored_Class_Postcondition)); + end Has_Class_Postconditions_Subprogram; + + ---------------------------------------- + -- Has_Class_Preconditions_Subprogram -- + ---------------------------------------- + + function Has_Class_Preconditions_Subprogram + (Spec_Id : Entity_Id) return Boolean is + begin + return + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Class_Precondition)) + or else + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Spec_Id, + Kind => Ignored_Class_Precondition)); + end Has_Class_Preconditions_Subprogram; + + -- Local variables + + Prim_Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ)); + Prim : Entity_Id; + + -- Start of processing for Process_Class_Conditions_At_Freeze_Point + + begin + while Present (Prim_Elmt) loop + Prim := Node (Prim_Elmt); + + if Has_Class_Preconditions_Subprogram (Prim) + or else Has_Class_Postconditions_Subprogram (Prim) + then + if Comes_From_Source (Prim) then + if Has_Significant_Contract (Prim) then + Merge_Class_Conditions (Prim); + end if; + + -- Handle wrapper of protected operation + + elsif Is_Primitive_Wrapper (Prim) then + Merge_Class_Conditions (Prim); + + -- Check inherited class-wide conditions, excluding internal + -- entities built for mapping of interface primitives. + + elsif Is_Derived_Type (Typ) + and then Present (Alias (Prim)) + and then No (Interface_Alias (Prim)) + then + Check_Class_Conditions (Prim); + end if; + end if; + + Next_Elmt (Prim_Elmt); + end loop; + end Process_Class_Conditions_At_Freeze_Point; + + ---------------------------- + -- Merge_Class_Conditions -- + ---------------------------- + + procedure Merge_Class_Conditions (Spec_Id : Entity_Id) is + + procedure Preanalyze_Condition + (Subp : Entity_Id; + Expr : Node_Id); + -- Preanalyze the class-wide condition Expr of Subp + + procedure Process_Inherited_Conditions (Kind : Condition_Kind); + -- Collect all inherited class-wide conditions of Spec_Id and merge + -- them into one big condition. + + -------------------------- + -- Preanalyze_Condition -- + -------------------------- + + procedure Preanalyze_Condition + (Subp : Entity_Id; + Expr : Node_Id) + is + procedure Clear_Unset_References; + -- Clear unset references on formals of Subp since preanalysis + -- occurs in a place unrelated to the actual code. + + procedure Remove_Controlling_Arguments; + -- Traverse Expr and clear the Controlling_Argument of calls to + -- nonabstract functions. + + procedure Remove_Formals (Id : Entity_Id); + -- Remove formals from homonym chains and make them not visible + + ---------------------------- + -- Clear_Unset_References -- + ---------------------------- + + procedure Clear_Unset_References is + F : Entity_Id := First_Formal (Subp); + + begin + while Present (F) loop + Set_Unset_Reference (F, Empty); + Next_Formal (F); + end loop; + end Clear_Unset_References; + + ---------------------------------- + -- Remove_Controlling_Arguments -- + ---------------------------------- + + procedure Remove_Controlling_Arguments is + function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result; + -- Reset the Controlling_Argument of calls to nonabstract + -- function calls. + + --------------------- + -- Remove_Ctrl_Arg -- + --------------------- + + function Remove_Ctrl_Arg (N : Node_Id) return Traverse_Result is + begin + if Nkind (N) = N_Function_Call + and then Present (Controlling_Argument (N)) + and then not Is_Abstract_Subprogram (Entity (Name (N))) + then + Set_Controlling_Argument (N, Empty); + end if; + + return OK; + end Remove_Ctrl_Arg; + + procedure Remove_Ctrl_Args is new Traverse_Proc (Remove_Ctrl_Arg); + begin + Remove_Ctrl_Args (Expr); + end Remove_Controlling_Arguments; + + -------------------- + -- Remove_Formals -- + -------------------- + + procedure Remove_Formals (Id : Entity_Id) is + F : Entity_Id := First_Formal (Id); + + begin + while Present (F) loop + Set_Is_Immediately_Visible (F, False); + Remove_Homonym (F); + Next_Formal (F); + end loop; + end Remove_Formals; + + -- Start of processing for Preanalyze_Condition + + begin + pragma Assert (Present (Expr)); + pragma Assert (Inside_Class_Condition_Preanalysis = False); + + Push_Scope (Subp); + Install_Formals (Subp); + Inside_Class_Condition_Preanalysis := True; + + Preanalyze_And_Resolve (Expr, Standard_Boolean); + + Inside_Class_Condition_Preanalysis := False; + Remove_Formals (Subp); + Pop_Scope; + + -- Traverse Expr and clear the Controlling_Argument of calls to + -- nonabstract functions. Required since the preanalyzed condition + -- is not yet installed on its definite context and will be cloned + -- and extended in derivations with additional conditions. + + Remove_Controlling_Arguments; + + -- Clear also attribute Unset_Reference; again because preanalysis + -- occurs in a place unrelated to the actual code. + + Clear_Unset_References; + end Preanalyze_Condition; + + ---------------------------------- + -- Process_Inherited_Conditions -- + ---------------------------------- + + procedure Process_Inherited_Conditions (Kind : Condition_Kind) is + Tag_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id); + Subps : constant Subprogram_List := Inherited_Subprograms (Spec_Id); + Seen : Subprogram_List (Subps'Range) := (others => Empty); + + function Inherit_Condition + (Par_Subp : Entity_Id; + Subp : Entity_Id) return Node_Id; + -- Inherit the class-wide condition from Par_Subp to Subp and adjust + -- all the references to formals in the inherited condition. + + procedure Merge_Conditions (From : Node_Id; Into : Node_Id); + -- Merge two class-wide preconditions or postconditions (the former + -- are merged using "or else", and the latter are merged using "and- + -- then"). The changes are accumulated in parameter Into. + + function Seen_Subp (Id : Entity_Id) return Boolean; + -- Return True if the contract of subprogram Id has been processed + + ----------------------- + -- Inherit_Condition -- + ----------------------- + + function Inherit_Condition + (Par_Subp : Entity_Id; + Subp : Entity_Id) return Node_Id + is + Installed_Calls : constant Elist_Id := New_Elmt_List; + + procedure Install_Original_Selected_Component (Expr : Node_Id); + -- Traverse the given expression searching for dispatching calls + -- to functions whose original nodes was a selected component, + -- and replacing them temporarily by a copy of their original + -- node. Modified calls are stored in the list Installed_Calls + -- (to undo this work later). + + procedure Restore_Dispatching_Calls (Expr : Node_Id); + -- Undo the work done by Install_Original_Selected_Component. + + ----------------------------------------- + -- Install_Original_Selected_Component -- + ----------------------------------------- + + procedure Install_Original_Selected_Component (Expr : Node_Id) is + function Install_Node (N : Node_Id) return Traverse_Result; + -- Process a single node + + ------------------ + -- Install_Node -- + ------------------ + + function Install_Node (N : Node_Id) return Traverse_Result is + New_N : Node_Id; + Orig_Nod : Node_Id; + + begin + if Nkind (N) = N_Function_Call + and then Nkind (Original_Node (N)) = N_Selected_Component + and then Is_Dispatching_Operation (Entity (Name (N))) + then + Orig_Nod := Original_Node (N); + + -- Temporarily use the original node field to keep the + -- reference to this node (to undo this work later!). + + New_N := New_Copy (N); + Set_Original_Node (New_N, Orig_Nod); + Append_Elmt (New_N, Installed_Calls); + + Rewrite (N, Orig_Nod); + Set_Original_Node (N, New_N); + end if; + + return OK; + end Install_Node; + + procedure Install_Nodes is new Traverse_Proc (Install_Node); + + begin + Install_Nodes (Expr); + end Install_Original_Selected_Component; + + ------------------------------- + -- Restore_Dispatching_Calls -- + ------------------------------- + + procedure Restore_Dispatching_Calls (Expr : Node_Id) is + function Restore_Node (N : Node_Id) return Traverse_Result; + -- Process a single node + + ------------------ + -- Restore_Node -- + ------------------ + + function Restore_Node (N : Node_Id) return Traverse_Result is + Orig_Sel_N : Node_Id; + + begin + if Nkind (N) = N_Selected_Component + and then Nkind (Original_Node (N)) = N_Function_Call + and then Contains (Installed_Calls, Original_Node (N)) + then + Orig_Sel_N := Original_Node (Original_Node (N)); + pragma Assert (Nkind (Orig_Sel_N) = N_Selected_Component); + Rewrite (N, Original_Node (N)); + Set_Original_Node (N, Orig_Sel_N); + end if; + + return OK; + end Restore_Node; + + procedure Restore_Nodes is new Traverse_Proc (Restore_Node); + + begin + Restore_Nodes (Expr); + end Restore_Dispatching_Calls; + + -- Local variables + + Assoc_List : constant Elist_Id := New_Elmt_List; + Par_Formal_Id : Entity_Id := First_Formal (Par_Subp); + Subp_Formal_Id : Entity_Id := First_Formal (Subp); + New_Expr : Node_Id; + Class_Cond : Node_Id; + + -- Start of processing for Inherit_Condition + + begin + while Present (Par_Formal_Id) loop + Append_Elmt (Par_Formal_Id, Assoc_List); + Append_Elmt (Subp_Formal_Id, Assoc_List); + + Next_Formal (Par_Formal_Id); + Next_Formal (Subp_Formal_Id); + end loop; + + -- In order to properly preanalyze an inherited preanalyzed + -- condition that has occurrences of the Object.Operation + -- notation we must restore the original node; otherwise we + -- would report spurious errors. + + Class_Cond := Class_Condition (Kind, Par_Subp); + + Install_Original_Selected_Component (Class_Cond); + New_Expr := New_Copy_Tree (Class_Cond); + Restore_Dispatching_Calls (Class_Cond); + + return New_Copy_Tree (New_Expr, Map => Assoc_List); + end Inherit_Condition; + + ---------------------- + -- Merge_Conditions -- + ---------------------- + + procedure Merge_Conditions (From : Node_Id; Into : Node_Id) is + function Expression_Arg (Expr : Node_Id) return Node_Id; + -- Return the boolean expression argument of a condition while + -- updating its parentheses count for the subsequent merge. + + -------------------- + -- Expression_Arg -- + -------------------- + + function Expression_Arg (Expr : Node_Id) return Node_Id is + begin + if Paren_Count (Expr) = 0 then + Set_Paren_Count (Expr, 1); + end if; + + return Expr; + end Expression_Arg; + + -- Local variables + + From_Expr : constant Node_Id := Expression_Arg (From); + Into_Expr : constant Node_Id := Expression_Arg (Into); + Loc : constant Source_Ptr := Sloc (Into); + + -- Start of processing for Merge_Conditions + + begin + case Kind is + + -- Merge the two preconditions by "or else"-ing them + + when Ignored_Class_Precondition + | Class_Precondition + => + Rewrite (Into_Expr, + Make_Or_Else (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); + + -- Merge the two postconditions by "and then"-ing them + + when Ignored_Class_Postcondition + | Class_Postcondition + => + Rewrite (Into_Expr, + Make_And_Then (Loc, + Right_Opnd => Relocate_Node (Into_Expr), + Left_Opnd => From_Expr)); + end case; + end Merge_Conditions; + + --------------- + -- Seen_Subp -- + --------------- + + function Seen_Subp (Id : Entity_Id) return Boolean is + begin + for Index in Seen'Range loop + if Seen (Index) = Id then + return True; + end if; + end loop; + + return False; + end Seen_Subp; + + -- Local variables + + Class_Cond : Node_Id; + Cond : Node_Id; + Subp_Id : Entity_Id; + Par_Prim : Entity_Id := Empty; + Par_Iface_Prims : Elist_Id := No_Elist; + + -- Start of processing for Process_Inherited_Conditions + + begin + Class_Cond := Class_Condition (Kind, Spec_Id); + + -- Process parent primitives looking for nearest ancestor with + -- class-wide conditions. + + for Index in Subps'Range loop + Subp_Id := Subps (Index); + + if No (Par_Prim) + and then Is_Ancestor (Find_Dispatching_Type (Subp_Id), Tag_Typ) + then + 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 and help + -- us to climb fast. + + if Is_Wrapper (Subp_Id) + and then Present (LSP_Subprogram (Subp_Id)) + then + Subp_Id := LSP_Subprogram (Subp_Id); + end if; + + if not Seen_Subp (Subp_Id) + and then Present (Class_Condition (Kind, Subp_Id)) + then + Seen (Index) := Subp_Id; + Par_Prim := Subp_Id; + Par_Iface_Prims := Covered_Interface_Primitives (Par_Prim); + + Cond := Inherit_Condition + (Subp => Spec_Id, + Par_Subp => Subp_Id); + + if Present (Class_Cond) then + Merge_Conditions (Cond, Class_Cond); + else + Class_Cond := Cond; + end if; + + Check_Class_Condition + (Cond => Class_Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + Build_Class_Wide_Expression + (Pragma_Or_Expr => Class_Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Adjust_Sloc => False); + + -- We are done as soon as we process the nearest ancestor + + exit; + end if; + end if; + end loop; + + -- Process the contract of interface primitives not covered by + -- the nearest ancestor. + + for Index in Subps'Range loop + Subp_Id := Subps (Index); + + if Is_Interface (Find_Dispatching_Type (Subp_Id)) then + if Present (Alias (Subp_Id)) then + Subp_Id := Ultimate_Alias (Subp_Id); + end if; + + if not Seen_Subp (Subp_Id) + and then Present (Class_Condition (Kind, Subp_Id)) + and then not Contains (Par_Iface_Prims, Subp_Id) + then + Seen (Index) := Subp_Id; + + Cond := Inherit_Condition + (Subp => Spec_Id, + Par_Subp => Subp_Id); + + Check_Class_Condition + (Cond => Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Is_Precondition => Kind in Ignored_Class_Precondition + | Class_Precondition); + Build_Class_Wide_Expression + (Pragma_Or_Expr => Cond, + Subp => Spec_Id, + Par_Subp => Subp_Id, + Adjust_Sloc => False); + + if Present (Class_Cond) then + Merge_Conditions (Cond, Class_Cond); + else + Class_Cond := Cond; + end if; + end if; + end if; + end loop; + + Set_Class_Condition (Kind, Spec_Id, Class_Cond); + end Process_Inherited_Conditions; + + -- Local variables + + Cond : Node_Id; + + -- Start of processing for Merge_Class_Conditions + + begin + for Kind in Condition_Kind loop + Cond := Class_Condition (Kind, Spec_Id); + + -- If this subprogram has class-wide conditions then preanalyze + -- them before processing inherited conditions since conditions + -- are checked and merged from right to left. + + if Present (Cond) then + Preanalyze_Condition (Spec_Id, Cond); + end if; + + Process_Inherited_Conditions (Kind); + + -- Preanalyze merged inherited conditions + + if Cond /= Class_Condition (Kind, Spec_Id) then + Preanalyze_Condition (Spec_Id, + Class_Condition (Kind, Spec_Id)); + end if; + end loop; + end Merge_Class_Conditions; + + ---------------------------------------- + -- Save_Global_References_In_Contract -- + ---------------------------------------- + + procedure Save_Global_References_In_Contract + (Templ : Node_Id; + Gen_Id : Entity_Id) + is + procedure Save_Global_References_In_List (First_Prag : Node_Id); + -- Save all global references in contract-related source pragmas found + -- in the list, starting with pragma First_Prag. + + ------------------------------------ + -- Save_Global_References_In_List -- + ------------------------------------ + + procedure Save_Global_References_In_List (First_Prag : Node_Id) is + Prag : Node_Id := First_Prag; + + begin + while Present (Prag) loop + if Is_Generic_Contract_Pragma (Prag) then + Save_Global_References (Prag); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end Save_Global_References_In_List; + + -- Local variables + + Items : constant Node_Id := Contract (Defining_Entity (Templ)); + + -- Start of processing for Save_Global_References_In_Contract + + begin + -- The entity of the analyzed generic copy must be on the scope stack + -- to ensure proper detection of global references. + + Push_Scope (Gen_Id); + + if Permits_Aspect_Specifications (Templ) + and then Has_Aspects (Templ) + then + Save_Global_References_In_Aspects (Templ); + end if; + + if Present (Items) then + Save_Global_References_In_List (Pre_Post_Conditions (Items)); + Save_Global_References_In_List (Contract_Test_Cases (Items)); + Save_Global_References_In_List (Classifications (Items)); + end if; + + Pop_Scope; + end Save_Global_References_In_Contract; + + ------------------------- + -- Set_Class_Condition -- + ------------------------- + + procedure Set_Class_Condition + (Kind : Condition_Kind; + Subp : Entity_Id; + Cond : Node_Id) + is + begin + case Kind is + when Class_Postcondition => + Set_Class_Postconditions (Subp, Cond); + + when Class_Precondition => + Set_Class_Preconditions (Subp, Cond); + + when Ignored_Class_Postcondition => + Set_Ignored_Class_Postconditions (Subp, Cond); + + when Ignored_Class_Precondition => + Set_Ignored_Class_Preconditions (Subp, Cond); + end case; + end Set_Class_Condition; end Contracts; diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index bfd482e3053..eb26ebf1332 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); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 94c56624fef..f890fe54230 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -610,12 +610,23 @@ package Einfo is -- tables must be consulted to determine if there actually is an active -- Suppress or Unsuppress pragma that applies to the entity. --- Class_Wide_Clone --- Defined on subprogram entities. Set if the subprogram has a class-wide --- pre- or postcondition, and the expression contains calls to other --- primitive funtions of the type. Used to implement properly the --- semantics of inherited operations whose class-wide condition may --- be different from that of the ancestor (See AI012-0195). +-- Class_Postconditions +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- postconditions. Denotes the (and-then) expression built by merging +-- inherited class-wide postconditions with its own class-wide +-- postconditions. + +-- Class_Preconditions +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- preconditions. Denotes the (or-else) expression built by merging +-- inherited class-wide preconditions with its own class-wide +-- preconditions. + +-- Class_Preconditions_Subprogram +-- Defined on subprogram entities. Set on subprogram helpers and also on +-- the indirect-call wrapper internally built for subprograms that have +-- class-wide preconditions. References the subprogram that has the +-- class-wide preconditions. -- Class_Wide_Type -- Defined in all type entities. For a tagged type or subtype, returns @@ -1029,6 +1040,11 @@ package Einfo is -- associated with the tagged type. For an untagged record, contains -- No_Elist. +-- Dynamic_Call_Helper +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- preconditions. Denotes the helper that evaluates at run time the +-- class-wide preconditions performing dispatching calls. + -- DTC_Entity -- Defined in function and procedure entities. Set to Empty unless -- the subprogram is dispatching in which case it references the @@ -2182,6 +2198,18 @@ package Einfo is -- "off" and indicates that all SPARK_Mode pragmas found within must -- be ignored. +-- Ignored_Class_Postconditions +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- postconditions. Denotes the (and-then) expression built by merging +-- inherited ignored class-wide postconditions with its own ignored +-- class-wide postconditions. + +-- Ignored_Class_Preconditions +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- preconditions. Denotes the (or-else) expression built by merging +-- inherited ignored class-wide preconditions with its own ignored +-- class-wide preconditions. + -- Implementation_Base_Type (synthesized) -- Applies to all entities. For types, similar to Base_Type, but never -- returns a private type when applied to a non-private type. Instead in @@ -2216,6 +2244,12 @@ package Einfo is -- is relocated to the corresponding package body, which must have a -- corresponding nonlimited with_clause. +-- Indirect_Call_Wrapper +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- preconditions. Denotes the internal wrapper that checks preconditions +-- and invokes the subprogram body. Subp'Access points to the indirect +-- call wrapper if available. + -- Initialization_Statements -- Defined in constants and variables. For a composite object initialized -- with an aggregate that has been converted to a sequence of @@ -2507,6 +2541,11 @@ package Einfo is -- Applies to all entities. Set to indicate to the backend that this -- entity is associated with a dispatch table. +-- Is_Dispatch_Table_Wrapper +-- Applies to all entities. Set on wrappers built when the subprogram has +-- class-wide preconditions or class-wide postconditions affected by +-- overriding (AI12-0195). + -- Is_Dispatching_Operation -- Defined in all entities. Set for procedures, functions, generic -- procedures, and generic functions if the corresponding operation @@ -4401,6 +4440,11 @@ package Einfo is -- Default_Scalar_Storage_Order (High_Order_First) was active at the time -- the record or array was declared and therefore applies to it. +-- Static_Call_Helper +-- Defined on subprogram entities. Set if the subprogram has class-wide +-- preconditions. Denotes the helper that evaluates at runtime the +-- class-wide preconditions performing static calls. + -- Static_Discrete_Predicate -- Defined in discrete types/subtypes with static predicates (with the -- two flags Has_Predicates and Has_Static_Predicate set). Set if the @@ -4878,6 +4922,7 @@ package Einfo is -- Is_Discrim_SO_Function -- Is_Discriminant_Check_Function -- Is_Dispatch_Table_Entity + -- Is_Dispatch_Table_Wrapper -- Is_Dispatching_Operation -- Is_Entry_Formal -- Is_Exported @@ -5484,7 +5529,14 @@ package Einfo is -- Linker_Section_Pragma -- Contract -- Import_Pragma (non-generic case only) - -- Class_Wide_Clone + -- Class_Postconditions + -- Class_Preconditions + -- Class_Preconditions_Subprogram + -- Dynamic_Call_Helper + -- Ignored_Class_Preconditions + -- Ignored_Class_Postconditions + -- Indirect_Call_Wrapper + -- Static_Call_Helper -- Protected_Subprogram (non-generic case only) -- SPARK_Pragma -- Original_Protected_Subprogram @@ -5840,7 +5892,14 @@ package Einfo is -- Linker_Section_Pragma -- Contract -- Import_Pragma (non-generic case only) - -- Class_Wide_Clone + -- Class_Postconditions + -- Class_Preconditions + -- Class_Preconditions_Subprogram + -- Dynamic_Call_Helper + -- Ignored_Class_Preconditions + -- Ignored_Class_Postconditions + -- Indirect_Call_Wrapper + -- Static_Call_Helper -- Protected_Subprogram (non-generic case only) -- SPARK_Pragma -- Original_Protected_Subprogram diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index c962c2a8516..3e7bb838118 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -2216,6 +2216,20 @@ package body Exp_Attr is if Is_Access_Protected_Subprogram_Type (Btyp) then Expand_Access_To_Protected_Op (N, Pref, Typ); + -- If prefix is a subprogram that has class-wide preconditions and + -- an indirect-call wrapper (ICW) of such subprogram is available + -- then replace the prefix by the ICW. + + elsif Is_Access_Subprogram_Type (Btyp) + and then Is_Entity_Name (Pref) + and then Present (Class_Preconditions (Entity (Pref))) + and then Present (Indirect_Call_Wrapper (Entity (Pref))) + then + Rewrite (Pref, + New_Occurrence_Of + (Indirect_Call_Wrapper (Entity (Pref)), Loc)); + Analyze_And_Resolve (N, Typ); + -- If prefix is a type name, this is a reference to the current -- instance of the type, within its initialization procedure. diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 45d5baf51b4..418306f3040 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -26,6 +26,7 @@ with Aspects; use Aspects; with Atree; use Atree; with Checks; use Checks; +with Contracts; use Contracts; with Einfo; use Einfo; with Einfo.Entities; use Einfo.Entities; with Einfo.Utils; use Einfo.Utils; @@ -5352,10 +5353,66 @@ package body Exp_Ch3 is ------------------------------- procedure Expand_Freeze_Record_Type (N : Node_Id) is + + procedure Build_Class_Condition_Subprograms (Typ : Entity_Id); + -- Create internal subprograms of Typ primitives that have class-wide + -- preconditions or postconditions; they are invoked by the caller to + -- evaluate the conditions. + procedure Build_Variant_Record_Equality (Typ : Entity_Id); -- Create An Equality function for the untagged variant record Typ and -- attach it to the TSS list. + procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id); + -- Register dispatch-table wrappers in the dispatch table of Typ + + --------------------------------------- + -- Build_Class_Condition_Subprograms -- + --------------------------------------- + + procedure Build_Class_Condition_Subprograms (Typ : Entity_Id) is + Prim_List : constant Elist_Id := Primitive_Operations (Typ); + Prim_Elmt : Elmt_Id := First_Elmt (Prim_List); + Prim : Entity_Id; + + begin + while Present (Prim_Elmt) loop + Prim := Node (Prim_Elmt); + + -- Primitive with class-wide preconditions + + if Comes_From_Source (Prim) + and then Has_Significant_Contract (Prim) + and then + (Present (Class_Preconditions (Prim)) + or else Present (Ignored_Class_Preconditions (Prim))) + then + if Expander_Active then + Make_Class_Precondition_Subps (Prim); + end if; + + -- Wrapper of a primitive that has or inherits class-wide + -- preconditions. + + elsif Is_Primitive_Wrapper (Prim) + and then + (Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Prim, + Kind => Class_Precondition)) + or else + Present (Nearest_Class_Condition_Subprogram + (Spec_Id => Prim, + Kind => Ignored_Class_Precondition))) + then + if Expander_Active then + Make_Class_Precondition_Subps (Prim); + end if; + end if; + + Next_Elmt (Prim_Elmt); + end loop; + end Build_Class_Condition_Subprograms; + ----------------------------------- -- Build_Variant_Record_Equality -- ----------------------------------- @@ -5417,6 +5474,27 @@ package body Exp_Ch3 is end if; end Build_Variant_Record_Equality; + -------------------------------------- + -- Register_Dispatch_Table_Wrappers -- + -------------------------------------- + + procedure Register_Dispatch_Table_Wrappers (Typ : Entity_Id) is + Elmt : Elmt_Id := First_Elmt (Primitive_Operations (Typ)); + Subp : Entity_Id; + + begin + while Present (Elmt) loop + Subp := Node (Elmt); + + if Is_Dispatch_Table_Wrapper (Subp) then + Append_Freeze_Actions (Typ, + Register_Primitive (Sloc (Subp), Subp)); + end if; + + Next_Elmt (Elmt); + end loop; + end Register_Dispatch_Table_Wrappers; + -- Local variables Typ : constant Node_Id := Entity (N); @@ -5666,6 +5744,13 @@ package body Exp_Ch3 is if not Building_Static_DT (Typ) then Append_Freeze_Actions (Typ, Make_DT (Typ)); + + -- Register dispatch table wrappers in the dispatch table. + -- It could not be done when these wrappers were built + -- because, at that stage, the dispatch table was not + -- available. + + Register_Dispatch_Table_Wrappers (Typ); end if; end if; @@ -5857,6 +5942,13 @@ package body Exp_Ch3 is end loop; end; end if; + + -- Build internal subprograms of primitives with class-wide + -- pre/postconditions. + + if Is_Tagged_Type (Typ) then + Build_Class_Condition_Subprograms (Typ); + end if; end Expand_Freeze_Record_Type; ------------------------------------ diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 7717fa7c0ab..ffd14759a7f 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -73,8 +73,10 @@ with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; with Sinfo.Utils; use Sinfo.Utils; +with Sinput; use Sinput; with Snames; use Snames; with Stand; use Stand; +with Stringt; use Stringt; with Tbuild; use Tbuild; with Uintp; use Uintp; with Validsw; use Validsw; @@ -4065,7 +4067,7 @@ package body Exp_Ch6 is end; end if; - -- If the formal is class wide and the actual is an aggregate, force + -- If the formal is class-wide and the actual is an aggregate, force -- evaluation so that the back end who does not know about class-wide -- type, does not generate a temporary of the wrong size. @@ -4250,6 +4252,16 @@ package body Exp_Ch6 is Expand_Interface_Actuals (Call_Node); end if; + -- Install class-wide preconditions runtime check when this is a + -- dispatching primitive that has or inherits class-wide preconditions; + -- otherwise no runtime check is installed. + + if Nkind (Call_Node) in N_Subprogram_Call + and then Is_Dispatching_Operation (Subp) + then + Install_Class_Preconditions_Check (Call_Node); + end if; + -- Deals with Dispatch_Call if we still have a call, before expanding -- extra actuals since this will be done on the re-analysis of the -- dispatching call. Note that we do not try to shorten the actual list @@ -7855,18 +7867,6 @@ package body Exp_Ch6 is -- returned type may not be known yet (for private types). Compute_Returns_By_Ref (Subp); - - -- When freezing a null procedure, analyze its delayed aspects now - -- because we may not have reached the end of the declarative list when - -- delayed aspects are normally analyzed. This ensures that dispatching - -- calls are properly rewritten when the generated _Postcondition - -- procedure is analyzed in the null procedure body. - - if Nkind (Parent (Subp)) = N_Procedure_Specification - and then Null_Present (Parent (Subp)) - then - Analyze_Entry_Or_Subprogram_Contract (Subp); - end if; end Freeze_Subprogram; -------------------------- @@ -8101,6 +8101,367 @@ package body Exp_Ch6 is end if; end Insert_Post_Call_Actions; + --------------------------------------- + -- Install_Class_Preconditions_Check -- + --------------------------------------- + + procedure Install_Class_Preconditions_Check (Call_Node : Node_Id) is + Loc : constant Source_Ptr := Sloc (Call_Node); + + function Build_Dynamic_Check_Helper_Call return Node_Id; + -- Build call to the helper runtime function of the nearest ancestor + -- of the target subprogram that dynamically evaluates the merged + -- or-else preconditions. + + function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id; + -- Build message associated with the class-wide precondition of Subp_Id + -- indicating the call that caused it. + + function Build_Static_Check_Helper_Call return Node_Id; + -- Build call to the helper runtime function of the nearest ancestor + -- of the target subprogram that dynamically evaluates the merged + -- or-else preconditions. + + function Class_Preconditions_Subprogram + (Spec_Id : Entity_Id; + Dynamic : Boolean) return Node_Id; + -- Return the nearest ancestor of Spec_Id defining a helper function + -- that evaluates a combined or-else expression containing all the + -- inherited class-wide preconditions; Dynamic enables searching for + -- the helper that dynamically evaluates preconditions using dispatching + -- calls; if False it searches for the helper that statically evaluates + -- preconditions; return Empty when not available (which means that no + -- preconditions check is required). + + ------------------------------------- + -- Build_Dynamic_Check_Helper_Call -- + ------------------------------------- + + function Build_Dynamic_Check_Helper_Call return Node_Id is + Spec_Id : constant Entity_Id := Entity (Name (Call_Node)); + CW_Subp : constant Entity_Id := + Class_Preconditions_Subprogram (Spec_Id, + Dynamic => True); + Helper_Id : constant Entity_Id := + Dynamic_Call_Helper (CW_Subp); + Actuals : constant List_Id := New_List; + A : Node_Id := First_Actual (Call_Node); + F : Entity_Id := First_Formal (Helper_Id); + + begin + while Present (A) loop + + -- Ensure that the evaluation of the actuals will not produce + -- side effects. + + Remove_Side_Effects (A); + + Append_To (Actuals, New_Copy_Tree (A)); + Next_Formal (F); + Next_Actual (A); + end loop; + + return + Make_Function_Call (Loc, + Name => New_Occurrence_Of (Helper_Id, Loc), + Parameter_Associations => Actuals); + end Build_Dynamic_Check_Helper_Call; + + ------------------------- + -- Build_Error_Message -- + ------------------------- + + function Build_Error_Message (Subp_Id : Entity_Id) return Node_Id is + + procedure Append_Message + (Id : Entity_Id; + Is_First : in out Boolean); + -- Build the fragment of the message associated with subprogram Id; + -- Is_First facilitates identifying continuation messages. + + -------------------- + -- Append_Message -- + -------------------- + + procedure Append_Message + (Id : Entity_Id; + Is_First : in out Boolean) + is + Prag : constant Node_Id := Get_Class_Wide_Pragma (Id, + Pragma_Precondition); + Msg : Node_Id; + Str_Id : String_Id; + + begin + if No (Prag) or else Is_Ignored (Prag) then + return; + end if; + + Msg := Expression (Last (Pragma_Argument_Associations (Prag))); + Str_Id := Strval (Msg); + + if Is_First then + Is_First := False; + + Append (Global_Name_Buffer, Strval (Msg)); + + if Id /= Subp_Id + and then Name_Buffer (1 .. 19) = "failed precondition" + then + Insert_Str_In_Name_Buffer ("inherited ", 8); + end if; + + else + declare + Str : constant String := To_String (Str_Id); + From_Idx : Integer; + + begin + Append (Global_Name_Buffer, ASCII.LF); + Append (Global_Name_Buffer, " or "); + + From_Idx := Name_Len; + Append (Global_Name_Buffer, Str_Id); + + if Str (1 .. 19) = "failed precondition" then + Insert_Str_In_Name_Buffer ("inherited ", From_Idx + 8); + end if; + end; + end if; + end Append_Message; + + -- Local variables + + Str_Loc : constant String := Build_Location_String (Loc); + Subps : constant Subprogram_List := + Inherited_Subprograms (Subp_Id); + Is_First : Boolean := True; + + -- Start of processing for Build_Error_Message + + begin + Name_Len := 0; + Append_Message (Subp_Id, Is_First); + + for Index in Subps'Range loop + Append_Message (Subps (Index), Is_First); + end loop; + + if Present (Controlling_Argument (Call_Node)) then + Append (Global_Name_Buffer, " in dispatching call at "); + else + Append (Global_Name_Buffer, " in call at "); + end if; + + Append (Global_Name_Buffer, Str_Loc); + + return Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len)); + end Build_Error_Message; + + ------------------------------------ + -- Build_Static_Check_Helper_Call -- + ------------------------------------ + + function Build_Static_Check_Helper_Call return Node_Id is + Actuals : constant List_Id := New_List; + A : Node_Id; + Helper_Id : Entity_Id; + F : Entity_Id; + CW_Subp : Entity_Id; + Spec_Id : constant Entity_Id := Entity (Name (Call_Node)); + + begin + -- The target is the wrapper built to support inheriting body but + -- overriding pre/postconditions (AI12-0195). + + if Is_Dispatch_Table_Wrapper (Spec_Id) then + CW_Subp := Spec_Id; + + -- Common case + + else + CW_Subp := Class_Preconditions_Subprogram (Spec_Id, + Dynamic => False); + end if; + + Helper_Id := Static_Call_Helper (CW_Subp); + + F := First_Formal (Helper_Id); + A := First_Actual (Call_Node); + while Present (A) loop + + -- Ensure that the evaluation of the actuals will not produce + -- side effects. + + Remove_Side_Effects (A); + + if Is_Controlling_Actual (A) + and then Etype (F) /= Etype (A) + then + Append_To (Actuals, + Make_Unchecked_Type_Conversion (Loc, + New_Occurrence_Of (Etype (F), Loc), + New_Copy_Tree (A))); + else + Append_To (Actuals, New_Copy_Tree (A)); + end if; + + Next_Formal (F); + Next_Actual (A); + end loop; + + return + Make_Function_Call (Loc, + Name => New_Occurrence_Of (Helper_Id, Loc), + Parameter_Associations => Actuals); + end Build_Static_Check_Helper_Call; + + ------------------------------------ + -- Class_Preconditions_Subprogram -- + ------------------------------------ + + function Class_Preconditions_Subprogram + (Spec_Id : Entity_Id; + Dynamic : Boolean) return Node_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 the helper we are + -- searching + + elsif Dynamic then + if Present (Dynamic_Call_Helper (Subp_Id)) then + return Subp_Id; + end if; + else + if Present (Static_Call_Helper (Subp_Id)) then + return Subp_Id; + end if; + end if; + + -- Process inherited subprograms looking for class-wide + -- preconditions. + + 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 Dynamic then + if Present (Dynamic_Call_Helper (Subp_Id)) then + return Subp_Id; + end if; + else + if Present (Static_Call_Helper (Subp_Id)) then + return Subp_Id; + end if; + end if; + end loop; + end; + + return Empty; + end Class_Preconditions_Subprogram; + + -- Local variables + + Dynamic_Check : constant Boolean := + Present (Controlling_Argument (Call_Node)); + Class_Subp : Entity_Id; + Cond : Node_Id; + Subp : Entity_Id; + + -- Start of processing for Install_Class_Preconditions_Check + + begin + -- Do not expand the check if we are compiling under restriction + -- No_Dispatching_Calls; the semantic analyzer has previously + -- notified the violation of this restriction. + + if Dynamic_Check + and then Restriction_Active (No_Dispatching_Calls) + then + return; + + -- Class-wide precondition check not needed in interface thunks since + -- they are installed in the dispatching call that caused invoking the + -- thunk. + + elsif Is_Thunk (Current_Scope) then + return; + end if; + + Subp := Entity (Name (Call_Node)); + + -- No check needed for this subprogram call if no class-wide + -- preconditions apply (or if the unique available preconditions + -- are ignored preconditions). + + Class_Subp := Class_Preconditions_Subprogram (Subp, Dynamic_Check); + + if No (Class_Subp) + or else No (Class_Preconditions (Class_Subp)) + then + return; + end if; + + -- Build and install the check + + if Dynamic_Check then + Cond := Build_Dynamic_Check_Helper_Call; + else + Cond := Build_Static_Check_Helper_Call; + end if; + + if Exception_Locations_Suppressed then + Insert_Action (Call_Node, + Make_If_Statement (Loc, + Condition => Make_Op_Not (Loc, Cond), + Then_Statements => New_List ( + Make_Raise_Statement (Loc, + Name => + New_Occurrence_Of + (RTE (RE_Assert_Failure), Loc))))); + + -- Failed check with message indicating the failed precondition and the + -- call that caused it. + + else + Insert_Action (Call_Node, + Make_If_Statement (Loc, + Condition => Make_Op_Not (Loc, Cond), + Then_Statements => New_List ( + Make_Procedure_Call_Statement (Loc, + Name => + New_Occurrence_Of + (RTE (RE_Raise_Assert_Failure), Loc), + Parameter_Associations => + New_List (Build_Error_Message (Subp)))))); + end if; + end Install_Class_Preconditions_Check; + ----------------------------------- -- Is_Build_In_Place_Result_Type -- ----------------------------------- diff --git a/gcc/ada/exp_ch6.ads b/gcc/ada/exp_ch6.ads index 76cec4d4e47..196f7e6d941 100644 --- a/gcc/ada/exp_ch6.ads +++ b/gcc/ada/exp_ch6.ads @@ -121,6 +121,9 @@ package Exp_Ch6 is -- The returned node is the root of the procedure body which will replace -- the original function body, which is not needed for the C program. + procedure Install_Class_Preconditions_Check (Call_Node : Node_Id); + -- Install check of class-wide preconditions on the caller. + function Is_Build_In_Place_Entity (E : Entity_Id) return Boolean; -- Ada 2005 (AI-318-02): Returns True if E is a BIP entity. diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 7cce41b234e..72f4e7c90b7 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -63,7 +63,6 @@ with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinfo.Nodes; use Sinfo.Nodes; with Sinfo.Utils; use Sinfo.Utils; -with Sinput; use Sinput; with Snames; use Snames; with Stand; use Stand; with Stringt; use Stringt; @@ -697,233 +696,11 @@ package body Exp_Disp is Eq_Prim_Op : Entity_Id := Empty; Controlling_Tag : Node_Id; - procedure Build_Class_Wide_Check (E : Entity_Id); - -- If the denoted subprogram has a class-wide precondition, generate a - -- check using that precondition before the dispatching call, because - -- this is the only class-wide precondition that applies to the call; - -- otherwise climb to the ancestors searching for the enclosing - -- overridden primitive of E that has a class-wide precondition (and - -- use it to generate the check). - function New_Value (From : Node_Id) return Node_Id; -- From is the original Expression. New_Value is equivalent to a call -- to Duplicate_Subexpr with an explicit dereference when From is an -- access parameter. - ---------------------------- - -- Build_Class_Wide_Check -- - ---------------------------- - - procedure Build_Class_Wide_Check (E : Entity_Id) is - Subp : Entity_Id := E; - - function Has_Class_Wide_Precondition - (Subp : Entity_Id) return Boolean; - -- Evaluates if the dispatching subprogram Subp has a class-wide - -- precondition. - - function Replace_Formals (N : Node_Id) return Traverse_Result; - -- Replace occurrences of the formals of the subprogram by the - -- corresponding actuals in the call, given that this check is - -- performed outside of the body of the subprogram. - - -- If the dispatching call appears in the same scope as the - -- declaration of the dispatching subprogram (for example in - -- the expression of a local expression function), the spec - -- has not been analyzed yet, in which case we use the Chars - -- field to recognize intended occurrences of the formals. - - --------------------------------- - -- Has_Class_Wide_Precondition -- - --------------------------------- - - function Has_Class_Wide_Precondition - (Subp : Entity_Id) return Boolean - is - Prec : Node_Id := Empty; - - begin - if Present (Contract (Subp)) - and then Present (Pre_Post_Conditions (Contract (Subp))) - then - Prec := Pre_Post_Conditions (Contract (Subp)); - - while Present (Prec) loop - exit when Pragma_Name (Prec) = Name_Precondition - and then Class_Present (Prec); - Prec := Next_Pragma (Prec); - end loop; - end if; - - return Present (Prec) - and then not Is_Ignored (Prec); - end Has_Class_Wide_Precondition; - - --------------------- - -- Replace_Formals -- - --------------------- - - function Replace_Formals (N : Node_Id) return Traverse_Result is - A : Node_Id; - F : Entity_Id; - begin - if Is_Entity_Name (N) then - F := First_Formal (Subp); - A := First_Actual (Call_Node); - - if Present (Entity (N)) and then Is_Formal (Entity (N)) then - while Present (F) loop - if F = Entity (N) then - if not Is_Controlling_Actual (N) then - Rewrite (N, New_Copy_Tree (A)); - - -- If the formal is class-wide, and thus not a - -- controlling argument, preserve its type because - -- it may appear in a nested call with a class-wide - -- parameter. - - if Is_Class_Wide_Type (Etype (F)) then - Set_Etype (N, Etype (F)); - - -- Conversely, if this is a controlling argument - -- (in a dispatching call in the condition) that - -- is a dereference, the source is an access-to- - -- -class-wide type, so preserve the dispatching - -- nature of the call in the rewritten condition. - - elsif Nkind (Parent (N)) = N_Explicit_Dereference - and then Is_Controlling_Actual (Parent (N)) - then - Set_Controlling_Argument (Parent (Parent (N)), - Parent (N)); - end if; - - -- Ensure that the type of the controlling actual - -- matches the type of the controlling formal of the - -- parent primitive Subp defining the class-wide - -- precondition. - - elsif Is_Class_Wide_Type (Etype (A)) then - Rewrite (N, - Convert_To - (Class_Wide_Type (Etype (F)), - New_Copy_Tree (A))); - - else - Rewrite (N, - Convert_To - (Etype (F), - New_Copy_Tree (A))); - end if; - - exit; - end if; - - Next_Formal (F); - Next_Actual (A); - end loop; - - -- If the node is not analyzed, recognize occurrences of a - -- formal by name, as would be done when resolving the aspect - -- expression in the context of the subprogram. - - elsif not Analyzed (N) - and then Nkind (N) = N_Identifier - and then No (Entity (N)) - then - while Present (F) loop - if Chars (N) = Chars (F) then - Rewrite (N, New_Copy_Tree (A)); - return Skip; - end if; - - Next_Formal (F); - Next_Actual (A); - end loop; - end if; - end if; - - return OK; - end Replace_Formals; - - procedure Update is new Traverse_Proc (Replace_Formals); - - -- Local variables - - Str_Loc : constant String := Build_Location_String (Loc); - - A : Node_Id; - Cond : Node_Id; - Msg : Node_Id; - Prec : Node_Id; - - -- Start of processing for Build_Class_Wide_Check - - begin - -- Climb searching for the enclosing class-wide precondition - - while not Has_Class_Wide_Precondition (Subp) - and then Present (Overridden_Operation (Subp)) - loop - Subp := Overridden_Operation (Subp); - end loop; - - -- Locate class-wide precondition, if any - - if Present (Contract (Subp)) - and then Present (Pre_Post_Conditions (Contract (Subp))) - then - Prec := Pre_Post_Conditions (Contract (Subp)); - - while Present (Prec) loop - exit when Pragma_Name (Prec) = Name_Precondition - and then Class_Present (Prec); - Prec := Next_Pragma (Prec); - end loop; - - if No (Prec) or else Is_Ignored (Prec) then - return; - end if; - - -- Ensure that the evaluation of the actuals will not produce side - -- effects (since the check will use a copy of the actuals). - - A := First_Actual (Call_Node); - while Present (A) loop - Remove_Side_Effects (A); - Next_Actual (A); - end loop; - - -- The expression for the precondition is analyzed within the - -- generated pragma. The message text is the last parameter of - -- the generated pragma, indicating source of precondition. - - Cond := - New_Copy_Tree - (Expression (First (Pragma_Argument_Associations (Prec)))); - Update (Cond); - - -- Build message indicating the failed precondition and the - -- dispatching call that caused it. - - Msg := Expression (Last (Pragma_Argument_Associations (Prec))); - Name_Len := 0; - Append (Global_Name_Buffer, Strval (Msg)); - Append (Global_Name_Buffer, " in dispatching call at "); - Append (Global_Name_Buffer, Str_Loc); - Msg := Make_String_Literal (Loc, Name_Buffer (1 .. Name_Len)); - - Insert_Action (Call_Node, - Make_If_Statement (Loc, - Condition => Make_Op_Not (Loc, Cond), - Then_Statements => New_List ( - Make_Procedure_Call_Statement (Loc, - Name => - New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc), - Parameter_Associations => New_List (Msg))))); - end if; - end Build_Class_Wide_Check; - --------------- -- New_Value -- --------------- @@ -984,8 +761,6 @@ package body Exp_Disp is Subp := Alias (Subp); end if; - Build_Class_Wide_Check (Subp); - -- Definition of the class-wide type and the tagged type -- If the controlling argument is itself a tag rather than a tagged diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 807afb2c580..7c366663dcb 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1270,11 +1270,10 @@ package body Exp_Util is --------------------------------- procedure Build_Class_Wide_Expression - (Prag : Node_Id; - Subp : Entity_Id; - Par_Subp : Entity_Id; - Adjust_Sloc : Boolean; - Needs_Wrapper : out Boolean) + (Pragma_Or_Expr : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id; + Adjust_Sloc : Boolean) is function Replace_Entity (N : Node_Id) return Traverse_Result; -- Replace reference to formal of inherited operation or to primitive @@ -1319,84 +1318,6 @@ package body Exp_Util is if Present (New_E) then Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); - - -- AI12-0166: a precondition for a protected operation - -- cannot include an internal call to a protected function - -- of the type. In the case of an inherited condition for an - -- overriding operation, both the operation and the function - -- are given by primitive wrappers. - -- Move this check to sem??? - - if Ekind (New_E) = E_Function - and then Is_Primitive_Wrapper (New_E) - and then Is_Primitive_Wrapper (Subp) - and then Scope (Subp) = Scope (New_E) - and then Chars (Pragma_Identifier (Prag)) = Name_Precondition - then - Error_Msg_Node_2 := Wrapped_Entity (Subp); - Error_Msg_NE - ("internal call to& cannot appear in inherited " - & "precondition of protected operation&", - N, Wrapped_Entity (New_E)); - end if; - - -- If the entity is an overridden primitive and we are not - -- in GNATprove mode, we must build a wrapper for the current - -- inherited operation. If the reference is the prefix of an - -- attribute such as 'Result (or others ???) there is no need - -- for a wrapper: the condition is just rewritten in terms of - -- the inherited subprogram. - - if Is_Subprogram (New_E) - and then Nkind (Parent (N)) /= N_Attribute_Reference - and then not GNATprove_Mode - then - Needs_Wrapper := True; - end if; - end if; - - -- Check that there are no calls left to abstract operations if - -- the current subprogram is not abstract. - -- Move this check to sem??? - - if Nkind (Parent (N)) = N_Function_Call - and then N = Name (Parent (N)) - then - if not Is_Abstract_Subprogram (Subp) - and then Is_Abstract_Subprogram (Entity (N)) - then - Error_Msg_Sloc := Sloc (Current_Scope); - Error_Msg_Node_2 := Subp; - if Comes_From_Source (Subp) then - Error_Msg_NE - ("cannot call abstract subprogram & in inherited " - & "condition for&#", Subp, Entity (N)); - else - Error_Msg_NE - ("cannot call abstract subprogram & in inherited " - & "condition for inherited&#", Subp, Entity (N)); - end if; - - -- In SPARK mode, reject an inherited condition for an - -- inherited operation if it contains a call to an overriding - -- operation, because this implies that the pre/postconditions - -- of the inherited operation have changed silently. - - elsif SPARK_Mode = On - and then Warn_On_Suspicious_Contract - and then Present (Alias (Subp)) - and then Present (New_E) - and then Comes_From_Source (New_E) - then - Error_Msg_N - ("cannot modify inherited condition (SPARK RM 6.1.1(1))", - Parent (Subp)); - Error_Msg_Sloc := Sloc (New_E); - Error_Msg_Node_2 := Subp; - Error_Msg_NE - ("\overriding of&# forces overriding of&", - Parent (Subp), New_E); - end if; end if; -- Update type of function call node, which should be the same as @@ -1422,26 +1343,17 @@ package body Exp_Util is -- Local variables - Par_Formal : Entity_Id; - Subp_Formal : Entity_Id; + Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Subp); + Subp_Typ : constant Entity_Id := Find_Dispatching_Type (Subp); -- Start of processing for Build_Class_Wide_Expression begin - Needs_Wrapper := False; - - -- Add mapping from old formals to new formals + pragma Assert (Par_Typ /= Subp_Typ); - Par_Formal := First_Formal (Par_Subp); - Subp_Formal := First_Formal (Subp); - - while Present (Par_Formal) and then Present (Subp_Formal) loop - Type_Map.Set (Par_Formal, Subp_Formal); - Next_Formal (Par_Formal); - Next_Formal (Subp_Formal); - end loop; - - Replace_Condition_Entities (Prag); + Update_Primitives_Mapping (Par_Subp, Subp); + Map_Formals (Par_Subp, Subp); + Replace_Condition_Entities (Pragma_Or_Expr); end Build_Class_Wide_Expression; -------------------- @@ -1895,7 +1807,33 @@ package body Exp_Util is Priv_Typ : Entity_Id; -- The partial view of Par_Typ + Op_Node : Elmt_Id; + Par_Prim : Entity_Id; + Prim : Entity_Id; + begin + -- Map the overridden primitive to the overriding one; required by + -- Replace_References (called by Add_Inherited_DICs) to handle calls + -- to parent primitives. + + Op_Node := First_Elmt (Primitive_Operations (T)); + while Present (Op_Node) loop + Prim := Node (Op_Node); + + if Present (Overridden_Operation (Prim)) + and then Comes_From_Source (Prim) + then + Par_Prim := Overridden_Operation (Prim); + + -- Create a mapping of the form: + -- parent type primitive -> derived type primitive + + Type_Map.Set (Par_Prim, Prim); + end if; + + Next_Elmt (Op_Node); + end loop; + -- Climb the parent type chain Curr_Typ := T; @@ -7073,6 +7011,15 @@ package body Exp_Util is return Etype (Indx); end Get_Index_Subtype; + ----------------------- + -- Get_Mapped_Entity -- + ----------------------- + + function Get_Mapped_Entity (E : Entity_Id) return Entity_Id is + begin + return Type_Map.Get (E); + end Get_Mapped_Entity; + --------------------- -- Get_Stream_Size -- --------------------- @@ -10350,6 +10297,36 @@ package body Exp_Util is end if; end Make_Variant_Comparison; + ----------------- + -- Map_Formals -- + ----------------- + + procedure Map_Formals + (Parent_Subp : Entity_Id; + Derived_Subp : Entity_Id; + Force_Update : Boolean := False) + is + Par_Formal : Entity_Id := First_Formal (Parent_Subp); + Subp_Formal : Entity_Id := First_Formal (Derived_Subp); + + begin + if Force_Update then + Type_Map.Set (Parent_Subp, Derived_Subp); + end if; + + -- At this stage either we are under regular processing and the caller + -- has previously ensured that these primitives are already mapped (by + -- means of calling previously to Update_Primitives_Mapping), or we are + -- processing a late-overriding primitive and Force_Update updated above + -- the mapping of these primitives. + + while Present (Par_Formal) and then Present (Subp_Formal) loop + Type_Map.Set (Par_Formal, Subp_Formal); + Next_Formal (Par_Formal); + Next_Formal (Subp_Formal); + end loop; + end Map_Formals; + --------------- -- Map_Types -- --------------- @@ -10861,7 +10838,7 @@ package body Exp_Util is -- they relate to the primitives of the parent type. If there is a -- meaningful relation, create a mapping of the form: - -- parent type primitive -> perived type primitive + -- parent type primitive -> derived type primitive if Present (Direct_Primitive_Operations (Deriv_Typ)) then Prim_Elmt := First_Elmt (Direct_Primitive_Operations (Deriv_Typ)); @@ -14123,10 +14100,12 @@ package body Exp_Util is (Inher_Id : Entity_Id; Subp_Id : Entity_Id) is + Parent_Type : constant Entity_Id := Find_Dispatching_Type (Inher_Id); + Derived_Type : constant Entity_Id := Find_Dispatching_Type (Subp_Id); + begin - Map_Types - (Parent_Type => Find_Dispatching_Type (Inher_Id), - Derived_Type => Find_Dispatching_Type (Subp_Id)); + pragma Assert (Parent_Type /= Derived_Type); + Map_Types (Parent_Type, Derived_Type); end Update_Primitives_Mapping; ---------------------------------- diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index 56ff61f489b..eddf314c932 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; diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 5b7607d051d..5f81d9efbda 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -35,6 +35,7 @@ with Elists; use Elists; with Errout; use Errout; with Exp_Ch3; use Exp_Ch3; with Exp_Ch7; use Exp_Ch7; +with Exp_Disp; use Exp_Disp; with Exp_Pakd; use Exp_Pakd; with Exp_Util; use Exp_Util; with Exp_Tss; use Exp_Tss; @@ -56,6 +57,7 @@ with Sem_Ch6; use Sem_Ch6; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; with Sem_Ch13; use Sem_Ch13; +with Sem_Disp; use Sem_Disp; with Sem_Eval; use Sem_Eval; with Sem_Mech; use Sem_Mech; with Sem_Prag; use Sem_Prag; @@ -132,11 +134,6 @@ package body Freeze is -- Attribute references to outer types are freeze points for those types; -- this routine generates the required freeze nodes for them. - procedure Check_Inherited_Conditions (R : Entity_Id); - -- For a tagged derived type, create wrappers for inherited operations - -- that have a class-wide condition, so it can be properly rewritten if - -- it involves calls to other overriding primitives. - procedure Check_Strict_Alignment (E : Entity_Id); -- E is a base type. If E is tagged or has a component that is aliased -- or tagged or contains something this is aliased or tagged, set @@ -160,7 +157,7 @@ package body Freeze is procedure Freeze_Enumeration_Type (Typ : Entity_Id); -- Freeze enumeration type. The Esize field is set as processing -- proceeds (i.e. set by default when the type is declared and then - -- adjusted by rep clauses. What this procedure does is to make sure + -- adjusted by rep clauses). What this procedure does is to make sure -- that if a foreign convention is specified, and no specific size -- is given, then the size must be at least Integer'Size. @@ -1483,90 +1480,322 @@ package body Freeze is -- Check_Inherited_Conditions -- -------------------------------- - procedure Check_Inherited_Conditions (R : Entity_Id) is - Prim_Ops : constant Elist_Id := Primitive_Operations (R); - Decls : List_Id; - Needs_Wrapper : Boolean; - Op_Node : Elmt_Id; - Par_Prim : Entity_Id; - Prim : Entity_Id; - - procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id); + procedure Check_Inherited_Conditions + (R : Entity_Id; + Late_Overriding : Boolean := False) + is + Prim_Ops : constant Elist_Id := Primitive_Operations (R); + Decls : List_Id; + Op_Node : Elmt_Id; + Par_Prim : Entity_Id; + Prim : Entity_Id; + Wrapper_Needed : Boolean; + + function Build_DTW_Body + (Loc : Source_Ptr; + DTW_Spec : Node_Id; + DTW_Decls : List_Id; + Par_Prim : Entity_Id; + Wrapped_Subp : Entity_Id) return Node_Id; + -- Build the body of the dispatch table wrapper containing the given + -- spec and declarations; the call to the wrapped subprogram includes + -- the proper type conversion. + + function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id; + -- Build the spec of the dispatch table wrapper + + procedure Build_Inherited_Condition_Pragmas + (Subp : Entity_Id; + Wrapper_Needed : out Boolean); -- Build corresponding pragmas for an operation whose ancestor has - -- class-wide pre/postconditions. If the operation is inherited, the - -- pragmas force the creation of a wrapper for the inherited operation. - -- If the ancestor is being overridden, the pragmas are constructed only - -- to verify their legality, in case they contain calls to other - -- primitives that may have been overridden. + -- class-wide pre/postconditions. If the operation is inherited then + -- Wrapper_Needed is returned True to force the creation of a wrapper + -- for the inherited operation. If the ancestor is being overridden, + -- the pragmas are constructed only to verify their legality, in case + -- they contain calls to other primitives that may have been overridden. + + function Needs_Wrapper + (Class_Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id) return Boolean; + -- Checks whether the dispatch-table wrapper (DTW) for Subp must be + -- built to evaluate the given class-wide condition. + + -------------------- + -- Build_DTW_Body -- + -------------------- + + function Build_DTW_Body + (Loc : Source_Ptr; + DTW_Spec : Node_Id; + DTW_Decls : List_Id; + Par_Prim : Entity_Id; + Wrapped_Subp : Entity_Id) return Node_Id + is + Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Prim); + Actuals : constant List_Id := Empty_List; + Call : Node_Id; + Formal : Entity_Id := First_Formal (Par_Prim); + New_F_Spec : Entity_Id := First (Parameter_Specifications (DTW_Spec)); + New_Formal : Entity_Id; + + begin + -- Build parameter association for call to wrapped subprogram + + while Present (Formal) loop + New_Formal := Defining_Identifier (New_F_Spec); + + -- If the controlling argument is inherited, add conversion to + -- parent type for the call. + + if Etype (Formal) = Par_Typ + and then Is_Controlling_Formal (Formal) + then + Append_To (Actuals, + Make_Type_Conversion (Loc, + New_Occurrence_Of (Par_Typ, 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 (Wrapped_Subp) = E_Procedure then + Call := + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Wrapped_Subp, Loc), + Parameter_Associations => Actuals); + else + Call := + Make_Simple_Return_Statement (Loc, + Expression => + Make_Function_Call (Loc, + Name => New_Occurrence_Of (Wrapped_Subp, Loc), + Parameter_Associations => Actuals)); + end if; + + return + Make_Subprogram_Body (Loc, + Specification => Copy_Subprogram_Spec (DTW_Spec), + Declarations => DTW_Decls, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List (Call), + End_Label => Make_Identifier (Loc, + Chars (Defining_Entity (DTW_Spec))))); + end Build_DTW_Body; + + -------------------- + -- Build_DTW_Spec -- + -------------------- + + function Build_DTW_Spec (Par_Prim : Entity_Id) return Node_Id is + DTW_Id : Entity_Id; + DTW_Spec : Node_Id; + + begin + DTW_Spec := Build_Overriding_Spec (Par_Prim, R); + DTW_Id := Defining_Entity (DTW_Spec); + + -- Add minimal decoration of fields + + Mutate_Ekind (DTW_Id, Ekind (Par_Prim)); + Set_LSP_Subprogram (DTW_Id, Par_Prim); + Set_Is_Dispatch_Table_Wrapper (DTW_Id); + Set_Is_Wrapper (DTW_Id); + + -- The DTW wrapper is never a null procedure + + if Nkind (DTW_Spec) = N_Procedure_Specification then + Set_Null_Present (DTW_Spec, False); + end if; + + return DTW_Spec; + end Build_DTW_Spec; --------------------------------------- -- Build_Inherited_Condition_Pragmas -- --------------------------------------- - procedure Build_Inherited_Condition_Pragmas (Subp : Entity_Id) is - A_Post : Node_Id; - A_Pre : Node_Id; - New_Prag : Node_Id; + procedure Build_Inherited_Condition_Pragmas + (Subp : Entity_Id; + Wrapper_Needed : out Boolean) + is + Class_Pre : constant Node_Id := + Class_Preconditions (Ultimate_Alias (Subp)); + Class_Post : Node_Id := Class_Postconditions (Par_Prim); + A_Post : Node_Id; + New_Prag : Node_Id; begin - A_Pre := Get_Class_Wide_Pragma (Par_Prim, Pragma_Precondition); + Wrapper_Needed := False; - if Present (A_Pre) then - New_Prag := New_Copy_Tree (A_Pre); - Build_Class_Wide_Expression - (Prag => New_Prag, - Subp => Prim, - Par_Subp => Par_Prim, - Adjust_Sloc => False, - Needs_Wrapper => Needs_Wrapper); - - if Needs_Wrapper - and then not Comes_From_Source (Subp) - and then Expander_Active - then - Append (New_Prag, Decls); - end if; + if No (Class_Pre) and then No (Class_Post) then + return; end if; - A_Post := Get_Class_Wide_Pragma (Par_Prim, Pragma_Postcondition); + -- For class-wide preconditions we just evaluate whether the wrapper + -- is needed; there is no need to build the pragma since the check + -- is performed on the caller side. - if Present (A_Post) then - New_Prag := New_Copy_Tree (A_Post); + if Present (Class_Pre) + and then Needs_Wrapper (Class_Pre, Subp, Par_Prim) + then + Wrapper_Needed := True; + end if; + + -- For class-wide postconditions we evaluate whether the wrapper is + -- needed and we build the class-wide postcondition pragma to install + -- it in the wrapper. + + if Present (Class_Post) + and then Needs_Wrapper (Class_Post, Subp, Par_Prim) + then + Wrapper_Needed := True; + + -- Update the class-wide postcondition + + Class_Post := New_Copy_Tree (Class_Post); Build_Class_Wide_Expression - (Prag => New_Prag, - Subp => Prim, + (Pragma_Or_Expr => Class_Post, + Subp => Subp, Par_Subp => Par_Prim, - Adjust_Sloc => False, - Needs_Wrapper => Needs_Wrapper); + Adjust_Sloc => False); - if Needs_Wrapper - and then not Comes_From_Source (Subp) - and then Expander_Active - then - Append (New_Prag, Decls); + -- Install the updated class-wide postcondition in a copy of the + -- pragma postcondition defined for the nearest ancestor. + + A_Post := Get_Class_Wide_Pragma (Par_Prim, + Pragma_Postcondition); + + if No (A_Post) then + declare + Subps : constant Subprogram_List := + Inherited_Subprograms (Subp); + begin + for Index in Subps'Range loop + A_Post := Get_Class_Wide_Pragma (Subps (Index), + Pragma_Postcondition); + exit when Present (A_Post); + end loop; + end; end if; + + New_Prag := New_Copy_Tree (A_Post); + Rewrite + (Expression (First (Pragma_Argument_Associations (New_Prag))), + Class_Post); + Append (New_Prag, Decls); end if; end Build_Inherited_Condition_Pragmas; + ------------------- + -- Needs_Wrapper -- + ------------------- + + function Needs_Wrapper + (Class_Cond : Node_Id; + Subp : Entity_Id; + Par_Subp : Entity_Id) return Boolean + is + Result : Boolean := False; + + function Check_Entity (N : Node_Id) return Traverse_Result; + -- Check calls to overridden primitives + + -------------------- + -- Replace_Entity -- + -------------------- + + function Check_Entity (N : Node_Id) return Traverse_Result is + New_E : Entity_Id; + + begin + if Nkind (N) = N_Identifier + and then Present (Entity (N)) + and then + (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N))) + and then + (Nkind (Parent (N)) /= N_Attribute_Reference + or else Attribute_Name (Parent (N)) /= Name_Class) + then + -- The check does not apply to dispatching calls within the + -- condition, but only to calls whose static tag is that of + -- the parent type. + + if Is_Subprogram (Entity (N)) + and then Nkind (Parent (N)) = N_Function_Call + and then Present (Controlling_Argument (Parent (N))) + then + return OK; + end if; + + -- Determine whether entity has a renaming + + New_E := Get_Mapped_Entity (Entity (N)); + + -- If the entity is an overridden primitive and we are not + -- in GNATprove mode, we must build a wrapper for the current + -- inherited operation. If the reference is the prefix of an + -- attribute such as 'Result (or others ???) there is no need + -- for a wrapper: the condition is just rewritten in terms of + -- the inherited subprogram. + + if Present (New_E) + and then Comes_From_Source (New_E) + and then Is_Subprogram (New_E) + and then Nkind (Parent (N)) /= N_Attribute_Reference + and then not GNATprove_Mode + then + Result := True; + return Abandon; + end if; + end if; + + return OK; + end Check_Entity; + + procedure Check_Condition_Entities is + new Traverse_Proc (Check_Entity); + + -- Start of processing for Needs_Wrapper + + begin + Update_Primitives_Mapping (Par_Subp, Subp); + + Map_Formals (Par_Subp, Subp); + Check_Condition_Entities (Class_Cond); + + return Result; + end Needs_Wrapper; + -- Start of processing for Check_Inherited_Conditions begin - Op_Node := First_Elmt (Prim_Ops); - while Present (Op_Node) loop - Prim := Node (Op_Node); + if Late_Overriding then + Op_Node := First_Elmt (Prim_Ops); + while Present (Op_Node) loop + Prim := Node (Op_Node); - -- Map the overridden primitive to the overriding one. This takes - -- care of all overridings and is done only once. + -- Map the overridden primitive to the overriding one - if Present (Overridden_Operation (Prim)) - and then Comes_From_Source (Prim) - then - Par_Prim := Overridden_Operation (Prim); - Update_Primitives_Mapping (Par_Prim, Prim); - end if; + if Present (Overridden_Operation (Prim)) + and then Comes_From_Source (Prim) + then + Par_Prim := Overridden_Operation (Prim); + Update_Primitives_Mapping (Par_Prim, Prim); - Next_Elmt (Op_Node); - end loop; + -- Force discarding previous mappings of its formals + + Map_Formals (Par_Prim, Prim, Force_Update => True); + end if; + + Next_Elmt (Op_Node); + end loop; + end if; -- Perform validity checks on the inherited conditions of overriding -- operations, for conformance with LSP, and apply SPARK-specific @@ -1602,12 +1831,6 @@ package body Freeze is if GNATprove_Mode then Collect_Inherited_Class_Wide_Conditions (Prim); - - -- Otherwise build the corresponding pragmas to check for legality - -- of the inherited condition. - - else - Build_Inherited_Condition_Pragmas (Prim); end if; end if; @@ -1621,12 +1844,17 @@ package body Freeze is Op_Node := First_Elmt (Prim_Ops); while Present (Op_Node) loop - Decls := Empty_List; - Prim := Node (Op_Node); - Needs_Wrapper := False; + Decls := Empty_List; + Prim := Node (Op_Node); + Wrapper_Needed := False; + + -- Skip internal entities built for mapping interface primitives - if not Comes_From_Source (Prim) and then Present (Alias (Prim)) then - Par_Prim := Alias (Prim); + if not Comes_From_Source (Prim) + and then Present (Alias (Prim)) + and then No (Interface_Alias (Prim)) + then + Par_Prim := Ultimate_Alias (Prim); -- When the primitive is an LSP wrapper we climb to the parent -- primitive that has the inherited contract. @@ -1644,39 +1872,39 @@ package body Freeze is -- in the loop above. Analyze_Entry_Or_Subprogram_Contract (Par_Prim); - Build_Inherited_Condition_Pragmas (Prim); + Build_Inherited_Condition_Pragmas (Prim, Wrapper_Needed); end if; - if Needs_Wrapper + if Wrapper_Needed and then not Is_Abstract_Subprogram (Par_Prim) and then Expander_Active then - -- We need to build a new primitive that overrides the inherited - -- one, and whose inherited expression has been updated above. - -- These expressions are the arguments of pragmas that are part - -- of the declarations of the wrapper. The wrapper holds a single - -- statement that is a call to the class-wide clone, where the - -- controlling actuals are conversions to the corresponding type - -- in the parent primitive: - - -- procedure New_Prim (F1 : T1; ...); - -- procedure New_Prim (F1 : T1; ...) is - -- pragma Check (Precondition, Expr); - -- begin - -- Par_Prim_Clone (Par_Type (F1), ...); - -- end; - - -- If the primitive is a function the statement is a return - -- statement with a call. + -- Build the dispatch-table wrapper (DTW). The support for + -- AI12-0195 relies on two kind of wrappers: one for indirect + -- calls (also used for AI12-0220), and one for putting in the + -- dispatch table: + -- + -- 1) "indirect-call wrapper" (ICW) is needed anytime there are + -- class-wide preconditions. Prim'Access will point directly + -- at the ICW if any, or at the "pristine" body if Prim has + -- no class-wide preconditions. + -- + -- 2) "dispatch-table wrapper" (DTW) is needed anytime the class + -- wide preconditions *or* the class-wide postconditions are + -- affected by overriding. + -- + -- The DTW holds a single statement that is a single call where + -- the controlling actuals are conversions to the corresponding + -- type in the parent primitive. If the primitive is a function + -- the statement is a return statement with a call. declare Alias_Id : constant Entity_Id := Ultimate_Alias (Prim); Loc : constant Source_Ptr := Sloc (R); - Par_R : constant Node_Id := Parent (R); - New_Body : Node_Id; - New_Decl : Node_Id; - New_Id : Entity_Id; - New_Spec : Node_Id; + DTW_Body : Node_Id; + DTW_Decl : Node_Id; + DTW_Id : Entity_Id; + DTW_Spec : Node_Id; begin -- The wrapper must be analyzed in the scope of its wrapped @@ -1684,47 +1912,130 @@ package body Freeze is Push_Scope (Scope (Prim)); - New_Spec := Build_Overriding_Spec (Par_Prim, R); - New_Id := Defining_Entity (New_Spec); - New_Decl := - Make_Subprogram_Declaration (Loc, - Specification => New_Spec); + DTW_Spec := Build_DTW_Spec (Par_Prim); + DTW_Id := Defining_Entity (DTW_Spec); + DTW_Decl := Make_Subprogram_Declaration (Loc, + Specification => DTW_Spec); + + -- For inherited class-wide preconditions the DTW wrapper + -- reuses the ICW of the parent (which checks the parent + -- interpretation of the class-wide preconditions); the + -- interpretation of the class-wide preconditions for the + -- inherited subprogram is checked at the caller side. + + -- When the subprogram inherits class-wide postconditions + -- the DTW also checks the interpretation of the class-wide + -- postconditions for the inherited subprogram, and the body + -- of the parent checks its interpretation of the parent for + -- the class-wide postconditions. + + -- procedure Prim (F1 : T1; ...) is + -- [ pragma Check (Postcondition, Expr); ] + -- begin + -- Par_Prim_ICW (Par_Type (F1), ...); + -- end; + + if Present (Indirect_Call_Wrapper (Par_Prim)) then + DTW_Body := + Build_DTW_Body (Loc, + DTW_Spec => DTW_Spec, + DTW_Decls => Decls, + Par_Prim => Par_Prim, + Wrapped_Subp => Indirect_Call_Wrapper (Par_Prim)); + + -- For subprograms that only inherit class-wide postconditions + -- the DTW wrapper calls the parent primitive (which on its + -- body checks the interpretation of the class-wide post- + -- conditions for the parent subprogram), and the DTW checks + -- the interpretation of the class-wide postconditions for the + -- inherited subprogram. + + -- procedure Prim (F1 : T1; ...) is + -- pragma Check (Postcondition, Expr); + -- begin + -- Par_Prim (Par_Type (F1), ...); + -- end; - -- Insert the declaration and the body of the wrapper after - -- type declaration that generates inherited operation. For - -- a null procedure, the declaration implies a null body. - - -- Before insertion, do some minimal decoration of fields + else + DTW_Body := + Build_DTW_Body (Loc, + DTW_Spec => DTW_Spec, + DTW_Decls => Decls, + Par_Prim => Par_Prim, + Wrapped_Subp => Par_Prim); + end if; - Mutate_Ekind (New_Id, Ekind (Par_Prim)); - Set_LSP_Subprogram (New_Id, Par_Prim); - Set_Is_Wrapper (New_Id); + -- Insert the declaration of the wrapper before the freezing + -- node of the record type declaration to ensure that it will + -- override the internal primitive built by Derive_Subprogram. - if Nkind (New_Spec) = N_Procedure_Specification - and then Null_Present (New_Spec) - then - Insert_After_And_Analyze (Par_R, New_Decl); + Ensure_Freeze_Node (R); + if Late_Overriding then + Insert_Before_And_Analyze (Freeze_Node (R), DTW_Decl); else - -- Build body as wrapper to a call to the already built - -- class-wide clone. + Append_Freeze_Action (R, DTW_Decl); + end if; + + Analyze (DTW_Decl); + + -- Insert the body of the wrapper in the freeze actions of + -- its record type declaration to ensure that it is placed + -- in the scope of its declaration but not too early to cause + -- premature freezing of other entities. + + Append_Freeze_Action (R, DTW_Body); + Analyze (DTW_Body); + + -- Ensure correct decoration + + pragma Assert (Is_Dispatching_Operation (DTW_Id)); + pragma Assert (Present (Overridden_Operation (DTW_Id))); + pragma Assert (Overridden_Operation (DTW_Id) = Alias_Id); - New_Body := - Build_Class_Wide_Clone_Call - (Loc, Decls, Par_Prim, New_Spec); + -- Inherit dispatch table slot - Insert_List_After_And_Analyze - (Par_R, New_List (New_Decl, New_Body)); + Set_DTC_Entity_Value (R, DTW_Id); + Set_DT_Position (DTW_Id, DT_Position (Alias_Id)); - -- Ensure correct decoration + -- Register the wrapper in the dispatch table - pragma Assert (Present (Alias (Prim))); - pragma Assert (Present (Overridden_Operation (New_Id))); - pragma Assert (Overridden_Operation (New_Id) = Alias_Id); + if Late_Overriding + and then not Building_Static_DT (R) + then + Insert_List_After_And_Analyze (Freeze_Node (R), + Register_Primitive (Loc, DTW_Id)); end if; - pragma Assert (Is_Dispatching_Operation (Prim)); - pragma Assert (Is_Dispatching_Operation (New_Id)); + -- Build the helper and ICW for the DTW + + if Present (Indirect_Call_Wrapper (Par_Prim)) then + declare + CW_Subp : Entity_Id; + Decl_N : Node_Id; + Body_N : Node_Id; + + begin + Merge_Class_Conditions (DTW_Id); + Make_Class_Precondition_Subps (DTW_Id, + Late_Overriding => Late_Overriding); + + CW_Subp := Static_Call_Helper (DTW_Id); + Decl_N := Unit_Declaration_Node (CW_Subp); + Analyze (Decl_N); + + -- If the DTW was built for a late-overriding primitive + -- its body must be analyzed now (since the tagged type + -- is already frozen). + + if Late_Overriding then + Body_N := + Unit_Declaration_Node + (Corresponding_Body (Decl_N)); + Analyze (Body_N); + end if; + end; + end if; Pop_Scope; end; @@ -7417,7 +7728,7 @@ package body Freeze is if Is_Type (E) then Freeze_And_Append (First_Subtype (E), N, Result); - -- If we just froze a tagged non-class wide record, then freeze the + -- If we just froze a tagged non-class-wide record, then freeze the -- corresponding class-wide type. This must be done after the tagged -- type itself is frozen, because the class-wide type refers to the -- tagged type which generates the class. diff --git a/gcc/ada/freeze.ads b/gcc/ada/freeze.ads index 6f4fecaea72..01747562b20 100644 --- a/gcc/ada/freeze.ads +++ b/gcc/ada/freeze.ads @@ -174,6 +174,15 @@ package Freeze is -- do not allow a size clause if the size would not otherwise be known at -- compile time in any case. + procedure Check_Inherited_Conditions + (R : Entity_Id; + Late_Overriding : Boolean := False); + -- For a tagged derived type R, create wrappers for inherited operations + -- that have class-wide conditions, so it can be properly rewritten if + -- it involves calls to other overriding primitives. Late_Overriding is + -- True when we are processing the body of a primitive with no previous + -- spec defined after R is frozen (see Check_Dispatching_Operation). + function Is_Full_Access_Aggregate (N : Node_Id) return Boolean; -- If a full access object is initialized with an aggregate or is assigned -- an aggregate, we have to prevent a piecemeal access or assignment to the diff --git a/gcc/ada/gen_il-fields.ads b/gcc/ada/gen_il-fields.ads index 360e2e1e0eb..24f57b4b241 100644 --- a/gcc/ada/gen_il-fields.ads +++ b/gcc/ada/gen_il-fields.ads @@ -461,7 +461,9 @@ package Gen_IL.Fields is Can_Never_Be_Null, Can_Use_Internal_Rep, Checks_May_Be_Suppressed, - Class_Wide_Clone, + Class_Postconditions, + Class_Preconditions, + Class_Preconditions_Subprogram, Class_Wide_Type, Cloned_Subtype, Component_Alignment, @@ -509,6 +511,7 @@ package Gen_IL.Fields is Discriminant_Default_Value, Discriminant_Number, Dispatch_Table_Wrappers, + Dynamic_Call_Helper, DT_Entry_Count, DT_Offset_To_Top_Func, DT_Position, @@ -649,9 +652,12 @@ package Gen_IL.Fields is Hiding_Loop_Variable, Hidden_In_Formal_Instance, Homonym, + Ignored_Class_Postconditions, + Ignored_Class_Preconditions, Ignore_SPARK_Mode_Pragmas, Import_Pragma, Incomplete_Actuals, + Indirect_Call_Wrapper, In_Package_Body, In_Private_Part, In_Use, @@ -693,6 +699,7 @@ package Gen_IL.Fields is Is_Discrim_SO_Function, Is_Discriminant_Check_Function, Is_Dispatch_Table_Entity, + Is_Dispatch_Table_Wrapper, Is_Dispatching_Operation, Is_Elaboration_Checks_OK_Id, Is_Elaboration_Warnings_OK_Id, @@ -892,6 +899,7 @@ package Gen_IL.Fields is Spec_Entity, SSO_Set_High_By_Default, SSO_Set_Low_By_Default, + Static_Call_Helper, Static_Discrete_Predicate, Static_Elaboration_Desired, Static_Initialization, diff --git a/gcc/ada/gen_il-gen-gen_entities.adb b/gcc/ada/gen_il-gen-gen_entities.adb index 0b70dae6c2f..bf0997e795d 100644 --- a/gcc/ada/gen_il-gen-gen_entities.adb +++ b/gcc/ada/gen_il-gen-gen_entities.adb @@ -139,6 +139,7 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (Is_Discrim_SO_Function, Flag), Sm (Is_Discriminant_Check_Function, Flag), Sm (Is_Dispatch_Table_Entity, Flag), + Sm (Is_Dispatch_Table_Wrapper, Flag), Sm (Is_Dispatching_Operation, Flag), Sm (Is_Eliminated, Flag), Sm (Is_Entry_Formal, Flag), @@ -977,8 +978,11 @@ begin -- Gen_IL.Gen.Gen_Entities Ab (Subprogram_Kind, Overloadable_Kind, (Sm (Body_Needed_For_SAL, Flag), - Sm (Class_Wide_Clone, Node_Id), + Sm (Class_Postconditions, Node_Id), + Sm (Class_Preconditions, Node_Id), + Sm (Class_Preconditions_Subprogram, Node_Id), Sm (Contract, Node_Id), + Sm (Dynamic_Call_Helper, Node_Id), Sm (Elaboration_Entity, Node_Id), Sm (Elaboration_Entity_Required, Flag), Sm (First_Entity, Node_Id), @@ -986,8 +990,11 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (Has_Nested_Subprogram, Flag), Sm (Has_Out_Or_In_Out_Parameter, Flag), Sm (Has_Recursive_Call, Flag), + Sm (Ignored_Class_Postconditions, Node_Id), + Sm (Ignored_Class_Preconditions, Node_Id), Sm (Ignore_SPARK_Mode_Pragmas, Flag), Sm (Import_Pragma, Node_Id), + Sm (Indirect_Call_Wrapper, Node_Id), Sm (Interface_Alias, Node_Id), Sm (Interface_Name, Node_Id), Sm (Is_Elaboration_Checks_OK_Id, Flag), @@ -998,6 +1005,7 @@ begin -- Gen_IL.Gen.Gen_Entities Sm (Overridden_Operation, Node_Id), Sm (Protected_Body_Subprogram, Node_Id), Sm (Scope_Depth_Value, Uint), + Sm (Static_Call_Helper, Node_Id), Sm (SPARK_Pragma, Node_Id), Sm (SPARK_Pragma_Inherited, Flag), Sm (Subps_Index, Uint))); diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 42ea0f52cf3..1720fe01cb8 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -584,6 +584,15 @@ package body Ghost is -- Start of processing for Check_Ghost_Context begin + -- Class-wide pre/postconditions of ignored pragmas are preanalyzed + -- to report errors on wrong conditions; however, ignored pragmas may + -- also have references to ghost entities and we must disable checking + -- their context to avoid reporting spurious errors. + + if Inside_Class_Condition_Preanalysis then + return; + end if; + -- Once it has been established that the reference to the Ghost entity -- is within a suitable context, ensure that the policy at the point of -- declaration and at the point of use match. diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads index 2fdccf756a6..699f68520ba 100644 --- a/gcc/ada/sem.ads +++ b/gcc/ada/sem.ads @@ -291,6 +291,10 @@ package Sem is -- freezing nodes can modify the status of this flag, any other client -- should regard it as read-only. + Inside_Class_Condition_Preanalysis : Boolean := False; + -- Flag indicating whether we are preanalyzing a class-wide precondition + -- or postcondition. + Inside_Preanalysis_Without_Freezing : Nat := 0; -- Flag indicating whether we are preanalyzing an expression performing no -- freezing. Non-zero means we are inside (it is actually a level counter diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index d954d46aaad..7b6dc21b6f0 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1339,6 +1339,16 @@ package body Sem_Attr is Legal := False; Spec_Id := Empty; + -- Skip processing during preanalysis of class-wide preconditions and + -- postconditions since at this stage the expression is not installed + -- yet on its definite context. + + if Inside_Class_Condition_Preanalysis then + Legal := True; + Spec_Id := Current_Scope; + return; + end if; + -- Traverse the parent chain to find the aspect or pragma where the -- attribute resides. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 595a741346f..15b3c444125 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; ------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 7a8d0cc7f1d..63bb80c1291 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -3028,6 +3028,10 @@ package body Sem_Ch5 is then Analyze_And_Resolve (Original_Bound, Typ); return Original_Bound; + + elsif Inside_Class_Condition_Preanalysis then + Analyze_And_Resolve (Original_Bound, Typ); + return Original_Bound; end if; -- Normally, the best approach is simply to generate a constant @@ -3333,11 +3337,17 @@ package body Sem_Ch5 is -- or post-condition has been expanded. Update the type of the loop -- variable to reflect the proper itype at each stage of analysis. + -- Loop_Nod might not be present when we are preanalyzing a class-wide + -- pre/postcondition since preanalysis occurs in a place unrelated to + -- the actual code and the quantified expression may be the outermost + -- expression of the class-wide condition. + if No (Etype (Id)) or else Etype (Id) = Any_Type or else (Present (Etype (Id)) and then Is_Itype (Etype (Id)) + and then Present (Loop_Nod) and then Nkind (Parent (Loop_Nod)) = N_Expression_With_Actions and then Nkind (Original_Node (Parent (Loop_Nod))) = N_Quantified_Expression) diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 02928342744..1fcbdfbf918 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4498,29 +4498,6 @@ package body Sem_Ch6 is end if; end if; - -- If the subprogram has a class-wide clone, build its body as a copy - -- of the original body, and rewrite body of original subprogram as a - -- wrapper that calls the clone. If N is a stub, this construction will - -- take place when the proper body is analyzed. No action needed if this - -- subprogram has been eliminated. - - if Present (Spec_Id) - and then Present (Class_Wide_Clone (Spec_Id)) - and then (Comes_From_Source (N) or else Was_Expression_Function (N)) - and then Nkind (N) /= N_Subprogram_Body_Stub - and then not (Expander_Active and then Is_Eliminated (Spec_Id)) - then - Build_Class_Wide_Clone_Body (Spec_Id, N); - - -- This is the new body for the existing primitive operation - - Rewrite (N, Build_Class_Wide_Clone_Call - (Sloc (N), New_List, Spec_Id, Parent (Spec_Id))); - Set_Has_Completion (Spec_Id, False); - Analyze (N); - return; - end if; - -- Place subprogram on scope stack, and make formals visible. If there -- is a spec, the visible entity remains that of the spec. @@ -10413,6 +10390,7 @@ package body Sem_Ch6 is begin Set_Is_Immediately_Visible (E); Set_Current_Entity (E); + pragma Assert (Prev /= E); Set_Homonym (E, Prev); end Install_Entity; diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index cc612db9f1b..cba3c9dbb0d 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. diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads index 7b42cf54d12..f37391b6307 100644 --- a/gcc/ada/sem_disp.ads +++ b/gcc/ada/sem_disp.ads @@ -74,6 +74,10 @@ package Sem_Disp is -- The Alias of Old_Subp is adjusted to point to the inherited procedure -- of the full view because it is always this one which has to be called. + function Covered_Interface_Primitives (Prim : Entity_Id) return Elist_Id; + -- Returns all the interface primitives covered by Prim, when its + -- controlling type has progenitors. + function Covered_Interface_Op (Prim : Entity_Id) return Entity_Id; -- Returns the interface primitive that Prim covers, when its controlling -- type has progenitors. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0228717d707..7386ecc1b93 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -25896,23 +25896,6 @@ package body Sem_Prag is ("operation in class-wide condition must be primitive " & "of &", Nod, Disp_Typ); end if; - - -- Otherwise we have a call to an overridden primitive, and we - -- will create a common class-wide clone for the body of - -- original operation and its eventual inherited versions. If - -- the original operation dispatches on result it is never - -- inherited and there is no need for a clone. There is not - -- need for a clone either in GNATprove mode, as cases that - -- would require it are rejected (when an inherited primitive - -- calls an overridden operation in a class-wide contract), and - -- the clone would make proof impossible in some cases. - - elsif not Is_Abstract_Subprogram (Spec_Id) - and then No (Class_Wide_Clone (Spec_Id)) - and then not Has_Controlling_Result (Spec_Id) - and then not GNATprove_Mode - then - Build_Class_Wide_Clone_Decl (Spec_Id); end if; end; @@ -26033,15 +26016,6 @@ package body Sem_Prag is End_Scope; end if; - -- If analysis of the condition indicates that a class-wide clone - -- has been created, build and analyze its declaration. - - if Is_Subprogram (Spec_Id) - and then Present (Class_Wide_Clone (Spec_Id)) - then - Analyze (Unit_Declaration_Node (Class_Wide_Clone (Spec_Id))); - end if; - -- Currently it is not possible to inline pre/postconditions on a -- subprogram subject to pragma Inline_Always. @@ -29528,9 +29502,6 @@ package body Sem_Prag is Msg_Arg : Node_Id; Nam : Name_Id; - Needs_Wrapper : Boolean; - pragma Unreferenced (Needs_Wrapper); - -- Start of processing for Build_Pragma_Check_Equivalent begin @@ -29557,11 +29528,10 @@ package body Sem_Prag is -- Build the inherited class-wide condition Build_Class_Wide_Expression - (Prag => Check_Prag, - Subp => Subp_Id, - Par_Subp => Inher_Id, - Adjust_Sloc => True, - Needs_Wrapper => Needs_Wrapper); + (Pragma_Or_Expr => Check_Prag, + Subp => Subp_Id, + Par_Subp => Inher_Id, + Adjust_Sloc => True); -- If not an inherited condition simply copy the original pragma diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 7b9f8ab48d8..0d013ba7ec1 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4891,10 +4891,15 @@ package body Sem_Res is -- Apply legality rule 3.9.2 (9/1) + -- Skip this check on helpers and indirect-call wrappers built to + -- support class-wide preconditions. + if (Is_Class_Wide_Type (A_Typ) or else Is_Dynamically_Tagged (A)) and then not Is_Class_Wide_Type (F_Typ) and then not Is_Controlling_Formal (F) and then not In_Instance + and then (not Is_Subprogram (Nam) + or else No (Class_Preconditions_Subprogram (Nam))) then Error_Msg_N ("class-wide argument not allowed here!", A); @@ -4992,9 +4997,13 @@ package body Sem_Res is -- "False" cannot act as an actual in a subprogram with value -- "True" (SPARK RM 6.1.7(3)). + -- No check needed for helpers and indirect-call wrappers built to + -- support class-wide preconditions. + if Is_EVF_Expression (A) and then Extensions_Visible_Status (Nam) = Extensions_Visible_True + and then No (Class_Preconditions_Subprogram (Current_Scope)) then Error_Msg_N ("formal parameter cannot act as actual parameter when " diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 816fb451fd0..98e68779107 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 diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 4e896a3599f..7a7771562c6 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -283,30 +283,6 @@ package Sem_Util is -- take care of constructing declaration and body of the clone, and -- building the calls to it within the appropriate wrappers. - procedure Build_Class_Wide_Clone_Body - (Spec_Id : Entity_Id; - Bod : Node_Id); - -- Build body of subprogram that has a class-wide condition that contains - -- calls to other primitives. Spec_Id is the Id of the subprogram, and B - -- is its source body, which becomes the body of the clone. - - function Build_Class_Wide_Clone_Call - (Loc : Source_Ptr; - Decls : List_Id; - Spec_Id : Entity_Id; - Spec : Node_Id) return Node_Id; - -- Build a call to the common class-wide clone of a subprogram with - -- class-wide conditions. The body of the subprogram becomes a wrapper - -- for a call to the clone. The inherited operation becomes a similar - -- wrapper to which modified conditions apply, and the call to the - -- clone includes the proper conversion in a call the parent operation. - - procedure Build_Class_Wide_Clone_Decl (Spec_Id : Entity_Id); - -- For a subprogram that has a class-wide condition that contains calls - -- to other primitives, build an internal subprogram that is invoked - -- through a type-specific wrapper for all inherited subprograms that - -- may have a modified condition. - procedure Build_Constrained_Itype (N : Node_Id; Typ : Entity_Id; @@ -527,6 +503,18 @@ package Sem_Util is -- reasons these nodes have a different structure even though they play -- similar roles in array aggregates. + type Condition_Kind is + (Ignored_Class_Precondition, + Ignored_Class_Postcondition, + Class_Precondition, + Class_Postcondition); + -- Kind of class-wide conditions + + function Class_Condition + (Kind : Condition_Kind; + Subp : Entity_Id) return Node_Id; + -- Class-wide Kind condition of Subp + function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id; -- Gather the entities of all abstract states and objects declared in the -- body state space of package body Body_Id. @@ -2621,6 +2609,12 @@ package Sem_Util is -- if we're not sure, we return True. If N is a subprogram body, this is -- about whether execution of that body can raise. + function Nearest_Class_Condition_Subprogram + (Kind : Condition_Kind; + Spec_Id : Entity_Id) return Entity_Id; + -- Return the nearest ancestor containing the merged class-wide conditions + -- that statically apply to Spec_Id; return Empty otherwise. + function Nearest_Enclosing_Instance (E : Entity_Id) return Entity_Id; -- Return the entity of the nearest enclosing instance which encapsulates -- entity E. If no such instance exits, return Empty.