diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2023-12-07 00:27:16 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2024-01-09 14:13:31 +0100 |
commit | 9afbf898ce89f6bcb314ddf03da20abdf0ac79cd (patch) | |
tree | aa65a5814bee240c7a0018a152eedacc4c96f7fc | |
parent | 00a97303c2ab27263b18a008a389c3567650123b (diff) | |
download | gcc-9afbf898ce89f6bcb314ddf03da20abdf0ac79cd.zip gcc-9afbf898ce89f6bcb314ddf03da20abdf0ac79cd.tar.gz gcc-9afbf898ce89f6bcb314ddf03da20abdf0ac79cd.tar.bz2 |
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.
-rw-r--r-- | gcc/ada/sem_ch6.adb | 5 | ||||
-rw-r--r-- | 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 da6f6c4..bdfe446 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 d81a5af..cfcbb94 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 |