* [COMMITTED] ada: Prevent inlining in GNATprove for memory leaks
@ 2024-05-06 9:17 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2024-05-06 9:17 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
From: Yannick Moy <moy@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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2024-05-06 9:17 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2024-05-06 9:17 [COMMITTED] ada: Prevent inlining in GNATprove for memory leaks Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).