[Ada] Update for Ownership rules for access types according to AI12-0240

Message ID	20180821150422.GA57110@adacore.com
State	New
Headers	show Return-Path: <gcc-patches-return-484104-incoming=patchwork.ozlabs.org@gcc.gnu.org> DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=P6EowF3m5e/G1iPxgojyDKJ7pE+uL1ZFXtY2XeE7zylwx7RGOo gp3G7I/xZGbynOKYMpYVIdeUXHJRAGDNjlfQyDJACqpzhKIRXUxvIcKqIKP9yYlc 69giyutxcqUjyOQa4oaVSmtAK2gKoBXbyqwCmXSvdQJ15HeQSnrEL4AVs= Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk Sender: gcc-patches-owner@gcc.gnu.org Date: Tue, 21 Aug 2018 11:04:22 -0400 From: Pierre-Marie de Rodat <derodat@adacore.com> To: gcc-patches@gcc.gnu.org Cc: Maroua Maalej <maalej@adacore.com> Subject: [Ada] Update for Ownership rules for access types according to AI12-0240 Message-ID: <20180821150422.GA57110@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="SUOF0GtieIMvvwua" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12)
Series	[Ada] Update for Ownership rules for access types according to AI12-0240 \| expand [Ada] Update for Ownership rules for access types according to AI12-0240

--- gcc/ada/sem_spark.adb +++ gcc/ada/sem_spark.adb @@ -52,15 +52,16 @@ package body Sem_SPARK is type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1; - function Elaboration_Context_Hash - (Key : Entity_Id) return Elaboration_Context_Index; + function Elaboration_Context_Hash (Key : Entity_Id) + return Elaboration_Context_Index; -- Function to hash any node of the AST - type Perm_Kind is (No_Access, Read_Only, Read_Write, Write_Only); - -- Permission type associated with paths - - subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write; - subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only; + type Perm_Kind is (Borrowed, Observed, Unrestricted, Moved); + -- Permission type associated with paths. The Moved permission is + -- equivalent to the Unrestricted one (same permissions). The Moved is + -- however used to mark the RHS after a move (which still unrestricted). + -- This way, we may generate warnings when manipulating the RHS + -- afterwads since it is set to Null after the assignment. type Perm_Tree_Wrapper; @@ -94,6 +95,7 @@ package body Sem_SPARK is -- The definition of permission trees. This is a tree, which has a -- permission at each node, and depending on the type of the node, -- can have zero, one, or more children pointed to by an access to tree. + type Perm_Tree (Kind : Path_Kind := Entire_Object) is record Permission : Perm_Kind; -- Permission at this level in the path @@ -103,7 +105,6 @@ package body Sem_SPARK is -- path. case Kind is - -- An entire object is either a leaf (an object which cannot be -- extended further in a path) or a subtree in folded form (which -- could later be unfolded further in another kind of node). The @@ -111,19 +112,19 @@ package body Sem_SPARK is -- extension of that node if that permission is different from -- the node's permission. - when Entire_Object => + when Entire_Object => Children_Permission : Perm_Kind; -- Unfolded path of access type. The permission of the object -- pointed to is given in Get_All. - when Reference => + when Reference => Get_All : Perm_Tree_Access; -- Unfolded path of array type. The permission of the elements is -- given in Get_Elem. - when Array_Component => + when Array_Component => Get_Elem : Perm_Tree_Access; -- Unfolded path of record type. The permission of the regular @@ -229,7 +230,7 @@ package body Sem_SPARK is -------------------- procedure Perm_Mismatch - (Exp_Perm, Act_Perm : Perm_Kind; + (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id); -- Issues a continuation error message about a mismatch between a -- desired permission Exp_Perm and a permission obtained Act_Perm. N @@ -243,10 +244,7 @@ package body Sem_SPARK is -- Children_Permission -- ------------------------- - function Children_Permission - (T : Perm_Tree_Access) - return Perm_Kind - is + function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is begin return T.all.Tree.Children_Permission; end Children_Permission; @@ -257,7 +255,7 @@ package body Sem_SPARK is function Component (T : Perm_Tree_Access) - return Perm_Tree_Maps.Instance + return Perm_Tree_Maps.Instance is begin return T.all.Tree.Component; @@ -267,13 +265,10 @@ package body Sem_SPARK is -- Copy_Env -- -------------- - procedure Copy_Env - (From : Perm_Env; - To : in out Perm_Env) - is + procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is Comp_From : Perm_Tree_Access; - Key_From : Perm_Tree_Maps.Key_Option; - Son : Perm_Tree_Access; + Key_From : Perm_Tree_Maps.Key_Option; + Son : Perm_Tree_Access; begin Reset (To); @@ -296,7 +291,7 @@ package body Sem_SPARK is procedure Copy_Init_Map (From : Initialization_Map; - To : in out Initialization_Map) + To : in out Initialization_Map) is Comp_From : Boolean; Key_From : Boolean_Variables_Maps.Key_Option; @@ -315,25 +310,19 @@ package body Sem_SPARK is -- Copy_Tree -- --------------- - procedure Copy_Tree - (From : Perm_Tree_Access; - To : Perm_Tree_Access) - is + procedure Copy_Tree (From : Perm_Tree_Access; To : Perm_Tree_Access) is begin To.all := From.all; - case Kind (From) is when Entire_Object => null; when Reference => To.all.Tree.Get_All := new Perm_Tree_Wrapper; - Copy_Tree (Get_All (From), Get_All (To)); when Array_Component => To.all.Tree.Get_Elem := new Perm_Tree_Wrapper; - Copy_Tree (Get_Elem (From), Get_Elem (To)); when Record_Component => @@ -346,31 +335,26 @@ package body Sem_SPARK is -- We put a new hash table, so that it gets dealiased from the -- Component (From) hash table. To.all.Tree.Component := Hash_Table; - To.all.Tree.Other_Components := new Perm_Tree_Wrapper'(Other_Components (From).all); - Copy_Tree (Other_Components (From), Other_Components (To)); - Key_From := Perm_Tree_Maps.Get_First_Key (Component (From)); + while Key_From.Present loop Comp_From := Perm_Tree_Maps.Get (Component (From), Key_From.K); - pragma Assert (Comp_From /= null); Son := new Perm_Tree_Wrapper; - Copy_Tree (Comp_From, Son); - Perm_Tree_Maps.Set (To.all.Tree.Component, Key_From.K, Son); - Key_From := Perm_Tree_Maps.Get_Next_Key (Component (From)); end loop; end; end case; + end Copy_Tree; ------------------------------ @@ -402,9 +386,7 @@ package body Sem_SPARK is -- Free_Perm_Tree -- -------------------- - procedure Free_Perm_Tree - (PT : in out Perm_Tree_Access) - is + procedure Free_Perm_Tree (PT : in out Perm_Tree_Access) is procedure Free_Perm_Tree_Dealloc is new Ada.Unchecked_Deallocation (Perm_Tree_Wrapper, Perm_Tree_Access); @@ -430,6 +412,7 @@ package body Sem_SPARK is Free_Perm_Tree (PT.all.Tree.Other_Components); Comp := Perm_Tree_Maps.Get_First (Component (PT)); while Comp /= null loop + -- Free every Component subtree Free_Perm_Tree (Comp); @@ -444,10 +427,7 @@ package body Sem_SPARK is -- Get_All -- ------------- - function Get_All - (T : Perm_Tree_Access) - return Perm_Tree_Access - is + function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is begin return T.all.Tree.Get_All; end Get_All; @@ -456,10 +436,7 @@ package body Sem_SPARK is -- Get_Elem -- -------------- - function Get_Elem - (T : Perm_Tree_Access) - return Perm_Tree_Access - is + function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is begin return T.all.Tree.Get_Elem; end Get_Elem; @@ -468,10 +445,7 @@ package body Sem_SPARK is -- Is_Node_Deep -- ------------------ - function Is_Node_Deep - (T : Perm_Tree_Access) - return Boolean - is + function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is begin return T.all.Tree.Is_Node_Deep; end Is_Node_Deep; @@ -480,10 +454,7 @@ package body Sem_SPARK is -- Kind -- ---------- - function Kind - (T : Perm_Tree_Access) - return Path_Kind - is + function Kind (T : Perm_Tree_Access) return Path_Kind is begin return T.all.Tree.Kind; end Kind; @@ -494,7 +465,7 @@ package body Sem_SPARK is function Other_Components (T : Perm_Tree_Access) - return Perm_Tree_Access + return Perm_Tree_Access is begin return T.all.Tree.Other_Components; @@ -504,10 +475,7 @@ package body Sem_SPARK is -- Permission -- ---------------- - function Permission - (T : Perm_Tree_Access) - return Perm_Kind - is + function Permission (T : Perm_Tree_Access) return Perm_Kind is begin return T.all.Tree.Permission; end Permission; @@ -516,13 +484,10 @@ package body Sem_SPARK is -- Perm_Mismatch -- ------------------- - procedure Perm_Mismatch - (Exp_Perm, Act_Perm : Perm_Kind; - N : Node_Id) - is + procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is begin - Error_Msg_N ("\expected at least `" - & Perm_Kind'Image (Exp_Perm) & "`, got `" + Error_Msg_N ("\expected state `" + & Perm_Kind'Image (Exp_Perm) & "` at least, got `" & Perm_Kind'Image (Act_Perm) & "`", N); end Perm_Mismatch; @@ -543,34 +508,29 @@ package body Sem_SPARK is -- Default mode. Checks that paths have Read_Perm permission. Move, - -- Regular moving semantics (not under 'Access). Checks that paths have - -- Read_Write permission. After moving a path, its permission is set to - -- Write_Only and the permission of its extensions is set to No_Access. + -- Regular moving semantics. Checks that paths have + -- Unrestricted permission. After moving a path, its permission is set + -- to Unrestricted and the permission of its extensions is set + -- to Unrestricted. Assign, -- Used for the target of an assignment, or an actual parameter with - -- mode OUT. Checks that paths have Write_Perm permission. After - -- assigning to a path, its permission is set to Read_Write. - - Super_Move, - -- Enhanced moving semantics (under 'Access). Checks that paths have - -- Read_Write permission (shallow types may have only Write permission). - -- After moving a path, its permission is set to No_Access, as well as - -- the permission of its extensions and the permission of its prefixes - -- up to the first Reference node. - - Borrow_Out, - -- Used for actual OUT parameters. Checks that paths have Write_Perm - -- permission. After checking a path, its permission is set to Read_Only - -- when of a by-copy type, to No_Access otherwise. After the call, its - -- permission is set to Read_Write. + -- mode OUT. Checks that paths have Unrestricted permission. After + -- assigning to a path, its permission is set to Unrestricted. + + Borrow, + -- Used for the source of an assignement when initializes a stand alone + -- object of anonymous type, constant, or IN parameter and also OUT + -- or IN OUT composite object. + -- In the borrowed state, the access object is completely "dead". Observe -- Used for actual IN parameters of a scalar type. Checks that paths -- have Read_Perm permission. After checking a path, its permission - -- is set to Read_Only. + -- is set to Observed. -- -- Also used for formal IN parameters + ); type Result_Kind is (Folded, Unfolded, Function_Call); @@ -593,11 +553,6 @@ package body Sem_SPARK is -- Local subprograms -- ----------------------- - function "<=" (P1, P2 : Perm_Kind) return Boolean; - function ">=" (P1, P2 : Perm_Kind) return Boolean; - function Glb (P1, P2 : Perm_Kind) return Perm_Kind; - function Lub (P1, P2 : Perm_Kind) return Perm_Kind; - -- Checking proceduress for safe pointer usage. These procedures traverse -- the AST, check nodes for correct permissions according to SPARK RM -- 6.4.2, and update permissions depending on the node kind. @@ -608,24 +563,15 @@ package body Sem_SPARK is -- We are not in End_Of_Callee mode, hence we will save the environment -- and start from a new one. We will add in the environment all formal -- parameters as well as global used during the subprogram, with the - -- appropriate permissions (write-only for out, read-only for observed, - -- read-write for others). - -- - -- After that we analyze the body of the function, and finaly, we check - -- that each borrowed parameter and global has read-write permission. We - -- then clean up the environment and put back the saved environment. + -- appropriate permissions (unrestricted for borrowed and moved, observed + -- for observed names). procedure Check_Declaration (Decl : Node_Id); procedure Check_Expression (Expr : Node_Id); - procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode); - -- This procedure takes a global pragma and checks depending on mode: - -- Mode Read: every in global is readable - -- Mode Observe: same as Check_Param_Observes but on globals - -- Mode Borrow_Out: Check_Param_Outs for globals - -- Mode Move: Check_Param for globals with mode Read - -- Mode Assign: Check_Param for globals with mode Assign + procedure Check_Globals (N : Node_Id); + -- This procedure takes a global pragma and checks it procedure Check_List (L : List_Id); -- Calls Check_Node on each element of the list @@ -638,25 +584,15 @@ package body Sem_SPARK is procedure Check_Package_Body (Pack : Node_Id); - procedure Check_Param (Formal : Entity_Id; Actual : Node_Id); - -- This procedure takes a formal and an actual parameter and calls the - -- analyze node if the parameter is borrowed with mode in out, with the - -- appropriate Checking_Mode (Move). - - procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id); - -- This procedure takes a formal and an actual parameter and calls - -- the analyze node if the parameter is observed, with the appropriate - -- Checking_Mode. - - procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id); - -- This procedure takes a formal and an actual parameter and calls the - -- analyze node if the parameter is of mode out, with the appropriate - -- Checking_Mode. + procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and checks the + -- permission of every in-mode parameter. This includes Observing and + -- Borrowing. - procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id); + procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id); -- This procedure takes a formal and an actual parameter and checks the - -- readability of every in-mode parameter. This includes observed in, and - -- also borrowed in, that are then checked afterwards. + -- state of every out-mode and in out-mode parameter. This includes + -- Moving and Borrowing. procedure Check_Statement (Stmt : Node_Id); @@ -674,20 +610,6 @@ package body Sem_SPARK is -- appropriate subtree for that Node_Id. If the tree is folded, then -- it unrolls the tree up to the appropriate level. - function Has_Alias - (N : Node_Id) - return Boolean; - -- Function that returns whether the path given as parameter contains an - -- extension that is declared as aliased. - - function Has_Array_Component (N : Node_Id) return Boolean; - -- This function gets a Node_Id and looks recursively to find if the given - -- path has any array component. - - function Has_Function_Component (N : Node_Id) return Boolean; - -- This function gets a Node_Id and looks recursively to find if the given - -- path has any function component. - procedure Hp (P : Perm_Env); -- A procedure that outputs the hash table. This function is used only in -- the debugger to look into a hash table. @@ -698,28 +620,13 @@ package body Sem_SPARK is -- A procedure that is called when deep globals or aliased globals are used -- without any global aspect. - function Is_Borrowed_In (E : Entity_Id) return Boolean; - -- Function that tells if the given entity is a borrowed in a formal - -- parameter, that is, if it is an access-to-variable type. - function Is_Deep (E : Entity_Id) return Boolean; -- A function that can tell if a type is deep or not. Returns true if the -- type passed as argument is deep. - function Is_Shallow (E : Entity_Id) return Boolean; - -- A function that can tell if a type is shallow or not. Returns true if - -- the type passed as argument is shallow. - - function Loop_Of_Exit (N : Node_Id) return Entity_Id; - -- A function that takes an exit statement node and returns the entity of - -- the loop that this statement is exiting from. - - procedure Merge_Envs (Target : in out Perm_Env; Source : in out Perm_Env); - -- Merge Target and Source into Target, and then deallocate the Source - procedure Perm_Error - (N : Node_Id; - Perm : Perm_Kind; + (N : Node_Id; + Perm : Perm_Kind; Found_Perm : Perm_Kind); -- A procedure that is called when the permissions found contradict the -- rules established by the RM. This function is called with the node, its @@ -742,7 +649,7 @@ package body Sem_SPARK is procedure Return_Declarations (L : List_Id); -- Check correct permissions on every declared object at the end of a -- callee. Used at the end of the body of a callable entity. Checks that - -- paths of all borrowed formal parameters and global have Read_Write + -- paths of all borrowed formal parameters and global have Unrestricted -- permission. procedure Return_Globals (Subp : Entity_Id); @@ -750,65 +657,32 @@ package body Sem_SPARK is -- of the subprogram indeed have RW permission at the end of the subprogram -- execution. - procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - -- Auxiliary procedure to Return_Parameters and Return_Globals - - procedure Return_Parameters (Subp : Entity_Id); - -- Takes a subprogram as input, and checks that all borrowed parameters of - -- the subprogram indeed have RW permission at the end of the subprogram - -- execution. + procedure Return_The_Global + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id); + -- Auxiliary procedure to Return_Globals + -- There is no need to return parameters because they will be reassigned + -- their state once the subprogram returns. Local variables that have + -- borrowed, observed, or moved an actual parameter go out of the scope. procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind); -- This procedure takes an access to a permission tree and modifies the -- tree so that any strict extensions of the given tree become of the -- access specified by parameter P. - procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id); - -- Set permissions to - -- No for any extension with more .all - -- W for any deep extension with same number of .all - -- RW for any shallow extension with same number of .all - - function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access; - -- This function takes a name as an input and sets in the permission - -- tree the given permission to the given name. The general rule here is - -- that everybody updates the permission of the subtree it is returning. - -- The permission of the assigned path has been set to RW by the caller. - -- - -- Case where we have to normalize a tree after the correct permissions - -- have been assigned already. We look for the right subtree at the given - -- path, actualize its permissions, and then call the normalization on its - -- parent. - -- - -- Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will - -- change the permission of x to RW because all of its components have - -- permission have permission RW. - - function Set_Perm_Prefixes_Borrow_Out (N : Node_Id) return Perm_Tree_Access; + function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access; -- This function modifies the permissions of a given node_id in the -- permission environment as well as in all the prefixes of the path, -- given that the path is borrowed with mode out. - function Set_Perm_Prefixes_Move - (N : Node_Id; Mode : Checking_Mode) + function Set_Perm_Prefixes + (N : Node_Id; + New_Perm : Perm_Kind) return Perm_Tree_Access; - pragma Precondition (Mode = Move or Mode = Super_Move); - -- Given a node and a mode (that can be either Move or Super_Move), this - -- function modifies the permissions of a given node_id in the permission - -- environment as well as all the prefixes of the path, given that the path - -- is moved with or without 'Access. The general rule here is everybody - -- updates the permission of the subtree they are returning. - -- - -- This case describes a move either under 'Access or without 'Access. - - function Set_Perm_Prefixes_Observe (N : Node_Id) return Perm_Tree_Access; - -- This function modifies the permissions of a given node_id in the - -- permission environment as well as all the prefixes of the path, - -- given that the path is observed. + -- This function sets the permissions of a given node_id in the + -- permission environment as well as in all the prefixes of the path + -- to the one given in parameter (P). procedure Setup_Globals (Subp : Entity_Id); -- Takes a subprogram as input, and sets up the environment by adding @@ -824,6 +698,15 @@ package body Sem_SPARK is -- Takes a subprogram as input, and sets up the environment by adding -- formal parameters with appropriate permissions. + function Has_Ownership_Aspect_True + (N : Node_Id; + Msg : String) + return Boolean; + -- Takes a node as an input, and finds out whether it has ownership aspect + -- True or False. This function is recursive whenever the node has a + -- composite type. Access-to-objects have ownership aspect False if they + -- have a general access type. + ---------------------- -- Global Variables -- ---------------------- @@ -861,31 +744,6 @@ package body Sem_SPARK is -- after declaration. Hence we can exclude from analysis variables that -- are just declared and never accessed, typically at package declaration. - ---------- - -- "<=" -- - ---------- - - function "<=" (P1, P2 : Perm_Kind) return Boolean - is - begin - return P2 >= P1; - end "<="; - - ---------- - -- ">=" -- - ---------- - - function ">=" (P1, P2 : Perm_Kind) return Boolean - is - begin - case P2 is - when No_Access => return True; - when Read_Only => return P1 in Read_Perm; - when Write_Only => return P1 in Write_Perm; - when Read_Write => return P1 = Read_Write; - end case; - end ">="; - -------------------------- -- Check_Call_Statement -- -------------------------- @@ -893,64 +751,40 @@ package body Sem_SPARK is procedure Check_Call_Statement (Call : Node_Id) is Saved_Env : Perm_Env; - procedure Iterate_Call is new - Iterate_Call_Parameters (Check_Param); - procedure Iterate_Call_Observes is new - Iterate_Call_Parameters (Check_Param_Observes); - procedure Iterate_Call_Outs is new - Iterate_Call_Parameters (Check_Param_Outs); - procedure Iterate_Call_Read is new - Iterate_Call_Parameters (Check_Param_Read); + procedure Iterate_Call_In is new + Iterate_Call_Parameters (Check_Param_In); + procedure Iterate_Call_Out is new + Iterate_Call_Parameters (Check_Param_Out); begin -- Save environment, so that the modifications done by analyzing the -- parameters are not kept at the end of the call. - Copy_Env (Current_Perm_Env, - Saved_Env); - - -- We first check the Read access on every in parameter - Current_Checking_Mode := Read; - Iterate_Call_Read (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), Read); - - -- We first observe, then borrow with mode out, and then with other - -- modes. This ensures that we do not have to check for by-copy types - -- specially, because we read them before borrowing them. - - Iterate_Call_Observes (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), - Observe); + Copy_Env (Current_Perm_Env, Saved_Env); - Iterate_Call_Outs (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), - Borrow_Out); + -- We first check the globals then parameters to handle the + -- No_Parameter_Aliasing Restriction. An out or in-out global is + -- considered as borrowing while a parameter with the same mode is + -- a move. This order disallow passing a part of a variable to a + -- subprogram if it is referenced as a global by the callable (when + -- writable). + -- For paremeters, we fisrt check in parameters and then the out ones. + -- This is to avoid Observing or Borrowing objects that are already + -- moved. This order is not mandatory but allows to catch runtime + -- errors like null pointer dereferencement at the analysis time. - Iterate_Call (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), Move); + Current_Checking_Mode := Read; + Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global)); + Iterate_Call_In (Call); + Iterate_Call_Out (Call); -- Restore environment, because after borrowing/observing actual -- parameters, they get their permission reverted to the ones before -- the call. Free_Env (Current_Perm_Env); - - Copy_Env (Saved_Env, - Current_Perm_Env); - + Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (Saved_Env); - - -- We assign the out parameters (necessarily borrowed per RM) - Current_Checking_Mode := Assign; - Iterate_Call (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), - Assign); - end Check_Call_Statement; ------------------------- @@ -959,15 +793,12 @@ package body Sem_SPARK is procedure Check_Callable_Body (Body_N : Node_Id) is - Mode_Before : constant Checking_Mode := Current_Checking_Mode; - - Saved_Env : Perm_Env; + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + Saved_Env : Perm_Env; Saved_Init_Map : Initialization_Map; - - New_Env : Perm_Env; - - Body_Id : constant Entity_Id := Defining_Entity (Body_N); - Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); + New_Env : Perm_Env; + Body_Id : constant Entity_Id := Defining_Entity (Body_N); + Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); begin -- Check if SPARK pragma is not set to Off @@ -989,9 +820,8 @@ package body Sem_SPARK is -- Save initialization map Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map); - Current_Checking_Mode := Read; - Current_Perm_Env := New_Env; + Current_Perm_Env := New_Env; -- Add formals and globals to the environment with adequate permissions @@ -1010,23 +840,18 @@ package body Sem_SPARK is if Ekind_In (Spec_Id, E_Procedure, E_Entry) and then not No_Return (Spec_Id) then - Return_Parameters (Spec_Id); Return_Globals (Spec_Id); end if; -- Free the environments Free_Env (Current_Perm_Env); - - Copy_Env (Saved_Env, - Current_Perm_Env); - + Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (Saved_Env); -- Restore initialization map Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map); - Reset (Saved_Init_Map); -- The assignment of all out parameters will be done by caller @@ -1039,51 +864,248 @@ package body Sem_SPARK is ----------------------- procedure Check_Declaration (Decl : Node_Id) is + + Target_Ent : constant Entity_Id := Defining_Identifier (Decl); + Target_Typ : Node_Id renames Etype (Target_Ent); + Check : Boolean := True; begin case N_Declaration'(Nkind (Decl)) is when N_Full_Type_Declaration => + if not Has_Ownership_Aspect_True (Target_Ent, "type declaration") + then + Check := False; + end if; - -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE - - null; + -- ??? What about component declarations with defaults. when N_Object_Declaration => + if (Is_Access_Type (Target_Typ) + or else Is_Deep (Target_Typ)) + and then not Has_Ownership_Aspect_True + (Target_Ent, "Object declaration ") + then + Check := False; + end if; + + if Is_Anonymous_Access_Type (Target_Typ) + and then not Present (Expression (Decl)) + then + + -- ??? Check the case of default value (AI) + -- ??? How an anonymous access type can be with default exp? + + Error_Msg_NE ("? object declaration & has OAF (Anonymous " + & "access-to-object with no initialization)", + Decl, Target_Ent); + + -- If it it an initialization + + elsif Present (Expression (Decl)) and Check then + + -- Find out the operation to be done on the right-hand side + + -- Initializing object, access type + + if Is_Access_Type (Target_Typ) then + + -- Initializing object, constant access type + + if Is_Constant_Object (Target_Ent) then + + -- Initializing object, constant access to variable type + + if not Is_Access_Constant (Target_Typ) then + Current_Checking_Mode := Borrow; + + -- Initializing object, constant access to constant type + + -- Initializing object, + -- constant access to constant anonymous type. + + elsif Is_Anonymous_Access_Type (Target_Typ) then + + -- This is an object declaration so the target + -- of the assignement is a stand-alone object. + + Current_Checking_Mode := Observe; + + -- Initializing object, constant access to constant + -- named type. + + else + -- If named then it is a general access type + -- Hence, Has_Ownership_Aspec_True is False. + + raise Program_Error; + end if; + + -- Initializing object, variable access type + + else + -- Initializing object, variable access to variable type - -- First move the right-hand side + if not Is_Access_Constant (Target_Typ) then - Current_Checking_Mode := Move; - Check_Node (Expression (Decl)); + -- Initializing object, variable named access to + -- variable type. + + if not Is_Anonymous_Access_Type (Target_Typ) then + Current_Checking_Mode := Move; + + -- Initializing object, variable anonymous access to + -- variable type. + + else + -- This is an object declaration so the target + -- object of the assignement is a stand-alone + -- object. + + Current_Checking_Mode := Borrow; + end if; + + -- Initializing object, variable access to constant type + + else + -- Initializing object, + -- variable named access to constant type. + + if not Is_Anonymous_Access_Type (Target_Typ) then + Error_Msg_N ("assignment not allowed, Ownership " + & "Aspect False (Anonymous Access " + & "Object)", Decl); + Check := False; + + -- Initializing object, + -- variable anonymous access to constant type. + + else + -- This is an object declaration so the target + -- of the assignement is a stand-alone object. + + Current_Checking_Mode := Observe; + end if; + end if; + end if; + + -- Initializing object, composite (deep) type + + elsif Is_Deep (Target_Typ) then + + -- Initializing object, constant composite type + + if Is_Constant_Object (Target_Ent) then + Current_Checking_Mode := Observe; + + -- Initializing object, variable composite type + + else + + -- Initializing object, variable anonymous composite type + + if Nkind (Object_Definition (Decl)) = + N_Constrained_Array_Definition + + -- An N_Constrained_Array_Definition is an anonymous + -- array (to be checked). Record types are always + -- named and are considered in the else part. + + then + declare + Com_Ty : constant Node_Id := + Component_Type (Etype (Target_Typ)); + begin + + if Is_Access_Type (Com_Ty) then + + -- If components are of anonymous type + + if Is_Anonymous_Access_Type (Com_Ty) then + if Is_Access_Constant (Com_Ty) then + Current_Checking_Mode := Observe; + + else + Current_Checking_Mode := Borrow; + end if; + + else + Current_Checking_Mode := Move; + end if; + + elsif Is_Deep (Com_Ty) then + + -- This is certainly named so it is a move + + Current_Checking_Mode := Move; + end if; + end; + + else + Current_Checking_Mode := Move; + end if; + end if; + + elsif Nkind_In (Expression (Decl), + N_Attribute_Reference, + N_Attribute_Reference, + N_Expanded_Name, + N_Explicit_Dereference, + N_Indexed_Component, + N_Reference, + N_Selected_Component, + N_Slice) + then + if Is_Access_Type (Etype (Prefix (Expression (Decl)))) + or else Is_Deep (Etype (Prefix (Expression (Decl)))) + then + Current_Checking_Mode := Observe; + Check := True; + end if; + end if; + end if; + + if Check then + Check_Node (Expression (Decl)); + end if; + + -- If lhs is not a pointer, we still give it the appropriate + -- state which is useless but not harmful. declare - Deep : constant Boolean := - Is_Deep (Etype (Defining_Identifier (Decl))); Elem : Perm_Tree_Access; + Deep : constant Boolean := Is_Deep (Target_Typ); begin - Elem := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Deep, - Permission => Read_Write, - Children_Permission => Read_Write)); - - -- If unitialized declaration, then set to Write_Only. If a - -- pointer declaration, it has a null default initialization. - - if No (Expression (Decl)) - and then not Has_Full_Default_Initialization - (Etype (Defining_Identifier (Decl))) - and then not Is_Access_Type - (Etype (Defining_Identifier (Decl))) - - -- Objects of shallow types are considered as always - -- initialized, leaving the checking of initialization to - -- flow analysis. - - and then Deep - then - Elem.all.Tree.Permission := Write_Only; - Elem.all.Tree.Children_Permission := Write_Only; + -- Note that all declared variables are set to the unrestricted + -- state. + -- + -- If variables are not initialized: + -- unrestricted to every declared object. + -- Exp: + -- R : Rec + -- S : Rec := (...) + -- R := S + -- The assignement R := S is not allowed in the new rules + -- if R is not unrestricted. + -- + -- If variables are initialized: + -- If it is a move, then the target is unrestricted + -- If it is a borrow, then the target is unrestricted + -- If it is an observe, then the target should be observed + + if Current_Checking_Mode = Observe then + Elem := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Deep, + Permission => Observed, + Children_Permission => Observed)); + else + Elem := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Deep, + Permission => Unrestricted, + Children_Permission => Unrestricted)); end if; -- Create new tree for defining identifier @@ -1091,7 +1113,6 @@ package body Sem_SPARK is Set (Current_Perm_Env, Unique_Entity (Defining_Identifier (Decl)), Elem); - pragma Assert (Get_First (Current_Perm_Env) /= null); end; @@ -1099,19 +1120,17 @@ package body Sem_SPARK is Check_Node (Subtype_Indication (Decl)); when N_Iterator_Specification => - pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl)))); null; when N_Loop_Parameter_Specification => - pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl)))); null; -- Checking should not be called directly on these nodes - when N_Component_Declaration - | N_Function_Specification + when N_Function_Specification | N_Entry_Declaration | N_Procedure_Specification + | N_Component_Declaration => raise Program_Error; @@ -1141,29 +1160,33 @@ package body Sem_SPARK is Mode_Before : constant Checking_Mode := Current_Checking_Mode; begin case N_Subexpr'(Nkind (Expr)) is - when N_Procedure_Call_Statement => + when N_Procedure_Call_Statement + | N_Function_Call + => Check_Call_Statement (Expr); when N_Identifier | N_Expanded_Name => -- Check if identifier is pointing to nothing (On/Off/...) + if not Present (Entity (Expr)) then return; end if; -- Do not analyze things that are not of object Kind + if Ekind (Entity (Expr)) not in Object_Kind then return; end if; -- Consider as ident + Process_Path (Expr); -- Switch to read mode and then check the readability of each operand when N_Binary_Op => - Current_Checking_Mode := Read; Check_Node (Left_Opnd (Expr)); Check_Node (Right_Opnd (Expr)); @@ -1175,7 +1198,6 @@ package body Sem_SPARK is | N_Op_Not | N_Op_Plus => - pragma Assert (Is_Shallow (Etype (Expr))); Current_Checking_Mode := Read; Check_Node (Right_Opnd (Expr)); @@ -1184,32 +1206,7 @@ package body Sem_SPARK is when N_Attribute_Reference => case Attribute_Name (Expr) is when Name_Access => - case Current_Checking_Mode is - when Read => - Check_Node (Prefix (Expr)); - - when Move => - Current_Checking_Mode := Super_Move; - Check_Node (Prefix (Expr)); - - -- Only assign names, not expressions - - when Assign => - raise Program_Error; - - -- Prefix in Super_Move should be a name, error here - - when Super_Move => - raise Program_Error; - - -- Could only borrow names of mode out, not n'Access - - when Borrow_Out => - raise Program_Error; - - when Observe => - Check_Node (Prefix (Expr)); - end case; + Error_Msg_N ("access attribute not allowed in SPARK", Expr); when Name_Last | Name_First @@ -1239,7 +1236,7 @@ package body Sem_SPARK is Check_Node (Prefix (Expr)); when Name_Pred - | Name_Succ + | Name_Succ => Check_List (Expressions (Expr)); Check_Node (Prefix (Expr)); @@ -1254,12 +1251,12 @@ package body Sem_SPARK is -- analysis. when Name_Address - | Name_Alignment - | Name_Component_Size - | Name_First_Bit - | Name_Last_Bit - | Name_Size - | Name_Position + | Name_Alignment + | Name_Component_Size + | Name_First_Bit + | Name_Last_Bit + | Name_Size + | Name_Position => null; @@ -1270,7 +1267,6 @@ package body Sem_SPARK is | Name_Val => null; - -- Other attributes that fall out of the scope of the analysis when others => @@ -1292,17 +1288,12 @@ package body Sem_SPARK is when N_And_Then | N_Or_Else => - pragma Assert (Is_Shallow (Etype (Expr))); Current_Checking_Mode := Read; Check_Node (Left_Opnd (Expr)); Check_Node (Right_Opnd (Expr)); -- Check the arguments of the call - when N_Function_Call => - Current_Checking_Mode := Read; - Check_List (Parameter_Associations (Expr)); - when N_Explicit_Dereference => Process_Path (Expr); @@ -1315,20 +1306,16 @@ package body Sem_SPARK is -- Accumulator for the different branches New_Env : Perm_Env; - - Elmt : Node_Id := First (Expressions (Expr)); + Elmt : Node_Id := First (Expressions (Expr)); begin Current_Checking_Mode := Read; - Check_Node (Elmt); - Current_Checking_Mode := Mode_Before; -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); + Copy_Env (Current_Perm_Env, Saved_Env); -- Here we have the original env in saved, current with a fresh -- copy, and new aliased. @@ -1341,15 +1328,10 @@ package body Sem_SPARK is -- Here the new_environment contains curr env after then block -- ELSE part - -- Restore environment before if - Copy_Env (Current_Perm_Env, - New_Env); - + Copy_Env (Current_Perm_Env, New_Env); Free_Env (Current_Perm_Env); - - Copy_Env (Saved_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); -- Here new environment contains the environment after then and -- current the fresh copy of old one. @@ -1357,14 +1339,9 @@ package body Sem_SPARK is Next (Elmt); Check_Node (Elmt); - Merge_Envs (New_Env, - Current_Perm_Env); - -- CLEANUP - Copy_Env (New_Env, - Current_Perm_Env); - + Copy_Env (New_Env, Current_Perm_Env); Free_Env (New_Env); Free_Env (Saved_Env); end; @@ -1380,6 +1357,7 @@ package body Sem_SPARK is when N_Quantified_Expression => declare Saved_Env : Perm_Env; + begin Copy_Env (Current_Perm_Env, Saved_Env); Current_Checking_Mode := Read; @@ -1391,7 +1369,6 @@ package body Sem_SPARK is Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (Saved_Env); end; - -- Analyze the list of associations in the aggregate when N_Aggregate => @@ -1408,19 +1385,16 @@ package body Sem_SPARK is -- Accumulator for the different branches New_Env : Perm_Env; - Elmt : Node_Id := First (Alternatives (Expr)); begin Current_Checking_Mode := Read; Check_Node (Expression (Expr)); - Current_Checking_Mode := Mode_Before; -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); + Copy_Env (Current_Perm_Env, Saved_Env); -- Here we have the original env in saved, current with a fresh -- copy, and new aliased. @@ -1429,43 +1403,29 @@ package body Sem_SPARK is Check_Node (Elmt); Next (Elmt); - - Copy_Env (Current_Perm_Env, - New_Env); - + Copy_Env (Current_Perm_Env, New_Env); Free_Env (Current_Perm_Env); -- Other alternatives while Present (Elmt) loop - -- Restore environment - Copy_Env (Saved_Env, - Current_Perm_Env); + -- Restore environment + Copy_Env (Saved_Env, Current_Perm_Env); Check_Node (Elmt); - - -- Merge Current_Perm_Env into New_Env - - Merge_Envs (New_Env, - Current_Perm_Env); - Next (Elmt); end loop; - -- CLEANUP - Copy_Env (New_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (New_Env); Free_Env (Saved_Env); end; - -- Analyze the list of associates in the aggregate as well as the -- ancestor part. when N_Extension_Aggregate => - Check_Node (Ancestor_Part (Expr)); Check_List (Expressions (Expr)); @@ -1507,7 +1467,6 @@ package body Sem_SPARK is | N_Raise_xxx_Error => null; - -- The following nodes are never generated in GNATprove mode when N_Expression_With_Actions @@ -1515,7 +1474,6 @@ package body Sem_SPARK is | N_Unchecked_Expression => raise Program_Error; - end case; end Check_Expression; @@ -1523,150 +1481,63 @@ package body Sem_SPARK is -- Check_Globals -- ------------------- - procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is + procedure Check_Globals (N : Node_Id) is begin if Nkind (N) = N_Empty then return; end if; declare - pragma Assert - (List_Length (Pragma_Argument_Associations (N)) = 1); - - PAA : constant Node_Id := - First (Pragma_Argument_Associations (N)); + pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1); + PAA : constant Node_Id := First (Pragma_Argument_Associations (N)); pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association); - Row : Node_Id; The_Mode : Name_Id; RHS : Node_Id; - procedure Process (Mode : Name_Id; - The_Global : Entity_Id); - - procedure Process (Mode : Name_Id; - The_Global : Node_Id) - is - Ident_Elt : constant Entity_Id := + procedure Process (Mode : Name_Id; The_Global : Entity_Id); + procedure Process (Mode : Name_Id; The_Global : Node_Id) is + Ident_Elt : constant Entity_Id := Unique_Entity (Entity (The_Global)); - Mode_Before : constant Checking_Mode := Current_Checking_Mode; begin if Ekind (Ident_Elt) = E_Abstract_State then return; end if; + case Mode is + when Name_Input + | Name_Proof_In + => + Current_Checking_Mode := Observe; + Check_Node (The_Global); - case Check_Mode is - when Read => - case Mode is - when Name_Input - | Name_Proof_In - => - Check_Node (The_Global); + when Name_Output + | Name_In_Out + => + -- ??? Borrow not Move? + Current_Checking_Mode := Borrow; + Check_Node (The_Global); - when Name_Output - | Name_In_Out - => - null; + when others => + raise Program_Error; + end case; + Current_Checking_Mode := Mode_Before; + end Process; - when others => - raise Program_Error; + begin + if Nkind (Expression (PAA)) = N_Null then - end case; - - when Observe => - case Mode is - when Name_Input - | Name_Proof_In - => - if not Is_Borrowed_In (Ident_Elt) then - -- Observed in - - Current_Checking_Mode := Observe; - Check_Node (The_Global); - end if; - - when others => - null; - - end case; - - when Borrow_Out => - - case Mode is - when Name_Output => - -- Borrowed out - Current_Checking_Mode := Borrow_Out; - Check_Node (The_Global); - - when others => - null; - - end case; - - when Move => - case Mode is - when Name_Input - | Name_Proof_In - => - if Is_Borrowed_In (Ident_Elt) then - -- Borrowed in - - Current_Checking_Mode := Move; - else - -- Observed - - return; - end if; - - when Name_Output => - return; - - when Name_In_Out => - -- Borrowed in out - - Current_Checking_Mode := Move; - - when others => - raise Program_Error; - end case; - - Check_Node (The_Global); - when Assign => - case Mode is - when Name_Input - | Name_Proof_In - => - null; - - when Name_Output - | Name_In_Out - => - -- Borrowed out or in out - - Process_Path (The_Global); - - when others => - raise Program_Error; - end case; - - when others => - raise Program_Error; - end case; - - Current_Checking_Mode := Mode_Before; - end Process; - - begin - if Nkind (Expression (PAA)) = N_Null then -- global => null -- No globals, nothing to do + return; elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then + -- global => foo -- A single input + Process (Name_Input, Expression (PAA)); elsif Nkind (Expression (PAA)) = N_Aggregate @@ -1674,6 +1545,7 @@ package body Sem_SPARK is then -- global => (foo, bar) -- Inputs + RHS := First (Expressions (Expression (PAA))); while Present (RHS) loop case Nkind (RHS) is @@ -1687,7 +1559,6 @@ package body Sem_SPARK is when others => raise Program_Error; - end case; RHS := Next (RHS); end loop; @@ -1707,8 +1578,8 @@ package body Sem_SPARK is while Present (Row) loop pragma Assert (List_Length (Choices (Row)) = 1); The_Mode := Chars (First (Choices (Row))); - RHS := Expression (Row); + case Nkind (RHS) is when N_Aggregate => RHS := First (Expressions (RHS)); @@ -1719,7 +1590,6 @@ package body Sem_SPARK is when others => Process (The_Mode, RHS); - end case; RHS := Next (RHS); end loop; @@ -1737,9 +1607,7 @@ package body Sem_SPARK is when others => raise Program_Error; - end case; - Row := Next (Row); end loop; end; @@ -1770,339 +1638,6 @@ package body Sem_SPARK is procedure Check_Loop_Statement (Loop_N : Node_Id) is - -- Local Subprograms - - procedure Check_Is_Less_Restrictive_Env - (Exiting_Env : Perm_Env; - Entry_Env : Perm_Env); - -- This procedure checks that the Exiting_Env environment is less - -- restrictive than the Entry_Env environment. - - procedure Check_Is_Less_Restrictive_Tree - (New_Tree : Perm_Tree_Access; - Orig_Tree : Perm_Tree_Access; - E : Entity_Id); - -- Auxiliary procedure to check that the tree New_Tree is less - -- restrictive than the tree Orig_Tree for the entity E. - - procedure Perm_Error_Loop_Exit - (E : Entity_Id; - Loop_Id : Node_Id; - Perm : Perm_Kind; - Found_Perm : Perm_Kind); - -- A procedure that is called when the permissions found contradict - -- the rules established by the RM at the exit of loops. This function - -- is called with the entity, the node of the enclosing loop, the - -- permission that was expected and the permission found, and issues - -- an appropriate error message. - - ----------------------------------- - -- Check_Is_Less_Restrictive_Env -- - ----------------------------------- - - procedure Check_Is_Less_Restrictive_Env - (Exiting_Env : Perm_Env; - Entry_Env : Perm_Env) - is - Comp_Entry : Perm_Tree_Maps.Key_Option; - Iter_Entry, Iter_Exit : Perm_Tree_Access; - - begin - Comp_Entry := Get_First_Key (Entry_Env); - while Comp_Entry.Present loop - Iter_Entry := Get (Entry_Env, Comp_Entry.K); - pragma Assert (Iter_Entry /= null); - Iter_Exit := Get (Exiting_Env, Comp_Entry.K); - pragma Assert (Iter_Exit /= null); - Check_Is_Less_Restrictive_Tree - (New_Tree => Iter_Exit, - Orig_Tree => Iter_Entry, - E => Comp_Entry.K); - Comp_Entry := Get_Next_Key (Entry_Env); - end loop; - end Check_Is_Less_Restrictive_Env; - - ------------------------------------ - -- Check_Is_Less_Restrictive_Tree -- - ------------------------------------ - - procedure Check_Is_Less_Restrictive_Tree - (New_Tree : Perm_Tree_Access; - Orig_Tree : Perm_Tree_Access; - E : Entity_Id) - is - ----------------------- - -- Local Subprograms -- - ----------------------- - - procedure Check_Is_Less_Restrictive_Tree_Than - (Tree : Perm_Tree_Access; - Perm : Perm_Kind; - E : Entity_Id); - -- Auxiliary procedure to check that the tree N is less restrictive - -- than the given permission P. - - procedure Check_Is_More_Restrictive_Tree_Than - (Tree : Perm_Tree_Access; - Perm : Perm_Kind; - E : Entity_Id); - -- Auxiliary procedure to check that the tree N is more restrictive - -- than the given permission P. - - ----------------------------------------- - -- Check_Is_Less_Restrictive_Tree_Than -- - ----------------------------------------- - - procedure Check_Is_Less_Restrictive_Tree_Than - (Tree : Perm_Tree_Access; - Perm : Perm_Kind; - E : Entity_Id) - is - begin - if not (Permission (Tree) >= Perm) then - Perm_Error_Loop_Exit - (E, Loop_N, Permission (Tree), Perm); - end if; - - case Kind (Tree) is - when Entire_Object => - if not (Children_Permission (Tree) >= Perm) then - Perm_Error_Loop_Exit - (E, Loop_N, Children_Permission (Tree), Perm); - - end if; - - when Reference => - Check_Is_Less_Restrictive_Tree_Than - (Get_All (Tree), Perm, E); - - when Array_Component => - Check_Is_Less_Restrictive_Tree_Than - (Get_Elem (Tree), Perm, E); - - when Record_Component => - declare - Comp : Perm_Tree_Access; - begin - Comp := Perm_Tree_Maps.Get_First (Component (Tree)); - while Comp /= null loop - Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E); - Comp := - Perm_Tree_Maps.Get_Next (Component (Tree)); - end loop; - - Check_Is_Less_Restrictive_Tree_Than - (Other_Components (Tree), Perm, E); - end; - end case; - end Check_Is_Less_Restrictive_Tree_Than; - - ----------------------------------------- - -- Check_Is_More_Restrictive_Tree_Than -- - ----------------------------------------- - - procedure Check_Is_More_Restrictive_Tree_Than - (Tree : Perm_Tree_Access; - Perm : Perm_Kind; - E : Entity_Id) - is - begin - if not (Perm >= Permission (Tree)) then - Perm_Error_Loop_Exit - (E, Loop_N, Permission (Tree), Perm); - end if; - - case Kind (Tree) is - when Entire_Object => - if not (Perm >= Children_Permission (Tree)) then - Perm_Error_Loop_Exit - (E, Loop_N, Children_Permission (Tree), Perm); - end if; - - when Reference => - Check_Is_More_Restrictive_Tree_Than - (Get_All (Tree), Perm, E); - - when Array_Component => - Check_Is_More_Restrictive_Tree_Than - (Get_Elem (Tree), Perm, E); - - when Record_Component => - declare - Comp : Perm_Tree_Access; - begin - Comp := Perm_Tree_Maps.Get_First (Component (Tree)); - while Comp /= null loop - Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E); - Comp := - Perm_Tree_Maps.Get_Next (Component (Tree)); - end loop; - - Check_Is_More_Restrictive_Tree_Than - (Other_Components (Tree), Perm, E); - end; - end case; - end Check_Is_More_Restrictive_Tree_Than; - - -- Start of processing for Check_Is_Less_Restrictive_Tree - - begin - if not (Permission (New_Tree) <= Permission (Orig_Tree)) then - Perm_Error_Loop_Exit - (E => E, - Loop_Id => Loop_N, - Perm => Permission (New_Tree), - Found_Perm => Permission (Orig_Tree)); - end if; - - case Kind (New_Tree) is - - -- Potentially folded tree. We check the other tree Orig_Tree to - -- check whether it is folded or not. If folded we just compare - -- their Permission and Children_Permission, if not, then we - -- look at the Children_Permission of the folded tree against - -- the unfolded tree Orig_Tree. - - when Entire_Object => - case Kind (Orig_Tree) is - when Entire_Object => - if not (Children_Permission (New_Tree) <= - Children_Permission (Orig_Tree)) - then - Perm_Error_Loop_Exit - (E, Loop_N, - Children_Permission (New_Tree), - Children_Permission (Orig_Tree)); - end if; - - when Reference => - Check_Is_More_Restrictive_Tree_Than - (Get_All (Orig_Tree), Children_Permission (New_Tree), E); - - when Array_Component => - Check_Is_More_Restrictive_Tree_Than - (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E); - - when Record_Component => - declare - Comp : Perm_Tree_Access; - begin - Comp := Perm_Tree_Maps.Get_First - (Component (Orig_Tree)); - while Comp /= null loop - Check_Is_More_Restrictive_Tree_Than - (Comp, Children_Permission (New_Tree), E); - Comp := Perm_Tree_Maps.Get_Next - (Component (Orig_Tree)); - end loop; - - Check_Is_More_Restrictive_Tree_Than - (Other_Components (Orig_Tree), - Children_Permission (New_Tree), E); - end; - end case; - - when Reference => - case Kind (Orig_Tree) is - when Entire_Object => - Check_Is_Less_Restrictive_Tree_Than - (Get_All (New_Tree), Children_Permission (Orig_Tree), E); - - when Reference => - Check_Is_Less_Restrictive_Tree - (Get_All (New_Tree), Get_All (Orig_Tree), E); - - when others => - raise Program_Error; - end case; - - when Array_Component => - case Kind (Orig_Tree) is - when Entire_Object => - Check_Is_Less_Restrictive_Tree_Than - (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E); - - when Array_Component => - Check_Is_Less_Restrictive_Tree - (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E); - - when others => - raise Program_Error; - end case; - - when Record_Component => - declare - CompN : Perm_Tree_Access; - begin - CompN := - Perm_Tree_Maps.Get_First (Component (New_Tree)); - case Kind (Orig_Tree) is - when Entire_Object => - while CompN /= null loop - Check_Is_Less_Restrictive_Tree_Than - (CompN, Children_Permission (Orig_Tree), E); - - CompN := - Perm_Tree_Maps.Get_Next (Component (New_Tree)); - end loop; - - Check_Is_Less_Restrictive_Tree_Than - (Other_Components (New_Tree), - Children_Permission (Orig_Tree), - E); - - when Record_Component => - declare - - KeyO : Perm_Tree_Maps.Key_Option; - CompO : Perm_Tree_Access; - begin - KeyO := Perm_Tree_Maps.Get_First_Key - (Component (Orig_Tree)); - while KeyO.Present loop - pragma Assert (CompO /= null); - - Check_Is_Less_Restrictive_Tree (CompN, CompO, E); - - KeyO := Perm_Tree_Maps.Get_Next_Key - (Component (Orig_Tree)); - CompN := Perm_Tree_Maps.Get - (Component (New_Tree), KeyO.K); - CompO := Perm_Tree_Maps.Get - (Component (Orig_Tree), KeyO.K); - end loop; - - Check_Is_Less_Restrictive_Tree - (Other_Components (New_Tree), - Other_Components (Orig_Tree), - E); - end; - - when others => - raise Program_Error; - end case; - end; - end case; - end Check_Is_Less_Restrictive_Tree; - - -------------------------- - -- Perm_Error_Loop_Exit -- - -------------------------- - - procedure Perm_Error_Loop_Exit - (E : Entity_Id; - Loop_Id : Node_Id; - Perm : Perm_Kind; - Found_Perm : Perm_Kind) - is - begin - Error_Msg_Node_2 := Loop_Id; - Error_Msg_N ("insufficient permission for & when exiting loop &", E); - Perm_Mismatch (Exp_Perm => Perm, - Act_Perm => Found_Perm, - N => Loop_Id); - end Perm_Error_Loop_Exit; - -- Local variables Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N)); @@ -2126,6 +1661,7 @@ package body Sem_SPARK is if Present (Iteration_Scheme (Loop_N)) then declare Exit_Env : constant Perm_Env_Access := new Perm_Env; + begin Copy_Env (From => Current_Perm_Env, To => Exit_Env.all); Set (Current_Loops_Accumulators, Loop_Name, Exit_Env); @@ -2137,12 +1673,6 @@ package body Sem_SPARK is Check_Node (Iteration_Scheme (Loop_N)); Check_List (Statements (Loop_N)); - -- Check that environment gets less restrictive at end of loop - - Check_Is_Less_Restrictive_Env - (Exiting_Env => Current_Perm_Env, - Entry_Env => Loop_Env.all); - -- Set environment to the one for exiting the loop declare @@ -2208,6 +1738,7 @@ package body Sem_SPARK is when N_Package_Declaration => declare Spec : constant Node_Id := Specification (N); + begin Current_Checking_Mode := Read; Check_List (Visible_Declarations (Spec)); @@ -2274,7 +1805,6 @@ package body Sem_SPARK is | N_Delay_Alternative | N_Derived_Type_Definition | N_Designator - | N_Discriminant_Association | N_Discriminant_Specification | N_Elsif_Part | N_Entry_Body_Formal_Part @@ -2366,9 +1896,12 @@ package body Sem_SPARK is | N_Use_Type_Clause | N_Validate_Unchecked_Conversion | N_Variable_Reference_Marker + | N_Discriminant_Association + + -- ??? check whether we should do sth special for + -- N_Discriminant_Association, or maybe raise a program error. => null; - -- The following nodes are rewritten by semantic analysis when N_Single_Protected_Declaration @@ -2408,15 +1941,12 @@ package body Sem_SPARK is -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); - + Copy_Env (Current_Perm_Env, Saved_Env); Check_List (Private_Declarations (CorSp)); -- Set mode to Read, and then analyze declarations and statements Current_Checking_Mode := Read; - Check_List (Declarations (Pack)); Check_Node (Handled_Statement_Sequence (Pack)); @@ -2430,137 +1960,129 @@ package body Sem_SPARK is -- declaration) from environment. Free_Env (Current_Perm_Env); - Copy_Env (Saved_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); end Check_Package_Body; - ----------------- - -- Check_Param -- - ----------------- + -------------------- + -- Check_Param_In -- + -------------------- - procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is + procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is Mode : constant Entity_Kind := Ekind (Formal); Mode_Before : constant Checking_Mode := Current_Checking_Mode; - begin - case Current_Checking_Mode is - when Read => - case Formal_Kind'(Mode) is - when E_In_Parameter => - if Is_Borrowed_In (Formal) then - -- Borrowed in - - Current_Checking_Mode := Move; - else - -- Observed + case Formal_Kind'(Mode) is - return; - end if; + -- Formal IN parameter - when E_Out_Parameter => - return; + when E_In_Parameter => - when E_In_Out_Parameter => - -- Borrowed in out + -- Formal IN parameter, access type - Current_Checking_Mode := Move; + if Is_Access_Type (Etype (Formal)) then - end case; + -- Formal IN parameter, access to variable type - Check_Node (Actual); + if not Is_Access_Constant (Etype (Formal)) then - when Assign => - case Formal_Kind'(Mode) is - when E_In_Parameter => - null; + -- Formal IN parameter, named/anonymous access to variable + -- type. - when E_Out_Parameter - | E_In_Out_Parameter - => - -- Borrowed out or in out + Current_Checking_Mode := Borrow; + Check_Node (Actual); - Process_Path (Actual); + -- Formal IN parameter, access to constant type + -- Formal IN parameter, access to named constant type - end case; + elsif not Is_Anonymous_Access_Type (Etype (Formal)) then + Error_Msg_N ("assignment not allowed, Ownership Aspect" + & " False (Named general access type)", + Formal); - when others => - raise Program_Error; + -- Formal IN parameter, access to anonymous constant type - end case; - Current_Checking_Mode := Mode_Before; - end Check_Param; + else + Current_Checking_Mode := Observe; + Check_Node (Actual); + end if; - -------------------------- - -- Check_Param_Observes -- - -------------------------- + -- Formal IN parameter, composite type - procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); - Mode_Before : constant Checking_Mode := Current_Checking_Mode; + elsif Is_Deep (Etype (Formal)) then - begin - case Mode is - when E_In_Parameter => - if not Is_Borrowed_In (Formal) then - -- Observed in + -- Composite formal types should be named + -- Formal IN parameter, composite named type Current_Checking_Mode := Observe; Check_Node (Actual); end if; - when others => + when E_Out_Parameter + | E_In_Out_Parameter + => null; - end case; Current_Checking_Mode := Mode_Before; - end Check_Param_Observes; + end Check_Param_In; ---------------------- - -- Check_Param_Outs -- + -- Check_Param_Out -- ---------------------- - procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); + procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id) is + Mode : constant Entity_Kind := Ekind (Formal); Mode_Before : constant Checking_Mode := Current_Checking_Mode; begin + case Formal_Kind'(Mode) is - case Mode is - when E_Out_Parameter => - -- Borrowed out - Current_Checking_Mode := Borrow_Out; - Check_Node (Actual); + -- Formal OUT/IN OUT parameter - when others => - null; + when E_Out_Parameter + | E_In_Out_Parameter + => - end case; + -- Formal OUT/IN OUT parameter, access type - Current_Checking_Mode := Mode_Before; - end Check_Param_Outs; + if Is_Access_Type (Etype (Formal)) then - ---------------------- - -- Check_Param_Read -- - ---------------------- + -- Formal OUT/IN OUT parameter, access to variable type - procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); + if not Is_Access_Constant (Etype (Formal)) then - begin - pragma Assert (Current_Checking_Mode = Read); + -- Cannot have anonymous out access parameter + -- Formal out/in out parameter, access to named variable + -- type. - case Formal_Kind'(Mode) is - when E_In_Parameter => - Check_Node (Actual); + Current_Checking_Mode := Move; + Check_Node (Actual); - when E_Out_Parameter - | E_In_Out_Parameter - => - null; + -- Formal out/in out parameter, access to constant type + + else + Error_Msg_N ("assignment not allowed, Ownership Aspect False" + & " (Named general access type)", Formal); + + end if; + + -- Formal out/in out parameter, composite type + + elsif Is_Deep (Etype (Formal)) then + + -- Composite formal types should be named + -- Formal out/in out Parameter, Composite Named type. + Current_Checking_Mode := Borrow; + Check_Node (Actual); + end if; + + when E_In_Parameter => + null; end case; - end Check_Param_Read; + + Current_Checking_Mode := Mode_Before; + end Check_Param_Out; ------------------------- -- Check_Safe_Pointers -- @@ -2605,13 +2127,13 @@ package body Sem_SPARK is -- Local variables Prag : Node_Id; + -- SPARK_Mode pragma in application -- Start of processing for Check_Safe_Pointers begin Initialize; - case Nkind (N) is when N_Compilation_Unit => Check_Safe_Pointers (Unit (N)); @@ -2647,33 +2169,233 @@ package body Sem_SPARK is procedure Check_Statement (Stmt : Node_Id) is Mode_Before : constant Checking_Mode := Current_Checking_Mode; - begin - case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is - when N_Entry_Call_Statement => - Check_Call_Statement (Stmt); - - -- Move right-hand side first, and then assign left-hand side + State_N : Perm_Kind; + Check : Boolean := True; + St_Name : Node_Id; + Ty_St_Name : Node_Id; - when N_Assignment_Statement => - if Is_Deep (Etype (Expression (Stmt))) then - Current_Checking_Mode := Move; - else - Current_Checking_Mode := Read; - end if; + function Get_Root (Comp_Stmt : Node_Id) return Node_Id; + -- Return the root of the name given as input - Check_Node (Expression (Stmt)); - Current_Checking_Mode := Assign; - Check_Node (Name (Stmt)); + function Get_Root (Comp_Stmt : Node_Id) return Node_Id is + begin + case Nkind (Comp_Stmt) is + when N_Identifier + | N_Expanded_Name + => return Comp_Stmt; - when N_Block_Statement => + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Get_Root (Expression (Comp_Stmt)); + + when N_Parameter_Specification => + return Get_Root (Defining_Identifier (Comp_Stmt)); + + when N_Selected_Component + | N_Indexed_Component + | N_Slice + | N_Explicit_Dereference + => + return Get_Root (Prefix (Comp_Stmt)); + + when others => + raise Program_Error; + end case; + end Get_Root; + + begin + case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is + when N_Entry_Call_Statement => + Check_Call_Statement (Stmt); + + -- Move right-hand side first, and then assign left-hand side + + when N_Assignment_Statement => + + St_Name := Name (Stmt); + Ty_St_Name := Etype (Name (Stmt)); + + -- Check that is not a *general* access type + + if Has_Ownership_Aspect_True (St_Name, "assigning to") then + + -- Assigning to access type + + if Is_Access_Type (Ty_St_Name) then + + -- Assigning to access to variable type + + if not Is_Access_Constant (Ty_St_Name) then + + -- Assigning to named access to variable type + + if not Is_Anonymous_Access_Type (Ty_St_Name) then + Current_Checking_Mode := Move; + + -- Assigning to anonymous access to variable type + + else + -- Target /= source root + + if Nkind_In (Expression (Stmt), N_Allocator, N_Null) + or else St_Name /= Get_Root (Expression (Stmt)) + then + Error_Msg_N ("assignment not allowed, anonymous " + & "access Object with Different Root", + Stmt); + Check := False; + + -- Target = source root + + else + -- Here we do nothing on the source nor on the + -- target. However, we check the the legality rule: + -- "The source shall be an owning access object + -- denoted by a name that is not in the observed + -- state". + + State_N := Get_Perm (Expression (Stmt)); + if State_N = Observed then + Error_Msg_N ("assignment not allowed, Anonymous " + & "access object with the same root" + & " but source Observed", Stmt); + Check := False; + end if; + end if; + end if; + + -- else access-to-constant + + -- Assigning to anonymous access-to-constant type + + elsif Is_Anonymous_Access_Type (Ty_St_Name) then + + -- ??? Check the follwing condition. We may have to + -- add that the root is in the observed state too. + + State_N := Get_Perm (Expression (Stmt)); + if State_N /= Observed then + Error_Msg_N ("assignment not allowed, anonymous " + & "access-to-constant object not in " + & "the observed state)", Stmt); + Check := False; + + else + Error_Msg_N ("?here check accessibility level cited in" + & " the second legality rule of assign", + Stmt); + Check := False; + end if; + + -- Assigning to named access-to-constant type: + -- This case should have been detected when checking + -- Has_Onwership_Aspect_True (Name (Stmt), "msg"). + + else + raise Program_Error; + end if; + + -- Assigning to composite (deep) type. + + elsif Is_Deep (Ty_St_Name) then + if Ekind (Ty_St_Name) = E_Record_Type then + declare + Elmt : Entity_Id := + First_Component_Or_Discriminant (Ty_St_Name); + + begin + while Present (Elmt) loop + if Is_Anonymous_Access_Type (Etype (Elmt)) or + Ekind (Elmt) = E_General_Access_Type + then + Error_Msg_N ("assignment not allowed, Ownership " + & "Aspect False (Components have " + & "Ownership Aspect False)", Stmt); + Check := False; + exit; + end if; + + Next_Component_Or_Discriminant (Elmt); + end loop; + end; + + -- Record types are always named so this is a move + + if Check then + Current_Checking_Mode := Move; + end if; + end if; + + -- Now handle legality rules of using a borrowed, observed, + -- or moved name as a prefix in an assignment. + + else + if Nkind_In (St_Name, + N_Attribute_Reference, + N_Expanded_Name, + N_Explicit_Dereference, + N_Indexed_Component, + N_Reference, + N_Selected_Component, + N_Slice) + then + + if Is_Access_Type (Etype (Prefix (St_Name))) or + Is_Deep (Etype (Prefix (St_Name))) + then + + -- We set the Check variable to True so that we can + -- Check_Node of the expression and the name first + -- under the assumption of Current_Checking_Mode = + -- Read => nothing to be done for the RHS if the + -- following check on the expression fails, and + -- Current_Checking_Mode := Assign => the name should + -- not be borrowed or observed so that we can use it + -- as a prefix in the target of an assignement. + -- + -- Note that we do not need to check the OA here + -- because we are allowed to read and write "through" + -- an object of OAF (example: traversing a DS). + + Check := True; + end if; + end if; + + if Nkind_In (Expression (Stmt), + N_Attribute_Reference, + N_Expanded_Name, + N_Explicit_Dereference, + N_Indexed_Component, + N_Reference, + N_Selected_Component, + N_Slice) + then + + if Is_Access_Type (Etype (Prefix (Expression (Stmt)))) + or else Is_Deep (Etype (Prefix (Expression (Stmt)))) + then + Current_Checking_Mode := Observe; + Check := True; + end if; + end if; + end if; + + if Check then + Check_Node (Expression (Stmt)); + Current_Checking_Mode := Assign; + Check_Node (St_Name); + end if; + end if; + + when N_Block_Statement => declare Saved_Env : Perm_Env; - begin -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); + Copy_Env (Current_Perm_Env, Saved_Env); -- Analyze declarations and Handled_Statement_Sequences @@ -2684,8 +2406,7 @@ package body Sem_SPARK is -- Restore environment Free_Env (Current_Perm_Env); - Copy_Env (Saved_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); end; when N_Case_Statement => @@ -2695,7 +2416,6 @@ package body Sem_SPARK is -- Accumulator for the different branches New_Env : Perm_Env; - Elmt : Node_Id := First (Alternatives (Stmt)); begin @@ -2705,8 +2425,7 @@ package body Sem_SPARK is -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); + Copy_Env (Current_Perm_Env, Saved_Env); -- Here we have the original env in saved, current with a fresh -- copy, and new aliased. @@ -2715,33 +2434,21 @@ package body Sem_SPARK is Check_Node (Elmt); Next (Elmt); - - Copy_Env (Current_Perm_Env, - New_Env); + Copy_Env (Current_Perm_Env, New_Env); Free_Env (Current_Perm_Env); -- Other alternatives while Present (Elmt) loop - -- Restore environment - Copy_Env (Saved_Env, - Current_Perm_Env); + -- Restore environment + Copy_Env (Saved_Env, Current_Perm_Env); Check_Node (Elmt); - - -- Merge Current_Perm_Env into New_Env - - Merge_Envs (New_Env, - Current_Perm_Env); - Next (Elmt); end loop; - -- CLEANUP - Copy_Env (New_Env, - Current_Perm_Env); - + Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (New_Env); Free_Env (Saved_Env); end; @@ -2755,7 +2462,7 @@ package body Sem_SPARK is when N_Loop_Statement => Check_Loop_Statement (Stmt); - -- If deep type expression, then move, else read + -- If deep type expression, then move, else read when N_Simple_Return_Statement => case Nkind (Expression (Stmt)) is @@ -2767,65 +2474,42 @@ package body Sem_SPARK is Subp : constant Entity_Id := Return_Applies_To (Return_Statement_Entity (Stmt)); begin - Return_Parameters (Subp); Return_Globals (Subp); end; when others => if Is_Deep (Etype (Expression (Stmt))) then Current_Checking_Mode := Move; - elsif Is_Shallow (Etype (Expression (Stmt))) then - Current_Checking_Mode := Read; else - raise Program_Error; + Check := False; end if; - Check_Node (Expression (Stmt)); + if Check then + Check_Node (Expression (Stmt)); + end if; end case; when N_Extended_Return_Statement => Check_List (Return_Object_Declarations (Stmt)); Check_Node (Handled_Statement_Sequence (Stmt)); - Return_Declarations (Return_Object_Declarations (Stmt)); - declare -- ??? This does not take into account the fact that a simple -- return inside an extended return statement applies to the -- extended return statement. Subp : constant Entity_Id := Return_Applies_To (Return_Statement_Entity (Stmt)); + begin - Return_Parameters (Subp); Return_Globals (Subp); end; - -- Merge the current_Perm_Env with the accumulator for the given loop + -- Nothing to do when exiting a loop. No merge needed when N_Exit_Statement => - declare - Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt); - - Saved_Accumulator : constant Perm_Env_Access := - Get (Current_Loops_Accumulators, Loop_Name); - - Environment_Copy : constant Perm_Env_Access := - new Perm_Env; - begin - - Copy_Env (Current_Perm_Env, - Environment_Copy.all); - - if Saved_Accumulator = null then - Set (Current_Loops_Accumulators, - Loop_Name, Environment_Copy); - else - Merge_Envs (Saved_Accumulator.all, - Environment_Copy.all); - end if; - end; + null; - -- Copy environment, run on each branch, and then merge + -- Copy environment, run on each branch when N_If_Statement => declare @@ -2836,13 +2520,11 @@ package body Sem_SPARK is New_Env : Perm_Env; begin - Check_Node (Condition (Stmt)); -- Save environment - Copy_Env (Current_Perm_Env, - Saved_Env); + Copy_Env (Current_Perm_Env, Saved_Env); -- Here we have the original env in saved, current with a fresh -- copy. @@ -2850,34 +2532,25 @@ package body Sem_SPARK is -- THEN PART Check_List (Then_Statements (Stmt)); - - Copy_Env (Current_Perm_Env, - New_Env); - + Copy_Env (Current_Perm_Env, New_Env); Free_Env (Current_Perm_Env); -- Here the new_environment contains curr env after then block -- ELSIF part + declare Elmt : Node_Id; begin Elmt := First (Elsif_Parts (Stmt)); while Present (Elmt) loop - -- Transfer into accumulator, and restore from save - Copy_Env (Saved_Env, - Current_Perm_Env); + -- Transfer into accumulator, and restore from save + Copy_Env (Saved_Env, Current_Perm_Env); Check_Node (Condition (Elmt)); Check_List (Then_Statements (Stmt)); - - -- Merge Current_Perm_Env into New_Env - - Merge_Envs (New_Env, - Current_Perm_Env); - Next (Elmt); end loop; end; @@ -2886,21 +2559,16 @@ package body Sem_SPARK is -- Restore environment before if - Copy_Env (Saved_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); -- Here new environment contains the environment after then and -- current the fresh copy of old one. Check_List (Else_Statements (Stmt)); - Merge_Envs (New_Env, - Current_Perm_Env); - -- CLEANUP - Copy_Env (New_Env, - Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (New_Env); Free_Env (Saved_Env); @@ -2956,8 +2624,7 @@ package body Sem_SPARK is -- which means that the association permission is RW. when Function_Call => - return Read_Write; - + return Unrestricted; end case; end Get_Perm; @@ -2980,7 +2647,6 @@ package body Sem_SPARK is => declare P : constant Entity_Id := Entity (N); - C : constant Perm_Tree_Access := Get (Current_Perm_Env, Unique_Entity (P)); @@ -2990,13 +2656,13 @@ package body Sem_SPARK is -- of elaboration of package. Set (Current_Initialization_Map, Unique_Entity (P), True); - if C = null then -- No null possible here, there are no parents for the path. -- This means we are using a global variable without adding -- it in environment with a global aspect. Illegal_Global_Usage (N); + else return (R => Unfolded, Tree_Access => C); end if; @@ -3023,8 +2689,7 @@ package body Sem_SPARK is when N_Selected_Component => declare - C : constant Perm_Or_Tree := - Get_Perm_Or_Tree (Prefix (N)); + C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); begin case C.R is @@ -3035,7 +2700,6 @@ package body Sem_SPARK is when Unfolded => pragma Assert (C.Tree_Access /= null); - pragma Assert (Kind (C.Tree_Access) = Entire_Object or else Kind (C.Tree_Access) = Record_Component); @@ -3044,30 +2708,32 @@ package body Sem_SPARK is declare Selected_Component : constant Entity_Id := Entity (Selector_Name (N)); - Selected_C : constant Perm_Tree_Access := Perm_Tree_Maps.Get (Component (C.Tree_Access), Selected_Component); begin if Selected_C = null then - return (R => Unfolded, + return (R => Unfolded, Tree_Access => Other_Components (C.Tree_Access)); + else - return (R => Unfolded, + return (R => Unfolded, Tree_Access => Selected_C); end if; end; + elsif Kind (C.Tree_Access) = Entire_Object then - return (R => Folded, Found_Permission => + return (R => Folded, + Found_Permission => Children_Permission (C.Tree_Access)); + else raise Program_Error; end if; end case; end; - -- We get the permission tree of its prefix, and then get either the -- subtree associated with that specific selection, or if we have a -- leaf that folds its children, we take the children's permission @@ -3077,8 +2743,7 @@ package body Sem_SPARK is | N_Slice => declare - C : constant Perm_Or_Tree := - Get_Perm_Or_Tree (Prefix (N)); + C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); begin case C.R is @@ -3089,25 +2754,24 @@ package body Sem_SPARK is when Unfolded => pragma Assert (C.Tree_Access /= null); - pragma Assert (Kind (C.Tree_Access) = Entire_Object or else Kind (C.Tree_Access) = Array_Component); if Kind (C.Tree_Access) = Array_Component then pragma Assert (Get_Elem (C.Tree_Access) /= null); - return (R => Unfolded, Tree_Access => Get_Elem (C.Tree_Access)); + elsif Kind (C.Tree_Access) = Entire_Object then return (R => Folded, Found_Permission => Children_Permission (C.Tree_Access)); + else raise Program_Error; end if; end case; end; - -- We get the permission tree of its prefix, and then get either the -- subtree associated with that specific selection, or if we have a -- leaf that folds its children, we take the children's permission @@ -3115,8 +2779,7 @@ package body Sem_SPARK is when N_Explicit_Dereference => declare - C : constant Perm_Or_Tree := - Get_Perm_Or_Tree (Prefix (N)); + C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); begin case C.R is @@ -3127,29 +2790,32 @@ package body Sem_SPARK is when Unfolded => pragma Assert (C.Tree_Access /= null); - pragma Assert (Kind (C.Tree_Access) = Entire_Object or else Kind (C.Tree_Access) = Reference); if Kind (C.Tree_Access) = Reference then if Get_All (C.Tree_Access) = null then + -- Hash_Table_Error + raise Program_Error; + else return (R => Unfolded, Tree_Access => Get_All (C.Tree_Access)); end if; + elsif Kind (C.Tree_Access) = Entire_Object then return (R => Folded, Found_Permission => Children_Permission (C.Tree_Access)); + else raise Program_Error; end if; end case; end; - -- The name contains a function call, hence the given path is always -- new. We do not have to check for anything. @@ -3165,10 +2831,7 @@ package body Sem_SPARK is -- Get_Perm_Tree -- ------------------- - function Get_Perm_Tree - (N : Node_Id) - return Perm_Tree_Access - is + function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is begin case Nkind (N) is @@ -3183,7 +2846,6 @@ package body Sem_SPARK is => declare P : constant Node_Id := Entity (N); - C : constant Perm_Tree_Access := Get (Current_Perm_Env, Unique_Entity (P)); @@ -3193,13 +2855,13 @@ package body Sem_SPARK is -- of elaboration of package. Set (Current_Initialization_Map, Unique_Entity (P), True); - if C = null then -- No null possible here, there are no parents for the path. -- This means we are using a global variable without adding -- it in environment with a global aspect. Illegal_Global_Usage (N); + else return C; end if; @@ -3220,11 +2882,11 @@ package body Sem_SPARK is when N_Selected_Component => declare - C : constant Perm_Tree_Access := - Get_Perm_Tree (Prefix (N)); + C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N)); begin if C = null then + -- If null then it means we went through a function call return null; @@ -3234,6 +2896,7 @@ package body Sem_SPARK is or else Kind (C) = Record_Component); if Kind (C) = Record_Component then + -- The tree is unfolded. We just return the subtree. declare @@ -3247,9 +2910,9 @@ package body Sem_SPARK is if Selected_C = null then return Other_Components (C); end if; - return Selected_C; end; + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with @@ -3265,7 +2928,6 @@ package body Sem_SPARK is Children_Permission (C); begin - -- We change the current node from Entire_Object to -- Record_Component with same permission and an empty -- hash table as component list. @@ -3288,6 +2950,7 @@ package body Sem_SPARK is -- We fill the hash table with all sons of the record, -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (Etype (Prefix (N))); @@ -3301,10 +2964,8 @@ package body Sem_SPARK is Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son); - Next_Component_Or_Discriminant (Elem); end loop; - -- we return the tree to the sons, so that the recursion -- can continue. @@ -3318,16 +2979,13 @@ package body Sem_SPARK is begin pragma Assert (Selected_C /= null); - return Selected_C; end; - end; else raise Program_Error; end if; end; - -- We set the permission tree of its prefix, and then we extract from -- the returned pointer the subtree. If folded, we unroll the tree at -- one step. @@ -3336,8 +2994,7 @@ package body Sem_SPARK is | N_Slice => declare - C : constant Perm_Tree_Access := - Get_Perm_Tree (Prefix (N)); + C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N)); begin if C = null then @@ -3345,16 +3002,16 @@ package body Sem_SPARK is return null; end if; - pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Array_Component); if Kind (C) = Array_Component then + -- The tree is unfolded. We just return the elem subtree pragma Assert (Get_Elem (C) = null); - return Get_Elem (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace node with Array_Component. @@ -3377,14 +3034,12 @@ package body Sem_SPARK is Is_Node_Deep => Is_Node_Deep (C), Permission => Permission (C), Get_Elem => Son); - return Get_Elem (C); end; else raise Program_Error; end if; end; - -- We get the permission tree of its prefix, and then get either the -- subtree associated with that specific selection, or if we have a -- leaf that folds its children, we unroll the tree. @@ -3397,6 +3052,7 @@ package body Sem_SPARK is C := Get_Perm_Tree (Prefix (N)); if C = null then + -- If null, we went through a function call return null; @@ -3406,14 +3062,17 @@ package body Sem_SPARK is or else Kind (C) = Reference); if Kind (C) = Reference then + -- The tree is unfolded. We return the elem subtree if Get_All (C) = null then + -- Hash_Table_Error + raise Program_Error; end if; - return Get_All (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with Reference. @@ -3432,19 +3091,16 @@ package body Sem_SPARK is -- Reference with same permission and the previous son. pragma Assert (Is_Node_Deep (C)); - C.all.Tree := (Kind => Reference, Is_Node_Deep => Is_Node_Deep (C), Permission => Permission (C), Get_All => Son); - return Get_All (C); end; else raise Program_Error; end if; end; - -- No permission tree for function calls when N_Function_Call => @@ -3455,316 +3111,65 @@ package body Sem_SPARK is end case; end Get_Perm_Tree; - --------- - -- Glb -- - --------- + -------- + -- Hp -- + -------- - function Glb (P1, P2 : Perm_Kind) return Perm_Kind - is - begin - case P1 is - when No_Access => - return No_Access; - - when Read_Only => - case P2 is - when No_Access - | Write_Only - => - return No_Access; + procedure Hp (P : Perm_Env) is + Elem : Perm_Tree_Maps.Key_Option; - when Read_Perm => - return Read_Only; - end case; + begin + Elem := Get_First_Key (P); + while Elem.Present loop + Print_Node_Briefly (Elem.K); + Elem := Get_Next_Key (P); + end loop; + end Hp; - when Write_Only => - case P2 is - when No_Access - | Read_Only - => - return No_Access; + -------------------------- + -- Illegal_Global_Usage -- + -------------------------- - when Write_Perm => - return Write_Only; - end case; + procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is + begin + Error_Msg_NE ("cannot use global variable & of deep type", N, N); + Error_Msg_N ("\without prior declaration in a Global aspect", N); + Errout.Finalize (Last_Call => True); + Errout.Output_Messages; + Exit_Program (E_Errors); + end Illegal_Global_Usage; - when Read_Write => - return P2; - end case; - end Glb; + ------------- + -- Is_Deep -- + ------------- - --------------- - -- Has_Alias -- - --------------- + function Is_Deep (E : Entity_Id) return Boolean is + function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean; + function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is + Decl : Node_Id; + Pack_Decl : Node_Id; - function Has_Alias - (N : Node_Id) - return Boolean - is - function Has_Alias_Deep (Typ : Entity_Id) return Boolean; - function Has_Alias_Deep (Typ : Entity_Id) return Boolean - is - Comp : Node_Id; begin + if Is_Itype (E) then + Decl := Associated_Node_For_Itype (E); + else + Decl := Parent (E); + end if; - if Is_Array_Type (Typ) - and then Has_Aliased_Components (Typ) - then - return True; - - -- Note: Has_Aliased_Components applies only to arrays - - elsif Is_Record_Type (Typ) then - -- It is possible to have an aliased discriminant, so they must be - -- checked along with normal components. - - Comp := First_Component_Or_Discriminant (Typ); - while Present (Comp) loop - if Is_Aliased (Comp) - or else Is_Aliased (Etype (Comp)) - then - return True; - end if; - - if Has_Alias_Deep (Etype (Comp)) then - return True; - end if; + Pack_Decl := Parent (Parent (Decl)); - Next_Component_Or_Discriminant (Comp); - end loop; + if Nkind (Pack_Decl) /= N_Package_Declaration then return False; - else - return Is_Aliased (Typ); end if; - end Has_Alias_Deep; - begin - case Nkind (N) is + return + Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) + and then Get_SPARK_Mode_From_Annotation + (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off; + end Is_Private_Entity_Mode_Off; - when N_Identifier - | N_Expanded_Name - => - return Is_Aliased (Entity (N)) or else Has_Alias_Deep (Etype (N)); - - when N_Defining_Identifier => - return Is_Aliased (N) or else Has_Alias_Deep (Etype (N)); - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Has_Alias (Expression (N)); - - when N_Parameter_Specification => - return Has_Alias (Defining_Identifier (N)); - - when N_Selected_Component => - case Nkind (Selector_Name (N)) is - when N_Identifier => - if Is_Aliased (Entity (Selector_Name (N))) then - return True; - end if; - - when others => null; - - end case; - - return Has_Alias (Prefix (N)); - - when N_Indexed_Component - | N_Slice - => - return Has_Alias (Prefix (N)); - - when N_Explicit_Dereference => - return True; - - when N_Function_Call => - return False; - - when N_Attribute_Reference => - if Is_Deep (Etype (Prefix (N))) then - raise Program_Error; - end if; - return False; - - when others => - return False; - end case; - end Has_Alias; - - ------------------------- - -- Has_Array_Component -- - ------------------------- - - function Has_Array_Component (N : Node_Id) return Boolean is - begin - case Nkind (N) is - -- Base identifier. There is no array component here. - - when N_Identifier - | N_Expanded_Name - | N_Defining_Identifier - => - return False; - - -- We check if the expression inside the conversion has an array - -- component. - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Has_Array_Component (Expression (N)); - - -- We check if the prefix has an array component - - when N_Selected_Component => - return Has_Array_Component (Prefix (N)); - - -- We found the array component, return True - - when N_Indexed_Component - | N_Slice - => - return True; - - -- We check if the prefix has an array component - - when N_Explicit_Dereference => - return Has_Array_Component (Prefix (N)); - - when N_Function_Call => - return False; - - when others => - raise Program_Error; - end case; - end Has_Array_Component; - - ---------------------------- - -- Has_Function_Component -- - ---------------------------- - - function Has_Function_Component (N : Node_Id) return Boolean is - begin - case Nkind (N) is - -- Base identifier. There is no function component here. - - when N_Identifier - | N_Expanded_Name - | N_Defining_Identifier - => - return False; - - -- We check if the expression inside the conversion has a function - -- component. - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Has_Function_Component (Expression (N)); - - -- We check if the prefix has a function component - - when N_Selected_Component => - return Has_Function_Component (Prefix (N)); - - -- We check if the prefix has a function component - - when N_Indexed_Component - | N_Slice - => - return Has_Function_Component (Prefix (N)); - - -- We check if the prefix has a function component - - when N_Explicit_Dereference => - return Has_Function_Component (Prefix (N)); - - -- We found the function component, return True - - when N_Function_Call => - return True; - - when others => - raise Program_Error; - - end case; - end Has_Function_Component; - - -------- - -- Hp -- - -------- - - procedure Hp (P : Perm_Env) is - Elem : Perm_Tree_Maps.Key_Option; - - begin - Elem := Get_First_Key (P); - while Elem.Present loop - Print_Node_Briefly (Elem.K); - Elem := Get_Next_Key (P); - end loop; - end Hp; - - -------------------------- - -- Illegal_Global_Usage -- - -------------------------- - - procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is - begin - Error_Msg_NE ("cannot use global variable & of deep type", N, N); - Error_Msg_N ("\without prior declaration in a Global aspect", N); - - Errout.Finalize (Last_Call => True); - Errout.Output_Messages; - Exit_Program (E_Errors); - end Illegal_Global_Usage; - - -------------------- - -- Is_Borrowed_In -- - -------------------- - - function Is_Borrowed_In (E : Entity_Id) return Boolean is - begin - return Is_Access_Type (Etype (E)) - and then not Is_Access_Constant (Etype (E)); - end Is_Borrowed_In; - - ------------- - -- Is_Deep -- - ------------- - - function Is_Deep (E : Entity_Id) return Boolean is - function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean; - - function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is - Decl : Node_Id; - Pack_Decl : Node_Id; - - begin - if Is_Itype (E) then - Decl := Associated_Node_For_Itype (E); - else - Decl := Parent (E); - end if; - - Pack_Decl := Parent (Parent (Decl)); - - if Nkind (Pack_Decl) /= N_Package_Declaration then - return False; - end if; - - return - Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) - and then Get_SPARK_Mode_From_Annotation - (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off; - end Is_Private_Entity_Mode_Off; begin pragma Assert (Is_Type (E)); - case Ekind (E) is when Scalar_Kind => return False; @@ -3793,7 +3198,7 @@ package body Sem_SPARK is when E_Record_Type | E_Record_Subtype - => + => declare Elmt : Entity_Id; @@ -3806,7 +3211,6 @@ package body Sem_SPARK is Next_Component_Or_Discriminant (Elmt); end if; end loop; - return False; end; @@ -3821,10 +3225,9 @@ package body Sem_SPARK is end if; end if; - when E_Incomplete_Type => - return True; - - when E_Incomplete_Subtype => + when E_Incomplete_Type + | E_Incomplete_Subtype + => return True; -- No problem with synchronized types @@ -3845,373 +3248,67 @@ package body Sem_SPARK is end Is_Deep; ---------------- - -- Is_Shallow -- + -- Perm_Error -- ---------------- - function Is_Shallow (E : Entity_Id) return Boolean is - begin - pragma Assert (Is_Type (E)); - return not Is_Deep (E); - end Is_Shallow; - - ------------------ - -- Loop_Of_Exit -- - ------------------ - - function Loop_Of_Exit (N : Node_Id) return Entity_Id is - Nam : Node_Id := Name (N); - Stmt : Node_Id := N; - begin - if No (Nam) then - while Present (Stmt) loop - Stmt := Parent (Stmt); - if Nkind (Stmt) = N_Loop_Statement then - Nam := Identifier (Stmt); - exit; - end if; - end loop; - end if; - return Entity (Nam); - end Loop_Of_Exit; - --------- - -- Lub -- - --------- - - function Lub (P1, P2 : Perm_Kind) return Perm_Kind + procedure Perm_Error + (N : Node_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind) is - begin - case P1 is - when No_Access => - return P2; - - when Read_Only => - case P2 is - when No_Access - | Read_Only - => - return Read_Only; - - when Write_Perm => - return Read_Write; - end case; - - when Write_Only => - case P2 is - when No_Access - | Write_Only - => - return Write_Only; + procedure Set_Root_Object + (Path : Node_Id; + Obj : out Entity_Id; + Deref : out Boolean); + -- Set the root object Obj, and whether the path contains a dereference, + -- from a path Path. - when Read_Perm => - return Read_Write; - end case; + --------------------- + -- Set_Root_Object -- + --------------------- - when Read_Write => - return Read_Write; - end case; - end Lub; + procedure Set_Root_Object + (Path : Node_Id; + Obj : out Entity_Id; + Deref : out Boolean) + is + begin + case Nkind (Path) is + when N_Identifier + | N_Expanded_Name + => + Obj := Entity (Path); + Deref := False; - ---------------- - -- Merge_Envs -- - ---------------- + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + Set_Root_Object (Expression (Path), Obj, Deref); - procedure Merge_Envs - (Target : in out Perm_Env; - Source : in out Perm_Env) - is - procedure Merge_Trees - (Target : Perm_Tree_Access; - Source : Perm_Tree_Access); + when N_Indexed_Component + | N_Selected_Component + | N_Slice + => + Set_Root_Object (Prefix (Path), Obj, Deref); - procedure Merge_Trees - (Target : Perm_Tree_Access; - Source : Perm_Tree_Access) - is - procedure Apply_Glb_Tree - (A : Perm_Tree_Access; - P : Perm_Kind); - - procedure Apply_Glb_Tree - (A : Perm_Tree_Access; - P : Perm_Kind) - is - begin - A.all.Tree.Permission := Glb (Permission (A), P); + when N_Explicit_Dereference => + Set_Root_Object (Prefix (Path), Obj, Deref); + Deref := True; - case Kind (A) is - when Entire_Object => - A.all.Tree.Children_Permission := - Glb (Children_Permission (A), P); + when others => + raise Program_Error; + end case; + end Set_Root_Object; + -- Local variables - when Reference => - Apply_Glb_Tree (Get_All (A), P); + Root : Entity_Id; + Is_Deref : Boolean; - when Array_Component => - Apply_Glb_Tree (Get_Elem (A), P); + -- Start of processing for Perm_Error - when Record_Component => - declare - Comp : Perm_Tree_Access; - begin - Comp := Perm_Tree_Maps.Get_First (Component (A)); - while Comp /= null loop - Apply_Glb_Tree (Comp, P); - Comp := Perm_Tree_Maps.Get_Next (Component (A)); - end loop; - - Apply_Glb_Tree (Other_Components (A), P); - end; - end case; - end Apply_Glb_Tree; - - Perm : constant Perm_Kind := - Glb (Permission (Target), Permission (Source)); - - begin - pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source)); - Target.all.Tree.Permission := Perm; - - case Kind (Target) is - when Entire_Object => - declare - Child_Perm : constant Perm_Kind := - Children_Permission (Target); - - begin - case Kind (Source) is - when Entire_Object => - Target.all.Tree.Children_Permission := - Glb (Child_Perm, Children_Permission (Source)); - - when Reference => - Copy_Tree (Source, Target); - Target.all.Tree.Permission := Perm; - Apply_Glb_Tree (Get_All (Target), Child_Perm); - - when Array_Component => - Copy_Tree (Source, Target); - Target.all.Tree.Permission := Perm; - Apply_Glb_Tree (Get_Elem (Target), Child_Perm); - - when Record_Component => - Copy_Tree (Source, Target); - Target.all.Tree.Permission := Perm; - declare - Comp : Perm_Tree_Access; - - begin - Comp := - Perm_Tree_Maps.Get_First (Component (Target)); - while Comp /= null loop - -- Apply glb tree on every component subtree - - Apply_Glb_Tree (Comp, Child_Perm); - Comp := Perm_Tree_Maps.Get_Next - (Component (Target)); - end loop; - end; - Apply_Glb_Tree (Other_Components (Target), Child_Perm); - - end case; - end; - when Reference => - case Kind (Source) is - when Entire_Object => - Apply_Glb_Tree (Get_All (Target), - Children_Permission (Source)); - - when Reference => - Merge_Trees (Get_All (Target), Get_All (Source)); - - when others => - raise Program_Error; - - end case; - - when Array_Component => - case Kind (Source) is - when Entire_Object => - Apply_Glb_Tree (Get_Elem (Target), - Children_Permission (Source)); - - when Array_Component => - Merge_Trees (Get_Elem (Target), Get_Elem (Source)); - - when others => - raise Program_Error; - - end case; - - when Record_Component => - case Kind (Source) is - when Entire_Object => - declare - Child_Perm : constant Perm_Kind := - Children_Permission (Source); - - Comp : Perm_Tree_Access; - - begin - Comp := Perm_Tree_Maps.Get_First - (Component (Target)); - while Comp /= null loop - -- Apply glb tree on every component subtree - - Apply_Glb_Tree (Comp, Child_Perm); - Comp := - Perm_Tree_Maps.Get_Next (Component (Target)); - end loop; - Apply_Glb_Tree (Other_Components (Target), Child_Perm); - end; - - when Record_Component => - declare - Key_Source : Perm_Tree_Maps.Key_Option; - CompTarget : Perm_Tree_Access; - CompSource : Perm_Tree_Access; - - begin - Key_Source := Perm_Tree_Maps.Get_First_Key - (Component (Source)); - - while Key_Source.Present loop - CompSource := Perm_Tree_Maps.Get - (Component (Source), Key_Source.K); - CompTarget := Perm_Tree_Maps.Get - (Component (Target), Key_Source.K); - - pragma Assert (CompSource /= null); - Merge_Trees (CompTarget, CompSource); - - Key_Source := Perm_Tree_Maps.Get_Next_Key - (Component (Source)); - end loop; - - Merge_Trees (Other_Components (Target), - Other_Components (Source)); - end; - - when others => - raise Program_Error; - - end case; - end case; - end Merge_Trees; - - CompTarget : Perm_Tree_Access; - CompSource : Perm_Tree_Access; - KeyTarget : Perm_Tree_Maps.Key_Option; - - begin - KeyTarget := Get_First_Key (Target); - -- Iterate over every tree of the environment in the target, and merge - -- it with the source if there is such a similar one that exists. If - -- there is none, then skip. - while KeyTarget.Present loop - - CompSource := Get (Source, KeyTarget.K); - CompTarget := Get (Target, KeyTarget.K); - - pragma Assert (CompTarget /= null); - - if CompSource /= null then - Merge_Trees (CompTarget, CompSource); - Remove (Source, KeyTarget.K); - end if; - - KeyTarget := Get_Next_Key (Target); - end loop; - - -- Iterate over every tree of the environment of the source. And merge - -- again. If there is not any tree of the target then just copy the tree - -- from source to target. - declare - KeySource : Perm_Tree_Maps.Key_Option; - begin - KeySource := Get_First_Key (Source); - while KeySource.Present loop - - CompSource := Get (Source, KeySource.K); - CompTarget := Get (Target, KeySource.K); - - if CompTarget = null then - CompTarget := new Perm_Tree_Wrapper'(CompSource.all); - Copy_Tree (CompSource, CompTarget); - Set (Target, KeySource.K, CompTarget); - else - Merge_Trees (CompTarget, CompSource); - end if; - - KeySource := Get_Next_Key (Source); - end loop; - end; - - Free_Env (Source); - end Merge_Envs; - - ---------------- - -- Perm_Error -- - ---------------- - - procedure Perm_Error - (N : Node_Id; - Perm : Perm_Kind; - Found_Perm : Perm_Kind) - is - procedure Set_Root_Object - (Path : Node_Id; - Obj : out Entity_Id; - Deref : out Boolean); - -- Set the root object Obj, and whether the path contains a dereference, - -- from a path Path. - - --------------------- - -- Set_Root_Object -- - --------------------- - - procedure Set_Root_Object - (Path : Node_Id; - Obj : out Entity_Id; - Deref : out Boolean) - is - begin - case Nkind (Path) is - when N_Identifier - | N_Expanded_Name - => - Obj := Entity (Path); - Deref := False; - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - Set_Root_Object (Expression (Path), Obj, Deref); - - when N_Indexed_Component - | N_Selected_Component - | N_Slice - => - Set_Root_Object (Prefix (Path), Obj, Deref); - - when N_Explicit_Dereference => - Set_Root_Object (Prefix (Path), Obj, Deref); - Deref := True; - - when others => - raise Program_Error; - end case; - end Set_Root_Object; - - -- Local variables - - Root : Entity_Id; - Is_Deref : Boolean; - - -- Start of processing for Perm_Error - - begin - Set_Root_Object (N, Root, Is_Deref); + begin + Set_Root_Object (N, Root, Is_Deref); if Is_Deref then Error_Msg_NE @@ -4245,8 +3342,8 @@ package body Sem_SPARK is ------------------ procedure Process_Path (N : Node_Id) is - Root : constant Entity_Id := Get_Enclosing_Object (N); - + Root : constant Entity_Id := Get_Enclosing_Object (N); + State_N : Perm_Kind; begin -- We ignore if yielding to synchronized @@ -4256,200 +3353,153 @@ package body Sem_SPARK is return; end if; - -- We ignore shallow unaliased. They are checked in flow analysis, - -- allowing backward compatibility. + State_N := Get_Perm (N); - if Current_Checking_Mode /= Super_Move - and then not Has_Alias (N) - and then Is_Shallow (Etype (N)) - then - return; - end if; - - declare - Perm_N : constant Perm_Kind := Get_Perm (N); - - begin + case Current_Checking_Mode is - case Current_Checking_Mode is - -- Check permission R, do nothing + -- Check permission R, do nothing - when Read => - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - return; - end if; + when Read => - -- If shallow type no need for RW, only R + -- This condition should be removed when removing the read + -- checking mode. - when Move => - if Is_Shallow (Etype (N)) then - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - return; - end if; - else - -- Check permission RW if deep + return; - if Perm_N /= Read_Write then - Perm_Error (N, Read_Write, Perm_N); - return; - end if; + when Move => - declare - -- Set permission to W to the path and any of its prefix + -- The rhs object in an assignment statement (including copy in + -- and copy back) should be in the Unrestricted or Moved state. + -- Otherwise the move is not allowed. + -- This applies to both stand-alone and composite objects. + -- If the state of the source is Moved, then a warning message + -- is prompt to make the user aware of reading a nullified + -- object. - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (N, Move); + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + return; + end if; - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. + -- In the AI, after moving a path nothing to do since the rhs + -- object was in the Unrestricted state and it shall be + -- refreshed to Unrestricted. The object should be nullified + -- however. To avoid moving again a name that has already been + -- moved, in this implementation we set the state of the moved + -- object to "Moved". This shall be used to prompt a warning + -- when manipulating a null pointer and also to implement + -- the no aliasing parameter restriction. + + if State_N = Moved then + Error_Msg_N ("?the source or one of its extensions has" + & " already been moved", N); + end if; - return; - end if; + declare + -- Set state to Borrowed to the path and any of its prefixes - -- Set permissions to - -- No for any extension with more .all - -- W for any deep extension with same number of .all - -- RW for any shallow extension with same number of .all + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes (N, Moved); - Set_Perm_Extensions_Move (Tree, Etype (N)); - end; - end if; + begin + if Tree = null then - -- Check permission RW + -- We went through a function call, no permission to + -- modify. - when Super_Move => - if Perm_N /= Read_Write then - Perm_Error (N, Read_Write, Perm_N); return; end if; - declare - -- Set permission to No to the path and any of its prefix up - -- to the first .all and then W. - - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (N, Super_Move); - - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. - - return; - end if; + -- Set state to Borrowed on any strict extension of the path - -- Set permissions to No on any strict extension of the path + Set_Perm_Extensions (Tree, Moved); + end; - Set_Perm_Extensions (Tree, No_Access); - end; + when Assign => - -- Check permission W + -- The lhs object in an assignment statement (including copy in + -- and copy back) should be in the Unrestricted state. + -- Otherwise the move is not allowed. + -- This applies to both stand-alone and composite objects. - when Assign => - if Perm_N not in Write_Perm then - Perm_Error (N, Write_Only, Perm_N); - return; - end if; + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + return; + end if; - -- If the tree has an array component, then the permissions do - -- not get modified by the assignment. + -- After assigning to a path nothing to do since it was in the + -- Unrestricted state and it would be refreshed to + -- Unrestricted. - if Has_Array_Component (N) then - return; - end if; + when Borrow => - -- Same if has function component + -- Borrowing is only allowed on Unrestricted objects. - if Has_Function_Component (N) then -- Dead code? - return; - end if; + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + end if; - declare - -- Get the permission tree for the path + if State_N = Moved then + Error_Msg_N ("?the source or one of its extensions has" + & " already been moved", N); + end if; - Tree : constant Perm_Tree_Access := - Get_Perm_Tree (N); + declare + -- Set state to Borrowed to the path and any of its prefixes - Dummy : Perm_Tree_Access; + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes (N, Borrowed); - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. + begin + if Tree = null then - return; - end if; + -- We went through a function call, no permission to + -- modify. - -- Set permission RW for it and all of its extensions + return; + end if; - Tree.all.Tree.Permission := Read_Write; + -- Set state to Borrowed on any strict extension of the path - Set_Perm_Extensions (Tree, Read_Write); + Set_Perm_Extensions (Tree, Borrowed); + end; - -- Normalize the permission tree + when Observe => + if State_N /= Unrestricted + and then State_N /= Observed + then + Perm_Error (N, Observed, State_N); + end if; - Dummy := Set_Perm_Prefixes_Assign (N); - end; + declare + -- Set permission to Observed on the path and any of its + -- prefixes if it is of a deep type. Actually, some operation + -- like reading from an object of access type is considered as + -- observe while it should not affect the permissions of + -- the considered tree. - -- Check permission W + Tree : Perm_Tree_Access; - when Borrow_Out => - if Perm_N not in Write_Perm then - Perm_Error (N, Write_Only, Perm_N); + begin + if Is_Deep (Etype (N)) then + Tree := Set_Perm_Prefixes (N, Observed); + else + Tree := null; end if; - declare - -- Set permission to No to the path and any of its prefixes - - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (N); - - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. - - return; - end if; - - -- Set permissions to No on any strict extension of the path - - Set_Perm_Extensions (Tree, No_Access); - end; + if Tree = null then - when Observe => - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - end if; + -- We went through a function call, no permission to + -- modify. - if Is_By_Copy_Type (Etype (N)) then return; end if; - declare - -- Set permission to No on the path and any of its prefixes - - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (N); - - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. - - return; - end if; - - -- Set permissions to No on any strict extension of the path + -- Set permissions to No on any strict extension of the path - Set_Perm_Extensions (Tree, Read_Only); - end; - end case; - end; + Set_Perm_Extensions (Tree, Observed); + end; + end case; end Process_Path; ------------------------- @@ -4457,7 +3507,6 @@ package body Sem_SPARK is ------------------------- procedure Return_Declarations (L : List_Id) is - procedure Return_Declaration (Decl : Node_Id); -- Check correct permissions for every declared object @@ -4468,6 +3517,7 @@ package body Sem_SPARK is procedure Return_Declaration (Decl : Node_Id) is begin if Nkind (Decl) = N_Object_Declaration then + -- Check RW for object declared, unless the object has never been -- initialized. @@ -4477,15 +3527,6 @@ package body Sem_SPARK is return; end if; - -- We ignore shallow unaliased. They are checked in flow analysis, - -- allowing backward compatibility. - - if not Has_Alias (Defining_Identifier (Decl)) - and then Is_Shallow (Etype (Defining_Identifier (Decl))) - then - return; - end if; - declare Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, @@ -4493,22 +3534,23 @@ package body Sem_SPARK is begin if Elem = null then + -- Here we are on a declaration. Hence it should have been -- added in the environment when analyzing this node with -- mode Read. Hence it is not possible to find a null -- pointer here. -- Hash_Table_Error + raise Program_Error; end if; - if Permission (Elem) /= Read_Write then - Perm_Error (Decl, Read_Write, Permission (Elem)); + if Permission (Elem) /= Unrestricted then + Perm_Error (Decl, Unrestricted, Permission (Elem)); end if; end; end if; end Return_Declaration; - -- Local Variables N : Node_Id; @@ -4517,831 +3559,227 @@ package body Sem_SPARK is begin N := First (L); - while Present (N) loop - Return_Declaration (N); - Next (N); - end loop; - end Return_Declarations; - - -------------------- - -- Return_Globals -- - -------------------- - - procedure Return_Globals (Subp : Entity_Id) is - - procedure Return_Globals_From_List - (First_Item : Node_Id; - Kind : Formal_Kind); - -- Return global items from the list starting at Item - - procedure Return_Globals_Of_Mode (Global_Mode : Name_Id); - -- Return global items for the mode Global_Mode - - ------------------------------ - -- Return_Globals_From_List -- - ------------------------------ - - procedure Return_Globals_From_List - (First_Item : Node_Id; - Kind : Formal_Kind) - is - Item : Node_Id := First_Item; - E : Entity_Id; - - begin - while Present (Item) loop - E := Entity (Item); - - -- Ignore abstract states, which play no role in pointer aliasing - - if Ekind (E) = E_Abstract_State then - null; - else - Return_Parameter_Or_Global (E, Kind, Subp, Global_Var => True); - end if; - Next_Global (Item); - end loop; - end Return_Globals_From_List; - - ---------------------------- - -- Return_Globals_Of_Mode -- - ---------------------------- - - procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is - Kind : Formal_Kind; - - begin - case Global_Mode is - when Name_Input | Name_Proof_In => - Kind := E_In_Parameter; - when Name_Output => - Kind := E_Out_Parameter; - when Name_In_Out => - Kind := E_In_Out_Parameter; - when others => - raise Program_Error; - end case; - - -- Return both global items from Global and Refined_Global pragmas - - Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind); - Return_Globals_From_List - (First_Global (Subp, Global_Mode, Refined => True), Kind); - end Return_Globals_Of_Mode; - - -- Start of processing for Return_Globals - - begin - Return_Globals_Of_Mode (Name_Proof_In); - Return_Globals_Of_Mode (Name_Input); - Return_Globals_Of_Mode (Name_Output); - Return_Globals_Of_Mode (Name_In_Out); - end Return_Globals; - - -------------------------------- - -- Return_Parameter_Or_Global -- - -------------------------------- - - procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean) - is - Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); - pragma Assert (Elem /= null); - - begin - -- Shallow unaliased parameters and globals cannot introduce pointer - -- aliasing. - - if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then - null; - - -- Observed IN parameters and globals need not return a permission to - -- the caller. - - elsif Mode = E_In_Parameter - and then (not Is_Borrowed_In (Id) or else Global_Var) - then - null; - - -- All other parameters and globals should return with mode RW to the - -- caller. - - else - if Permission (Elem) /= Read_Write then - Perm_Error_Subprogram_End - (E => Id, - Subp => Subp, - Perm => Read_Write, - Found_Perm => Permission (Elem)); - end if; - end if; - end Return_Parameter_Or_Global; - - ----------------------- - -- Return_Parameters -- - ----------------------- - - procedure Return_Parameters (Subp : Entity_Id) is - Formal : Entity_Id; - - begin - Formal := First_Formal (Subp); - while Present (Formal) loop - Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp, False); - Next_Formal (Formal); - end loop; - end Return_Parameters; - - ------------------------- - -- Set_Perm_Extensions -- - ------------------------- - - procedure Set_Perm_Extensions - (T : Perm_Tree_Access; - P : Perm_Kind) - is - procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); - - procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) - is - begin - case Kind (T) is - when Entire_Object => - null; - - when Reference => - Free_Perm_Tree (T.all.Tree.Get_All); - - when Array_Component => - Free_Perm_Tree (T.all.Tree.Get_Elem); - - -- Free every Component subtree - - when Record_Component => - declare - Comp : Perm_Tree_Access; - - begin - Comp := Perm_Tree_Maps.Get_First (Component (T)); - while Comp /= null loop - Free_Perm_Tree (Comp); - Comp := Perm_Tree_Maps.Get_Next (Component (T)); - end loop; - - Free_Perm_Tree (T.all.Tree.Other_Components); - end; - end case; - end Free_Perm_Tree_Children; - - Son : constant Perm_Tree := - Perm_Tree' - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (T), - Permission => Permission (T), - Children_Permission => P); - - begin - Free_Perm_Tree_Children (T); - T.all.Tree := Son; - end Set_Perm_Extensions; - - ------------------------------ - -- Set_Perm_Extensions_Move -- - ------------------------------ - - procedure Set_Perm_Extensions_Move - (T : Perm_Tree_Access; - E : Entity_Id) - is - begin - if not Is_Node_Deep (T) then - -- We are a shallow extension with same number of .all - - Set_Perm_Extensions (T, Read_Write); - return; - end if; - - -- We are a deep extension here (or the moved deep path) - - T.all.Tree.Permission := Write_Only; - - case T.all.Tree.Kind is - -- Unroll the tree depending on the type - - when Entire_Object => - case Ekind (E) is - when Scalar_Kind - | E_String_Literal_Subtype - => - Set_Perm_Extensions (T, No_Access); - - -- No need to unroll here, directly put sons to No_Access - - when Access_Kind => - if Ekind (E) in Access_Subprogram_Kind then - null; - else - Set_Perm_Extensions (T, No_Access); - end if; - - -- No unrolling done, too complicated - - when E_Class_Wide_Subtype - | E_Class_Wide_Type - | E_Incomplete_Type - | E_Incomplete_Subtype - | E_Exception_Type - | E_Task_Type - | E_Task_Subtype - => - Set_Perm_Extensions (T, No_Access); - - -- Expand the tree. Replace the node with Array component. - - when E_Array_Type - | E_Array_Subtype => - declare - Son : Perm_Tree_Access; - - begin - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (T), - Permission => Read_Write, - Children_Permission => Read_Write)); - - Set_Perm_Extensions_Move (Son, Component_Type (E)); - - -- We change the current node from Entire_Object to - -- Reference with Write_Only and the previous son. - - pragma Assert (Is_Node_Deep (T)); - - T.all.Tree := (Kind => Array_Component, - Is_Node_Deep => Is_Node_Deep (T), - Permission => Write_Only, - Get_Elem => Son); - end; - - -- Unroll, and set permission extensions with component type - - when E_Record_Type - | E_Record_Subtype - | E_Record_Type_With_Private - | E_Record_Subtype_With_Private - | E_Protected_Type - | E_Protected_Subtype - => - declare - -- Expand the tree. Replace the node with - -- Record_Component. - - Elem : Node_Id; - - Son : Perm_Tree_Access; - - begin - -- We change the current node from Entire_Object to - -- Record_Component with same permission and an empty - -- hash table as component list. - - pragma Assert (Is_Node_Deep (T)); - - T.all.Tree := - (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (T), - Permission => Write_Only, - Component => Perm_Tree_Maps.Nil, - Other_Components => - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => True, - Permission => Read_Write, - Children_Permission => Read_Write) - ) - ); - - -- We fill the hash table with all sons of the record, - -- with basic Entire_Objects nodes. - Elem := First_Component_Or_Discriminant (E); - while Present (Elem) loop - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (Elem)), - Permission => Read_Write, - Children_Permission => Read_Write)); - - Set_Perm_Extensions_Move (Son, Etype (Elem)); - - Perm_Tree_Maps.Set - (T.all.Tree.Component, Elem, Son); - - Next_Component_Or_Discriminant (Elem); - end loop; - end; - - when E_Private_Type - | E_Private_Subtype - | E_Limited_Private_Type - | E_Limited_Private_Subtype - => - Set_Perm_Extensions_Move (T, Underlying_Type (E)); - - when others => - raise Program_Error; - end case; - - when Reference => - -- Now the son does not have the same number of .all - Set_Perm_Extensions (T, No_Access); - - when Array_Component => - Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E)); - - when Record_Component => - declare - Comp : Perm_Tree_Access; - It : Node_Id; - - begin - It := First_Component_Or_Discriminant (E); - while It /= Empty loop - Comp := Perm_Tree_Maps.Get (Component (T), It); - pragma Assert (Comp /= null); - Set_Perm_Extensions_Move (Comp, It); - It := Next_Component_Or_Discriminant (E); - end loop; - - Set_Perm_Extensions (Other_Components (T), No_Access); - end; - end case; - end Set_Perm_Extensions_Move; - - ------------------------------ - -- Set_Perm_Prefixes_Assign -- - ------------------------------ - - function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access is - C : constant Perm_Tree_Access := Get_Perm_Tree (N); - - begin - pragma Assert (Current_Checking_Mode = Assign); - - -- The function should not be called if has_function_component - - pragma Assert (C /= null); - - case Kind (C) is - when Entire_Object => - pragma Assert (Children_Permission (C) = Read_Write); - - -- Maroua: Children could have read_only perm. Why Read_Write? - - C.all.Tree.Permission := Read_Write; - - when Reference => - pragma Assert (Get_All (C) /= null); - - C.all.Tree.Permission := - Lub (Permission (C), Permission (Get_All (C))); - - when Array_Component => - pragma Assert (C.all.Tree.Get_Elem /= null); - - -- Given that it is not possible to know which element has been - -- assigned, then the permissions do not get changed in case of - -- Array_Component. - - null; - - when Record_Component => - declare - Comp : Perm_Tree_Access; - Perm : Perm_Kind := Read_Write; - - begin - -- We take the Glb of all the descendants, and then update the - -- permission of the node with it. - - Comp := Perm_Tree_Maps.Get_First (Component (C)); - while Comp /= null loop - Perm := Glb (Perm, Permission (Comp)); - Comp := Perm_Tree_Maps.Get_Next (Component (C)); - end loop; - - Perm := Glb (Perm, Permission (Other_Components (C))); - - C.all.Tree.Permission := Lub (Permission (C), Perm); - end; - end case; - - case Nkind (N) is - - -- Base identifier. End recursion here. - - when N_Identifier - | N_Expanded_Name - | N_Defining_Identifier - => - return null; - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Set_Perm_Prefixes_Assign (Expression (N)); - - when N_Parameter_Specification => - raise Program_Error; - - -- Continue recursion on prefix - - when N_Selected_Component => - return Set_Perm_Prefixes_Assign (Prefix (N)); - - -- Continue recursion on prefix - - when N_Indexed_Component - | N_Slice - => - return Set_Perm_Prefixes_Assign (Prefix (N)); - - -- Continue recursion on prefix - - when N_Explicit_Dereference => - return Set_Perm_Prefixes_Assign (Prefix (N)); - - when N_Function_Call => - raise Program_Error; - - when others => - raise Program_Error; - - end case; - end Set_Perm_Prefixes_Assign; - - ---------------------------------- - -- Set_Perm_Prefixes_Borrow_Out -- - ---------------------------------- - - function Set_Perm_Prefixes_Borrow_Out - (N : Node_Id) - return Perm_Tree_Access - is - begin - pragma Assert (Current_Checking_Mode = Borrow_Out); - - case Nkind (N) is - -- Base identifier. Set permission to No. - - when N_Identifier - | N_Expanded_Name - => - declare - P : constant Node_Id := Entity (N); - - C : constant Perm_Tree_Access := - Get (Current_Perm_Env, Unique_Entity (P)); - - pragma Assert (C /= null); - - begin - -- Setting the initialization map to True, so that this - -- variable cannot be ignored anymore when looking at end - -- of elaboration of package. - - Set (Current_Initialization_Map, Unique_Entity (P), True); - - C.all.Tree.Permission := No_Access; - return C; - end; - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Set_Perm_Prefixes_Borrow_Out (Expression (N)); - - when N_Parameter_Specification - | N_Defining_Identifier - => - raise Program_Error; - - -- We set the permission tree of its prefix, and then we extract - -- our subtree from the returned pointer and assign an adequate - -- permission to it, if unfolded. If folded, we unroll the tree - -- in one step. - - when N_Selected_Component => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (Prefix (N)); - - begin - if C = null then - -- We went through a function call, do nothing - - return null; - end if; - - -- The permission of the returned node should be No - - pragma Assert (Permission (C) = No_Access); - - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Record_Component); - - if Kind (C) = Record_Component then - -- The tree is unfolded. We just modify the permission and - -- return the record subtree. - - declare - Selected_Component : constant Entity_Id := - Entity (Selector_Name (N)); - - Selected_C : Perm_Tree_Access := - Perm_Tree_Maps.Get - (Component (C), Selected_Component); - - begin - if Selected_C = null then - Selected_C := Other_Components (C); - end if; - - pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := No_Access; - - return Selected_C; - end; - elsif Kind (C) = Entire_Object then - declare - -- Expand the tree. Replace the node with - -- Record_Component. - - Elem : Node_Id; - - -- Create an empty hash table - - Hashtbl : Perm_Tree_Maps.Instance; - - -- We create the unrolled nodes, that will all have same - -- permission than parent. - - Son : Perm_Tree_Access; - - ChildrenPerm : constant Perm_Kind := - Children_Permission (C); - - begin - -- We change the current node from Entire_Object to - -- Record_Component with same permission and an empty - -- hash table as component list. - - C.all.Tree := - (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (C), - Permission => Permission (C), - Component => Hashtbl, - Other_Components => - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => True, - Permission => ChildrenPerm, - Children_Permission => ChildrenPerm) - )); - - -- We fill the hash table with all sons of the record, - -- with basic Entire_Objects nodes. - Elem := First_Component_Or_Discriminant - (Etype (Prefix (N))); - - while Present (Elem) loop - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (Elem)), - Permission => ChildrenPerm, - Children_Permission => ChildrenPerm)); - - Perm_Tree_Maps.Set - (C.all.Tree.Component, Elem, Son); - - Next_Component_Or_Discriminant (Elem); - end loop; - - -- Now we set the right field to No_Access, and then we - -- return the tree to the sons, so that the recursion can - -- continue. - - declare - Selected_Component : constant Entity_Id := - Entity (Selector_Name (N)); - - Selected_C : Perm_Tree_Access := - Perm_Tree_Maps.Get - (Component (C), Selected_Component); - - begin - if Selected_C = null then - Selected_C := Other_Components (C); - end if; - - pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := No_Access; - - return Selected_C; - end; - end; - else - raise Program_Error; - end if; - end; - - -- We set the permission tree of its prefix, and then we extract - -- from the returned pointer the subtree and assign an adequate - -- permission to it, if unfolded. If folded, we unroll the tree in - -- one step. + while Present (N) loop + Return_Declaration (N); + Next (N); + end loop; + end Return_Declarations; - when N_Indexed_Component - | N_Slice - => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + -------------------- + -- Return_Globals -- + -------------------- - begin - if C = null then - -- We went through a function call, do nothing + procedure Return_Globals (Subp : Entity_Id) is + procedure Return_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind); + -- Return global items from the list starting at Item - return null; - end if; + procedure Return_Globals_Of_Mode (Global_Mode : Name_Id); + -- Return global items for the mode Global_Mode - -- The permission of the returned node should be either W - -- (because the recursive call sets <= Write_Only) or No - -- (if another path has been moved with 'Access). + ------------------------------ + -- Return_Globals_From_List -- + ------------------------------ - pragma Assert (Permission (C) = No_Access); + procedure Return_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind) + is + Item : Node_Id := First_Item; + E : Entity_Id; - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Array_Component); + begin + while Present (Item) loop + E := Entity (Item); - if Kind (C) = Array_Component then - -- The tree is unfolded. We just modify the permission and - -- return the elem subtree. + -- Ignore abstract states, which play no role in pointer aliasing - pragma Assert (Get_Elem (C) /= null); + if Ekind (E) = E_Abstract_State then + null; + else + Return_The_Global (E, Kind, Subp); + end if; + Next_Global (Item); + end loop; + end Return_Globals_From_List; - C.all.Tree.Get_Elem.all.Tree.Permission := No_Access; + ---------------------------- + -- Return_Globals_Of_Mode -- + ---------------------------- - return Get_Elem (C); - elsif Kind (C) = Entire_Object then - declare - -- Expand the tree. Replace node with Array_Component. + procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is + Kind : Formal_Kind; - Son : Perm_Tree_Access; + begin + case Global_Mode is + when Name_Input + | Name_Proof_In + => + Kind := E_In_Parameter; + when Name_Output => + Kind := E_Out_Parameter; + when Name_In_Out => + Kind := E_In_Out_Parameter; + when others => + raise Program_Error; + end case; - begin - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (C), - Permission => No_Access, - Children_Permission => Children_Permission (C))); + -- Return both global items from Global and Refined_Global pragmas - -- We change the current node from Entire_Object - -- to Array_Component with same permission and the - -- previously defined son. + Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind); + Return_Globals_From_List + (First_Global (Subp, Global_Mode, Refined => True), Kind); + end Return_Globals_Of_Mode; - C.all.Tree := (Kind => Array_Component, - Is_Node_Deep => Is_Node_Deep (C), - Permission => No_Access, - Get_Elem => Son); + -- Start of processing for Return_Globals - return Get_Elem (C); - end; - else - raise Program_Error; - end if; - end; + begin + Return_Globals_Of_Mode (Name_Proof_In); + Return_Globals_Of_Mode (Name_Input); + Return_Globals_Of_Mode (Name_Output); + Return_Globals_Of_Mode (Name_In_Out); + end Return_Globals; - -- We set the permission tree of its prefix, and then we extract - -- from the returned pointer the subtree and assign an adequate - -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. + -------------------------------- + -- Return_Parameter_Or_Global -- + -------------------------------- - when N_Explicit_Dereference => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + procedure Return_The_Global + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id) + is + Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); + pragma Assert (Elem /= null); - begin - if C = null then - -- We went through a function call. Do nothing. + begin + -- Observed IN parameters and globals need not return a permission to + -- the caller. - return null; - end if; + if Mode = E_In_Parameter - -- The permission of the returned node should be No + -- Check this for read-only globals. - pragma Assert (Permission (C) = No_Access); - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Reference); + then + if Permission (Elem) /= Unrestricted + and then Permission (Elem) /= Observed + then + Perm_Error_Subprogram_End + (E => Id, + Subp => Subp, + Perm => Observed, + Found_Perm => Permission (Elem)); + end if; - if Kind (C) = Reference then - -- The tree is unfolded. We just modify the permission and - -- return the elem subtree. + -- All globals of mode out or in/out should return with mode + -- Unrestricted. - pragma Assert (Get_All (C) /= null); + else + if Permission (Elem) /= Unrestricted then + Perm_Error_Subprogram_End + (E => Id, + Subp => Subp, + Perm => Unrestricted, + Found_Perm => Permission (Elem)); + end if; + end if; + end Return_The_Global; - C.all.Tree.Get_All.all.Tree.Permission := No_Access; + ------------------------- + -- Set_Perm_Extensions -- + ------------------------- - return Get_All (C); - elsif Kind (C) = Entire_Object then - declare - -- Expand the tree. Replace the node with Reference. + procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is + procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); + procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is + begin + case Kind (T) is + when Entire_Object => + null; - Son : Perm_Tree_Access; + when Reference => + Free_Perm_Tree (T.all.Tree.Get_All); - begin - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (N)), - Permission => No_Access, - Children_Permission => Children_Permission (C))); + when Array_Component => + Free_Perm_Tree (T.all.Tree.Get_Elem); - -- We change the current node from Entire_Object to - -- Reference with No_Access and the previous son. + -- Free every Component subtree - pragma Assert (Is_Node_Deep (C)); + when Record_Component => + declare + Comp : Perm_Tree_Access; - C.all.Tree := (Kind => Reference, - Is_Node_Deep => Is_Node_Deep (C), - Permission => No_Access, - Get_All => Son); + begin + Comp := Perm_Tree_Maps.Get_First (Component (T)); + while Comp /= null loop + Free_Perm_Tree (Comp); + Comp := Perm_Tree_Maps.Get_Next (Component (T)); + end loop; - return Get_All (C); - end; - else - raise Program_Error; - end if; - end; + Free_Perm_Tree (T.all.Tree.Other_Components); + end; + end case; + end Free_Perm_Tree_Children; - when N_Function_Call => - return null; + Son : constant Perm_Tree := + Perm_Tree' + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (T), + Permission => Permission (T), + Children_Permission => P); - when others => - raise Program_Error; - end case; - end Set_Perm_Prefixes_Borrow_Out; + begin + Free_Perm_Tree_Children (T); + T.all.Tree := Son; + end Set_Perm_Extensions; - ---------------------------- - -- Set_Perm_Prefixes_Move -- - ---------------------------- + ------------------------------ + -- Set_Perm_Prefixes -- + ------------------------------ - function Set_Perm_Prefixes_Move - (N : Node_Id; Mode : Checking_Mode) - return Perm_Tree_Access + function Set_Perm_Prefixes + (N : Node_Id; + New_Perm : Perm_Kind) + return Perm_Tree_Access is begin - case Nkind (N) is - -- Base identifier. Set permission to W or No depending on Mode. + case Nkind (N) is when N_Identifier | N_Expanded_Name + | N_Defining_Identifier => + if Nkind (N) = N_Defining_Identifier + and then New_Perm = Borrowed + then + raise Program_Error; + end if; + declare - P : constant Node_Id := Entity (N); - C : constant Perm_Tree_Access := - Get (Current_Perm_Env, Unique_Entity (P)); + P : Node_Id; + C : Perm_Tree_Access; begin - -- The base tree can be RW (first move from this base path) or - -- W (already some extensions values moved), or even No_Access - -- (extensions moved with 'Access). But it cannot be Read_Only - -- (we get an error). - - if Permission (C) = Read_Only then - raise Unrecoverable_Error; + if Nkind (N) = N_Defining_Identifier then + P := N; + else + P := Entity (N); end if; + C := Get (Current_Perm_Env, Unique_Entity (P)); + pragma Assert (C /= null); + -- Setting the initialization map to True, so that this -- variable cannot be ignored anymore when looking at end -- of elaboration of package. Set (Current_Initialization_Map, Unique_Entity (P), True); + if New_Perm = Observed + and then C = null + then - if C = null then -- No null possible here, there are no parents for the path. -- This means we are using a global variable without adding -- it in environment with a global aspect. @@ -5349,12 +3787,7 @@ package body Sem_SPARK is Illegal_Global_Usage (N); end if; - if Mode = Super_Move then - C.all.Tree.Permission := No_Access; - else - C.all.Tree.Permission := Glb (Write_Only, Permission (C)); - end if; - + C.all.Tree.Permission := New_Perm; return C; end; @@ -5362,45 +3795,29 @@ package body Sem_SPARK is | N_Unchecked_Type_Conversion | N_Qualified_Expression => - return Set_Perm_Prefixes_Move (Expression (N), Mode); + return Set_Perm_Prefixes (Expression (N), New_Perm); - when N_Parameter_Specification - | N_Defining_Identifier - => + when N_Parameter_Specification => raise Program_Error; -- We set the permission tree of its prefix, and then we extract - -- from the returned pointer our subtree and assign an adequate + -- our subtree from the returned pointer and assign an adequate -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. + -- in one step. when N_Selected_Component => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (Prefix (N), Mode); + Set_Perm_Prefixes (Prefix (N), New_Perm); begin if C = null then + -- We went through a function call, do nothing return null; end if; - -- The permission of the returned node should be either W - -- (because the recursive call sets <= Write_Only) or No - -- (if another path has been moved with 'Access). - - pragma Assert (Permission (C) = No_Access - or else Permission (C) = Write_Only); - - if Mode = Super_Move then - -- The permission of the returned node should be No (thanks - -- to the recursion). - - pragma Assert (Permission (C) = No_Access); - null; - end if; - pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Record_Component); @@ -5418,31 +3835,14 @@ package body Sem_SPARK is begin if Selected_C = null then - -- If the hash table returns no element, then we fall - -- into the part of Other_Components. - pragma Assert (Is_Tagged_Type (Etype (Prefix (N)))); - - Selected_C := Other_Components (C); - end if; - - pragma Assert (Selected_C /= null); - - -- The Selected_C can have permissions: - -- RW : first move in this path - -- W : Already other moves in this path - -- No : Already other moves with 'Access - - pragma Assert (Permission (Selected_C) /= Read_Only); - if Mode = Super_Move then - Selected_C.all.Tree.Permission := No_Access; - else - Selected_C.all.Tree.Permission := - Glb (Write_Only, Permission (Selected_C)); - + Selected_C := Other_Components (C); end if; + pragma Assert (Selected_C /= null); + Selected_C.all.Tree.Permission := New_Perm; return Selected_C; end; + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with @@ -5454,17 +3854,12 @@ package body Sem_SPARK is Hashtbl : Perm_Tree_Maps.Instance; - -- We are in Move or Super_Move mode, hence we can assume - -- that the Children_permission is RW, given that there - -- are no other paths that could have been moved. - - pragma Assert (Children_Permission (C) = Read_Write); - - -- We create the unrolled nodes, that will all have RW - -- permission given that we are in move mode. We will - -- then set the right node to W. + -- We create the unrolled nodes, that will all have same + -- permission than parent. - Son : Perm_Tree_Access; + Son : Perm_Tree_Access; + Children_Perm : constant Perm_Kind := + Children_Permission (C); begin -- We change the current node from Entire_Object to @@ -5472,21 +3867,22 @@ package body Sem_SPARK is -- hash table as component list. C.all.Tree := - (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (C), - Permission => Permission (C), - Component => Hashtbl, + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Hashtbl, Other_Components => new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, Is_Node_Deep => True, - Permission => Read_Write, - Children_Permission => Read_Write) + Permission => Children_Perm, + Children_Permission => Children_Perm) )); -- We fill the hash table with all sons of the record, -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (Etype (Prefix (N))); @@ -5495,23 +3891,19 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Elem)), - Permission => Read_Write, - Children_Permission => Read_Write)); - - Perm_Tree_Maps.Set - (C.all.Tree.Component, Elem, Son); + Permission => Children_Perm, + Children_Permission => Children_Perm)); + Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son); Next_Component_Or_Discriminant (Elem); end loop; - - -- Now we set the right field to Write_Only or No_Access - -- depending on mode, and then we return the tree to the - -- sons, so that the recursion can continue. + -- Now we set the right field to Borrowed, and then we + -- return the tree to the sons, so that the recursion can + -- continue. declare Selected_Component : constant Entity_Id := Entity (Selector_Name (N)); - Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get (Component (C), Selected_Component); @@ -5522,19 +3914,7 @@ package body Sem_SPARK is end if; pragma Assert (Selected_C /= null); - - -- Given that this is a newly created Select_C, we can - -- safely assume that its permission is Read_Write. - - pragma Assert (Permission (Selected_C) = - Read_Write); - - if Mode = Super_Move then - Selected_C.all.Tree.Permission := No_Access; - else - Selected_C.all.Tree.Permission := Write_Only; - end if; - + Selected_C.all.Tree.Permission := New_Perm; return Selected_C; end; end; @@ -5545,72 +3925,40 @@ package body Sem_SPARK is -- We set the permission tree of its prefix, and then we extract -- from the returned pointer the subtree and assign an adequate - -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. + -- permission to it, if unfolded. If folded, we unroll the tree in + -- one step. when N_Indexed_Component | N_Slice => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (Prefix (N), Mode); + Set_Perm_Prefixes (Prefix (N), New_Perm); begin if C = null then + -- We went through a function call, do nothing return null; end if; - -- The permission of the returned node should be either - -- W (because the recursive call sets <= Write_Only) - -- or No (if another path has been moved with 'Access) - - if Mode = Super_Move then - pragma Assert (Permission (C) = No_Access); - null; - else - pragma Assert (Permission (C) = Write_Only - or else Permission (C) = No_Access); - null; - end if; - pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Array_Component); if Kind (C) = Array_Component then + -- The tree is unfolded. We just modify the permission and -- return the elem subtree. - if Get_Elem (C) = null then - -- Hash_Table_Error - raise Program_Error; - end if; - - -- The Get_Elem can have permissions : - -- RW : first move in this path - -- W : Already other moves in this path - -- No : Already other moves with 'Access - - pragma Assert (Permission (Get_Elem (C)) /= Read_Only); - - if Mode = Super_Move then - C.all.Tree.Get_Elem.all.Tree.Permission := No_Access; - else - C.all.Tree.Get_Elem.all.Tree.Permission := - Glb (Write_Only, Permission (Get_Elem (C))); - end if; - + pragma Assert (Get_Elem (C) /= null); + C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm; return Get_Elem (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace node with Array_Component. - -- We are in move mode, hence we can assume that the - -- Children_permission is RW. - - pragma Assert (Children_Permission (C) = Read_Write); - Son : Perm_Tree_Access; begin @@ -5618,14 +3966,12 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (C), - Permission => Read_Write, - Children_Permission => Read_Write)); + Permission => New_Perm, + Children_Permission => Children_Permission (C))); - if Mode = Super_Move then - Son.all.Tree.Permission := No_Access; - else - Son.all.Tree.Permission := Write_Only; - end if; + -- Children_Permission => Children_Permission (C) + -- this line should be checked maybe New_Perm + -- instead of Children_Permission (C) -- We change the current node from Entire_Object -- to Array_Component with same permission and the @@ -5633,9 +3979,8 @@ package body Sem_SPARK is C.all.Tree := (Kind => Array_Component, Is_Node_Deep => Is_Node_Deep (C), - Permission => Permission (C), + Permission => New_Perm, Get_Elem => Son); - return Get_Elem (C); end; else @@ -5651,56 +3996,32 @@ package body Sem_SPARK is when N_Explicit_Dereference => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (Prefix (N), Move); + Set_Perm_Prefixes (Prefix (N), New_Perm); begin if C = null then - -- We went through a function call: do nothing + + -- We went through a function call. Do nothing. return null; end if; - -- The permission of the returned node should be only - -- W (because the recursive call sets <= Write_Only) - -- No is NOT POSSIBLE here - - pragma Assert (Permission (C) = Write_Only); - pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Reference); if Kind (C) = Reference then + -- The tree is unfolded. We just modify the permission and -- return the elem subtree. - if Get_All (C) = null then - -- Hash_Table_Error - raise Program_Error; - end if; - - -- The Get_All can have permissions : - -- RW : first move in this path - -- W : Already other moves in this path - -- No : Already other moves with 'Access - - pragma Assert (Permission (Get_All (C)) /= Read_Only); - - if Mode = Super_Move then - C.all.Tree.Get_All.all.Tree.Permission := No_Access; - else - Get_All (C).all.Tree.Permission := - Glb (Write_Only, Permission (Get_All (C))); - end if; + pragma Assert (Get_All (C) /= null); + C.all.Tree.Get_All.all.Tree.Permission := New_Perm; return Get_All (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with Reference. - -- We are in Move or Super_Move mode, hence we can assume - -- that the Children_permission is RW. - - pragma Assert (Children_Permission (C) = Read_Write); - Son : Perm_Tree_Access; begin @@ -5708,28 +4029,20 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (N)), - Permission => Read_Write, - Children_Permission => Read_Write)); - - if Mode = Super_Move then - Son.all.Tree.Permission := No_Access; - else - Son.all.Tree.Permission := Write_Only; - end if; + Permission => New_Perm, + Children_Permission => Children_Permission (C))); -- We change the current node from Entire_Object to - -- Reference with Write_Only and the previous son. + -- Reference with Borrowed and the previous son. pragma Assert (Is_Node_Deep (C)); - C.all.Tree := (Kind => Reference, Is_Node_Deep => Is_Node_Deep (C), - Permission => Write_Only, - -- Write_only is equal to C.Permission + Permission => New_Perm, Get_All => Son); - return Get_All (C); end; + else raise Program_Error; end if; @@ -5741,55 +4054,34 @@ package body Sem_SPARK is when others => raise Program_Error; end case; + end Set_Perm_Prefixes; - end Set_Perm_Prefixes_Move; - - ------------------------------- - -- Set_Perm_Prefixes_Observe -- - ------------------------------- + ------------------------------ + -- Set_Perm_Prefixes_Borrow -- + ------------------------------ - function Set_Perm_Prefixes_Observe - (N : Node_Id) - return Perm_Tree_Access + function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access is begin - pragma Assert (Current_Checking_Mode = Observe); - + pragma Assert (Current_Checking_Mode = Borrow); case Nkind (N) is - -- Base identifier. Set permission to R. when N_Identifier | N_Expanded_Name - | N_Defining_Identifier => declare - P : Node_Id; - C : Perm_Tree_Access; + P : constant Node_Id := Entity (N); + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (P)); + pragma Assert (C /= null); begin - if Nkind (N) = N_Defining_Identifier then - P := N; - else - P := Entity (N); - end if; - - C := Get (Current_Perm_Env, Unique_Entity (P)); -- Setting the initialization map to True, so that this -- variable cannot be ignored anymore when looking at end -- of elaboration of package. Set (Current_Initialization_Map, Unique_Entity (P), True); - - if C = null then - -- No null possible here, there are no parents for the path. - -- This means we are using a global variable without adding - -- it in environment with a global aspect. - - Illegal_Global_Usage (N); - end if; - - C.all.Tree.Permission := Glb (Read_Only, Permission (C)); - + C.all.Tree.Permission := Borrowed; return C; end; @@ -5797,42 +4089,45 @@ package body Sem_SPARK is | N_Unchecked_Type_Conversion | N_Qualified_Expression => - return Set_Perm_Prefixes_Observe (Expression (N)); + return Set_Perm_Prefixes_Borrow (Expression (N)); - when N_Parameter_Specification => + when N_Parameter_Specification + | N_Defining_Identifier + => raise Program_Error; -- We set the permission tree of its prefix, and then we extract - -- from the returned pointer our subtree and assign an adequate + -- our subtree from the returned pointer and assign an adequate -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. + -- in one step. when N_Selected_Component => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); + Set_Perm_Prefixes_Borrow (Prefix (N)); begin if C = null then + -- We went through a function call, do nothing return null; end if; + -- The permission of the returned node should be No + + pragma Assert (Permission (C) = Borrowed); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Record_Component); if Kind (C) = Record_Component then + -- The tree is unfolded. We just modify the permission and - -- return the record subtree. We put the permission to the - -- glb of read_only and its current permission, to consider - -- the case of observing x.y while x.z has been moved. Then - -- x should be No_Access. + -- return the record subtree. declare Selected_Component : constant Entity_Id := Entity (Selector_Name (N)); - Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get (Component (C), Selected_Component); @@ -5843,12 +4138,10 @@ package body Sem_SPARK is end if; pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := - Glb (Read_Only, Permission (Selected_C)); - + Selected_C.all.Tree.Permission := Borrowed; return Selected_C; end; + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with @@ -5860,13 +4153,11 @@ package body Sem_SPARK is Hashtbl : Perm_Tree_Maps.Instance; - -- We create the unrolled nodes, that will all have RW - -- permission given that we are in move mode. We will - -- then set the right node to W. + -- We create the unrolled nodes, that will all have same + -- permission than parent. Son : Perm_Tree_Access; - - Child_Perm : constant Perm_Kind := + ChildrenPerm : constant Perm_Kind := Children_Permission (C); begin @@ -5875,21 +4166,22 @@ package body Sem_SPARK is -- hash table as component list. C.all.Tree := - (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (C), - Permission => Permission (C), - Component => Hashtbl, + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Hashtbl, Other_Components => new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, Is_Node_Deep => True, - Permission => Child_Perm, - Children_Permission => Child_Perm) + Permission => ChildrenPerm, + Children_Permission => ChildrenPerm) )); -- We fill the hash table with all sons of the record, -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (Etype (Prefix (N))); @@ -5898,26 +4190,21 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Elem)), - Permission => Child_Perm, - Children_Permission => Child_Perm)); - - Perm_Tree_Maps.Set - (C.all.Tree.Component, Elem, Son); - + Permission => ChildrenPerm, + Children_Permission => ChildrenPerm)); + Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son); Next_Component_Or_Discriminant (Elem); end loop; - -- Now we set the right field to Read_Only. and then we + -- Now we set the right field to Borrowed, and then we -- return the tree to the sons, so that the recursion can -- continue. declare Selected_Component : constant Entity_Id := Entity (Selector_Name (N)); - - Selected_C : Perm_Tree_Access := - Perm_Tree_Maps.Get - (Component (C), Selected_Component); + Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get + (Component (C), Selected_Component); begin if Selected_C = null then @@ -5925,65 +4212,62 @@ package body Sem_SPARK is end if; pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := - Glb (Read_Only, Child_Perm); - + Selected_C.all.Tree.Permission := Borrowed; return Selected_C; end; end; + else raise Program_Error; end if; end; - -- We set the permission tree of its prefix, and then we extract from - -- the returned pointer the subtree and assign an adequate permission - -- to it, if unfolded. If folded, we unroll the tree at one step. + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree in + -- one step. when N_Indexed_Component | N_Slice => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); + Set_Perm_Prefixes_Borrow (Prefix (N)); begin if C = null then + -- We went through a function call, do nothing return null; end if; + pragma Assert (Permission (C) = Borrowed); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Array_Component); if Kind (C) = Array_Component then + -- The tree is unfolded. We just modify the permission and -- return the elem subtree. pragma Assert (Get_Elem (C) /= null); - - C.all.Tree.Get_Elem.all.Tree.Permission := - Glb (Read_Only, Permission (Get_Elem (C))); - + C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed; return Get_Elem (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace node with Array_Component. Son : Perm_Tree_Access; - Child_Perm : constant Perm_Kind := - Glb (Read_Only, Children_Permission (C)); - begin Son := new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (C), - Permission => Child_Perm, - Children_Permission => Child_Perm)); + Permission => Borrowed, + Children_Permission => Children_Permission (C))); -- We change the current node from Entire_Object -- to Array_Component with same permission and the @@ -5991,9 +4275,8 @@ package body Sem_SPARK is C.all.Tree := (Kind => Array_Component, Is_Node_Deep => Is_Node_Deep (C), - Permission => Child_Perm, + Permission => Borrowed, Get_Elem => Son); - return Get_Elem (C); end; @@ -6002,64 +4285,64 @@ package body Sem_SPARK is end if; end; - -- We set the permission tree of its prefix, and then we extract from - -- the returned pointer the subtree and assign an adequate permission - -- to it, if unfolded. If folded, we unroll the tree at one step. + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. when N_Explicit_Dereference => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); + Set_Perm_Prefixes_Borrow (Prefix (N)); begin if C = null then - -- We went through a function call, do nothing + + -- We went through a function call. Do nothing. return null; end if; + -- The permission of the returned node should be No + + pragma Assert (Permission (C) = Borrowed); pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Reference); if Kind (C) = Reference then + -- The tree is unfolded. We just modify the permission and -- return the elem subtree. pragma Assert (Get_All (C) /= null); - - C.all.Tree.Get_All.all.Tree.Permission := - Glb (Read_Only, Permission (Get_All (C))); - + C.all.Tree.Get_All.all.Tree.Permission := Borrowed; return Get_All (C); + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with Reference. Son : Perm_Tree_Access; - Child_Perm : constant Perm_Kind := - Glb (Read_Only, Children_Permission (C)); - begin Son := new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (N)), - Permission => Child_Perm, - Children_Permission => Child_Perm)); + Permission => Borrowed, + Children_Permission => Children_Permission (C))); -- We change the current node from Entire_Object to - -- Reference with Write_Only and the previous son. + -- Reference with Borrowed and the previous son. pragma Assert (Is_Node_Deep (C)); - C.all.Tree := (Kind => Reference, Is_Node_Deep => Is_Node_Deep (C), - Permission => Child_Perm, + Permission => Borrowed, Get_All => Son); - return Get_All (C); end; + else raise Program_Error; end if; @@ -6070,16 +4353,14 @@ package body Sem_SPARK is when others => raise Program_Error; - end case; - end Set_Perm_Prefixes_Observe; + end Set_Perm_Prefixes_Borrow; ------------------- -- Setup_Globals -- ------------------- procedure Setup_Globals (Subp : Entity_Id) is - procedure Setup_Globals_From_List (First_Item : Node_Id; Kind : Formal_Kind); @@ -6123,12 +4404,17 @@ package body Sem_SPARK is begin case Global_Mode is - when Name_Input | Name_Proof_In => + when Name_Input + | Name_Proof_In + => Kind := E_In_Parameter; + when Name_Output => Kind := E_Out_Parameter; + when Name_In_Out => Kind := E_In_Out_Parameter; + when others => raise Program_Error; end case; @@ -6165,36 +4451,57 @@ package body Sem_SPARK is (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (Id)), - Permission => Read_Write, - Children_Permission => Read_Write)); + Permission => Unrestricted, + Children_Permission => Unrestricted)); case Mode is - when E_In_Parameter => - -- Borrowed IN: RW for everybody + -- All out and in out parameters are considered to be unrestricted. + -- They are whether borrowed or moved. Ada Rules would restrict + -- these permissions further. For example an in parameter cannot + -- be written. - if Is_Borrowed_In (Id) and not Global_Var then - Elem.all.Tree.Permission := Read_Write; - Elem.all.Tree.Children_Permission := Read_Write; + -- In the following we deal with in parameters that can be observed. + -- We only consider the observing cases. - -- Observed IN: R for everybody + when E_In_Parameter => - else - Elem.all.Tree.Permission := Read_Only; - Elem.all.Tree.Children_Permission := Read_Only; - end if; + -- Handling global variables as in parameters here + -- Remove the following condition once decided how globals + -- should be considered. + + if not Global_Var then + if (Is_Access_Type (Etype (Id)) + and then Is_Access_Constant (Etype (Id)) + and then Is_Anonymous_Access_Type (Etype (Id))) + or else + (not Is_Access_Type (Etype (Id)) + and then Is_Deep (Etype (Id)) + and then not Is_Anonymous_Access_Type (Etype (Id))) + then + Elem.all.Tree.Permission := Observed; + Elem.all.Tree.Children_Permission := Observed; - -- OUT: borrow, but callee has W only + else + Elem.all.Tree.Permission := Unrestricted; + Elem.all.Tree.Children_Permission := Unrestricted; + end if; - when E_Out_Parameter => - Elem.all.Tree.Permission := Write_Only; - Elem.all.Tree.Children_Permission := Write_Only; + else + Elem.all.Tree.Permission := Observed; + Elem.all.Tree.Children_Permission := Observed; + end if; - -- IN OUT: borrow and callee has RW + -- When out or in/out formal or global parameters, we set them to + -- the Unrestricted state. "We want to be able to assume that all + -- relevant writable globals are unrestricted when a subprogram + -- starts executing". Formal parameters of mode out or in/out + -- are whether Borrowers or the targets of a move operation: + -- they start theirs lives in the subprogram as Unrestricted. - when E_In_Out_Parameter => - Elem.all.Tree.Permission := Read_Write; - Elem.all.Tree.Children_Permission := Read_Write; + when others => + Elem.all.Tree.Permission := Unrestricted; + Elem.all.Tree.Children_Permission := Unrestricted; end case; Set (Current_Perm_Env, Id, Elem); @@ -6204,9 +4511,7 @@ package body Sem_SPARK is -- Setup_Parameters -- ---------------------- - procedure Setup_Parameters (Subp : Entity_Id) is - Formal : Entity_Id; - + procedure Setup_Parameters (Subp : Entity_Id) is Formal : Entity_Id; begin Formal := First_Formal (Subp); while Present (Formal) loop @@ -6216,4 +4521,85 @@ package body Sem_SPARK is end loop; end Setup_Parameters; + ------------------------------- + -- Has_Ownership_Aspect_True -- + ------------------------------- + + function Has_Ownership_Aspect_True + (N : Entity_Id; + Msg : String) + return Boolean + is + begin + case Ekind (Etype (N)) is + when Access_Kind => + if Ekind (Etype (N)) = E_General_Access_Type then + Error_Msg_NE (Msg & " & not allowed " & + "(Named General Access type)", N, N); + return False; + + else + return True; + end if; + + when E_Array_Type + | E_Array_Subtype + => + declare + Com_Ty : constant Node_Id := Component_Type (Etype (N)); + Ret : Boolean := Has_Ownership_Aspect_True (Com_Ty, ""); + + begin + if Nkind (Parent (N)) = N_Full_Type_Declaration and + Is_Anonymous_Access_Type (Com_Ty) + then + Ret := False; + end if; + + if not Ret then + Error_Msg_NE (Msg & " & not allowed " + & "(Components of Named General Access type or" + & " Anonymous type)", N, N); + end if; + return Ret; + end; + + -- ??? What about hidden components + + when E_Record_Type + | E_Record_Subtype + => + declare + Elmt : Entity_Id; + Elmt_T_Perm : Boolean := True; + Elmt_Perm, Elmt_Anonym : Boolean; + + begin + Elmt := First_Component_Or_Discriminant (Etype (N)); + while Present (Elmt) loop + Elmt_Perm := Has_Ownership_Aspect_True (Elmt, + "type of component"); + Elmt_Anonym := Is_Anonymous_Access_Type (Etype (Elmt)); + if Elmt_Anonym then + Error_Msg_NE + ("type of component & not allowed" + & " (Components of Anonymous type)", Elmt, Elmt); + end if; + Elmt_T_Perm := Elmt_T_Perm and Elmt_Perm and not Elmt_Anonym; + Next_Component_Or_Discriminant (Elmt); + end loop; + if not Elmt_T_Perm then + Error_Msg_NE + (Msg & " & not allowed (One or " + & "more components have Ownership Aspect False)", + N, N); + end if; + return Elmt_T_Perm; + end; + + when others => + return True; + end case; + + end Has_Ownership_Aspect_True; end Sem_SPARK;

[Ada] Update for Ownership rules for access types according to AI12-0240

Commit Message

Patch