===================================================================
@@ -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-
===================================================================
@@ -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)
===================================================================
@@ -23,7 +23,7 @@
-- --
------------------------------------------------------------------------------
+-- 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.
+-- 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;
===================================================================
@@ -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;
===================================================================
@@ -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
===================================================================
@@ -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);
===================================================================
@@ -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;
===================================================================
@@ -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