From 2178830b048787f68c0b8b7c3dd3d26580a795aa Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 30 Jul 2014 15:54:18 +0200 Subject: [PATCH] [multiple changes] 2014-07-30 Pat Rogers * gnat_rm.texi: Minor word error. 2014-07-30 Ed Schonberg * exp_prag.adb (Expand_Old): Insert declarationss of temporaries created to capture the value of the prefix of 'Old at the beginning of the current declarative part, to prevent data flow anomalies in the postcondition procedure that will follow. 2014-07-30 Yannick Moy * debug.adb: Retire debug flag -gnatdQ. * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode on decl, not on body. Ignore predicate functions. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and body when generating a decl for a body on which SPARK_Mode aspect is given. * sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for attaching pragma to entity, to account for declaration not coming from source. * sem_res.adb (Resolve_Call): Issue warning and flag subprogram as not always inlined in GNATprove mode, when called in an assertion context. From-SVN: r213271 --- gcc/ada/ChangeLog | 27 +++++++++++++++++++++++ gcc/ada/debug.adb | 7 +----- gcc/ada/exp_prag.adb | 5 ++++- gcc/ada/gnat_rm.texi | 2 +- gcc/ada/inline.adb | 21 ++++++++++++------ gcc/ada/sem_ch13.adb | 2 +- gcc/ada/sem_ch6.adb | 42 +++++++++++++++++++++++++++++++---- gcc/ada/sem_prag.adb | 10 ++++----- gcc/ada/sem_res.adb | 52 ++++++++++++++++++++++++++++++++++---------- 9 files changed, 132 insertions(+), 36 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 81d1faa3ffc..408f6d07c4a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,30 @@ +2014-07-30 Pat Rogers + + * gnat_rm.texi: Minor word error. + +2014-07-30 Ed Schonberg + + * exp_prag.adb (Expand_Old): Insert declarationss of temporaries + created to capture the value of the prefix of 'Old at the + beginning of the current declarative part, to prevent data flow + anomalies in the postcondition procedure that will follow. + +2014-07-30 Yannick Moy + + * debug.adb: Retire debug flag -gnatdQ. + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode + on decl, not on body. Ignore predicate functions. + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of + debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and + body when generating a decl for a body on which SPARK_Mode aspect + is given. + * sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for + attaching pragma to entity, to account for declaration not coming + from source. + * sem_res.adb (Resolve_Call): Issue warning and flag subprogram + as not always inlined in GNATprove mode, when called in an + assertion context. + 2014-07-30 Vincent Celier * debug.adb: Minor comment update. diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index a93af0f6a30..64162ef0602 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 Enable inlining of bodies-without-decl in GNATprove mode + -- dQ -- 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,11 +438,6 @@ package body Debug is -- in preelaborable packages, but this restriction is a huge pain, -- especially in the predefined library units. - -- dQ Enable inlining of bodies-without-decl in GNATprove mode. A decl is - -- created by the frontend so that the usual frontend inlining - -- mechanism can be used for 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/exp_prag.adb b/gcc/ada/exp_prag.adb index 696d0635065..c48f3d2acf1 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -440,6 +440,9 @@ package body Exp_Prag is -- Generate a temporary to capture the value of the prefix: -- Temp : ; + -- Place that temporary at the beginning of declarations, to + -- prevent anomolies in the GNATprove flow analysis pass in + -- the precondition procedure that follows. Decl := Make_Object_Declaration (Loc, @@ -448,7 +451,7 @@ package body Exp_Prag is New_Occurrence_Of (Etype (Pref), Loc)); Set_No_Initialization (Decl); - Append_To (Decls, Decl); + Prepend_To (Decls, Decl); -- Evaluate the prefix, generate: -- Temp := ; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 18673029661..b0a018bf497 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -7215,7 +7215,7 @@ The meaning of a test case is that there is at least one context where that context, then @code{Ensures} holds when the subprogram returns. Mode @code{Nominal} indicates that the input context should also satisfy the precondition of the subprogram, and the output context should also satisfy its -postcondition. More @code{Robustness} indicates that the precondition and +postcondition. Mode @code{Robustness} indicates that the precondition and postcondition of the subprogram should be ignored for this test case. @node Pragma Thread_Local_Storage diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 4f099585da4..be556fb2eb8 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1692,13 +1692,14 @@ package body Inline is elsif Is_Generic_Instance (Spec_Id) then return False; - -- Only inline subprograms whose body is marked SPARK_Mode On. Other - -- subprogram bodies should not be analyzed. - - elsif Present (Body_Id) - and then (No (SPARK_Pragma (Body_Id)) - or else - Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On) + -- Only inline subprograms whose spec is marked SPARK_Mode On. For + -- the subprogram body, a similar check is performed after the body + -- is analyzed, as this is where a pragma SPARK_Mode might be inserted. + + elsif Present (Spec_Id) + and then (No (SPARK_Pragma (Spec_Id)) + or else + Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On) then return False; @@ -1708,6 +1709,12 @@ package body Inline is elsif Instantiation_Location (Sloc (Id)) /= No_Location then return False; + -- Predicate functions are treated specially by GNATprove. Do not inline + -- them. + + elsif Is_Predicate_Function (Id) 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. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index a9fa109e98c..f359b486901 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1497,7 +1497,7 @@ package body Sem_Ch13 is -- Start of processing for Analyze_One_Aspect begin - -- Skip aspect if already analyzed (not clear if this is needed) + -- Skip aspect if already analyzed, to avoid looping in some cases if Analyzed (Aspect) then goto Continue; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 393d557ad6a..72ee3824687 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3034,10 +3034,6 @@ package body Sem_Ch6 is if No (Spec_Id) and then GNATprove_Mode - -- Under a debug flag until remaining issues are fixed - - and then Debug_Flag_QQ - -- Inlining does not apply during pre-analysis of code and then Full_Analysis @@ -3077,13 +3073,51 @@ package body Sem_Ch6 is New_Decl : constant Node_Id := Make_Subprogram_Declaration (Loc, Copy_Separate_Tree (Specification (N))); + SPARK_Mode_Aspect : Node_Id; + Aspects : List_Id; + Prag, Aspect : Node_Id; begin Insert_Before (N, New_Decl); Move_Aspects (From => N, To => New_Decl); + + -- Mark the newly moved aspects as not analyzed, so that + -- their effect on New_Decl is properly analyzed. + + Aspect := First (Aspect_Specifications (New_Decl)); + while Present (Aspect) loop + Set_Analyzed (Aspect, False); + Next (Aspect); + end loop; + Analyze (New_Decl); + + -- The analysis of the generated subprogram declaration + -- may have introduced pragmas, which need to be + -- analyzed. + + Prag := Next (New_Decl); + while Prag /= N loop + Analyze (Prag); + Next (Prag); + end loop; + Spec_Id := Defining_Entity (New_Decl); + -- If aspect SPARK_Mode was specified on the body, it + -- needs to be repeated on the generated decl and the + -- body. Since the original aspect was moved to the + -- generated decl, copy it for the body. + + if Has_Aspect (Spec_Id, Aspect_SPARK_Mode) then + SPARK_Mode_Aspect := + New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode)); + Set_Analyzed (SPARK_Mode_Aspect, False); + Aspects := New_List; + Append (SPARK_Mode_Aspect, Aspects); + Set_Aspect_Specifications (N, Aspects); + end if; + Set_Specification (N, Body_Spec); Body_Id := Analyze_Subprogram_Specification (Body_Spec); Set_Corresponding_Spec (N, Spec_Id); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 122d47ce312..983cb321752 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -19830,11 +19830,6 @@ package body Sem_Prag is raise Pragma_Exit; end if; - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - elsif Nkind (Stmt) in N_Generic_Declaration then Error_Pragma ("incorrect placement of pragma% on a generic"); @@ -19869,6 +19864,11 @@ package body Sem_Prag is Set_SPARK_Pragma_Inherited (Spec_Id, False); return; + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + null; + -- The pragma does not apply to a legal construct, issue an -- error and stop the analysis. diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 88356fd6127..92317edaf49 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6210,7 +6210,6 @@ package body Sem_Res is if GNATprove_Mode and then Is_Overloadable (Nam) and then SPARK_Mode = On - and then Full_Analysis then -- Retrieve the body to inline from the ultimate alias of Nam, if -- there is one, otherwise calls that should be inlined end up not @@ -6220,23 +6219,54 @@ package body Sem_Res is Nam_Alias : constant Entity_Id := Ultimate_Alias (Nam); Decl : constant Node_Id := Unit_Declaration_Node (Nam_Alias); begin - if Nkind (Decl) = N_Subprogram_Declaration - and then Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty) - and then No (Corresponding_Body (Decl)) + -- If the subprogram is not eligible for inlining in GNATprove + -- mode, do nothing. + + if not Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty) + or else Nkind (Decl) /= N_Subprogram_Declaration + or else not Is_Inlined_Always (Nam_Alias) then - Error_Msg_NE - ("?cannot inline call to & (body not seen yet)", N, Nam); + null; + + -- Calls cannot be inlined inside assertions, as GNATprove treats + -- assertions as logic expressions. + + elsif In_Assertion_Expr /= 0 then + Error_Msg_NE ("?cannot inline call to &", N, Nam); + Error_Msg_N ("\call appears in assertion expression", N); Set_Is_Inlined_Always (Nam_Alias, False); - elsif Nkind (Decl) = N_Subprogram_Declaration - and then Present (Body_To_Inline (Decl)) - and then Is_Inlined (Nam_Alias) - then - if Is_Potentially_Unevaluated (N) then + -- Inlining should not be performed during pre-analysis + + elsif Full_Analysis then + + -- With the one-pass inlining technique, a call cannot be + -- inlined if the corresponding body has not been seen yet. + + if No (Corresponding_Body (Decl)) then + Error_Msg_NE + ("?cannot inline call to & (body not seen yet)", N, Nam); + Set_Is_Inlined_Always (Nam_Alias, False); + + -- Nothing to do if there is no body to inline, indicating that + -- the subprogram is not suitable for inlining in GNATprove + -- mode. + + elsif No (Body_To_Inline (Decl)) then + null; + + -- Calls cannot be inlined inside potentially unevaluated + -- expressions, as this would create complex actions inside + -- expressions, that are not handled by GNATprove. + + elsif Is_Potentially_Unevaluated (N) then Error_Msg_NE ("?cannot inline call to &", N, Nam); Error_Msg_N ("\call appears in potentially unevaluated context", N); Set_Is_Inlined_Always (Nam_Alias, False); + + -- Otherwise, inline the call + else Expand_Inlined_Call (N, Nam_Alias, Nam); end if; -- 2.30.2