From 90a4b3367997dd7327bb1668c0a89c2318e8ef9c Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 26 May 2015 09:35:07 +0000 Subject: [PATCH] inline.adb (Has_Initialized_Type): Adapt to new names. 2015-05-26 Yannick Moy * inline.adb (Has_Initialized_Type): Adapt to new names. * sem_aux.adb, sem_aux.ads (Get_Low_Bound, Number_Components, Subprogram_Body, Subprogram_Body_Entity, Subprogram_Spec, Subprogram_Specification): New query functions used in GNATprove. * sem_disp.adb, sem_disp.ads (Is_Overriding_Subprogram): New query functions used in GNATprove. * sem_util.adb, sem_util.adso (Enclosing_Lib_Unit_Node, Get_Cursor_Type, Get_Return_Object, Get_User_Defined_Eq, Is_Double_Precision_Floating_Point_Type, Is_Single_Precision_Floating_Point_Type): New query functions used in GNATprove. From-SVN: r223674 --- gcc/ada/ChangeLog | 14 +++++ gcc/ada/inline.adb | 2 +- gcc/ada/sem_aux.adb | 133 +++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_aux.ads | 38 +++++++++++-- gcc/ada/sem_disp.adb | 10 ++++ gcc/ada/sem_disp.ads | 3 + gcc/ada/sem_util.adb | 115 +++++++++++++++++++++++++++++-------- gcc/ada/sem_util.ads | 53 +++++++++++++---- 8 files changed, 328 insertions(+), 40 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 457b146b40a..960a118b110 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2015-05-26 Yannick Moy + + * inline.adb (Has_Initialized_Type): Adapt to new names. + * sem_aux.adb, sem_aux.ads (Get_Low_Bound, Number_Components, + Subprogram_Body, Subprogram_Body_Entity, Subprogram_Spec, + Subprogram_Specification): New query functions used in GNATprove. + * sem_disp.adb, sem_disp.ads (Is_Overriding_Subprogram): New + query functions used in GNATprove. + * sem_util.adb, sem_util.adso (Enclosing_Lib_Unit_Node, + Get_Cursor_Type, Get_Return_Object, Get_User_Defined_Eq, + Is_Double_Precision_Floating_Point_Type, + Is_Single_Precision_Floating_Point_Type): New query functions + used in GNATprove. + 2015-05-26 Bob Duff * s-rpc.ads (Partition_ID): Increase maximum Partition_ID to diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index cf53aae810a..b36ec52908e 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -3639,7 +3639,7 @@ package body Inline is -------------------------- function Has_Initialized_Type (E : Entity_Id) return Boolean is - E_Body : constant Node_Id := Get_Subprogram_Body (E); + E_Body : constant Node_Id := Subprogram_Body (E); Decl : Node_Id; begin diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index a6ba49f5da1..63f74d9d63c 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -472,6 +472,19 @@ package body Sem_Aux is end case; end Get_Binary_Nkind; + ------------------- + -- Get_Low_Bound -- + ------------------- + + function Get_Low_Bound (E : Entity_Id) return Node_Id is + begin + if Ekind (E) = E_String_Literal_Subtype then + return String_Literal_Low_Bound (E); + else + return Low_Bound (Scalar_Range (E)); + end if; + end Get_Low_Bound; + ------------------ -- Get_Rep_Item -- ------------------ @@ -1361,6 +1374,35 @@ package body Sem_Aux is return Empty; end Next_Tag_Component; + ----------------------- + -- Number_Components -- + ----------------------- + + function Number_Components (Typ : Entity_Id) return Pos is + N : Int; + Comp : Entity_Id; + + begin + N := 0; + + -- We do not call Einfo.First_Component_Or_Discriminant, as this + -- function does not skip completely hidden discriminants, which we + -- want to skip here. + + if Has_Discriminants (Typ) then + Comp := First_Discriminant (Typ); + else + Comp := First_Component (Typ); + end if; + + while Present (Comp) loop + N := N + 1; + Comp := Next_Component_Or_Discriminant (Comp); + end loop; + + return N; + end Number_Components; + -------------------------- -- Number_Discriminants -- -------------------------- @@ -1419,6 +1461,97 @@ package body Sem_Aux is return N; end Package_Specification; + --------------------- + -- Subprogram_Body -- + --------------------- + + function Subprogram_Body (E : Entity_Id) return Node_Id is + Body_E : constant Entity_Id := Subprogram_Body_Entity (E); + + begin + if No (Body_E) then + return Empty; + else + return Parent (Subprogram_Specification (Body_E)); + end if; + end Subprogram_Body; + + ---------------------------- + -- Subprogram_Body_Entity -- + ---------------------------- + + function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id is + N : Node_Id; + + begin + -- Retrieve the declaration for E + + N := Parent (Subprogram_Specification (E)); + + -- If this declaration is not a subprogram body, then it must be a + -- subprogram declaration, from which we can retrieve the entity for + -- the corresponding subprogram body if any. + + if Nkind (N) = N_Subprogram_Body then + return E; + else + return Corresponding_Body (N); + end if; + end Subprogram_Body_Entity; + + --------------------- + -- Subprogram_Spec -- + --------------------- + + function Subprogram_Spec (E : Entity_Id) return Node_Id is + N : Node_Id; + + begin + -- Retrieve the declaration for E + + N := Parent (Subprogram_Specification (E)); + + -- This declaration is either subprogram declaration or a subprogram + -- body, in which case return Empty. + + if Nkind (N) = N_Subprogram_Declaration then + return N; + else + return Empty; + end if; + end Subprogram_Spec; + + ------------------------------ + -- Subprogram_Specification -- + ------------------------------ + + function Subprogram_Specification (E : Entity_Id) return Node_Id is + N : Node_Id; + + begin + N := Parent (E); + + if Nkind (N) = N_Defining_Program_Unit_Name then + N := Parent (N); + end if; + + -- If the Parent pointer of E is not a subprogram specification node + -- (going through an intermediate N_Defining_Program_Unit_Name node + -- for subprogram units), then E is an inherited operation. Its parent + -- points to the type derivation that produces the inheritance: that's + -- the node that generates the subprogram specification. Its alias + -- is the parent subprogram, and that one points to a subprogram + -- declaration, or to another type declaration if this is a hierarchy + -- of derivations. + + if Nkind (N) not in N_Subprogram_Specification then + pragma Assert (Present (Alias (E))); + N := Subprogram_Specification (Alias (E)); + end if; + + return N; + end Subprogram_Specification; + --------------- -- Tree_Read -- --------------- diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads index bb539e2e17a..e3117f253f4 100644 --- a/gcc/ada/sem_aux.ads +++ b/gcc/ada/sem_aux.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -158,6 +158,9 @@ package Sem_Aux is -- referencing this entity. It is an error to call this function if Ekind -- (Op) /= E_Operator. + function Get_Low_Bound (E : Entity_Id) return Node_Id; + -- For an index subtype or string literal subtype, return its low bound + function Get_Unary_Nkind (Op : Entity_Id) return Node_Kind; -- Op must be an entity with an Ekind of E_Operator. This function returns -- the Nkind value that would be used to construct a unary operator node @@ -369,6 +372,10 @@ package Sem_Aux is -- The result returned is the next _Tag field in this record, or Empty -- if this is the last such field. + function Number_Components (Typ : Entity_Id) return Pos; + -- Typ is a record type, yields number of components (including + -- discriminants) in type. + function Number_Discriminants (Typ : Entity_Id) return Pos; -- Typ is a type with discriminants, yields number of discriminants in type @@ -381,6 +388,30 @@ package Sem_Aux is -- derived type, and the subtype is not an unconstrained array subtype -- (RM 3.3(23.10/3)). + function Package_Specification (Pack_Id : Entity_Id) return Node_Id; + -- Given an entity for a package or generic package, return corresponding + -- package specification. Simplifies handling of child units, and better + -- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)). + + function Subprogram_Body (E : Entity_Id) return Node_Id; + -- Given an entity for a subprogram (spec or body), return the + -- corresponding subprogram body if any, or else Empty. + + function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id; + -- Given an entity for a subprogram (spec or body), return the entity + -- corresponding to the subprogram body, which may be the same as E or + -- Empty if no body is available. + + function Subprogram_Spec (E : Entity_Id) return Node_Id; + -- Given an entity for a subprogram spec, return the corresponding + -- subprogram spec if any, or else Empty. + + function Subprogram_Specification (E : Entity_Id) return Node_Id; + -- Given an entity for a subprogram, return the corresponding subprogram + -- specification. If the entity is an inherited subprogram without + -- specification itself, return the specification of the inherited + -- subprogram. + function Ultimate_Alias (Prim : Entity_Id) return Entity_Id; pragma Inline (Ultimate_Alias); -- Return the last entity in the chain of aliased entities of Prim. If Prim @@ -393,9 +424,4 @@ package Sem_Aux is -- it returns the subprogram, task or protected body node for it. The unit -- may be a child unit with any number of ancestors. - function Package_Specification (Pack_Id : Entity_Id) return Node_Id; - -- Given an entity for a package or generic package, return corresponding - -- package specification. Simplifies handling of child units, and better - -- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)). - end Sem_Aux; diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index 55e5dcd8686..52eda74da9b 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -2239,6 +2239,16 @@ package body Sem_Disp is end if; end Is_Inherited_Public_Operation; + ------------------------------ + -- Is_Overriding_Subprogram -- + ------------------------------ + + function Is_Overriding_Subprogram (E : Entity_Id) return Boolean is + Inherited : constant Subprogram_List := Inherited_Subprograms (E); + begin + return Inherited'Length > 0; + end Is_Overriding_Subprogram; + -------------------------- -- Is_Tag_Indeterminate -- -------------------------- diff --git a/gcc/ada/sem_disp.ads b/gcc/ada/sem_disp.ads index 21d1da5fe39..d2aa620ddb7 100644 --- a/gcc/ada/sem_disp.ads +++ b/gcc/ada/sem_disp.ads @@ -129,6 +129,9 @@ package Sem_Disp is function Is_Null_Interface_Primitive (E : Entity_Id) return Boolean; -- Returns True if E is a null procedure that is an interface primitive + function Is_Overriding_Subprogram (E : Entity_Id) return Boolean; + -- Returns True if E is an overriding subprogram + function Is_Tag_Indeterminate (N : Node_Id) return Boolean; -- Returns true if the expression N is tag-indeterminate. An expression -- is tag-indeterminate if it is a call that dispatches on result, and all diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 2bf22f6ca6d..99bf2bab030 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -5674,6 +5674,25 @@ package body Sem_Util is end if; end Enclosing_Comp_Unit_Node; + ----------------------------- + -- Enclosing_Lib_Unit_Node -- + ----------------------------- + + function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id is + Encl_Unit : Node_Id; + + begin + Encl_Unit := Enclosing_Comp_Unit_Node (N); + + while Present (Encl_Unit) + and then Nkind (Unit (Encl_Unit)) = N_Subunit + loop + Encl_Unit := Library_Unit (Encl_Unit); + end loop; + + return Encl_Unit; + end Enclosing_Lib_Unit_Node; + -------------------------- -- Enclosing_CPP_Parent -- -------------------------- @@ -7417,6 +7436,11 @@ package body Sem_Util is return Cursor; end Get_Cursor_Type; + function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id is + begin + return Etype (Get_Iterable_Type_Primitive (Typ, Name_First)); + end Get_Cursor_Type; + ------------------------------- -- Get_Default_External_Name -- ------------------------------- @@ -7771,34 +7795,24 @@ package body Sem_Util is return R; end Get_Renamed_Entity; - ------------------------- - -- Get_Subprogram_Body -- - ------------------------- + ----------------------- + -- Get_Return_Object -- + ----------------------- - function Get_Subprogram_Body (E : Entity_Id) return Node_Id is + function Get_Return_Object (N : Node_Id) return Entity_Id is Decl : Node_Id; begin - Decl := Unit_Declaration_Node (E); - - if Nkind (Decl) = N_Subprogram_Body then - return Decl; - - -- The below comment is bad, because it is possible for - -- Nkind (Decl) to be an N_Subprogram_Body_Stub ??? - - else -- Nkind (Decl) = N_Subprogram_Declaration - - if Present (Corresponding_Body (Decl)) then - return Unit_Declaration_Node (Corresponding_Body (Decl)); - - -- Imported subprogram case + Decl := First (Return_Object_Declarations (N)); + while Present (Decl) loop + exit when Nkind (Decl) = N_Object_Declaration + and then Is_Return_Object (Defining_Identifier (Decl)); + Next (Decl); + end loop; - else - return Empty; - end if; - end if; - end Get_Subprogram_Body; + pragma Assert (Present (Decl)); + return Defining_Identifier (Decl); + end Get_Return_Object; --------------------------- -- Get_Subprogram_Entity -- @@ -7878,6 +7892,33 @@ package body Sem_Util is return Task_Body_Procedure (Underlying_Type (Root_Type (E))); end Get_Task_Body_Procedure; + ------------------------- + -- Get_User_Defined_Eq -- + ------------------------- + + function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id is + Prim : Elmt_Id; + Op : Entity_Id; + + begin + Prim := First_Elmt (Collect_Primitive_Operations (E)); + while Present (Prim) loop + Op := Node (Prim); + + if Chars (Op) = Name_Op_Eq + and then Etype (Op) = Standard_Boolean + and then Etype (First_Formal (Op)) = E + and then Etype (Next_Formal (First_Formal (Op))) = E + then + return Op; + end if; + + Next_Elmt (Prim); + end loop; + + return Empty; + end Get_User_Defined_Eq; + ----------------------- -- Has_Access_Values -- ----------------------- @@ -11242,6 +11283,20 @@ package body Sem_Util is end if; end Is_Descendent_Of; + --------------------------------------------- + -- Is_Double_Precision_Floating_Point_Type -- + --------------------------------------------- + + function Is_Double_Precision_Floating_Point_Type + (E : Entity_Id) return Boolean is + begin + return Is_Floating_Point_Type (E) + and then Machine_Radix_Value (E) = Uint_2 + and then Machine_Mantissa_Value (E) = UI_From_Int (53) + and then Machine_Emax_Value (E) = Uint_2 ** Uint_10 + and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_10); + end Is_Double_Precision_Floating_Point_Type; + ----------------------------- -- Is_Effectively_Volatile -- ----------------------------- @@ -12703,6 +12758,20 @@ package body Sem_Util is end if; end Is_Selector_Name; + --------------------------------------------- + -- Is_Single_Precision_Floating_Point_Type -- + --------------------------------------------- + + function Is_Single_Precision_Floating_Point_Type + (E : Entity_Id) return Boolean is + begin + return Is_Floating_Point_Type (E) + and then Machine_Radix_Value (E) = Uint_2 + and then Machine_Mantissa_Value (E) = Uint_24 + and then Machine_Emax_Value (E) = Uint_2 ** Uint_7 + and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_7); + end Is_Single_Precision_Floating_Point_Type; + ------------------------------------- -- Is_SPARK_05_Initialization_Expr -- ------------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index cf74bf75dbc..8394b105586 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -529,9 +529,16 @@ package Sem_Util is -- related expression evaluates to True. function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id; - -- Returns the enclosing N_Compilation_Unit Node that is the root of a + -- Returns the enclosing N_Compilation_Unit node that is the root of a -- subtree containing N. + function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id; + -- Returns the N_Compilation_Unit node of the library unit that is directly + -- or indirectly (through a subunit) at the root of a subtree containing + -- N. This may be either the same as Enclosing_Comp_Unit_Node, or if + -- Enclosing_Comp_Unit_Node returns a subunit, then the corresponding + -- library unit. + function Enclosing_CPP_Parent (Typ : Entity_Id) return Entity_Id; -- Returns the closest ancestor of Typ that is a CPP type. @@ -814,10 +821,15 @@ package Sem_Util is function Get_Cursor_Type (Aspect : Node_Id; Typ : Entity_Id) return Entity_Id; - -- Find Cursor type in scope of formal container Typ, by locating primitive - -- operation First. For use in resolving the other primitive operations - -- of an Iterable type and expanding loops and quantified expressions - -- over formal containers. + -- Find Cursor type in scope of type Typ with Iterable aspect, by locating + -- primitive operation First. For use in resolving the other primitive + -- operations of an Iterable type and expanding loops and quantified + -- expressions over formal containers. + + function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id; + -- Find Cursor type in scope of type Typ with Iterable aspect, by locating + -- primitive operation First. For use after resolving the primitive + -- operations of an Iterable type. function Get_Default_External_Name (E : Node_Or_Entity_Id) return Node_Id; -- This is used to construct the string literal node representing a @@ -906,22 +918,25 @@ package Sem_Util is -- not a renamed entity, returns its argument. It is an error to call this -- with any other kind of entity. + function Get_Return_Object (N : Node_Id) return Entity_Id; + -- Given an extended return statement, return the corresponding return + -- object, identified as the one for which Is_Return_Object = True. + function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id; -- Nod is either a procedure call statement, or a function call, or an -- accept statement node. This procedure finds the Entity_Id of the related -- subprogram or entry and returns it, or if no subprogram can be found, -- returns Empty. - function Get_Subprogram_Body (E : Entity_Id) return Node_Id; - -- Given the entity for a subprogram (E_Function or E_Procedure), return - -- the corresponding N_Subprogram_Body node. If the corresponding body - -- is missing (as for an imported subprogram), return Empty. - function Get_Task_Body_Procedure (E : Entity_Id) return Node_Id; pragma Inline (Get_Task_Body_Procedure); -- Given an entity for a task type or subtype, retrieves the -- Task_Body_Procedure field from the corresponding task type declaration. + function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id; + -- For a type entity, return the entity of the primitive equality function + -- for the type if it exists, otherwise return Empty. + function Has_Access_Values (T : Entity_Id) return Boolean; -- Returns true if type or subtype T is an access type, or has a component -- (at any recursive level) that is an access type. This is a conservative @@ -1248,6 +1263,15 @@ package Sem_Util is -- This is the RM definition, a type is a descendent of another type if it -- is the same type or is derived from a descendent of the other type. + function Is_Double_Precision_Floating_Point_Type + (E : Entity_Id) return Boolean; + -- Return whether E is a double precision floating point type, + -- characterized by: + -- . machine_radix = 2 + -- . machine_mantissa = 53 + -- . machine_emax = 2**10 + -- . machine_emin = 3 - machine_emax + function Is_Effectively_Volatile (Id : Entity_Id) return Boolean; -- The SPARK property "effectively volatile" applies to both types and -- objects. To qualify as such, an entity must be either volatile or be @@ -1410,6 +1434,15 @@ package Sem_Util is -- represent use of the N_Identifier node for a true identifier, when -- normally such nodes represent a direct name. + function Is_Single_Precision_Floating_Point_Type + (E : Entity_Id) return Boolean; + -- Return whether E is a single precision floating point type, + -- characterized by: + -- . machine_radix = 2 + -- . machine_mantissa = 24 + -- . machine_emax = 2**7 + -- . machine_emin = 3 - machine_emax + function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean; -- Determines if the tree referenced by N represents an initialization -- expression in SPARK 2005, suitable for initializing an object in an -- 2.30.2