2014-07-29 Yannick Moy <moy@adacore.com>

	* debug.adb Enable GNATprove inlining under debug flag -gnatdQ for now.
	* inline.ads, inline.adb (Can_Be_Inlined_In_GNATprove_Mode): New
	function to decide when a subprogram can be inlined in GNATprove mode.
	(Check_And_Build_Body_To_Inline): Include GNATprove_Mode as a
	condition for possible inlining.
	* sem_ch10.adb (Analyze_Compilation_Unit): Remove special case
	for Inline_Always in GNATprove mode.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build inlined
	body for subprograms in GNATprove mode, under debug flag -gnatdQ.
	* sem_prag.adb Minor change in comments.
	* sem_res.adb (Resolve_Call): Only perform GNATprove inlining
	inside subprograms marked as SPARK_Mode On.
	* sinfo.ads: Minor typo fix.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@213205 138bc75d-0d04-0410-961f-82ee72b054a4

9 files changed, 240 insertions, 28 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 7f36e12d715..aaf8a145394 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,19 @@
+2014-07-29  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb Enable GNATprove inlining under debug flag -gnatdQ for now.
+	* inline.ads, inline.adb (Can_Be_Inlined_In_GNATprove_Mode): New
+	function to decide when a subprogram can be inlined in GNATprove mode.
+	(Check_And_Build_Body_To_Inline): Include GNATprove_Mode as a
+	condition for possible inlining.
+	* sem_ch10.adb (Analyze_Compilation_Unit): Remove special case
+	for Inline_Always in GNATprove mode.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Build inlined
+	body for subprograms in GNATprove mode, under debug flag -gnatdQ.
+	* sem_prag.adb Minor change in comments.
+	* sem_res.adb (Resolve_Call): Only perform GNATprove inlining
+	inside subprograms marked as SPARK_Mode On.
+	* sinfo.ads: Minor typo fix.
+
 2014-07-29  Vincent Celier  <celier@adacore.com>
 
 	* frontend.adb: Add dependency on gnat.adc when taken into account
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index d375205e73b..5e9c0daf02a 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -80,7 +80,7 @@ package body Debug is
    --  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 @@ package body Debug is
    --       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
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index a27c4a29780..dda78d6a256 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -44,8 +44,10 @@ with Sem_Ch8;  use Sem_Ch8;
 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 @@ package body Inline is
          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 @@ package body Inline is
       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 @@ package body Inline is
 
          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)
diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads
index e8b1c0134de..a4a95279524 100644
--- a/gcc/ada/inline.ads
+++ b/gcc/ada/inline.ads
@@ -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,10 +37,12 @@
 
 --  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;
@@ -233,4 +235,11 @@ package Inline is
    --  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;
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index f0f0ba16947..a58a8a40d18 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -1203,10 +1203,9 @@ package body Sem_Ch10 is
         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;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 92e7998c1cd..727a3beb7d7 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3341,29 +3341,64 @@ package body Sem_Ch6 is
 
       --  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
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index dac93429657..a25f451a00c 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -15389,10 +15389,8 @@ package body Sem_Prag is
             --  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);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 168cfb32c45..0e73216971f 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6124,15 +6124,16 @@ package body Sem_Res is
       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;
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 0da8b6ac0e9..427919e7d3a 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -817,7 +817,7 @@ package Sinfo is
    --    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-