Mercurial > hg > CbC > CbC_gcc
diff gcc/ada/sem_spark.adb @ 131:84e7813d76e9
gcc-8.2
| author | mir3636 |
|---|---|
| date | Thu, 25 Oct 2018 07:37:49 +0900 |
| parents | 04ced10e8804 |
| children |
line wrap: on
line diff
--- a/gcc/ada/sem_spark.adb Fri Oct 27 22:46:09 2017 +0900 +++ b/gcc/ada/sem_spark.adb Thu Oct 25 07:37:49 2018 +0900 @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2017, Free Software Foundation, Inc. -- +-- Copyright (C) 2017-2018, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -52,15 +52,16 @@ 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 @@ -- 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 @@ -- 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 @@ -- 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 @@ -------------------- 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 @@ -- 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 @@ 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 @@ -- 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 @@ 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 @@ -- 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 @@ -- 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 @@ -- 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 @@ 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 @@ -- 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 @@ -- 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 @@ -- 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 @@ -- 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 @@ 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 @@ -- 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 @@ -- 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; @@ -540,36 +505,31 @@ type Checking_Mode is (Read, - -- Default mode. Checks that paths have Read_Perm permission. + -- Default mode 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, the permission of both it and + -- its extensions are 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. 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); @@ -592,11 +552,6 @@ -- 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. @@ -607,24 +562,15 @@ -- 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 @@ -637,25 +583,15 @@ 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_Read (Formal : Entity_Id; Actual : Node_Id); + procedure Check_Param_In (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. + -- permission of every in-mode parameter. This includes Observing and + -- Borrowing. + + procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and checks the + -- state of every out-mode and in out-mode parameter. This includes + -- Moving and Borrowing. procedure Check_Statement (Stmt : Node_Id); @@ -673,20 +609,6 @@ -- 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. @@ -697,28 +619,13 @@ -- 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 @@ -741,7 +648,7 @@ 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); @@ -749,78 +656,56 @@ -- of the subprogram indeed have RW permission at the end of the subprogram -- execution. - procedure Return_Parameter_Or_Global + procedure Return_The_Global (Id : Entity_Id; Mode : Formal_Kind; Subp : Entity_Id); - -- 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. + -- 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 -- global items with appropriate permissions. procedure Setup_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind); + (Id : Entity_Id; + Mode : Formal_Kind; + Global_Var : Boolean); -- Auxiliary procedure to Setup_Parameters and Setup_Globals procedure Setup_Parameters (Subp : Entity_Id); -- 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 -- ---------------------- @@ -858,31 +743,6 @@ -- 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 -- -------------------------- @@ -890,64 +750,40 @@ 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 + + Copy_Env (Current_Perm_Env, Saved_Env); + + -- 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. 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); - - Iterate_Call_Outs (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), - Borrow_Out); - - Iterate_Call (Call); - Check_Globals (Get_Pragma - (Get_Called_Entity (Call), Pragma_Global), Move); + 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; ------------------------- @@ -956,15 +792,12 @@ 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 @@ -986,9 +819,8 @@ -- 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 @@ -1007,23 +839,18 @@ 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 @@ -1036,39 +863,241 @@ ----------------------- procedure Check_Declaration (Decl : Node_Id) is + + Target_Ent : constant Entity_Id := Defining_Identifier (Decl); + Target_Typ : Node_Id renames Etype (Target_Ent); + + Target_View_Typ : Entity_Id; + + Check : Boolean := True; begin + if Present (Full_View (Target_Typ)) then + Target_View_Typ := Full_View (Target_Typ); + else + Target_View_Typ := Target_Typ; + end if; + case N_Declaration'(Nkind (Decl)) is when N_Full_Type_Declaration => - -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE - null; + if not Has_Ownership_Aspect_True (Target_Ent, "type declaration") + then + Check := False; + end if; + + -- ??? What about component declarations with defaults. when N_Object_Declaration => - -- First move the right-hand side - Current_Checking_Mode := Move; - Check_Node (Expression (Decl)); + if (Is_Access_Type (Target_View_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_View_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_View_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_View_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_View_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 + + if not Is_Access_Constant (Target_View_Typ) then + + -- Initializing object, variable named access to + -- variable type. + + if not Is_Anonymous_Access_Type (Target_View_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_View_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; + + end if; + end if; + + if Check then + Check_Node (Expression (Decl)); + end if; + + -- If lhs is not a pointer, we still give it the unrestricted + -- state which is useless but not harmful. declare Elem : Perm_Tree_Access; + Deep : constant Boolean := Is_Deep (Target_Typ); begin - Elem := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => - Is_Deep (Etype (Defining_Identifier (Decl))), - 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 Nkind (Expression (Decl)) = N_Empty - and then not Has_Full_Default_Initialization - (Etype (Defining_Identifier (Decl))) - and then not Is_Access_Type - (Etype (Defining_Identifier (Decl))) - 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 @@ -1076,29 +1105,24 @@ Set (Current_Perm_Env, Unique_Entity (Defining_Identifier (Decl)), Elem); - - pragma Assert (Get_First (Current_Perm_Env) - /= null); - + pragma Assert (Get_First (Current_Perm_Env) /= null); end; when N_Subtype_Declaration => 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; @@ -1128,29 +1152,33 @@ 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)); @@ -1162,41 +1190,16 @@ | N_Op_Not | N_Op_Plus => - pragma Assert (Is_Shallow (Etype (Expr))); Current_Checking_Mode := Read; Check_Node (Right_Opnd (Expr)); -- Forbid all deep expressions for Attribute ??? + -- What about generics? (formal parameters). 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", Expr); when Name_Last | Name_First @@ -1209,6 +1212,9 @@ Check_Node (Prefix (Expr)); when Name_Image => + Check_List (Expressions (Expr)); + + when Name_Img => Check_Node (Prefix (Expr)); when Name_SPARK_Mode => @@ -1223,7 +1229,7 @@ Check_Node (Prefix (Expr)); when Name_Pred - | Name_Succ + | Name_Succ => Check_List (Expressions (Expr)); Check_Node (Prefix (Expr)); @@ -1238,12 +1244,12 @@ -- 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; @@ -1254,7 +1260,6 @@ | Name_Val => null; - -- Other attributes that fall out of the scope of the analysis when others => @@ -1276,17 +1281,12 @@ 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); @@ -1299,20 +1299,16 @@ -- 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. @@ -1325,15 +1321,10 @@ -- 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. @@ -1341,14 +1332,9 @@ 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; @@ -1364,6 +1350,7 @@ when N_Quantified_Expression => declare Saved_Env : Perm_Env; + begin Copy_Env (Current_Perm_Env, Saved_Env); Current_Checking_Mode := Read; @@ -1375,7 +1362,6 @@ Copy_Env (Saved_Env, Current_Perm_Env); Free_Env (Saved_Env); end; - -- Analyze the list of associations in the aggregate when N_Aggregate => @@ -1392,19 +1378,16 @@ -- 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. @@ -1413,43 +1396,29 @@ 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); - + 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)); @@ -1491,7 +1460,6 @@ | N_Raise_xxx_Error => null; - -- The following nodes are never generated in GNATprove mode when N_Expression_With_Actions @@ -1499,7 +1467,6 @@ | N_Unchecked_Expression => raise Program_Error; - end case; end Check_Expression; @@ -1507,150 +1474,63 @@ -- 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 Check_Mode is - when Read => - case Mode is - when Name_Input - | Name_Proof_In - => - Check_Node (The_Global); - - when Name_Output - | Name_In_Out - => - null; - - when others => - raise Program_Error; - - 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; - + case Mode is + when Name_Input + | Name_Proof_In + => + Current_Checking_Mode := Observe; 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 Name_Output + | Name_In_Out + => + -- ??? Borrow not Move? + Current_Checking_Mode := Borrow; + Check_Node (The_Global); 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 @@ -1658,6 +1538,7 @@ then -- global => (foo, bar) -- Inputs + RHS := First (Expressions (Expression (PAA))); while Present (RHS) loop case Nkind (RHS) is @@ -1671,7 +1552,6 @@ when others => raise Program_Error; - end case; RHS := Next (RHS); end loop; @@ -1691,8 +1571,8 @@ 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)); @@ -1703,7 +1583,6 @@ when others => Process (The_Mode, RHS); - end case; RHS := Next (RHS); end loop; @@ -1721,9 +1600,7 @@ when others => raise Program_Error; - end case; - Row := Next (Row); end loop; end; @@ -1754,339 +1631,6 @@ 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)); @@ -2110,6 +1654,7 @@ 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); @@ -2121,12 +1666,6 @@ 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 @@ -2145,12 +1684,12 @@ if Exit_Env /= null then Copy_Env (From => Exit_Env.all, To => Current_Perm_Env); + Free_Env (Loop_Env.all); + Free_Env (Exit_Env.all); else Copy_Env (From => Loop_Env.all, To => Current_Perm_Env); + Free_Env (Loop_Env.all); end if; - - Free_Env (Loop_Env.all); - Free_Env (Exit_Env.all); end; end Check_Loop_Statement; @@ -2192,6 +1731,7 @@ when N_Package_Declaration => declare Spec : constant Node_Id := Specification (N); + begin Current_Checking_Mode := Read; Check_List (Visible_Declarations (Spec)); @@ -2258,7 +1798,6 @@ | N_Delay_Alternative | N_Derived_Type_Definition | N_Designator - | N_Discriminant_Association | N_Discriminant_Specification | N_Elsif_Part | N_Entry_Body_Formal_Part @@ -2349,9 +1888,13 @@ | N_With_Clause | 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 @@ -2391,15 +1934,12 @@ -- 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)); @@ -2413,137 +1953,137 @@ -- 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 -- - ----------------- - - procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is + -------------------- + -- Check_Param_In -- + -------------------- + + 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; + case Formal_Kind'(Mode) is + + -- Formal IN parameter + + when E_In_Parameter => + + -- Formal IN parameter, access type + + if Is_Access_Type (Etype (Formal)) then + + -- Formal IN parameter, access to variable type + + if not Is_Access_Constant (Etype (Formal)) then + + -- Formal IN parameter, named/anonymous access-to-variable + -- type. + -- + -- In SPARK, IN access-to-variable is an observe operation + -- for a function, and a borrow operation for a procedure. + + if Ekind (Scope (Formal)) = E_Function then + Current_Checking_Mode := Observe; + Check_Node (Actual); else - -- Observed - - return; + Current_Checking_Mode := Borrow; + Check_Node (Actual); end if; - when E_Out_Parameter => - return; - - when E_In_Out_Parameter => - -- Borrowed in out - - Current_Checking_Mode := Move; - - end case; - - Check_Node (Actual); - - when Assign => - case Formal_Kind'(Mode) is - when E_In_Parameter => - null; - - when E_Out_Parameter - | E_In_Out_Parameter - => - -- Borrowed out or in out - - Process_Path (Actual); - - end case; - - when others => - raise Program_Error; - - end case; - Current_Checking_Mode := Mode_Before; - end Check_Param; - - -------------------------- - -- Check_Param_Observes -- - -------------------------- - - 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; - - begin - case Mode is - when E_In_Parameter => - if not Is_Borrowed_In (Formal) then - -- Observed in + -- Formal IN parameter, access-to-constant type + -- Formal IN parameter, access-to-named-constant type + + elsif not Is_Anonymous_Access_Type (Etype (Formal)) then + Error_Msg_N ("assignment not allowed, Ownership Aspect" + & " False (Named general access type)", + Formal); + + -- Formal IN parameter, access to anonymous constant type + + else + Current_Checking_Mode := Observe; + Check_Node (Actual); + end if; + + -- Formal IN parameter, composite type + + elsif Is_Deep (Etype (Formal)) then + + -- Composite formal types should be named + -- Formal IN parameter, composite named type Current_Checking_Mode := Observe; Check_Node (Actual); end if; - when others => - null; - - end case; - - Current_Checking_Mode := Mode_Before; - end Check_Param_Observes; - - ---------------------- - -- Check_Param_Outs -- - ---------------------- - - procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); - Mode_Before : constant Checking_Mode := Current_Checking_Mode; - - begin - - case Mode is - when E_Out_Parameter => - -- Borrowed out - Current_Checking_Mode := Borrow_Out; - Check_Node (Actual); - - when others => - null; - - end case; - - Current_Checking_Mode := Mode_Before; - end Check_Param_Outs; - - ---------------------- - -- Check_Param_Read -- - ---------------------- - - procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); - - begin - pragma Assert (Current_Checking_Mode = Read); - - case Formal_Kind'(Mode) is - when E_In_Parameter => - Check_Node (Actual); - when E_Out_Parameter | E_In_Out_Parameter => null; - end case; - end Check_Param_Read; + + Current_Checking_Mode := Mode_Before; + end Check_Param_In; + + ---------------------- + -- Check_Param_Out -- + ---------------------- + + 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 + + -- Formal OUT/IN OUT parameter + + when E_Out_Parameter + | E_In_Out_Parameter + => + + -- Formal OUT/IN OUT parameter, access type + + if Is_Access_Type (Etype (Formal)) then + + -- Formal OUT/IN OUT parameter, access to variable type + + if not Is_Access_Constant (Etype (Formal)) then + + -- Cannot have anonymous out access parameter + -- Formal out/in out parameter, access to named variable + -- type. + + Current_Checking_Mode := Move; + Check_Node (Actual); + + -- 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; + + Current_Checking_Mode := Mode_Before; + end Check_Param_Out; ------------------------- -- Check_Safe_Pointers -- @@ -2588,13 +2128,13 @@ -- 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)); @@ -2630,6 +2170,42 @@ procedure Check_Statement (Stmt : Node_Id) is Mode_Before : constant Checking_Mode := Current_Checking_Mode; + State_N : Perm_Kind; + Check : Boolean := True; + St_Name : Node_Id; + Ty_St_Name : Node_Id; + + function Get_Root (Comp_Stmt : Node_Id) return Node_Id; + -- Return the root of the name given as input + + 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_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 => @@ -2638,25 +2214,200 @@ -- Move right-hand side first, and then assign left-hand side when N_Assignment_Statement => - if Is_Deep (Etype (Expression (Stmt))) then - Current_Checking_Mode := Move; - else - Current_Checking_Mode := Read; + + 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 Entity (St_Name) /= + Entity (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_In (Ty_St_Name, + E_Record_Type, + E_Record_Subtype) + 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; + + elsif Ekind_In (Ty_St_Name, + E_Array_Type, + E_Array_Subtype) + and then Check + then + Current_Checking_Mode := Move; + 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; - Check_Node (Expression (Stmt)); - Current_Checking_Mode := Assign; - Check_Node (Name (Stmt)); - 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 @@ -2667,8 +2418,7 @@ -- 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 => @@ -2678,7 +2428,6 @@ -- Accumulator for the different branches New_Env : Perm_Env; - Elmt : Node_Id := First (Alternatives (Stmt)); begin @@ -2688,8 +2437,7 @@ -- 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. @@ -2698,33 +2446,21 @@ 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); - + 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; @@ -2738,7 +2474,7 @@ 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 @@ -2750,65 +2486,42 @@ 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; - - -- Copy environment, run on each branch, and then merge + null; + + -- Copy environment, run on each branch when N_If_Statement => declare @@ -2819,13 +2532,11 @@ 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. @@ -2833,34 +2544,25 @@ -- 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); - + 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; @@ -2869,21 +2571,16 @@ -- 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); @@ -2939,8 +2636,7 @@ -- which means that the association permission is RW. when Function_Call => - return Read_Write; - + return Unrestricted; end case; end Get_Perm; @@ -2963,7 +2659,6 @@ => declare P : constant Entity_Id := Entity (N); - C : constant Perm_Tree_Access := Get (Current_Perm_Env, Unique_Entity (P)); @@ -2973,13 +2668,13 @@ -- 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; @@ -3006,8 +2701,7 @@ 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 @@ -3018,7 +2712,6 @@ when Unfolded => pragma Assert (C.Tree_Access /= null); - pragma Assert (Kind (C.Tree_Access) = Entire_Object or else Kind (C.Tree_Access) = Record_Component); @@ -3027,30 +2720,32 @@ 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 @@ -3060,8 +2755,7 @@ | 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 @@ -3072,25 +2766,24 @@ 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 @@ -3098,8 +2791,7 @@ 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 @@ -3110,29 +2802,32 @@ 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. @@ -3148,10 +2843,7 @@ -- 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 @@ -3166,7 +2858,6 @@ => declare P : constant Node_Id := Entity (N); - C : constant Perm_Tree_Access := Get (Current_Perm_Env, Unique_Entity (P)); @@ -3176,13 +2867,13 @@ -- 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; @@ -3203,11 +2894,11 @@ 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; @@ -3217,6 +2908,7 @@ or else Kind (C) = Record_Component); if Kind (C) = Record_Component then + -- The tree is unfolded. We just return the subtree. declare @@ -3230,9 +2922,9 @@ 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 @@ -3248,7 +2940,6 @@ 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. @@ -3271,6 +2962,7 @@ -- We fill the hash table with all sons of the record, -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (Etype (Prefix (N))); @@ -3284,10 +2976,8 @@ 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. @@ -3301,16 +2991,13 @@ 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. @@ -3319,8 +3006,7 @@ | 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 @@ -3328,16 +3014,16 @@ 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. @@ -3360,14 +3046,12 @@ 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. @@ -3380,6 +3064,7 @@ C := Get_Perm_Tree (Prefix (N)); if C = null then + -- If null, we went through a function call return null; @@ -3389,14 +3074,17 @@ 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. @@ -3415,19 +3103,16 @@ -- 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 => @@ -3438,245 +3123,6 @@ end case; end Get_Perm_Tree; - --------- - -- Glb -- - --------- - - 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; - - when Read_Perm => - return Read_Only; - end case; - - when Write_Only => - case P2 is - when No_Access - | Read_Only - => - return No_Access; - - when Write_Perm => - return Write_Only; - end case; - - when Read_Write => - return P2; - end case; - end Glb; - - --------------- - -- Has_Alias -- - --------------- - - 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_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; - - Next_Component_Or_Discriminant (Comp); - end loop; - return False; - else - return Is_Aliased (Typ); - end if; - end Has_Alias_Deep; - - begin - case Nkind (N) is - - when N_Identifier - | N_Expanded_Name - => - return Has_Alias_Deep (Etype (N)); - - when N_Defining_Identifier => - return 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 -- -------- @@ -3700,29 +3146,17 @@ 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; @@ -3745,9 +3179,9 @@ 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; @@ -3776,7 +3210,7 @@ when E_Record_Type | E_Record_Subtype - => + => declare Elmt : Entity_Id; @@ -3789,7 +3223,6 @@ Next_Component_Or_Discriminant (Elmt); end if; end loop; - return False; end; @@ -3804,10 +3237,9 @@ 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 @@ -3828,311 +3260,6 @@ end Is_Deep; ---------------- - -- Is_Shallow -- - ---------------- - - 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 - 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; - - when Read_Perm => - return Read_Write; - end case; - - when Read_Write => - return Read_Write; - end case; - end Lub; - - ---------------- - -- Merge_Envs -- - ---------------- - - 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); - - 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); - - case Kind (A) is - when Entire_Object => - A.all.Tree.Children_Permission := - Glb (Children_Permission (A), P); - - when Reference => - Apply_Glb_Tree (Get_All (A), P); - - when Array_Component => - Apply_Glb_Tree (Get_Elem (A), P); - - 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 -- ---------------- @@ -4185,7 +3312,6 @@ raise Program_Error; end case; end Set_Root_Object; - -- Local variables Root : Entity_Id; @@ -4228,7 +3354,8 @@ ------------------ 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 @@ -4238,194 +3365,153 @@ return; end if; - -- We ignore shallow unaliased. They are checked in flow analysis, - -- allowing backward compatibility. - - if 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 - -- Check permission R, do nothing - - when Read => - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - end if; - - -- If shallow type no need for RW, only R - - when Move => - if Is_Shallow (Etype (N)) then - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - end if; - else - -- Check permission RW if deep - - if Perm_N /= Read_Write then - Perm_Error (N, Read_Write, Perm_N); - end if; - - declare - -- Set permission to W to the path and any of its prefix - - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (N, Move); - - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. - - return; - end if; - - -- 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 - - Set_Perm_Extensions_Move (Tree, Etype (N)); - end; - end if; - - -- Check permission RW - - when Super_Move => - if Perm_N /= Read_Write then - Perm_Error (N, Read_Write, Perm_N); - 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 permissions to No on any strict extension of the path - - Set_Perm_Extensions (Tree, No_Access); - end; - - -- Check permission W - - when Assign => - if Perm_N not in Write_Perm then - Perm_Error (N, Write_Only, Perm_N); - end if; - - -- If the tree has an array component, then the permissions do - -- not get modified by the assignment. - - if Has_Array_Component (N) then + State_N := Get_Perm (N); + + case Current_Checking_Mode is + + -- Check permission R, do nothing + + when Read => + + -- This condition should be removed when removing the read + -- checking mode. + + return; + + when Move => + + -- 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. + + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + return; + end if; + + -- 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; + + declare + -- Set state to Moved to the path and any of its prefixes + + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes (N, Moved); + + begin + if Tree = null then + + -- We went through a function call, no permission to + -- modify. + return; end if; - -- Same if has function component - - if Has_Function_Component (N) then + -- Set state to Moved on any strict extension of the path + + Set_Perm_Extensions (Tree, Moved); + end; + + when Assign => + + -- 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. + + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + return; + end if; + + -- After assigning to a path nothing to do since it was in the + -- Unrestricted state and it would be refreshed to + -- Unrestricted. + + when Borrow => + + -- Borrowing is only allowed on Unrestricted objects. + + if State_N /= Unrestricted and State_N /= Moved then + Perm_Error (N, Unrestricted, State_N); + end if; + + if State_N = Moved then + Error_Msg_N ("?the source or one of its extensions has" + & " already been moved", N); + end if; + + declare + -- Set state to Borrowed to the path and any of its prefixes + + 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. + return; end if; - declare - -- Get the permission tree for the path - - Tree : constant Perm_Tree_Access := - Get_Perm_Tree (N); - - Dummy : Perm_Tree_Access; - - begin - if Tree = null then - -- We went through a function call, no permission to - -- modify. - - return; - end if; - - -- Set permission RW for it and all of its extensions - - Tree.all.Tree.Permission := Read_Write; - - Set_Perm_Extensions (Tree, Read_Write); - - -- Normalize the permission tree - - Dummy := Set_Perm_Prefixes_Assign (N); - end; - - -- Check permission W - - when Borrow_Out => - if Perm_N not in Write_Perm then - Perm_Error (N, Write_Only, Perm_N); + -- Set state to Borrowed on any strict extension of the path + + Set_Perm_Extensions (Tree, Borrowed); + end; + + when Observe => + if State_N /= Unrestricted + and then State_N /= Observed + then + Perm_Error (N, Observed, State_N); + end if; + + 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. + + Tree : Perm_Tree_Access; + + 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; - - when Observe => - if Perm_N not in Read_Perm then - Perm_Error (N, Read_Only, Perm_N); - end if; - - if Is_By_Copy_Type (Etype (N)) then + if Tree = null then + + -- We went through a function call, no permission to + -- modify. + 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_Perm_Extensions (Tree, Read_Only); - end; - end case; - end; + -- Set permissions to No on any strict extension of the path + + Set_Perm_Extensions (Tree, Observed); + end; + end case; end Process_Path; ------------------------- @@ -4433,7 +3519,6 @@ ------------------------- procedure Return_Declarations (L : List_Id) is - procedure Return_Declaration (Decl : Node_Id); -- Check correct permissions for every declared object @@ -4444,6 +3529,7 @@ 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. @@ -4453,15 +3539,6 @@ 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, @@ -4469,22 +3546,23 @@ 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; @@ -4504,7 +3582,6 @@ -------------------- procedure Return_Globals (Subp : Entity_Id) is - procedure Return_Globals_From_List (First_Item : Node_Id; Kind : Formal_Kind); @@ -4533,7 +3610,7 @@ if Ekind (E) = E_Abstract_State then null; else - Return_Parameter_Or_Global (E, Kind, Subp); + Return_The_Global (E, Kind, Subp); end if; Next_Global (Item); end loop; @@ -4548,7 +3625,9 @@ 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; @@ -4578,7 +3657,7 @@ -- Return_Parameter_Or_Global -- -------------------------------- - procedure Return_Parameter_Or_Global + procedure Return_The_Global (Id : Entity_Id; Mode : Formal_Kind; Subp : Entity_Id) @@ -4587,59 +3666,45 @@ 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) then - null; - - -- All other parameters and globals should return with mode RW to the - -- caller. - - else - if Permission (Elem) /= Read_Write then + if Mode = E_In_Parameter + + -- Check this for read-only globals. + + then + if Permission (Elem) /= Unrestricted + and then Permission (Elem) /= Observed + then Perm_Error_Subprogram_End (E => Id, Subp => Subp, - Perm => Read_Write, + Perm => Observed, + Found_Perm => Permission (Elem)); + end if; + + -- All globals of mode out or in/out should return with mode + -- Unrestricted. + + 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_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); - Next_Formal (Formal); - end loop; - end Return_Parameters; + end Return_The_Global; ------------------------- -- Set_Perm_Extensions -- ------------------------- - procedure Set_Perm_Extensions - (T : Perm_Tree_Access; - P : Perm_Kind) - is + 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 + procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is begin case Kind (T) is when Entire_Object => @@ -4682,315 +3747,59 @@ end Set_Perm_Extensions; ------------------------------ - -- Set_Perm_Extensions_Move -- + -- Set_Perm_Prefixes -- ------------------------------ - procedure Set_Perm_Extensions_Move - (T : Perm_Tree_Access; - E : Entity_Id) + function Set_Perm_Prefixes + (N : Node_Id; + New_Perm : Perm_Kind) + return Perm_Tree_Access 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); - 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 - Perm : Perm_Kind := Read_Write; - - Comp : Perm_Tree_Access; - - 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 - => + 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)); - - pragma Assert (C /= null); + P : Node_Id; + C : Perm_Tree_Access; begin + 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); - - C.all.Tree.Permission := No_Access; + if New_Perm = Observed + and then 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 := New_Perm; return C; end; @@ -4998,11 +3807,9 @@ | N_Unchecked_Type_Conversion | N_Qualified_Expression => - return Set_Perm_Prefixes_Borrow_Out (Expression (N)); - - when N_Parameter_Specification - | N_Defining_Identifier - => + return Set_Perm_Prefixes (Expression (N), New_Perm); + + when N_Parameter_Specification => raise Program_Error; -- We set the permission tree of its prefix, and then we extract @@ -5013,19 +3820,16 @@ when N_Selected_Component => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + 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 No - - pragma Assert (Permission (C) = No_Access); - pragma Assert (Kind (C) = Entire_Object or else Kind (C) = Record_Component); @@ -5047,11 +3851,309 @@ end if; pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := No_Access; - + 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 + -- 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; + Children_Perm : 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 => 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))); + + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + 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 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); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + Selected_C.all.Tree.Permission := New_Perm; + 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. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes (Prefix (N), New_Perm); + + begin + if C = null then + + -- We went through a function call, do nothing + + 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 modify the permission and + -- return the elem subtree. + + 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. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (C), + Permission => New_Perm, + Children_Permission => Children_Permission (C))); + + -- 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 + -- previously defined son. + + C.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => New_Perm, + Get_Elem => Son); + return Get_Elem (C); + 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. + + when N_Explicit_Dereference => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes (Prefix (N), New_Perm); + + begin + if C = null then + + -- We went through a function call. Do nothing. + + return null; + end if; + + 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 := New_Perm; + return Get_All (C); + + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with Reference. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (N)), + Permission => New_Perm, + Children_Permission => Children_Permission (C))); + + -- We change the current node from Entire_Object to + -- 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 => New_Perm, + Get_All => Son); + return Get_All (C); + end; + + else + raise Program_Error; + end if; + end; + + when N_Function_Call => + return null; + + when others => + raise Program_Error; + end case; + end Set_Perm_Prefixes; + + ------------------------------ + -- Set_Perm_Prefixes_Borrow -- + ------------------------------ + + function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access + is + begin + pragma Assert (Current_Checking_Mode = Borrow); + case Nkind (N) is + + 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 := Borrowed; + return C; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Set_Perm_Prefixes_Borrow (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 (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. + + 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 := Borrowed; + return Selected_C; + end; + elsif Kind (C) = Entire_Object then declare -- Expand the tree. Replace the node with @@ -5067,7 +4169,6 @@ -- permission than parent. Son : Perm_Tree_Access; - ChildrenPerm : constant Perm_Kind := Children_Permission (C); @@ -5092,6 +4193,7 @@ -- We fill the hash table with all sons of the record, -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (Etype (Prefix (N))); @@ -5102,24 +4204,19 @@ Is_Node_Deep => Is_Deep (Etype (Elem)), Permission => ChildrenPerm, Children_Permission => ChildrenPerm)); - - Perm_Tree_Maps.Set - (C.all.Tree.Component, Elem, Son); - + 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 + -- 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 @@ -5127,12 +4224,11 @@ end if; pragma Assert (Selected_C /= null); - - Selected_C.all.Tree.Permission := No_Access; - + Selected_C.all.Tree.Permission := Borrowed; return Selected_C; end; end; + else raise Program_Error; end if; @@ -5148,33 +4244,29 @@ => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (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 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); - + 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 := No_Access; - + 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. @@ -5186,7 +4278,7 @@ (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Node_Deep (C), - Permission => No_Access, + Permission => Borrowed, Children_Permission => Children_Permission (C))); -- We change the current node from Entire_Object @@ -5195,11 +4287,11 @@ C.all.Tree := (Kind => Array_Component, Is_Node_Deep => Is_Node_Deep (C), - Permission => No_Access, + Permission => Borrowed, Get_Elem => Son); - return Get_Elem (C); end; + else raise Program_Error; end if; @@ -5213,10 +4305,11 @@ when N_Explicit_Dereference => declare C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + Set_Perm_Prefixes_Borrow (Prefix (N)); begin if C = null then + -- We went through a function call. Do nothing. return null; @@ -5224,19 +4317,19 @@ -- The permission of the returned node should be No - pragma Assert (Permission (C) = No_Access); + 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 := No_Access; - + 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. @@ -5248,21 +4341,20 @@ (Tree => (Kind => Entire_Object, Is_Node_Deep => Is_Deep (Etype (N)), - Permission => No_Access, + Permission => Borrowed, Children_Permission => Children_Permission (C))); -- We change the current node from Entire_Object to - -- Reference with No_Access 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 => No_Access, + Permission => Borrowed, Get_All => Son); - return Get_All (C); end; + else raise Program_Error; end if; @@ -5274,784 +4366,13 @@ when others => raise Program_Error; end case; - end Set_Perm_Prefixes_Borrow_Out; - - ---------------------------- - -- Set_Perm_Prefixes_Move -- - ---------------------------- - - function Set_Perm_Prefixes_Move - (N : Node_Id; Mode : Checking_Mode) - return Perm_Tree_Access - is - begin - case Nkind (N) is - - -- Base identifier. Set permission to W or No depending on Mode. - - 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)); - - 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; - end if; - - -- 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; - - if Mode = Super_Move then - C.all.Tree.Permission := No_Access; - else - C.all.Tree.Permission := Glb (Write_Only, Permission (C)); - end if; - - return C; - end; - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Set_Perm_Prefixes_Move (Expression (N), Mode); - - 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 - -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. - - when N_Selected_Component => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (Prefix (N), Mode); - - 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); - - 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 - -- 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)); - - end if; - - 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 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. - - 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. - - 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 => 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 - (Etype (Prefix (N))); - - 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)); - - 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. - - 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); - - -- 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; - - 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. - - when N_Indexed_Component - | N_Slice - => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Move (Prefix (N), Mode); - - 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; - - 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 - Son := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (C), - 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; - - -- We change the current node from Entire_Object - -- to Array_Component with same permission and the - -- previously defined son. - - C.all.Tree := (Kind => Array_Component, - 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 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_Move (Prefix (N), Move); - - 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 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; - 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 - Son := new Perm_Tree_Wrapper' - (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; - - -- We change the current node from Entire_Object to - -- Reference with Write_Only 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 - Get_All => Son); - - return Get_All (C); - end; - else - raise Program_Error; - end if; - end; - - when N_Function_Call => - return null; - - when others => - raise Program_Error; - end case; - - end Set_Perm_Prefixes_Move; - - ------------------------------- - -- Set_Perm_Prefixes_Observe -- - ------------------------------- - - function Set_Perm_Prefixes_Observe - (N : Node_Id) - return Perm_Tree_Access - is - begin - pragma Assert (Current_Checking_Mode = Observe); - - 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; - - 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)); - - return C; - end; - - when N_Type_Conversion - | N_Unchecked_Type_Conversion - | N_Qualified_Expression - => - return Set_Perm_Prefixes_Observe (Expression (N)); - - 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 - -- permission to it, if unfolded. If folded, we unroll the tree - -- at one step. - - when N_Selected_Component => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); - - begin - if C = null then - -- We went through a function call, do nothing - - return null; - end if; - - 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. - - 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 := - Glb (Read_Only, Permission (Selected_C)); - - 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 RW - -- permission given that we are in move mode. We will - -- then set the right node to W. - - Son : Perm_Tree_Access; - - Child_Perm : 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 => Child_Perm, - Children_Permission => Child_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))); - - while Present (Elem) loop - Son := new Perm_Tree_Wrapper' - (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); - - Next_Component_Or_Discriminant (Elem); - end loop; - - -- Now we set the right field to Read_Only. 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 := - Glb (Read_Only, Child_Perm); - - 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. - - when N_Indexed_Component - | N_Slice - => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); - - begin - if C = null then - -- We went through a function call, do nothing - - 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 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))); - - 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)); - - -- We change the current node from Entire_Object - -- to Array_Component with same permission and the - -- previously defined son. - - C.all.Tree := (Kind => Array_Component, - Is_Node_Deep => Is_Node_Deep (C), - Permission => Child_Perm, - Get_Elem => Son); - - return Get_Elem (C); - 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. - - when N_Explicit_Dereference => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes_Observe (Prefix (N)); - - begin - if C = null then - -- We went through a function call, do nothing - - return null; - end if; - - 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))); - - 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)); - - -- We change the current node from Entire_Object to - -- Reference with Write_Only 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, - Get_All => Son); - - return Get_All (C); - end; - else - raise Program_Error; - end if; - end; - - when N_Function_Call => - return null; - - 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); @@ -6080,7 +4401,7 @@ if Ekind (E) = E_Abstract_State then null; else - Setup_Parameter_Or_Global (E, Kind); + Setup_Parameter_Or_Global (E, Kind, Global_Var => True); end if; Next_Global (Item); end loop; @@ -6095,12 +4416,17 @@ 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; @@ -6126,46 +4452,81 @@ ------------------------------- procedure Setup_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind) + (Id : Entity_Id; + Mode : Formal_Kind; + Global_Var : Boolean) is - Elem : Perm_Tree_Access; + Elem : Perm_Tree_Access; + View_Typ : Entity_Id; begin + if Present (Full_View (Etype (Id))) then + View_Typ := Full_View (Etype (Id)); + else + View_Typ := Etype (Id); + end if; + Elem := new Perm_Tree_Wrapper' (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 + + -- 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. + + -- In the following we deal with in parameters that can be observed. + -- We only consider the observing cases. + when E_In_Parameter => - -- Borrowed IN: RW for everybody - - if Is_Borrowed_In (Id) then - Elem.all.Tree.Permission := Read_Write; - Elem.all.Tree.Children_Permission := Read_Write; - - -- Observed IN: R for everybody + -- Handling global variables as IN parameters here. + -- Remove the following condition once it's decided how globals + -- should be considered. ??? + -- + -- In SPARK, IN access-to-variable is an observe operation for + -- a function, and a borrow operation for a procedure. + + if not Global_Var then + if (Is_Access_Type (View_Typ) + and then Is_Access_Constant (View_Typ) + and then Is_Anonymous_Access_Type (View_Typ)) + or else + (Is_Access_Type (View_Typ) + and then Ekind (Scope (Id)) = E_Function) + or else + (not Is_Access_Type (View_Typ) + and then Is_Deep (View_Typ) + and then not Is_Anonymous_Access_Type (View_Typ)) + then + Elem.all.Tree.Permission := Observed; + Elem.all.Tree.Children_Permission := Observed; + + else + Elem.all.Tree.Permission := Unrestricted; + Elem.all.Tree.Children_Permission := Unrestricted; + end if; else - Elem.all.Tree.Permission := Read_Only; - Elem.all.Tree.Children_Permission := Read_Only; + Elem.all.Tree.Permission := Observed; + Elem.all.Tree.Children_Permission := Observed; end if; - -- OUT: borrow, but callee has W only - - when E_Out_Parameter => - Elem.all.Tree.Permission := Write_Only; - Elem.all.Tree.Children_Permission := Write_Only; - - -- IN OUT: borrow and callee has RW - - when E_In_Out_Parameter => - Elem.all.Tree.Permission := Read_Write; - Elem.all.Tree.Children_Permission := Read_Write; + -- 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 others => + Elem.all.Tree.Permission := Unrestricted; + Elem.all.Tree.Children_Permission := Unrestricted; end case; Set (Current_Perm_Env, Id, Elem); @@ -6175,15 +4536,95 @@ -- 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 - Setup_Parameter_Or_Global (Formal, Ekind (Formal)); + Setup_Parameter_Or_Global + (Formal, Ekind (Formal), Global_Var => False); Next_Formal (Formal); 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;