From 3e5400f4acc56a3e6a25ebeb5f7bfcf9d7d3646a Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Wed, 8 Nov 2017 16:04:35 +0000 Subject: [PATCH] [multiple changes] 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now represented by Entity_Id. (SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now represented by Entity_Id; this information is not repeated as Scope_Entity. (Heap): Moved from lib-xref-spark_specific.adb, to reside next to Name_Of_Heap_Variable. * spark_xrefs.adb (dspark): Adapt debug routine to above changes in data types. * lib-xref-spark_specific.adb: Adapt routines for populating SPARK scope and xrefs tables to above changes in data types. 2017-11-08 Justin Squirek * sem_ch8.adb (Mark_Use_Clauses): Add condition to always mark the primitives of generic actuals. (Mark_Use_Type): Add recursive call to properly mark class-wide type's base type clauses as per ARM 8.4 (8.2/3). 2017-11-08 Ed Schonberg * sem_ch6.adb (Analyze_Generic_Subprobram_Body): Validate categorization dependency of the body, as is done for non-generic units. (New_Overloaded_Entity, Visible_Part_Type): Remove linear search through declarations (Simple optimization, no behavior change). From-SVN: r254539 --- gcc/ada/ChangeLog | 29 ++++++++++++++++++++++ gcc/ada/lib-xref-spark_specific.adb | 30 ++++++++++------------- gcc/ada/sem_ch6.adb | 37 +++++++++-------------------- gcc/ada/sem_ch8.adb | 19 ++++++++++++--- gcc/ada/spark_xrefs.adb | 13 ++++------ gcc/ada/spark_xrefs.ads | 15 ++++++------ 6 files changed, 80 insertions(+), 63 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b607ce6df99..6b1d7cab580 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2017-11-08 Piotr Trojanek + + * spark_xrefs.ads (SPARK_Xref_Record): Referenced object is now + represented by Entity_Id. + (SPARK_Scope_Record): Referenced scope (e.g. subprogram) is now + represented by Entity_Id; this information is not repeated as + Scope_Entity. + (Heap): Moved from lib-xref-spark_specific.adb, to reside next to + Name_Of_Heap_Variable. + * spark_xrefs.adb (dspark): Adapt debug routine to above changes in + data types. + * lib-xref-spark_specific.adb: Adapt routines for populating SPARK + scope and xrefs tables to above changes in data types. + +2017-11-08 Justin Squirek + + * sem_ch8.adb (Mark_Use_Clauses): Add condition to always mark the + primitives of generic actuals. + (Mark_Use_Type): Add recursive call to properly mark class-wide type's + base type clauses as per ARM 8.4 (8.2/3). + +2017-11-08 Ed Schonberg + + * sem_ch6.adb (Analyze_Generic_Subprobram_Body): Validate + categorization dependency of the body, as is done for non-generic + units. + (New_Overloaded_Entity, Visible_Part_Type): Remove linear search + through declarations (Simple optimization, no behavior change). + 2017-11-08 Piotr Trojanek * spark_xrefs.ads (SPARK_Xref_Record): Remove inessential components. diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 395071976a0..1b31c6acd11 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -66,9 +66,6 @@ package body SPARK_Specific is -- Local Variables -- --------------------- - Heap : Entity_Id := Empty; - -- A special entity which denotes the heap object - package Drefs is new Table.Table ( Table_Component_Type => Xref_Entry, Table_Index_Type => Xref_Entry_Number, @@ -164,14 +161,13 @@ package body SPARK_Specific is -- range. SPARK_Scope_Table.Append - ((Scope_Name => new String'(Unique_Name (E)), + ((Scope_Id => E, File_Num => Dspec, Scope_Num => Scope_Id, Spec_File_Num => 0, Spec_Scope_Num => 0, From_Xref => 1, - To_Xref => 0, - Scope_Entity => E)); + To_Xref => 0)); Scope_Id := Scope_Id + 1; end Add_SPARK_Scope; @@ -351,7 +347,7 @@ package body SPARK_Specific is function Entity_Of_Scope (S : Scope_Index) return Entity_Id is begin - return SPARK_Scope_Table.Table (S).Scope_Entity; + return SPARK_Scope_Table.Table (S).Scope_Id; end Entity_Of_Scope; ------------------- @@ -423,7 +419,7 @@ package body SPARK_Specific is function Is_Past_Scope_Entity return Boolean is begin for Index in SPARK_Scope_Table.First .. S - 1 loop - if SPARK_Scope_Table.Table (Index).Scope_Entity = E then + if SPARK_Scope_Table.Table (Index).Scope_Id = E then return True; end if; end loop; @@ -435,7 +431,7 @@ package body SPARK_Specific is begin for Index in S .. SPARK_Scope_Table.Last loop - if SPARK_Scope_Table.Table (Index).Scope_Entity = E then + if SPARK_Scope_Table.Table (Index).Scope_Id = E then return True; end if; end loop; @@ -634,7 +630,7 @@ package body SPARK_Specific is declare S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); begin - Set_Scope_Num (S.Scope_Entity, S.Scope_Num); + Set_Scope_Num (S.Scope_Id, S.Scope_Num); end; end loop; @@ -800,10 +796,10 @@ package body SPARK_Specific is end if; SPARK_Xref_Table.Append ( - (Entity_Name => new String'(Unique_Name (Ref.Ent)), - File_Num => Dependency_Num (Ref.Lun), - Scope_Num => Get_Scope_Num (Ref.Ref_Scope), - Rtype => Typ)); + (Entity => Unique_Entity (Ref.Ent), + File_Num => Dependency_Num (Ref.Lun), + Scope_Num => Get_Scope_Num (Ref.Ref_Scope), + Rtype => Typ)); end; end loop; @@ -948,7 +944,7 @@ package body SPARK_Specific is declare Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); begin - Entity_Hash_Table.Set (Srec.Scope_Entity, S); + Entity_Hash_Table.Set (Srec.Scope_Id, S); end; end loop; @@ -959,14 +955,14 @@ package body SPARK_Specific is Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); Spec_Entity : constant Entity_Id := - Unique_Entity (Srec.Scope_Entity); + Unique_Entity (Srec.Scope_Id); Spec_Scope : constant Scope_Index := Entity_Hash_Table.Get (Spec_Entity); begin -- Generic spec may be missing in which case Spec_Scope is zero - if Spec_Entity /= Srec.Scope_Entity + if Spec_Entity /= Srec.Scope_Id and then Spec_Scope /= 0 then Srec.Spec_File_Num := diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 4f719e9b81c..5dc92d28634 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1510,6 +1510,7 @@ package body Sem_Ch6 is Process_End_Label (Handled_Statement_Sequence (N), 't', Current_Scope); Update_Use_Clause_Chain; + Validate_Categorization_Dependency (N, Gen_Id); End_Scope; Check_Subprogram_Order (N); @@ -10118,7 +10119,6 @@ package body Sem_Ch6 is function Visible_Part_Type (T : Entity_Id) return Boolean is P : constant Node_Id := Unit_Declaration_Node (Scope (T)); - N : Node_Id; begin -- If the entity is a private type, then it must be declared in a @@ -10126,34 +10126,19 @@ package body Sem_Ch6 is if Ekind (T) in Private_Kind then return True; - end if; - - -- Otherwise, we traverse the visible part looking for its - -- corresponding declaration. We cannot use the declaration - -- node directly because in the private part the entity of a - -- private type is the one in the full view, which does not - -- indicate that it is the completion of something visible. - - N := First (Visible_Declarations (Specification (P))); - while Present (N) loop - if Nkind (N) = N_Full_Type_Declaration - and then Present (Defining_Identifier (N)) - and then T = Defining_Identifier (N) - then - return True; - elsif Nkind_In (N, N_Private_Type_Declaration, - N_Private_Extension_Declaration) - and then Present (Defining_Identifier (N)) - and then T = Full_View (Defining_Identifier (N)) - then - return True; - end if; + elsif Is_Type (T) and then Has_Private_Declaration (T) then + return True; - Next (N); - end loop; + elsif Is_List_Member (Declaration_Node (T)) + and then List_Containing (Declaration_Node (T)) = + Visible_Declarations (Specification (P)) + then + return True; - return False; + else + return False; + end if; end Visible_Part_Type; -- Start of processing for Check_For_Primitive_Subprogram diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 86ceb52bf60..31ce62b3867 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -8320,6 +8320,7 @@ package body Sem_Ch8 is procedure Mark_Use_Type (E : Entity_Id) is Curr : Node_Id; + Base : Entity_Id; begin -- Ignore void types and unresolved string literals and primitives @@ -8331,12 +8332,22 @@ package body Sem_Ch8 is return; end if; + -- Primitives with class-wide operands might additionally render + -- their base type's use_clauses effective - so do a recursive check + -- here. + + Base := Base_Type (Etype (E)); + + if Ekind (Base) = E_Class_Wide_Type then + Mark_Use_Type (Base); + end if; + -- The package containing the type or operator function being used -- may be in use as well, so mark any use_package_clauses for it as -- effective. There are also additional sanity checks performed here -- for ignoring previous errors. - Mark_Use_Package (Scope (Base_Type (Etype (E)))); + Mark_Use_Package (Scope (Base)); if Nkind (E) in N_Op and then Present (Entity (E)) @@ -8345,7 +8356,7 @@ package body Sem_Ch8 is Mark_Use_Package (Scope (Entity (E))); end if; - Curr := Current_Use_Clause (Base_Type (Etype (E))); + Curr := Current_Use_Clause (Base); while Present (Curr) and then not Is_Effective_Use_Clause (Curr) loop @@ -8397,7 +8408,9 @@ package body Sem_Ch8 is or else Ekind_In (Id, E_Generic_Function, E_Generic_Procedure)) and then (Is_Potentially_Use_Visible (Id) - or else Is_Intrinsic_Subprogram (Id)) + or else Is_Intrinsic_Subprogram (Id) + or else (Ekind_In (Id, E_Function, E_Procedure) + and then Is_Generic_Actual_Subprogram (Id))) then Mark_Parameters (Id); end if; diff --git a/gcc/ada/spark_xrefs.adb b/gcc/ada/spark_xrefs.adb index ebec6c48021..e093139704f 100644 --- a/gcc/ada/spark_xrefs.adb +++ b/gcc/ada/spark_xrefs.adb @@ -23,7 +23,8 @@ -- -- ------------------------------------------------------------------------------ -with Output; use Output; +with Output; use Output; +with Sem_Util; use Sem_Util; package body SPARK_Xrefs is @@ -81,17 +82,13 @@ package body SPARK_Xrefs is Write_Int (Int (ASR.Scope_Num)); Write_Str (" Scope_Name = """); - if ASR.Scope_Name /= null then - Write_Str (ASR.Scope_Name.all); - end if; + Write_Str (Unique_Name (ASR.Scope_Id)); Write_Char ('"'); Write_Str (" From = "); Write_Int (Int (ASR.From_Xref)); Write_Str (" To = "); Write_Int (Int (ASR.To_Xref)); - Write_Str (" Scope_Entity = "); - Write_Int (Int (ASR.Scope_Entity)); Write_Eol; end; end loop; @@ -111,9 +108,7 @@ package body SPARK_Xrefs is Write_Int (Int (Index)); Write_Str (". Entity_Name = """); - if AXR.Entity_Name /= null then - Write_Str (AXR.Entity_Name.all); - end if; + Write_Str (Unique_Name (AXR.Entity)); Write_Char ('"'); Write_Str (" File_Num = "); diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 962b7afe8d3..e4f1eef1497 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -66,7 +66,7 @@ package SPARK_Xrefs is -- until a proper value is determined. type SPARK_Xref_Record is record - Entity_Name : String_Ptr; + Entity : Entity_Id; -- Pointer to entity name in ALI file File_Num : Nat; @@ -109,7 +109,7 @@ package SPARK_Xrefs is -- determined. type SPARK_Scope_Record is record - Scope_Name : String_Ptr; + Scope_Id : Entity_Id; -- Pointer to scope name in ALI file File_Num : Nat; @@ -131,12 +131,6 @@ package SPARK_Xrefs is To_Xref : Xref_Index; -- Ending index in Xref table for this scope - - -- The following component is only used in-memory, not printed out in - -- ALI file. - - Scope_Entity : Entity_Id := Empty; - -- Entity (subprogram or package) for the scope end record; package SPARK_Scope_Table is new Table.Table ( @@ -193,6 +187,11 @@ package SPARK_Xrefs is -- Name of special variable used in effects to denote reads and writes -- through explicit dereference. + Heap : Entity_Id := Empty; + -- A special entity which denotes the heap object; it should be considered + -- constant, but needs to be variable, because it can only be initialized + -- after the node tables are created. + ----------------- -- Subprograms -- ----------------- -- 2.30.2