From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 2BA993858403; Wed, 1 Dec 2021 10:25:34 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 2BA993858403 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-5659] [Ada] Improve messages on incorrect state refinement in SPARK X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 7b4069fb7c00564523f822c7fd94210862eeeae4 X-Git-Newrev: aeaabe7b3cb0ca9b9426468afb838f3d84126349 Message-Id: <20211201102534.2BA993858403@sourceware.org> Date: Wed, 1 Dec 2021 10:25:34 +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: Wed, 01 Dec 2021 10:25:34 -0000 https://gcc.gnu.org/g:aeaabe7b3cb0ca9b9426468afb838f3d84126349 commit r12-5659-gaeaabe7b3cb0ca9b9426468afb838f3d84126349 Author: Yannick Moy Date: Wed Sep 29 15:26:54 2021 +0200 [Ada] Improve messages on incorrect state refinement in SPARK gcc/ada/ * sem_ch10.adb (Is_Private_Library_Unit): Move query to Sem_Util for sharing. * sem_ch7.adb (Analyze_Package_Body_Helper): Add continuation message. * sem_prag.adb (Analyze_Part_Of): Call new function Is_Private_Library_Unit. (Check_Valid_Library_Unit_Pragma): Specialize error messages on misplaced pragmas. (Analyze_Refined_State_In_Decl_Part): Recognize missing Part_Of on object in private part. * sem_util.adb (Check_State_Refinements): Add continuation message. (Find_Placement_In_State_Space): Fix detection of placement, which relied wrongly on queries In_Package_Body/In_Private_Part which do not provide the right information here for all cases. (Is_Private_Library_Unit): Move query here for sharing. * sem_util.ads (Is_Private_Library_Unit): Move query here for sharing. Diff: --- gcc/ada/sem_ch10.adb | 17 ------- gcc/ada/sem_ch7.adb | 2 + gcc/ada/sem_prag.adb | 129 ++++++++++++++++++++++++++++++++++++++++----------- gcc/ada/sem_util.adb | 100 +++++++++++++++++++++++++++++++++------ gcc/ada/sem_util.ads | 4 ++ 5 files changed, 194 insertions(+), 58 deletions(-) diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index 6305bdb7371..f586461b4a8 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -2952,23 +2952,6 @@ package body Sem_Ch10 is Par_Lib : Entity_Id; Par_Spec : Node_Id; - function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean; - -- Returns true if and only if the library unit is declared with - -- an explicit designation of private. - - ----------------------------- - -- Is_Private_Library_Unit -- - ----------------------------- - - function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean is - Comp_Unit : constant Node_Id := Parent (Unit_Declaration_Node (Unit)); - - begin - return Private_Present (Comp_Unit); - end Is_Private_Library_Unit; - - -- Start of processing for Check_Private_Child_Unit - begin if Nkind (Lib_Unit) in N_Package_Body | N_Subprogram_Body then Curr_Unit := Defining_Entity (Unit (Library_Unit (N))); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 95d7ad4c1cd..6e799490c10 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -759,6 +759,8 @@ package body Sem_Ch7 is ("optional package body (not allowed in Ada 95)??", N); else Error_Msg_N ("spec of this package does not allow a body", N); + Error_Msg_N ("\either remove the body or add pragma " + & "Elaborate_Body in the spec", N); end if; end if; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c3ea16df54d..1d5cc2535bd 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3453,9 +3453,7 @@ package body Sem_Prag is Parent_Unit := Pack_Id; while Present (Parent_Unit) loop - exit when - Private_Present - (Parent (Unit_Declaration_Node (Parent_Unit))); + exit when Is_Private_Library_Unit (Parent_Unit); Parent_Unit := Scope (Parent_Unit); end loop; @@ -3503,17 +3501,80 @@ package body Sem_Prag is -- encapsulating state must be declared in the same package. elsif Placement = Private_State_Space then - if Scope (Encap_Id) /= Pack_Id then - SPARK_Msg_NE - ("indicator Part_Of must denote an abstract state of " - & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); - Error_Msg_Name_1 := Chars (Pack_Id); - SPARK_Msg_NE - ("\& is declared in the private part of package %", - Indic, Item_Id); - return; - end if; + -- In the case of the abstract state of a nongeneric private + -- child package, it may be encapsulated in the state of a + -- public descendant of its parent package. + + declare + function Is_Public_Descendant + (Child, Ancestor : Entity_Id) + return Boolean; + -- Return True if Child is a public descendant of Pack + + -------------------------- + -- Is_Public_Descendant -- + -------------------------- + + function Is_Public_Descendant + (Child, Ancestor : Entity_Id) + return Boolean + is + P : Entity_Id := Child; + begin + while Is_Child_Unit (P) + and then not Is_Private_Library_Unit (P) + loop + if Scope (P) = Ancestor then + return True; + end if; + + P := Scope (P); + end loop; + + return False; + end Is_Public_Descendant; + + -- Local variables + + Immediate_Pack_Id : constant Entity_Id := Scope (Item_Id); + + Is_State_Of_Private_Child : constant Boolean := + Is_Child_Unit (Immediate_Pack_Id) + and then not Is_Generic_Unit (Immediate_Pack_Id) + and then Is_Private_Descendant (Immediate_Pack_Id); + + Is_OK_Through_Sibling : Boolean := False; + + begin + if Ekind (Item_Id) = E_Abstract_State + and then Is_State_Of_Private_Child + and then Is_Public_Descendant (Scope (Encap_Id), Pack_Id) + then + Is_OK_Through_Sibling := True; + end if; + + if Scope (Encap_Id) /= Pack_Id + and then not Is_OK_Through_Sibling + then + if Is_State_Of_Private_Child then + SPARK_Msg_NE + ("indicator Part_Of must denote abstract state of & " + & "or of its public descendant " + & "(SPARK RM 7.2.6(3))", Indic, Pack_Id); + else + SPARK_Msg_NE + ("indicator Part_Of must denote an abstract state of " + & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id); + end if; + + Error_Msg_Name_1 := Chars (Pack_Id); + SPARK_Msg_NE + ("\& is declared in the private part of package %", + Indic, Item_Id); + return; + end if; + end; -- Items declared in the body state space of a package do not need -- Part_Of indicators as the refinement has already been seen. @@ -6612,7 +6673,9 @@ package body Sem_Prag is elsif Nkind (Parent_Node) = N_Compilation_Unit_Aux then if Plist /= Pragmas_After (Parent_Node) then - Pragma_Misplaced; + Error_Pragma + ("pragma% misplaced, must be inside or after the " + & "compilation unit"); elsif Arg_Count = 0 then Error_Pragma @@ -6679,26 +6742,36 @@ package body Sem_Prag is Unit_Node := Unit_Declaration_Node (Current_Scope); Unit_Kind := Nkind (Unit_Node); - if Nkind (Parent (Unit_Node)) /= N_Compilation_Unit then - Pragma_Misplaced; + if Unit_Node = Standard_Package_Node then + Error_Pragma + ("pragma% misplaced, must be inside or after the " + & "compilation unit"); + + elsif Nkind (Parent (Unit_Node)) /= N_Compilation_Unit then + Error_Pragma + ("pragma% misplaced, must be on library unit"); elsif Unit_Kind = N_Subprogram_Body and then not Acts_As_Spec (Unit_Node) then - Pragma_Misplaced; + Error_Pragma + ("pragma% misplaced, must be on the subprogram spec"); elsif Nkind (Parent_Node) = N_Package_Body then - Pragma_Misplaced; + Error_Pragma + ("pragma% misplaced, must be on the package spec"); elsif Nkind (Parent_Node) = N_Package_Specification and then Plist = Private_Declarations (Parent_Node) then - Pragma_Misplaced; + Error_Pragma + ("pragma% misplaced, must be in the public part"); elsif Nkind (Parent_Node) in N_Generic_Declaration and then Plist = Generic_Formal_Declarations (Parent_Node) then - Pragma_Misplaced; + Error_Pragma + ("pragma% misplaced, must not be in formal part"); elsif Arg_Count > 0 then Analyze (Get_Pragma_Arg (Arg1)); @@ -28761,13 +28834,17 @@ package body Sem_Prag is Placement => Placement, Pack_Id => Pack_Id); - -- The constituent is part of the visible state of a - -- private child package, but lacks a Part_Of indicator. + -- The constituent is either part of the hidden state of + -- the package or part of the visible state of a private + -- child package, but lacks a Part_Of indicator. - if Placement = Visible_State_Space - and then Is_Child_Unit (Pack_Id) - and then not Is_Generic_Unit (Pack_Id) - and then Is_Private_Descendant (Pack_Id) + if (Placement = Private_State_Space + and then Pack_Id = Spec_Id) + or else + (Placement = Visible_State_Space + and then Is_Child_Unit (Pack_Id) + and then not Is_Generic_Unit (Pack_Id) + and then Is_Private_Descendant (Pack_Id)) then Error_Msg_Name_1 := Chars (State_Id); SPARK_Msg_NE diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 5feb83d3151..bd8c88da865 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -5246,6 +5246,8 @@ package body Sem_Util is and then not Has_Non_Null_Refinement (State_Id) then Error_Msg_N ("state & requires refinement", State_Id); + Error_Msg_N ("\package body should have Refined_State " + & "for state & with constituents", State_Id); end if; Next_Elmt (State_Elmt); @@ -9586,35 +9588,88 @@ package body Sem_Util is Placement : out State_Space_Kind; Pack_Id : out Entity_Id) is + function Inside_Package_Body (Id : Entity_Id) return Boolean; + function Inside_Private_Part (Id : Entity_Id) return Boolean; + -- Return True if Id is declared directly within the package body + -- and the package private parts, respectively. We cannot use + -- In_Private_Part/In_Body_Part flags, as these are only set during the + -- analysis of the package itself, while Find_Placement_In_State_Space + -- can be called on an entity of another package. + + ------------------------ + -- Inside_Package_Body -- + ------------------------ + + function Inside_Package_Body (Id : Entity_Id) return Boolean is + Spec_Id : constant Entity_Id := Scope (Id); + Body_Decl : constant Opt_N_Package_Body_Id := Package_Body (Spec_Id); + Decl : constant Node_Id := Enclosing_Declaration (Id); + begin + if Present (Body_Decl) + and then Is_List_Member (Decl) + and then List_Containing (Decl) = Declarations (Body_Decl) + then + return True; + else + return False; + end if; + end Inside_Package_Body; + + ------------------------- + -- Inside_Private_Part -- + ------------------------- + + function Inside_Private_Part (Id : Entity_Id) return Boolean is + Spec_Id : constant Entity_Id := Scope (Id); + Private_Decls : constant List_Id := + Private_Declarations (Package_Specification (Spec_Id)); + Decl : constant Node_Id := Enclosing_Declaration (Id); + begin + if Is_List_Member (Decl) + and then List_Containing (Decl) = Private_Decls + then + return True; + + elsif Ekind (Id) = E_Package + and then Is_Private_Library_Unit (Id) + then + return True; + + else + return False; + end if; + end Inside_Private_Part; + + -- Local variables + Context : Entity_Id; + -- Start of processing for Find_Placement_In_State_Space + begin -- Assume that the item does not appear in the state space of a package Placement := Not_In_Package; - Pack_Id := Empty; -- Climb the scope stack and examine the enclosing context - Context := Scope (Item_Id); - while Present (Context) and then Context /= Standard_Standard loop - if Is_Package_Or_Generic_Package (Context) then - Pack_Id := Context; + Context := Item_Id; + Pack_Id := Scope (Context); + while Present (Pack_Id) and then Pack_Id /= Standard_Standard loop + if Is_Package_Or_Generic_Package (Pack_Id) then - -- A package body is a cut off point for the traversal as the item - -- cannot be visible to the outside from this point on. Note that - -- this test must be done first as a body is also classified as a - -- private part. + -- A package body is a cut off point for the traversal as the + -- item cannot be visible to the outside from this point on. - if In_Package_Body (Context) then + if Inside_Package_Body (Context) then Placement := Body_State_Space; return; -- The private part of a package is a cut off point for the - -- traversal as the item cannot be visible to the outside from - -- this point on. + -- traversal as the item cannot be visible to the outside + -- from this point on. - elsif In_Private_Part (Context) then + elsif Inside_Private_Part (Context) then Placement := Private_State_Space; return; @@ -9626,9 +9681,11 @@ package body Sem_Util is Placement := Visible_State_Space; -- The visible state space of a child unit acts as the proper - -- placement of an item. + -- placement of an item, unless this is a private child unit. - if Is_Child_Unit (Context) then + if Is_Child_Unit (Pack_Id) + and then not Is_Private_Library_Unit (Pack_Id) + then return; end if; end if; @@ -9638,10 +9695,12 @@ package body Sem_Util is else Placement := Not_In_Package; + Pack_Id := Empty; return; end if; Context := Scope (Context); + Pack_Id := Scope (Context); end loop; end Find_Placement_In_State_Space; @@ -20308,6 +20367,17 @@ package body Sem_Util is return False; end Is_Preelaborable_Function; + ----------------------------- + -- Is_Private_Library_Unit -- + ----------------------------- + + function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean is + Comp_Unit : constant Node_Id := Parent (Unit_Declaration_Node (Unit)); + begin + return Nkind (Comp_Unit) = N_Compilation_Unit + and then Private_Present (Comp_Unit); + end Is_Private_Library_Unit; + --------------------------------- -- Is_Protected_Self_Reference -- --------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index abc18ec8d63..8b74ab6fe68 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2276,6 +2276,10 @@ package Sem_Util is -- Is_Non_Preelaborable_Construct takes into account the syntactic -- and semantic properties of N for a more accurate diagnostic. + function Is_Private_Library_Unit (Unit : Entity_Id) return Boolean; + -- Returns True if and only if the library unit is declared with an + -- explicit designation of private. + function Is_Protected_Self_Reference (N : Node_Id) return Boolean; -- Return True if node N denotes a protected type name which represents -- the current instance of a protected object according to RM 9.4(21/2).