From 9d98b6d8dcaed2b0f5c87418ca2036d1bdc5a881 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 10 Oct 2019 15:23:47 +0000 Subject: [PATCH] [Ada] Do not inline subprograms with deep parameter/result in GNATprove 2019-10-10 Yannick Moy gcc/ada/ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add subprograms with deep parameter or result type as not candidates for inlining. From-SVN: r276821 --- gcc/ada/ChangeLog | 7 +-- gcc/ada/inline.adb | 112 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 116 insertions(+), 3 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index db07f3b845a..6eca0b8b7cc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,4 +1,5 @@ -2019-10-10 Vadim Godunko +2019-10-10 Yannick Moy - * libgnat/g-exptty.ads (TTY_Process_Descriptor): Set default - value for Process. \ No newline at end of file + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add subprograms + with deep parameter or result type as not candidates for + inlining. \ No newline at end of file diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index dab2275b766..be2259479d2 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1493,6 +1493,12 @@ package body Inline is (Spec_Id : Entity_Id; Body_Id : Entity_Id) return Boolean is + function Has_Formal_Or_Result_Of_Deep_Type + (Id : Entity_Id) return Boolean; + -- Returns true if the subprogram has at least one formal parameter or + -- a return type of a deep type: either an access type or a composite + -- type containing an access type. + function Has_Formal_With_Discriminant_Dependent_Fields (Id : Entity_Id) return Boolean; -- Returns true if the subprogram has at least one formal parameter of @@ -1518,6 +1524,104 @@ package body Inline is -- knowledge of the SPARK boundary is needed to determine exactly -- traversal functions. + --------------------------------------- + -- Has_Formal_Or_Result_Of_Deep_Type -- + --------------------------------------- + + function Has_Formal_Or_Result_Of_Deep_Type + (Id : Entity_Id) return Boolean + is + function Is_Deep (Typ : Entity_Id) return Boolean; + -- Return True if Typ is deep: either an access type or a composite + -- type containing an access type. + + ------------- + -- Is_Deep -- + ------------- + + function Is_Deep (Typ : Entity_Id) return Boolean is + begin + case Type_Kind'(Ekind (Typ)) is + when Access_Kind => + return True; + + when E_Array_Type + | E_Array_Subtype + => + return Is_Deep (Component_Type (Typ)); + + when Record_Kind => + declare + Comp : Entity_Id := First_Component_Or_Discriminant (Typ); + begin + while Present (Comp) loop + if Is_Deep (Etype (Comp)) then + return True; + end if; + Next_Component_Or_Discriminant (Comp); + end loop; + end; + return False; + + when Scalar_Kind + | E_String_Literal_Subtype + | Concurrent_Kind + | Incomplete_Kind + | E_Exception_Type + | E_Subprogram_Type + => + return False; + + when E_Private_Type + | E_Private_Subtype + | E_Limited_Private_Type + | E_Limited_Private_Subtype + => + -- Conservatively consider that the type might be deep if + -- its completion has not been seen yet. + + if No (Underlying_Type (Typ)) then + return True; + else + return Is_Deep (Underlying_Type (Typ)); + end if; + end case; + end Is_Deep; + + -- Local variables + + Subp_Id : constant Entity_Id := Ultimate_Alias (Id); + Formal : Entity_Id; + Formal_Typ : Entity_Id; + + -- Start of processing for Has_Formal_Or_Result_Of_Deep_Type + + begin + -- Inspect all parameters of the subprogram looking for a formal + -- of a deep type. + + Formal := First_Formal (Subp_Id); + while Present (Formal) loop + Formal_Typ := Etype (Formal); + + if Is_Deep (Formal_Typ) then + return True; + end if; + + Next_Formal (Formal); + end loop; + + -- Check whether this is a function whose return type is deep + + if Ekind (Subp_Id) = E_Function + and then Is_Deep (Etype (Subp_Id)) + then + return True; + end if; + + return False; + end Has_Formal_Or_Result_Of_Deep_Type; + --------------------------------------------------- -- Has_Formal_With_Discriminant_Dependent_Fields -- --------------------------------------------------- @@ -1777,6 +1881,14 @@ package body Inline is elsif Has_Formal_With_Discriminant_Dependent_Fields (Id) then return False; + -- Do not inline subprograms with a formal parameter or return type of + -- a deep type, as in that case inlining might generate code that + -- violates borrow-checking rules of SPARK 3.10 even if the original + -- code did not. + + elsif Has_Formal_Or_Result_Of_Deep_Type (Id) then + return False; + -- Do not inline subprograms which may be traversal functions. Such -- inlining introduces temporary variables of named access type for -- which assignments are move instead of borrow/observe, possibly -- 2.30.2