From 52c1498c862bf1363560f8d487b1af327fd9256b Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 30 Jul 2014 12:41:59 +0000 Subject: [PATCH] einfo.ads (Is_Inlined): Document new use in GNATprove mode. 2014-07-30 Yannick Moy * einfo.ads (Is_Inlined): Document new use in GNATprove mode. * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add comments to explain rationale for inlining or not in GNATprove mode. (Expand_Inlined_Call): In GNATprove mode, set Is_Inlined flag to False when inlining is not possible. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Set Is_Inlined flag to indicate that subprogram is fully inlined. To be reversed if inlining problem is found. * sem_res.adb (Resolve_Call): Set Is_Inlined flag to False when call in potentially unevaluated context. From-SVN: r213255 --- gcc/ada/ChangeLog | 13 +++++++++++++ gcc/ada/einfo.ads | 4 ++++ gcc/ada/inline.adb | 36 +++++++++++++++++++++++------------- gcc/ada/sem_ch6.adb | 3 +++ gcc/ada/sem_res.adb | 9 ++++++++- 5 files changed, 51 insertions(+), 14 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 4b379a2c8f9..f34919648c2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2014-07-30 Yannick Moy + + * einfo.ads (Is_Inlined): Document new use in GNATprove mode. + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add comments + to explain rationale for inlining or not in GNATprove mode. + (Expand_Inlined_Call): In GNATprove mode, set Is_Inlined flag + to False when inlining is not possible. + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Set Is_Inlined + flag to indicate that subprogram is fully inlined. To be reversed + if inlining problem is found. + * sem_res.adb (Resolve_Call): Set Is_Inlined flag to False when + call in potentially unevaluated context. + 2014-07-30 Jose Ruiz * s-tarest.adb, s-tarest.ads: Fix comments. diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index c20e96454d1..6d03646ef6e 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2477,6 +2477,10 @@ package Einfo is -- inherited by their instances. It is also set on the body entities -- of inlined subprograms. See also Has_Pragma_Inline. +-- Is_Inlined is also set for subprograms that are always inlined in +-- GNATprove mode. GNATprove uses this flag to know when a body does not +-- need to be analyzed. + -- Is_Instantiated (Flag126) -- Defined in generic packages and generic subprograms. Set if the unit -- is instantiated from somewhere in the extended main source unit. This diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 57a663d6014..9701f3ab92f 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1558,9 +1558,14 @@ package body Inline is Id := Body_Id; end if; - -- General note. The following comments clearly say what cannot be - -- inlined, but they do not give any clue on the motivation for the - -- exclusion. It would be good to document the motivations ??? + -- Only local subprograms without contracts are inlined in GNATprove + -- mode, as these are the subprograms which a user is not interested in + -- analyzing in isolation, but rather in the context of their call. This + -- is a convenient convention, that could be changed for an explicit + -- pragma/aspect one day. + + -- In a number of special cases, inlining is not desirable or not + -- possible, see below. -- Do not inline unit-level subprograms @@ -1584,19 +1589,22 @@ package body Inline is then return False; - -- Do not inline expression functions + -- Do not inline expression functions, which are directly inlined at the + -- prover level. elsif (Present (Spec_Id) and then Is_Expression_Function (Spec_Id)) or else Is_Expression_Function (Body_Id) then return False; - -- Do not inline generic subprogram instances + -- Do not inline generic subprogram instances. The visibility rules of + -- generic instances plays badly with inlining. elsif Is_Generic_Instance (Spec_Id) then return False; - -- Only inline subprograms whose body is marked SPARK_Mode On + -- Only inline subprograms whose body is marked SPARK_Mode On. Other + -- subprogram bodies should not be analyzed. elsif No (SPARK_Pragma (Body_Id)) or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On @@ -2952,11 +2960,11 @@ package body Inline is function Process_Sloc (Nod : Node_Id) return Traverse_Result; -- If the call being expanded is that of an internal subprogram, set the -- sloc of the generated block to that of the call itself, so that the - -- expansion is skipped by the "next" command in gdb. - -- Same processing for a subprogram in a predefined file, e.g. - -- Ada.Tags. If Debug_Generated_Code is true, suppress this change to - -- simplify our own development. Same in in GNATprove mode, to ensure - -- that warnings and diagnostics point to the proper location. + -- expansion is skipped by the "next" command in gdb. Same processing + -- for a subprogram in a predefined file, e.g. Ada.Tags. If + -- Debug_Generated_Code is true, suppress this change to simplify our + -- own development. Same in GNATprove mode, to ensure that warnings and + -- diagnostics point to the proper location. procedure Reset_Dispatching_Calls (N : Node_Id); -- In subtree N search for occurrences of dispatching calls that use the @@ -3634,8 +3642,9 @@ package body Inline is if Present (Renamed_Object (F)) then -- If expander is active, it is an error to try to inline a - -- recursive program. In GNATprove mode, just indicate that - -- the inlining will not happen. + -- recursive program. In GNATprove mode, just indicate that the + -- inlining will not happen, and mark the subprogram as not always + -- inlined. if Expander_Active then Error_Msg_N @@ -3643,6 +3652,7 @@ package body Inline is else Cannot_Inline ("cannot inline call to recursive subprogram?", N, Subp); + Set_Is_Inlined (Subp, False); end if; return; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index a7cfce25a7f..4d0264f1452 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3483,6 +3483,7 @@ package body Sem_Ch6 is and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) and then not Body_Has_Contract then + Set_Is_Inlined (Spec_Id, True); Build_Body_To_Inline (N, Spec_Id); end if; @@ -3510,6 +3511,7 @@ package body Sem_Ch6 is and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) and then not Body_Has_Contract then + Set_Is_Inlined (Spec_Id, True); Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id); end if; @@ -3644,6 +3646,7 @@ package body Sem_Ch6 is and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration then Set_Body_To_Inline (Parent (Parent (Spec_Id)), Empty); + Set_Is_Inlined (Spec_Id, False); end if; -- Check completion, and analyze the statements diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 10edd1a77e9..332bc6090c7 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6222,7 +6222,14 @@ package body Sem_Res is if Nkind (Decl) = N_Subprogram_Declaration and then Present (Body_To_Inline (Decl)) then - Expand_Inlined_Call (N, Nam_Alias, Nam); + if Is_Potentially_Unevaluated (N) then + Error_Msg_NE ("?cannot inline call to &", N, Nam); + Error_Msg_N + ("\call appears in potentially unevaluated context", N); + Set_Is_Inlined (Nam, False); + else + Expand_Inlined_Call (N, Nam_Alias, Nam); + end if; end if; end; end if;