OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
f6d17c4d02
gcc/gcc/ada/sem_spark.adb
Arnaud Charlet 4dfba737a4 [Ada] Bump copyright notices to 2018 
2018-01-11  Arnaud Charlet  <charlet@adacore.com>

gcc/ada/

	Bump copyright notices to 2018.

From-SVN: r256519
2018-01-11 08:55:25 +00:00

6197 lines
200 KiB
Ada
Raw Blame History

------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- S E M _ S P A R K --
-- --
-- B o d y --
-- --
-- Copyright (C) 2017-2018, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- 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;
when N_Reduction_Expression =>
null;
when N_Reduction_Expression_Parameter =>
null;
-- 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_Call_Marker
| 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
| N_Variable_Reference_Marker
=>
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;
Reference in New Issue View Git Blame Copy Permalink