[COMMITTED] ada: More aggressive inlining of subprogram calls in GNATprove mode
Checks
| Context |
Check |
Description |
| snail/gcc-patch-check |
success
|
Github commit url
|
Commit Message
From: Piotr Trojanek <trojanek@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_ch6.adb | 5 ++++-
gcc/ada/sem_res.adb | 11 +++++++----
2 files changed, 11 insertions(+), 5 deletions(-)
@@ -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
@@ -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