diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 14 | ||||
| -rw-r--r-- | gcc/ada/inline.adb | 77 | ||||
| -rw-r--r-- | gcc/ada/inline.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 8 |
4 files changed, 100 insertions, 8 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8cac665..549ee1a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -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, diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 1be03ae..bf0f705 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.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, diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index 04662b8..96cff58 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -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; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 2a8baaa..51629f2 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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 |