mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-04 04:40:27 +08:00
Code Issues Packages Projects Releases Wiki Activity

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

Browse Source 
* 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.

From-SVN: r213205
This commit is contained in:
Yannick Moy 2014-07-29 14:55:24 +00:00 committed by Arnaud Charlet
parent 5ae2431279
commit 2d180af122
9 changed files with 240 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
gcc/ada/ChangeLog
View File

@ -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

6
gcc/ada/debug.adb
View File

@ -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

160
gcc/ada/inline.adb
View File

@ -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)

19
gcc/ada/inline.ads
View File

@ -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;

5
gcc/ada/sem_ch10.adb
View File

@ -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;

45
gcc/ada/sem_ch6.adb
View File

@ -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

6
gcc/ada/sem_prag.adb
View File

@ -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);

9
gcc/ada/sem_res.adb
View File

@ -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;

2
gcc/ada/sinfo.ads
View File

@ -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-