Index: sinfo.ads =================================================================== --- sinfo.ads (revision 213201) +++ sinfo.ads (working copy) @@ -817,7 +817,7 @@ -- set, it means that the front end can assure no overlap of operands. -- Body_To_Inline (Node3-Sem) - -- present in subprogram declarations. Denotes analyzed but unexpanded + -- Present in subprogram declarations. Denotes analyzed but unexpanded -- body of subprogram, to be used when inlining calls. Present when the -- subprogram has an Inline pragma and inlining is enabled. If the -- declaration is completed by a renaming_as_body, and the renamed en- Index: inline.adb =================================================================== --- inline.adb (revision 213201) +++ inline.adb (working copy) @@ -44,8 +44,10 @@ with Sem_Ch10; use Sem_Ch10; with Sem_Ch12; use Sem_Ch12; with Sem_Eval; use Sem_Eval; +with Sem_Prag; use Sem_Prag; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; +with Sinput; use Sinput; with Snames; use Snames; with Stand; use Stand; with Uname; use Uname; @@ -1257,12 +1259,13 @@ end if; end if; - -- We do not inline a subprogram that is too large, unless it is - -- marked Inline_Always. This pragma does not suppress the other - -- checks on inlining (forbidden declarations, handlers, etc). + -- We do not inline a subprogram that is too large, unless it is marked + -- Inline_Always or we are in GNATprove mode. This pragma does not + -- suppress the other checks on inlining (forbidden declarations, + -- handlers, etc). if Stat_Count > Max_Size - and then not Has_Pragma_Inline_Always (Subp) + and then not (Has_Pragma_Inline_Always (Subp) or else GNATprove_Mode) then Cannot_Inline ("cannot inline& (body too large)?", N, Subp); return; @@ -1454,6 +1457,152 @@ end if; end Cannot_Inline; + -------------------------------------- + -- Can_Be_Inlined_In_GNATprove_Mode -- + -------------------------------------- + + function Can_Be_Inlined_In_GNATprove_Mode + (Spec_Id : Entity_Id; + Body_Id : Entity_Id) return Boolean + is + function Has_Some_Contract (Id : Entity_Id) return Boolean; + -- Returns True if subprogram Id has any contract (Pre, Post, Global, + -- Depends, etc.) + + function In_Some_Private_Part (N : Node_Id) return Boolean; + -- Returns True if node N is defined in the private part of a package + + function In_Unit_Body (N : Node_Id) return Boolean; + -- Returns True if node N is defined in the body of a unit + + function Is_Expression_Function (Id : Entity_Id) return Boolean; + -- Returns True if subprogram Id was defined originally as an expression + -- function. + + ----------------------- + -- Has_Some_Contract -- + ----------------------- + + function Has_Some_Contract (Id : Entity_Id) return Boolean is + Items : constant Node_Id := Contract (Id); + begin + return Present (Items) + and then (Present (Pre_Post_Conditions (Items)) + or else + Present (Contract_Test_Cases (Items)) + or else + Present (Classifications (Items))); + end Has_Some_Contract; + + -------------------------- + -- In_Some_Private_Part -- + -------------------------- + + function In_Some_Private_Part (N : Node_Id) return Boolean is + P : Node_Id := N; + PP : Node_Id; + begin + while Present (P) + and then Present (Parent (P)) + loop + PP := Parent (P); + + if Nkind (PP) = N_Package_Specification + and then List_Containing (P) = Private_Declarations (PP) + then + return True; + end if; + + P := PP; + end loop; + return False; + end In_Some_Private_Part; + + ------------------ + -- In_Unit_Body -- + ------------------ + + function In_Unit_Body (N : Node_Id) return Boolean is + CU : constant Node_Id := Enclosing_Comp_Unit_Node (N); + begin + return Present (CU) + and then Nkind_In (Unit (CU), N_Package_Body, + N_Subprogram_Body, + N_Subunit); + end In_Unit_Body; + + ---------------------------- + -- Is_Expression_Function -- + ---------------------------- + + function Is_Expression_Function (Id : Entity_Id) return Boolean is + Decl : constant Node_Id := Parent (Parent (Id)); + begin + return Nkind (Original_Node (Decl)) = N_Expression_Function; + end Is_Expression_Function; + + Id : Entity_Id; -- Procedure or function entity for the subprogram + + -- Start of Can_Be_Inlined_In_GNATprove_Mode + + begin + if Present (Spec_Id) then + Id := Spec_Id; + else + Id := Body_Id; + end if; + + -- Do not inline unit-level subprograms + + if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then + return False; + + -- Do not inline subprograms declared in the visible part of a library + -- package. + + elsif Is_Library_Level_Entity (Id) + and then not In_Unit_Body (Id) + and then not In_Some_Private_Part (Id) + then + return False; + + -- Do not inline subprograms that have a contract on the spec or the + -- body. Use the contract(s) instead in GNATprove. + + elsif (Present (Spec_Id) and then Has_Some_Contract (Spec_Id)) + or else Has_Some_Contract (Body_Id) + then + return False; + + -- Do not inline expression functions + + elsif (Present (Spec_Id) and then Is_Expression_Function (Spec_Id)) + or else Is_Expression_Function (Body_Id) + then + return False; + + -- Only inline subprograms whose body is marked SPARK_Mode On + + elsif No (SPARK_Pragma (Body_Id)) + or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On + then + return False; + + -- Subprograms in generic instances are currently not inlined, to avoid + -- problems with inlining of standard library subprograms. + + elsif Instantiation_Location (Sloc (Id)) /= No_Location then + return False; + + -- Otherwise, this is a subprogram declared inside the private part of a + -- package, or inside a package body, or locally in a subprogram, and it + -- does not have any contract. Inline it. + + else + return True; + end if; + end Can_Be_Inlined_In_GNATprove_Mode; + ------------------------------------ -- Check_And_Build_Body_To_Inline -- ------------------------------------ @@ -2009,7 +2158,8 @@ Decl : constant Node_Id := Unit_Declaration_Node (Spec_Id); May_Inline : constant Boolean := - Has_Pragma_Inline_Always (Spec_Id) + GNATprove_Mode + or else Has_Pragma_Inline_Always (Spec_Id) or else (Has_Pragma_Inline (Spec_Id) and then ((Optimization_Level > 0 and then Ekind (Spec_Id) Index: inline.ads =================================================================== --- inline.ads (revision 213201) +++ inline.ads (working copy) @@ -23,7 +23,7 @@ -- -- ------------------------------------------------------------------------------ --- This module handles three kinds of inlining activity: +-- This module handles four kinds of inlining activity: -- a) Instantiation of generic bodies. This is done unconditionally, after -- analysis and expansion of the main unit. @@ -37,11 +37,13 @@ -- c) Front-end inlining for Inline_Always subprograms. This is primarily an -- expansion activity that is performed for performance reasons, and when the --- target does not use the gcc backend. Inline_Always can also be used in the --- context of GNATprove, to perform source transformations to simplify proof --- obligations. The machinery used in both cases is similar, but there are --- fewer restrictions on the source of subprograms in the latter case. +-- target does not use the gcc backend. +-- d) Front-end inlining for GNATprove, to perform source transformations +-- to simplify formal verification. The machinery used is the same than for +-- Inline_Always subprograms, but there are fewer restrictions on the source +-- of subprograms. + with Alloc; with Opt; use Opt; with Sem; use Sem; @@ -233,4 +235,11 @@ -- If an instantiation appears in unreachable code, delete the pending -- body instance. + function Can_Be_Inlined_In_GNATprove_Mode + (Spec_Id : Entity_Id; + Body_Id : Entity_Id) return Boolean; + -- Returns True if the subprogram identified by Spec_Id (possibly Empty) + -- and Body_Id (not Empty) can be inlined in GNATprove mode. GNATprove + -- relies on this to adapt its treatment of the subprogram. + end Inline; Index: sem_ch10.adb =================================================================== --- sem_ch10.adb (revision 213201) +++ sem_ch10.adb (working copy) @@ -1203,10 +1203,9 @@ and then Get_Cunit_Unit_Number (N) /= Main_Unit -- We don't need to do this if the Expander is not active, since there - -- is no code to inline. However an exception is that we do the call - -- in GNATprove mode, since the resulting inlining eases proofs. + -- is no code to inline. - and then (Expander_Active or GNATprove_Mode) + and then Expander_Active then declare Save_Style_Check : constant Boolean := Style_Check; Index: debug.adb =================================================================== --- debug.adb (revision 213201) +++ debug.adb (working copy) @@ -80,7 +80,7 @@ -- dN No file name information in exception messages -- dO Output immediate error messages -- dP Do not check for controlled objects in preelaborable packages - -- dQ + -- dQ Enable inlining in GNATprove mode -- dR Bypass check for correct version of s-rpc -- dS Never convert numbers to machine numbers in Sem_Eval -- dT Convert to machine numbers only for constant declarations @@ -438,6 +438,10 @@ -- in preelaborable packages, but this restriction is a huge pain, -- especially in the predefined library units. + -- dQ Enable inlining in GNATprove mode. Although expansion is not set in + -- GNATprove mode, inlining is useful for improving the precision of + -- formal verification. Under a debug flag until fully reliable. + -- dR Bypass the check for a proper version of s-rpc being present -- to use the -gnatz? switch. This allows debugging of the use -- of stubs generation without needing to have GLADE (or some Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 213201) +++ sem_prag.adb (working copy) @@ -15389,10 +15389,8 @@ -- if caused walk order issues. -- Historical note: this pragma used to be disabled in GNATprove - -- mode as well, but that was odd since walk order shoult not be - -- an issue in that case. Furthermore, we now like to do as much - -- front-end inlining as possible in GNATprove mode since it makes - -- proving things easier. + -- mode as well, but that was odd since walk order should not be + -- an issue in that case. if not CodePeer_Mode then Process_Inline (Enabled); Index: sem_res.adb =================================================================== --- sem_res.adb (revision 213201) +++ sem_res.adb (working copy) @@ -6124,15 +6124,16 @@ Eval_Call (N); Check_Elab_Call (N); - -- In GNATprove_Mode expansion is disabled, but we want to inline - -- subprograms that are marked Inline_Always, since the inlining - -- is useful in making it easier to prove things about the inlined body. - -- Indirect calls, through a subprogram type, cannot be inlined. + -- In GNATprove mode, expansion is disabled, but we want to inline + -- some subprograms to facilitate formal verification. Indirect calls, + -- through a subprogram type, cannot be inlined. Inlining is only + -- performed for calls for which SPARK_Mode is On. if GNATprove_Mode and then Is_Overloadable (Nam) and then Nkind (Unit_Declaration_Node (Nam)) = N_Subprogram_Declaration and then Present (Body_To_Inline (Unit_Declaration_Node (Nam))) + and then SPARK_Mode = On then Expand_Inlined_Call (N, Nam, Nam); end if; Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 213201) +++ sem_ch6.adb (working copy) @@ -3341,29 +3341,64 @@ -- Note: Normally we don't do any inlining if expansion is off, since -- we won't generate code in any case. An exception arises in GNATprove - -- mode where we want to expand calls in place whenever possible, even - -- with expansion disabled since the inlining eases proofs. + -- mode where we want to expand some calls in place, even with expansion + -- disabled, since the inlining eases formal verification. -- Old semantics if not Debug_Flag_Dot_K then if Present (Spec_Id) - and then (Expander_Active or else GNATprove_Mode) + and then Expander_Active and then (Has_Pragma_Inline_Always (Spec_Id) - or else (Has_Pragma_Inline (Spec_Id) and Front_End_Inlining)) + or else (Has_Pragma_Inline (Spec_Id) and Front_End_Inlining)) then Build_Body_To_Inline (N, Spec_Id); + + -- In GNATprove mode, inline only when there is a separate subprogram + -- declaration for now, as inlining of subprogram bodies acting as + -- declarations, or subprogram stubs, are not supported by frontend + -- inlining. This inlining should occur after analysis of the body, + -- so that it is known whether the value of SPARK_Mode applicable to + -- the body, which can be defined by a pragma inside the body. + + elsif GNATprove_Mode + and then Debug_Flag_QQ + and then Full_Analysis + and then not Inside_A_Generic + and then Present (Spec_Id) + and then + Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration + and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) + then + Build_Body_To_Inline (N, Spec_Id); end if; -- New semantics (enabled by debug flag gnatd.k for testing) - elsif (Expander_Active or else GNATprove_Mode) + elsif Expander_Active and then Serious_Errors_Detected = 0 and then Present (Spec_Id) and then Has_Pragma_Inline (Spec_Id) then Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id); + + -- In GNATprove mode, inline only when there is a separate subprogram + -- declaration for now, as inlining of subprogram bodies acting as + -- declarations, or subprogram stubs, are not supported by frontend + -- inlining. This inlining should occur after analysis of the body, so + -- that it is known whether the value of SPARK_Mode applicable to the + -- body, which can be defined by a pragma inside the body. + + elsif GNATprove_Mode + and then Debug_Flag_QQ + and then Full_Analysis + and then not Inside_A_Generic + and then Present (Spec_Id) + and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration + and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) + then + Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id); end if; -- Ada 2005 (AI-262): In library subprogram bodies, after the analysis