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;
-- 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
-- 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
-- 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
--------------------
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
-- 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;
function Component
(T : Perm_Tree_Access)
- return Perm_Tree_Maps.Instance
+ return Perm_Tree_Maps.Instance
is
begin
return T.all.Tree.Component;
-- 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);
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;
-- 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 =>
-- 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;
------------------------------
-- 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);
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);
-- 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;
-- 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;
-- 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;
-- 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;
function Other_Components
(T : Perm_Tree_Access)
- return Perm_Tree_Access
+ return Perm_Tree_Access
is
begin
return T.all.Tree.Other_Components;
-- 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;
-- 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;
-- Default mode. Checks that paths have Read_Perm permission.
Move,
- -- Regular moving semantics (not under 'Access). Checks that paths have
- -- Read_Write permission. After moving a path, its permission is set to
- -- Write_Only and the permission of its extensions is set to No_Access.
+ -- Regular moving semantics. Checks that paths have
+ -- Unrestricted permission. After moving a path, its permission is set
+ -- to Unrestricted and the permission of its extensions is set
+ -- to Unrestricted.
Assign,
-- Used for the target of an assignment, or an actual parameter with
- -- mode OUT. Checks that paths have Write_Perm permission. After
- -- assigning to a path, its permission is set to Read_Write.
-
- Super_Move,
- -- Enhanced moving semantics (under 'Access). Checks that paths have
- -- Read_Write permission (shallow types may have only Write permission).
- -- After moving a path, its permission is set to No_Access, as well as
- -- the permission of its extensions and the permission of its prefixes
- -- up to the first Reference node.
-
- Borrow_Out,
- -- Used for actual OUT parameters. Checks that paths have Write_Perm
- -- permission. After checking a path, its permission is set to Read_Only
- -- when of a by-copy type, to No_Access otherwise. After the call, its
- -- permission is set to Read_Write.
+ -- mode OUT. Checks that paths have Unrestricted permission. After
+ -- assigning to a path, its permission is set to Unrestricted.
+
+ Borrow,
+ -- Used for the source of an assignement when initializes a stand alone
+ -- object of anonymous type, constant, or IN parameter and also OUT
+ -- or IN OUT composite object.
+ -- In the borrowed state, the access object is completely "dead".
Observe
-- Used for actual IN parameters of a scalar type. Checks that paths
-- have Read_Perm permission. After checking a path, its permission
- -- is set to Read_Only.
+ -- is set to Observed.
--
-- Also used for formal IN parameters
+
);
type Result_Kind is (Folded, Unfolded, Function_Call);
-- 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.
-- 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
procedure Check_Package_Body (Pack : Node_Id);
- procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
- -- This procedure takes a formal and an actual parameter and calls the
- -- analyze node if the parameter is borrowed with mode in out, with the
- -- appropriate Checking_Mode (Move).
-
- procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id);
- -- This procedure takes a formal and an actual parameter and calls
- -- the analyze node if the parameter is observed, with the appropriate
- -- Checking_Mode.
-
- procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id);
- -- This procedure takes a formal and an actual parameter and calls the
- -- analyze node if the parameter is of mode out, with the appropriate
- -- Checking_Mode.
+ procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id);
+ -- This procedure takes a formal and an actual parameter and checks the
+ -- permission of every in-mode parameter. This includes Observing and
+ -- Borrowing.
- procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id);
+ procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
-- This procedure takes a formal and an actual parameter and checks the
- -- readability of every in-mode parameter. This includes observed in, and
- -- also borrowed in, that are then checked afterwards.
+ -- state of every out-mode and in out-mode parameter. This includes
+ -- Moving and Borrowing.
procedure Check_Statement (Stmt : Node_Id);
-- 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.
-- 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
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);
-- of the subprogram indeed have RW permission at the end of the subprogram
-- execution.
- procedure Return_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id;
- Global_Var : Boolean);
- -- Auxiliary procedure to Return_Parameters and Return_Globals
-
- procedure Return_Parameters (Subp : Entity_Id);
- -- Takes a subprogram as input, and checks that all borrowed parameters of
- -- the subprogram indeed have RW permission at the end of the subprogram
- -- execution.
+ procedure Return_The_Global
+ (Id : Entity_Id;
+ Mode : Formal_Kind;
+ Subp : Entity_Id);
+ -- Auxiliary procedure to Return_Globals
+ -- There is no need to return parameters because they will be reassigned
+ -- their state once the subprogram returns. Local variables that have
+ -- borrowed, observed, or moved an actual parameter go out of the scope.
procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
-- This procedure takes an access to a permission tree and modifies the
-- tree so that any strict extensions of the given tree become of the
-- access specified by parameter P.
- procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id);
- -- Set permissions to
- -- No for any extension with more .all
- -- W for any deep extension with same number of .all
- -- RW for any shallow extension with same number of .all
-
- function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access;
- -- This function takes a name as an input and sets in the permission
- -- tree the given permission to the given name. The general rule here is
- -- that everybody updates the permission of the subtree it is returning.
- -- The permission of the assigned path has been set to RW by the caller.
- --
- -- Case where we have to normalize a tree after the correct permissions
- -- have been assigned already. We look for the right subtree at the given
- -- path, actualize its permissions, and then call the normalization on its
- -- parent.
- --
- -- Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will
- -- change the permission of x to RW because all of its components have
- -- permission have permission RW.
-
- function Set_Perm_Prefixes_Borrow_Out (N : Node_Id) return Perm_Tree_Access;
+ function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
-- This function modifies the permissions of a given node_id in the
-- permission environment as well as in all the prefixes of the path,
-- given that the path is borrowed with mode out.
- function Set_Perm_Prefixes_Move
- (N : Node_Id; Mode : Checking_Mode)
+ function Set_Perm_Prefixes
+ (N : Node_Id;
+ New_Perm : Perm_Kind)
return Perm_Tree_Access;
- pragma Precondition (Mode = Move or Mode = Super_Move);
- -- Given a node and a mode (that can be either Move or Super_Move), this
- -- function modifies the permissions of a given node_id in the permission
- -- environment as well as all the prefixes of the path, given that the path
- -- is moved with or without 'Access. The general rule here is everybody
- -- updates the permission of the subtree they are returning.
- --
- -- This case describes a move either under 'Access or without 'Access.
-
- function Set_Perm_Prefixes_Observe (N : Node_Id) return Perm_Tree_Access;
- -- This function modifies the permissions of a given node_id in the
- -- permission environment as well as all the prefixes of the path,
- -- given that the path is observed.
+ -- This function sets the permissions of a given node_id in the
+ -- permission environment as well as in all the prefixes of the path
+ -- to the one given in parameter (P).
procedure Setup_Globals (Subp : Entity_Id);
-- Takes a subprogram as input, and sets up the environment by adding
-- 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 --
----------------------
-- 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 --
--------------------------
procedure Check_Call_Statement (Call : Node_Id) is
Saved_Env : Perm_Env;
- procedure Iterate_Call is new
- Iterate_Call_Parameters (Check_Param);
- procedure Iterate_Call_Observes is new
- Iterate_Call_Parameters (Check_Param_Observes);
- procedure Iterate_Call_Outs is new
- Iterate_Call_Parameters (Check_Param_Outs);
- procedure Iterate_Call_Read is new
- Iterate_Call_Parameters (Check_Param_Read);
+ procedure Iterate_Call_In is new
+ Iterate_Call_Parameters (Check_Param_In);
+ procedure Iterate_Call_Out is new
+ Iterate_Call_Parameters (Check_Param_Out);
begin
-- Save environment, so that the modifications done by analyzing the
-- parameters are not kept at the end of the call.
- Copy_Env (Current_Perm_Env,
- Saved_Env);
-
- -- We first check the Read access on every in parameter
- Current_Checking_Mode := Read;
- Iterate_Call_Read (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global), Read);
-
- -- We first observe, then borrow with mode out, and then with other
- -- modes. This ensures that we do not have to check for by-copy types
- -- specially, because we read them before borrowing them.
-
- Iterate_Call_Observes (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global),
- Observe);
+ Copy_Env (Current_Perm_Env, Saved_Env);
- Iterate_Call_Outs (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global),
- Borrow_Out);
+ -- We first check the globals then parameters to handle the
+ -- No_Parameter_Aliasing Restriction. An out or in-out global is
+ -- considered as borrowing while a parameter with the same mode is
+ -- a move. This order disallow passing a part of a variable to a
+ -- subprogram if it is referenced as a global by the callable (when
+ -- writable).
+ -- For paremeters, we fisrt check in parameters and then the out ones.
+ -- This is to avoid Observing or Borrowing objects that are already
+ -- moved. This order is not mandatory but allows to catch runtime
+ -- errors like null pointer dereferencement at the analysis time.
- Iterate_Call (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global), Move);
+ Current_Checking_Mode := Read;
+ Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
+ Iterate_Call_In (Call);
+ Iterate_Call_Out (Call);
-- Restore environment, because after borrowing/observing actual
-- parameters, they get their permission reverted to the ones before
-- the call.
Free_Env (Current_Perm_Env);
-
- Copy_Env (Saved_Env,
- Current_Perm_Env);
-
+ Copy_Env (Saved_Env, Current_Perm_Env);
Free_Env (Saved_Env);
-
- -- We assign the out parameters (necessarily borrowed per RM)
- Current_Checking_Mode := Assign;
- Iterate_Call (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global),
- Assign);
-
end Check_Call_Statement;
-------------------------
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
-- 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
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
-----------------------
procedure Check_Declaration (Decl : Node_Id) is
+
+ Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : Node_Id renames Etype (Target_Ent);
+ Check : Boolean := True;
begin
case N_Declaration'(Nkind (Decl)) is
when N_Full_Type_Declaration =>
+ if not Has_Ownership_Aspect_True (Target_Ent, "type declaration")
+ then
+ Check := False;
+ end if;
- -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
-
- null;
+ -- ??? What about component declarations with defaults.
when N_Object_Declaration =>
+ if (Is_Access_Type (Target_Typ)
+ or else Is_Deep (Target_Typ))
+ and then not Has_Ownership_Aspect_True
+ (Target_Ent, "Object declaration ")
+ then
+ Check := False;
+ end if;
+
+ if Is_Anonymous_Access_Type (Target_Typ)
+ and then not Present (Expression (Decl))
+ then
+
+ -- ??? Check the case of default value (AI)
+ -- ??? How an anonymous access type can be with default exp?
+
+ Error_Msg_NE ("? object declaration & has OAF (Anonymous "
+ & "access-to-object with no initialization)",
+ Decl, Target_Ent);
+
+ -- If it it an initialization
+
+ elsif Present (Expression (Decl)) and Check then
+
+ -- Find out the operation to be done on the right-hand side
+
+ -- Initializing object, access type
+
+ if Is_Access_Type (Target_Typ) then
+
+ -- Initializing object, constant access type
+
+ if Is_Constant_Object (Target_Ent) then
+
+ -- Initializing object, constant access to variable type
+
+ if not Is_Access_Constant (Target_Typ) then
+ Current_Checking_Mode := Borrow;
+
+ -- Initializing object, constant access to constant type
+
+ -- Initializing object,
+ -- constant access to constant anonymous type.
+
+ elsif Is_Anonymous_Access_Type (Target_Typ) then
+
+ -- This is an object declaration so the target
+ -- of the assignement is a stand-alone object.
+
+ Current_Checking_Mode := Observe;
+
+ -- Initializing object, constant access to constant
+ -- named type.
+
+ else
+ -- If named then it is a general access type
+ -- Hence, Has_Ownership_Aspec_True is False.
+
+ raise Program_Error;
+ end if;
+
+ -- Initializing object, variable access type
+
+ else
+ -- Initializing object, variable access to variable type
- -- First move the right-hand side
+ if not Is_Access_Constant (Target_Typ) then
- Current_Checking_Mode := Move;
- Check_Node (Expression (Decl));
+ -- Initializing object, variable named access to
+ -- variable type.
+
+ if not Is_Anonymous_Access_Type (Target_Typ) then
+ Current_Checking_Mode := Move;
+
+ -- Initializing object, variable anonymous access to
+ -- variable type.
+
+ else
+ -- This is an object declaration so the target
+ -- object of the assignement is a stand-alone
+ -- object.
+
+ Current_Checking_Mode := Borrow;
+ end if;
+
+ -- Initializing object, variable access to constant type
+
+ else
+ -- Initializing object,
+ -- variable named access to constant type.
+
+ if not Is_Anonymous_Access_Type (Target_Typ) then
+ Error_Msg_N ("assignment not allowed, Ownership "
+ & "Aspect False (Anonymous Access "
+ & "Object)", Decl);
+ Check := False;
+
+ -- Initializing object,
+ -- variable anonymous access to constant type.
+
+ else
+ -- This is an object declaration so the target
+ -- of the assignement is a stand-alone object.
+
+ Current_Checking_Mode := Observe;
+ end if;
+ end if;
+ end if;
+
+ -- Initializing object, composite (deep) type
+
+ elsif Is_Deep (Target_Typ) then
+
+ -- Initializing object, constant composite type
+
+ if Is_Constant_Object (Target_Ent) then
+ Current_Checking_Mode := Observe;
+
+ -- Initializing object, variable composite type
+
+ else
+
+ -- Initializing object, variable anonymous composite type
+
+ if Nkind (Object_Definition (Decl)) =
+ N_Constrained_Array_Definition
+
+ -- An N_Constrained_Array_Definition is an anonymous
+ -- array (to be checked). Record types are always
+ -- named and are considered in the else part.
+
+ then
+ declare
+ Com_Ty : constant Node_Id :=
+ Component_Type (Etype (Target_Typ));
+ begin
+
+ if Is_Access_Type (Com_Ty) then
+
+ -- If components are of anonymous type
+
+ if Is_Anonymous_Access_Type (Com_Ty) then
+ if Is_Access_Constant (Com_Ty) then
+ Current_Checking_Mode := Observe;
+
+ else
+ Current_Checking_Mode := Borrow;
+ end if;
+
+ else
+ Current_Checking_Mode := Move;
+ end if;
+
+ elsif Is_Deep (Com_Ty) then
+
+ -- This is certainly named so it is a move
+
+ Current_Checking_Mode := Move;
+ end if;
+ end;
+
+ else
+ Current_Checking_Mode := Move;
+ end if;
+ end if;
+
+ elsif Nkind_In (Expression (Decl),
+ N_Attribute_Reference,
+ N_Attribute_Reference,
+ N_Expanded_Name,
+ N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Reference,
+ N_Selected_Component,
+ N_Slice)
+ then
+ if Is_Access_Type (Etype (Prefix (Expression (Decl))))
+ or else Is_Deep (Etype (Prefix (Expression (Decl))))
+ then
+ Current_Checking_Mode := Observe;
+ Check := True;
+ end if;
+ end if;
+ end if;
+
+ if Check then
+ Check_Node (Expression (Decl));
+ end if;
+
+ -- If lhs is not a pointer, we still give it the appropriate
+ -- state which is useless but not harmful.
declare
- Deep : constant Boolean :=
- Is_Deep (Etype (Defining_Identifier (Decl)));
Elem : Perm_Tree_Access;
+ Deep : constant Boolean := Is_Deep (Target_Typ);
begin
- Elem := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Deep,
- Permission => Read_Write,
- Children_Permission => Read_Write));
-
- -- If unitialized declaration, then set to Write_Only. If a
- -- pointer declaration, it has a null default initialization.
-
- if No (Expression (Decl))
- and then not Has_Full_Default_Initialization
- (Etype (Defining_Identifier (Decl)))
- and then not Is_Access_Type
- (Etype (Defining_Identifier (Decl)))
-
- -- Objects of shallow types are considered as always
- -- initialized, leaving the checking of initialization to
- -- flow analysis.
-
- and then Deep
- then
- Elem.all.Tree.Permission := Write_Only;
- Elem.all.Tree.Children_Permission := Write_Only;
+ -- Note that all declared variables are set to the unrestricted
+ -- state.
+ --
+ -- If variables are not initialized:
+ -- unrestricted to every declared object.
+ -- Exp:
+ -- R : Rec
+ -- S : Rec := (...)
+ -- R := S
+ -- The assignement R := S is not allowed in the new rules
+ -- if R is not unrestricted.
+ --
+ -- If variables are initialized:
+ -- If it is a move, then the target is unrestricted
+ -- If it is a borrow, then the target is unrestricted
+ -- If it is an observe, then the target should be observed
+
+ if Current_Checking_Mode = Observe then
+ Elem := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Deep,
+ Permission => Observed,
+ Children_Permission => Observed));
+ else
+ Elem := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Deep,
+ Permission => Unrestricted,
+ Children_Permission => Unrestricted));
end if;
-- Create new tree for defining identifier
Set (Current_Perm_Env,
Unique_Entity (Defining_Identifier (Decl)),
Elem);
-
pragma Assert (Get_First (Current_Perm_Env) /= null);
end;
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;
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));
| N_Op_Not
| N_Op_Plus
=>
- pragma Assert (Is_Shallow (Etype (Expr)));
Current_Checking_Mode := Read;
Check_Node (Right_Opnd (Expr));
when N_Attribute_Reference =>
case Attribute_Name (Expr) is
when Name_Access =>
- case Current_Checking_Mode is
- when Read =>
- Check_Node (Prefix (Expr));
-
- when Move =>
- Current_Checking_Mode := Super_Move;
- Check_Node (Prefix (Expr));
-
- -- Only assign names, not expressions
-
- when Assign =>
- raise Program_Error;
-
- -- Prefix in Super_Move should be a name, error here
-
- when Super_Move =>
- raise Program_Error;
-
- -- Could only borrow names of mode out, not n'Access
-
- when Borrow_Out =>
- raise Program_Error;
-
- when Observe =>
- Check_Node (Prefix (Expr));
- end case;
+ Error_Msg_N ("access attribute not allowed in SPARK", Expr);
when Name_Last
| Name_First
Check_Node (Prefix (Expr));
when Name_Pred
- | Name_Succ
+ | Name_Succ
=>
Check_List (Expressions (Expr));
Check_Node (Prefix (Expr));
-- 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;
| Name_Val
=>
null;
-
-- Other attributes that fall out of the scope of the analysis
when others =>
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);
-- 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.
-- 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.
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;
when N_Quantified_Expression =>
declare
Saved_Env : Perm_Env;
+
begin
Copy_Env (Current_Perm_Env, Saved_Env);
Current_Checking_Mode := Read;
Copy_Env (Saved_Env, Current_Perm_Env);
Free_Env (Saved_Env);
end;
-
-- Analyze the list of associations in the aggregate
when N_Aggregate =>
-- 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.
Check_Node (Elmt);
Next (Elmt);
-
- Copy_Env (Current_Perm_Env,
- New_Env);
-
+ Copy_Env (Current_Perm_Env, New_Env);
Free_Env (Current_Perm_Env);
-- Other alternatives
while Present (Elmt) loop
- -- Restore environment
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ -- Restore environment
+ Copy_Env (Saved_Env, Current_Perm_Env);
Check_Node (Elmt);
-
- -- Merge Current_Perm_Env into New_Env
-
- Merge_Envs (New_Env,
- Current_Perm_Env);
-
Next (Elmt);
end loop;
-
-- CLEANUP
- Copy_Env (New_Env,
- Current_Perm_Env);
+ Copy_Env (Saved_Env, Current_Perm_Env);
Free_Env (New_Env);
Free_Env (Saved_Env);
end;
-
-- Analyze the list of associates in the aggregate as well as the
-- ancestor part.
when N_Extension_Aggregate =>
-
Check_Node (Ancestor_Part (Expr));
Check_List (Expressions (Expr));
| N_Raise_xxx_Error
=>
null;
-
-- The following nodes are never generated in GNATprove mode
when N_Expression_With_Actions
| N_Unchecked_Expression
=>
raise Program_Error;
-
end case;
end Check_Expression;
-- Check_Globals --
-------------------
- procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
+ procedure Check_Globals (N : Node_Id) is
begin
if Nkind (N) = N_Empty then
return;
end if;
declare
- pragma Assert
- (List_Length (Pragma_Argument_Associations (N)) = 1);
-
- PAA : constant Node_Id :=
- First (Pragma_Argument_Associations (N));
+ pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
+ PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
-
Row : Node_Id;
The_Mode : Name_Id;
RHS : Node_Id;
- procedure Process (Mode : Name_Id;
- The_Global : Entity_Id);
-
- procedure Process (Mode : Name_Id;
- The_Global : Node_Id)
- is
- Ident_Elt : constant Entity_Id :=
+ procedure Process (Mode : Name_Id; The_Global : Entity_Id);
+ procedure Process (Mode : Name_Id; The_Global : Node_Id) is
+ Ident_Elt : constant Entity_Id :=
Unique_Entity (Entity (The_Global));
-
Mode_Before : constant Checking_Mode := Current_Checking_Mode;
begin
if Ekind (Ident_Elt) = E_Abstract_State then
return;
end if;
+ case Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ Current_Checking_Mode := Observe;
+ Check_Node (The_Global);
- case Check_Mode is
- when Read =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- Check_Node (The_Global);
+ when Name_Output
+ | Name_In_Out
+ =>
+ -- ??? Borrow not Move?
+ Current_Checking_Mode := Borrow;
+ Check_Node (The_Global);
- when Name_Output
- | Name_In_Out
- =>
- null;
+ when others =>
+ raise Program_Error;
+ end case;
+ Current_Checking_Mode := Mode_Before;
+ end Process;
- when others =>
- raise Program_Error;
+ begin
+ if Nkind (Expression (PAA)) = N_Null then
- end case;
-
- when Observe =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- if not Is_Borrowed_In (Ident_Elt) then
- -- Observed in
-
- Current_Checking_Mode := Observe;
- Check_Node (The_Global);
- end if;
-
- when others =>
- null;
-
- end case;
-
- when Borrow_Out =>
-
- case Mode is
- when Name_Output =>
- -- Borrowed out
- Current_Checking_Mode := Borrow_Out;
- Check_Node (The_Global);
-
- when others =>
- null;
-
- end case;
-
- when Move =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- if Is_Borrowed_In (Ident_Elt) then
- -- Borrowed in
-
- Current_Checking_Mode := Move;
- else
- -- Observed
-
- return;
- end if;
-
- when Name_Output =>
- return;
-
- when Name_In_Out =>
- -- Borrowed in out
-
- Current_Checking_Mode := Move;
-
- when others =>
- raise Program_Error;
- end case;
-
- Check_Node (The_Global);
- when Assign =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- null;
-
- when Name_Output
- | Name_In_Out
- =>
- -- Borrowed out or in out
-
- Process_Path (The_Global);
-
- when others =>
- raise Program_Error;
- end case;
-
- when others =>
- raise Program_Error;
- end case;
-
- Current_Checking_Mode := Mode_Before;
- end Process;
-
- begin
- if Nkind (Expression (PAA)) = N_Null then
-- global => null
-- No globals, nothing to do
+
return;
elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
+
-- global => foo
-- A single input
+
Process (Name_Input, Expression (PAA));
elsif Nkind (Expression (PAA)) = N_Aggregate
then
-- global => (foo, bar)
-- Inputs
+
RHS := First (Expressions (Expression (PAA)));
while Present (RHS) loop
case Nkind (RHS) is
when others =>
raise Program_Error;
-
end case;
RHS := Next (RHS);
end loop;
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));
when others =>
Process (The_Mode, RHS);
-
end case;
RHS := Next (RHS);
end loop;
when others =>
raise Program_Error;
-
end case;
-
Row := Next (Row);
end loop;
end;
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));
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);
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
when N_Package_Declaration =>
declare
Spec : constant Node_Id := Specification (N);
+
begin
Current_Checking_Mode := Read;
Check_List (Visible_Declarations (Spec));
| N_Delay_Alternative
| N_Derived_Type_Definition
| N_Designator
- | N_Discriminant_Association
| N_Discriminant_Specification
| N_Elsif_Part
| N_Entry_Body_Formal_Part
| 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
-- 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));
-- declaration) from environment.
Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ Copy_Env (Saved_Env, Current_Perm_Env);
end Check_Package_Body;
- -----------------
- -- Check_Param --
- -----------------
+ --------------------
+ -- Check_Param_In --
+ --------------------
- procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
+ procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
Mode : constant Entity_Kind := Ekind (Formal);
Mode_Before : constant Checking_Mode := Current_Checking_Mode;
-
begin
- case Current_Checking_Mode is
- when Read =>
- case Formal_Kind'(Mode) is
- when E_In_Parameter =>
- if Is_Borrowed_In (Formal) then
- -- Borrowed in
-
- Current_Checking_Mode := Move;
- else
- -- Observed
+ case Formal_Kind'(Mode) is
- return;
- end if;
+ -- Formal IN parameter
- when E_Out_Parameter =>
- return;
+ when E_In_Parameter =>
- when E_In_Out_Parameter =>
- -- Borrowed in out
+ -- Formal IN parameter, access type
- Current_Checking_Mode := Move;
+ if Is_Access_Type (Etype (Formal)) then
- end case;
+ -- Formal IN parameter, access to variable type
- Check_Node (Actual);
+ if not Is_Access_Constant (Etype (Formal)) then
- when Assign =>
- case Formal_Kind'(Mode) is
- when E_In_Parameter =>
- null;
+ -- Formal IN parameter, named/anonymous access to variable
+ -- type.
- when E_Out_Parameter
- | E_In_Out_Parameter
- =>
- -- Borrowed out or in out
+ Current_Checking_Mode := Borrow;
+ Check_Node (Actual);
- Process_Path (Actual);
+ -- Formal IN parameter, access to constant type
+ -- Formal IN parameter, access to named constant type
- end case;
+ elsif not Is_Anonymous_Access_Type (Etype (Formal)) then
+ Error_Msg_N ("assignment not allowed, Ownership Aspect"
+ & " False (Named general access type)",
+ Formal);
- when others =>
- raise Program_Error;
+ -- Formal IN parameter, access to anonymous constant type
- end case;
- Current_Checking_Mode := Mode_Before;
- end Check_Param;
+ else
+ Current_Checking_Mode := Observe;
+ Check_Node (Actual);
+ end if;
- --------------------------
- -- Check_Param_Observes --
- --------------------------
+ -- Formal IN parameter, composite type
- procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ elsif Is_Deep (Etype (Formal)) then
- begin
- case Mode is
- when E_In_Parameter =>
- if not Is_Borrowed_In (Formal) then
- -- Observed in
+ -- Composite formal types should be named
+ -- Formal IN parameter, composite named type
Current_Checking_Mode := Observe;
Check_Node (Actual);
end if;
- when others =>
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
null;
-
end case;
Current_Checking_Mode := Mode_Before;
- end Check_Param_Observes;
+ end Check_Param_In;
----------------------
- -- Check_Param_Outs --
+ -- Check_Param_Out --
----------------------
- procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
+ procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
Mode_Before : constant Checking_Mode := Current_Checking_Mode;
begin
+ case Formal_Kind'(Mode) is
- case Mode is
- when E_Out_Parameter =>
- -- Borrowed out
- Current_Checking_Mode := Borrow_Out;
- Check_Node (Actual);
+ -- Formal OUT/IN OUT parameter
- when others =>
- null;
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
- end case;
+ -- Formal OUT/IN OUT parameter, access type
- Current_Checking_Mode := Mode_Before;
- end Check_Param_Outs;
+ if Is_Access_Type (Etype (Formal)) then
- ----------------------
- -- Check_Param_Read --
- ----------------------
+ -- Formal OUT/IN OUT parameter, access to variable type
- procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
+ if not Is_Access_Constant (Etype (Formal)) then
- begin
- pragma Assert (Current_Checking_Mode = Read);
+ -- Cannot have anonymous out access parameter
+ -- Formal out/in out parameter, access to named variable
+ -- type.
- case Formal_Kind'(Mode) is
- when E_In_Parameter =>
- Check_Node (Actual);
+ Current_Checking_Mode := Move;
+ Check_Node (Actual);
- when E_Out_Parameter
- | E_In_Out_Parameter
- =>
- null;
+ -- Formal out/in out parameter, access to constant type
+
+ else
+ Error_Msg_N ("assignment not allowed, Ownership Aspect False"
+ & " (Named general access type)", Formal);
+
+ end if;
+
+ -- Formal out/in out parameter, composite type
+
+ elsif Is_Deep (Etype (Formal)) then
+
+ -- Composite formal types should be named
+ -- Formal out/in out Parameter, Composite Named type.
+ Current_Checking_Mode := Borrow;
+ Check_Node (Actual);
+ end if;
+
+ when E_In_Parameter =>
+ null;
end case;
- end Check_Param_Read;
+
+ Current_Checking_Mode := Mode_Before;
+ end Check_Param_Out;
-------------------------
-- Check_Safe_Pointers --
-- 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));
procedure Check_Statement (Stmt : Node_Id) is
Mode_Before : constant Checking_Mode := Current_Checking_Mode;
- begin
- case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
- when N_Entry_Call_Statement =>
- Check_Call_Statement (Stmt);
-
- -- Move right-hand side first, and then assign left-hand side
+ State_N : Perm_Kind;
+ Check : Boolean := True;
+ St_Name : Node_Id;
+ Ty_St_Name : Node_Id;
- when N_Assignment_Statement =>
- if Is_Deep (Etype (Expression (Stmt))) then
- Current_Checking_Mode := Move;
- else
- Current_Checking_Mode := Read;
- end if;
+ function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
+ -- Return the root of the name given as input
- Check_Node (Expression (Stmt));
- Current_Checking_Mode := Assign;
- Check_Node (Name (Stmt));
+ function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
+ begin
+ case Nkind (Comp_Stmt) is
+ when N_Identifier
+ | N_Expanded_Name
+ => return Comp_Stmt;
- when N_Block_Statement =>
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Get_Root (Expression (Comp_Stmt));
+
+ when N_Parameter_Specification =>
+ return Get_Root (Defining_Identifier (Comp_Stmt));
+
+ when N_Selected_Component
+ | N_Indexed_Component
+ | N_Slice
+ | N_Explicit_Dereference
+ =>
+ return Get_Root (Prefix (Comp_Stmt));
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Root;
+
+ begin
+ case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
+ when N_Entry_Call_Statement =>
+ Check_Call_Statement (Stmt);
+
+ -- Move right-hand side first, and then assign left-hand side
+
+ when N_Assignment_Statement =>
+
+ St_Name := Name (Stmt);
+ Ty_St_Name := Etype (Name (Stmt));
+
+ -- Check that is not a *general* access type
+
+ if Has_Ownership_Aspect_True (St_Name, "assigning to") then
+
+ -- Assigning to access type
+
+ if Is_Access_Type (Ty_St_Name) then
+
+ -- Assigning to access to variable type
+
+ if not Is_Access_Constant (Ty_St_Name) then
+
+ -- Assigning to named access to variable type
+
+ if not Is_Anonymous_Access_Type (Ty_St_Name) then
+ Current_Checking_Mode := Move;
+
+ -- Assigning to anonymous access to variable type
+
+ else
+ -- Target /= source root
+
+ if Nkind_In (Expression (Stmt), N_Allocator, N_Null)
+ or else St_Name /= Get_Root (Expression (Stmt))
+ then
+ Error_Msg_N ("assignment not allowed, anonymous "
+ & "access Object with Different Root",
+ Stmt);
+ Check := False;
+
+ -- Target = source root
+
+ else
+ -- Here we do nothing on the source nor on the
+ -- target. However, we check the the legality rule:
+ -- "The source shall be an owning access object
+ -- denoted by a name that is not in the observed
+ -- state".
+
+ State_N := Get_Perm (Expression (Stmt));
+ if State_N = Observed then
+ Error_Msg_N ("assignment not allowed, Anonymous "
+ & "access object with the same root"
+ & " but source Observed", Stmt);
+ Check := False;
+ end if;
+ end if;
+ end if;
+
+ -- else access-to-constant
+
+ -- Assigning to anonymous access-to-constant type
+
+ elsif Is_Anonymous_Access_Type (Ty_St_Name) then
+
+ -- ??? Check the follwing condition. We may have to
+ -- add that the root is in the observed state too.
+
+ State_N := Get_Perm (Expression (Stmt));
+ if State_N /= Observed then
+ Error_Msg_N ("assignment not allowed, anonymous "
+ & "access-to-constant object not in "
+ & "the observed state)", Stmt);
+ Check := False;
+
+ else
+ Error_Msg_N ("?here check accessibility level cited in"
+ & " the second legality rule of assign",
+ Stmt);
+ Check := False;
+ end if;
+
+ -- Assigning to named access-to-constant type:
+ -- This case should have been detected when checking
+ -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
+
+ else
+ raise Program_Error;
+ end if;
+
+ -- Assigning to composite (deep) type.
+
+ elsif Is_Deep (Ty_St_Name) then
+ if Ekind (Ty_St_Name) = E_Record_Type then
+ declare
+ Elmt : Entity_Id :=
+ First_Component_Or_Discriminant (Ty_St_Name);
+
+ begin
+ while Present (Elmt) loop
+ if Is_Anonymous_Access_Type (Etype (Elmt)) or
+ Ekind (Elmt) = E_General_Access_Type
+ then
+ Error_Msg_N ("assignment not allowed, Ownership "
+ & "Aspect False (Components have "
+ & "Ownership Aspect False)", Stmt);
+ Check := False;
+ exit;
+ end if;
+
+ Next_Component_Or_Discriminant (Elmt);
+ end loop;
+ end;
+
+ -- Record types are always named so this is a move
+
+ if Check then
+ Current_Checking_Mode := Move;
+ end if;
+ end if;
+
+ -- Now handle legality rules of using a borrowed, observed,
+ -- or moved name as a prefix in an assignment.
+
+ else
+ if Nkind_In (St_Name,
+ N_Attribute_Reference,
+ N_Expanded_Name,
+ N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Reference,
+ N_Selected_Component,
+ N_Slice)
+ then
+
+ if Is_Access_Type (Etype (Prefix (St_Name))) or
+ Is_Deep (Etype (Prefix (St_Name)))
+ then
+
+ -- We set the Check variable to True so that we can
+ -- Check_Node of the expression and the name first
+ -- under the assumption of Current_Checking_Mode =
+ -- Read => nothing to be done for the RHS if the
+ -- following check on the expression fails, and
+ -- Current_Checking_Mode := Assign => the name should
+ -- not be borrowed or observed so that we can use it
+ -- as a prefix in the target of an assignement.
+ --
+ -- Note that we do not need to check the OA here
+ -- because we are allowed to read and write "through"
+ -- an object of OAF (example: traversing a DS).
+
+ Check := True;
+ end if;
+ end if;
+
+ if Nkind_In (Expression (Stmt),
+ N_Attribute_Reference,
+ N_Expanded_Name,
+ N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Reference,
+ N_Selected_Component,
+ N_Slice)
+ then
+
+ if Is_Access_Type (Etype (Prefix (Expression (Stmt))))
+ or else Is_Deep (Etype (Prefix (Expression (Stmt))))
+ then
+ Current_Checking_Mode := Observe;
+ Check := True;
+ end if;
+ end if;
+ end if;
+
+ if Check then
+ Check_Node (Expression (Stmt));
+ Current_Checking_Mode := Assign;
+ Check_Node (St_Name);
+ end if;
+ end if;
+
+ when N_Block_Statement =>
declare
Saved_Env : Perm_Env;
-
begin
-- Save environment
- Copy_Env (Current_Perm_Env,
- Saved_Env);
+ Copy_Env (Current_Perm_Env, Saved_Env);
-- Analyze declarations and Handled_Statement_Sequences
-- 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 =>
-- Accumulator for the different branches
New_Env : Perm_Env;
-
Elmt : Node_Id := First (Alternatives (Stmt));
begin
-- 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.
Check_Node (Elmt);
Next (Elmt);
-
- Copy_Env (Current_Perm_Env,
- New_Env);
+ Copy_Env (Current_Perm_Env, New_Env);
Free_Env (Current_Perm_Env);
-- Other alternatives
while Present (Elmt) loop
- -- Restore environment
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ -- Restore environment
+ Copy_Env (Saved_Env, Current_Perm_Env);
Check_Node (Elmt);
-
- -- Merge Current_Perm_Env into New_Env
-
- Merge_Envs (New_Env,
- Current_Perm_Env);
-
Next (Elmt);
end loop;
- -- CLEANUP
- Copy_Env (New_Env,
- Current_Perm_Env);
-
+ Copy_Env (Saved_Env, Current_Perm_Env);
Free_Env (New_Env);
Free_Env (Saved_Env);
end;
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
Subp : constant Entity_Id :=
Return_Applies_To (Return_Statement_Entity (Stmt));
begin
- Return_Parameters (Subp);
Return_Globals (Subp);
end;
when others =>
if Is_Deep (Etype (Expression (Stmt))) then
Current_Checking_Mode := Move;
- elsif Is_Shallow (Etype (Expression (Stmt))) then
- Current_Checking_Mode := Read;
else
- raise Program_Error;
+ Check := False;
end if;
- Check_Node (Expression (Stmt));
+ if Check then
+ Check_Node (Expression (Stmt));
+ end if;
end case;
when N_Extended_Return_Statement =>
Check_List (Return_Object_Declarations (Stmt));
Check_Node (Handled_Statement_Sequence (Stmt));
-
Return_Declarations (Return_Object_Declarations (Stmt));
-
declare
-- ??? This does not take into account the fact that a simple
-- return inside an extended return statement applies to the
-- extended return statement.
Subp : constant Entity_Id :=
Return_Applies_To (Return_Statement_Entity (Stmt));
+
begin
- Return_Parameters (Subp);
Return_Globals (Subp);
end;
- -- Merge the current_Perm_Env with the accumulator for the given loop
+ -- Nothing to do when exiting a loop. No merge needed
when N_Exit_Statement =>
- declare
- Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
-
- Saved_Accumulator : constant Perm_Env_Access :=
- Get (Current_Loops_Accumulators, Loop_Name);
-
- Environment_Copy : constant Perm_Env_Access :=
- new Perm_Env;
- begin
-
- Copy_Env (Current_Perm_Env,
- Environment_Copy.all);
-
- if Saved_Accumulator = null then
- Set (Current_Loops_Accumulators,
- Loop_Name, Environment_Copy);
- else
- Merge_Envs (Saved_Accumulator.all,
- Environment_Copy.all);
- end if;
- end;
+ null;
- -- Copy environment, run on each branch, and then merge
+ -- Copy environment, run on each branch
when N_If_Statement =>
declare
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.
-- THEN PART
Check_List (Then_Statements (Stmt));
-
- Copy_Env (Current_Perm_Env,
- New_Env);
-
+ Copy_Env (Current_Perm_Env, New_Env);
Free_Env (Current_Perm_Env);
-- Here the new_environment contains curr env after then block
-- ELSIF part
+
declare
Elmt : Node_Id;
begin
Elmt := First (Elsif_Parts (Stmt));
while Present (Elmt) loop
- -- Transfer into accumulator, and restore from save
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ -- Transfer into accumulator, and restore from save
+ Copy_Env (Saved_Env, Current_Perm_Env);
Check_Node (Condition (Elmt));
Check_List (Then_Statements (Stmt));
-
- -- Merge Current_Perm_Env into New_Env
-
- Merge_Envs (New_Env,
- Current_Perm_Env);
-
Next (Elmt);
end loop;
end;
-- 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);
-- which means that the association permission is RW.
when Function_Call =>
- return Read_Write;
-
+ return Unrestricted;
end case;
end Get_Perm;
=>
declare
P : constant Entity_Id := Entity (N);
-
C : constant Perm_Tree_Access :=
Get (Current_Perm_Env, Unique_Entity (P));
-- 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;
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
when Unfolded =>
pragma Assert (C.Tree_Access /= null);
-
pragma Assert (Kind (C.Tree_Access) = Entire_Object
or else
Kind (C.Tree_Access) = Record_Component);
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
| 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
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
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
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.
-- 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
=>
declare
P : constant Node_Id := Entity (N);
-
C : constant Perm_Tree_Access :=
Get (Current_Perm_Env, Unique_Entity (P));
-- 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;
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;
or else Kind (C) = Record_Component);
if Kind (C) = Record_Component then
+
-- The tree is unfolded. We just return the subtree.
declare
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
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.
-- We fill the hash table with all sons of the record,
-- with basic Entire_Objects nodes.
+
Elem := First_Component_Or_Discriminant
(Etype (Prefix (N)));
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.
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.
| 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
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.
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.
C := Get_Perm_Tree (Prefix (N));
if C = null then
+
-- If null, we went through a function call
return null;
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.
-- 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 =>
end case;
end Get_Perm_Tree;
- ---------
- -- Glb --
- ---------
+ --------
+ -- Hp --
+ --------
- function Glb (P1, P2 : Perm_Kind) return Perm_Kind
- is
- begin
- case P1 is
- when No_Access =>
- return No_Access;
-
- when Read_Only =>
- case P2 is
- when No_Access
- | Write_Only
- =>
- return No_Access;
+ procedure Hp (P : Perm_Env) is
+ Elem : Perm_Tree_Maps.Key_Option;
- when Read_Perm =>
- return Read_Only;
- end case;
+ begin
+ Elem := Get_First_Key (P);
+ while Elem.Present loop
+ Print_Node_Briefly (Elem.K);
+ Elem := Get_Next_Key (P);
+ end loop;
+ end Hp;
- when Write_Only =>
- case P2 is
- when No_Access
- | Read_Only
- =>
- return No_Access;
+ --------------------------
+ -- Illegal_Global_Usage --
+ --------------------------
- when Write_Perm =>
- return Write_Only;
- end case;
+ procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
+ begin
+ Error_Msg_NE ("cannot use global variable & of deep type", N, N);
+ Error_Msg_N ("\without prior declaration in a Global aspect", N);
+ Errout.Finalize (Last_Call => True);
+ Errout.Output_Messages;
+ Exit_Program (E_Errors);
+ end Illegal_Global_Usage;
- when Read_Write =>
- return P2;
- end case;
- end Glb;
+ -------------
+ -- Is_Deep --
+ -------------
- ---------------
- -- Has_Alias --
- ---------------
+ function Is_Deep (E : Entity_Id) return Boolean is
+ function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
+ function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
+ Decl : Node_Id;
+ Pack_Decl : Node_Id;
- function Has_Alias
- (N : Node_Id)
- return Boolean
- is
- function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
- function Has_Alias_Deep (Typ : Entity_Id) return Boolean
- is
- Comp : Node_Id;
begin
+ if Is_Itype (E) then
+ Decl := Associated_Node_For_Itype (E);
+ else
+ Decl := Parent (E);
+ end if;
- if Is_Array_Type (Typ)
- and then Has_Aliased_Components (Typ)
- then
- return True;
-
- -- Note: Has_Aliased_Components applies only to arrays
-
- elsif Is_Record_Type (Typ) then
- -- It is possible to have an aliased discriminant, so they must be
- -- checked along with normal components.
-
- Comp := First_Component_Or_Discriminant (Typ);
- while Present (Comp) loop
- if Is_Aliased (Comp)
- or else Is_Aliased (Etype (Comp))
- then
- return True;
- end if;
-
- if Has_Alias_Deep (Etype (Comp)) then
- return True;
- end if;
+ Pack_Decl := Parent (Parent (Decl));
- Next_Component_Or_Discriminant (Comp);
- end loop;
+ if Nkind (Pack_Decl) /= N_Package_Declaration then
return False;
- else
- return Is_Aliased (Typ);
end if;
- end Has_Alias_Deep;
- begin
- case Nkind (N) is
+ return
+ Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
+ and then Get_SPARK_Mode_From_Annotation
+ (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
+ end Is_Private_Entity_Mode_Off;
- when N_Identifier
- | N_Expanded_Name
- =>
- return Is_Aliased (Entity (N)) or else Has_Alias_Deep (Etype (N));
-
- when N_Defining_Identifier =>
- return Is_Aliased (N) or else Has_Alias_Deep (Etype (N));
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Has_Alias (Expression (N));
-
- when N_Parameter_Specification =>
- return Has_Alias (Defining_Identifier (N));
-
- when N_Selected_Component =>
- case Nkind (Selector_Name (N)) is
- when N_Identifier =>
- if Is_Aliased (Entity (Selector_Name (N))) then
- return True;
- end if;
-
- when others => null;
-
- end case;
-
- return Has_Alias (Prefix (N));
-
- when N_Indexed_Component
- | N_Slice
- =>
- return Has_Alias (Prefix (N));
-
- when N_Explicit_Dereference =>
- return True;
-
- when N_Function_Call =>
- return False;
-
- when N_Attribute_Reference =>
- if Is_Deep (Etype (Prefix (N))) then
- raise Program_Error;
- end if;
- return False;
-
- when others =>
- return False;
- end case;
- end Has_Alias;
-
- -------------------------
- -- Has_Array_Component --
- -------------------------
-
- function Has_Array_Component (N : Node_Id) return Boolean is
- begin
- case Nkind (N) is
- -- Base identifier. There is no array component here.
-
- when N_Identifier
- | N_Expanded_Name
- | N_Defining_Identifier
- =>
- return False;
-
- -- We check if the expression inside the conversion has an array
- -- component.
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Has_Array_Component (Expression (N));
-
- -- We check if the prefix has an array component
-
- when N_Selected_Component =>
- return Has_Array_Component (Prefix (N));
-
- -- We found the array component, return True
-
- when N_Indexed_Component
- | N_Slice
- =>
- return True;
-
- -- We check if the prefix has an array component
-
- when N_Explicit_Dereference =>
- return Has_Array_Component (Prefix (N));
-
- when N_Function_Call =>
- return False;
-
- when others =>
- raise Program_Error;
- end case;
- end Has_Array_Component;
-
- ----------------------------
- -- Has_Function_Component --
- ----------------------------
-
- function Has_Function_Component (N : Node_Id) return Boolean is
- begin
- case Nkind (N) is
- -- Base identifier. There is no function component here.
-
- when N_Identifier
- | N_Expanded_Name
- | N_Defining_Identifier
- =>
- return False;
-
- -- We check if the expression inside the conversion has a function
- -- component.
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Has_Function_Component (Expression (N));
-
- -- We check if the prefix has a function component
-
- when N_Selected_Component =>
- return Has_Function_Component (Prefix (N));
-
- -- We check if the prefix has a function component
-
- when N_Indexed_Component
- | N_Slice
- =>
- return Has_Function_Component (Prefix (N));
-
- -- We check if the prefix has a function component
-
- when N_Explicit_Dereference =>
- return Has_Function_Component (Prefix (N));
-
- -- We found the function component, return True
-
- when N_Function_Call =>
- return True;
-
- when others =>
- raise Program_Error;
-
- end case;
- end Has_Function_Component;
-
- --------
- -- Hp --
- --------
-
- procedure Hp (P : Perm_Env) is
- Elem : Perm_Tree_Maps.Key_Option;
-
- begin
- Elem := Get_First_Key (P);
- while Elem.Present loop
- Print_Node_Briefly (Elem.K);
- Elem := Get_Next_Key (P);
- end loop;
- end Hp;
-
- --------------------------
- -- Illegal_Global_Usage --
- --------------------------
-
- procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
- begin
- Error_Msg_NE ("cannot use global variable & of deep type", N, N);
- Error_Msg_N ("\without prior declaration in a Global aspect", N);
-
- Errout.Finalize (Last_Call => True);
- Errout.Output_Messages;
- Exit_Program (E_Errors);
- end Illegal_Global_Usage;
-
- --------------------
- -- Is_Borrowed_In --
- --------------------
-
- function Is_Borrowed_In (E : Entity_Id) return Boolean is
- begin
- return Is_Access_Type (Etype (E))
- and then not Is_Access_Constant (Etype (E));
- end Is_Borrowed_In;
-
- -------------
- -- Is_Deep --
- -------------
-
- function Is_Deep (E : Entity_Id) return Boolean is
- function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
-
- function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
- Decl : Node_Id;
- Pack_Decl : Node_Id;
-
- begin
- if Is_Itype (E) then
- Decl := Associated_Node_For_Itype (E);
- else
- Decl := Parent (E);
- end if;
-
- Pack_Decl := Parent (Parent (Decl));
-
- if Nkind (Pack_Decl) /= N_Package_Declaration then
- return False;
- end if;
-
- return
- Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
- and then Get_SPARK_Mode_From_Annotation
- (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
- end Is_Private_Entity_Mode_Off;
begin
pragma Assert (Is_Type (E));
-
case Ekind (E) is
when Scalar_Kind =>
return False;
when E_Record_Type
| E_Record_Subtype
- =>
+ =>
declare
Elmt : Entity_Id;
Next_Component_Or_Discriminant (Elmt);
end if;
end loop;
-
return False;
end;
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
end Is_Deep;
----------------
- -- Is_Shallow --
+ -- Perm_Error --
----------------
- function Is_Shallow (E : Entity_Id) return Boolean is
- begin
- pragma Assert (Is_Type (E));
- return not Is_Deep (E);
- end Is_Shallow;
-
- ------------------
- -- Loop_Of_Exit --
- ------------------
-
- function Loop_Of_Exit (N : Node_Id) return Entity_Id is
- Nam : Node_Id := Name (N);
- Stmt : Node_Id := N;
- begin
- if No (Nam) then
- while Present (Stmt) loop
- Stmt := Parent (Stmt);
- if Nkind (Stmt) = N_Loop_Statement then
- Nam := Identifier (Stmt);
- exit;
- end if;
- end loop;
- end if;
- return Entity (Nam);
- end Loop_Of_Exit;
- ---------
- -- Lub --
- ---------
-
- function Lub (P1, P2 : Perm_Kind) return Perm_Kind
+ procedure Perm_Error
+ (N : Node_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind)
is
- begin
- case P1 is
- when No_Access =>
- return P2;
-
- when Read_Only =>
- case P2 is
- when No_Access
- | Read_Only
- =>
- return Read_Only;
-
- when Write_Perm =>
- return Read_Write;
- end case;
-
- when Write_Only =>
- case P2 is
- when No_Access
- | Write_Only
- =>
- return Write_Only;
+ procedure Set_Root_Object
+ (Path : Node_Id;
+ Obj : out Entity_Id;
+ Deref : out Boolean);
+ -- Set the root object Obj, and whether the path contains a dereference,
+ -- from a path Path.
- when Read_Perm =>
- return Read_Write;
- end case;
+ ---------------------
+ -- Set_Root_Object --
+ ---------------------
- when Read_Write =>
- return Read_Write;
- end case;
- end Lub;
+ procedure Set_Root_Object
+ (Path : Node_Id;
+ Obj : out Entity_Id;
+ Deref : out Boolean)
+ is
+ begin
+ case Nkind (Path) is
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ Obj := Entity (Path);
+ Deref := False;
- ----------------
- -- Merge_Envs --
- ----------------
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ Set_Root_Object (Expression (Path), Obj, Deref);
- procedure Merge_Envs
- (Target : in out Perm_Env;
- Source : in out Perm_Env)
- is
- procedure Merge_Trees
- (Target : Perm_Tree_Access;
- Source : Perm_Tree_Access);
+ when N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ Set_Root_Object (Prefix (Path), Obj, Deref);
- procedure Merge_Trees
- (Target : Perm_Tree_Access;
- Source : Perm_Tree_Access)
- is
- procedure Apply_Glb_Tree
- (A : Perm_Tree_Access;
- P : Perm_Kind);
-
- procedure Apply_Glb_Tree
- (A : Perm_Tree_Access;
- P : Perm_Kind)
- is
- begin
- A.all.Tree.Permission := Glb (Permission (A), P);
+ when N_Explicit_Dereference =>
+ Set_Root_Object (Prefix (Path), Obj, Deref);
+ Deref := True;
- case Kind (A) is
- when Entire_Object =>
- A.all.Tree.Children_Permission :=
- Glb (Children_Permission (A), P);
+ when others =>
+ raise Program_Error;
+ end case;
+ end Set_Root_Object;
+ -- Local variables
- when Reference =>
- Apply_Glb_Tree (Get_All (A), P);
+ Root : Entity_Id;
+ Is_Deref : Boolean;
- when Array_Component =>
- Apply_Glb_Tree (Get_Elem (A), P);
+ -- Start of processing for Perm_Error
- when Record_Component =>
- declare
- Comp : Perm_Tree_Access;
- begin
- Comp := Perm_Tree_Maps.Get_First (Component (A));
- while Comp /= null loop
- Apply_Glb_Tree (Comp, P);
- Comp := Perm_Tree_Maps.Get_Next (Component (A));
- end loop;
-
- Apply_Glb_Tree (Other_Components (A), P);
- end;
- end case;
- end Apply_Glb_Tree;
-
- Perm : constant Perm_Kind :=
- Glb (Permission (Target), Permission (Source));
-
- begin
- pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
- Target.all.Tree.Permission := Perm;
-
- case Kind (Target) is
- when Entire_Object =>
- declare
- Child_Perm : constant Perm_Kind :=
- Children_Permission (Target);
-
- begin
- case Kind (Source) is
- when Entire_Object =>
- Target.all.Tree.Children_Permission :=
- Glb (Child_Perm, Children_Permission (Source));
-
- when Reference =>
- Copy_Tree (Source, Target);
- Target.all.Tree.Permission := Perm;
- Apply_Glb_Tree (Get_All (Target), Child_Perm);
-
- when Array_Component =>
- Copy_Tree (Source, Target);
- Target.all.Tree.Permission := Perm;
- Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
-
- when Record_Component =>
- Copy_Tree (Source, Target);
- Target.all.Tree.Permission := Perm;
- declare
- Comp : Perm_Tree_Access;
-
- begin
- Comp :=
- Perm_Tree_Maps.Get_First (Component (Target));
- while Comp /= null loop
- -- Apply glb tree on every component subtree
-
- Apply_Glb_Tree (Comp, Child_Perm);
- Comp := Perm_Tree_Maps.Get_Next
- (Component (Target));
- end loop;
- end;
- Apply_Glb_Tree (Other_Components (Target), Child_Perm);
-
- end case;
- end;
- when Reference =>
- case Kind (Source) is
- when Entire_Object =>
- Apply_Glb_Tree (Get_All (Target),
- Children_Permission (Source));
-
- when Reference =>
- Merge_Trees (Get_All (Target), Get_All (Source));
-
- when others =>
- raise Program_Error;
-
- end case;
-
- when Array_Component =>
- case Kind (Source) is
- when Entire_Object =>
- Apply_Glb_Tree (Get_Elem (Target),
- Children_Permission (Source));
-
- when Array_Component =>
- Merge_Trees (Get_Elem (Target), Get_Elem (Source));
-
- when others =>
- raise Program_Error;
-
- end case;
-
- when Record_Component =>
- case Kind (Source) is
- when Entire_Object =>
- declare
- Child_Perm : constant Perm_Kind :=
- Children_Permission (Source);
-
- Comp : Perm_Tree_Access;
-
- begin
- Comp := Perm_Tree_Maps.Get_First
- (Component (Target));
- while Comp /= null loop
- -- Apply glb tree on every component subtree
-
- Apply_Glb_Tree (Comp, Child_Perm);
- Comp :=
- Perm_Tree_Maps.Get_Next (Component (Target));
- end loop;
- Apply_Glb_Tree (Other_Components (Target), Child_Perm);
- end;
-
- when Record_Component =>
- declare
- Key_Source : Perm_Tree_Maps.Key_Option;
- CompTarget : Perm_Tree_Access;
- CompSource : Perm_Tree_Access;
-
- begin
- Key_Source := Perm_Tree_Maps.Get_First_Key
- (Component (Source));
-
- while Key_Source.Present loop
- CompSource := Perm_Tree_Maps.Get
- (Component (Source), Key_Source.K);
- CompTarget := Perm_Tree_Maps.Get
- (Component (Target), Key_Source.K);
-
- pragma Assert (CompSource /= null);
- Merge_Trees (CompTarget, CompSource);
-
- Key_Source := Perm_Tree_Maps.Get_Next_Key
- (Component (Source));
- end loop;
-
- Merge_Trees (Other_Components (Target),
- Other_Components (Source));
- end;
-
- when others =>
- raise Program_Error;
-
- end case;
- end case;
- end Merge_Trees;
-
- CompTarget : Perm_Tree_Access;
- CompSource : Perm_Tree_Access;
- KeyTarget : Perm_Tree_Maps.Key_Option;
-
- begin
- KeyTarget := Get_First_Key (Target);
- -- Iterate over every tree of the environment in the target, and merge
- -- it with the source if there is such a similar one that exists. If
- -- there is none, then skip.
- while KeyTarget.Present loop
-
- CompSource := Get (Source, KeyTarget.K);
- CompTarget := Get (Target, KeyTarget.K);
-
- pragma Assert (CompTarget /= null);
-
- if CompSource /= null then
- Merge_Trees (CompTarget, CompSource);
- Remove (Source, KeyTarget.K);
- end if;
-
- KeyTarget := Get_Next_Key (Target);
- end loop;
-
- -- Iterate over every tree of the environment of the source. And merge
- -- again. If there is not any tree of the target then just copy the tree
- -- from source to target.
- declare
- KeySource : Perm_Tree_Maps.Key_Option;
- begin
- KeySource := Get_First_Key (Source);
- while KeySource.Present loop
-
- CompSource := Get (Source, KeySource.K);
- CompTarget := Get (Target, KeySource.K);
-
- if CompTarget = null then
- CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
- Copy_Tree (CompSource, CompTarget);
- Set (Target, KeySource.K, CompTarget);
- else
- Merge_Trees (CompTarget, CompSource);
- end if;
-
- KeySource := Get_Next_Key (Source);
- end loop;
- end;
-
- Free_Env (Source);
- end Merge_Envs;
-
- ----------------
- -- Perm_Error --
- ----------------
-
- procedure Perm_Error
- (N : Node_Id;
- Perm : Perm_Kind;
- Found_Perm : Perm_Kind)
- is
- procedure Set_Root_Object
- (Path : Node_Id;
- Obj : out Entity_Id;
- Deref : out Boolean);
- -- Set the root object Obj, and whether the path contains a dereference,
- -- from a path Path.
-
- ---------------------
- -- Set_Root_Object --
- ---------------------
-
- procedure Set_Root_Object
- (Path : Node_Id;
- Obj : out Entity_Id;
- Deref : out Boolean)
- is
- begin
- case Nkind (Path) is
- when N_Identifier
- | N_Expanded_Name
- =>
- Obj := Entity (Path);
- Deref := False;
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- Set_Root_Object (Expression (Path), Obj, Deref);
-
- when N_Indexed_Component
- | N_Selected_Component
- | N_Slice
- =>
- Set_Root_Object (Prefix (Path), Obj, Deref);
-
- when N_Explicit_Dereference =>
- Set_Root_Object (Prefix (Path), Obj, Deref);
- Deref := True;
-
- when others =>
- raise Program_Error;
- end case;
- end Set_Root_Object;
-
- -- Local variables
-
- Root : Entity_Id;
- Is_Deref : Boolean;
-
- -- Start of processing for Perm_Error
-
- begin
- Set_Root_Object (N, Root, Is_Deref);
+ begin
+ Set_Root_Object (N, Root, Is_Deref);
if Is_Deref then
Error_Msg_NE
------------------
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
return;
end if;
- -- We ignore shallow unaliased. They are checked in flow analysis,
- -- allowing backward compatibility.
+ State_N := Get_Perm (N);
- if Current_Checking_Mode /= Super_Move
- and then not Has_Alias (N)
- and then Is_Shallow (Etype (N))
- then
- return;
- end if;
-
- declare
- Perm_N : constant Perm_Kind := Get_Perm (N);
-
- begin
+ case Current_Checking_Mode is
- case Current_Checking_Mode is
- -- Check permission R, do nothing
+ -- Check permission R, do nothing
- when Read =>
- if Perm_N not in Read_Perm then
- Perm_Error (N, Read_Only, Perm_N);
- return;
- end if;
+ when Read =>
- -- If shallow type no need for RW, only R
+ -- This condition should be removed when removing the read
+ -- checking mode.
- when Move =>
- if Is_Shallow (Etype (N)) then
- if Perm_N not in Read_Perm then
- Perm_Error (N, Read_Only, Perm_N);
- return;
- end if;
- else
- -- Check permission RW if deep
+ return;
- if Perm_N /= Read_Write then
- Perm_Error (N, Read_Write, Perm_N);
- return;
- end if;
+ when Move =>
- declare
- -- Set permission to W to the path and any of its prefix
+ -- The rhs object in an assignment statement (including copy in
+ -- and copy back) should be in the Unrestricted or Moved state.
+ -- Otherwise the move is not allowed.
+ -- This applies to both stand-alone and composite objects.
+ -- If the state of the source is Moved, then a warning message
+ -- is prompt to make the user aware of reading a nullified
+ -- object.
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (N, Move);
+ if State_N /= Unrestricted and State_N /= Moved then
+ Perm_Error (N, Unrestricted, State_N);
+ return;
+ end if;
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ -- In the AI, after moving a path nothing to do since the rhs
+ -- object was in the Unrestricted state and it shall be
+ -- refreshed to Unrestricted. The object should be nullified
+ -- however. To avoid moving again a name that has already been
+ -- moved, in this implementation we set the state of the moved
+ -- object to "Moved". This shall be used to prompt a warning
+ -- when manipulating a null pointer and also to implement
+ -- the no aliasing parameter restriction.
+
+ if State_N = Moved then
+ Error_Msg_N ("?the source or one of its extensions has"
+ & " already been moved", N);
+ end if;
- return;
- end if;
+ declare
+ -- Set state to Borrowed to the path and any of its prefixes
- -- Set permissions to
- -- No for any extension with more .all
- -- W for any deep extension with same number of .all
- -- RW for any shallow extension with same number of .all
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes (N, Moved);
- Set_Perm_Extensions_Move (Tree, Etype (N));
- end;
- end if;
+ begin
+ if Tree = null then
- -- Check permission RW
+ -- We went through a function call, no permission to
+ -- modify.
- when Super_Move =>
- if Perm_N /= Read_Write then
- Perm_Error (N, Read_Write, Perm_N);
return;
end if;
- declare
- -- Set permission to No to the path and any of its prefix up
- -- to the first .all and then W.
-
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (N, Super_Move);
-
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
-
- return;
- end if;
+ -- Set state to Borrowed on any strict extension of the path
- -- Set permissions to No on any strict extension of the path
+ Set_Perm_Extensions (Tree, Moved);
+ end;
- Set_Perm_Extensions (Tree, No_Access);
- end;
+ when Assign =>
- -- Check permission W
+ -- The lhs object in an assignment statement (including copy in
+ -- and copy back) should be in the Unrestricted state.
+ -- Otherwise the move is not allowed.
+ -- This applies to both stand-alone and composite objects.
- when Assign =>
- if Perm_N not in Write_Perm then
- Perm_Error (N, Write_Only, Perm_N);
- return;
- end if;
+ if State_N /= Unrestricted and State_N /= Moved then
+ Perm_Error (N, Unrestricted, State_N);
+ return;
+ end if;
- -- If the tree has an array component, then the permissions do
- -- not get modified by the assignment.
+ -- After assigning to a path nothing to do since it was in the
+ -- Unrestricted state and it would be refreshed to
+ -- Unrestricted.
- if Has_Array_Component (N) then
- return;
- end if;
+ when Borrow =>
- -- Same if has function component
+ -- Borrowing is only allowed on Unrestricted objects.
- if Has_Function_Component (N) then -- Dead code?
- return;
- end if;
+ if State_N /= Unrestricted and State_N /= Moved then
+ Perm_Error (N, Unrestricted, State_N);
+ end if;
- declare
- -- Get the permission tree for the path
+ if State_N = Moved then
+ Error_Msg_N ("?the source or one of its extensions has"
+ & " already been moved", N);
+ end if;
- Tree : constant Perm_Tree_Access :=
- Get_Perm_Tree (N);
+ declare
+ -- Set state to Borrowed to the path and any of its prefixes
- Dummy : Perm_Tree_Access;
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes (N, Borrowed);
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ begin
+ if Tree = null then
- return;
- end if;
+ -- We went through a function call, no permission to
+ -- modify.
- -- Set permission RW for it and all of its extensions
+ return;
+ end if;
- Tree.all.Tree.Permission := Read_Write;
+ -- Set state to Borrowed on any strict extension of the path
- Set_Perm_Extensions (Tree, Read_Write);
+ Set_Perm_Extensions (Tree, Borrowed);
+ end;
- -- Normalize the permission tree
+ when Observe =>
+ if State_N /= Unrestricted
+ and then State_N /= Observed
+ then
+ Perm_Error (N, Observed, State_N);
+ end if;
- Dummy := Set_Perm_Prefixes_Assign (N);
- end;
+ declare
+ -- Set permission to Observed on the path and any of its
+ -- prefixes if it is of a deep type. Actually, some operation
+ -- like reading from an object of access type is considered as
+ -- observe while it should not affect the permissions of
+ -- the considered tree.
- -- Check permission W
+ Tree : Perm_Tree_Access;
- when Borrow_Out =>
- if Perm_N not in Write_Perm then
- Perm_Error (N, Write_Only, Perm_N);
+ begin
+ if Is_Deep (Etype (N)) then
+ Tree := Set_Perm_Prefixes (N, Observed);
+ else
+ Tree := null;
end if;
- declare
- -- Set permission to No to the path and any of its prefixes
-
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow_Out (N);
-
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
-
- return;
- end if;
-
- -- Set permissions to No on any strict extension of the path
-
- Set_Perm_Extensions (Tree, No_Access);
- end;
+ if Tree = null then
- when Observe =>
- if Perm_N not in Read_Perm then
- Perm_Error (N, Read_Only, Perm_N);
- end if;
+ -- We went through a function call, no permission to
+ -- modify.
- if Is_By_Copy_Type (Etype (N)) then
return;
end if;
- declare
- -- Set permission to No on the path and any of its prefixes
-
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Observe (N);
-
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
-
- return;
- end if;
-
- -- Set permissions to No on any strict extension of the path
+ -- Set permissions to No on any strict extension of the path
- Set_Perm_Extensions (Tree, Read_Only);
- end;
- end case;
- end;
+ Set_Perm_Extensions (Tree, Observed);
+ end;
+ end case;
end Process_Path;
-------------------------
-------------------------
procedure Return_Declarations (L : List_Id) is
-
procedure Return_Declaration (Decl : Node_Id);
-- Check correct permissions for every declared object
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.
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,
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;
begin
N := First (L);
- while Present (N) loop
- Return_Declaration (N);
- Next (N);
- end loop;
- end Return_Declarations;
-
- --------------------
- -- Return_Globals --
- --------------------
-
- procedure Return_Globals (Subp : Entity_Id) is
-
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind);
- -- Return global items from the list starting at Item
-
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
- -- Return global items for the mode Global_Mode
-
- ------------------------------
- -- Return_Globals_From_List --
- ------------------------------
-
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind)
- is
- Item : Node_Id := First_Item;
- E : Entity_Id;
-
- begin
- while Present (Item) loop
- E := Entity (Item);
-
- -- Ignore abstract states, which play no role in pointer aliasing
-
- if Ekind (E) = E_Abstract_State then
- null;
- else
- Return_Parameter_Or_Global (E, Kind, Subp, Global_Var => True);
- end if;
- Next_Global (Item);
- end loop;
- end Return_Globals_From_List;
-
- ----------------------------
- -- Return_Globals_Of_Mode --
- ----------------------------
-
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
- Kind : Formal_Kind;
-
- begin
- case Global_Mode is
- when Name_Input | Name_Proof_In =>
- Kind := E_In_Parameter;
- when Name_Output =>
- Kind := E_Out_Parameter;
- when Name_In_Out =>
- Kind := E_In_Out_Parameter;
- when others =>
- raise Program_Error;
- end case;
-
- -- Return both global items from Global and Refined_Global pragmas
-
- Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
- Return_Globals_From_List
- (First_Global (Subp, Global_Mode, Refined => True), Kind);
- end Return_Globals_Of_Mode;
-
- -- Start of processing for Return_Globals
-
- begin
- Return_Globals_Of_Mode (Name_Proof_In);
- Return_Globals_Of_Mode (Name_Input);
- Return_Globals_Of_Mode (Name_Output);
- Return_Globals_Of_Mode (Name_In_Out);
- end Return_Globals;
-
- --------------------------------
- -- Return_Parameter_Or_Global --
- --------------------------------
-
- procedure Return_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id;
- Global_Var : Boolean)
- is
- Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
- pragma Assert (Elem /= null);
-
- begin
- -- Shallow unaliased parameters and globals cannot introduce pointer
- -- aliasing.
-
- if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then
- null;
-
- -- Observed IN parameters and globals need not return a permission to
- -- the caller.
-
- elsif Mode = E_In_Parameter
- and then (not Is_Borrowed_In (Id) or else Global_Var)
- then
- null;
-
- -- All other parameters and globals should return with mode RW to the
- -- caller.
-
- else
- if Permission (Elem) /= Read_Write then
- Perm_Error_Subprogram_End
- (E => Id,
- Subp => Subp,
- Perm => Read_Write,
- Found_Perm => Permission (Elem));
- end if;
- end if;
- end Return_Parameter_Or_Global;
-
- -----------------------
- -- Return_Parameters --
- -----------------------
-
- procedure Return_Parameters (Subp : Entity_Id) is
- Formal : Entity_Id;
-
- begin
- Formal := First_Formal (Subp);
- while Present (Formal) loop
- Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp, False);
- Next_Formal (Formal);
- end loop;
- end Return_Parameters;
-
- -------------------------
- -- Set_Perm_Extensions --
- -------------------------
-
- procedure Set_Perm_Extensions
- (T : Perm_Tree_Access;
- P : Perm_Kind)
- is
- procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
-
- procedure Free_Perm_Tree_Children (T : Perm_Tree_Access)
- is
- begin
- case Kind (T) is
- when Entire_Object =>
- null;
-
- when Reference =>
- Free_Perm_Tree (T.all.Tree.Get_All);
-
- when Array_Component =>
- Free_Perm_Tree (T.all.Tree.Get_Elem);
-
- -- Free every Component subtree
-
- when Record_Component =>
- declare
- Comp : Perm_Tree_Access;
-
- begin
- Comp := Perm_Tree_Maps.Get_First (Component (T));
- while Comp /= null loop
- Free_Perm_Tree (Comp);
- Comp := Perm_Tree_Maps.Get_Next (Component (T));
- end loop;
-
- Free_Perm_Tree (T.all.Tree.Other_Components);
- end;
- end case;
- end Free_Perm_Tree_Children;
-
- Son : constant Perm_Tree :=
- Perm_Tree'
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (T),
- Permission => Permission (T),
- Children_Permission => P);
-
- begin
- Free_Perm_Tree_Children (T);
- T.all.Tree := Son;
- end Set_Perm_Extensions;
-
- ------------------------------
- -- Set_Perm_Extensions_Move --
- ------------------------------
-
- procedure Set_Perm_Extensions_Move
- (T : Perm_Tree_Access;
- E : Entity_Id)
- is
- begin
- if not Is_Node_Deep (T) then
- -- We are a shallow extension with same number of .all
-
- Set_Perm_Extensions (T, Read_Write);
- return;
- end if;
-
- -- We are a deep extension here (or the moved deep path)
-
- T.all.Tree.Permission := Write_Only;
-
- case T.all.Tree.Kind is
- -- Unroll the tree depending on the type
-
- when Entire_Object =>
- case Ekind (E) is
- when Scalar_Kind
- | E_String_Literal_Subtype
- =>
- Set_Perm_Extensions (T, No_Access);
-
- -- No need to unroll here, directly put sons to No_Access
-
- when Access_Kind =>
- if Ekind (E) in Access_Subprogram_Kind then
- null;
- else
- Set_Perm_Extensions (T, No_Access);
- end if;
-
- -- No unrolling done, too complicated
-
- when E_Class_Wide_Subtype
- | E_Class_Wide_Type
- | E_Incomplete_Type
- | E_Incomplete_Subtype
- | E_Exception_Type
- | E_Task_Type
- | E_Task_Subtype
- =>
- Set_Perm_Extensions (T, No_Access);
-
- -- Expand the tree. Replace the node with Array component.
-
- when E_Array_Type
- | E_Array_Subtype =>
- declare
- Son : Perm_Tree_Access;
-
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (T),
- Permission => Read_Write,
- Children_Permission => Read_Write));
-
- Set_Perm_Extensions_Move (Son, Component_Type (E));
-
- -- We change the current node from Entire_Object to
- -- Reference with Write_Only and the previous son.
-
- pragma Assert (Is_Node_Deep (T));
-
- T.all.Tree := (Kind => Array_Component,
- Is_Node_Deep => Is_Node_Deep (T),
- Permission => Write_Only,
- Get_Elem => Son);
- end;
-
- -- Unroll, and set permission extensions with component type
-
- when E_Record_Type
- | E_Record_Subtype
- | E_Record_Type_With_Private
- | E_Record_Subtype_With_Private
- | E_Protected_Type
- | E_Protected_Subtype
- =>
- declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
-
- Elem : Node_Id;
-
- Son : Perm_Tree_Access;
-
- begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
-
- pragma Assert (Is_Node_Deep (T));
-
- T.all.Tree :=
- (Kind => Record_Component,
- Is_Node_Deep => Is_Node_Deep (T),
- Permission => Write_Only,
- Component => Perm_Tree_Maps.Nil,
- Other_Components =>
- new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => True,
- Permission => Read_Write,
- Children_Permission => Read_Write)
- )
- );
-
- -- We fill the hash table with all sons of the record,
- -- with basic Entire_Objects nodes.
- Elem := First_Component_Or_Discriminant (E);
- while Present (Elem) loop
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Elem)),
- Permission => Read_Write,
- Children_Permission => Read_Write));
-
- Set_Perm_Extensions_Move (Son, Etype (Elem));
-
- Perm_Tree_Maps.Set
- (T.all.Tree.Component, Elem, Son);
-
- Next_Component_Or_Discriminant (Elem);
- end loop;
- end;
-
- when E_Private_Type
- | E_Private_Subtype
- | E_Limited_Private_Type
- | E_Limited_Private_Subtype
- =>
- Set_Perm_Extensions_Move (T, Underlying_Type (E));
-
- when others =>
- raise Program_Error;
- end case;
-
- when Reference =>
- -- Now the son does not have the same number of .all
- Set_Perm_Extensions (T, No_Access);
-
- when Array_Component =>
- Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E));
-
- when Record_Component =>
- declare
- Comp : Perm_Tree_Access;
- It : Node_Id;
-
- begin
- It := First_Component_Or_Discriminant (E);
- while It /= Empty loop
- Comp := Perm_Tree_Maps.Get (Component (T), It);
- pragma Assert (Comp /= null);
- Set_Perm_Extensions_Move (Comp, It);
- It := Next_Component_Or_Discriminant (E);
- end loop;
-
- Set_Perm_Extensions (Other_Components (T), No_Access);
- end;
- end case;
- end Set_Perm_Extensions_Move;
-
- ------------------------------
- -- Set_Perm_Prefixes_Assign --
- ------------------------------
-
- function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access is
- C : constant Perm_Tree_Access := Get_Perm_Tree (N);
-
- begin
- pragma Assert (Current_Checking_Mode = Assign);
-
- -- The function should not be called if has_function_component
-
- pragma Assert (C /= null);
-
- case Kind (C) is
- when Entire_Object =>
- pragma Assert (Children_Permission (C) = Read_Write);
-
- -- Maroua: Children could have read_only perm. Why Read_Write?
-
- C.all.Tree.Permission := Read_Write;
-
- when Reference =>
- pragma Assert (Get_All (C) /= null);
-
- C.all.Tree.Permission :=
- Lub (Permission (C), Permission (Get_All (C)));
-
- when Array_Component =>
- pragma Assert (C.all.Tree.Get_Elem /= null);
-
- -- Given that it is not possible to know which element has been
- -- assigned, then the permissions do not get changed in case of
- -- Array_Component.
-
- null;
-
- when Record_Component =>
- declare
- Comp : Perm_Tree_Access;
- Perm : Perm_Kind := Read_Write;
-
- begin
- -- We take the Glb of all the descendants, and then update the
- -- permission of the node with it.
-
- Comp := Perm_Tree_Maps.Get_First (Component (C));
- while Comp /= null loop
- Perm := Glb (Perm, Permission (Comp));
- Comp := Perm_Tree_Maps.Get_Next (Component (C));
- end loop;
-
- Perm := Glb (Perm, Permission (Other_Components (C)));
-
- C.all.Tree.Permission := Lub (Permission (C), Perm);
- end;
- end case;
-
- case Nkind (N) is
-
- -- Base identifier. End recursion here.
-
- when N_Identifier
- | N_Expanded_Name
- | N_Defining_Identifier
- =>
- return null;
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Set_Perm_Prefixes_Assign (Expression (N));
-
- when N_Parameter_Specification =>
- raise Program_Error;
-
- -- Continue recursion on prefix
-
- when N_Selected_Component =>
- return Set_Perm_Prefixes_Assign (Prefix (N));
-
- -- Continue recursion on prefix
-
- when N_Indexed_Component
- | N_Slice
- =>
- return Set_Perm_Prefixes_Assign (Prefix (N));
-
- -- Continue recursion on prefix
-
- when N_Explicit_Dereference =>
- return Set_Perm_Prefixes_Assign (Prefix (N));
-
- when N_Function_Call =>
- raise Program_Error;
-
- when others =>
- raise Program_Error;
-
- end case;
- end Set_Perm_Prefixes_Assign;
-
- ----------------------------------
- -- Set_Perm_Prefixes_Borrow_Out --
- ----------------------------------
-
- function Set_Perm_Prefixes_Borrow_Out
- (N : Node_Id)
- return Perm_Tree_Access
- is
- begin
- pragma Assert (Current_Checking_Mode = Borrow_Out);
-
- case Nkind (N) is
- -- Base identifier. Set permission to No.
-
- when N_Identifier
- | N_Expanded_Name
- =>
- declare
- P : constant Node_Id := Entity (N);
-
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
-
- pragma Assert (C /= null);
-
- begin
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
-
- Set (Current_Initialization_Map, Unique_Entity (P), True);
-
- C.all.Tree.Permission := No_Access;
- return C;
- end;
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Set_Perm_Prefixes_Borrow_Out (Expression (N));
-
- when N_Parameter_Specification
- | N_Defining_Identifier
- =>
- raise Program_Error;
-
- -- We set the permission tree of its prefix, and then we extract
- -- our subtree from the returned pointer and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree
- -- in one step.
-
- when N_Selected_Component =>
- declare
- C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow_Out (Prefix (N));
-
- begin
- if C = null then
- -- We went through a function call, do nothing
-
- return null;
- end if;
-
- -- The permission of the returned node should be No
-
- pragma Assert (Permission (C) = No_Access);
-
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Record_Component);
-
- if Kind (C) = Record_Component then
- -- The tree is unfolded. We just modify the permission and
- -- return the record subtree.
-
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
-
- Selected_C : Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
-
- begin
- if Selected_C = null then
- Selected_C := Other_Components (C);
- end if;
-
- pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission := No_Access;
-
- return Selected_C;
- end;
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
-
- Elem : Node_Id;
-
- -- Create an empty hash table
-
- Hashtbl : Perm_Tree_Maps.Instance;
-
- -- We create the unrolled nodes, that will all have same
- -- permission than parent.
-
- Son : Perm_Tree_Access;
-
- ChildrenPerm : constant Perm_Kind :=
- Children_Permission (C);
-
- begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
-
- C.all.Tree :=
- (Kind => Record_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Component => Hashtbl,
- Other_Components =>
- new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => True,
- Permission => ChildrenPerm,
- Children_Permission => ChildrenPerm)
- ));
-
- -- We fill the hash table with all sons of the record,
- -- with basic Entire_Objects nodes.
- Elem := First_Component_Or_Discriminant
- (Etype (Prefix (N)));
-
- while Present (Elem) loop
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Elem)),
- Permission => ChildrenPerm,
- Children_Permission => ChildrenPerm));
-
- Perm_Tree_Maps.Set
- (C.all.Tree.Component, Elem, Son);
-
- Next_Component_Or_Discriminant (Elem);
- end loop;
-
- -- Now we set the right field to No_Access, and then we
- -- return the tree to the sons, so that the recursion can
- -- continue.
-
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
-
- Selected_C : Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
-
- begin
- if Selected_C = null then
- Selected_C := Other_Components (C);
- end if;
-
- pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission := No_Access;
-
- return Selected_C;
- end;
- end;
- else
- raise Program_Error;
- end if;
- end;
-
- -- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer the subtree and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree in
- -- one step.
+ while Present (N) loop
+ Return_Declaration (N);
+ Next (N);
+ end loop;
+ end Return_Declarations;
- when N_Indexed_Component
- | N_Slice
- =>
- declare
- C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+ --------------------
+ -- Return_Globals --
+ --------------------
- begin
- if C = null then
- -- We went through a function call, do nothing
+ procedure Return_Globals (Subp : Entity_Id) is
+ procedure Return_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind);
+ -- Return global items from the list starting at Item
- return null;
- end if;
+ procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
+ -- Return global items for the mode Global_Mode
- -- The permission of the returned node should be either W
- -- (because the recursive call sets <= Write_Only) or No
- -- (if another path has been moved with 'Access).
+ ------------------------------
+ -- Return_Globals_From_List --
+ ------------------------------
- pragma Assert (Permission (C) = No_Access);
+ procedure Return_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind)
+ is
+ Item : Node_Id := First_Item;
+ E : Entity_Id;
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Array_Component);
+ begin
+ while Present (Item) loop
+ E := Entity (Item);
- if Kind (C) = Array_Component then
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
+ -- Ignore abstract states, which play no role in pointer aliasing
- pragma Assert (Get_Elem (C) /= null);
+ if Ekind (E) = E_Abstract_State then
+ null;
+ else
+ Return_The_Global (E, Kind, Subp);
+ end if;
+ Next_Global (Item);
+ end loop;
+ end Return_Globals_From_List;
- C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
+ ----------------------------
+ -- Return_Globals_Of_Mode --
+ ----------------------------
- return Get_Elem (C);
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace node with Array_Component.
+ procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
+ Kind : Formal_Kind;
- Son : Perm_Tree_Access;
+ begin
+ case Global_Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ Kind := E_In_Parameter;
+ when Name_Output =>
+ Kind := E_Out_Parameter;
+ when Name_In_Out =>
+ Kind := E_In_Out_Parameter;
+ when others =>
+ raise Program_Error;
+ end case;
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => No_Access,
- Children_Permission => Children_Permission (C)));
+ -- Return both global items from Global and Refined_Global pragmas
- -- We change the current node from Entire_Object
- -- to Array_Component with same permission and the
- -- previously defined son.
+ Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
+ Return_Globals_From_List
+ (First_Global (Subp, Global_Mode, Refined => True), Kind);
+ end Return_Globals_Of_Mode;
- C.all.Tree := (Kind => Array_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => No_Access,
- Get_Elem => Son);
+ -- Start of processing for Return_Globals
- return Get_Elem (C);
- end;
- else
- raise Program_Error;
- end if;
- end;
+ begin
+ Return_Globals_Of_Mode (Name_Proof_In);
+ Return_Globals_Of_Mode (Name_Input);
+ Return_Globals_Of_Mode (Name_Output);
+ Return_Globals_Of_Mode (Name_In_Out);
+ end Return_Globals;
- -- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer the subtree and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree
- -- at one step.
+ --------------------------------
+ -- Return_Parameter_Or_Global --
+ --------------------------------
- when N_Explicit_Dereference =>
- declare
- C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow_Out (Prefix (N));
+ procedure Return_The_Global
+ (Id : Entity_Id;
+ Mode : Formal_Kind;
+ Subp : Entity_Id)
+ is
+ Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
+ pragma Assert (Elem /= null);
- begin
- if C = null then
- -- We went through a function call. Do nothing.
+ begin
+ -- Observed IN parameters and globals need not return a permission to
+ -- the caller.
- return null;
- end if;
+ if Mode = E_In_Parameter
- -- The permission of the returned node should be No
+ -- Check this for read-only globals.
- pragma Assert (Permission (C) = No_Access);
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Reference);
+ then
+ if Permission (Elem) /= Unrestricted
+ and then Permission (Elem) /= Observed
+ then
+ Perm_Error_Subprogram_End
+ (E => Id,
+ Subp => Subp,
+ Perm => Observed,
+ Found_Perm => Permission (Elem));
+ end if;
- if Kind (C) = Reference then
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
+ -- All globals of mode out or in/out should return with mode
+ -- Unrestricted.
- pragma Assert (Get_All (C) /= null);
+ else
+ if Permission (Elem) /= Unrestricted then
+ Perm_Error_Subprogram_End
+ (E => Id,
+ Subp => Subp,
+ Perm => Unrestricted,
+ Found_Perm => Permission (Elem));
+ end if;
+ end if;
+ end Return_The_Global;
- C.all.Tree.Get_All.all.Tree.Permission := No_Access;
+ -------------------------
+ -- Set_Perm_Extensions --
+ -------------------------
- return Get_All (C);
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with Reference.
+ procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is
+ procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
+ procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
+ begin
+ case Kind (T) is
+ when Entire_Object =>
+ null;
- Son : Perm_Tree_Access;
+ when Reference =>
+ Free_Perm_Tree (T.all.Tree.Get_All);
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => No_Access,
- Children_Permission => Children_Permission (C)));
+ when Array_Component =>
+ Free_Perm_Tree (T.all.Tree.Get_Elem);
- -- We change the current node from Entire_Object to
- -- Reference with No_Access and the previous son.
+ -- Free every Component subtree
- pragma Assert (Is_Node_Deep (C));
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => No_Access,
- Get_All => Son);
+ begin
+ Comp := Perm_Tree_Maps.Get_First (Component (T));
+ while Comp /= null loop
+ Free_Perm_Tree (Comp);
+ Comp := Perm_Tree_Maps.Get_Next (Component (T));
+ end loop;
- return Get_All (C);
- end;
- else
- raise Program_Error;
- end if;
- end;
+ Free_Perm_Tree (T.all.Tree.Other_Components);
+ end;
+ end case;
+ end Free_Perm_Tree_Children;
- when N_Function_Call =>
- return null;
+ Son : constant Perm_Tree :=
+ Perm_Tree'
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (T),
+ Permission => Permission (T),
+ Children_Permission => P);
- when others =>
- raise Program_Error;
- end case;
- end Set_Perm_Prefixes_Borrow_Out;
+ begin
+ Free_Perm_Tree_Children (T);
+ T.all.Tree := Son;
+ end Set_Perm_Extensions;
- ----------------------------
- -- Set_Perm_Prefixes_Move --
- ----------------------------
+ ------------------------------
+ -- Set_Perm_Prefixes --
+ ------------------------------
- function Set_Perm_Prefixes_Move
- (N : Node_Id; Mode : Checking_Mode)
- return Perm_Tree_Access
+ function Set_Perm_Prefixes
+ (N : Node_Id;
+ New_Perm : Perm_Kind)
+ return Perm_Tree_Access
is
begin
- case Nkind (N) is
- -- Base identifier. Set permission to W or No depending on Mode.
+ case Nkind (N) is
when N_Identifier
| N_Expanded_Name
+ | N_Defining_Identifier
=>
+ if Nkind (N) = N_Defining_Identifier
+ and then New_Perm = Borrowed
+ then
+ raise Program_Error;
+ end if;
+
declare
- P : constant Node_Id := Entity (N);
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
+ P : Node_Id;
+ C : Perm_Tree_Access;
begin
- -- The base tree can be RW (first move from this base path) or
- -- W (already some extensions values moved), or even No_Access
- -- (extensions moved with 'Access). But it cannot be Read_Only
- -- (we get an error).
-
- if Permission (C) = Read_Only then
- raise Unrecoverable_Error;
+ if Nkind (N) = N_Defining_Identifier then
+ P := N;
+ else
+ P := Entity (N);
end if;
+ C := Get (Current_Perm_Env, Unique_Entity (P));
+ pragma Assert (C /= null);
+
-- Setting the initialization map to True, so that this
-- variable cannot be ignored anymore when looking at end
-- of elaboration of package.
Set (Current_Initialization_Map, Unique_Entity (P), True);
+ if New_Perm = Observed
+ and then C = null
+ then
- if C = null then
-- No null possible here, there are no parents for the path.
-- This means we are using a global variable without adding
-- it in environment with a global aspect.
Illegal_Global_Usage (N);
end if;
- if Mode = Super_Move then
- C.all.Tree.Permission := No_Access;
- else
- C.all.Tree.Permission := Glb (Write_Only, Permission (C));
- end if;
-
+ C.all.Tree.Permission := New_Perm;
return C;
end;
| N_Unchecked_Type_Conversion
| N_Qualified_Expression
=>
- return Set_Perm_Prefixes_Move (Expression (N), Mode);
+ return Set_Perm_Prefixes (Expression (N), New_Perm);
- when N_Parameter_Specification
- | N_Defining_Identifier
- =>
+ when N_Parameter_Specification =>
raise Program_Error;
-- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer our subtree and assign an adequate
+ -- our subtree from the returned pointer and assign an adequate
-- permission to it, if unfolded. If folded, we unroll the tree
- -- at one step.
+ -- in one step.
when N_Selected_Component =>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (Prefix (N), Mode);
+ Set_Perm_Prefixes (Prefix (N), New_Perm);
begin
if C = null then
+
-- We went through a function call, do nothing
return null;
end if;
- -- The permission of the returned node should be either W
- -- (because the recursive call sets <= Write_Only) or No
- -- (if another path has been moved with 'Access).
-
- pragma Assert (Permission (C) = No_Access
- or else Permission (C) = Write_Only);
-
- if Mode = Super_Move then
- -- The permission of the returned node should be No (thanks
- -- to the recursion).
-
- pragma Assert (Permission (C) = No_Access);
- null;
- end if;
-
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Record_Component);
begin
if Selected_C = null then
- -- If the hash table returns no element, then we fall
- -- into the part of Other_Components.
- pragma Assert (Is_Tagged_Type (Etype (Prefix (N))));
-
- Selected_C := Other_Components (C);
- end if;
-
- pragma Assert (Selected_C /= null);
-
- -- The Selected_C can have permissions:
- -- RW : first move in this path
- -- W : Already other moves in this path
- -- No : Already other moves with 'Access
-
- pragma Assert (Permission (Selected_C) /= Read_Only);
- if Mode = Super_Move then
- Selected_C.all.Tree.Permission := No_Access;
- else
- Selected_C.all.Tree.Permission :=
- Glb (Write_Only, Permission (Selected_C));
-
+ Selected_C := Other_Components (C);
end if;
+ pragma Assert (Selected_C /= null);
+ Selected_C.all.Tree.Permission := New_Perm;
return Selected_C;
end;
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace the node with
Hashtbl : Perm_Tree_Maps.Instance;
- -- We are in Move or Super_Move mode, hence we can assume
- -- that the Children_permission is RW, given that there
- -- are no other paths that could have been moved.
-
- pragma Assert (Children_Permission (C) = Read_Write);
-
- -- We create the unrolled nodes, that will all have RW
- -- permission given that we are in move mode. We will
- -- then set the right node to W.
+ -- We create the unrolled nodes, that will all have same
+ -- permission than parent.
- Son : Perm_Tree_Access;
+ Son : Perm_Tree_Access;
+ Children_Perm : constant Perm_Kind :=
+ Children_Permission (C);
begin
-- We change the current node from Entire_Object to
-- hash table as component list.
C.all.Tree :=
- (Kind => Record_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Component => Hashtbl,
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Component => Hashtbl,
Other_Components =>
new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => True,
- Permission => Read_Write,
- Children_Permission => Read_Write)
+ Permission => Children_Perm,
+ Children_Permission => Children_Perm)
));
-- We fill the hash table with all sons of the record,
-- with basic Entire_Objects nodes.
+
Elem := First_Component_Or_Discriminant
(Etype (Prefix (N)));
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Deep (Etype (Elem)),
- Permission => Read_Write,
- Children_Permission => Read_Write));
-
- Perm_Tree_Maps.Set
- (C.all.Tree.Component, Elem, Son);
+ Permission => Children_Perm,
+ Children_Permission => Children_Perm));
+ Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
Next_Component_Or_Discriminant (Elem);
end loop;
-
- -- Now we set the right field to Write_Only or No_Access
- -- depending on mode, and then we return the tree to the
- -- sons, so that the recursion can continue.
+ -- Now we set the right field to Borrowed, and then we
+ -- return the tree to the sons, so that the recursion can
+ -- continue.
declare
Selected_Component : constant Entity_Id :=
Entity (Selector_Name (N));
-
Selected_C : Perm_Tree_Access :=
Perm_Tree_Maps.Get
(Component (C), Selected_Component);
end if;
pragma Assert (Selected_C /= null);
-
- -- Given that this is a newly created Select_C, we can
- -- safely assume that its permission is Read_Write.
-
- pragma Assert (Permission (Selected_C) =
- Read_Write);
-
- if Mode = Super_Move then
- Selected_C.all.Tree.Permission := No_Access;
- else
- Selected_C.all.Tree.Permission := Write_Only;
- end if;
-
+ Selected_C.all.Tree.Permission := New_Perm;
return Selected_C;
end;
end;
-- We set the permission tree of its prefix, and then we extract
-- from the returned pointer the subtree and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree
- -- at one step.
+ -- permission to it, if unfolded. If folded, we unroll the tree in
+ -- one step.
when N_Indexed_Component
| N_Slice
=>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (Prefix (N), Mode);
+ Set_Perm_Prefixes (Prefix (N), New_Perm);
begin
if C = null then
+
-- We went through a function call, do nothing
return null;
end if;
- -- The permission of the returned node should be either
- -- W (because the recursive call sets <= Write_Only)
- -- or No (if another path has been moved with 'Access)
-
- if Mode = Super_Move then
- pragma Assert (Permission (C) = No_Access);
- null;
- else
- pragma Assert (Permission (C) = Write_Only
- or else Permission (C) = No_Access);
- null;
- end if;
-
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Array_Component);
if Kind (C) = Array_Component then
+
-- The tree is unfolded. We just modify the permission and
-- return the elem subtree.
- if Get_Elem (C) = null then
- -- Hash_Table_Error
- raise Program_Error;
- end if;
-
- -- The Get_Elem can have permissions :
- -- RW : first move in this path
- -- W : Already other moves in this path
- -- No : Already other moves with 'Access
-
- pragma Assert (Permission (Get_Elem (C)) /= Read_Only);
-
- if Mode = Super_Move then
- C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
- else
- C.all.Tree.Get_Elem.all.Tree.Permission :=
- Glb (Write_Only, Permission (Get_Elem (C)));
- end if;
-
+ pragma Assert (Get_Elem (C) /= null);
+ C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
return Get_Elem (C);
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace node with Array_Component.
- -- We are in move mode, hence we can assume that the
- -- Children_permission is RW.
-
- pragma Assert (Children_Permission (C) = Read_Write);
-
Son : Perm_Tree_Access;
begin
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Read_Write,
- Children_Permission => Read_Write));
+ Permission => New_Perm,
+ Children_Permission => Children_Permission (C)));
- if Mode = Super_Move then
- Son.all.Tree.Permission := No_Access;
- else
- Son.all.Tree.Permission := Write_Only;
- end if;
+ -- Children_Permission => Children_Permission (C)
+ -- this line should be checked maybe New_Perm
+ -- instead of Children_Permission (C)
-- We change the current node from Entire_Object
-- to Array_Component with same permission and the
C.all.Tree := (Kind => Array_Component,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
+ Permission => New_Perm,
Get_Elem => Son);
-
return Get_Elem (C);
end;
else
when N_Explicit_Dereference =>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (Prefix (N), Move);
+ Set_Perm_Prefixes (Prefix (N), New_Perm);
begin
if C = null then
- -- We went through a function call: do nothing
+
+ -- We went through a function call. Do nothing.
return null;
end if;
- -- The permission of the returned node should be only
- -- W (because the recursive call sets <= Write_Only)
- -- No is NOT POSSIBLE here
-
- pragma Assert (Permission (C) = Write_Only);
-
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Reference);
if Kind (C) = Reference then
+
-- The tree is unfolded. We just modify the permission and
-- return the elem subtree.
- if Get_All (C) = null then
- -- Hash_Table_Error
- raise Program_Error;
- end if;
-
- -- The Get_All can have permissions :
- -- RW : first move in this path
- -- W : Already other moves in this path
- -- No : Already other moves with 'Access
-
- pragma Assert (Permission (Get_All (C)) /= Read_Only);
-
- if Mode = Super_Move then
- C.all.Tree.Get_All.all.Tree.Permission := No_Access;
- else
- Get_All (C).all.Tree.Permission :=
- Glb (Write_Only, Permission (Get_All (C)));
- end if;
+ pragma Assert (Get_All (C) /= null);
+ C.all.Tree.Get_All.all.Tree.Permission := New_Perm;
return Get_All (C);
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace the node with Reference.
- -- We are in Move or Super_Move mode, hence we can assume
- -- that the Children_permission is RW.
-
- pragma Assert (Children_Permission (C) = Read_Write);
-
Son : Perm_Tree_Access;
begin
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => Read_Write,
- Children_Permission => Read_Write));
-
- if Mode = Super_Move then
- Son.all.Tree.Permission := No_Access;
- else
- Son.all.Tree.Permission := Write_Only;
- end if;
+ Permission => New_Perm,
+ Children_Permission => Children_Permission (C)));
-- We change the current node from Entire_Object to
- -- Reference with Write_Only and the previous son.
+ -- Reference with Borrowed and the previous son.
pragma Assert (Is_Node_Deep (C));
-
C.all.Tree := (Kind => Reference,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Write_Only,
- -- Write_only is equal to C.Permission
+ Permission => New_Perm,
Get_All => Son);
-
return Get_All (C);
end;
+
else
raise Program_Error;
end if;
when others =>
raise Program_Error;
end case;
+ end Set_Perm_Prefixes;
- end Set_Perm_Prefixes_Move;
-
- -------------------------------
- -- Set_Perm_Prefixes_Observe --
- -------------------------------
+ ------------------------------
+ -- Set_Perm_Prefixes_Borrow --
+ ------------------------------
- function Set_Perm_Prefixes_Observe
- (N : Node_Id)
- return Perm_Tree_Access
+ function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
is
begin
- pragma Assert (Current_Checking_Mode = Observe);
-
+ pragma Assert (Current_Checking_Mode = Borrow);
case Nkind (N) is
- -- Base identifier. Set permission to R.
when N_Identifier
| N_Expanded_Name
- | N_Defining_Identifier
=>
declare
- P : Node_Id;
- C : Perm_Tree_Access;
+ P : constant Node_Id := Entity (N);
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (P));
+ pragma Assert (C /= null);
begin
- if Nkind (N) = N_Defining_Identifier then
- P := N;
- else
- P := Entity (N);
- end if;
-
- C := Get (Current_Perm_Env, Unique_Entity (P));
-- Setting the initialization map to True, so that this
-- variable cannot be ignored anymore when looking at end
-- of elaboration of package.
Set (Current_Initialization_Map, Unique_Entity (P), True);
-
- if C = null then
- -- No null possible here, there are no parents for the path.
- -- This means we are using a global variable without adding
- -- it in environment with a global aspect.
-
- Illegal_Global_Usage (N);
- end if;
-
- C.all.Tree.Permission := Glb (Read_Only, Permission (C));
-
+ C.all.Tree.Permission := Borrowed;
return C;
end;
| N_Unchecked_Type_Conversion
| N_Qualified_Expression
=>
- return Set_Perm_Prefixes_Observe (Expression (N));
+ return Set_Perm_Prefixes_Borrow (Expression (N));
- when N_Parameter_Specification =>
+ when N_Parameter_Specification
+ | N_Defining_Identifier
+ =>
raise Program_Error;
-- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer our subtree and assign an adequate
+ -- our subtree from the returned pointer and assign an adequate
-- permission to it, if unfolded. If folded, we unroll the tree
- -- at one step.
+ -- in one step.
when N_Selected_Component =>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Observe (Prefix (N));
+ Set_Perm_Prefixes_Borrow (Prefix (N));
begin
if C = null then
+
-- We went through a function call, do nothing
return null;
end if;
+ -- The permission of the returned node should be No
+
+ pragma Assert (Permission (C) = Borrowed);
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Record_Component);
if Kind (C) = Record_Component then
+
-- The tree is unfolded. We just modify the permission and
- -- return the record subtree. We put the permission to the
- -- glb of read_only and its current permission, to consider
- -- the case of observing x.y while x.z has been moved. Then
- -- x should be No_Access.
+ -- return the record subtree.
declare
Selected_Component : constant Entity_Id :=
Entity (Selector_Name (N));
-
Selected_C : Perm_Tree_Access :=
Perm_Tree_Maps.Get
(Component (C), Selected_Component);
end if;
pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission :=
- Glb (Read_Only, Permission (Selected_C));
-
+ Selected_C.all.Tree.Permission := Borrowed;
return Selected_C;
end;
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace the node with
Hashtbl : Perm_Tree_Maps.Instance;
- -- We create the unrolled nodes, that will all have RW
- -- permission given that we are in move mode. We will
- -- then set the right node to W.
+ -- We create the unrolled nodes, that will all have same
+ -- permission than parent.
Son : Perm_Tree_Access;
-
- Child_Perm : constant Perm_Kind :=
+ ChildrenPerm : constant Perm_Kind :=
Children_Permission (C);
begin
-- hash table as component list.
C.all.Tree :=
- (Kind => Record_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Component => Hashtbl,
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Component => Hashtbl,
Other_Components =>
new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => True,
- Permission => Child_Perm,
- Children_Permission => Child_Perm)
+ Permission => ChildrenPerm,
+ Children_Permission => ChildrenPerm)
));
-- We fill the hash table with all sons of the record,
-- with basic Entire_Objects nodes.
+
Elem := First_Component_Or_Discriminant
(Etype (Prefix (N)));
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Deep (Etype (Elem)),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
-
- Perm_Tree_Maps.Set
- (C.all.Tree.Component, Elem, Son);
-
+ Permission => ChildrenPerm,
+ Children_Permission => ChildrenPerm));
+ Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
Next_Component_Or_Discriminant (Elem);
end loop;
- -- Now we set the right field to Read_Only. and then we
+ -- Now we set the right field to Borrowed, and then we
-- return the tree to the sons, so that the recursion can
-- continue.
declare
Selected_Component : constant Entity_Id :=
Entity (Selector_Name (N));
-
- Selected_C : Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
begin
if Selected_C = null then
end if;
pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission :=
- Glb (Read_Only, Child_Perm);
-
+ Selected_C.all.Tree.Permission := Borrowed;
return Selected_C;
end;
end;
+
else
raise Program_Error;
end if;
end;
- -- We set the permission tree of its prefix, and then we extract from
- -- the returned pointer the subtree and assign an adequate permission
- -- to it, if unfolded. If folded, we unroll the tree at one step.
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer the subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree in
+ -- one step.
when N_Indexed_Component
| N_Slice
=>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Observe (Prefix (N));
+ Set_Perm_Prefixes_Borrow (Prefix (N));
begin
if C = null then
+
-- We went through a function call, do nothing
return null;
end if;
+ pragma Assert (Permission (C) = Borrowed);
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Array_Component);
if Kind (C) = Array_Component then
+
-- The tree is unfolded. We just modify the permission and
-- return the elem subtree.
pragma Assert (Get_Elem (C) /= null);
-
- C.all.Tree.Get_Elem.all.Tree.Permission :=
- Glb (Read_Only, Permission (Get_Elem (C)));
-
+ C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed;
return Get_Elem (C);
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace node with Array_Component.
Son : Perm_Tree_Access;
- Child_Perm : constant Perm_Kind :=
- Glb (Read_Only, Children_Permission (C));
-
begin
Son := new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
+ Permission => Borrowed,
+ Children_Permission => Children_Permission (C)));
-- We change the current node from Entire_Object
-- to Array_Component with same permission and the
C.all.Tree := (Kind => Array_Component,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
+ Permission => Borrowed,
Get_Elem => Son);
-
return Get_Elem (C);
end;
end if;
end;
- -- We set the permission tree of its prefix, and then we extract from
- -- the returned pointer the subtree and assign an adequate permission
- -- to it, if unfolded. If folded, we unroll the tree at one step.
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer the subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
when N_Explicit_Dereference =>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Observe (Prefix (N));
+ Set_Perm_Prefixes_Borrow (Prefix (N));
begin
if C = null then
- -- We went through a function call, do nothing
+
+ -- We went through a function call. Do nothing.
return null;
end if;
+ -- The permission of the returned node should be No
+
+ pragma Assert (Permission (C) = Borrowed);
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Reference);
if Kind (C) = Reference then
+
-- The tree is unfolded. We just modify the permission and
-- return the elem subtree.
pragma Assert (Get_All (C) /= null);
-
- C.all.Tree.Get_All.all.Tree.Permission :=
- Glb (Read_Only, Permission (Get_All (C)));
-
+ C.all.Tree.Get_All.all.Tree.Permission := Borrowed;
return Get_All (C);
+
elsif Kind (C) = Entire_Object then
declare
-- Expand the tree. Replace the node with Reference.
Son : Perm_Tree_Access;
- Child_Perm : constant Perm_Kind :=
- Glb (Read_Only, Children_Permission (C));
-
begin
Son := new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
+ Permission => Borrowed,
+ Children_Permission => Children_Permission (C)));
-- We change the current node from Entire_Object to
- -- Reference with Write_Only and the previous son.
+ -- Reference with Borrowed and the previous son.
pragma Assert (Is_Node_Deep (C));
-
C.all.Tree := (Kind => Reference,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
+ Permission => Borrowed,
Get_All => Son);
-
return Get_All (C);
end;
+
else
raise Program_Error;
end if;
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);
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;
(Tree =>
(Kind => Entire_Object,
Is_Node_Deep => Is_Deep (Etype (Id)),
- Permission => Read_Write,
- Children_Permission => Read_Write));
+ Permission => Unrestricted,
+ Children_Permission => Unrestricted));
case Mode is
- when E_In_Parameter =>
- -- Borrowed IN: RW for everybody
+ -- All out and in out parameters are considered to be unrestricted.
+ -- They are whether borrowed or moved. Ada Rules would restrict
+ -- these permissions further. For example an in parameter cannot
+ -- be written.
- if Is_Borrowed_In (Id) and not Global_Var then
- Elem.all.Tree.Permission := Read_Write;
- Elem.all.Tree.Children_Permission := Read_Write;
+ -- In the following we deal with in parameters that can be observed.
+ -- We only consider the observing cases.
- -- Observed IN: R for everybody
+ when E_In_Parameter =>
- else
- Elem.all.Tree.Permission := Read_Only;
- Elem.all.Tree.Children_Permission := Read_Only;
- end if;
+ -- Handling global variables as in parameters here
+ -- Remove the following condition once decided how globals
+ -- should be considered.
+
+ if not Global_Var then
+ if (Is_Access_Type (Etype (Id))
+ and then Is_Access_Constant (Etype (Id))
+ and then Is_Anonymous_Access_Type (Etype (Id)))
+ or else
+ (not Is_Access_Type (Etype (Id))
+ and then Is_Deep (Etype (Id))
+ and then not Is_Anonymous_Access_Type (Etype (Id)))
+ then
+ Elem.all.Tree.Permission := Observed;
+ Elem.all.Tree.Children_Permission := Observed;
- -- OUT: borrow, but callee has W only
+ else
+ Elem.all.Tree.Permission := Unrestricted;
+ Elem.all.Tree.Children_Permission := Unrestricted;
+ end if;
- when E_Out_Parameter =>
- Elem.all.Tree.Permission := Write_Only;
- Elem.all.Tree.Children_Permission := Write_Only;
+ else
+ Elem.all.Tree.Permission := Observed;
+ Elem.all.Tree.Children_Permission := Observed;
+ end if;
- -- IN OUT: borrow and callee has RW
+ -- When out or in/out formal or global parameters, we set them to
+ -- the Unrestricted state. "We want to be able to assume that all
+ -- relevant writable globals are unrestricted when a subprogram
+ -- starts executing". Formal parameters of mode out or in/out
+ -- are whether Borrowers or the targets of a move operation:
+ -- they start theirs lives in the subprogram as Unrestricted.
- when E_In_Out_Parameter =>
- Elem.all.Tree.Permission := Read_Write;
- Elem.all.Tree.Children_Permission := Read_Write;
+ when others =>
+ Elem.all.Tree.Permission := Unrestricted;
+ Elem.all.Tree.Children_Permission := Unrestricted;
end case;
Set (Current_Perm_Env, Id, Elem);
-- 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
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;
projects / gcc.git / commitdiff