mirror of
git://gcc.gnu.org/git/gcc.git
synced 2025-04-04 02:50:29 +08:00
inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mode): New function to detect when a call may be inlined or not in GNATprove mode.
2017-01-13 Yannick Moy <moy@adacore.com> * inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mode): New function to detect when a call may be inlined or not in GNATprove mode. (Expand_Inlined_Call): Ensure that a temporary is always created in the cases where a type conversion may be needed on an input parameter in GNATprove mode, so that GNATprove sees the check to perform. * sem_res.adb (Resolve_Call): In GNATprove mode, skip inlining when not applicable due to actual requiring type conversion with possible check but no temporary value can be copied for GNATprove to see the check. From-SVN: r244408
This commit is contained in:
Yannick Moy
Arnaud Charlet
parent
4ccff88b71
commit
3de3a1be9e
@ -1,3 +1,17 @@
|
||||
2017-01-13 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* inline.adb, inline.ads (Call_Can_Be_Inlined_In_GNATprove_Mode):
|
||||
New function to detect when a call may be inlined or not in
|
||||
GNATprove mode.
|
||||
(Expand_Inlined_Call): Ensure that a temporary
|
||||
is always created in the cases where a type conversion may be
|
||||
needed on an input parameter in GNATprove mode, so that GNATprove
|
||||
sees the check to perform.
|
||||
* sem_res.adb (Resolve_Call): In GNATprove mode, skip inlining
|
||||
when not applicable due to actual requiring type conversion
|
||||
with possible check but no temporary value can be copied for
|
||||
GNATprove to see the check.
|
||||
|
||||
2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_aggr.adb, par_sco.adb, s-osprim-mingw.adb, exp_ch5.adb,
|
||||
|
||||
@ -1149,7 +1149,7 @@ package body Inline is
|
||||
Make_Defining_Identifier (Sloc (N), Name_uParent));
|
||||
Set_Corresponding_Spec (Original_Body, Empty);
|
||||
|
||||
-- Remove all aspects/pragmas that have no meaining in an inlined body
|
||||
-- Remove all aspects/pragmas that have no meaning in an inlined body
|
||||
|
||||
Remove_Aspects_And_Pragmas (Original_Body);
|
||||
|
||||
@ -1204,6 +1204,37 @@ package body Inline is
|
||||
Set_Is_Inlined (Spec_Id);
|
||||
end Build_Body_To_Inline;
|
||||
|
||||
-------------------------------------------
|
||||
-- Call_Can_Be_Inlined_In_GNATprove_Mode --
|
||||
-------------------------------------------
|
||||
|
||||
function Call_Can_Be_Inlined_In_GNATprove_Mode
|
||||
(N : Node_Id;
|
||||
Subp : Entity_Id) return Boolean
|
||||
is
|
||||
F : Entity_Id;
|
||||
A : Node_Id;
|
||||
|
||||
begin
|
||||
F := First_Formal (Subp);
|
||||
A := First_Actual (N);
|
||||
while Present (F) loop
|
||||
if Ekind (F) /= E_Out_Parameter
|
||||
and then not Same_Type (Etype (F), Etype (A))
|
||||
and then
|
||||
(Is_By_Reference_Type (Etype (A))
|
||||
or else Is_Limited_Type (Etype (A)))
|
||||
then
|
||||
return False;
|
||||
end if;
|
||||
|
||||
Next_Formal (F);
|
||||
Next_Actual (A);
|
||||
end loop;
|
||||
|
||||
return True;
|
||||
end Call_Can_Be_Inlined_In_GNATprove_Mode;
|
||||
|
||||
-------------------
|
||||
-- Cannot_Inline --
|
||||
-------------------
|
||||
@ -1406,8 +1437,8 @@ package body Inline is
|
||||
Formal : Entity_Id;
|
||||
Formal_Typ : Entity_Id;
|
||||
|
||||
-- Start of processing for
|
||||
-- Has_Formal_With_Discriminant_Dependent_Component
|
||||
-- Start of processing for
|
||||
-- Has_Formal_With_Discriminant_Dependent_Fields
|
||||
|
||||
begin
|
||||
-- Inspect all parameters of the subprogram looking for a formal
|
||||
@ -3065,19 +3096,25 @@ package body Inline is
|
||||
|
||||
-- If the actual is a literal and the formal has its address taken,
|
||||
-- we cannot pass the literal itself as an argument, so its value
|
||||
-- must be captured in a temporary.
|
||||
-- must be captured in a temporary. Skip this optimization in
|
||||
-- GNATprove mode, to make sure any check on a type conversion
|
||||
-- will be issued.
|
||||
|
||||
if (Is_Entity_Name (A)
|
||||
and then
|
||||
(not Is_Scalar_Type (Etype (A))
|
||||
or else Ekind (Entity (A)) = E_Enumeration_Literal))
|
||||
or else Ekind (Entity (A)) = E_Enumeration_Literal)
|
||||
and then not GNATprove_Mode)
|
||||
|
||||
-- When the actual is an identifier and the corresponding formal is
|
||||
-- used only once in the original body, the formal can be substituted
|
||||
-- directly with the actual parameter.
|
||||
-- directly with the actual parameter. Skip this optimization in
|
||||
-- GNATprove mode, to make sure any check on a type conversion
|
||||
-- will be issued.
|
||||
|
||||
or else (Nkind (A) = N_Identifier
|
||||
and then Formal_Is_Used_Once (F))
|
||||
and then Formal_Is_Used_Once (F)
|
||||
and then not GNATprove_Mode)
|
||||
|
||||
or else
|
||||
(Nkind_In (A, N_Real_Literal,
|
||||
@ -3147,7 +3184,33 @@ package body Inline is
|
||||
Constant_Present => True,
|
||||
Object_Definition => New_Occurrence_Of (Temp_Typ, Loc),
|
||||
Expression => New_A);
|
||||
|
||||
else
|
||||
-- In GNATprove mode, make an explicit copy of input
|
||||
-- parameters when formal and actual types differ, to make
|
||||
-- sure any check on the type conversion will be issued.
|
||||
-- The legality of the copy is ensured by calling first
|
||||
-- Call_Can_Be_Inlined_In_GNATprove_Mode.
|
||||
|
||||
if GNATprove_Mode
|
||||
and then Ekind (F) /= E_Out_Parameter
|
||||
and then not Same_Type (Etype (F), Etype (A))
|
||||
then
|
||||
pragma Assert (not (Is_By_Reference_Type (Etype (A))));
|
||||
pragma Assert (not (Is_Limited_Type (Etype (A))));
|
||||
Decl :=
|
||||
Make_Object_Declaration (Loc,
|
||||
Defining_Identifier => Temp,
|
||||
Constant_Present => True,
|
||||
Object_Definition => New_Occurrence_Of (Temp_Typ, Loc),
|
||||
Expression => New_Copy_Tree (New_A));
|
||||
Append (Decl, Decls);
|
||||
|
||||
-- Create another name for the renaming
|
||||
|
||||
Temp := Make_Temporary (Loc, 'C');
|
||||
end if;
|
||||
|
||||
Decl :=
|
||||
Make_Object_Renaming_Declaration (Loc,
|
||||
Defining_Identifier => Temp,
|
||||
|
||||
@ -6,7 +6,7 @@
|
||||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNAT is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
@ -167,6 +167,13 @@ package Inline is
|
||||
-- enabled and the subprogram contains a construct that cannot be inlined,
|
||||
-- the problematic construct is flagged accordingly.
|
||||
|
||||
function Call_Can_Be_Inlined_In_GNATprove_Mode
|
||||
(N : Node_Id;
|
||||
Subp : Entity_Id) return Boolean;
|
||||
-- Returns False if the call in node N to subprogram Subp cannot be inlined
|
||||
-- in GNATprove mode, because it may lead to missing a check on type
|
||||
-- conversion of input parameters otherwise. Returns True otherwise.
|
||||
|
||||
function Can_Be_Inlined_In_GNATprove_Mode
|
||||
(Spec_Id : Entity_Id;
|
||||
Body_Id : Entity_Id) return Boolean;
|
||||
|
||||
@ -6624,6 +6624,14 @@ package body Sem_Res is
|
||||
("cannot inline & (in potentially unevaluated context)?",
|
||||
N, Nam_UA);
|
||||
|
||||
-- Do not inline calls which would possibly lead to missing a
|
||||
-- type conversion check on an input parameter.
|
||||
|
||||
elsif not Call_Can_Be_Inlined_In_GNATprove_Mode (N, Nam) then
|
||||
Cannot_Inline
|
||||
("cannot inline & (possible check on input parameters)?",
|
||||
N, Nam_UA);
|
||||
|
||||
-- Otherwise, inline the call
|
||||
|
||||
else
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user