From b3a699930b7b61d37753e8714929cd2d9c1fb6d8 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 27 Jan 2014 17:37:28 +0100 Subject: [PATCH] [multiple changes] 2014-01-27 Thomas Quinot * exp_smem.adb (Expand_Shared_Passive_Variable): For a reference to a shared variable as an OUT formal in a call to an init proc, the 'Read call must be emitted after, not before, the call. 2014-01-27 Robert Dewar * gnat_rm.texi: Remove mention of AUTO mode for SPARK_Mode pragma. From-SVN: r207139 --- gcc/ada/ChangeLog | 10 +++++ gcc/ada/exp_smem.adb | 122 +++++++++++++++++++++++++++++++-------------------- gcc/ada/gnat_rm.texi | 26 +++++------ 3 files changed, 95 insertions(+), 63 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8f9f89f..3cebcd0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2014-01-27 Thomas Quinot + + * exp_smem.adb (Expand_Shared_Passive_Variable): For a reference + to a shared variable as an OUT formal in a call to an init proc, + the 'Read call must be emitted after, not before, the call. + +2014-01-27 Robert Dewar + + * gnat_rm.texi: Remove mention of AUTO mode for SPARK_Mode pragma. + 2014-01-27 Robert Dewar * a-wichha.adb (Character_Set_Version): Change to output proper diff --git a/gcc/ada/exp_smem.adb b/gcc/ada/exp_smem.adb index 1f23ac1..2b83105 100644 --- a/gcc/ada/exp_smem.adb +++ b/gcc/ada/exp_smem.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1998-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1998-2013, 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- -- @@ -26,6 +26,7 @@ with Atree; use Atree; with Einfo; use Einfo; with Exp_Ch9; use Exp_Ch9; +with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Nmake; use Nmake; with Namet; use Namet; @@ -49,36 +50,38 @@ package body Exp_Smem is -- Local Subprograms -- ----------------------- - procedure Add_Read_Before (N : Node_Id); - -- Insert a Shared_Var_ROpen call for variable before node N + procedure Add_Read (N : Node_Id; Call : Node_Id := Empty); + -- Insert a Shared_Var_ROpen call for variable before node N, unless + -- Call is a call to an init-proc, in which case the call is inserted + -- after Call. procedure Add_Write_After (N : Node_Id); - -- Insert a Shared_Var_WOpen call for variable after the node - -- Insert_Node, as recorded by On_Lhs_Of_Assignment (where it points - -- to the assignment statement) or Is_Out_Actual (where it points to - -- the procedure call statement). + -- Insert a Shared_Var_WOpen call for variable after the node Insert_Node, + -- as recorded by On_Lhs_Of_Assignment (where it points to the assignment + -- statement) or Is_Out_Actual (where it points to the procedure call + -- statement). procedure Build_Full_Name (E : Entity_Id; N : out String_Id); -- Build the fully qualified string name of a shared variable function On_Lhs_Of_Assignment (N : Node_Id) return Boolean; - -- Determines if N is on the left hand of the assignment. This means - -- that either it is a simple variable, or it is a record or array - -- variable with a corresponding selected or indexed component on - -- the left side of an assignment. If the result is True, then - -- Insert_Node is set to point to the assignment + -- Determines if N is on the left hand of the assignment. This means that + -- either it is a simple variable, or it is a record or array variable with + -- a corresponding selected or indexed component on the left side of an + -- assignment. If the result is True, then Insert_Node is set to point + -- to the assignment function Is_Out_Actual (N : Node_Id) return Boolean; - -- In a similar manner, this function determines if N appears as an - -- OUT or IN OUT parameter to a procedure call. If the result is - -- True, then Insert_Node is set to point to the call. + -- In a similar manner, this function determines if N appears as an OUT + -- or IN OUT parameter to a procedure call. If the result is True, then + -- Insert_Node is set to point to the call. function Build_Shared_Var_Proc_Call (Loc : Source_Ptr; E : Node_Id; N : Name_Id) return Node_Id; - -- Build a call to support procedure N for shared object E (provided by - -- the instance of System.Shared_Storage.Shared_Var_Procs associated to E). + -- Build a call to support procedure N for shared object E (provided by the + -- instance of System.Shared_Storage.Shared_Var_Procs associated to E). -------------------------------- -- Build_Shared_Var_Proc_Call -- @@ -87,7 +90,8 @@ package body Exp_Smem is function Build_Shared_Var_Proc_Call (Loc : Source_Ptr; E : Entity_Id; - N : Name_Id) return Node_Id is + N : Name_Id) return Node_Id + is begin return Make_Procedure_Call_Statement (Loc, Name => Make_Selected_Component (Loc, @@ -96,18 +100,26 @@ package body Exp_Smem is Selector_Name => Make_Identifier (Loc, N))); end Build_Shared_Var_Proc_Call; - --------------------- - -- Add_Read_Before -- - --------------------- + -------------- + -- Add_Read -- + -------------- - procedure Add_Read_Before (N : Node_Id) is + procedure Add_Read (N : Node_Id; Call : Node_Id := Empty) is Loc : constant Source_Ptr := Sloc (N); Ent : constant Node_Id := Entity (N); + SVC : Node_Id; + begin if Present (Shared_Var_Procs_Instance (Ent)) then - Insert_Action (N, Build_Shared_Var_Proc_Call (Loc, Ent, Name_Read)); + SVC := Build_Shared_Var_Proc_Call (Loc, Ent, Name_Read); + + if Present (Call) and then Is_Init_Proc (Name (Call)) then + Insert_After_And_Analyze (Call, SVC); + else + Insert_Action (N, SVC); + end if; end if; - end Add_Read_Before; + end Add_Read; ------------------------------- -- Add_Shared_Var_Lock_Procs -- @@ -121,10 +133,10 @@ package body Exp_Smem is begin -- We have to add Shared_Var_Lock and Shared_Var_Unlock calls around - -- the procedure or function call node. First we locate the right - -- place to do the insertion, which is the call itself in the - -- procedure call case, or else the nearest non subexpression - -- node that contains the function call. + -- the procedure or function call node. First we locate the right place + -- to do the insertion, which is the call itself in the procedure call + -- case, or else the nearest non subexpression node that contains the + -- function call. Inode := N; while Nkind (Inode) /= N_Procedure_Call_Statement @@ -135,11 +147,11 @@ package body Exp_Smem is -- Now insert the Lock and Unlock calls and the read/write calls - -- Two concerns here. First we are not dealing with the exception - -- case, really we need some kind of cleanup routine to do the - -- Unlock. Second, these lock calls should be inside the protected - -- object processing, not outside, otherwise they can be done at - -- the wrong priority, resulting in dead lock situations ??? + -- Two concerns here. First we are not dealing with the exception case, + -- really we need some kind of cleanup routine to do the Unlock. Second, + -- these lock calls should be inside the protected object processing, + -- not outside, otherwise they can be done at the wrong priority, + -- resulting in dead lock situations ??? Build_Full_Name (Obj, Vnm); @@ -171,7 +183,6 @@ package body Exp_Smem is Insert_After_And_Analyze (Inode, Build_Shared_Var_Proc_Call (Loc, Obj, Name_Write)); end if; - end Add_Shared_Var_Lock_Procs; --------------------- @@ -235,23 +246,41 @@ package body Exp_Smem is if Is_Limited_Type (Typ) or else Is_Concurrent_Type (Typ) then return; - -- If we are on the left hand side of an assignment, then we add - -- the write call after the assignment. + -- If we are on the left hand side of an assignment, then we add the + -- write call after the assignment. elsif On_Lhs_Of_Assignment (N) then Add_Write_After (N); - -- If we are a parameter for an out or in out formal, then put - -- the read before and the write after. + -- If we are a parameter for an out or in out formal, then in general + -- we do: + + -- read + -- call + -- write + + -- but in the special case of a call to an init proc, we need to first + -- call the init proc (to set discriminants), then read (to possibly + -- set other components), then write (to record the updated components + -- to the backing store): + + -- init-proc-call + -- read + -- write elsif Is_Out_Actual (N) then - Add_Read_Before (N); + + -- Note: For an init proc call, Add_Read inserts just after the + -- call node, and we want to have first the read, then the write, + -- so we need to first Add_Write_After, then Add_Read. + Add_Write_After (N); + Add_Read (N, Call => Insert_Node); -- All other cases are simple reads else - Add_Read_Before (N); + Add_Read (N); end if; end Expand_Shared_Passive_Variable; @@ -297,8 +326,7 @@ package body Exp_Smem is SVP_Instance : constant Entity_Id := Make_Defining_Identifier (Loc, Chars => New_External_Name (Chars (Ent), 'G')); - -- Instance of System.Shared_Storage.Shared_Var_Procs associated - -- with Ent. + -- Instance of Shared_Storage.Shared_Var_Procs associated with Ent Instantiation : Node_Id; -- Package instantiation node for SVP_Instance @@ -308,9 +336,9 @@ package body Exp_Smem is begin Build_Full_Name (Ent, Vnm); - -- We turn off Shared_Passive during construction and analysis of - -- the generic package instantiation, to avoid improper attempts to - -- process the variable references within these instantiation. + -- We turn off Shared_Passive during construction and analysis of the + -- generic package instantiation, to avoid improper attempts to process + -- the variable references within these instantiation. Set_Is_Shared_Passive (Ent, False); @@ -376,9 +404,7 @@ package body Exp_Smem is return False; end if; - elsif (Nkind (P) = N_Indexed_Component - or else - Nkind (P) = N_Selected_Component) + elsif Nkind_In (P, N_Indexed_Component, N_Selected_Component) and then N = Prefix (P) then return On_Lhs_Of_Assignment (P); diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 54edf04..6f04498 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -6305,7 +6305,7 @@ is needed for error messages issued by all phases of the compiler. Syntax: @smallexample @c ada -pragma SPARK_Mode [ (On | Off | Auto) ] ; +pragma SPARK_Mode [(On | Off)] ; @end smallexample @noindent @@ -6315,16 +6315,14 @@ language. The pragma is intended for use with formal verification tools and has no effect on the generated code. The SPARK_Mode pragma is used to specify the value of the SPARK_Mode aspect -(a three-valued aspect having values of On, Off, or Auto) of an entity. +(either Off or On) of an entity. More precisely, it is used to specify the aspect value of a ``section'' of an entity (the term ``section'' is defined below). If a Spark_Mode pragma's (optional) argument is omitted, an implicit argument of On is assumed. A SPARK_Mode pragma may be used as a configuration pragma and then has the -semantics described below. A SPARK_Mode pragma which is not used as a -configuration pragma (or an equivalent SPARK_Mode aspect_specification) -shall not have an argument of Auto. +semantics described below. A SPARK_Mode pragma can be used as a local pragma only in the following contexts: @@ -6374,8 +6372,7 @@ completion is defined to have 2 ``sections'': its declaration and its completion. Any other construct is defined to have 1 section. The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity -or construct is then defined to be the following value (except if this yields -a result of Auto for a non-package; see below): +or construct is then defined to be the following value: @itemize @@ -6392,7 +6389,7 @@ else for any of the visible part or body declarations of a library unit package or either section of a library unit subprogram, if there is an applicable SPARK_Mode configuration pragma then the value specified by the pragma; if no such configuration pragma applies, then an implicit -specification of Auto is assumed; +specification of Off is assumed; @item else for any subsequent (i.e., not the first) section of a library unit @@ -6404,12 +6401,11 @@ or subprogram; @end itemize -If the above computation yields a result of Auto for any construct other than -one of the four sections of a package, then a result of On or Off is -determined instead based on the legality (with respect to the rules of -SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only -if the construct is in SPARK 2014. [A SPARK_Mode of -Auto is therefore only possible for sections of a package.] +If the above computation does not specify a SPARK_Mode setting for any +construct other than one of the four sections of a package, then a result of On +or Off is determined instead based on the legality (with respect to the rules +of SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only +if the construct is in SPARK 2014. If an earlier section of an entity has a Spark_Mode of Off, then the Spark_Mode aspect of any later section of that entity shall not be @@ -12472,7 +12468,7 @@ See A.3.5(3). @end cartouche @noindent @code{Ada.Wide_Characters.Handling.Character_Set_Version} returns -the string "Unicode 6.2", referring to version 6.2.x of the +the string "Unicode 4.0", referring to version 4.0 of the Unicode specification. @sp 1 -- 2.7.4