--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S E M _ S P A R K --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2017, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+with Atree; use Atree;
+with Einfo; use Einfo;
+with Errout; use Errout;
+with Namet; use Namet;
+with Nlists; use Nlists;
+with Opt; use Opt;
+with Osint; use Osint;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sem_Aux; use Sem_Aux;
+with Sinfo; use Sinfo;
+with Snames; use Snames;
+with Treepr; use Treepr;
+
+with Ada.Unchecked_Deallocation;
+with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
+
+package body Sem_SPARK is
+
+ -------------------------------------------------
+ -- Handling of Permissions Associated to Paths --
+ -------------------------------------------------
+
+ package Permissions is
+ Elaboration_Context_Max : constant := 1009;
+ -- The hash range
+
+ type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
+
+ 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_Tree_Wrapper;
+
+ type Perm_Tree_Access is access Perm_Tree_Wrapper;
+ -- A tree of permissions is defined, where the root is a whole object
+ -- and tree branches follow access paths in memory. As Perm_Tree is a
+ -- discriminated record, a wrapper type is used for the access type
+ -- designating a subtree, to make it unconstrained so that it can be
+ -- updated.
+
+ -- Nodes in the permission tree are of different kinds
+
+ type Path_Kind is
+ (Entire_Object, -- Scalar object, or folded object of any type
+ Reference, -- Unfolded object of access type
+ Array_Component, -- Unfolded object of array type
+ Record_Component -- Unfolded object of record type
+ );
+
+ package Perm_Tree_Maps is new Simple_HTable
+ (Header_Num => Elaboration_Context_Index,
+ Key => Node_Id,
+ Element => Perm_Tree_Access,
+ No_Element => null,
+ Hash => Elaboration_Context_Hash,
+ Equal => "=");
+ -- The instantation of a hash table, with keys being nodes and values
+ -- being pointers to trees. This is used to reference easily all
+ -- extensions of a Record_Component node (that can have name x, y, ...).
+
+ -- 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
+
+ Is_Node_Deep : Boolean;
+ -- Whether this node is of a deep type, to be used when moving the
+ -- 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
+ -- field Children_Permission specifies a permission for every
+ -- extension of that node if that permission is different from
+ -- the node's permission.
+
+ 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 =>
+ Get_All : Perm_Tree_Access;
+
+ -- Unfolded path of array type. The permission of the elements is
+ -- given in Get_Elem.
+
+ when Array_Component =>
+ Get_Elem : Perm_Tree_Access;
+
+ -- Unfolded path of record type. The permission of the regular
+ -- components is given in Component. The permission of unknown
+ -- components (for objects of tagged type) is given in
+ -- Other_Components.
+
+ when Record_Component =>
+ Component : Perm_Tree_Maps.Instance;
+ Other_Components : Perm_Tree_Access;
+ end case;
+ end record;
+
+ type Perm_Tree_Wrapper is record
+ Tree : Perm_Tree;
+ end record;
+ -- We use this wrapper in order to have unconstrained discriminants
+
+ type Perm_Env is new Perm_Tree_Maps.Instance;
+ -- The definition of a permission environment for the analysis. This
+ -- is just a hash table of permission trees, each of them rooted with
+ -- an Identifier/Expanded_Name.
+
+ type Perm_Env_Access is access Perm_Env;
+ -- Access to permission environments
+
+ package Env_Maps is new Simple_HTable
+ (Header_Num => Elaboration_Context_Index,
+ Key => Entity_Id,
+ Element => Perm_Env_Access,
+ No_Element => null,
+ Hash => Elaboration_Context_Hash,
+ Equal => "=");
+ -- The instantiation of a hash table whose elements are permission
+ -- environments. This hash table is used to save the environments at
+ -- the entry of each loop, with the key being the loop label.
+
+ type Env_Backups is new Env_Maps.Instance;
+ -- The type defining the hash table saving the environments at the entry
+ -- of each loop.
+
+ package Boolean_Variables_Maps is new Simple_HTable
+ (Header_Num => Elaboration_Context_Index,
+ Key => Entity_Id,
+ Element => Boolean,
+ No_Element => False,
+ Hash => Elaboration_Context_Hash,
+ Equal => "=");
+ -- These maps allow tracking the variables that have been declared but
+ -- never used anywhere in the source code. Especially, we do not raise
+ -- an error if the variable stays write-only and is declared at package
+ -- level, because there is no risk that the variable has been moved,
+ -- because it has never been used.
+
+ type Initialization_Map is new Boolean_Variables_Maps.Instance;
+
+ --------------------
+ -- Simple Getters --
+ --------------------
+
+ -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
+ -- that's only for the top access, as otherwise this reverses the order
+ -- in accesses visually.
+
+ function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
+ function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
+ function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
+ function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
+ function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
+ function Kind (T : Perm_Tree_Access) return Path_Kind;
+ function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access;
+ function Permission (T : Perm_Tree_Access) return Perm_Kind;
+
+ -----------------------
+ -- Memory Management --
+ -----------------------
+
+ procedure Copy_Env
+ (From : Perm_Env;
+ To : in out Perm_Env);
+ -- Procedure to copy a permission environment
+
+ procedure Copy_Init_Map
+ (From : Initialization_Map;
+ To : in out Initialization_Map);
+ -- Procedure to copy an initialization map
+
+ procedure Copy_Tree
+ (From : Perm_Tree_Access;
+ To : Perm_Tree_Access);
+ -- Procedure to copy a permission tree
+
+ procedure Free_Env
+ (PE : in out Perm_Env);
+ -- Procedure to free a permission environment
+
+ procedure Free_Perm_Tree
+ (PT : in out Perm_Tree_Access);
+ -- Procedure to free a permission tree
+
+ --------------------
+ -- Error Messages --
+ --------------------
+
+ procedure Perm_Mismatch
+ (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
+ -- is the node on which the error is reported.
+
+ end Permissions;
+
+ package body Permissions is
+
+ -------------------------
+ -- Children_Permission --
+ -------------------------
+
+ function Children_Permission
+ (T : Perm_Tree_Access)
+ return Perm_Kind
+ is
+ begin
+ return T.all.Tree.Children_Permission;
+ end Children_Permission;
+
+ ---------------
+ -- Component --
+ ---------------
+
+ function Component
+ (T : Perm_Tree_Access)
+ return Perm_Tree_Maps.Instance
+ is
+ begin
+ return T.all.Tree.Component;
+ end Component;
+
+ --------------
+ -- Copy_Env --
+ --------------
+
+ 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;
+
+ begin
+ Reset (To);
+ Key_From := Get_First_Key (From);
+ while Key_From.Present loop
+ Comp_From := Get (From, Key_From.K);
+ pragma Assert (Comp_From /= null);
+
+ Son := new Perm_Tree_Wrapper;
+ Copy_Tree (Comp_From, Son);
+
+ Set (To, Key_From.K, Son);
+ Key_From := Get_Next_Key (From);
+ end loop;
+ end Copy_Env;
+
+ -------------------
+ -- Copy_Init_Map --
+ -------------------
+
+ procedure Copy_Init_Map
+ (From : Initialization_Map;
+ To : in out Initialization_Map)
+ is
+ Comp_From : Boolean;
+ Key_From : Boolean_Variables_Maps.Key_Option;
+
+ begin
+ Reset (To);
+ Key_From := Get_First_Key (From);
+ while Key_From.Present loop
+ Comp_From := Get (From, Key_From.K);
+ Set (To, Key_From.K, Comp_From);
+ Key_From := Get_Next_Key (From);
+ end loop;
+ end Copy_Init_Map;
+
+ ---------------
+ -- Copy_Tree --
+ ---------------
+
+ 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 =>
+ declare
+ Comp_From : Perm_Tree_Access;
+ Key_From : Perm_Tree_Maps.Key_Option;
+ Son : Perm_Tree_Access;
+ Hash_Table : Perm_Tree_Maps.Instance;
+ begin
+ -- 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;
+
+ ------------------------------
+ -- Elaboration_Context_Hash --
+ ------------------------------
+
+ function Elaboration_Context_Hash
+ (Key : Entity_Id) return Elaboration_Context_Index
+ is
+ begin
+ return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
+ end Elaboration_Context_Hash;
+
+ --------------
+ -- Free_Env --
+ --------------
+
+ procedure Free_Env (PE : in out Perm_Env) is
+ CompO : Perm_Tree_Access;
+ begin
+ CompO := Get_First (PE);
+ while CompO /= null loop
+ Free_Perm_Tree (CompO);
+ CompO := Get_Next (PE);
+ end loop;
+ end Free_Env;
+
+ --------------------
+ -- Free_Perm_Tree --
+ --------------------
+
+ 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);
+ -- The deallocator for permission_trees
+
+ begin
+ case Kind (PT) is
+ when Entire_Object =>
+ Free_Perm_Tree_Dealloc (PT);
+
+ when Reference =>
+ Free_Perm_Tree (PT.all.Tree.Get_All);
+ Free_Perm_Tree_Dealloc (PT);
+
+ when Array_Component =>
+ Free_Perm_Tree (PT.all.Tree.Get_Elem);
+
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+
+ begin
+ 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);
+ Comp := Perm_Tree_Maps.Get_Next (Component (PT));
+ end loop;
+ end;
+ Free_Perm_Tree_Dealloc (PT);
+ end case;
+ end Free_Perm_Tree;
+
+ -------------
+ -- Get_All --
+ -------------
+
+ 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
+ begin
+ return T.all.Tree.Get_Elem;
+ end Get_Elem;
+
+ ------------------
+ -- Is_Node_Deep --
+ ------------------
+
+ 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
+ begin
+ return T.all.Tree.Kind;
+ end Kind;
+
+ ----------------------
+ -- Other_Components --
+ ----------------------
+
+ function Other_Components
+ (T : Perm_Tree_Access)
+ return Perm_Tree_Access
+ is
+ begin
+ return T.all.Tree.Other_Components;
+ end Other_Components;
+
+ ----------------
+ -- Permission --
+ ----------------
+
+ 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
+ begin
+ Error_Msg_N ("\expected at least `"
+ & Perm_Kind'Image (Exp_Perm) & "`, got `"
+ & Perm_Kind'Image (Act_Perm) & "`", N);
+ end Perm_Mismatch;
+
+ end Permissions;
+
+ use Permissions;
+
+ --------------------------------------
+ -- Analysis modes for AST traversal --
+ --------------------------------------
+
+ -- The different modes for analysis. This allows to checking whether a path
+ -- found in the code should be moved, borrowed, or observed.
+
+ type Checking_Mode is
+
+ (Read,
+ -- 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.
+
+ Assign,
+ -- Used for the target of an assignment, or an actual parameter with
+ -- mode OUT. Checks that paths have Write_Perm permission. After
+ -- assigning to a path, its permission is set to Read_Write.
+
+ Super_Move,
+ -- Enhanced moving semantics (under 'Access). Checks that paths have
+ -- Read_Write permission. After moving a path, its permission is set
+ -- to No_Access, as well as the permission of its extensions and the
+ -- permission of its prefixes up to the first Reference node.
+
+ Borrow_Out,
+ -- Used for actual OUT parameters. Checks that paths have Write_Perm
+ -- permission. After checking a path, its permission is set to Read_Only
+ -- when of a by-copy type, to No_Access otherwise. After the call, its
+ -- permission is set to Read_Write.
+
+ 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.
+ --
+ -- Also used for formal IN parameters
+ );
+
+ type Result_Kind is (Folded, Unfolded, Function_Call);
+ -- The type declaration to discriminate in the Perm_Or_Tree type
+
+ -- The result type of the function Get_Perm_Or_Tree. This returns either a
+ -- tree when it found the appropriate tree, or a permission when the search
+ -- finds a leaf and the subtree we are looking for is folded. In the last
+ -- case, we return instead the Children_Permission field of the leaf.
+
+ type Perm_Or_Tree (R : Result_Kind) is record
+ case R is
+ when Folded => Found_Permission : Perm_Kind;
+ when Unfolded => Tree_Access : Perm_Tree_Access;
+ when Function_Call => null;
+ end case;
+ end record;
+
+ -----------------------
+ -- 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.
+
+ procedure Check_Call_Statement (Call : Node_Id);
+
+ procedure Check_Callable_Body (Body_N : Node_Id);
+ -- 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.
+
+ 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_List (L : List_Id);
+ -- Calls Check_Node on each element of the list
+
+ procedure Check_Loop_Statement (Loop_N : Node_Id);
+
+ procedure Check_Node (N : Node_Id);
+ -- Main traversal procedure to check safe pointer usage. This procedure is
+ -- mutually recursive with the specialized procedures that follow.
+
+ procedure Check_Package_Body (Pack : Node_Id);
+
+ procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- This procedure takes a formal and an actual parameter and calls the
+ -- analyze node if the parameter is borrowed with mode in out, with the
+ -- appropriate Checking_Mode (Move).
+
+ procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id);
+ -- This procedure takes a formal and an actual parameter and calls
+ -- the analyze node if the parameter is observed, with the appropriate
+ -- Checking_Mode.
+
+ procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id);
+ -- This procedure takes a formal and an actual parameter and calls the
+ -- analyze node if the parameter is of mode out, with the appropriate
+ -- Checking_Mode.
+
+ procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id);
+ -- 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.
+
+ procedure Check_Statement (Stmt : Node_Id);
+
+ function Get_Perm (N : Node_Id) return Perm_Kind;
+ -- The function that takes a name as input and returns a permission
+ -- associated to it.
+
+ function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
+ -- This function gets a Node_Id and looks recursively to find the
+ -- appropriate subtree for that Node_Id. If the tree is folded on
+ -- that node, then it returns the permission given at the right level.
+
+ function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
+ -- This function gets a Node_Id and looks recursively to find the
+ -- 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.
+ pragma Unreferenced (Hp);
+
+ procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
+ pragma No_Return (Illegal_Global_Usage);
+ -- 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;
+ 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
+ -- entity and the permission that was expected, and adds an error message
+ -- with the appropriate values.
+
+ procedure Perm_Error_Subprogram_End
+ (E : Entity_Id;
+ Subp : Entity_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 end of subprograms. This function
+ -- is called with the node, its entity, the node of the returning function
+ -- and the permission that was expected, and adds an error message with the
+ -- appropriate values.
+
+ procedure Process_Path (N : Node_Id);
+
+ 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
+ -- permission.
+
+ procedure Return_Globals (Subp : Entity_Id);
+ -- Takes a subprogram as input, and checks that all borrowed global items
+ -- 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);
+ -- 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 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;
+ -- 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)
+ 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.
+
+ procedure Setup_Globals (Subp : Entity_Id);
+ -- Takes a subprogram as input, and sets up the environment by adding
+ -- global items with appropriate permissions.
+
+ procedure Setup_Parameter_Or_Global
+ (Id : Entity_Id;
+ Mode : Formal_Kind);
+ -- Auxiliary procedure to Setup_Parameters and Setup_Globals
+
+ procedure Setup_Parameters (Subp : Entity_Id);
+ -- Takes a subprogram as input, and sets up the environment by adding
+ -- formal parameters with appropriate permissions.
+
+ ----------------------
+ -- Global Variables --
+ ----------------------
+
+ Current_Perm_Env : Perm_Env;
+ -- The permission environment that is used for the analysis. This
+ -- environment can be saved, modified, reinitialized, but should be the
+ -- only one valid from which to extract the permissions of the paths in
+ -- scope. The analysis ensures at each point that this variables contains
+ -- a valid permission environment with all bindings in scope.
+
+ Current_Checking_Mode : Checking_Mode := Read;
+ -- The current analysis mode. This global variable indicates at each point
+ -- of the analysis whether the node being analyzed is moved, borrowed,
+ -- assigned, read, ... The full list of possible values can be found in
+ -- the declaration of type Checking_Mode.
+
+ Current_Loops_Envs : Env_Backups;
+ -- This variable contains saves of permission environments at each loop the
+ -- analysis entered. Each saved environment can be reached with the label
+ -- of the loop.
+
+ Current_Loops_Accumulators : Env_Backups;
+ -- This variable contains the environments used as accumulators for loops,
+ -- that consist of the merge of all environments at each exit point of
+ -- the loop (which can also be the entry point of the loop in the case of
+ -- non-infinite loops), each of them reachable from the label of the loop.
+ -- We require that the environment stored in the accumulator be less
+ -- restrictive than the saved environment at the beginning of the loop, and
+ -- the permission environment after the loop is equal to the accumulator.
+
+ Current_Initialization_Map : Initialization_Map;
+ -- This variable contains a map that binds each variable of the analyzed
+ -- source code to a boolean that becomes true whenever the variable is used
+ -- 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);
+
+ 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);
+
+ Iterate_Call_Outs (Call);
+ Check_Globals (Get_Pragma
+ (Get_Called_Entity (Call), Pragma_Global),
+ Borrow_Out);
+
+ Iterate_Call (Call);
+ Check_Globals (Get_Pragma
+ (Get_Called_Entity (Call), Pragma_Global), Move);
+
+ -- 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);
+
+ 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;
+
+ -------------------------
+ -- Check_Callable_Body --
+ -------------------------
+
+ procedure Check_Callable_Body (Body_N : Node_Id) is
+
+ 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);
+
+ begin
+ -- Check if SPARK pragma is not set to Off
+
+ if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
+ if Get_SPARK_Mode_From_Annotation
+ (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
+ then
+ return;
+ end if;
+ else
+ return;
+ end if;
+
+ -- Save environment and put a new one in place
+
+ Copy_Env (Current_Perm_Env, Saved_Env);
+
+ -- Save initialization map
+
+ Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
+
+ Current_Checking_Mode := Read;
+ Current_Perm_Env := New_Env;
+
+ -- Add formals and globals to the environment with adequate permissions
+
+ if Is_Subprogram_Or_Entry (Spec_Id) then
+ Setup_Parameters (Spec_Id);
+ Setup_Globals (Spec_Id);
+ end if;
+
+ -- Analyze the body of the function
+
+ Check_List (Declarations (Body_N));
+ Check_Node (Handled_Statement_Sequence (Body_N));
+
+ -- Check the read-write permissions of borrowed parameters/globals
+
+ 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);
+
+ 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
+
+ Current_Checking_Mode := Mode_Before;
+ end Check_Callable_Body;
+
+ -----------------------
+ -- Check_Declaration --
+ -----------------------
+
+ procedure Check_Declaration (Decl : Node_Id) is
+ begin
+ case N_Declaration'(Nkind (Decl)) is
+ when N_Full_Type_Declaration =>
+ -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
+ null;
+
+ when N_Object_Declaration =>
+ -- First move the right-hand side
+ Current_Checking_Mode := Move;
+ Check_Node (Expression (Decl));
+
+ declare
+ Elem : Perm_Tree_Access;
+
+ begin
+ Elem := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep =>
+ Is_Deep (Etype (Defining_Identifier (Decl))),
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+
+ -- If unitialized declaration, then set to Write_Only. If a
+ -- pointer declaration, it has a null default initialization.
+ if Nkind (Expression (Decl)) = N_Empty
+ and then not Has_Full_Default_Initialization
+ (Etype (Defining_Identifier (Decl)))
+ and then not Is_Access_Type
+ (Etype (Defining_Identifier (Decl)))
+ then
+ Elem.all.Tree.Permission := Write_Only;
+ Elem.all.Tree.Children_Permission := Write_Only;
+ 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;
+
+ when N_Subtype_Declaration =>
+ Check_Node (Subtype_Indication (Decl));
+
+ when N_Iterator_Specification =>
+ pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
+ null;
+
+ when N_Loop_Parameter_Specification =>
+ pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
+ null;
+
+ -- Checking should not be called directly on these nodes
+
+ when N_Component_Declaration
+ | N_Function_Specification
+ | N_Entry_Declaration
+ | N_Procedure_Specification
+ =>
+ raise Program_Error;
+
+ -- Ignored constructs for pointer checking
+
+ when N_Formal_Object_Declaration
+ | N_Formal_Type_Declaration
+ | N_Incomplete_Type_Declaration
+ | N_Private_Extension_Declaration
+ | N_Private_Type_Declaration
+ | N_Protected_Type_Declaration
+ =>
+ null;
+
+ -- The following nodes are rewritten by semantic analysis
+
+ when N_Expression_Function =>
+ raise Program_Error;
+ end case;
+ end Check_Declaration;
+
+ ----------------------
+ -- Check_Expression --
+ ----------------------
+
+ procedure Check_Expression (Expr : Node_Id) is
+ Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ begin
+ case N_Subexpr'(Nkind (Expr)) is
+ when N_Procedure_Call_Statement =>
+ 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));
+
+ -- Switch to read mode and then check the readability of each operand
+
+ when N_Op_Abs
+ | N_Op_Minus
+ | N_Op_Not
+ | N_Op_Plus
+ =>
+ pragma Assert (Is_Shallow (Etype (Expr)));
+ Current_Checking_Mode := Read;
+ Check_Node (Right_Opnd (Expr));
+
+ -- Forbid all deep expressions for Attribute ???
+
+ 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;
+
+ when Name_Last
+ | Name_First
+ =>
+ Current_Checking_Mode := Read;
+ Check_Node (Prefix (Expr));
+
+ when Name_Min =>
+ Current_Checking_Mode := Read;
+ Check_Node (Prefix (Expr));
+
+ when Name_Image =>
+ Check_Node (Prefix (Expr));
+
+ when Name_SPARK_Mode =>
+ null;
+
+ when Name_Value =>
+ Current_Checking_Mode := Read;
+ Check_Node (Prefix (Expr));
+
+ when Name_Update =>
+ Check_List (Expressions (Expr));
+ Check_Node (Prefix (Expr));
+
+ when Name_Pred
+ | Name_Succ
+ =>
+ Check_List (Expressions (Expr));
+ Check_Node (Prefix (Expr));
+
+ when Name_Length =>
+ Current_Checking_Mode := Read;
+ Check_Node (Prefix (Expr));
+
+ -- Any Attribute referring to the underlying memory is ignored
+ -- in the analysis. This means that taking the address of a
+ -- variable makes a silent alias that is not rejected by the
+ -- analysis.
+
+ when Name_Address
+ | Name_Alignment
+ | Name_Component_Size
+ | Name_First_Bit
+ | Name_Last_Bit
+ | Name_Size
+ | Name_Position
+ =>
+ null;
+
+ -- Attributes referring to types (get values from types), hence
+ -- no need to check either for borrows or any loans.
+
+ when Name_Base
+ | Name_Val
+ =>
+ null;
+
+ -- Other attributes that fall out of the scope of the analysis
+
+ when others =>
+ null;
+ end case;
+
+ when N_In =>
+ Current_Checking_Mode := Read;
+ Check_Node (Left_Opnd (Expr));
+ Check_Node (Right_Opnd (Expr));
+
+ when N_Not_In =>
+ Current_Checking_Mode := Read;
+ Check_Node (Left_Opnd (Expr));
+ Check_Node (Right_Opnd (Expr));
+
+ -- Switch to read mode and then check the readability of each operand
+
+ 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);
+
+ -- Copy environment, run on each branch, and then merge
+
+ when N_If_Expression =>
+ declare
+ Saved_Env : Perm_Env;
+
+ -- Accumulator for the different branches
+
+ New_Env : Perm_Env;
+
+ 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);
+
+ -- Here we have the original env in saved, current with a fresh
+ -- copy, and new aliased.
+
+ -- THEN PART
+
+ Next (Elmt);
+ Check_Node (Elmt);
+
+ -- Here the new_environment contains curr env after then block
+
+ -- ELSE part
+
+ -- Restore environment before if
+ Copy_Env (Current_Perm_Env,
+ New_Env);
+
+ Free_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);
+
+ Free_Env (New_Env);
+ Free_Env (Saved_Env);
+ end;
+
+ when N_Indexed_Component =>
+ Process_Path (Expr);
+
+ -- Analyze the expression that is getting qualified
+
+ when N_Qualified_Expression =>
+ Check_Node (Expression (Expr));
+
+ when N_Quantified_Expression =>
+ declare
+ Saved_Env : Perm_Env;
+ begin
+ Copy_Env (Current_Perm_Env, Saved_Env);
+ Current_Checking_Mode := Read;
+ Check_Node (Iterator_Specification (Expr));
+ Check_Node (Loop_Parameter_Specification (Expr));
+
+ Check_Node (Condition (Expr));
+ Free_Env (Current_Perm_Env);
+ Copy_Env (Saved_Env, Current_Perm_Env);
+ Free_Env (Saved_Env);
+ end;
+
+ -- Analyze the list of associations in the aggregate
+
+ when N_Aggregate =>
+ Check_List (Expressions (Expr));
+ Check_List (Component_Associations (Expr));
+
+ when N_Allocator =>
+ Check_Node (Expression (Expr));
+
+ when N_Case_Expression =>
+ declare
+ Saved_Env : Perm_Env;
+
+ -- 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);
+
+ -- Here we have the original env in saved, current with a fresh
+ -- copy, and new aliased.
+
+ -- First alternative
+
+ Check_Node (Elmt);
+ Next (Elmt);
+
+ 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);
+
+ 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);
+
+ 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));
+
+ when N_Range =>
+ Check_Node (Low_Bound (Expr));
+ Check_Node (High_Bound (Expr));
+
+ -- We arrived at a path. Process it.
+
+ when N_Selected_Component =>
+ Process_Path (Expr);
+
+ when N_Slice =>
+ Process_Path (Expr);
+
+ when N_Type_Conversion =>
+ Check_Node (Expression (Expr));
+
+ when N_Unchecked_Type_Conversion =>
+ Check_Node (Expression (Expr));
+
+ -- Checking should not be called directly on these nodes
+
+ when N_Target_Name =>
+ raise Program_Error;
+
+ -- Unsupported constructs in SPARK
+
+ when N_Delta_Aggregate =>
+ Error_Msg_N ("unsupported construct in SPARK", Expr);
+
+ -- Ignored constructs for pointer checking
+
+ when N_Character_Literal
+ | N_Null
+ | N_Numeric_Or_String_Literal
+ | N_Operator_Symbol
+ | N_Raise_Expression
+ | N_Raise_xxx_Error
+ =>
+ null;
+
+ -- The following nodes are never generated in GNATprove mode
+
+ when N_Expression_With_Actions
+ | N_Reference
+ | N_Unchecked_Expression
+ =>
+ raise Program_Error;
+
+ end case;
+ end Check_Expression;
+
+ -------------------
+ -- Check_Globals --
+ -------------------
+
+ procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) 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 (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 :=
+ Unique_Entity (Entity (The_Global));
+
+ Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+ begin
+ if Ekind (Ident_Elt) = E_Abstract_State then
+ return;
+ end if;
+
+ case Check_Mode is
+ when Read =>
+ case Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ Check_Node (The_Global);
+
+ when Name_Output
+ | Name_In_Out
+ =>
+ null;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+
+ when Observe =>
+ case Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ if not Is_Borrowed_In (Ident_Elt) then
+ -- Observed in
+
+ Current_Checking_Mode := Observe;
+ Check_Node (The_Global);
+ end if;
+
+ when others =>
+ null;
+
+ end case;
+
+ when Borrow_Out =>
+
+ case Mode is
+ when Name_Output =>
+ -- Borrowed out
+ Current_Checking_Mode := Borrow_Out;
+ Check_Node (The_Global);
+
+ when others =>
+ null;
+
+ end case;
+
+ when Move =>
+ case Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ if Is_Borrowed_In (Ident_Elt) then
+ -- Borrowed in
+
+ Current_Checking_Mode := Move;
+ else
+ -- Observed
+
+ return;
+ end if;
+
+ when Name_Output =>
+ return;
+
+ when Name_In_Out =>
+ -- Borrowed in out
+
+ Current_Checking_Mode := Move;
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ 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
+ and then Expressions (Expression (PAA)) /= No_List
+ then
+ -- global => (foo, bar)
+ -- Inputs
+ RHS := First (Expressions (Expression (PAA)));
+ while Present (RHS) loop
+ case Nkind (RHS) is
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ Process (Name_Input, RHS);
+
+ when N_Numeric_Or_String_Literal =>
+ Process (Name_Input, Original_Node (RHS));
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ RHS := Next (RHS);
+ end loop;
+
+ elsif Nkind (Expression (PAA)) = N_Aggregate
+ and then Component_Associations (Expression (PAA)) /= No_List
+ then
+ -- global => (mode => foo,
+ -- mode => (bar, baz))
+ -- A mixture of things
+
+ declare
+ CA : constant List_Id :=
+ Component_Associations (Expression (PAA));
+ begin
+ Row := First (CA);
+ 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));
+ while Present (RHS) loop
+ case Nkind (RHS) is
+ when N_Numeric_Or_String_Literal =>
+ Process (The_Mode, Original_Node (RHS));
+
+ when others =>
+ Process (The_Mode, RHS);
+
+ end case;
+ RHS := Next (RHS);
+ end loop;
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ Process (The_Mode, RHS);
+
+ when N_Null =>
+ null;
+
+ when N_Numeric_Or_String_Literal =>
+ Process (The_Mode, Original_Node (RHS));
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+
+ Row := Next (Row);
+ end loop;
+ end;
+
+ else
+ raise Program_Error;
+ end if;
+ end;
+ end Check_Globals;
+
+ ----------------
+ -- Check_List --
+ ----------------
+
+ procedure Check_List (L : List_Id) is
+ N : Node_Id;
+ begin
+ N := First (L);
+ while Present (N) loop
+ Check_Node (N);
+ Next (N);
+ end loop;
+ end Check_List;
+
+ --------------------------
+ -- Check_Loop_Statement --
+ --------------------------
+
+ 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));
+ Loop_Env : constant Perm_Env_Access := new Perm_Env;
+
+ begin
+ -- Save environment prior to the loop
+
+ Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
+
+ -- Add saved environment to loop environment
+
+ Set (Current_Loops_Envs, Loop_Name, Loop_Env);
+
+ -- If the loop is not a plain-loop, then it may either never be entered,
+ -- or it may be exited after a number of iterations. Hence add the
+ -- current permission environment as the initial loop exit environment.
+ -- Otherwise, the loop exit environment remains empty until it is
+ -- populated by analyzing exit statements.
+
+ 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);
+ end;
+ end if;
+
+ -- Analyze loop
+
+ 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
+ Exit_Env : constant Perm_Env_Access :=
+ Get (Current_Loops_Accumulators, Loop_Name);
+ begin
+ Free_Env (Current_Perm_Env);
+
+ -- In the normal case, Exit_Env is not null and we use it. In the
+ -- degraded case of a plain-loop without exit statements, Exit_Env is
+ -- null, and we use the initial permission environment at the start
+ -- of the loop to continue analysis. Any environment would be fine
+ -- here, since the code after the loop is dead code, but this way we
+ -- avoid spurious errors by having at least variables in scope inside
+ -- the environment.
+
+ if Exit_Env /= null then
+ Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
+ else
+ Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
+ end if;
+
+ Free_Env (Loop_Env.all);
+ Free_Env (Exit_Env.all);
+ end;
+ end Check_Loop_Statement;
+
+ ----------------
+ -- Check_Node --
+ ----------------
+
+ procedure Check_Node (N : Node_Id) is
+ Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration (N);
+
+ when N_Subexpr =>
+ Check_Expression (N);
+
+ when N_Subtype_Indication =>
+ Check_Node (Constraint (N));
+
+ when N_Body_Stub =>
+ Check_Node (Get_Body_From_Stub (N));
+
+ when N_Statement_Other_Than_Procedure_Call =>
+ Check_Statement (N);
+
+ when N_Package_Body =>
+ Check_Package_Body (N);
+
+ when N_Subprogram_Body
+ | N_Entry_Body
+ | N_Task_Body
+ =>
+ Check_Callable_Body (N);
+
+ when N_Protected_Body =>
+ Check_List (Declarations (N));
+
+ when N_Package_Declaration =>
+ declare
+ Spec : constant Node_Id := Specification (N);
+ begin
+ Current_Checking_Mode := Read;
+ Check_List (Visible_Declarations (Spec));
+ Check_List (Private_Declarations (Spec));
+
+ Return_Declarations (Visible_Declarations (Spec));
+ Return_Declarations (Private_Declarations (Spec));
+ end;
+
+ when N_Iteration_Scheme =>
+ Current_Checking_Mode := Read;
+ Check_Node (Condition (N));
+ Check_Node (Iterator_Specification (N));
+ Check_Node (Loop_Parameter_Specification (N));
+
+ when N_Case_Expression_Alternative =>
+ Current_Checking_Mode := Read;
+ Check_List (Discrete_Choices (N));
+ Current_Checking_Mode := Mode_Before;
+ Check_Node (Expression (N));
+
+ when N_Case_Statement_Alternative =>
+ Current_Checking_Mode := Read;
+ Check_List (Discrete_Choices (N));
+ Current_Checking_Mode := Mode_Before;
+ Check_List (Statements (N));
+
+ when N_Component_Association =>
+ Check_Node (Expression (N));
+
+ when N_Handled_Sequence_Of_Statements =>
+ Check_List (Statements (N));
+
+ when N_Parameter_Association =>
+ Check_Node (Explicit_Actual_Parameter (N));
+
+ when N_Range_Constraint =>
+ Check_Node (Range_Expression (N));
+
+ when N_Index_Or_Discriminant_Constraint =>
+ Check_List (Constraints (N));
+
+ -- Checking should not be called directly on these nodes
+
+ when N_Abortable_Part
+ | N_Accept_Alternative
+ | N_Access_Definition
+ | N_Access_Function_Definition
+ | N_Access_Procedure_Definition
+ | N_Access_To_Object_Definition
+ | N_Aspect_Specification
+ | N_Compilation_Unit
+ | N_Compilation_Unit_Aux
+ | N_Component_Clause
+ | N_Component_Definition
+ | N_Component_List
+ | N_Constrained_Array_Definition
+ | N_Contract
+ | N_Decimal_Fixed_Point_Definition
+ | N_Defining_Character_Literal
+ | N_Defining_Identifier
+ | N_Defining_Operator_Symbol
+ | N_Defining_Program_Unit_Name
+ | N_Delay_Alternative
+ | N_Derived_Type_Definition
+ | N_Designator
+ | N_Discriminant_Association
+ | N_Discriminant_Specification
+ | N_Elsif_Part
+ | N_Entry_Body_Formal_Part
+ | N_Enumeration_Type_Definition
+ | N_Entry_Call_Alternative
+ | N_Entry_Index_Specification
+ | N_Error
+ | N_Exception_Handler
+ | N_Floating_Point_Definition
+ | N_Formal_Decimal_Fixed_Point_Definition
+ | N_Formal_Derived_Type_Definition
+ | N_Formal_Discrete_Type_Definition
+ | N_Formal_Floating_Point_Definition
+ | N_Formal_Incomplete_Type_Definition
+ | N_Formal_Modular_Type_Definition
+ | N_Formal_Ordinary_Fixed_Point_Definition
+ | N_Formal_Private_Type_Definition
+ | N_Formal_Signed_Integer_Type_Definition
+ | N_Generic_Association
+ | N_Mod_Clause
+ | N_Modular_Type_Definition
+ | N_Ordinary_Fixed_Point_Definition
+ | N_Package_Specification
+ | N_Parameter_Specification
+ | N_Pragma_Argument_Association
+ | N_Protected_Definition
+ | N_Push_Pop_xxx_Label
+ | N_Real_Range_Specification
+ | N_Record_Definition
+ | N_SCIL_Dispatch_Table_Tag_Init
+ | N_SCIL_Dispatching_Call
+ | N_SCIL_Membership_Test
+ | N_Signed_Integer_Type_Definition
+ | N_Subunit
+ | N_Task_Definition
+ | N_Terminate_Alternative
+ | N_Triggering_Alternative
+ | N_Unconstrained_Array_Definition
+ | N_Unused_At_Start
+ | N_Unused_At_End
+ | N_Variant
+ | N_Variant_Part
+ =>
+ raise Program_Error;
+
+ -- Unsupported constructs in SPARK
+
+ when N_Iterated_Component_Association =>
+ Error_Msg_N ("unsupported construct in SPARK", N);
+
+ -- Ignored constructs for pointer checking
+
+ when N_Abstract_Subprogram_Declaration
+ | N_At_Clause
+ | N_Attribute_Definition_Clause
+ | N_Delta_Constraint
+ | N_Digits_Constraint
+ | N_Empty
+ | N_Enumeration_Representation_Clause
+ | N_Exception_Declaration
+ | N_Exception_Renaming_Declaration
+ | N_Formal_Package_Declaration
+ | N_Formal_Subprogram_Declaration
+ | N_Freeze_Entity
+ | N_Freeze_Generic_Entity
+ | N_Function_Instantiation
+ | N_Generic_Function_Renaming_Declaration
+ | N_Generic_Package_Declaration
+ | N_Generic_Package_Renaming_Declaration
+ | N_Generic_Procedure_Renaming_Declaration
+ | N_Generic_Subprogram_Declaration
+ | N_Implicit_Label_Declaration
+ | N_Itype_Reference
+ | N_Label
+ | N_Number_Declaration
+ | N_Object_Renaming_Declaration
+ | N_Others_Choice
+ | N_Package_Instantiation
+ | N_Package_Renaming_Declaration
+ | N_Pragma
+ | N_Procedure_Instantiation
+ | N_Record_Representation_Clause
+ | N_Subprogram_Declaration
+ | N_Subprogram_Renaming_Declaration
+ | N_Task_Type_Declaration
+ | N_Use_Package_Clause
+ | N_With_Clause
+ | N_Use_Type_Clause
+ | N_Validate_Unchecked_Conversion
+ =>
+ null;
+
+ -- The following nodes are rewritten by semantic analysis
+
+ when N_Single_Protected_Declaration
+ | N_Single_Task_Declaration
+ =>
+ raise Program_Error;
+ end case;
+
+ Current_Checking_Mode := Mode_Before;
+ end Check_Node;
+
+ ------------------------
+ -- Check_Package_Body --
+ ------------------------
+
+ procedure Check_Package_Body (Pack : Node_Id) is
+ Saved_Env : Perm_Env;
+ CorSp : Node_Id;
+
+ begin
+ if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
+ if Get_SPARK_Mode_From_Annotation
+ (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
+ then
+ return;
+ end if;
+ else
+ return;
+ end if;
+
+ CorSp := Parent (Corresponding_Spec (Pack));
+ while Nkind (CorSp) /= N_Package_Specification loop
+ CorSp := Parent (CorSp);
+ end loop;
+
+ Check_List (Visible_Declarations (CorSp));
+
+ -- Save environment
+
+ 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));
+
+ -- Check RW for every stateful variable (i.e. in declarations)
+
+ Return_Declarations (Private_Declarations (CorSp));
+ Return_Declarations (Visible_Declarations (CorSp));
+ Return_Declarations (Declarations (Pack));
+
+ -- Restore previous environment (i.e. delete every nonvisible
+ -- declaration) from environment.
+
+ Free_Env (Current_Perm_Env);
+ Copy_Env (Saved_Env,
+ Current_Perm_Env);
+ end Check_Package_Body;
+
+ -----------------
+ -- Check_Param --
+ -----------------
+
+ procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
+ 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
+
+ return;
+ end if;
+
+ when E_Out_Parameter =>
+ return;
+
+ when E_In_Out_Parameter =>
+ -- Borrowed in out
+
+ Current_Checking_Mode := Move;
+
+ end case;
+
+ Check_Node (Actual);
+
+ when Assign =>
+ case Formal_Kind'(Mode) is
+ when E_In_Parameter =>
+ null;
+
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
+ -- Borrowed out or in out
+
+ Process_Path (Actual);
+
+ end case;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ Current_Checking_Mode := Mode_Before;
+ end Check_Param;
+
+ --------------------------
+ -- Check_Param_Observes --
+ --------------------------
+
+ procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
+ Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+ begin
+ case Mode is
+ when E_In_Parameter =>
+ if not Is_Borrowed_In (Formal) then
+ -- Observed in
+
+ Current_Checking_Mode := Observe;
+ Check_Node (Actual);
+ end if;
+
+ when others =>
+ null;
+
+ end case;
+
+ Current_Checking_Mode := Mode_Before;
+ end Check_Param_Observes;
+
+ ----------------------
+ -- Check_Param_Outs --
+ ----------------------
+
+ procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
+ Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+
+ begin
+
+ case Mode is
+ when E_Out_Parameter =>
+ -- Borrowed out
+ Current_Checking_Mode := Borrow_Out;
+ Check_Node (Actual);
+
+ when others =>
+ null;
+
+ end case;
+
+ Current_Checking_Mode := Mode_Before;
+ end Check_Param_Outs;
+
+ ----------------------
+ -- Check_Param_Read --
+ ----------------------
+
+ procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
+
+ begin
+ pragma Assert (Current_Checking_Mode = Read);
+
+ case Formal_Kind'(Mode) is
+ when E_In_Parameter =>
+ Check_Node (Actual);
+
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
+ null;
+
+ end case;
+ end Check_Param_Read;
+
+ -------------------------
+ -- Check_Safe_Pointers --
+ -------------------------
+
+ procedure Check_Safe_Pointers (N : Node_Id) is
+
+ -- Local subprograms
+
+ procedure Check_List (L : List_Id);
+ -- Call the main analysis procedure on each element of the list
+
+ procedure Initialize;
+ -- Initialize global variables before starting the analysis of a body
+
+ ----------------
+ -- Check_List --
+ ----------------
+
+ procedure Check_List (L : List_Id) is
+ N : Node_Id;
+ begin
+ N := First (L);
+ while Present (N) loop
+ Check_Safe_Pointers (N);
+ Next (N);
+ end loop;
+ end Check_List;
+
+ ----------------
+ -- Initialize --
+ ----------------
+
+ procedure Initialize is
+ begin
+ Reset (Current_Loops_Envs);
+ Reset (Current_Loops_Accumulators);
+ Reset (Current_Perm_Env);
+ Reset (Current_Initialization_Map);
+ end Initialize;
+
+ -- 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));
+
+ when N_Package_Body
+ | N_Package_Declaration
+ | N_Subprogram_Body
+ =>
+ Prag := SPARK_Pragma (Defining_Entity (N));
+ if Present (Prag) then
+ if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
+ return;
+ else
+ Check_Node (N);
+ end if;
+
+ elsif Nkind (N) = N_Package_Body then
+ Check_List (Declarations (N));
+
+ elsif Nkind (N) = N_Package_Declaration then
+ Check_List (Private_Declarations (Specification (N)));
+ Check_List (Visible_Declarations (Specification (N)));
+ end if;
+
+ when others =>
+ null;
+ end case;
+ end Check_Safe_Pointers;
+
+ ---------------------
+ -- Check_Statement --
+ ---------------------
+
+ 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
+
+ when N_Assignment_Statement =>
+ if Is_Deep (Etype (Expression (Stmt))) then
+ Current_Checking_Mode := Move;
+ else
+ Current_Checking_Mode := Read;
+ end if;
+
+ Check_Node (Expression (Stmt));
+ Current_Checking_Mode := Assign;
+ Check_Node (Name (Stmt));
+
+ when N_Block_Statement =>
+ declare
+ Saved_Env : Perm_Env;
+
+ begin
+ -- Save environment
+
+ Copy_Env (Current_Perm_Env,
+ Saved_Env);
+
+ -- Analyze declarations and Handled_Statement_Sequences
+
+ Current_Checking_Mode := Read;
+ Check_List (Declarations (Stmt));
+ Check_Node (Handled_Statement_Sequence (Stmt));
+
+ -- Restore environment
+
+ Free_Env (Current_Perm_Env);
+ Copy_Env (Saved_Env,
+ Current_Perm_Env);
+ end;
+
+ when N_Case_Statement =>
+ declare
+ Saved_Env : Perm_Env;
+
+ -- Accumulator for the different branches
+
+ New_Env : Perm_Env;
+
+ Elmt : Node_Id := First (Alternatives (Stmt));
+
+ begin
+ Current_Checking_Mode := Read;
+ Check_Node (Expression (Stmt));
+ Current_Checking_Mode := Mode_Before;
+
+ -- Save environment
+
+ Copy_Env (Current_Perm_Env,
+ Saved_Env);
+
+ -- Here we have the original env in saved, current with a fresh
+ -- copy, and new aliased.
+
+ -- First alternative
+
+ Check_Node (Elmt);
+ Next (Elmt);
+
+ 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);
+
+ 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);
+
+ Free_Env (New_Env);
+ Free_Env (Saved_Env);
+ end;
+
+ when N_Delay_Relative_Statement =>
+ Check_Node (Expression (Stmt));
+
+ when N_Delay_Until_Statement =>
+ Check_Node (Expression (Stmt));
+
+ when N_Loop_Statement =>
+ Check_Loop_Statement (Stmt);
+
+ -- If deep type expression, then move, else read
+
+ when N_Simple_Return_Statement =>
+ case Nkind (Expression (Stmt)) is
+ when N_Empty =>
+ 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;
+
+ 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;
+ end if;
+
+ Check_Node (Expression (Stmt));
+ 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
+
+ when N_Exit_Statement =>
+ declare
+ Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
+
+ Saved_Accumulator : constant Perm_Env_Access :=
+ Get (Current_Loops_Accumulators, Loop_Name);
+
+ Environment_Copy : constant Perm_Env_Access :=
+ new Perm_Env;
+ begin
+
+ Copy_Env (Current_Perm_Env,
+ Environment_Copy.all);
+
+ if Saved_Accumulator = null then
+ Set (Current_Loops_Accumulators,
+ Loop_Name, Environment_Copy);
+ else
+ Merge_Envs (Saved_Accumulator.all,
+ Environment_Copy.all);
+ end if;
+ end;
+
+ -- Copy environment, run on each branch, and then merge
+
+ when N_If_Statement =>
+ declare
+ Saved_Env : Perm_Env;
+
+ -- Accumulator for the different branches
+
+ New_Env : Perm_Env;
+
+ begin
+
+ Check_Node (Condition (Stmt));
+
+ -- Save environment
+
+ 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);
+
+ 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);
+
+ 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;
+
+ -- ELSE part
+
+ -- Restore environment before if
+
+ 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);
+
+ Free_Env (New_Env);
+ Free_Env (Saved_Env);
+ end;
+
+ -- Unsupported constructs in SPARK
+
+ when N_Abort_Statement
+ | N_Accept_Statement
+ | N_Asynchronous_Select
+ | N_Code_Statement
+ | N_Conditional_Entry_Call
+ | N_Goto_Statement
+ | N_Requeue_Statement
+ | N_Selective_Accept
+ | N_Timed_Entry_Call
+ =>
+ Error_Msg_N ("unsupported construct in SPARK", Stmt);
+
+ -- Ignored constructs for pointer checking
+
+ when N_Null_Statement
+ | N_Raise_Statement
+ =>
+ null;
+
+ -- The following nodes are never generated in GNATprove mode
+
+ when N_Compound_Statement
+ | N_Free_Statement
+ =>
+ raise Program_Error;
+ end case;
+ end Check_Statement;
+
+ --------------
+ -- Get_Perm --
+ --------------
+
+ function Get_Perm (N : Node_Id) return Perm_Kind is
+ Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
+
+ begin
+ case Tree_Or_Perm.R is
+ when Folded =>
+ return Tree_Or_Perm.Found_Permission;
+
+ when Unfolded =>
+ pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+ return Permission (Tree_Or_Perm.Tree_Access);
+
+ -- We encoutered a function call, hence the memory area is fresh,
+ -- which means that the association permission is RW.
+
+ when Function_Call =>
+ return Read_Write;
+
+ end case;
+ end Get_Perm;
+
+ ----------------------
+ -- Get_Perm_Or_Tree --
+ ----------------------
+
+ function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+ begin
+ case Nkind (N) is
+
+ -- Base identifier. Normally those are the roots of the trees stored
+ -- in the permission environment.
+
+ when N_Defining_Identifier =>
+ raise Program_Error;
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ declare
+ P : constant Entity_Id := Entity (N);
+
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (P));
+
+ 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);
+
+ 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;
+ end;
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Get_Perm_Or_Tree (Expression (N));
+
+ -- Happening when we try to get the permission of a variable that
+ -- is a formal parameter. We get instead the defining identifier
+ -- associated with the parameter (which is the one that has been
+ -- stored for indexing).
+
+ when N_Parameter_Specification =>
+ return Get_Perm_Or_Tree (Defining_Identifier (N));
+
+ -- 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
+ -- and return it using the discriminant Folded.
+
+ when N_Selected_Component =>
+ declare
+ C : constant Perm_Or_Tree :=
+ Get_Perm_Or_Tree (Prefix (N));
+
+ begin
+ case C.R is
+ when Folded
+ | Function_Call
+ =>
+ return C;
+
+ when Unfolded =>
+ pragma Assert (C.Tree_Access /= null);
+
+ pragma Assert (Kind (C.Tree_Access) = Entire_Object
+ or else
+ Kind (C.Tree_Access) = Record_Component);
+
+ if Kind (C.Tree_Access) = Record_Component then
+ 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,
+ Tree_Access =>
+ Other_Components (C.Tree_Access));
+ else
+ return (R => Unfolded,
+ Tree_Access => Selected_C);
+ end if;
+ end;
+ 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
+ -- and return it using the discriminant Folded.
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ declare
+ C : constant Perm_Or_Tree :=
+ Get_Perm_Or_Tree (Prefix (N));
+
+ begin
+ case C.R is
+ when Folded
+ | Function_Call
+ =>
+ return C;
+
+ 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
+ -- and return it using the discriminant Folded.
+
+ when N_Explicit_Dereference =>
+ declare
+ C : constant Perm_Or_Tree :=
+ Get_Perm_Or_Tree (Prefix (N));
+
+ begin
+ case C.R is
+ when Folded
+ | Function_Call
+ =>
+ return C;
+
+ 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.
+
+ when N_Function_Call =>
+ return (R => Function_Call);
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Perm_Or_Tree;
+
+ -------------------
+ -- Get_Perm_Tree --
+ -------------------
+
+ function Get_Perm_Tree
+ (N : Node_Id)
+ return Perm_Tree_Access
+ is
+ begin
+ case Nkind (N) is
+
+ -- Base identifier. Normally those are the roots of the trees stored
+ -- in the permission environment.
+
+ when N_Defining_Identifier =>
+ raise Program_Error;
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ declare
+ P : constant Node_Id := Entity (N);
+
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (P));
+
+ begin
+ -- 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);
+ else
+ return C;
+ end if;
+ end;
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Get_Perm_Tree (Expression (N));
+
+ when N_Parameter_Specification =>
+ return Get_Perm_Tree (Defining_Identifier (N));
+
+ -- 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 it in one step.
+
+ when N_Selected_Component =>
+ declare
+ 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;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Record_Component);
+
+ if Kind (C) = Record_Component then
+ -- The tree is unfolded. We just return the subtree.
+
+ declare
+ Selected_Component : constant Entity_Id :=
+ Entity (Selector_Name (N));
+ Selected_C : constant Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ begin
+ 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
+ -- Record_Component.
+
+ Elem : Node_Id;
+
+ -- Create the unrolled nodes
+
+ Son : Perm_Tree_Access;
+
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (C);
+
+ begin
+
+ -- We change the current node from Entire_Object to
+ -- Record_Component with same permission and an empty
+ -- hash table as component list.
+
+ C.all.Tree :=
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Component => Perm_Tree_Maps.Nil,
+ Other_Components =>
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ -- Is_Node_Deep is true, to be conservative
+ Is_Node_Deep => True,
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm)
+ )
+ );
+
+ -- We fill the hash table with all sons of the record,
+ -- with basic Entire_Objects nodes.
+ Elem := First_Component_Or_Discriminant
+ (Etype (Prefix (N)));
+
+ while Present (Elem) loop
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Elem)),
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm));
+
+ Perm_Tree_Maps.Set
+ (C.all.Tree.Component, Elem, Son);
+
+ Next_Component_Or_Discriminant (Elem);
+ end loop;
+
+ -- 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 : constant Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ 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.
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Get_Perm_Tree (Prefix (N));
+
+ begin
+ if C = null then
+ -- If null then we went through a function call
+
+ 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.
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Children_Permission (C),
+ Children_Permission => Children_Permission (C)));
+
+ -- We change the current node from Entire_Object
+ -- to Array_Component with same permission and the
+ -- previously defined son.
+
+ C.all.Tree := (Kind => Array_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => 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.
+
+ when N_Explicit_Dereference =>
+ declare
+ C : Perm_Tree_Access;
+
+ begin
+ C := Get_Perm_Tree (Prefix (N));
+
+ if C = null then
+ -- If null, we went through a function call
+
+ return null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Reference);
+
+ if Kind (C) = Reference then
+ -- The tree is unfolded. We 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.
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (N)),
+ Permission => Children_Permission (C),
+ Children_Permission => Children_Permission (C)));
+
+ -- We change the current node from Entire_Object to
+ -- 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 =>
+ return null;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Perm_Tree;
+
+ ---------
+ -- Glb --
+ ---------
+
+ function Glb (P1, P2 : Perm_Kind) return Perm_Kind
+ is
+ begin
+ case P1 is
+ when No_Access =>
+ return No_Access;
+
+ when Read_Only =>
+ case P2 is
+ when No_Access
+ | Write_Only
+ =>
+ return No_Access;
+
+ when Read_Perm =>
+ return Read_Only;
+ end case;
+
+ when Write_Only =>
+ case P2 is
+ when No_Access
+ | Read_Only
+ =>
+ return No_Access;
+
+ when Write_Perm =>
+ return Write_Only;
+ end case;
+
+ when Read_Write =>
+ return P2;
+ end case;
+ end Glb;
+
+ ---------------
+ -- Has_Alias --
+ ---------------
+
+ function Has_Alias
+ (N : Node_Id)
+ return Boolean
+ is
+ function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
+ function Has_Alias_Deep (Typ : Entity_Id) return Boolean
+ is
+ Comp : Node_Id;
+ begin
+
+ if Is_Array_Type (Typ)
+ and then Has_Aliased_Components (Typ)
+ then
+ return True;
+
+ -- Note: Has_Aliased_Components applies only to arrays
+
+ elsif Is_Record_Type (Typ) then
+ -- It is possible to have an aliased discriminant, so they must be
+ -- checked along with normal components.
+
+ Comp := First_Component_Or_Discriminant (Typ);
+ while Present (Comp) loop
+ if Is_Aliased (Comp)
+ or else Is_Aliased (Etype (Comp))
+ then
+ return True;
+ end if;
+
+ if Has_Alias_Deep (Etype (Comp)) then
+ return True;
+ end if;
+
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
+ return False;
+ else
+ return Is_Aliased (Typ);
+ end if;
+ end Has_Alias_Deep;
+
+ begin
+ case Nkind (N) is
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ return Has_Alias_Deep (Etype (N));
+
+ when N_Defining_Identifier =>
+ return Has_Alias_Deep (Etype (N));
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Has_Alias (Expression (N));
+
+ when N_Parameter_Specification =>
+ return Has_Alias (Defining_Identifier (N));
+
+ when N_Selected_Component =>
+ case Nkind (Selector_Name (N)) is
+ when N_Identifier =>
+ if Is_Aliased (Entity (Selector_Name (N))) then
+ return True;
+ end if;
+
+ when others => null;
+
+ end case;
+
+ return Has_Alias (Prefix (N));
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ return Has_Alias (Prefix (N));
+
+ when N_Explicit_Dereference =>
+ return True;
+
+ when N_Function_Call =>
+ return False;
+
+ when N_Attribute_Reference =>
+ if Is_Deep (Etype (Prefix (N))) then
+ raise Program_Error;
+ end if;
+ return False;
+
+ when others =>
+ return False;
+ end case;
+ end Has_Alias;
+
+ -------------------------
+ -- Has_Array_Component --
+ -------------------------
+
+ function Has_Array_Component (N : Node_Id) return Boolean is
+ begin
+ case Nkind (N) is
+ -- Base identifier. There is no array component here.
+
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Defining_Identifier
+ =>
+ return False;
+
+ -- We check if the expression inside the conversion has an array
+ -- component.
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Has_Array_Component (Expression (N));
+
+ -- We check if the prefix has an array component
+
+ when N_Selected_Component =>
+ return Has_Array_Component (Prefix (N));
+
+ -- We found the array component, return True
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ return True;
+
+ -- We check if the prefix has an array component
+
+ when N_Explicit_Dereference =>
+ return Has_Array_Component (Prefix (N));
+
+ when N_Function_Call =>
+ return False;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Has_Array_Component;
+
+ ----------------------------
+ -- Has_Function_Component --
+ ----------------------------
+
+ function Has_Function_Component (N : Node_Id) return Boolean is
+ begin
+ case Nkind (N) is
+ -- Base identifier. There is no function component here.
+
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Defining_Identifier
+ =>
+ return False;
+
+ -- We check if the expression inside the conversion has a function
+ -- component.
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Has_Function_Component (Expression (N));
+
+ -- We check if the prefix has a function component
+
+ when N_Selected_Component =>
+ return Has_Function_Component (Prefix (N));
+
+ -- We check if the prefix has a function component
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ return Has_Function_Component (Prefix (N));
+
+ -- We check if the prefix has a function component
+
+ when N_Explicit_Dereference =>
+ return Has_Function_Component (Prefix (N));
+
+ -- We found the function component, return True
+
+ when N_Function_Call =>
+ return True;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ end Has_Function_Component;
+
+ --------
+ -- Hp --
+ --------
+
+ 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 Access_Kind =>
+ return True;
+
+ -- Just check the depth of its component type
+
+ when E_Array_Type
+ | E_Array_Subtype
+ =>
+ return Is_Deep (Component_Type (E));
+
+ when E_String_Literal_Subtype =>
+ return False;
+
+ -- Per RM 8.11 for class-wide types
+
+ when E_Class_Wide_Subtype
+ | E_Class_Wide_Type
+ =>
+ return True;
+
+ -- ??? What about hidden components
+
+ when E_Record_Type
+ | E_Record_Subtype
+ =>
+ declare
+ Elmt : Entity_Id;
+
+ begin
+ Elmt := First_Component_Or_Discriminant (E);
+ while Present (Elmt) loop
+ if Is_Deep (Etype (Elmt)) then
+ return True;
+ else
+ Next_Component_Or_Discriminant (Elmt);
+ end if;
+ end loop;
+
+ return False;
+ end;
+
+ when Private_Kind =>
+ if Is_Private_Entity_Mode_Off (E) then
+ return False;
+ else
+ if Present (Full_View (E)) then
+ return Is_Deep (Full_View (E));
+ else
+ return True;
+ end if;
+ end if;
+
+ when E_Incomplete_Type =>
+ return True;
+
+ when E_Incomplete_Subtype =>
+ return True;
+
+ -- No problem with synchronized types
+
+ when E_Protected_Type
+ | E_Protected_Subtype
+ | E_Task_Subtype
+ | E_Task_Type
+ =>
+ return False;
+
+ when E_Exception_Type =>
+ return False;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Is_Deep;
+
+ ----------------
+ -- Is_Shallow --
+ ----------------
+
+ function Is_Shallow (E : Entity_Id) return Boolean is
+ begin
+ pragma Assert (Is_Type (E));
+ return not Is_Deep (E);
+ end Is_Shallow;
+
+ ------------------
+ -- Loop_Of_Exit --
+ ------------------
+
+ function Loop_Of_Exit (N : Node_Id) return Entity_Id is
+ Nam : Node_Id := Name (N);
+ Stmt : Node_Id := N;
+ begin
+ if No (Nam) then
+ while Present (Stmt) loop
+ Stmt := Parent (Stmt);
+ if Nkind (Stmt) = N_Loop_Statement then
+ Nam := Identifier (Stmt);
+ exit;
+ end if;
+ end loop;
+ end if;
+ return Entity (Nam);
+ end Loop_Of_Exit;
+ ---------
+ -- Lub --
+ ---------
+
+ function Lub (P1, P2 : Perm_Kind) return Perm_Kind
+ is
+ begin
+ case P1 is
+ when No_Access =>
+ return P2;
+
+ when Read_Only =>
+ case P2 is
+ when No_Access
+ | Read_Only
+ =>
+ return Read_Only;
+
+ when Write_Perm =>
+ return Read_Write;
+ end case;
+
+ when Write_Only =>
+ case P2 is
+ when No_Access
+ | Write_Only
+ =>
+ return Write_Only;
+
+ when Read_Perm =>
+ return Read_Write;
+ end case;
+
+ when Read_Write =>
+ return Read_Write;
+ end case;
+ end Lub;
+
+ ----------------
+ -- Merge_Envs --
+ ----------------
+
+ procedure Merge_Envs
+ (Target : in out Perm_Env;
+ Source : in out Perm_Env)
+ is
+ procedure Merge_Trees
+ (Target : Perm_Tree_Access;
+ Source : Perm_Tree_Access);
+
+ procedure Merge_Trees
+ (Target : Perm_Tree_Access;
+ Source : Perm_Tree_Access)
+ is
+ procedure Apply_Glb_Tree
+ (A : Perm_Tree_Access;
+ P : Perm_Kind);
+
+ procedure Apply_Glb_Tree
+ (A : Perm_Tree_Access;
+ P : Perm_Kind)
+ is
+ begin
+ A.all.Tree.Permission := Glb (Permission (A), P);
+
+ case Kind (A) is
+ when Entire_Object =>
+ A.all.Tree.Children_Permission :=
+ Glb (Children_Permission (A), P);
+
+ when Reference =>
+ Apply_Glb_Tree (Get_All (A), P);
+
+ when Array_Component =>
+ Apply_Glb_Tree (Get_Elem (A), P);
+
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ begin
+ Comp := Perm_Tree_Maps.Get_First (Component (A));
+ while Comp /= null loop
+ Apply_Glb_Tree (Comp, P);
+ Comp := Perm_Tree_Maps.Get_Next (Component (A));
+ end loop;
+
+ Apply_Glb_Tree (Other_Components (A), P);
+ end;
+ end case;
+ end Apply_Glb_Tree;
+
+ Perm : constant Perm_Kind :=
+ Glb (Permission (Target), Permission (Source));
+
+ begin
+ pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
+ Target.all.Tree.Permission := Perm;
+
+ case Kind (Target) is
+ when Entire_Object =>
+ declare
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (Target);
+
+ begin
+ case Kind (Source) is
+ when Entire_Object =>
+ Target.all.Tree.Children_Permission :=
+ Glb (Child_Perm, Children_Permission (Source));
+
+ when Reference =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ Apply_Glb_Tree (Get_All (Target), Child_Perm);
+
+ when Array_Component =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
+
+ when Record_Component =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ declare
+ Comp : Perm_Tree_Access;
+
+ begin
+ Comp :=
+ Perm_Tree_Maps.Get_First (Component (Target));
+ while Comp /= null loop
+ -- Apply glb tree on every component subtree
+
+ Apply_Glb_Tree (Comp, Child_Perm);
+ Comp := Perm_Tree_Maps.Get_Next
+ (Component (Target));
+ end loop;
+ end;
+ Apply_Glb_Tree (Other_Components (Target), Child_Perm);
+
+ end case;
+ end;
+ when Reference =>
+ case Kind (Source) is
+ when Entire_Object =>
+ Apply_Glb_Tree (Get_All (Target),
+ Children_Permission (Source));
+
+ when Reference =>
+ Merge_Trees (Get_All (Target), Get_All (Source));
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+
+ when Array_Component =>
+ case Kind (Source) is
+ when Entire_Object =>
+ Apply_Glb_Tree (Get_Elem (Target),
+ Children_Permission (Source));
+
+ when Array_Component =>
+ Merge_Trees (Get_Elem (Target), Get_Elem (Source));
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+
+ when Record_Component =>
+ case Kind (Source) is
+ when Entire_Object =>
+ declare
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (Source);
+
+ Comp : Perm_Tree_Access;
+
+ begin
+ Comp := Perm_Tree_Maps.Get_First
+ (Component (Target));
+ while Comp /= null loop
+ -- Apply glb tree on every component subtree
+
+ Apply_Glb_Tree (Comp, Child_Perm);
+ Comp :=
+ Perm_Tree_Maps.Get_Next (Component (Target));
+ end loop;
+ Apply_Glb_Tree (Other_Components (Target), Child_Perm);
+ end;
+
+ when Record_Component =>
+ declare
+ Key_Source : Perm_Tree_Maps.Key_Option;
+ CompTarget : Perm_Tree_Access;
+ CompSource : Perm_Tree_Access;
+
+ begin
+ Key_Source := Perm_Tree_Maps.Get_First_Key
+ (Component (Source));
+
+ while Key_Source.Present loop
+ CompSource := Perm_Tree_Maps.Get
+ (Component (Source), Key_Source.K);
+ CompTarget := Perm_Tree_Maps.Get
+ (Component (Target), Key_Source.K);
+
+ pragma Assert (CompSource /= null);
+ Merge_Trees (CompTarget, CompSource);
+
+ Key_Source := Perm_Tree_Maps.Get_Next_Key
+ (Component (Source));
+ end loop;
+
+ Merge_Trees (Other_Components (Target),
+ Other_Components (Source));
+ end;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ end case;
+ end Merge_Trees;
+
+ CompTarget : Perm_Tree_Access;
+ CompSource : Perm_Tree_Access;
+ KeyTarget : Perm_Tree_Maps.Key_Option;
+
+ begin
+ KeyTarget := Get_First_Key (Target);
+ -- Iterate over every tree of the environment in the target, and merge
+ -- it with the source if there is such a similar one that exists. If
+ -- there is none, then skip.
+ while KeyTarget.Present loop
+
+ CompSource := Get (Source, KeyTarget.K);
+ CompTarget := Get (Target, KeyTarget.K);
+
+ pragma Assert (CompTarget /= null);
+
+ if CompSource /= null then
+ Merge_Trees (CompTarget, CompSource);
+ Remove (Source, KeyTarget.K);
+ end if;
+
+ KeyTarget := Get_Next_Key (Target);
+ end loop;
+
+ -- Iterate over every tree of the environment of the source. And merge
+ -- again. If there is not any tree of the target then just copy the tree
+ -- from source to target.
+ declare
+ KeySource : Perm_Tree_Maps.Key_Option;
+ begin
+ KeySource := Get_First_Key (Source);
+ while KeySource.Present loop
+
+ CompSource := Get (Source, KeySource.K);
+ CompTarget := Get (Target, KeySource.K);
+
+ if CompTarget = null then
+ CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
+ Copy_Tree (CompSource, CompTarget);
+ Set (Target, KeySource.K, CompTarget);
+ else
+ Merge_Trees (CompTarget, CompSource);
+ end if;
+
+ KeySource := Get_Next_Key (Source);
+ end loop;
+ end;
+
+ Free_Env (Source);
+ end Merge_Envs;
+
+ ----------------
+ -- Perm_Error --
+ ----------------
+
+ 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);
+
+ if Is_Deref then
+ Error_Msg_NE
+ ("insufficient permission on dereference from &", N, Root);
+ else
+ Error_Msg_NE ("insufficient permission for &", N, Root);
+ end if;
+
+ Perm_Mismatch (Perm, Found_Perm, N);
+ end Perm_Error;
+
+ -------------------------------
+ -- Perm_Error_Subprogram_End --
+ -------------------------------
+
+ procedure Perm_Error_Subprogram_End
+ (E : Entity_Id;
+ Subp : Entity_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind)
+ is
+ begin
+ Error_Msg_Node_2 := Subp;
+ Error_Msg_NE ("insufficient permission for & when returning from &",
+ Subp, E);
+ Perm_Mismatch (Perm, Found_Perm, Subp);
+ end Perm_Error_Subprogram_End;
+
+ ------------------
+ -- Process_Path --
+ ------------------
+
+ procedure Process_Path (N : Node_Id) is
+ Root : constant Entity_Id := Get_Enclosing_Object (N);
+ begin
+ -- We ignore if yielding to synchronized
+
+ if Present (Root)
+ and then Is_Synchronized_Object (Root)
+ then
+ return;
+ end if;
+
+ -- We ignore shallow unaliased. They are checked in flow analysis,
+ -- allowing backward compatibility.
+
+ if not Has_Alias (N)
+ and then Is_Shallow (Etype (N))
+ then
+ return;
+ end if;
+
+ declare
+ Perm_N : constant Perm_Kind := Get_Perm (N);
+
+ begin
+
+ case Current_Checking_Mode is
+ -- Check permission R, do nothing
+
+ when Read =>
+ if Perm_N not in Read_Perm then
+ Perm_Error (N, Read_Only, Perm_N);
+ end if;
+
+ -- If shallow type no need for RW, only R
+
+ when Move =>
+ if Is_Shallow (Etype (N)) then
+ if Perm_N not in Read_Perm then
+ Perm_Error (N, Read_Only, Perm_N);
+ end if;
+ else
+ -- Check permission RW if deep
+
+ if Perm_N /= Read_Write then
+ Perm_Error (N, Read_Write, Perm_N);
+ end if;
+
+ declare
+ -- Set permission to W to the path and any of its prefix
+
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Move (N, Move);
+
+ begin
+ if Tree = null then
+ -- We went through a function call, no permission to
+ -- modify.
+
+ return;
+ end if;
+
+ -- Set permissions to
+ -- No for any extension with more .all
+ -- W for any deep extension with same number of .all
+ -- RW for any shallow extension with same number of .all
+
+ Set_Perm_Extensions_Move (Tree, Etype (N));
+ end;
+ end if;
+
+ -- Check permission RW
+
+ when Super_Move =>
+ if Perm_N /= Read_Write then
+ Perm_Error (N, Read_Write, Perm_N);
+ end if;
+
+ declare
+ -- Set permission to No to the path and any of its prefix up
+ -- to the first .all and then W.
+
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Move (N, Super_Move);
+
+ begin
+ if Tree = null then
+ -- We went through a function call, no permission to
+ -- modify.
+
+ return;
+ end if;
+
+ -- Set permissions to No on any strict extension of the path
+
+ Set_Perm_Extensions (Tree, No_Access);
+ end;
+
+ -- Check permission W
+
+ when Assign =>
+ if Perm_N not in Write_Perm then
+ Perm_Error (N, Write_Only, Perm_N);
+ end if;
+
+ -- If the tree has an array component, then the permissions do
+ -- not get modified by the assignment.
+
+ if Has_Array_Component (N) then
+ return;
+ end if;
+
+ -- Same if has function component
+
+ if Has_Function_Component (N) then
+ return;
+ end if;
+
+ declare
+ -- Get the permission tree for the path
+
+ Tree : constant Perm_Tree_Access :=
+ Get_Perm_Tree (N);
+
+ Dummy : Perm_Tree_Access;
+
+ begin
+ if Tree = null then
+ -- We went through a function call, no permission to
+ -- modify.
+
+ return;
+ end if;
+
+ -- Set permission RW for it and all of its extensions
+
+ Tree.all.Tree.Permission := Read_Write;
+
+ Set_Perm_Extensions (Tree, Read_Write);
+
+ -- Normalize the permission tree
+
+ Dummy := Set_Perm_Prefixes_Assign (N);
+ end;
+
+ -- Check permission W
+
+ when Borrow_Out =>
+ if Perm_N not in Write_Perm then
+ Perm_Error (N, Write_Only, Perm_N);
+ end if;
+
+ declare
+ -- Set permission to No to the path and any of its prefixes
+
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Borrow_Out (N);
+
+ begin
+ if Tree = null then
+ -- We went through a function call, no permission to
+ -- modify.
+
+ return;
+ end if;
+
+ -- Set permissions to No on any strict extension of the path
+
+ Set_Perm_Extensions (Tree, No_Access);
+ end;
+
+ when Observe =>
+ if Perm_N not in Read_Perm then
+ Perm_Error (N, Read_Only, Perm_N);
+ end if;
+
+ if Is_By_Copy_Type (Etype (N)) then
+ return;
+ end if;
+
+ declare
+ -- Set permission to No on the path and any of its prefixes
+
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Observe (N);
+
+ begin
+ if Tree = null then
+ -- We went through a function call, no permission to
+ -- modify.
+
+ return;
+ end if;
+
+ -- Set permissions to No on any strict extension of the path
+
+ Set_Perm_Extensions (Tree, Read_Only);
+ end;
+ end case;
+ end;
+ end Process_Path;
+
+ -------------------------
+ -- Return_Declarations --
+ -------------------------
+
+ procedure Return_Declarations (L : List_Id) is
+
+ procedure Return_Declaration (Decl : Node_Id);
+ -- Check correct permissions for every declared object
+
+ ------------------------
+ -- Return_Declaration --
+ ------------------------
+
+ 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.
+
+ if Get (Current_Initialization_Map,
+ Unique_Entity (Defining_Identifier (Decl))) = False
+ then
+ 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,
+ Unique_Entity (Defining_Identifier (Decl)));
+
+ 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));
+ end if;
+ end;
+ end if;
+ end Return_Declaration;
+
+ -- Local Variables
+
+ N : Node_Id;
+
+ -- Start of processing for Return_Declarations
+
+ 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);
+ 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)
+ 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) 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);
+ 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);
+ C.all.Tree.Permission := Read_Write;
+
+ when Reference =>
+ pragma Assert (Get_All (C) /= null);
+
+ C.all.Tree.Permission :=
+ Lub (Permission (C), Permission (Get_All (C)));
+
+ when Array_Component =>
+ pragma Assert (C.all.Tree.Get_Elem /= null);
+
+ -- Given that it is not possible to know which element has been
+ -- assigned, then the permissions do not get changed in case of
+ -- Array_Component.
+
+ null;
+
+ when Record_Component =>
+ declare
+ Perm : Perm_Kind := Read_Write;
+
+ Comp : Perm_Tree_Access;
+
+ begin
+ -- We take the Glb of all the descendants, and then update the
+ -- permission of the node with it.
+ Comp := Perm_Tree_Maps.Get_First (Component (C));
+ while Comp /= null loop
+ Perm := Glb (Perm, Permission (Comp));
+ Comp := Perm_Tree_Maps.Get_Next (Component (C));
+ end loop;
+
+ Perm := Glb (Perm, Permission (Other_Components (C)));
+
+ C.all.Tree.Permission := Lub (Permission (C), Perm);
+ end;
+ end case;
+
+ case Nkind (N) is
+ -- Base identifier. End recursion here.
+
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Defining_Identifier
+ =>
+ return null;
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Set_Perm_Prefixes_Assign (Expression (N));
+
+ when N_Parameter_Specification =>
+ raise Program_Error;
+
+ -- Continue recursion on prefix
+
+ when N_Selected_Component =>
+ return Set_Perm_Prefixes_Assign (Prefix (N));
+
+ -- Continue recursion on prefix
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ return Set_Perm_Prefixes_Assign (Prefix (N));
+
+ -- Continue recursion on prefix
+
+ when N_Explicit_Dereference =>
+ return Set_Perm_Prefixes_Assign (Prefix (N));
+
+ when N_Function_Call =>
+ raise Program_Error;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ end Set_Perm_Prefixes_Assign;
+
+ ----------------------------------
+ -- Set_Perm_Prefixes_Borrow_Out --
+ ----------------------------------
+
+ function Set_Perm_Prefixes_Borrow_Out
+ (N : Node_Id)
+ return Perm_Tree_Access
+ is
+ begin
+ pragma Assert (Current_Checking_Mode = Borrow_Out);
+
+ case Nkind (N) is
+ -- Base identifier. Set permission to No.
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ 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.
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ 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 either W
+ -- (because the recursive call sets <= Write_Only) or No
+ -- (if another path has been moved with 'Access).
+
+ pragma Assert (Permission (C) = No_Access);
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Array_Component);
+
+ if Kind (C) = Array_Component then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ pragma Assert (Get_Elem (C) /= null);
+
+ C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
+
+ return Get_Elem (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace node with Array_Component.
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => No_Access,
+ Children_Permission => Children_Permission (C)));
+
+ -- We change the current node from Entire_Object
+ -- to Array_Component with same permission and the
+ -- previously defined son.
+
+ C.all.Tree := (Kind => Array_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => No_Access,
+ Get_Elem => Son);
+
+ return Get_Elem (C);
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer the subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
+
+ when N_Explicit_Dereference =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_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) = Reference);
+
+ if Kind (C) = Reference then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ pragma Assert (Get_All (C) /= null);
+
+ C.all.Tree.Get_All.all.Tree.Permission := No_Access;
+
+ return Get_All (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace the node with Reference.
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (N)),
+ Permission => No_Access,
+ Children_Permission => Children_Permission (C)));
+
+ -- We change the current node from Entire_Object to
+ -- Reference with No_Access and the previous son.
+
+ pragma Assert (Is_Node_Deep (C));
+
+ C.all.Tree := (Kind => Reference,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => No_Access,
+ Get_All => Son);
+
+ return Get_All (C);
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ when N_Function_Call =>
+ return null;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Set_Perm_Prefixes_Borrow_Out;
+
+ ----------------------------
+ -- Set_Perm_Prefixes_Move --
+ ----------------------------
+
+ function Set_Perm_Prefixes_Move
+ (N : Node_Id; Mode : Checking_Mode)
+ return Perm_Tree_Access
+ is
+ begin
+ case Nkind (N) is
+ -- Base identifier. Set permission to W or No depending on Mode.
+
+ when N_Identifier
+ | N_Expanded_Name
+ =>
+ declare
+ P : constant Node_Id := Entity (N);
+
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (P));
+
+ begin
+ -- The base tree can be RW (first move from this base path) or
+ -- W (already some extensions values moved), or even No_Access
+ -- (extensions moved with 'Access). But it cannot be Read_Only
+ -- (we get an error).
+
+ if Permission (C) = Read_Only then
+ raise Unrecoverable_Error;
+ end if;
+
+ -- Setting the initialization map to True, so that this
+ -- variable cannot be ignored anymore when looking at end
+ -- of elaboration of package.
+
+ Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+ if C = null then
+ -- No null possible here, there are no parents for the path.
+ -- This means we are using a global variable without adding
+ -- it in environment with a global aspect.
+
+ Illegal_Global_Usage (N);
+ end if;
+
+ if Mode = Super_Move then
+ C.all.Tree.Permission := No_Access;
+ else
+ C.all.Tree.Permission := Glb (Write_Only, Permission (C));
+ end if;
+
+ return C;
+ end;
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Set_Perm_Prefixes_Move (Expression (N), Mode);
+
+ when N_Parameter_Specification
+ | N_Defining_Identifier
+ =>
+ raise Program_Error;
+
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer our subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
+
+ when N_Selected_Component =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Move (Prefix (N), Mode);
+
+ begin
+ if C = null then
+ -- We went through a function call, do nothing
+
+ return null;
+ end if;
+
+ -- The permission of the returned node should be either W
+ -- (because the recursive call sets <= Write_Only) or No
+ -- (if another path has been moved with 'Access).
+
+ pragma Assert (Permission (C) = No_Access
+ or else Permission (C) = Write_Only);
+
+ if Mode = Super_Move then
+ -- The permission of the returned node should be No (thanks
+ -- to the recursion).
+
+ pragma Assert (Permission (C) = No_Access);
+ null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Record_Component);
+
+ if Kind (C) = Record_Component then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the record subtree.
+
+ declare
+ Selected_Component : constant Entity_Id :=
+ Entity (Selector_Name (N));
+
+ Selected_C : Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ begin
+ if Selected_C = null then
+ -- If the hash table returns no element, then we fall
+ -- into the part of Other_Components.
+ pragma Assert (Is_Tagged_Type (Etype (Prefix (N))));
+
+ Selected_C := Other_Components (C);
+ end if;
+
+ pragma Assert (Selected_C /= null);
+
+ -- The Selected_C can have permissions:
+ -- RW : first move in this path
+ -- W : Already other moves in this path
+ -- No : Already other moves with 'Access
+
+ pragma Assert (Permission (Selected_C) /= Read_Only);
+ if Mode = Super_Move then
+ Selected_C.all.Tree.Permission := No_Access;
+ else
+ Selected_C.all.Tree.Permission :=
+ Glb (Write_Only, Permission (Selected_C));
+
+ end if;
+
+ return Selected_C;
+ end;
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace the node with
+ -- Record_Component.
+
+ Elem : Node_Id;
+
+ -- Create an empty hash table
+
+ Hashtbl : Perm_Tree_Maps.Instance;
+
+ -- We are in Move or Super_Move mode, hence we can assume
+ -- that the Children_permission is RW, given that there
+ -- are no other paths that could have been moved.
+
+ pragma Assert (Children_Permission (C) = Read_Write);
+
+ -- We create the unrolled nodes, that will all have RW
+ -- permission given that we are in move mode. We will
+ -- then set the right node to W.
+
+ Son : Perm_Tree_Access;
+
+ begin
+ -- We change the current node from Entire_Object to
+ -- Record_Component with same permission and an empty
+ -- hash table as component list.
+
+ C.all.Tree :=
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Component => Hashtbl,
+ Other_Components =>
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => True,
+ Permission => Read_Write,
+ Children_Permission => Read_Write)
+ ));
+
+ -- We fill the hash table with all sons of the record,
+ -- with basic Entire_Objects nodes.
+ Elem := First_Component_Or_Discriminant
+ (Etype (Prefix (N)));
+
+ while Present (Elem) loop
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Elem)),
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+
+ Perm_Tree_Maps.Set
+ (C.all.Tree.Component, Elem, Son);
+
+ Next_Component_Or_Discriminant (Elem);
+ end loop;
+
+ -- Now we set the right field to Write_Only or No_Access
+ -- depending on mode, and then we return the tree to the
+ -- sons, so that the recursion can continue.
+
+ declare
+ Selected_Component : constant Entity_Id :=
+ Entity (Selector_Name (N));
+
+ Selected_C : Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ begin
+ if Selected_C = null then
+ Selected_C := Other_Components (C);
+ end if;
+
+ pragma Assert (Selected_C /= null);
+
+ -- Given that this is a newly created Select_C, we can
+ -- safely assume that its permission is Read_Write.
+
+ pragma Assert (Permission (Selected_C) =
+ Read_Write);
+
+ if Mode = Super_Move then
+ Selected_C.all.Tree.Permission := No_Access;
+ else
+ Selected_C.all.Tree.Permission := Write_Only;
+ end if;
+
+ return Selected_C;
+ end;
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer the subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Move (Prefix (N), Mode);
+
+ begin
+ if C = null then
+ -- We went through a function call, do nothing
+
+ return null;
+ end if;
+
+ -- The permission of the returned node should be either
+ -- W (because the recursive call sets <= Write_Only)
+ -- or No (if another path has been moved with 'Access)
+
+ if Mode = Super_Move then
+ pragma Assert (Permission (C) = No_Access);
+ null;
+ else
+ pragma Assert (Permission (C) = Write_Only
+ or else Permission (C) = No_Access);
+ null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Array_Component);
+
+ if Kind (C) = Array_Component then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ if Get_Elem (C) = null then
+ -- Hash_Table_Error
+ raise Program_Error;
+ end if;
+
+ -- The Get_Elem can have permissions :
+ -- RW : first move in this path
+ -- W : Already other moves in this path
+ -- No : Already other moves with 'Access
+
+ pragma Assert (Permission (Get_Elem (C)) /= Read_Only);
+
+ if Mode = Super_Move then
+ C.all.Tree.Get_Elem.all.Tree.Permission := No_Access;
+ else
+ C.all.Tree.Get_Elem.all.Tree.Permission :=
+ Glb (Write_Only, Permission (Get_Elem (C)));
+ end if;
+
+ return Get_Elem (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace node with Array_Component.
+
+ -- We are in move mode, hence we can assume that the
+ -- Children_permission is RW.
+
+ pragma Assert (Children_Permission (C) = Read_Write);
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+
+ if Mode = Super_Move then
+ Son.all.Tree.Permission := No_Access;
+ else
+ Son.all.Tree.Permission := Write_Only;
+ end if;
+
+ -- We change the current node from Entire_Object
+ -- to Array_Component with same permission and the
+ -- previously defined son.
+
+ C.all.Tree := (Kind => Array_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Get_Elem => Son);
+
+ return Get_Elem (C);
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer the subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
+
+ when N_Explicit_Dereference =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Move (Prefix (N), Move);
+
+ begin
+ if C = null then
+ -- We went through a function call: do nothing
+
+ return null;
+ end if;
+
+ -- The permission of the returned node should be only
+ -- W (because the recursive call sets <= Write_Only)
+ -- No is NOT POSSIBLE here
+
+ pragma Assert (Permission (C) = Write_Only);
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Reference);
+
+ if Kind (C) = Reference then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ if Get_All (C) = null then
+ -- Hash_Table_Error
+ raise Program_Error;
+ end if;
+
+ -- The Get_All can have permissions :
+ -- RW : first move in this path
+ -- W : Already other moves in this path
+ -- No : Already other moves with 'Access
+
+ pragma Assert (Permission (Get_All (C)) /= Read_Only);
+
+ if Mode = Super_Move then
+ C.all.Tree.Get_All.all.Tree.Permission := No_Access;
+ else
+ Get_All (C).all.Tree.Permission :=
+ Glb (Write_Only, Permission (Get_All (C)));
+ end if;
+ return Get_All (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace the node with Reference.
+
+ -- We are in Move or Super_Move mode, hence we can assume
+ -- that the Children_permission is RW.
+
+ pragma Assert (Children_Permission (C) = Read_Write);
+
+ Son : Perm_Tree_Access;
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (N)),
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+
+ if Mode = Super_Move then
+ Son.all.Tree.Permission := No_Access;
+ else
+ Son.all.Tree.Permission := Write_Only;
+ end if;
+
+ -- We change the current node from Entire_Object to
+ -- Reference with Write_Only and the previous son.
+
+ pragma Assert (Is_Node_Deep (C));
+
+ C.all.Tree := (Kind => Reference,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Write_Only,
+ -- Write_only is equal to C.Permission
+ Get_All => Son);
+
+ return Get_All (C);
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ when N_Function_Call =>
+ return null;
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ end Set_Perm_Prefixes_Move;
+
+ -------------------------------
+ -- Set_Perm_Prefixes_Observe --
+ -------------------------------
+
+ function Set_Perm_Prefixes_Observe
+ (N : Node_Id)
+ return Perm_Tree_Access
+ is
+ begin
+ pragma Assert (Current_Checking_Mode = Observe);
+
+ case Nkind (N) is
+ -- Base identifier. Set permission to R.
+
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Defining_Identifier
+ =>
+ declare
+ P : Node_Id;
+ C : Perm_Tree_Access;
+
+ begin
+ if Nkind (N) = N_Defining_Identifier then
+ P := N;
+ else
+ P := Entity (N);
+ end if;
+
+ C := Get (Current_Perm_Env, Unique_Entity (P));
+ -- Setting the initialization map to True, so that this
+ -- variable cannot be ignored anymore when looking at end
+ -- of elaboration of package.
+
+ Set (Current_Initialization_Map, Unique_Entity (P), True);
+
+ if C = null then
+ -- No null possible here, there are no parents for the path.
+ -- This means we are using a global variable without adding
+ -- it in environment with a global aspect.
+
+ Illegal_Global_Usage (N);
+ end if;
+
+ C.all.Tree.Permission := Glb (Read_Only, Permission (C));
+
+ return C;
+ end;
+
+ when N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ | N_Qualified_Expression
+ =>
+ return Set_Perm_Prefixes_Observe (Expression (N));
+
+ when N_Parameter_Specification =>
+ raise Program_Error;
+
+ -- We set the permission tree of its prefix, and then we extract
+ -- from the returned pointer our subtree and assign an adequate
+ -- permission to it, if unfolded. If folded, we unroll the tree
+ -- at one step.
+
+ when N_Selected_Component =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Observe (Prefix (N));
+
+ begin
+ if C = null then
+ -- We went through a function call, do nothing
+
+ return null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Record_Component);
+
+ if Kind (C) = Record_Component then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the record subtree. We put the permission to the
+ -- glb of read_only and its current permission, to consider
+ -- the case of observing x.y while x.z has been moved. Then
+ -- x should be No_Access.
+
+ declare
+ Selected_Component : constant Entity_Id :=
+ Entity (Selector_Name (N));
+
+ Selected_C : Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ begin
+ if Selected_C = null then
+ Selected_C := Other_Components (C);
+ end if;
+
+ pragma Assert (Selected_C /= null);
+
+ Selected_C.all.Tree.Permission :=
+ Glb (Read_Only, Permission (Selected_C));
+
+ return Selected_C;
+ end;
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace the node with
+ -- Record_Component.
+
+ Elem : Node_Id;
+
+ -- Create an empty hash table
+
+ Hashtbl : Perm_Tree_Maps.Instance;
+
+ -- We create the unrolled nodes, that will all have RW
+ -- permission given that we are in move mode. We will
+ -- then set the right node to W.
+
+ Son : Perm_Tree_Access;
+
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (C);
+
+ begin
+ -- We change the current node from Entire_Object to
+ -- Record_Component with same permission and an empty
+ -- hash table as component list.
+
+ C.all.Tree :=
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Permission (C),
+ Component => Hashtbl,
+ Other_Components =>
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => True,
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm)
+ ));
+
+ -- We fill the hash table with all sons of the record,
+ -- with basic Entire_Objects nodes.
+ Elem := First_Component_Or_Discriminant
+ (Etype (Prefix (N)));
+
+ while Present (Elem) loop
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Elem)),
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm));
+
+ Perm_Tree_Maps.Set
+ (C.all.Tree.Component, Elem, Son);
+
+ Next_Component_Or_Discriminant (Elem);
+ end loop;
+
+ -- Now we set the right field to Read_Only. and then we
+ -- return the tree to the sons, so that the recursion can
+ -- continue.
+
+ declare
+ Selected_Component : constant Entity_Id :=
+ Entity (Selector_Name (N));
+
+ Selected_C : Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C), Selected_Component);
+
+ begin
+ if Selected_C = null then
+ Selected_C := Other_Components (C);
+ end if;
+
+ pragma Assert (Selected_C /= null);
+
+ Selected_C.all.Tree.Permission :=
+ Glb (Read_Only, Child_Perm);
+
+ return Selected_C;
+ end;
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ -- We set the permission tree of its prefix, and then we extract from
+ -- the returned pointer the subtree and assign an adequate permission
+ -- to it, if unfolded. If folded, we unroll the tree at one step.
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Observe (Prefix (N));
+
+ begin
+ if C = null then
+ -- We went through a function call, do nothing
+
+ return null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Array_Component);
+
+ if Kind (C) = Array_Component then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ pragma Assert (Get_Elem (C) /= null);
+
+ C.all.Tree.Get_Elem.all.Tree.Permission :=
+ Glb (Read_Only, Permission (Get_Elem (C)));
+
+ return Get_Elem (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace node with Array_Component.
+
+ Son : Perm_Tree_Access;
+
+ Child_Perm : constant Perm_Kind :=
+ Glb (Read_Only, Children_Permission (C));
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm));
+
+ -- We change the current node from Entire_Object
+ -- to Array_Component with same permission and the
+ -- previously defined son.
+
+ C.all.Tree := (Kind => Array_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Child_Perm,
+ Get_Elem => Son);
+
+ return Get_Elem (C);
+ end;
+
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ -- We set the permission tree of its prefix, and then we extract from
+ -- the returned pointer the subtree and assign an adequate permission
+ -- to it, if unfolded. If folded, we unroll the tree at one step.
+
+ when N_Explicit_Dereference =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes_Observe (Prefix (N));
+
+ begin
+ if C = null then
+ -- We went through a function call, do nothing
+
+ return null;
+ end if;
+
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Reference);
+
+ if Kind (C) = Reference then
+ -- The tree is unfolded. We just modify the permission and
+ -- return the elem subtree.
+
+ pragma Assert (Get_All (C) /= null);
+
+ C.all.Tree.Get_All.all.Tree.Permission :=
+ Glb (Read_Only, Permission (Get_All (C)));
+
+ return Get_All (C);
+ elsif Kind (C) = Entire_Object then
+ declare
+ -- Expand the tree. Replace the node with Reference.
+
+ Son : Perm_Tree_Access;
+
+ Child_Perm : constant Perm_Kind :=
+ Glb (Read_Only, Children_Permission (C));
+
+ begin
+ Son := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (N)),
+ Permission => Child_Perm,
+ Children_Permission => Child_Perm));
+
+ -- We change the current node from Entire_Object to
+ -- Reference with Write_Only and the previous son.
+
+ pragma Assert (Is_Node_Deep (C));
+
+ C.all.Tree := (Kind => Reference,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Permission => Child_Perm,
+ Get_All => Son);
+
+ return Get_All (C);
+ end;
+ else
+ raise Program_Error;
+ end if;
+ end;
+
+ when N_Function_Call =>
+ return null;
+
+ when others =>
+ raise Program_Error;
+
+ end case;
+ end Set_Perm_Prefixes_Observe;
+
+ -------------------
+ -- Setup_Globals --
+ -------------------
+
+ procedure Setup_Globals (Subp : Entity_Id) is
+
+ procedure Setup_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind);
+ -- Set up global items from the list starting at Item
+
+ procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
+ -- Set up global items for the mode Global_Mode
+
+ -----------------------------
+ -- Setup_Globals_From_List --
+ -----------------------------
+
+ procedure Setup_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
+ Setup_Parameter_Or_Global (E, Kind);
+ end if;
+ Next_Global (Item);
+ end loop;
+ end Setup_Globals_From_List;
+
+ ---------------------------
+ -- Setup_Globals_Of_Mode --
+ ---------------------------
+
+ procedure Setup_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;
+
+ -- Set up both global items from Global and Refined_Global pragmas
+
+ Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
+ Setup_Globals_From_List
+ (First_Global (Subp, Global_Mode, Refined => True), Kind);
+ end Setup_Globals_Of_Mode;
+
+ -- Start of processing for Setup_Globals
+
+ begin
+ Setup_Globals_Of_Mode (Name_Proof_In);
+ Setup_Globals_Of_Mode (Name_Input);
+ Setup_Globals_Of_Mode (Name_Output);
+ Setup_Globals_Of_Mode (Name_In_Out);
+ end Setup_Globals;
+
+ -------------------------------
+ -- Setup_Parameter_Or_Global --
+ -------------------------------
+
+ procedure Setup_Parameter_Or_Global
+ (Id : Entity_Id;
+ Mode : Formal_Kind)
+ is
+ Elem : Perm_Tree_Access;
+
+ begin
+ Elem := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Id)),
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+
+ case Mode is
+ when E_In_Parameter =>
+
+ -- Borrowed IN: RW for everybody
+
+ if Is_Borrowed_In (Id) then
+ Elem.all.Tree.Permission := Read_Write;
+ Elem.all.Tree.Children_Permission := Read_Write;
+
+ -- Observed IN: R for everybody
+
+ else
+ Elem.all.Tree.Permission := Read_Only;
+ Elem.all.Tree.Children_Permission := Read_Only;
+ end if;
+
+ -- OUT: borrow, but callee has W only
+
+ when E_Out_Parameter =>
+ Elem.all.Tree.Permission := Write_Only;
+ Elem.all.Tree.Children_Permission := Write_Only;
+
+ -- IN OUT: borrow and callee has RW
+
+ when E_In_Out_Parameter =>
+ Elem.all.Tree.Permission := Read_Write;
+ Elem.all.Tree.Children_Permission := Read_Write;
+ end case;
+
+ Set (Current_Perm_Env, Id, Elem);
+ end Setup_Parameter_Or_Global;
+
+ ----------------------
+ -- Setup_Parameters --
+ ----------------------
+
+ procedure Setup_Parameters (Subp : Entity_Id) is
+ Formal : Entity_Id;
+
+ begin
+ Formal := First_Formal (Subp);
+ while Present (Formal) loop
+ Setup_Parameter_Or_Global (Formal, Ekind (Formal));
+ Next_Formal (Formal);
+ end loop;
+ end Setup_Parameters;
+
+end Sem_SPARK;
projects / gcc.git / commitdiff