From: Yannick Moy <m...@adacore.com> In some cases, inlining a call in GNATprove could lead to missing a memory leak. Recognize such cases and do not inline such calls.
gcc/ada/ * inline.adb (Call_Can_Be_Inlined_In_GNATprove_Mode): Add case to prevent inlining of call. * inline.ads: Likewise. * sem_res.adb (Resolve_Call): Update comment and message. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/inline.adb | 58 +++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/inline.ads | 5 ++-- gcc/ada/sem_res.adb | 5 ++-- 3 files changed, 64 insertions(+), 4 deletions(-) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 2ec92ca9dff..98bed860760 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1460,10 +1460,47 @@ package body Inline is (N : Node_Id; Subp : Entity_Id) return Boolean is + function Has_Dereference (N : Node_Id) return Boolean; + -- Return whether N contains an explicit dereference + + --------------------- + -- Has_Dereference -- + --------------------- + + function Has_Dereference (N : Node_Id) return Boolean is + + function Process (N : Node_Id) return Traverse_Result; + -- Process one node in search for dereference + + ------------- + -- Process -- + ------------- + + function Process (N : Node_Id) return Traverse_Result is + begin + if Nkind (N) = N_Explicit_Dereference then + return Abandon; + else + return OK; + end if; + end Process; + + function Traverse is new Traverse_Func (Process); + -- Traverse tree to look for dereference + + begin + return Traverse (N) = Abandon; + end Has_Dereference; + + -- Local variables + F : Entity_Id; A : Node_Id; begin + -- Check if inlining may lead to missing a check on type conversion of + -- input parameters otherwise. + F := First_Formal (Subp); A := First_Actual (N); while Present (F) loop @@ -1480,6 +1517,27 @@ package body Inline is Next_Actual (A); end loop; + -- Check if inlining may lead to introducing temporaries of access type, + -- which can lead to missing checks for memory leaks. This can only + -- come from an (IN-)OUT parameter transformed into a renaming by SPARK + -- expansion, whose side-effects are removed, and a dereference in the + -- corresponding actual. If the formal itself is of a deep type (it has + -- access subcomponents), the subprogram already cannot be inlined in + -- GNATprove mode. + + F := First_Formal (Subp); + A := First_Actual (N); + while Present (F) loop + if Ekind (F) /= E_In_Parameter + and then Has_Dereference (A) + then + return False; + end if; + + Next_Formal (F); + Next_Actual (A); + end loop; + return True; end Call_Can_Be_Inlined_In_GNATprove_Mode; diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index 3df0a01b65d..bc90c0ce6d8 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -146,8 +146,9 @@ package Inline is (N : Node_Id; Subp : Entity_Id) return Boolean; -- Returns False if the call in node N to subprogram Subp cannot be inlined - -- in GNATprove mode, because it may lead to missing a check on type - -- conversion of input parameters otherwise. Returns True otherwise. + -- in GNATprove mode, because it may otherwise lead to missing a check + -- on type conversion of input parameters, or a missing memory leak on + -- an output parameter. Returns True otherwise. function Can_Be_Inlined_In_GNATprove_Mode (Spec_Id : Entity_Id; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 075c0d85ccd..67062c6b32b 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7329,11 +7329,12 @@ package body Sem_Res is ("cannot inline & (in while loop condition)?", N, Nam_UA); -- Do not inline calls which would possibly lead to missing a - -- type conversion check on an input parameter. + -- type conversion check on an input parameter or a memory leak + -- on an output parameter. elsif not Call_Can_Be_Inlined_In_GNATprove_Mode (N, Nam) then Cannot_Inline - ("cannot inline & (possible check on input parameters)?", + ("cannot inline & (possible check on parameters)?", N, Nam_UA); -- Otherwise, inline the call, issuing an info message when -- 2.43.2