From 9afbf898ce89f6bcb314ddf03da20abdf0ac79cd Mon Sep 17 00:00:00 2001
From: Piotr Trojanek <trojanek@adacore.com>
Date: Thu, 7 Dec 2023 00:27:16 +0100
Subject: [PATCH] ada: More aggressive inlining of subprogram calls in
GNATprove mode
Previously if a subprogram call could not be inlined in GNATprove mode,
then all subsequent calls to the same subprogram were not inlined
either (because a failed attempt to inline clears flag Is_Inlined_Always
and we tested this flag when attempting to inline subsequent calls).
Now a failure in inlining of a particular call does not prevent inlining
of subsequent calls to the same subprogram, except when inlining failed
because the subprogram was detected to be recursive (which clears the
Is_Inlined flag that we now examine).
This change allows more checks to be proved and reduces interactions
between inlining and SPARK legality checks.
gcc/ada/
* sem_ch6.adb (Analyze_Subprogram_Specification): Set Is_Inlined
flag by default in GNATprove mode.
* sem_res.adb (Resolve_Call): Only look at flag which is cleared
when inlined subprogram is detected to be recursive.
---
gcc/ada/sem_ch6.adb | 5 ++++-
gcc/ada/sem_res.adb | 11 +++++++----
2 files changed, 11 insertions(+), 5 deletions(-)
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index da6f6c40c92b..bdfe446d014c 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -5325,10 +5325,13 @@ package body Sem_Ch6 is
-- Flag Is_Inlined_Always is True by default, and reversed to False for
-- those subprograms which could be inlined in GNATprove mode (because
- -- Body_To_Inline is non-Empty) but should not be inlined.
+ -- Body_To_Inline is non-Empty) but should not be inlined. Flag
+ -- Is_Inlined is True by default and reversed to False when inlining
+ -- fails because the subprogram is detected to be recursive.
if GNATprove_Mode then
Set_Is_Inlined_Always (Designator);
+ Set_Is_Inlined (Designator);
end if;
-- Introduce new scope for analysis of the formals and the return type
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index d81a5af9032e..cfcbb94af89d 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7193,7 +7193,7 @@ package body Sem_Res is
-- In GNATprove mode, expansion is disabled, but we want to inline some
-- subprograms to facilitate formal verification. Indirect calls through
-- a subprogram type or within a generic cannot be inlined. Inlining is
- -- performed only for calls subject to SPARK_Mode on.
+ -- performed only for calls subject to SPARK_Mode => On.
elsif GNATprove_Mode
and then SPARK_Mode = On
@@ -7206,10 +7206,13 @@ package body Sem_Res is
if Nkind (Nam_Decl) = N_Subprogram_Declaration then
Body_Id := Corresponding_Body (Nam_Decl);
- -- Nothing to do if the subprogram is not eligible for inlining in
- -- GNATprove mode, or inlining is disabled with switch -gnatdm
+ -- Nothing to do if the subprogram is not inlined (because it is
+ -- recursive, directly or indirectly), or is not eligible for
+ -- inlining GNATprove mode (because of properties of the
+ -- subprogram itself), or inlining has been disabled with switch
+ -- -gnatdm.
- if not Is_Inlined_Always (Nam_UA)
+ if not Is_Inlined (Nam_UA)
or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id)
or else Debug_Flag_M
then
--
GitLab