===================================================================
@@ -0,0 +1,6188 @@
+------------------------------------------------------------------------------
+-- --
+-- 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;
===================================================================
@@ -0,0 +1,143 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S E M _ S P A R K --
+-- --
+-- S p e c --
+-- --
+-- 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. --
+-- --
+------------------------------------------------------------------------------
+
+-- This package implements an anti-aliasing analysis for access types. The
+-- rules that are enforced are defined in the anti-aliasing section of the
+-- SPARK RM 6.4.2
+--
+-- Analyze_SPARK is called by Gnat1drv, when GNATprove mode is activated. It
+-- does an analysis of the source code, looking for code that is considered
+-- as SPARK and launches another function called Analyze_Node that will do
+-- the whole analysis.
+--
+-- A path is an abstraction of a name, of which all indices, slices (for
+-- indexed components) and function calls have been abstracted and all
+-- dereferences are made explicit. A path is the atomic element viewed by the
+-- analysis, with the notion of prefixes and extensions of different paths.
+--
+-- The analysis explores the AST, and looks for different constructs
+-- that may involve aliasing. These main constructs are assignments
+-- (N_Assignment_Statement, N_Object_Declaration, ...), or calls
+-- (N_Procedure_Call_Statement, N_Entry_Call_Statement, N_Function_Call).
+-- The analysis checks the permissions of each construct and updates them
+-- according to the SPARK RM. This can follow three main different types
+-- of operations: move, borrow, and observe.
+
+----------------------------
+-- Deep and shallow types --
+----------------------------
+
+-- The analysis focuses on objects that can cause problems in terms of pointer
+-- aliasing. These objects have types that are called deep. Deep types are
+-- defined as being either types with an access part or class-wide types
+-- (which may have an access part in a derived type). Non-deep types are
+-- called shallow. Some objects of shallow type may cause pointer aliasing
+-- problems when they are explicitely marked as aliased (and then the aliasing
+-- occurs when we take the Access to this object and store it in a pointer).
+
+----------
+-- Move --
+----------
+
+-- Moves can happen at several points in the program: during assignment (and
+-- any similar statement such as object declaration with initial value), or
+-- during return statements.
+--
+-- The underlying concept consists of transferring the ownership of any path
+-- on the right-hand side to the left-hand side. There are some details that
+-- should be taken into account so as not to transfer paths that appear only
+-- as intermediate results of a more complex expression.
+
+-- More specifically, the SPARK RM defines moved expressions, and any moved
+-- expression that points directly to a path is then checked and sees its
+-- permissions updated accordingly.
+
+------------
+-- Borrow --
+------------
+
+-- Borrows can happen in subprogram calls. They consist of a temporary
+-- transfer of ownership from a caller to a callee. Expressions that can be
+-- borrowed can be found in either procedure or entry actual parameters, and
+-- consist of parameters of mode either "out" or "in out", or parameters of
+-- mode "in" that are of type nonconstant access-to-variable. We consider
+-- global variables as implicit parameters to subprograms, with their mode
+-- given by the Global contract associated to the subprogram. Note that the
+-- analysis looks for such a Global contract mentioning any global variable
+-- of deep type accessed directly in the subprogram, and it raises an error if
+-- there is no Global contract, or if the Global contract does not mention the
+-- variable.
+--
+-- A borrow of a parameter X is equivalent in terms of aliasing to moving
+-- X'Access to the callee, and then assigning back X at the end of the call.
+--
+-- Borrowed parameters should have read-write permission (or write-only for
+-- "out" parameters), and should all have read-write permission at the end
+-- of the call (this guarantee is ensured by the callee).
+
+-------------
+-- Observe --
+-------------
+
+-- Observed parameters are all the other parameters that are not borrowed and
+-- that may cause problems with aliasing. They are considered as being sent to
+-- the callee with Read-Only permission, so that they can be aliased safely.
+-- This is the only construct that allows aliasing that does not prevent
+-- accessing the old path that is being aliased. However, this comes with
+-- the restriction that those aliased path cannot be written in the callee.
+
+--------------------
+-- Implementation --
+--------------------
+
+-- The implementation is based on trees that represent the possible paths
+-- in the source code. Those trees can be unbounded in depth, hence they are
+-- represented using lazy data structures, whose laziness is handled manually.
+-- Each time an identifier is declared, its path is added to the permission
+-- environment as a tree with only one node, the declared identifier. Each
+-- time a path is checked or updated, we look in the tree at the adequate
+-- node, unfolding the tree whenever needed.
+
+-- For this, each node has several variables that indicate whether it is
+-- deep (Is_Node_Deep), what permission it has (Permission), and what is
+-- the lowest permission of all its descendants (Children_Permission). After
+-- unfolding the tree, we update the permissions of each node, deleting the
+-- Children_Permission, and specifying new ones for the leaves of the unfolded
+-- tree.
+
+-- After assigning a path, the descendants of the assigned path are dumped
+-- (and hence the tree is folded back), given that all descendants directly
+-- get read-write permission, which can be specified using the node's
+-- Children_Permission field.
+
+with Types; use Types;
+
+package Sem_SPARK is
+
+ procedure Check_Safe_Pointers (N : Node_Id);
+ -- The entry point of this package. It analyzes a node and reports errors
+ -- when there are violations of aliasing rules.
+
+end Sem_SPARK;
===================================================================
@@ -8093,6 +8093,124 @@
end if;
end First_Actual;
+ ------------------
+ -- First_Global --
+ ------------------
+
+ function First_Global
+ (Subp : Entity_Id;
+ Global_Mode : Name_Id;
+ Refined : Boolean := False) return Node_Id
+ is
+ function First_From_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input) return Entity_Id;
+ -- Get the first item with suitable mode from List
+
+ ----------------------------
+ -- First_From_Global_List --
+ ----------------------------
+
+ function First_From_Global_List
+ (List : Node_Id;
+ Global_Mode : Name_Id := Name_Input) return Entity_Id
+ is
+ Assoc : Node_Id;
+
+ begin
+ -- Empty list (no global items)
+
+ if Nkind (List) = N_Null then
+ return Empty;
+
+ -- Single global item declaration (only input items)
+
+ elsif Nkind_In (List, N_Expanded_Name,
+ N_Identifier,
+ N_Selected_Component)
+ then
+ if Global_Mode = Name_Input then
+ return List;
+ else
+ return Empty;
+ end if;
+
+ -- Simple global list (only input items) or moded global list
+ -- declaration.
+
+ elsif Nkind (List) = N_Aggregate then
+ if Present (Expressions (List)) then
+ if Global_Mode = Name_Input then
+ return First (Expressions (List));
+ else
+ return Empty;
+ end if;
+
+ else
+ Assoc := First (Component_Associations (List));
+ while Present (Assoc) loop
+
+ -- When we find the desired mode in an association, call
+ -- recursively First_From_Global_List as if the mode was
+ -- Name_Input, in order to reuse the existing machinery
+ -- for the other cases.
+
+ if Chars (First (Choices (Assoc))) = Global_Mode then
+ return First_From_Global_List (Expression (Assoc));
+ end if;
+
+ Next (Assoc);
+ end loop;
+
+ return Empty;
+ end if;
+
+ -- To accommodate partial decoration of disabled SPARK features,
+ -- this routine may be called with illegal input. If this is the
+ -- case, do not raise Program_Error.
+
+ else
+ return Empty;
+ end if;
+ end First_From_Global_List;
+
+ -- Local variables
+
+ Global : Node_Id := Empty;
+ Body_Id : Entity_Id;
+
+ begin
+ pragma Assert (Global_Mode = Name_Input
+ or else Global_Mode = Name_Output
+ or else Global_Mode = Name_In_Out
+ or else Global_Mode = Name_Proof_In);
+
+ -- Retrieve the suitable pragma Global or Refined_Global. In the second
+ -- case, it can only be located on the body entity.
+
+ if Refined then
+ Body_Id := Subprogram_Body_Entity (Subp);
+ if Present (Body_Id) then
+ Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
+ end if;
+ else
+ Global := Get_Pragma (Subp, Pragma_Global);
+ end if;
+
+ -- No corresponding global if pragma is not present
+
+ if No (Global) then
+ return Empty;
+
+ -- Otherwise retrieve the corresponding list of items depending on the
+ -- Global_Mode.
+
+ else
+ return First_From_Global_List
+ (Expression (Get_Argument (Global, Subp)), Global_Mode);
+ end if;
+ end First_Global;
+
-------------
-- Fix_Msg --
-------------
@@ -18980,6 +19098,27 @@
Actual_Id := Next_Actual (Actual_Id);
end Next_Actual;
+ -----------------
+ -- Next_Global --
+ -----------------
+
+ function Next_Global (Node : Node_Id) return Node_Id is
+ begin
+ -- The global item may either be in a list, or by itself, in which case
+ -- there is no next global item with the same mode.
+
+ if Is_List_Member (Node) then
+ return Next (Node);
+ else
+ return Empty;
+ end if;
+ end Next_Global;
+
+ procedure Next_Global (Node : in out Node_Id) is
+ begin
+ Node := Next_Global (Node);
+ end Next_Global;
+
----------------------------------
-- New_Requires_Transient_Scope --
----------------------------------
===================================================================
@@ -885,6 +885,17 @@
-- Note that the value returned is always the expression (not the
-- N_Parameter_Association nodes, even if named association is used).
+ function First_Global
+ (Subp : Entity_Id;
+ Global_Mode : Name_Id;
+ Refined : Boolean := False) return Node_Id;
+ -- Returns the first global item of mode Global_Mode (which can be
+ -- Name_Input, Name_Output, Name_In_Out or Name_Proof_In) associated to
+ -- subprogram Subp, or Empty otherwise. If Refined is True, the global item
+ -- is retrieved from the Refined_Global aspect/pragma associated to the
+ -- body of Subp if present. Next_Global can be used to get the next global
+ -- item with the same mode.
+
function Fix_Msg (Id : Entity_Id; Msg : String) return String;
-- Replace all occurrences of a particular word in string Msg depending on
-- the Ekind of Id as follows:
@@ -2177,6 +2188,16 @@
-- Note that the result produced is always an expression, not a parameter
-- association node, even if named notation was used.
+ procedure Next_Global (Node : in out Node_Id);
+ pragma Inline (Next_Actual);
+ -- Next_Global (N) is equivalent to N := Next_Global (N). Note that we
+ -- inline this procedural form, but not the functional form that follows.
+
+ function Next_Global (Node : Node_Id) return Node_Id;
+ -- Node is a global item from a list, obtained through calling First_Global
+ -- and possibly Next_Global a number of times. Returns the next global item
+ -- with the same mode.
+
function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ is subject to pragma No_Heap_Finalization
===================================================================
@@ -61,6 +61,7 @@
with Sem_Ch13;
with Sem_Elim;
with Sem_Eval;
+with Sem_SPARK; use Sem_SPARK;
with Sem_Type;
with Set_Targ;
with Sinfo; use Sinfo;
@@ -1449,12 +1450,19 @@
Prepcomp.Add_Dependencies;
- -- In gnatprove mode we're writing the ALI much earlier than usual
- -- as flow analysis needs the file present in order to append its
- -- own globals to it.
-
if GNATprove_Mode then
+ -- Perform the new SPARK checking rules for pointer aliasing. This is
+ -- only activated in GNATprove mode and on SPARK code.
+
+ if Debug_Flag_FF then
+ Check_Safe_Pointers (Main_Unit_Node);
+ end if;
+
+ -- In GNATprove mode we're writing the ALI much earlier than usual
+ -- as flow analysis needs the file present in order to append its
+ -- own globals to it.
+
-- Note: In GNATprove mode, an "object" file is always generated as
-- the result of calling gnat1 or gnat2why, although this is not the
-- same as the object file produced for compilation.
===================================================================
@@ -69,7 +69,7 @@
-- dC Output debugging information on check suppression
-- dD Delete elaboration checks in inner level routines
-- dE Apply elaboration checks to predefined units
- -- dF
+ -- dF Perform the new SPARK checking rules for pointer aliasing
-- dG Generate all warnings including those normally suppressed
-- dH Hold (kill) call to gigi
-- dI Inhibit internal name numbering in gnatG listing
@@ -383,6 +383,11 @@
-- dE Apply compile time elaboration checking for with relations between
-- predefined units. Normally no checks are made.
+ -- dF Perform the new SPARK checking rules for pointer aliasing. This is
+ -- only activated in GNATprove mode and on SPARK code. These rules are
+ -- not yet part of the official SPARK language, but are expected to be
+ -- included in a future version of SPARK.
+
-- dG Generate all warnings. Normally Errout suppresses warnings on
-- units that are not part of the main extended source, and also
-- suppresses warnings on instantiations in the main extended
===================================================================
@@ -44,6 +44,12 @@
-- which prevent execution of code on the stack, e.g. in windows environments
-- with DEP (Data Execution Protection) enabled.
+pragma Restrictions (No_Finalization);
+-- Use restriction No_Finalization to avoid pulling finalization (not allowed
+-- in GNAT) inside sem_spark.adb, when defining type Perm_Tree_Access as an
+-- access type on incomplete type Perm_Tree_Wrapper (which is required for
+-- defining a recursive type).
+
package System is
pragma Pure;
-- Note that we take advantage of the implementation permission to make
===================================================================
@@ -312,6 +312,7 @@
ada/freeze.o \
ada/frontend.o \
ada/libgnat/g-byorma.o \
+ ada/libgnat/g-dynhta.o \
ada/libgnat/g-hesora.o \
ada/libgnat/g-htable.o \
ada/libgnat/g-spchge.o \
@@ -443,6 +444,7 @@
ada/sem_res.o \
ada/sem_scil.o \
ada/sem_smem.o \
+ ada/sem_spark.o \
ada/sem_type.o \
ada/sem_util.o \
ada/sem_warn.o \
SPARK is evolving to support pointers in a way that does not introduce aliasing problems. SPARK RM will soon include the rules behind this analysis, that are summarized in the source code. This analysis is currently only triggered on SPARK code, when GNATprove mode is active (switch -gnatd.F) with the debug switch -gnatdF. For example, the analysis detects the following errors on the following source code: $ gcc -c -gnatd.F -gnatdF pointers.adb 1. package Pointers with 2. SPARK_Mode 3. is 4. type Int_Ptr is access Integer; 5. 6. procedure Bad_Swap (X, Y : in out Int_Ptr); | >>> insufficient permission for "Y" when returning from "Bad_Swap" >>> expected at least "read_write", got "write_only" 7. 8. procedure Swap (X, Y : in out Int_Ptr); 9. 10. X, Y : Int_Ptr; 11. 12. procedure Bad_Swap_Global with | >>> insufficient permission for "Y" when returning from "Bad_Swap_Global" >>> expected at least "read_write", got "write_only" 13. Global => (In_Out => (X, Y)); 14. 15. procedure Swap_Global with 16. Global => (In_Out => (X, Y)); 17. 18. procedure Bad_Borrow (X, Y : in out Int_Ptr); 19. 20. procedure Bad_Move (X, Y : in out Int_Ptr); | >>> insufficient permission for "Y" when returning from "Bad_Move" >>> expected at least "read_write", got "write_only" 21. 22. 23. end Pointers; 1. package body Pointers with 2. SPARK_Mode 3. is 4. 5. procedure Bad_Swap (X, Y : in out Int_Ptr) is 6. begin 7. X := Y; 8. end Bad_Swap; 9. 10. procedure Swap (X, Y : in out Int_Ptr) is 11. Tmp : Int_Ptr := X; 12. begin 13. X := Y; 14. Y := Tmp; 15. end Swap; 16. 17. procedure Bad_Swap_Global is 18. begin 19. X := Y; 20. end Bad_Swap_Global; 21. 22. procedure Swap_Global is 23. Tmp : Int_Ptr := X; 24. begin 25. X := Y; 26. Y := Tmp; 27. end Swap_Global; 28. 29. procedure Bad_Borrow (X, Y : in out Int_Ptr) is 30. begin 31. X := Y; 32. Swap (X, Y); | >>> insufficient permission for "Y" >>> expected at least "read_write", got "write_only" 33. end Bad_Borrow; 34. 35. procedure Bad_Move (X, Y : in out Int_Ptr) is 36. begin 37. X := Y; 38. X := Y; | >>> insufficient permission for "Y" >>> expected at least "read_write", got "write_only" 39. end Bad_Move; 40. 41. end Pointers; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-12 Georges-Axel Jaloyan <jaloyan@adacore.com> * debug.adb: Reserving flag -gnatdF for safe pointer checking. * gnat1drv.adb (gnat1drv): Adding the call to the analysis on dF flag. * sem_spark.adb, sem_spark.ads: Implementation of the analysis, in preparation for the evolution of the SPARK language that includes a pointer analysis for checking non-aliasing of access types. The Check_Safe_Pointers function is the entry point, and will traverse the AST and raise compile-time errors everytime it detects non-begign aliasing. Detailed comments are present in the sem_spark.ads file. * sem_util.adb, sem_util.ads (First_Global, Next_Global): New functions to iterate over the list of globals of a subprogram. * libgnat/system.ads: Add restriction No_Finalization. * gcc-interface/Make-lang.in: Add new file sem_spark.adb and dependency on g-dynhta.adb.