-- --
-- B o d y --
-- --
--- Copyright (C) 2017-2018, Free Software Foundation, Inc. --
+-- Copyright (C) 2017-2019, 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- --
package body Sem_SPARK is
- -------------------------------------------------
- -- Handling of Permissions Associated to Paths --
- -------------------------------------------------
+ ---------------------------------------------------
+ -- Handling of Permissions Associated with Paths --
+ ---------------------------------------------------
package Permissions is
Elaboration_Context_Max : constant := 1009;
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
+ -- The hash function
+
+ -- Permission type associated with paths. These are related to but not
+ -- the same as the states associated with names used in SPARK RM 3.10:
+ -- Unrestricted, Observed, Borrowed, Moved. When ownership rules lead to
+ -- a state change for a name, this may correspond to multiple permission
+ -- changes for the paths corresponding to the name, its prefixes, and
+ -- its extensions. For example, when an object is assigned to, the
+ -- corresponding name gets into state Moved, while the path for the name
+ -- gets permission Write_Only as well as every prefix of the name, and
+ -- every suffix gets permission No_Access.
+
+ type Perm_Kind_Option is
+ (None,
+ -- Special value used when no permission is passed around
+
+ No_Access,
+ -- The path cannot be accessed for reading or writing. This is the
+ -- case for the path of a name in the Borrowed state.
+
+ Read_Only,
+ -- The path can only be accessed for reading. This is the case for
+ -- the path of a name in the Observed state.
+
+ Read_Write,
+ -- The path can be accessed for both reading and writing. This is the
+ -- case for the path of a name in the Unrestricted state.
+
+ Write_Only
+ -- The path can only be accessed for writing. This is the case for
+ -- the path of a name in the Moved state.
+ );
+ subtype Perm_Kind is Perm_Kind_Option range No_Access .. Write_Only;
subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
package Perm_Tree_Maps is new Simple_HTable
(Header_Num => Elaboration_Context_Index,
- Key => Node_Id,
+ Key => Entity_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 instantation of a hash table, with keys being entities and values
+ -- being pointers to permission trees. This is used to define global
+ -- environment permissions (entities in that case are stand-alone
+ -- objects or formal parameters), as well as the permissions for the
+ -- extensions of a Record_Component node (entities in that case are
+ -- record components).
-- 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.
+ -- permission at each node, and depending on the type of the node, can
+ -- have zero, one, or more children reached through 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.
+ -- Whether this node is of a "deep" type, i.e. an access type or a
+ -- composite type containing access type subcomponents. This
+ -- corresponds to both "observing" and "owning" types in SPARK RM
+ -- 3.10. To be used when moving the path.
- case Kind is
+ Explanation : Node_Id;
+ -- Node that can be used in an explanation for a permission mismatch
+ 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.
+ -- extension of that node if that permission is different from the
+ -- node's permission.
- when Entire_Object =>
+ when Entire_Object =>
Children_Permission : Perm_Kind;
-- Unfolded path of access type. The permission of the object
-- pointed to is given in Get_All.
- when Reference =>
+ when Reference =>
Get_All : Perm_Tree_Access;
- -- Unfolded path of array type. The permission of the elements is
+ -- Unfolded path of array type. The permission of elements is
-- given in Get_Elem.
- when Array_Component =>
+ when Array_Component =>
Get_Elem : Perm_Tree_Access;
- -- Unfolded path of record type. The permission of the regular
- -- components is given in Component. The permission of unknown
- -- components (for objects of tagged type) is given in
- -- Other_Components.
+ -- Unfolded path of record type. The permission of the components
+ -- is given in Component.
when Record_Component =>
Component : Perm_Tree_Maps.Instance;
- Other_Components : Perm_Tree_Access;
end case;
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.
+ -- The definition of a permission environment for the analysis. This is
+ -- just a hash table from entities to permission trees.
type Perm_Env_Access is access Perm_Env;
-- Access to permission environments
-- The type defining the hash table saving the environments at the entry
-- of each loop.
- package Boolean_Variables_Maps is new Simple_HTable
+ package Variable_Maps is new Simple_HTable
(Header_Num => Elaboration_Context_Index,
Key => Entity_Id,
- Element => Boolean,
- No_Element => False,
+ Element => Node_Id,
+ No_Element => Empty,
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;
+ type Variable_Mapping is new Variable_Maps.Instance;
+ -- Mapping from variables to nodes denoting paths that are observed or
+ -- borrowed by the variable.
--------------------
-- Simple Getters --
function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
+ function Explanation (T : Perm_Tree_Access) return Node_Id;
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;
-----------------------
procedure Copy_Env
(From : Perm_Env;
- To : in out 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 Move_Env (From, To : in out Perm_Env);
+ -- Procedure to move a permission environment. It frees To, moves From
+ -- in To and sets From to Nil.
+
+ procedure Move_Variable_Mapping (From, To : in out Variable_Mapping);
+ -- Move a variable mapping, freeing memory as needed and resetting the
+ -- source mapping.
- procedure Copy_Tree
- (From : Perm_Tree_Access;
- To : Perm_Tree_Access);
+ procedure Copy_Tree (From, To : Perm_Tree_Access);
-- Procedure to copy a permission tree
- procedure Free_Env
- (PE : in out Perm_Env);
+ 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 Free_Tree (PT : in out Perm_Tree_Access);
-- Procedure to free a permission tree
--------------------
--------------------
procedure Perm_Mismatch
- (Exp_Perm, Act_Perm : Perm_Kind;
- N : Node_Id);
+ (N : Node_Id;
+ Exp_Perm : Perm_Kind;
+ Act_Perm : Perm_Kind;
+ Expl : Node_Id;
+ Forbidden_Perm : Boolean := False);
-- 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.
-- Children_Permission --
-------------------------
- function Children_Permission
- (T : Perm_Tree_Access)
- return Perm_Kind
- is
+ function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
begin
return T.all.Tree.Children_Permission;
end Children_Permission;
-- Component --
---------------
- function Component
- (T : Perm_Tree_Access)
- return Perm_Tree_Maps.Instance
+ function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance
is
begin
return T.all.Tree.Component;
-- Copy_Env --
--------------
- procedure Copy_Env
- (From : Perm_Env;
- To : in out Perm_Env)
- is
+ procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is
Comp_From : Perm_Tree_Access;
- Key_From : Perm_Tree_Maps.Key_Option;
- Son : Perm_Tree_Access;
+ Key_From : Perm_Tree_Maps.Key_Option;
+ Son : Perm_Tree_Access;
begin
- Reset (To);
+ Free_Env (To);
Key_From := Get_First_Key (From);
while Key_From.Present loop
Comp_From := Get (From, Key_From.K);
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
+ procedure Copy_Tree (From, To : Perm_Tree_Access) is
begin
+ -- Copy the direct components of the tree
+
To.all := From.all;
+ -- Now reallocate access components for a deep copy of the tree
+
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 =>
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.
+ -- 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;
begin
CompO := Get_First (PE);
while CompO /= null loop
- Free_Perm_Tree (CompO);
+ Free_Tree (CompO);
CompO := Get_Next (PE);
end loop;
+
+ Reset (PE);
end Free_Env;
- --------------------
- -- Free_Perm_Tree --
- --------------------
+ ---------------
+ -- Free_Tree --
+ ---------------
- procedure Free_Perm_Tree
- (PT : in out Perm_Tree_Access)
- is
+ procedure Free_Tree (PT : in out Perm_Tree_Access) is
procedure Free_Perm_Tree_Dealloc is
new Ada.Unchecked_Deallocation
(Perm_Tree_Wrapper, Perm_Tree_Access);
begin
case Kind (PT) is
when Entire_Object =>
- Free_Perm_Tree_Dealloc (PT);
+ null;
when Reference =>
- Free_Perm_Tree (PT.all.Tree.Get_All);
- Free_Perm_Tree_Dealloc (PT);
+ Free_Tree (PT.all.Tree.Get_All);
when Array_Component =>
- Free_Perm_Tree (PT.all.Tree.Get_Elem);
+ Free_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);
+ Free_Tree (Comp);
Comp := Perm_Tree_Maps.Get_Next (Component (PT));
end loop;
end;
- Free_Perm_Tree_Dealloc (PT);
end case;
- end Free_Perm_Tree;
+
+ Free_Perm_Tree_Dealloc (PT);
+ end Free_Tree;
+
+ -----------------
+ -- Explanation --
+ -----------------
+
+ function Explanation (T : Perm_Tree_Access) return Node_Id is
+ begin
+ return T.all.Tree.Explanation;
+ end Explanation;
-------------
-- Get_All --
-------------
- function Get_All
- (T : Perm_Tree_Access)
- return Perm_Tree_Access
- is
+ function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
begin
return T.all.Tree.Get_All;
end Get_All;
-- Get_Elem --
--------------
- function Get_Elem
- (T : Perm_Tree_Access)
- return Perm_Tree_Access
- is
+ function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
begin
return T.all.Tree.Get_Elem;
end Get_Elem;
-- Is_Node_Deep --
------------------
- function Is_Node_Deep
- (T : Perm_Tree_Access)
- return Boolean
- is
+ function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
begin
return T.all.Tree.Is_Node_Deep;
end Is_Node_Deep;
-- Kind --
----------
- function Kind
- (T : Perm_Tree_Access)
- return Path_Kind
- is
+ function Kind (T : Perm_Tree_Access) return Path_Kind is
begin
return T.all.Tree.Kind;
end Kind;
- ----------------------
- -- Other_Components --
- ----------------------
+ --------------
+ -- Move_Env --
+ --------------
- function Other_Components
- (T : Perm_Tree_Access)
- return Perm_Tree_Access
- is
+ procedure Move_Env (From, To : in out Perm_Env) is
+ begin
+ Free_Env (To);
+ To := From;
+ From := Perm_Env (Perm_Tree_Maps.Nil);
+ end Move_Env;
+
+ ---------------------------
+ -- Move_Variable_Mapping --
+ ---------------------------
+
+ procedure Move_Variable_Mapping (From, To : in out Variable_Mapping) is
begin
- return T.all.Tree.Other_Components;
- end Other_Components;
+ Reset (To);
+ To := From;
+ From := Variable_Mapping (Variable_Maps.Nil);
+ end Move_Variable_Mapping;
----------------
-- Permission --
----------------
- function Permission
- (T : Perm_Tree_Access)
- return Perm_Kind
- is
+ function Permission (T : Perm_Tree_Access) return Perm_Kind is
begin
return T.all.Tree.Permission;
end Permission;
-------------------
procedure Perm_Mismatch
- (Exp_Perm, Act_Perm : Perm_Kind;
- N : Node_Id)
+ (N : Node_Id;
+ Exp_Perm : Perm_Kind;
+ Act_Perm : Perm_Kind;
+ Expl : Node_Id;
+ Forbidden_Perm : Boolean := False)
is
begin
- Error_Msg_N ("\expected at least `"
- & Perm_Kind'Image (Exp_Perm) & "`, got `"
- & Perm_Kind'Image (Act_Perm) & "`", N);
+ Error_Msg_Sloc := Sloc (Expl);
+
+ if Forbidden_Perm then
+ if Exp_Perm = No_Access then
+ Error_Msg_N ("\object was moved #", N);
+ else
+ raise Program_Error;
+ end if;
+ else
+ case Exp_Perm is
+ when Write_Perm =>
+ if Act_Perm = Read_Only then
+ Error_Msg_N
+ ("\object was declared as not writeable #", N);
+ else
+ Error_Msg_N ("\object was moved #", N);
+ end if;
+
+ when Read_Only =>
+ Error_Msg_N ("\object was moved #", N);
+
+ when No_Access =>
+ raise Program_Error;
+ end case;
+ end if;
end Perm_Mismatch;
end 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.
+ -- The different modes for analysis. This allows checking whether a path
+ -- has the right permission, and also updating permissions when a path is
+ -- moved, borrowed, or observed.
- type Checking_Mode is
+ type Extended_Checking_Mode is
- (Read,
- -- Default mode. Checks that paths have Read_Perm permission.
+ (Read_Subexpr,
+ -- Special value used for assignment, to check that subexpressions of
+ -- the assigned path are readable.
+
+ Read,
+ -- Default mode
Move,
- -- Regular moving semantics (not under 'Access). Checks that paths have
- -- Read_Write permission. After moving a path, its permission is set to
- -- Write_Only and the permission of its extensions is set to No_Access.
+ -- Move semantics. Checks that paths have Read_Write permission. After
+ -- moving a path, its permission and the permission of its prefixes are
+ -- set to Write_Only, while 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.
+ -- assigning to a path, its permission and the permission of its
+ -- extensions are set to Read_Write. The permission of its prefixes may
+ -- be normalized from Write_Only to Read_Write depending on other
+ -- permissions in the tree (a prefix gets permission Read_Write when all
+ -- its extensions become Read_Write).
- 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.
+ Borrow,
+ -- Borrow semantics. Checks that paths have Read_Write permission. After
+ -- borrowing a path, its permission and the permission of its prefixes
+ -- and extensions are set to No_Access.
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
+ -- Observe semantics. Checks that paths have Read_Perm permission. After
+ -- observing a path, its permission and the permission of its prefixes
+ -- and extensions are set to Read_Only.
);
- type Result_Kind is (Folded, Unfolded, Function_Call);
+ subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe;
+
+ type Result_Kind is (Folded, Unfolded);
-- 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
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;
+ when Folded =>
+ Found_Permission : Perm_Kind;
+ Explanation : Node_Id;
+ when Unfolded =>
+ Tree_Access : Perm_Tree_Access;
end case;
end record;
+ type Error_Status is (OK, Error);
+
-----------------------
-- Local subprograms --
-----------------------
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_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id);
+ -- Handle assignment as part of an assignment statement or an object
+ -- declaration.
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.
+ -- Entry point for the analysis of a subprogram or entry body
procedure Check_Declaration (Decl : Node_Id);
- procedure Check_Expression (Expr : Node_Id);
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
+ -- Check the legality of declaration Decl regarding rules not related to
+ -- permissions. Update Legal to False if a rule is violated. Issue an
+ -- error message if Force is True and Emit_Messages returns True.
+
+ procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
+ pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
+ N_Range_Constraint,
+ N_Subtype_Indication,
+ N_Digits_Constraint,
+ N_Delta_Constraint)
+ or else Nkind (Expr) in N_Subexpr);
+
+ procedure Check_Globals (Subp : Entity_Id);
+ -- This procedure takes a subprogram called and checks the permission of
+ -- globals.
- 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
+ -- Checking proceduress for safe pointer usage. These procedures traverse
+ -- the AST, check nodes for correct permissions according to SPARK RM 3.10,
+ -- and update permissions depending on the node kind. The main procedure
+ -- Check_Node is mutually recursive with the specialized procedures that
+ -- follow.
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_Loop_Statement (Stmt : 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.
+ -- Main traversal procedure to check safe pointer usage
+
+ procedure Check_Old_Loop_Entry (N : Node_Id);
+ -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
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_Package_Spec (Pack : Node_Id);
- 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_Parameter_Or_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean);
+ -- Check the permission of every actual parameter or global
- 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_Pragma (Prag : Node_Id);
- 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_Source_Of_Borrow_Or_Observe
+ (Expr : Node_Id;
+ Status : out Error_Status);
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.
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
+ -- Check that type Typ is either not deep, or that it is an observing or
+ -- owning type according to SPARK RM 3.10
- 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_Expl (N : Node_Or_Entity_Id) return Node_Id;
+ -- The function that takes a name as input and returns an explanation node
+ -- for the permission associated with it.
- 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 Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
+ pragma Precondition (Is_Path_Expression (Expr));
+ -- Return the expression being borrowed/observed when borrowing or
+ -- observing Expr. If Expr is a call to a traversal function, this is
+ -- the first actual, otherwise it is Expr.
- 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 Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
+ -- The function that takes a name as input and returns a permission
+ -- associated with it.
- 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 Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
+ pragma Precondition (Is_Path_Expression (N));
+ -- This function gets a node and looks recursively to find the appropriate
+ -- subtree for that node. If the tree is folded on that node, then it
+ -- returns the permission given at the right level.
- 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.
+ function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
+ pragma Precondition (Is_Path_Expression (N));
+ -- This function gets a node and looks recursively to find the appropriate
+ -- subtree for that node. If the tree is folded, then it unrolls the tree
+ -- up to the appropriate level.
+
+ function Get_Root_Object
+ (Expr : Node_Id;
+ Through_Traversal : Boolean := True;
+ Is_Traversal : Boolean := False) return Entity_Id;
+ -- Return the root of the path expression Expr, or Empty for an allocator,
+ -- NULL, or a function call. Through_Traversal is True if it should follow
+ -- through calls to traversal functions. Is_Traversal is True if this
+ -- corresponds to a value returned from a traversal function, which should
+ -- allow if-expressions and case-expressions that refer to the same root,
+ -- even if the paths are not the same in all branches.
+
+ generic
+ with procedure Handle_Parameter_Or_Global
+ (Expr : Node_Id;
+ Formal_Typ : Entity_Id;
+ Param_Mode : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean);
+ procedure Handle_Globals (Subp : Entity_Id);
+ -- Handling of globals is factored in a generic instantiated below
+
+ function Has_Array_Component (Expr : Node_Id) return Boolean;
+ pragma Precondition (Is_Path_Expression (Expr));
+ -- This function gets a node and looks recursively to determine whether the
+ -- given path has any array 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);
+ procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : 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_Path_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean;
+ -- Return whether Expr corresponds to a path. Is_Traversal is True if this
+ -- corresponds to a value returned from a traversal function, which should
+ -- allow if-expressions and case-expressions.
- 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_Subpath_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean;
+ -- Return True if Expr can be part of a path expression. Is_Traversal is
+ -- True if this corresponds to a value returned from a traversal function,
+ -- which should allow if-expressions and case-expressions.
- 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 Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
+ -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
+ -- a prefix, in the sense that they could still refer to overlapping memory
+ -- locations.
+
+ function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean;
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);
+ procedure Merge_Env (Source : in out Perm_Env; Target : 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);
+ (N : Node_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id;
+ Forbidden_Perm : Boolean := False);
-- 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.
+ -- rules established by the RM. This function is called with the node and
+ -- the permission that was expected, and issues 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);
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id);
-- 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
+ -- rules established by the RM at the end of subprograms. This function is
+ -- called with the node, 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 Process_Path (Expr : Node_Id; Mode : Checking_Mode);
+ pragma Precondition (Is_Path_Expression (Expr));
+ -- Check correct permission for the path in the checking mode Mode, and
+ -- update permissions of the path and its prefixes/extensions.
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.
+ -- of the subprogram indeed have Read_Write permission at the end of the
+ -- subprogram execution.
procedure Return_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id);
+ (Id : Entity_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean);
-- Auxiliary procedure to Return_Parameters and Return_Globals
procedure Return_Parameters (Subp : Entity_Id);
- -- Takes a subprogram as input, and checks that all borrowed parameters of
- -- the subprogram indeed have RW permission at the end of the subprogram
- -- execution.
+ -- Takes a subprogram as input, and checks that all out parameters of the
+ -- subprogram indeed have Read_Write permission at the end of the
+ -- subprogram execution.
- procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
+ procedure Set_Perm_Extensions
+ (T : Perm_Tree_Access;
+ P : Perm_Kind;
+ Expl : Node_Id);
-- 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);
+ procedure Set_Perm_Extensions_Move
+ (T : Perm_Tree_Access;
+ E : Entity_Id;
+ Expl : Node_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
+ function Set_Perm_Prefixes
+ (N : Node_Id;
+ Perm : Perm_Kind_Option;
+ Expl : Node_Id) return Perm_Tree_Access;
+ pragma Precondition (Is_Path_Expression (N));
+ -- This function modifies the permissions of a given node in the permission
+ -- environment as well as all the prefixes of the path, to the new
+ -- permission Perm. The general rule here is that everybody updates the
+ -- permission of the subtree they are returning.
+
+ procedure Set_Perm_Prefixes_Assign (N : Node_Id);
+ pragma Precondition (Is_Path_Expression (N));
+ -- This procedure 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.
-- 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
+ -- Example: We assign x.y and x.z, and then Set_Perm_Prefixes_Assign 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.
+ -- permission RW.
procedure Setup_Globals (Subp : Entity_Id);
-- Takes a subprogram as input, and sets up the environment by adding
-- global items with appropriate permissions.
procedure Setup_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind);
+ (Id : Entity_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean;
+ Expl : Node_Id);
-- 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.
+ procedure Setup_Protected_Components (Subp : Entity_Id);
+ -- Takes a protected operation as input, and sets up the environment by
+ -- adding protected components with appropriate permissions.
+
----------------------
-- Global Variables --
----------------------
-- 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.
+ Inside_Procedure_Call : Boolean := False;
+ -- Set while checking the actual parameters of a procedure or entry call
+
+ Inside_Elaboration : Boolean := False;
+ -- Set during package spec/body elaboration, during which move and local
+ -- observe/borrow are not allowed. As a result, no other checking is needed
+ -- during elaboration.
Current_Loops_Envs : Env_Backups;
-- This variable contains saves of permission environments at each loop the
-- 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.
+ Current_Borrowers : Variable_Mapping;
+ -- Mapping from borrowers to the path borrowed
+
+ Current_Observers : Variable_Mapping;
+ -- Mapping from observers to the path observed
+
+ --------------------
+ -- Handle_Globals --
+ --------------------
+
+ -- Generic procedure is defined first so that instantiations can be defined
+ -- anywhere afterwards.
+
+ procedure Handle_Globals (Subp : Entity_Id) is
+
+ -- Local subprograms
+
+ procedure Handle_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind);
+ -- Handle global items from the list starting at Item
+
+ procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id);
+ -- Handle global items for the mode Global_Mode
+
+ ------------------------------
+ -- Handle_Globals_From_List --
+ ------------------------------
+
+ procedure Handle_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
+ Handle_Parameter_Or_Global (Expr => Item,
+ Formal_Typ => Retysp (Etype (Item)),
+ Param_Mode => Kind,
+ Subp => Subp,
+ Global_Var => True);
+ end if;
+
+ Next_Global (Item);
+ end loop;
+ end Handle_Globals_From_List;
+
+ ----------------------------
+ -- Handle_Globals_Of_Mode --
+ ----------------------------
+
+ procedure Handle_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;
+
+ -- Check both global items from Global and Refined_Global pragmas
+
+ Handle_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
+ Handle_Globals_From_List
+ (First_Global (Subp, Global_Mode, Refined => True), Kind);
+ end Handle_Globals_Of_Mode;
+
+ -- Start of processing for Handle_Globals
+
+ begin
+ Handle_Globals_Of_Mode (Name_Proof_In);
+ Handle_Globals_Of_Mode (Name_Input);
+ Handle_Globals_Of_Mode (Name_Output);
+ Handle_Globals_Of_Mode (Name_In_Out);
+ end Handle_Globals;
----------
-- "<=" --
----------
- function "<=" (P1, P2 : Perm_Kind) return Boolean
- is
+ function "<=" (P1, P2 : Perm_Kind) return Boolean is
begin
return P2 >= P1;
end "<=";
-- ">=" --
----------
- function ">=" (P1, P2 : Perm_Kind) return Boolean
- is
+ function ">=" (P1, P2 : Perm_Kind) return Boolean is
begin
case P2 is
when No_Access => return True;
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);
+ ----------------------
+ -- Check_Assignment --
+ ----------------------
- -- We first check the Read access on every in parameter
+ procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is
- Current_Checking_Mode := Read;
- Iterate_Call_Read (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global), Read);
+ -- Local subprograms
- -- 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.
+ procedure Handle_Borrow
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean);
+ -- Update map of current borrowers
- Iterate_Call_Observes (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global),
- Observe);
+ procedure Handle_Observe
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean);
+ -- Update map of current observers
- Iterate_Call_Outs (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global),
- Borrow_Out);
+ -------------------
+ -- Handle_Borrow --
+ -------------------
- Iterate_Call (Call);
- Check_Globals (Get_Pragma
- (Get_Called_Entity (Call), Pragma_Global), Move);
+ procedure Handle_Borrow
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean)
+ is
+ Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
- -- Restore environment, because after borrowing/observing actual
- -- parameters, they get their permission reverted to the ones before
- -- the call.
+ begin
+ -- SPARK RM 3.10(8): If the type of the target is an anonymous
+ -- access-to-variable type (an owning access type), the source shall
+ -- be an owning access object [..] whose root object is the target
+ -- object itself.
- Free_Env (Current_Perm_Env);
+ -- ??? In fact we could be slightly more permissive in allowing even
+ -- a call to a traversal function of the right form.
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ if not Is_Decl
+ and then (Is_Traversal_Function_Call (Expr)
+ or else Get_Root_Object (Borrowed) /= Var)
+ then
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of assignment must have & as root" &
+ " (SPARK RM 3.10(8)))",
+ Expr, Var);
+ end if;
+ return;
+ end if;
- Free_Env (Saved_Env);
+ Set (Current_Borrowers, Var, Borrowed);
+ end Handle_Borrow;
- -- 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);
+ --------------------
+ -- Handle_Observe --
+ --------------------
- end Check_Call_Statement;
+ procedure Handle_Observe
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean)
+ is
+ Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
- -------------------------
- -- Check_Callable_Body --
- -------------------------
+ begin
+ -- ??? We are currently using the same restriction for observers
+ -- as for borrowers. To be seen if the SPARK RM current rule really
+ -- allows more uses.
- procedure Check_Callable_Body (Body_N : Node_Id) is
+ if not Is_Decl
+ and then (Is_Traversal_Function_Call (Expr)
+ or else Get_Root_Object (Observed) /= Var)
+ then
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of assignment must have & as root" &
+ " (SPARK RM 3.10(8)))",
+ Expr, Var);
+ end if;
+ return;
+ end if;
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ Set (Current_Observers, Var, Observed);
+ end Handle_Observe;
- Saved_Env : Perm_Env;
- Saved_Init_Map : Initialization_Map;
+ -- Local variables
- New_Env : Perm_Env;
+ Target_Typ : constant Node_Id := Etype (Target);
+ Is_Decl : constant Boolean := Nkind (Target) = N_Defining_Identifier;
+ Target_Root : Entity_Id;
+ Expr_Root : Entity_Id;
+ Perm : Perm_Kind;
+ Status : Error_Status;
+ Dummy : Boolean := True;
- Body_Id : constant Entity_Id := Defining_Entity (Body_N);
- Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
+ -- Start of processing for Check_Assignment
begin
- -- Check if SPARK pragma is not set to Off
+ Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
- 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
+ if Is_Anonymous_Access_Type (Target_Typ) then
+ Check_Source_Of_Borrow_Or_Observe (Expr, Status);
+
+ if Status /= OK then
return;
end if;
- else
- return;
- end if;
-
- -- Save environment and put a new one in place
- Copy_Env (Current_Perm_Env, Saved_Env);
+ if Is_Decl then
+ Target_Root := Target;
+ else
+ Target_Root := Get_Root_Object (Target);
+ end if;
- -- Save initialization map
+ Expr_Root := Get_Root_Object (Expr);
- Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
+ -- SPARK RM 3.10(7): For an assignment statement where the target is
+ -- a stand-alone object of an anonymous access-to-object type.
- Current_Checking_Mode := Read;
- Current_Perm_Env := New_Env;
+ pragma Assert (Present (Target_Root));
- -- Add formals and globals to the environment with adequate permissions
+ -- If the type of the target is an anonymous access-to-constant type
+ -- (an observing access type), the source shall be an owning access
+ -- object denoted by a name that is not in the Moved state, and whose
+ -- root object is not in the Moved state and is not declared at a
+ -- statically deeper accessibility level than that of the target
+ -- object.
- if Is_Subprogram_Or_Entry (Spec_Id) then
- Setup_Parameters (Spec_Id);
- Setup_Globals (Spec_Id);
- end if;
+ if Is_Access_Constant (Target_Typ) then
+ Perm := Get_Perm (Expr);
- -- Analyze the body of the function
+ if Perm = No_Access then
+ Perm_Error (Expr, No_Access, No_Access,
+ Expl => Get_Expl (Expr),
+ Forbidden_Perm => True);
+ return;
+ end if;
- Check_List (Declarations (Body_N));
- Check_Node (Handled_Statement_Sequence (Body_N));
+ Perm := Get_Perm (Expr_Root);
- -- Check the read-write permissions of borrowed parameters/globals
+ if Perm = No_Access then
+ Perm_Error (Expr, No_Access, No_Access,
+ Expl => Get_Expl (Expr_Root),
+ Forbidden_Perm => True);
+ return;
+ end if;
- 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;
+ -- ??? check accessibility level
- -- Free the environments
+ -- If the type of the target is an anonymous access-to-variable
+ -- type (an owning access type), the source shall be an owning
+ -- access object denoted by a name that is in the Unrestricted
+ -- state, and whose root object is the target object itself.
- Free_Env (Current_Perm_Env);
+ Check_Expression (Expr, Observe);
+ Handle_Observe (Target_Root, Expr, Is_Decl);
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ else
+ Perm := Get_Perm (Expr);
- Free_Env (Saved_Env);
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- -- Restore initialization map
+ if not Is_Decl then
+ if not Is_Entity_Name (Target) then
+ if Emit_Messages then
+ Error_Msg_N
+ ("target of borrow must be stand-alone variable",
+ Target);
+ end if;
+ return;
- Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
+ elsif Target_Root /= Expr_Root then
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of borrow must be variable &",
+ Expr, Target);
+ end if;
+ return;
+ end if;
+ end if;
- Reset (Saved_Init_Map);
+ Check_Expression (Expr, Borrow);
+ Handle_Borrow (Target_Root, Expr, Is_Decl);
+ end if;
- -- The assignment of all out parameters will be done by caller
+ elsif Is_Deep (Target_Typ) then
- Current_Checking_Mode := Mode_Before;
- end Check_Callable_Body;
+ if Is_Path_Expression (Expr) then
+ Check_Expression (Expr, Move);
- -----------------------
- -- Check_Declaration --
- -----------------------
+ else
+ if Emit_Messages then
+ Error_Msg_N ("expression not allowed as source of move", Expr);
+ end if;
+ return;
+ end if;
- 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;
+ else
+ Check_Expression (Expr, Read);
+ end if;
+ end Check_Assignment;
- when N_Object_Declaration =>
- -- First move the right-hand side
- Current_Checking_Mode := Move;
- Check_Node (Expression (Decl));
+ --------------------------
+ -- Check_Call_Statement --
+ --------------------------
- declare
- Elem : Perm_Tree_Access;
+ procedure Check_Call_Statement (Call : Node_Id) is
- 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;
+ Subp : constant Entity_Id := Get_Called_Entity (Call);
+
+ -- Local subprograms
- -- Create new tree for defining identifier
+ procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Check the permission of every actual parameter
- Set (Current_Perm_Env,
- Unique_Entity (Defining_Identifier (Decl)),
- Elem);
+ procedure Update_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Update the permission of OUT actual parameters
- pragma Assert (Get_First (Current_Perm_Env)
- /= null);
+ -----------------
+ -- Check_Param --
+ -----------------
- end;
+ procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
+ begin
+ Check_Parameter_Or_Global
+ (Expr => Actual,
+ Typ => Retysp (Etype (Formal)),
+ Kind => Ekind (Formal),
+ Subp => Subp,
+ Global_Var => False);
+ end Check_Param;
+
+ ------------------
+ -- Update_Param --
+ ------------------
+
+ procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
+
+ begin
+ case Formal_Kind'(Mode) is
+ when E_Out_Parameter =>
+ Check_Expression (Actual, Assign);
+
+ when others =>
+ null;
+ end case;
+ end Update_Param;
+
+ procedure Check_Params is new
+ Iterate_Call_Parameters (Check_Param);
+
+ procedure Update_Params is new
+ Iterate_Call_Parameters (Update_Param);
+
+ -- Start of processing for Check_Call_Statement
+
+ begin
+ Inside_Procedure_Call := True;
+ Check_Params (Call);
+ if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then
+ if Emit_Messages then
+ Error_Msg_N
+ ("call through access to subprogram is not allowed in SPARK",
+ Call);
+ end if;
+ else
+ Check_Globals (Get_Called_Entity (Call));
+ end if;
+
+ Inside_Procedure_Call := False;
+ Update_Params (Call);
+ end Check_Call_Statement;
+
+ -------------------------
+ -- Check_Callable_Body --
+ -------------------------
+
+ procedure Check_Callable_Body (Body_N : Node_Id) is
+ Save_In_Elab : constant Boolean := Inside_Elaboration;
+ Body_Id : constant Entity_Id := Defining_Entity (Body_N);
+ Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
+ Prag : constant Node_Id := SPARK_Pragma (Body_Id);
+
+ Saved_Env : Perm_Env;
+ Saved_Borrowers : Variable_Mapping;
+ Saved_Observers : Variable_Mapping;
+
+ begin
+ -- Only SPARK bodies are analyzed
+
+ if No (Prag)
+ or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On
+ then
+ return;
+ end if;
+
+ Inside_Elaboration := False;
+
+ if Ekind (Spec_Id) = E_Function
+ and then Is_Anonymous_Access_Type (Etype (Spec_Id))
+ and then not Is_Traversal_Function (Spec_Id)
+ then
+ if Emit_Messages then
+ Error_Msg_N ("anonymous access type for result only allowed for "
+ & "traversal functions", Spec_Id);
+ end if;
+ return;
+ end if;
+
+ -- Save environment and put a new one in place
+
+ Move_Env (Current_Perm_Env, Saved_Env);
+ Move_Variable_Mapping (Current_Borrowers, Saved_Borrowers);
+ Move_Variable_Mapping (Current_Observers, Saved_Observers);
+
+ -- 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;
+
+ -- For protected operations, add protected components to the environment
+ -- with adequate permissions.
+
+ if Is_Protected_Operation (Spec_Id) then
+ Setup_Protected_Components (Spec_Id);
+ end if;
+
+ -- Analyze the body of the subprogram
+
+ 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;
+
+ -- Restore the saved environment and free the current one
+
+ Move_Env (Saved_Env, Current_Perm_Env);
+ Move_Variable_Mapping (Saved_Borrowers, Current_Borrowers);
+ Move_Variable_Mapping (Saved_Observers, Current_Observers);
+
+ Inside_Elaboration := Save_In_Elab;
+ end Check_Callable_Body;
+
+ -----------------------
+ -- Check_Declaration --
+ -----------------------
+
+ procedure Check_Declaration (Decl : Node_Id) is
+ Target : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : constant Node_Id := Etype (Target);
+ Expr : Node_Id;
+ Dummy : Boolean := True;
+
+ begin
+ -- Start with legality rules not related to permissions
+
+ Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
+
+ -- Now check permission-related legality rules
+
+ case N_Declaration'(Nkind (Decl)) is
+ when N_Full_Type_Declaration =>
+ null;
+
+ -- ??? What about component declarations with defaults.
when N_Subtype_Declaration =>
- Check_Node (Subtype_Indication (Decl));
+ Check_Expression (Subtype_Indication (Decl), Read);
+
+ when N_Object_Declaration =>
+ Expr := Expression (Decl);
+
+ if Present (Expr) then
+ Check_Assignment (Target => Target,
+ Expr => Expr);
+ end if;
+
+ if Is_Deep (Target_Typ) then
+ declare
+ Tree : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => True,
+ Explanation => Decl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ begin
+ Set (Current_Perm_Env, Target, Tree);
+ end;
+ end if;
when N_Iterator_Specification =>
- pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
null;
when N_Loop_Parameter_Specification =>
- pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl))));
null;
-- Checking should not be called directly on these nodes
- when N_Component_Declaration
- | N_Function_Specification
+ when N_Function_Specification
| N_Entry_Declaration
| N_Procedure_Specification
+ | N_Component_Declaration
=>
raise Program_Error;
end case;
end Check_Declaration;
- ----------------------
- -- Check_Expression --
- ----------------------
+ --------------------------------
+ -- Check_Declaration_Legality --
+ --------------------------------
- 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);
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
- when N_Identifier
- | N_Expanded_Name
- =>
- -- Check if identifier is pointing to nothing (On/Off/...)
- if not Present (Entity (Expr)) then
- return;
- end if;
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
- -- Do not analyze things that are not of object Kind
- if Ekind (Entity (Expr)) not in Object_Kind then
- return;
- end if;
+ -------------------
+ -- Emit_Messages --
+ -------------------
- -- Consider as ident
- Process_Path (Expr);
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
- -- Switch to read mode and then check the readability of each operand
+ -- Local variables
- when N_Binary_Op =>
+ Target : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : constant Node_Id := Etype (Target);
+ Expr : Node_Id;
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ -- Start of processing for Check_Declaration_Legality
- -- Switch to read mode and then check the readability of each operand
+ begin
+ case N_Declaration'(Nkind (Decl)) is
+ when N_Full_Type_Declaration =>
+ Check_Type_Legality (Target, Force, Legal);
- 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));
+ when N_Subtype_Declaration =>
+ null;
- -- Forbid all deep expressions for Attribute ???
+ when N_Object_Declaration =>
+ Expr := Expression (Decl);
- when N_Attribute_Reference =>
- case Attribute_Name (Expr) is
- when Name_Access =>
- case Current_Checking_Mode is
- when Read =>
- Check_Node (Prefix (Expr));
+ Check_Type_Legality (Target_Typ, Force, Legal);
- when Move =>
- Current_Checking_Mode := Super_Move;
- Check_Node (Prefix (Expr));
+ -- A declaration of a stand-alone object of an anonymous access
+ -- type shall have an explicit initial value and shall occur
+ -- immediately within a subprogram body, an entry body, or a
+ -- block statement (SPARK RM 3.10(4)).
- -- Only assign names, not expressions
+ if Is_Anonymous_Access_Type (Target_Typ) then
+ declare
+ Scop : constant Entity_Id := Scope (Target);
+ begin
+ if not Is_Local_Context (Scop) then
+ if Emit_Messages then
+ Error_Msg_N
+ ("object of anonymous access type must be declared "
+ & "immediately within a subprogram, entry or block "
+ & "(SPARK RM 3.10(4))", Decl);
+ end if;
+ end if;
+ end;
- when Assign =>
- raise Program_Error;
+ if No (Expr) then
+ if Emit_Messages then
+ Error_Msg_N ("object of anonymous access type must be "
+ & "initialized (SPARK RM 3.10(4))", Decl);
+ end if;
+ end if;
+ end if;
- -- Prefix in Super_Move should be a name, error here
+ when N_Iterator_Specification =>
+ null;
- when Super_Move =>
- raise Program_Error;
+ when N_Loop_Parameter_Specification =>
+ null;
- -- Could only borrow names of mode out, not n'Access
+ -- Checking should not be called directly on these nodes
- when Borrow_Out =>
- raise Program_Error;
+ when N_Function_Specification
+ | N_Entry_Declaration
+ | N_Procedure_Specification
+ | N_Component_Declaration
+ =>
+ raise Program_Error;
- when Observe =>
- Check_Node (Prefix (Expr));
- end case;
+ -- Ignored constructs for pointer checking
- when Name_Last
- | Name_First
- =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ 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;
- when Name_Min =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ -- The following nodes are rewritten by semantic analysis
- when Name_Image =>
- Check_Node (Prefix (Expr));
+ when N_Expression_Function =>
+ raise Program_Error;
+ end case;
+ end Check_Declaration_Legality;
- when Name_SPARK_Mode =>
- null;
+ ----------------------
+ -- Check_Expression --
+ ----------------------
- when Name_Value =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ procedure Check_Expression
+ (Expr : Node_Id;
+ Mode : Extended_Checking_Mode)
+ is
+ -- Local subprograms
- when Name_Update =>
- Check_List (Expressions (Expr));
- Check_Node (Prefix (Expr));
+ function Is_Type_Name (Expr : Node_Id) return Boolean;
+ -- Detect when a path expression is in fact a type name
- 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;
+ procedure Move_Expression (Expr : Node_Id);
+ -- Some subexpressions are only analyzed in Move mode. This is a
+ -- specialized version of Check_Expression for that case.
- -- Attributes referring to types (get values from types), hence
- -- no need to check either for borrows or any loans.
+ procedure Move_Expression_List (L : List_Id);
+ -- Call Move_Expression on every expression in the list L
- when Name_Base
- | Name_Val
- =>
- null;
+ procedure Read_Expression (Expr : Node_Id);
+ -- Most subexpressions are only analyzed in Read mode. This is a
+ -- specialized version of Check_Expression for that case.
- -- Other attributes that fall out of the scope of the analysis
+ procedure Read_Expression_List (L : List_Id);
+ -- Call Read_Expression on every expression in the list L
- when others =>
- null;
- end case;
+ procedure Read_Indexes (Expr : Node_Id);
+ -- When processing a path, the index expressions and function call
+ -- arguments occurring on the path should be analyzed in Read mode.
- when N_In =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ ------------------
+ -- Is_Type_Name --
+ ------------------
- when N_Not_In =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ function Is_Type_Name (Expr : Node_Id) return Boolean is
+ begin
+ return Nkind_In (Expr, N_Expanded_Name, N_Identifier)
+ and then Is_Type (Entity (Expr));
+ end Is_Type_Name;
- -- Switch to read mode and then check the readability of each operand
+ ---------------------
+ -- Move_Expression --
+ ---------------------
- 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));
+ -- Distinguish the case where the argument is a path expression that
+ -- needs explicit moving.
- -- Check the arguments of the call
+ procedure Move_Expression (Expr : Node_Id) is
+ begin
+ if Is_Path_Expression (Expr) then
+ Check_Expression (Expr, Move);
+ else
+ Read_Expression (Expr);
+ end if;
+ end Move_Expression;
- when N_Function_Call =>
- Current_Checking_Mode := Read;
- Check_List (Parameter_Associations (Expr));
+ --------------------------
+ -- Move_Expression_List --
+ --------------------------
- when N_Explicit_Dereference =>
- Process_Path (Expr);
+ procedure Move_Expression_List (L : List_Id) is
+ N : Node_Id;
+ begin
+ N := First (L);
+ while Present (N) loop
+ Move_Expression (N);
+ Next (N);
+ end loop;
+ end Move_Expression_List;
- -- Copy environment, run on each branch, and then merge
+ ---------------------
+ -- Read_Expression --
+ ---------------------
- when N_If_Expression =>
- declare
- Saved_Env : Perm_Env;
+ procedure Read_Expression (Expr : Node_Id) is
+ begin
+ Check_Expression (Expr, Read);
+ end Read_Expression;
- -- Accumulator for the different branches
+ --------------------------
+ -- Read_Expression_List --
+ --------------------------
- New_Env : Perm_Env;
+ procedure Read_Expression_List (L : List_Id) is
+ N : Node_Id;
+ begin
+ N := First (L);
+ while Present (N) loop
+ Read_Expression (N);
+ Next (N);
+ end loop;
+ end Read_Expression_List;
- Elmt : Node_Id := First (Expressions (Expr));
+ ------------------
+ -- Read_Indexes --
+ ------------------
- begin
- Current_Checking_Mode := Read;
+ procedure Read_Indexes (Expr : Node_Id) is
- Check_Node (Elmt);
+ -- Local subprograms
- Current_Checking_Mode := Mode_Before;
+ function Is_Singleton_Choice (Choices : List_Id) return Boolean;
+ -- Return whether Choices is a singleton choice
- -- Save environment
+ procedure Read_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Call Read_Expression on the actual
- Copy_Env (Current_Perm_Env,
- Saved_Env);
+ -------------------------
+ -- Is_Singleton_Choice --
+ -------------------------
- -- Here we have the original env in saved, current with a fresh
- -- copy, and new aliased.
+ function Is_Singleton_Choice (Choices : List_Id) return Boolean is
+ Choice : constant Node_Id := First (Choices);
+ begin
+ return List_Length (Choices) = 1
+ and then Nkind (Choice) /= N_Others_Choice
+ and then not Nkind_In (Choice, N_Subtype_Indication, N_Range)
+ and then not
+ (Nkind_In (Choice, N_Identifier, N_Expanded_Name)
+ and then Is_Type (Entity (Choice)));
+ end Is_Singleton_Choice;
+
+ ----------------
+ -- Read_Param --
+ ----------------
+
+ procedure Read_Param (Formal : Entity_Id; Actual : Node_Id) is
+ pragma Unreferenced (Formal);
+ begin
+ Read_Expression (Actual);
+ end Read_Param;
- -- THEN PART
+ procedure Read_Params is new Iterate_Call_Parameters (Read_Param);
- Next (Elmt);
- Check_Node (Elmt);
+ -- Start of processing for Read_Indexes
- -- Here the new_environment contains curr env after then block
+ begin
+ if not Is_Subpath_Expression (Expr) then
+ if Emit_Messages then
+ Error_Msg_N
+ ("name expected here for move/borrow/observe", Expr);
+ end if;
+ return;
+ end if;
- -- ELSE part
+ case N_Subexpr'(Nkind (Expr)) is
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Null
+ =>
+ null;
- -- Restore environment before if
- Copy_Env (Current_Perm_Env,
- New_Env);
+ when N_Explicit_Dereference
+ | N_Selected_Component
+ =>
+ Read_Indexes (Prefix (Expr));
- Free_Env (Current_Perm_Env);
+ when N_Indexed_Component =>
+ Read_Indexes (Prefix (Expr));
+ Read_Expression_List (Expressions (Expr));
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ when N_Slice =>
+ Read_Indexes (Prefix (Expr));
+ Read_Expression (Discrete_Range (Expr));
- -- Here new environment contains the environment after then and
- -- current the fresh copy of old one.
+ -- The argument of an allocator is moved as part of the implicit
+ -- assignment.
- Next (Elmt);
- Check_Node (Elmt);
+ when N_Allocator =>
+ Move_Expression (Expression (Expr));
- Merge_Envs (New_Env,
- Current_Perm_Env);
+ when N_Function_Call =>
+ Read_Params (Expr);
+ if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then
+ if Emit_Messages then
+ Error_Msg_N
+ ("call through access to subprogram is not allowed in "
+ & "SPARK", Expr);
+ end if;
+ else
+ Check_Globals (Get_Called_Entity (Expr));
+ end if;
- -- CLEANUP
+ when N_Op_Concat =>
+ Read_Expression (Left_Opnd (Expr));
+ Read_Expression (Right_Opnd (Expr));
- Copy_Env (New_Env,
- Current_Perm_Env);
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ Read_Indexes (Expression (Expr));
- Free_Env (New_Env);
- Free_Env (Saved_Env);
- end;
+ when N_Aggregate =>
+ declare
+ Assocs : constant List_Id := Component_Associations (Expr);
+ CL : List_Id;
+ Assoc : Node_Id := Nlists.First (Assocs);
+ Choice : Node_Id;
- when N_Indexed_Component =>
- Process_Path (Expr);
+ begin
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments. Handle the positional
+ -- components first.
- -- Analyze the expression that is getting qualified
+ Move_Expression_List (Expressions (Expr));
- when N_Qualified_Expression =>
- Check_Node (Expression (Expr));
+ -- Handle the named components next
- 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));
+ while Present (Assoc) loop
+ CL := Choices (Assoc);
- Check_Node (Condition (Expr));
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
- Free_Env (Saved_Env);
- end;
+ -- For an array aggregate, we should also check that the
+ -- expressions used in choices are readable.
- -- Analyze the list of associations in the aggregate
+ if Is_Array_Type (Etype (Expr)) then
+ Choice := Nlists.First (CL);
+ while Present (Choice) loop
+ if Nkind (Choice) /= N_Others_Choice then
+ Read_Expression (Choice);
+ end if;
+ Next (Choice);
+ end loop;
+ end if;
- when N_Aggregate =>
- Check_List (Expressions (Expr));
- Check_List (Component_Associations (Expr));
+ -- There can be only one element for a value of deep type
+ -- in order to avoid aliasing.
+
+ if not Box_Present (Assoc)
+ and then Is_Deep (Etype (Expression (Assoc)))
+ and then not Is_Singleton_Choice (CL)
+ and then Emit_Messages
+ then
+ Error_Msg_F
+ ("singleton choice required to prevent aliasing",
+ First (CL));
+ end if;
- when N_Allocator =>
- Check_Node (Expression (Expr));
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments.
- 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
+ if not Box_Present (Assoc) then
+ Move_Expression (Expression (Assoc));
+ end if;
- Merge_Envs (New_Env,
- Current_Perm_Env);
+ Next (Assoc);
+ end loop;
+ end;
- Next (Elmt);
- end loop;
+ when N_Extension_Aggregate =>
+ declare
+ Exprs : constant List_Id := Expressions (Expr);
+ Assocs : constant List_Id := Component_Associations (Expr);
+ CL : List_Id;
+ Assoc : Node_Id := Nlists.First (Assocs);
- -- CLEANUP
- Copy_Env (New_Env,
- Current_Perm_Env);
+ begin
+ Move_Expression (Ancestor_Part (Expr));
- Free_Env (New_Env);
- Free_Env (Saved_Env);
- end;
+ -- No positional components allowed at this stage
- -- Analyze the list of associates in the aggregate as well as the
- -- ancestor part.
+ if Present (Exprs) then
+ raise Program_Error;
+ end if;
- when N_Extension_Aggregate =>
+ while Present (Assoc) loop
+ CL := Choices (Assoc);
- Check_Node (Ancestor_Part (Expr));
- Check_List (Expressions (Expr));
+ -- Only singleton components allowed at this stage
- when N_Range =>
- Check_Node (Low_Bound (Expr));
- Check_Node (High_Bound (Expr));
+ if not Is_Singleton_Choice (CL) then
+ raise Program_Error;
+ end if;
- -- We arrived at a path. Process it.
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments.
- when N_Selected_Component =>
- Process_Path (Expr);
+ if not Box_Present (Assoc) then
+ Move_Expression (Expression (Assoc));
+ end if;
- when N_Slice =>
- Process_Path (Expr);
+ Next (Assoc);
+ end loop;
+ end;
- when N_Type_Conversion =>
- Check_Node (Expression (Expr));
+ when N_If_Expression =>
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ begin
+ Read_Expression (Cond);
+ Read_Indexes (Then_Part);
+ Read_Indexes (Else_Part);
+ end;
- when N_Unchecked_Type_Conversion =>
- Check_Node (Expression (Expr));
+ when N_Case_Expression =>
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
- -- Checking should not be called directly on these nodes
+ begin
+ Read_Expression (Expression (Expr));
- when N_Target_Name =>
- raise Program_Error;
+ while Present (Cur_Case) loop
+ Read_Indexes (Expression (Cur_Case));
+ Next (Cur_Case);
+ end loop;
+ end;
- -- Unsupported constructs in SPARK
+ when N_Attribute_Reference =>
+ pragma Assert
+ (Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Loop_Entry
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image);
+
+ Read_Expression (Prefix (Expr));
+
+ if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
+ or else (Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image
+ and then Is_Type_Name (Prefix (Expr)))
+ then
+ Read_Expression_List (Expressions (Expr));
+ end if;
- when N_Delta_Aggregate =>
- Error_Msg_N ("unsupported construct in SPARK", Expr);
+ when others =>
+ raise Program_Error;
+ end case;
+ end Read_Indexes;
- -- Ignored constructs for pointer checking
+ -- Start of processing for Check_Expression
- when N_Character_Literal
- | N_Null
- | N_Numeric_Or_String_Literal
- | N_Operator_Symbol
- | N_Raise_Expression
- | N_Raise_xxx_Error
- =>
- null;
+ begin
+ if Is_Type_Name (Expr) then
+ return;
- -- The following nodes are never generated in GNATprove mode
+ elsif Is_Path_Expression (Expr) then
+ if Mode /= Assign then
+ Read_Indexes (Expr);
+ end if;
- when N_Expression_With_Actions
- | N_Reference
- | N_Unchecked_Expression
- =>
- raise Program_Error;
+ if Mode /= Read_Subexpr then
+ Process_Path (Expr, Mode);
+ end if;
- end case;
- end Check_Expression;
+ return;
+ end if;
- -------------------
- -- Check_Globals --
- -------------------
+ -- Expressions that are not path expressions should only be analyzed in
+ -- Read mode.
- procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
- begin
- if Nkind (N) = N_Empty then
+ if Mode /= Read then
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+ end if;
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);
+ -- Special handling for nodes that may contain evaluated expressions in
+ -- the form of constraints.
- Row : Node_Id;
- The_Mode : Name_Id;
- RHS : Node_Id;
+ case Nkind (Expr) is
+ when N_Index_Or_Discriminant_Constraint =>
+ declare
+ Assn : Node_Id := First (Constraints (Expr));
+ begin
+ while Present (Assn) loop
+ case Nkind (Assn) is
+ when N_Discriminant_Association =>
+ Read_Expression (Expression (Assn));
- procedure Process (Mode : Name_Id;
- The_Global : Entity_Id);
+ when others =>
+ Read_Expression (Assn);
+ end case;
- procedure Process (Mode : Name_Id;
- The_Global : Node_Id)
- is
- Ident_Elt : constant Entity_Id :=
- Unique_Entity (Entity (The_Global));
+ Next (Assn);
+ end loop;
+ end;
+ return;
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ when N_Range_Constraint =>
+ Read_Expression (Range_Expression (Expr));
+ return;
- begin
- if Ekind (Ident_Elt) = E_Abstract_State then
- return;
+ when N_Subtype_Indication =>
+ if Present (Constraint (Expr)) then
+ Read_Expression (Constraint (Expr));
end if;
+ return;
- 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 N_Digits_Constraint =>
+ Read_Expression (Digits_Expression (Expr));
+ if Present (Range_Constraint (Expr)) then
+ Read_Expression (Range_Constraint (Expr));
+ end if;
+ return;
- when others =>
- raise Program_Error;
+ when N_Delta_Constraint =>
+ Read_Expression (Delta_Expression (Expr));
+ if Present (Range_Constraint (Expr)) then
+ Read_Expression (Range_Constraint (Expr));
+ end if;
+ return;
- end case;
+ when others =>
+ null;
+ end case;
- when Observe =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- if not Is_Borrowed_In (Ident_Elt) then
- -- Observed in
+ -- At this point Expr can only be a subexpression
- Current_Checking_Mode := Observe;
- Check_Node (The_Global);
- end if;
+ case N_Subexpr'(Nkind (Expr)) is
- when others =>
- null;
+ when N_Binary_Op
+ | N_Short_Circuit
+ =>
+ Read_Expression (Left_Opnd (Expr));
+ Read_Expression (Right_Opnd (Expr));
- end case;
+ when N_Membership_Test =>
+ Read_Expression (Left_Opnd (Expr));
+ if Present (Right_Opnd (Expr)) then
+ Read_Expression (Right_Opnd (Expr));
+ else
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
- when Borrow_Out =>
+ begin
+ while Present (Cur_Case) loop
+ Read_Expression (Cur_Case);
+ Next (Cur_Case);
+ end loop;
+ end;
+ end if;
- case Mode is
- when Name_Output =>
- -- Borrowed out
- Current_Checking_Mode := Borrow_Out;
- Check_Node (The_Global);
+ when N_Unary_Op =>
+ Read_Expression (Right_Opnd (Expr));
- when others =>
- null;
+ when N_Attribute_Reference =>
+ declare
+ Aname : constant Name_Id := Attribute_Name (Expr);
+ Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
+ Pref : constant Node_Id := Prefix (Expr);
+ Args : constant List_Id := Expressions (Expr);
- end case;
+ begin
+ case Attr_Id is
+
+ -- The following attributes take either no arguments, or
+ -- arguments that do not refer to evaluated expressions
+ -- (like Length or Loop_Entry), hence only the prefix
+ -- needs to be read.
+
+ when Attribute_Address
+ | Attribute_Alignment
+ | Attribute_Callable
+ | Attribute_Component_Size
+ | Attribute_Constrained
+ | Attribute_First
+ | Attribute_First_Bit
+ | Attribute_Last
+ | Attribute_Last_Bit
+ | Attribute_Length
+ | Attribute_Loop_Entry
+ | Attribute_Object_Size
+ | Attribute_Position
+ | Attribute_Size
+ | Attribute_Terminated
+ | Attribute_Valid
+ | Attribute_Value_Size
+ =>
+ Read_Expression (Pref);
+
+ -- The following attributes take a type name as prefix,
+ -- hence only the arguments need to be read.
+
+ when Attribute_Ceiling
+ | Attribute_Floor
+ | Attribute_Max
+ | Attribute_Min
+ | Attribute_Mod
+ | Attribute_Pos
+ | Attribute_Pred
+ | Attribute_Remainder
+ | Attribute_Rounding
+ | Attribute_Succ
+ | Attribute_Truncation
+ | Attribute_Val
+ | Attribute_Value
+ =>
+ Read_Expression_List (Args);
- when Move =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- if Is_Borrowed_In (Ident_Elt) then
- -- Borrowed in
+ -- Attributes Image and Img either take a type name as
+ -- prefix with an expression in argument, or the expression
+ -- directly as prefix. Adapt to each case.
- Current_Checking_Mode := Move;
- else
- -- Observed
+ when Attribute_Image
+ | Attribute_Img
+ =>
+ if No (Args) then
+ Read_Expression (Pref);
+ else
+ Read_Expression_List (Args);
+ end if;
- return;
- end if;
+ -- Attribute Update takes expressions as both prefix and
+ -- arguments, so both need to be read.
- when Name_Output =>
- return;
+ when Attribute_Update =>
+ Read_Expression (Pref);
+ Read_Expression_List (Args);
- when Name_In_Out =>
- -- Borrowed in out
+ -- Attribute Modulus does not reference the evaluated
+ -- expression, so it can be ignored for this analysis.
- Current_Checking_Mode := Move;
+ when Attribute_Modulus =>
+ null;
- when others =>
- raise Program_Error;
- end case;
+ -- The following attributes apply to types; there are no
+ -- expressions to read.
- Check_Node (The_Global);
- when Assign =>
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- null;
+ when Attribute_Class
+ | Attribute_Storage_Size
+ =>
+ null;
- when Name_Output
- | Name_In_Out
- =>
- -- Borrowed out or in out
+ -- Postconditions should not be analyzed
- Process_Path (The_Global);
+ when Attribute_Old
+ | Attribute_Result
+ =>
+ raise Program_Error;
- when others =>
- raise Program_Error;
- end case;
+ when others =>
+ null;
+ end case;
+ end;
- when others =>
- raise Program_Error;
- end case;
+ when N_Range =>
+ Read_Expression (Low_Bound (Expr));
+ Read_Expression (High_Bound (Expr));
- Current_Checking_Mode := Mode_Before;
- end Process;
+ when N_If_Expression =>
+ Read_Expression_List (Expressions (Expr));
- begin
- if Nkind (Expression (PAA)) = N_Null then
- -- global => null
- -- No globals, nothing to do
- return;
+ when N_Case_Expression =>
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
- elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
- -- global => foo
- -- A single input
- Process (Name_Input, Expression (PAA));
+ begin
+ while Present (Cur_Case) loop
+ Read_Expression (Expression (Cur_Case));
+ Next (Cur_Case);
+ end loop;
- 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);
+ Read_Expression (Expression (Expr));
+ end;
- when N_Numeric_Or_String_Literal =>
- Process (Name_Input, Original_Node (RHS));
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ Read_Expression (Expression (Expr));
- when others =>
- raise Program_Error;
+ when N_Quantified_Expression =>
+ declare
+ For_In_Spec : constant Node_Id :=
+ Loop_Parameter_Specification (Expr);
+ For_Of_Spec : constant Node_Id :=
+ Iterator_Specification (Expr);
+ For_Of_Spec_Typ : Node_Id;
- end case;
- RHS := Next (RHS);
- end loop;
+ begin
+ if Present (For_In_Spec) then
+ Read_Expression (Discrete_Subtype_Definition (For_In_Spec));
+ else
+ Read_Expression (Name (For_Of_Spec));
+ For_Of_Spec_Typ := Subtype_Indication (For_Of_Spec);
+ if Present (For_Of_Spec_Typ) then
+ Read_Expression (For_Of_Spec_Typ);
+ end if;
+ end if;
- 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
+ Read_Expression (Condition (Expr));
+ end;
- 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_Character_Literal
+ | N_Numeric_Or_String_Literal
+ | N_Operator_Symbol
+ | N_Raise_Expression
+ | N_Raise_xxx_Error
+ =>
+ null;
- when N_Identifier
- | N_Expanded_Name
- =>
- Process (The_Mode, RHS);
+ when N_Delta_Aggregate
+ | N_Target_Name
+ =>
+ null;
- when N_Null =>
- null;
+ -- Procedure calls are handled in Check_Node
- when N_Numeric_Or_String_Literal =>
- Process (The_Mode, Original_Node (RHS));
+ when N_Procedure_Call_Statement =>
+ raise Program_Error;
- when others =>
- raise Program_Error;
+ -- Path expressions are handled before this point
- end case;
+ when N_Aggregate
+ | N_Allocator
+ | N_Expanded_Name
+ | N_Explicit_Dereference
+ | N_Extension_Aggregate
+ | N_Function_Call
+ | N_Identifier
+ | N_Indexed_Component
+ | N_Null
+ | N_Selected_Component
+ | N_Slice
+ =>
+ raise Program_Error;
- Row := Next (Row);
- end loop;
- end;
+ -- The following nodes are never generated in GNATprove mode
- else
+ when N_Expression_With_Actions
+ | N_Reference
+ | N_Unchecked_Expression
+ =>
raise Program_Error;
- end if;
- end;
- end Check_Globals;
+ end case;
+ end Check_Expression;
----------------
-- Check_List --
-- Check_Loop_Statement --
--------------------------
- procedure Check_Loop_Statement (Loop_N : Node_Id) is
+ procedure Check_Loop_Statement (Stmt : Node_Id) is
-- Local Subprograms
(E : Entity_Id;
Loop_Id : Node_Id;
Perm : Perm_Kind;
- Found_Perm : Perm_Kind);
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id);
-- 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
+ -- permission that was expected, and the permission found, and issues
-- an appropriate error message.
-----------------------------------
Orig_Tree : Perm_Tree_Access;
E : Entity_Id)
is
- -----------------------
- -- Local Subprograms --
- -----------------------
+ -- Local subprograms
procedure Check_Is_Less_Restrictive_Tree_Than
(Tree : Perm_Tree_Access;
begin
if not (Permission (Tree) >= Perm) then
Perm_Error_Loop_Exit
- (E, Loop_N, Permission (Tree), Perm);
+ (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
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);
+ (E, Stmt, Children_Permission (Tree), Perm,
+ Explanation (Tree));
end if;
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;
begin
if not (Perm >= Permission (Tree)) then
Perm_Error_Loop_Exit
- (E, Loop_N, Permission (Tree), Perm);
+ (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
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);
+ (E, Stmt, Children_Permission (Tree), Perm,
+ Explanation (Tree));
end if;
when Reference =>
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;
if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
Perm_Error_Loop_Exit
(E => E,
- Loop_Id => Loop_N,
+ Loop_Id => Stmt,
Perm => Permission (New_Tree),
- Found_Perm => Permission (Orig_Tree));
+ Found_Perm => Permission (Orig_Tree),
+ Expl => Explanation (New_Tree));
end if;
case Kind (New_Tree) is
Children_Permission (Orig_Tree))
then
Perm_Error_Loop_Exit
- (E, Loop_N,
+ (E, Stmt,
Children_Permission (New_Tree),
- Children_Permission (Orig_Tree));
+ Children_Permission (Orig_Tree),
+ Explanation (New_Tree));
end if;
when Reference =>
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;
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.Get_First_Key
(Component (Orig_Tree));
while KeyO.Present loop
+ CompN := Perm_Tree_Maps.Get
+ (Component (New_Tree), KeyO.K);
+ CompO := Perm_Tree_Maps.Get
+ (Component (Orig_Tree), KeyO.K);
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 =>
(E : Entity_Id;
Loop_Id : Node_Id;
Perm : Perm_Kind;
- Found_Perm : Perm_Kind)
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id)
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);
+ if Emit_Messages then
+ 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,
+ Expl => Expl);
+ end if;
end Perm_Error_Loop_Exit;
-- Local variables
- Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
+ Loop_Name : constant Entity_Id := Entity (Identifier (Stmt));
Loop_Env : constant Perm_Env_Access := new Perm_Env;
+ Scheme : constant Node_Id := Iteration_Scheme (Stmt);
+
+ -- Start of processing for Check_Loop_Statement
begin
-- Save environment prior to the loop
-- Otherwise, the loop exit environment remains empty until it is
-- populated by analyzing exit statements.
- if Present (Iteration_Scheme (Loop_N)) then
+ if Present (Iteration_Scheme (Stmt)) then
declare
- Exit_Env : constant Perm_Env_Access := new Perm_Env;
+ 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);
-- Analyze loop
- Check_Node (Iteration_Scheme (Loop_N));
- Check_List (Statements (Loop_N));
+ if Present (Scheme) then
+
+ -- Case of a WHILE loop
+
+ if Present (Condition (Scheme)) then
+ Check_Expression (Condition (Scheme), Read);
+
+ -- Case of a FOR loop
+
+ else
+ declare
+ Param_Spec : constant Node_Id :=
+ Loop_Parameter_Specification (Scheme);
+ Iter_Spec : constant Node_Id := Iterator_Specification (Scheme);
+ begin
+ if Present (Param_Spec) then
+ Check_Expression
+ (Discrete_Subtype_Definition (Param_Spec), Read);
+ else
+ Check_Expression (Name (Iter_Spec), Read);
+ if Present (Subtype_Indication (Iter_Spec)) then
+ Check_Expression (Subtype_Indication (Iter_Spec), Read);
+ end if;
+ end if;
+ end;
+ end if;
+ end if;
+
+ Check_List (Statements (Stmt));
-- Check that environment gets less restrictive at end of loop
if Exit_Env /= null then
Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
+ Free_Env (Loop_Env.all);
+ Free_Env (Exit_Env.all);
else
Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
+ Free_Env (Loop_Env.all);
end if;
-
- Free_Env (Loop_Env.all);
- Free_Env (Exit_Env.all);
end;
end Check_Loop_Statement;
----------------
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));
+ procedure Check_Subprogram_Contract (N : Node_Id);
+ -- Check the postcondition-like contracts for use of 'Old
- when N_Body_Stub =>
- Check_Node (Get_Body_From_Stub (N));
+ -------------------------------
+ -- Check_Subprogram_Contract --
+ -------------------------------
- when N_Statement_Other_Than_Procedure_Call =>
+ procedure Check_Subprogram_Contract (N : Node_Id) is
+ begin
+ if Nkind (N) = N_Subprogram_Declaration
+ or else Acts_As_Spec (N)
+ then
+ declare
+ E : constant Entity_Id := Unique_Defining_Entity (N);
+ Post : constant Node_Id :=
+ Get_Pragma (E, Pragma_Postcondition);
+ Cases : constant Node_Id :=
+ Get_Pragma (E, Pragma_Contract_Cases);
+ begin
+ Check_Old_Loop_Entry (Post);
+ Check_Old_Loop_Entry (Cases);
+ end;
+
+ elsif Nkind (N) = N_Subprogram_Body then
+ declare
+ E : constant Entity_Id := Defining_Entity (N);
+ Ref_Post : constant Node_Id :=
+ Get_Pragma (E, Pragma_Refined_Post);
+ begin
+ Check_Old_Loop_Entry (Ref_Post);
+ end;
+ end if;
+ end Check_Subprogram_Contract;
+
+ -- Start of processing for Check_Node
+
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration (N);
+
+ when N_Body_Stub =>
+ Check_Node (Get_Body_From_Stub (N));
+
+ when N_Statement_Other_Than_Procedure_Call =>
Check_Statement (N);
+ when N_Procedure_Call_Statement =>
+ Check_Call_Statement (N);
+
when N_Package_Body =>
- Check_Package_Body (N);
+ if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
+ Check_Package_Body (N);
+ end if;
- when N_Subprogram_Body
- | N_Entry_Body
+ when N_Subprogram_Body =>
+ if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
+ Check_Subprogram_Contract (N);
+ Check_Callable_Body (N);
+ end if;
+
+ when N_Entry_Body
| N_Task_Body
=>
Check_Callable_Body (N);
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));
+ Check_Package_Spec (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_Pragma =>
+ Check_Pragma (N);
- 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;
+ when N_Subprogram_Declaration =>
+ Check_Subprogram_Contract (N);
- -- Unsupported constructs in SPARK
+ -- Attribute references in statement position are not supported in
+ -- SPARK and will be rejected by GNATprove.
- when N_Iterated_Component_Association =>
- Error_Msg_N ("unsupported construct in SPARK", N);
+ when N_Attribute_Reference =>
+ null;
-- Ignored constructs for pointer checking
| N_Others_Choice
| N_Package_Instantiation
| N_Package_Renaming_Declaration
- | N_Pragma
| N_Procedure_Instantiation
+ | N_Raise_xxx_Error
| N_Record_Representation_Clause
- | N_Subprogram_Declaration
| N_Subprogram_Renaming_Declaration
| N_Task_Type_Declaration
| N_Use_Package_Clause
| N_Use_Type_Clause
| N_Validate_Unchecked_Conversion
| N_Variable_Reference_Marker
+ | N_Discriminant_Association
+
+ -- ??? check whether we should do something special for
+ -- N_Discriminant_Association, or maybe raise Program_Error.
=>
null;
- -- The following nodes are rewritten by semantic analysis
+ -- Checking should not be called directly on these nodes
- when N_Single_Protected_Declaration
- | N_Single_Task_Declaration
- =>
+ when others =>
raise Program_Error;
end case;
-
- Current_Checking_Mode := Mode_Before;
end Check_Node;
+ --------------------------
+ -- Check_Old_Loop_Entry --
+ --------------------------
+
+ procedure Check_Old_Loop_Entry (N : Node_Id) is
+
+ function Check_Attribute (N : Node_Id) return Traverse_Result;
+
+ ---------------------
+ -- Check_Attribute --
+ ---------------------
+
+ function Check_Attribute (N : Node_Id) return Traverse_Result is
+ Attr_Id : Attribute_Id;
+ Aname : Name_Id;
+ Pref : Node_Id;
+
+ begin
+ if Nkind (N) = N_Attribute_Reference then
+ Attr_Id := Get_Attribute_Id (Attribute_Name (N));
+ Aname := Attribute_Name (N);
+
+ if Attr_Id = Attribute_Old
+ or else Attr_Id = Attribute_Loop_Entry
+ then
+ Pref := Prefix (N);
+
+ if Is_Deep (Etype (Pref)) then
+ if Nkind (Pref) /= N_Function_Call then
+ if Emit_Messages then
+ Error_Msg_Name_1 := Aname;
+ Error_Msg_N
+ ("prefix of % attribute must be a function call "
+ & "(SPARK RM 3.10(14))", Pref);
+ end if;
+
+ elsif Is_Traversal_Function_Call (Pref) then
+ if Emit_Messages then
+ Error_Msg_Name_1 := Aname;
+ Error_Msg_N
+ ("prefix of % attribute should not call a traversal "
+ & "function (SPARK RM 3.10(14))", Pref);
+ end if;
+ end if;
+ end if;
+ end if;
+ end if;
+
+ return OK;
+ end Check_Attribute;
+
+ procedure Check_All is new Traverse_Proc (Check_Attribute);
+
+ -- Start of processing for Check_Old_Loop_Entry
+
+ begin
+ Check_All (N);
+ end Check_Old_Loop_Entry;
+
------------------------
-- Check_Package_Body --
------------------------
procedure Check_Package_Body (Pack : Node_Id) is
- Saved_Env : Perm_Env;
- CorSp : Node_Id;
+ Save_In_Elab : constant Boolean := Inside_Elaboration;
+ Spec : constant Node_Id :=
+ Package_Specification (Corresponding_Spec (Pack));
+ Id : constant Entity_Id := Defining_Entity (Pack);
+ Prag : constant Node_Id := SPARK_Pragma (Id);
+ Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
+ Saved_Env : Perm_Env;
begin
- if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
- if Get_SPARK_Mode_From_Annotation
- (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
+ then
+ Inside_Elaboration := True;
+
+ -- Save environment and put a new one in place
+
+ Move_Env (Current_Perm_Env, Saved_Env);
+
+ -- Reanalyze package spec to have its variables in the environment
+
+ Check_List (Visible_Declarations (Spec));
+ Check_List (Private_Declarations (Spec));
+
+ -- Check declarations and statements in the special mode for
+ -- elaboration.
+
+ Check_List (Declarations (Pack));
+
+ if Present (Aux_Prag)
+ and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
then
- return;
+ Check_Node (Handled_Statement_Sequence (Pack));
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));
+ -- Restore the saved environment and free the current one
- -- Save environment
+ Move_Env (Saved_Env, Current_Perm_Env);
- Copy_Env (Current_Perm_Env,
- Saved_Env);
+ Inside_Elaboration := Save_In_Elab;
+ end if;
+ end Check_Package_Body;
- Check_List (Private_Declarations (CorSp));
+ ------------------------
+ -- Check_Package_Spec --
+ ------------------------
- -- Set mode to Read, and then analyze declarations and statements
+ procedure Check_Package_Spec (Pack : Node_Id) is
+ Save_In_Elab : constant Boolean := Inside_Elaboration;
+ Spec : constant Node_Id := Specification (Pack);
+ Id : constant Entity_Id := Defining_Entity (Pack);
+ Prag : constant Node_Id := SPARK_Pragma (Id);
+ Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
+ Saved_Env : Perm_Env;
- Current_Checking_Mode := Read;
+ begin
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
+ then
+ Inside_Elaboration := True;
- Check_List (Declarations (Pack));
- Check_Node (Handled_Statement_Sequence (Pack));
+ -- Save environment and put a new one in place
- -- Check RW for every stateful variable (i.e. in declarations)
+ Move_Env (Current_Perm_Env, Saved_Env);
- Return_Declarations (Private_Declarations (CorSp));
- Return_Declarations (Visible_Declarations (CorSp));
- Return_Declarations (Declarations (Pack));
+ -- Check declarations in the special mode for elaboration
- -- Restore previous environment (i.e. delete every nonvisible
- -- declaration) from environment.
+ Check_List (Visible_Declarations (Spec));
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env,
- Current_Perm_Env);
- end Check_Package_Body;
+ if Present (Aux_Prag)
+ and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
+ then
+ Check_List (Private_Declarations (Spec));
+ end if;
- -----------------
- -- Check_Param --
- -----------------
+ -- Restore the saved environment and free the current one. As part of
+ -- the restoration, the environment of the package spec is merged in
+ -- the enclosing environment, which may be an enclosing
+ -- package/subprogram spec or body which has access to the variables
+ -- of the package spec.
- procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ Merge_Env (Saved_Env, Current_Perm_Env);
- 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
+ Inside_Elaboration := Save_In_Elab;
+ end if;
+ end Check_Package_Spec;
- Current_Checking_Mode := Move;
- else
- -- Observed
+ -------------------------------
+ -- Check_Parameter_Or_Global --
+ -------------------------------
- return;
- end if;
+ procedure Check_Parameter_Or_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean)
+ is
+ Mode : Checking_Mode;
+ Status : Error_Status;
- when E_Out_Parameter =>
- return;
+ begin
+ if not Global_Var
+ and then Is_Anonymous_Access_Type (Typ)
+ then
+ Check_Source_Of_Borrow_Or_Observe (Expr, Status);
- when E_In_Out_Parameter =>
- -- Borrowed in out
+ if Status /= OK then
+ return;
+ end if;
+ end if;
- Current_Checking_Mode := Move;
+ case Kind is
+ when E_In_Parameter =>
- end case;
+ -- Inputs of functions have R permission only
- Check_Node (Actual);
+ if Ekind (Subp) = E_Function then
+ Mode := Read;
- when Assign =>
- case Formal_Kind'(Mode) is
- when E_In_Parameter =>
- null;
+ -- Input global variables have R permission only
- when E_Out_Parameter
- | E_In_Out_Parameter
- =>
- -- Borrowed out or in out
+ elsif Global_Var then
+ Mode := Read;
- Process_Path (Actual);
+ -- Anonymous access to constant is an observe
- end case;
+ elsif Is_Anonymous_Access_Type (Typ)
+ and then Is_Access_Constant (Typ)
+ then
+ Mode := Observe;
- when others =>
- raise Program_Error;
+ -- Other access types are a borrow
- end case;
- Current_Checking_Mode := Mode_Before;
- end Check_Param;
+ elsif Is_Access_Type (Typ) then
+ Mode := Borrow;
- --------------------------
- -- Check_Param_Observes --
- --------------------------
+ -- Deep types other than access types define an observe
- procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ elsif Is_Deep (Typ) then
+ Mode := Observe;
- begin
- case Mode is
- when E_In_Parameter =>
- if not Is_Borrowed_In (Formal) then
- -- Observed in
+ -- Otherwise the variable is read
- Current_Checking_Mode := Observe;
- Check_Node (Actual);
+ else
+ Mode := Read;
end if;
- when others =>
- null;
+ when E_Out_Parameter =>
+ Mode := Assign;
+ when E_In_Out_Parameter =>
+ Mode := Move;
end case;
- Current_Checking_Mode := Mode_Before;
- end Check_Param_Observes;
+ if Mode = Assign then
+ Check_Expression (Expr, Read_Subexpr);
+ end if;
- ----------------------
- -- Check_Param_Outs --
- ----------------------
+ Check_Expression (Expr, Mode);
+ end Check_Parameter_Or_Global;
- 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;
+ procedure Check_Globals_Inst is
+ new Handle_Globals (Check_Parameter_Or_Global);
- begin
+ procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst;
- case Mode is
- when E_Out_Parameter =>
- -- Borrowed out
- Current_Checking_Mode := Borrow_Out;
- Check_Node (Actual);
+ ------------------
+ -- Check_Pragma --
+ ------------------
- when others =>
- null;
+ procedure Check_Pragma (Prag : Node_Id) is
+ Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag);
+ Arg1 : constant Node_Id :=
+ First (Pragma_Argument_Associations (Prag));
+ Arg2 : Node_Id := Empty;
- end case;
+ begin
+ if Present (Arg1) then
+ Arg2 := Next (Arg1);
+ end if;
- Current_Checking_Mode := Mode_Before;
- end Check_Param_Outs;
+ case Prag_Id is
+ when Pragma_Check =>
+ declare
+ Expr : constant Node_Id := Expression (Arg2);
+ begin
+ Check_Expression (Expr, Read);
- ----------------------
- -- Check_Param_Read --
- ----------------------
+ -- Prefix of Loop_Entry should be checked inside any assertion
+ -- where it may appear.
- procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
+ Check_Old_Loop_Entry (Expr);
+ end;
- begin
- pragma Assert (Current_Checking_Mode = Read);
+ -- Prefix of Loop_Entry should be checked inside a Loop_Variant
- case Formal_Kind'(Mode) is
- when E_In_Parameter =>
- Check_Node (Actual);
+ when Pragma_Loop_Variant =>
+ Check_Old_Loop_Entry (Prag);
- when E_Out_Parameter
- | E_In_Out_Parameter
+ -- There is no need to check contracts, as these can only access
+ -- inputs and outputs of the subprogram. Inputs are checked
+ -- independently for R permission. Outputs are checked
+ -- independently to have RW permission on exit.
+
+ -- Postconditions are checked for correct use of 'Old, but starting
+ -- from the corresponding declaration, in order to avoid dealing with
+ -- with contracts on generic subprograms, which are not handled in
+ -- GNATprove.
+
+ when Pragma_Precondition
+ | Pragma_Postcondition
+ | Pragma_Contract_Cases
+ | Pragma_Refined_Post
=>
null;
+ -- The same holds for the initial condition after package
+ -- elaboration, for the different reason that library-level
+ -- variables can only be left in RW state after elaboration.
+
+ when Pragma_Initial_Condition =>
+ null;
+
+ -- These pragmas should have been rewritten and/or removed in
+ -- GNATprove mode.
+
+ when Pragma_Assert
+ | Pragma_Assert_And_Cut
+ | Pragma_Assume
+ | Pragma_Compile_Time_Error
+ | Pragma_Compile_Time_Warning
+ | Pragma_Debug
+ | Pragma_Loop_Invariant
+ =>
+ raise Program_Error;
+
+ when others =>
+ null;
end case;
- end Check_Param_Read;
+ end Check_Pragma;
-------------------------
-- Check_Safe_Pointers --
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
when N_Package_Body
| N_Package_Declaration
+ | N_Subprogram_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;
+ declare
+ E : constant Entity_Id := Defining_Entity (N);
+ Prag : constant Node_Id := SPARK_Pragma (E);
+ -- SPARK_Mode pragma in application
+
+ begin
+ if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
+ null;
- elsif Nkind (N) = N_Package_Body then
- Check_List (Declarations (N));
+ elsif Present (Prag) then
+ if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
+ Check_Node (N);
+ end if;
- elsif Nkind (N) = N_Package_Declaration then
- Check_List (Private_Declarations (Specification (N)));
- Check_List (Visible_Declarations (Specification (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;
+ end;
when others =>
null;
end case;
end Check_Safe_Pointers;
+ ---------------------------------------
+ -- Check_Source_Of_Borrow_Or_Observe --
+ ---------------------------------------
+
+ procedure Check_Source_Of_Borrow_Or_Observe
+ (Expr : Node_Id;
+ Status : out Error_Status)
+ is
+ Root : Entity_Id;
+
+ begin
+ if Is_Path_Expression (Expr) then
+ Root := Get_Root_Object (Expr);
+ else
+ Root := Empty;
+ end if;
+
+ Status := OK;
+
+ -- SPARK RM 3.10(3): If the target of an assignment operation is an
+ -- object of an anonymous access-to-object type (including copy-in for
+ -- a parameter), then the source shall be a name denoting a part of a
+ -- stand-alone object, a part of a parameter, or a call to a traversal
+ -- function.
+
+ if No (Root) then
+ if Emit_Messages then
+ if Nkind (Expr) = N_Function_Call then
+ Error_Msg_N
+ ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
+ Error_Msg_N
+ ("\function called must be a traversal function", Expr);
+ else
+ Error_Msg_N
+ ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
+ Error_Msg_N
+ ("\expression must be part of stand-alone object or " &
+ "parameter",
+ Expr);
+ end if;
+ end if;
+
+ Status := Error;
+ end if;
+ end Check_Source_Of_Borrow_Or_Observe;
+
---------------------
-- 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
+
+ -- An entry call is handled like other calls
+
when N_Entry_Call_Statement =>
Check_Call_Statement (Stmt);
- -- Move right-hand side first, and then assign left-hand side
+ -- An assignment may correspond to a move, a borrow, or an observe
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;
+ Target : constant Node_Id := Name (Stmt);
begin
- -- Save environment
+ -- Start with checking that the subexpressions of the target
+ -- path are readable, before possibly updating the permission
+ -- of these subexpressions in Check_Assignment.
- Copy_Env (Current_Perm_Env,
- Saved_Env);
+ Check_Expression (Target, Read_Subexpr);
- -- Analyze declarations and Handled_Statement_Sequences
+ Check_Assignment (Target => Target,
+ Expr => Expression (Stmt));
- Current_Checking_Mode := Read;
- Check_List (Declarations (Stmt));
- Check_Node (Handled_Statement_Sequence (Stmt));
+ -- ??? We need a rule that forbids targets of assignment for
+ -- which the path is not known, for example when there is a
+ -- function call involved (which includes calls to traversal
+ -- functions). Otherwise there is no way to update the
+ -- corresponding path permission.
- -- Restore environment
+ if No (Get_Root_Object
+ (Target, Through_Traversal => False))
+ then
+ if Emit_Messages then
+ Error_Msg_N ("illegal target for assignment", Target);
+ end if;
+ return;
+ end if;
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ Check_Expression (Target, Assign);
end;
- when N_Case_Statement =>
- declare
- Saved_Env : Perm_Env;
+ when N_Block_Statement =>
+ Check_List (Declarations (Stmt));
+ Check_Node (Handled_Statement_Sequence (Stmt));
- -- Accumulator for the different branches
+ -- Remove local borrowers and observers
+
+ declare
+ Decl : Node_Id := First (Declarations (Stmt));
+ Var : Entity_Id;
+ begin
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Object_Declaration then
+ Var := Defining_Identifier (Decl);
+ Remove (Current_Borrowers, Var);
+ Remove (Current_Observers, Var);
+ end if;
- New_Env : Perm_Env;
+ Next (Decl);
+ end loop;
+ end;
- Elmt : Node_Id := First (Alternatives (Stmt));
+ when N_Case_Statement =>
+ declare
+ Alt : Node_Id;
+ Saved_Env : Perm_Env;
+ -- Copy of environment for analysis of the different cases
+ New_Env : Perm_Env;
+ -- Accumulator for the different cases
begin
- Current_Checking_Mode := Read;
- Check_Node (Expression (Stmt));
- Current_Checking_Mode := Mode_Before;
+ Check_Expression (Expression (Stmt), Read);
-- 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.
+ Copy_Env (Current_Perm_Env, Saved_Env);
-- First alternative
- Check_Node (Elmt);
- Next (Elmt);
+ Alt := First (Alternatives (Stmt));
+ Check_List (Statements (Alt));
+ Next (Alt);
- Copy_Env (Current_Perm_Env,
- New_Env);
- Free_Env (Current_Perm_Env);
+ -- Cleanup
+
+ Move_Env (Current_Perm_Env, New_Env);
-- Other alternatives
- while Present (Elmt) loop
+ while Present (Alt) loop
+
-- Restore environment
- Copy_Env (Saved_Env,
- Current_Perm_Env);
+ Copy_Env (Saved_Env, Current_Perm_Env);
- Check_Node (Elmt);
+ -- Next alternative
- -- Merge Current_Perm_Env into New_Env
+ Check_List (Statements (Alt));
+ Next (Alt);
- Merge_Envs (New_Env,
- Current_Perm_Env);
+ -- Merge Current_Perm_Env into New_Env
- Next (Elmt);
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
end loop;
- -- CLEANUP
- Copy_Env (New_Env,
- Current_Perm_Env);
-
- Free_Env (New_Env);
+ Move_Env (New_Env, Current_Perm_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_Delay_Relative_Statement
+ | N_Delay_Until_Statement
+ =>
+ Check_Expression (Expression (Stmt), Read);
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
+ Subp : constant Entity_Id :=
+ Return_Applies_To (Return_Statement_Entity (Stmt));
+ Expr : constant Node_Id := Expression (Stmt);
+ begin
+ if Present (Expression (Stmt)) then
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;
+ Return_Typ : constant Entity_Id :=
+ Etype (Expression (Stmt));
- 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;
+ begin
+ -- SPARK RM 3.10(5): A return statement that applies
+ -- to a traversal function that has an anonymous
+ -- access-to-constant (respectively, access-to-variable)
+ -- result type, shall return either the literal null
+ -- or an access object denoted by a direct or indirect
+ -- observer (respectively, borrower) of the traversed
+ -- parameter.
+
+ if Is_Anonymous_Access_Type (Return_Typ) then
+ pragma Assert (Is_Traversal_Function (Subp));
+
+ if Nkind (Expr) /= N_Null then
+ declare
+ Expr_Root : constant Entity_Id :=
+ Get_Root_Object (Expr, Is_Traversal => True);
+ Param : constant Entity_Id :=
+ First_Formal (Subp);
+ begin
+ if Param /= Expr_Root and then Emit_Messages then
+ Error_Msg_NE
+ ("returned value must be rooted in "
+ & "traversed parameter & "
+ & "(SPARK RM 3.10(5))",
+ Stmt, Param);
+ end if;
+ end;
+ end if;
- Check_Node (Expression (Stmt));
- end case;
+ -- Move expression to caller
- when N_Extended_Return_Statement =>
- Check_List (Return_Object_Declarations (Stmt));
- Check_Node (Handled_Statement_Sequence (Stmt));
+ elsif Is_Deep (Return_Typ) then
- Return_Declarations (Return_Object_Declarations (Stmt));
+ if Is_Path_Expression (Expr) then
+ Check_Expression (Expr, Move);
- 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 :=
+ else
+ if Emit_Messages then
+ Error_Msg_N
+ ("expression not allowed as source of move",
+ Expr);
+ end if;
+ return;
+ end if;
+
+ else
+ Check_Expression (Expr, Read);
+ end if;
+
+ if Ekind_In (Subp, E_Procedure, E_Entry)
+ and then not No_Return (Subp)
+ then
+ Return_Parameters (Subp);
+ Return_Globals (Subp);
+ end if;
+ end;
+ end if;
+ end;
+
+ when N_Extended_Return_Statement =>
+ declare
+ Subp : constant Entity_Id :=
Return_Applies_To (Return_Statement_Entity (Stmt));
+ Decls : constant List_Id := Return_Object_Declarations (Stmt);
+ Decl : constant Node_Id := Last_Non_Pragma (Decls);
+ Obj : constant Entity_Id := Defining_Identifier (Decl);
+ Perm : Perm_Kind;
+
begin
- Return_Parameters (Subp);
- Return_Globals (Subp);
+ -- SPARK RM 3.10(5): return statement of traversal function
+
+ if Is_Traversal_Function (Subp) and then Emit_Messages then
+ Error_Msg_N
+ ("extended return cannot apply to a traversal function",
+ Stmt);
+ end if;
+
+ Check_List (Return_Object_Declarations (Stmt));
+ Check_Node (Handled_Statement_Sequence (Stmt));
+
+ if Is_Deep (Etype (Obj)) then
+ Perm := Get_Perm (Obj);
+
+ if Perm /= Read_Write then
+ Perm_Error (Decl, Read_Write, Perm,
+ Expl => Get_Expl (Obj));
+ end if;
+ end if;
+
+ if Ekind_In (Subp, E_Procedure, E_Entry)
+ and then not No_Return (Subp)
+ then
+ Return_Parameters (Subp);
+ Return_Globals (Subp);
+ end if;
end;
- -- Merge the current_Perm_Env with the accumulator for the given loop
+ -- On loop exit, merge the current permission environment with the
+ -- accumulator for the given loop.
when N_Exit_Statement =>
declare
- Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
-
+ 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 :=
+ Environment_Copy : constant Perm_Env_Access :=
new Perm_Env;
begin
-
- Copy_Env (Current_Perm_Env,
- Environment_Copy.all);
+ 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);
+ Merge_Env (Source => Environment_Copy.all,
+ Target => Saved_Accumulator.all);
+ -- ??? Either free Environment_Copy, or change the type
+ -- of loop accumulators to directly store permission
+ -- environments.
end if;
end;
- -- Copy environment, run on each branch, and then merge
+ -- On branches, analyze each branch independently on a fresh copy of
+ -- the permission environment, then merge the resulting permission
+ -- environments.
when N_If_Statement =>
declare
Saved_Env : Perm_Env;
-
+ New_Env : Perm_Env;
-- Accumulator for the different branches
- New_Env : Perm_Env;
-
begin
-
- Check_Node (Condition (Stmt));
+ Check_Expression (Condition (Stmt), Read);
-- Save environment
- Copy_Env (Current_Perm_Env,
- Saved_Env);
-
- -- Here we have the original env in saved, current with a fresh
- -- copy.
+ Copy_Env (Current_Perm_Env, Saved_Env);
- -- THEN PART
+ -- THEN branch
Check_List (Then_Statements (Stmt));
+ Move_Env (Current_Perm_Env, New_Env);
- Copy_Env (Current_Perm_Env,
- New_Env);
+ -- ELSIF branches
- Free_Env (Current_Perm_Env);
-
- -- Here the new_environment contains curr env after then block
-
- -- ELSIF part
declare
- Elmt : Node_Id;
-
+ Branch : 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);
+ Branch := First (Elsif_Parts (Stmt));
+ while Present (Branch) loop
- Check_Node (Condition (Elmt));
- Check_List (Then_Statements (Stmt));
+ -- Restore current permission environment
- -- Merge Current_Perm_Env into New_Env
+ Copy_Env (Saved_Env, Current_Perm_Env);
+ Check_Expression (Condition (Branch), Read);
+ Check_List (Then_Statements (Branch));
- Merge_Envs (New_Env,
- Current_Perm_Env);
+ -- Merge current permission environment
- Next (Elmt);
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
+ Next (Branch);
end loop;
end;
- -- ELSE part
+ -- ELSE branch
- -- 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.
+ -- Restore current permission environment
+ Copy_Env (Saved_Env, Current_Perm_Env);
Check_List (Else_Statements (Stmt));
- Merge_Envs (New_Env,
- Current_Perm_Env);
+ -- Merge current permission environment
- -- CLEANUP
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
- Copy_Env (New_Env,
- Current_Perm_Env);
+ -- Cleanup
- Free_Env (New_Env);
+ Move_Env (New_Env, Current_Perm_Env);
Free_Env (Saved_Env);
end;
+ -- We should ideally ignore the branch after raising an exception,
+ -- so that it is not taken into account in merges. For now, just
+ -- propagate the current environment.
+
+ when N_Raise_Statement =>
+ null;
+
+ when N_Null_Statement =>
+ null;
+
-- Unsupported constructs in SPARK
when N_Abort_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;
end case;
end Check_Statement;
- --------------
- -- Get_Perm --
- --------------
+ -------------------------
+ -- Check_Type_Legality --
+ -------------------------
+
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
+
+ -------------------
+ -- Emit_Messages --
+ -------------------
+
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
+
+ -- Local variables
+
+ Check_Typ : constant Entity_Id := Retysp (Typ);
- function Get_Perm (N : Node_Id) return Perm_Kind is
- Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
+ -- Start of processing for Check_Type_Legality
begin
- case Tree_Or_Perm.R is
- when Folded =>
- return Tree_Or_Perm.Found_Permission;
+ case Type_Kind'(Ekind (Check_Typ)) is
+ when Access_Kind =>
+ case Access_Kind'(Ekind (Check_Typ)) is
+ when E_Access_Type
+ | E_Anonymous_Access_Type
+ =>
+ null;
+ when E_Access_Subtype =>
+ Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
+ when E_Access_Attribute_Type =>
+ if Emit_Messages then
+ Error_Msg_N ("access attribute not allowed in SPARK",
+ Check_Typ);
+ end if;
+ when E_Allocator_Type =>
+ if Emit_Messages then
+ Error_Msg_N ("missing type resolution", Check_Typ);
+ end if;
+ when E_General_Access_Type =>
+ if Emit_Messages then
+ Error_Msg_NE
+ ("general access type & not allowed in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
+ when Access_Subprogram_Kind =>
+ if Emit_Messages then
+ Error_Msg_NE
+ ("access to subprogram type & not allowed in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
+ end case;
- when Unfolded =>
- pragma Assert (Tree_Or_Perm.Tree_Access /= null);
- return Permission (Tree_Or_Perm.Tree_Access);
+ when E_Array_Type
+ | E_Array_Subtype
+ =>
+ Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
- -- We encoutered a function call, hence the memory area is fresh,
- -- which means that the association permission is RW.
+ when Record_Kind =>
+ if Is_Deep (Check_Typ)
+ and then (Is_Tagged_Type (Check_Typ)
+ or else Is_Class_Wide_Type (Check_Typ))
+ then
+ if Emit_Messages then
+ Error_Msg_NE
+ ("tagged type & cannot be owning in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
- when Function_Call =>
- return Read_Write;
+ else
+ declare
+ Comp : Entity_Id;
+ begin
+ Comp := First_Component_Or_Discriminant (Check_Typ);
+ while Present (Comp) loop
+
+ -- Ignore components which are not visible in SPARK
+
+ if Component_Is_Visible_In_SPARK (Comp) then
+ Check_Type_Legality (Etype (Comp), Force, Legal);
+ end if;
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
+ end;
+ end if;
+
+ when Scalar_Kind
+ | E_String_Literal_Subtype
+ | Protected_Kind
+ | Task_Kind
+ | Incomplete_Kind
+ | E_Exception_Type
+ | E_Subprogram_Type
+ =>
+ null;
+
+ -- Do not check type whose full view is not SPARK
+ when E_Private_Type
+ | E_Private_Subtype
+ | E_Limited_Private_Type
+ | E_Limited_Private_Subtype
+ =>
+ null;
end case;
- end Get_Perm;
+ end Check_Type_Legality;
- ----------------------
- -- Get_Perm_Or_Tree --
- ----------------------
+ --------------
+ -- Get_Expl --
+ --------------
- function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+ function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is
begin
- case Nkind (N) is
+ -- Special case for the object declared in an extended return statement
- -- Base identifier. Normally those are the roots of the trees stored
- -- in the permission environment.
+ if Nkind (N) = N_Defining_Identifier then
+ declare
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (N));
+ begin
+ pragma Assert (C /= null);
+ return Explanation (C);
+ end;
- when N_Defining_Identifier =>
- raise Program_Error;
+ -- The expression is a call to a traversal function
- when N_Identifier
- | N_Expanded_Name
- =>
- declare
- P : constant Entity_Id := Entity (N);
+ elsif Is_Traversal_Function_Call (N) then
+ return N;
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
+ -- The expression is directly rooted in an object
- begin
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
+ elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
+ declare
+ 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.Explanation;
- Set (Current_Initialization_Map, Unique_Entity (P), True);
+ when Unfolded =>
+ pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+ return Explanation (Tree_Or_Perm.Tree_Access);
+ end case;
+ end;
- 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.
+ -- The expression is a function call, an allocation, or null
- Illegal_Global_Usage (N);
- else
- return (R => Unfolded, Tree_Access => C);
- end if;
- end;
+ else
+ return N;
+ end if;
+ end Get_Expl;
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Get_Perm_Or_Tree (Expression (N));
+ -----------------------------------
+ -- Get_Observed_Or_Borrowed_Expr --
+ -----------------------------------
+
+ function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is
+ begin
+ if Is_Traversal_Function_Call (Expr) then
+ return First_Actual (Expr);
+ else
+ return Expr;
+ end if;
+ end Get_Observed_Or_Borrowed_Expr;
- -- 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).
+ --------------
+ -- Get_Perm --
+ --------------
- when N_Parameter_Specification =>
- return Get_Perm_Or_Tree (Defining_Identifier (N));
+ function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is
+ begin
+ -- Special case for the object declared in an extended return statement
- -- 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.
+ if Nkind (N) = N_Defining_Identifier then
+ declare
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (N));
+ begin
+ pragma Assert (C /= null);
+ return Permission (C);
+ end;
- when N_Selected_Component =>
- declare
- C : constant Perm_Or_Tree :=
- Get_Perm_Or_Tree (Prefix (N));
+ -- The expression is a call to a traversal function
- begin
- case C.R is
- when Folded
- | Function_Call
- =>
- return C;
+ elsif Is_Traversal_Function_Call (N) then
+ declare
+ Callee : constant Entity_Id := Get_Called_Entity (N);
+ begin
+ if Is_Access_Constant (Etype (Callee)) then
+ return Read_Only;
+ else
+ return Read_Write;
+ end if;
+ end;
- 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;
+ -- The expression is directly rooted in an object
- -- 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.
+ elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
+ declare
+ 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 N_Indexed_Component
- | N_Slice
- =>
- declare
- C : constant Perm_Or_Tree :=
- Get_Perm_Or_Tree (Prefix (N));
+ when Unfolded =>
+ pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+ return Permission (Tree_Or_Perm.Tree_Access);
+ end case;
+ end;
- begin
- case C.R is
- when Folded
- | Function_Call
- =>
- return C;
+ -- The expression is a function call, an allocation, or null
- when Unfolded =>
- pragma Assert (C.Tree_Access /= null);
+ else
+ return Read_Write;
+ end if;
+ end Get_Perm;
+
+ ----------------------
+ -- Get_Perm_Or_Tree --
+ ----------------------
- pragma Assert (Kind (C.Tree_Access) = Entire_Object
- or else
- Kind (C.Tree_Access) = Array_Component);
+ function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+ begin
+ case Nkind (N) is
- if Kind (C.Tree_Access) = Array_Component then
- pragma Assert (Get_Elem (C.Tree_Access) /= null);
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Get (Current_Perm_Env, Unique_Entity (Entity (N)));
+ begin
+ -- Except during elaboration, the root object should have been
+ -- declared and entered into the current permission
+ -- environment.
- 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;
+ if not Inside_Elaboration
+ and then C = null
+ then
+ Illegal_Global_Usage (N, N);
+ end if;
+
+ return (R => Unfolded, Tree_Access => C);
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.
+ -- For a nonterminal path, we get the permission tree of its
+ -- prefix, and then get the subtree associated with the extension,
+ -- if unfolded. If folded, we return the permission associated with
+ -- children.
- when N_Explicit_Dereference =>
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
declare
- C : constant Perm_Or_Tree :=
- Get_Perm_Or_Tree (Prefix (N));
-
+ C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
begin
case C.R is
- when Folded
- | Function_Call
- =>
- return C;
- when Unfolded =>
- pragma Assert (C.Tree_Access /= null);
+ -- Some earlier prefix was already folded, return the
+ -- permission found.
- pragma Assert (Kind (C.Tree_Access) = Entire_Object
- or else
- Kind (C.Tree_Access) = Reference);
+ when Folded =>
+ return C;
- 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;
+ when Unfolded =>
+ case Kind (C.Tree_Access) is
+
+ -- If the prefix tree is already folded, return the
+ -- children permission.
+
+ when Entire_Object =>
+ return (R => Folded,
+ Found_Permission =>
+ Children_Permission (C.Tree_Access),
+ Explanation =>
+ Explanation (C.Tree_Access));
+
+ when Reference =>
+ pragma Assert (Nkind (N) = N_Explicit_Dereference);
+ return (R => Unfolded,
+ Tree_Access => Get_All (C.Tree_Access));
+
+ when Record_Component =>
+ pragma Assert (Nkind (N) = N_Selected_Component);
+ declare
+ Comp : constant Entity_Id :=
+ Original_Record_Component
+ (Entity (Selector_Name (N)));
+ D : constant Perm_Tree_Access :=
+ Perm_Tree_Maps.Get
+ (Component (C.Tree_Access), Comp);
+ begin
+ pragma Assert (D /= null);
+ return (R => Unfolded,
+ Tree_Access => D);
+ end;
+
+ when Array_Component =>
+ pragma Assert (Nkind (N) = N_Indexed_Component
+ or else
+ Nkind (N) = N_Slice);
+ pragma Assert (Get_Elem (C.Tree_Access) /= null);
+ return (R => Unfolded,
+ Tree_Access => Get_Elem (C.Tree_Access));
+ end case;
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 N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Get_Perm_Or_Tree (Expression (N));
when others =>
raise Program_Error;
-- Get_Perm_Tree --
-------------------
- function Get_Perm_Tree
- (N : Node_Id)
- return Perm_Tree_Access
- is
+ function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
begin
- case Nkind (N) is
-
- -- Base identifier. Normally those are the roots of the trees stored
- -- in the permission environment.
+ return Set_Perm_Prefixes (N, None, Empty);
+ end Get_Perm_Tree;
- when N_Defining_Identifier =>
- raise Program_Error;
+ ---------------------
+ -- Get_Root_Object --
+ ---------------------
- when N_Identifier
- | N_Expanded_Name
- =>
- declare
- P : constant Node_Id := Entity (N);
+ function Get_Root_Object
+ (Expr : Node_Id;
+ Through_Traversal : Boolean := True;
+ Is_Traversal : Boolean := False) return Entity_Id
+ is
+ function GRO (Expr : Node_Id) return Entity_Id;
+ -- Local wrapper on the actual function, to propagate the values of
+ -- optional parameters.
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
+ ---------
+ -- GRO --
+ ---------
- begin
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
+ function GRO (Expr : Node_Id) return Entity_Id is
+ begin
+ return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
+ end GRO;
- Set (Current_Initialization_Map, Unique_Entity (P), True);
+ Get_Root_Object : Boolean;
+ pragma Unmodified (Get_Root_Object);
+ -- Local variable to mask the name of function Get_Root_Object, to
+ -- prevent direct call. Instead GRO wrapper should be called.
- 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.
+ -- Start of processing for Get_Root_Object
- Illegal_Global_Usage (N);
- else
- return C;
- end if;
- end;
+ begin
+ if not Is_Subpath_Expression (Expr, Is_Traversal) then
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ end if;
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Identifier
=>
- return Get_Perm_Tree (Expression (N));
+ return Entity (Expr);
- 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_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ return GRO (Prefix (Expr));
- when N_Selected_Component =>
- declare
- C : constant Perm_Tree_Access :=
- Get_Perm_Tree (Prefix (N));
+ -- There is no root object for an (extension) aggregate, allocator,
+ -- concat, or NULL.
- begin
- if C = null then
- -- If null then it means we went through a function call
+ when N_Aggregate
+ | N_Allocator
+ | N_Extension_Aggregate
+ | N_Null
+ | N_Op_Concat
+ =>
+ return Empty;
- return null;
- end if;
+ -- In the case of a call to a traversal function, the root object is
+ -- the root of the traversed parameter. Otherwise there is no root
+ -- object.
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Record_Component);
+ when N_Function_Call =>
+ if Through_Traversal
+ and then Is_Traversal_Function_Call (Expr)
+ then
+ return GRO (First_Actual (Expr));
+ else
+ return Empty;
+ end if;
- if Kind (C) = Record_Component then
- -- The tree is unfolded. We just return the subtree.
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return GRO (Expression (Expr));
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
- Selected_C : constant Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ when N_Attribute_Reference =>
+ pragma Assert
+ (Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Loop_Entry
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Update
+ or else Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image);
+ return Empty;
- begin
- if Selected_C = null then
- return Other_Components (C);
+ when N_If_Expression =>
+ if Is_Traversal then
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ Then_Root : constant Entity_Id := GRO (Then_Part);
+ Else_Root : constant Entity_Id := GRO (Else_Part);
+ begin
+ if Nkind (Then_Part) = N_Null then
+ return Else_Root;
+ elsif Nkind (Else_Part) = N_Null then
+ return Then_Part;
+ elsif Then_Root = Else_Root then
+ return Then_Root;
+ else
+ if Emit_Messages then
+ Error_Msg_N
+ ("same name expected here in each branch", Expr);
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;
+ return Empty;
end if;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ 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));
+ when N_Case_Expression =>
+ if Is_Traversal then
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+ Cur_Root : Entity_Id;
+ Common_Root : Entity_Id := Empty;
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Get_All => Son);
+ begin
+ while Present (Cur_Case) loop
+ Cur_Root := GRO (Expression (Cur_Case));
+
+ if Common_Root = Empty then
+ Common_Root := Cur_Root;
+ elsif Common_Root /= Cur_Root then
+ if Emit_Messages then
+ Error_Msg_N
+ ("same name expected here in each branch", Expr);
+ end if;
+ return Empty;
+ end if;
+ Next (Cur_Case);
+ end loop;
- return Get_All (C);
- end;
- else
- raise Program_Error;
+ return Common_Root;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
end if;
- end;
-
- -- No permission tree for function calls
-
- when N_Function_Call =>
- return null;
+ return Empty;
+ end if;
when others =>
raise Program_Error;
end case;
- end Get_Perm_Tree;
+ end Get_Root_Object;
---------
-- Glb --
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
+ function Has_Array_Component (Expr : 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
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_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
+ when N_Explicit_Dereference
+ | N_Selected_Component
=>
- 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
+ return Has_Array_Component (Prefix (Expr));
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
+ when N_Allocator
+ | N_Null
+ | N_Function_Call
=>
return False;
- -- We check if the expression inside the conversion has a function
- -- component.
-
- when N_Type_Conversion
+ when N_Qualified_Expression
+ | 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;
+ return Has_Array_Component (Expression (Expr));
when others =>
raise Program_Error;
-
end case;
- end Has_Function_Component;
+ end Has_Array_Component;
--------
-- Hp --
-- Illegal_Global_Usage --
--------------------------
- procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
+ procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id)
+ is
begin
- Error_Msg_NE ("cannot use global variable & of deep type", N, N);
+ Error_Msg_NE ("cannot use global variable & of deep type", N, E);
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;
+ function Is_Deep (Typ : Entity_Id) return Boolean is
begin
- pragma Assert (Is_Type (E));
-
- case Ekind (E) is
- when Scalar_Kind =>
- return False;
-
+ case Type_Kind'(Ekind (Retysp (Typ))) is
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));
+ return Is_Deep (Component_Type (Retysp (Typ)));
- 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
- =>
+ when Record_Kind =>
declare
- Elmt : Entity_Id;
-
+ Comp : Entity_Id;
begin
- Elmt := First_Component_Or_Discriminant (E);
- while Present (Elmt) loop
- if Is_Deep (Etype (Elmt)) then
+ Comp := First_Component_Or_Discriminant (Retysp (Typ));
+ while Present (Comp) loop
+
+ -- Ignore components not visible in SPARK
+
+ if Component_Is_Visible_In_SPARK (Comp)
+ and then Is_Deep (Etype (Comp))
+ then
return True;
- else
- Next_Component_Or_Discriminant (Elmt);
end if;
+ Next_Component_Or_Discriminant (Comp);
end loop;
-
- return False;
end;
+ return False;
- 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 Scalar_Kind
+ | E_String_Literal_Subtype
+ | Protected_Kind
+ | Task_Kind
+ | Incomplete_Kind
+ | E_Exception_Type
+ | E_Subprogram_Type
+ =>
+ return False;
+
+ -- Ignore full view of types if it is not in SPARK
+
+ when E_Private_Type
+ | E_Private_Subtype
+ | E_Limited_Private_Type
+ | E_Limited_Private_Subtype
+ =>
+ return False;
+ end case;
+ end Is_Deep;
+
+ --------------
+ -- Is_Legal --
+ --------------
+
+ function Is_Legal (N : Node_Id) return Boolean is
+ Legal : Boolean := True;
+
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration_Legality (N, Force => False, Legal => Legal);
+ when others =>
+ null;
+ end case;
+
+ return Legal;
+ end Is_Legal;
+
+ ----------------------
+ -- Is_Local_Context --
+ ----------------------
+
+ function Is_Local_Context (Scop : Entity_Id) return Boolean is
+ begin
+ return Is_Subprogram_Or_Entry (Scop)
+ or else Ekind (Scop) = E_Block;
+ end Is_Local_Context;
+
+ ------------------------
+ -- Is_Path_Expression --
+ ------------------------
+
+ function Is_Path_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean
+ is
+ function IPE (Expr : Node_Id) return Boolean;
+ -- Local wrapper on the actual function, to propagate the values of
+ -- optional parameter Is_Traversal.
+
+ ---------
+ -- IPE --
+ ---------
+
+ function IPE (Expr : Node_Id) return Boolean is
+ begin
+ return Is_Path_Expression (Expr, Is_Traversal);
+ end IPE;
+
+ Is_Path_Expression : Boolean;
+ pragma Unmodified (Is_Path_Expression);
+ -- Local variable to mask the name of function Is_Path_Expression, to
+ -- prevent direct call. Instead IPE wrapper should be called.
- when E_Incomplete_Type =>
+ -- Start of processing for Is_Path_Expression
+
+ begin
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Explicit_Dereference
+ | N_Identifier
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
return True;
- when E_Incomplete_Subtype =>
+ -- Special value NULL corresponds to an empty path
+
+ when N_Null =>
return True;
- -- No problem with synchronized types
+ -- Object returned by an (extension) aggregate, an allocator, or
+ -- a function call corresponds to a path.
- when E_Protected_Type
- | E_Protected_Subtype
- | E_Task_Subtype
- | E_Task_Type
- =>
- return False;
+ when N_Aggregate
+ | N_Allocator
+ | N_Extension_Aggregate
+ | N_Function_Call
+ =>
+ return True;
- when E_Exception_Type =>
- return False;
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return IPE (Expression (Expr));
+
+ -- When returning from a traversal function, consider an
+ -- if-expression as a possible path expression.
+
+ when N_If_Expression =>
+ if Is_Traversal then
+ declare
+ Cond : constant Node_Id := First (Expressions (Expr));
+ Then_Part : constant Node_Id := Next (Cond);
+ Else_Part : constant Node_Id := Next (Then_Part);
+ begin
+ return IPE (Then_Part)
+ and then IPE (Else_Part);
+ end;
+ else
+ return False;
+ end if;
+
+ -- When returning from a traversal function, consider
+ -- a case-expression as a possible path expression.
+
+ when N_Case_Expression =>
+ if Is_Traversal then
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+
+ begin
+ while Present (Cur_Case) loop
+ if not IPE (Expression (Cur_Case)) then
+ return False;
+ end if;
+ Next (Cur_Case);
+ end loop;
+
+ return True;
+ end;
+ else
+ return False;
+ end if;
when others =>
- raise Program_Error;
+ return False;
end case;
- end Is_Deep;
+ end Is_Path_Expression;
- ----------------
- -- Is_Shallow --
- ----------------
+ -------------------------
+ -- Is_Prefix_Or_Almost --
+ -------------------------
+
+ function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is
+
+ type Expr_Array is array (Positive range <>) of Node_Id;
+ -- Sequence of expressions that make up a path
+
+ function Get_Expr_Array (Expr : Node_Id) return Expr_Array;
+ pragma Precondition (Is_Path_Expression (Expr));
+ -- Return the sequence of expressions that make up a path
+
+ --------------------
+ -- Get_Expr_Array --
+ --------------------
+
+ function Get_Expr_Array (Expr : Node_Id) return Expr_Array is
+ begin
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ return Expr_Array'(1 => Expr);
+
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ return Get_Expr_Array (Prefix (Expr)) & Expr;
+
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Get_Expr_Array (Expression (Expr));
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Expr_Array;
+
+ -- Local variables
+
+ Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref);
+ Expr_Path : constant Expr_Array := Get_Expr_Array (Expr);
+
+ Prefix_Root : constant Node_Id := Prefix_Path (1);
+ Expr_Root : constant Node_Id := Expr_Path (1);
+
+ Common_Len : constant Positive :=
+ Positive'Min (Prefix_Path'Length, Expr_Path'Length);
+
+ -- Start of processing for Is_Prefix_Or_Almost
+
+ begin
+ if Entity (Prefix_Root) /= Entity (Expr_Root) then
+ return False;
+ end if;
+
+ for J in 2 .. Common_Len loop
+ declare
+ Prefix_Elt : constant Node_Id := Prefix_Path (J);
+ Expr_Elt : constant Node_Id := Expr_Path (J);
+ begin
+ case Nkind (Prefix_Elt) is
+ when N_Explicit_Dereference =>
+ if Nkind (Expr_Elt) /= N_Explicit_Dereference then
+ return False;
+ end if;
+
+ when N_Selected_Component =>
+ if Nkind (Expr_Elt) /= N_Selected_Component
+ or else Original_Record_Component
+ (Entity (Selector_Name (Prefix_Elt)))
+ /= Original_Record_Component
+ (Entity (Selector_Name (Expr_Elt)))
+ then
+ return False;
+ end if;
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then
+ return False;
+ end if;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end;
+ end loop;
+
+ -- If the expression path is longer than the prefix one, then at this
+ -- point the prefix property holds.
+
+ if Expr_Path'Length > Prefix_Path'Length then
+ return True;
- function Is_Shallow (E : Entity_Id) return Boolean is
+ -- Otherwise check if none of the remaining path elements in the
+ -- candidate prefix involve a dereference.
+
+ else
+ for J in Common_Len + 1 .. Prefix_Path'Length loop
+ if Nkind (Prefix_Path (J)) = N_Explicit_Dereference then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end if;
+ end Is_Prefix_Or_Almost;
+
+ ---------------------------
+ -- Is_Subpath_Expression --
+ ---------------------------
+
+ function Is_Subpath_Expression
+ (Expr : Node_Id;
+ Is_Traversal : Boolean := False) return Boolean
+ is
+ begin
+ return Is_Path_Expression (Expr, Is_Traversal)
+
+ or else (Nkind_In (Expr, N_Qualified_Expression,
+ N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ and then Is_Subpath_Expression (Expression (Expr)))
+
+ or else (Nkind (Expr) = N_Attribute_Reference
+ and then
+ (Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Update
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Loop_Entry
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image))
+
+ or else Nkind (Expr) = N_Op_Concat;
+ end Is_Subpath_Expression;
+
+ ---------------------------
+ -- Is_Traversal_Function --
+ ---------------------------
+
+ function Is_Traversal_Function (E : Entity_Id) return Boolean is
+ begin
+ return Ekind (E) = E_Function
+
+ -- A function is said to be a traversal function if the result type of
+ -- the function is an anonymous access-to-object type,
+
+ and then Is_Anonymous_Access_Type (Etype (E))
+
+ -- the function has at least one formal parameter,
+
+ and then Present (First_Formal (E))
+
+ -- and the function's first parameter is of an access type.
+
+ and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
+ end Is_Traversal_Function;
+
+ --------------------------------
+ -- Is_Traversal_Function_Call --
+ --------------------------------
+
+ function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is
begin
- pragma Assert (Is_Type (E));
- return not Is_Deep (E);
- end Is_Shallow;
+ return Nkind (Expr) = N_Function_Call
+ and then Present (Get_Called_Entity (Expr))
+ and then Is_Traversal_Function (Get_Called_Entity (Expr));
+ end Is_Traversal_Function_Call;
------------------
-- Loop_Of_Exit --
end if;
return Entity (Nam);
end Loop_Of_Exit;
+
---------
-- Lub --
---------
- function Lub (P1, P2 : Perm_Kind) return Perm_Kind
- is
+ function Lub (P1, P2 : Perm_Kind) return Perm_Kind is
begin
case P1 is
when No_Access =>
end case;
end Lub;
- ----------------
- -- Merge_Envs --
- ----------------
+ ---------------
+ -- Merge_Env --
+ ---------------
+
+ procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is
+
+ -- Local subprograms
+
+ procedure Apply_Glb_Tree
+ (A : Perm_Tree_Access;
+ P : Perm_Kind);
- 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);
+ --------------------
+ -- Apply_Glb_Tree --
+ --------------------
- procedure Apply_Glb_Tree
- (A : Perm_Tree_Access;
- P : Perm_Kind)
- is
- begin
- A.all.Tree.Permission := Glb (Permission (A), P);
+ 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);
+ 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 Reference =>
+ Apply_Glb_Tree (Get_All (A), P);
- when Array_Component =>
- Apply_Glb_Tree (Get_Elem (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;
+ 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;
+ end;
+ end case;
+ end Apply_Glb_Tree;
- Apply_Glb_Tree (Other_Components (A), P);
- end;
- end case;
- end Apply_Glb_Tree;
+ -----------------
+ -- Merge_Trees --
+ -----------------
+ procedure Merge_Trees
+ (Target : Perm_Tree_Access;
+ Source : Perm_Tree_Access)
+ is
Perm : constant Perm_Kind :=
Glb (Permission (Target), Permission (Source));
(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 =>
Comp :=
Perm_Tree_Maps.Get_Next (Component (Target));
end loop;
- Apply_Glb_Tree (Other_Components (Target), Child_Perm);
end;
when Record_Component =>
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;
+ -- Local variables
+
CompTarget : Perm_Tree_Access;
CompSource : Perm_Tree_Access;
KeyTarget : Perm_Tree_Maps.Key_Option;
+ -- Start of processing for Merge_Env
+
begin
KeyTarget := Get_First_Key (Target);
-- Iterate over every tree of the environment in the target, and merge
end;
Free_Env (Source);
- end Merge_Envs;
+ end Merge_Env;
----------------
-- Perm_Error --
----------------
procedure Perm_Error
- (N : Node_Id;
- Perm : Perm_Kind;
- Found_Perm : Perm_Kind)
+ (N : Node_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id;
+ Forbidden_Perm : Boolean := False)
is
procedure Set_Root_Object
(Path : Node_Id;
raise Program_Error;
end case;
end Set_Root_Object;
-
-- Local variables
Root : Entity_Id;
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;
+ if Emit_Messages then
+ 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);
+ Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
+ end if;
end Perm_Error;
-------------------------------
(E : Entity_Id;
Subp : Entity_Id;
Perm : Perm_Kind;
- Found_Perm : Perm_Kind)
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id)
is
begin
- Error_Msg_Node_2 := Subp;
- Error_Msg_NE ("insufficient permission for & when returning from &",
- Subp, E);
- Perm_Mismatch (Perm, Found_Perm, Subp);
+ if Emit_Messages then
+ Error_Msg_Node_2 := Subp;
+ Error_Msg_NE ("insufficient permission for & when returning from &",
+ Subp, E);
+ Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
+ end if;
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;
+ procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is
- -- We ignore shallow unaliased. They are checked in flow analysis,
- -- allowing backward compatibility.
+ procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id);
+ -- Check expression Expr originating in Root was not borrowed
- if not Has_Alias (N)
- and then Is_Shallow (Etype (N))
- then
- return;
- end if;
+ procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id);
+ -- Check expression Expr originating in Root was not observed
- declare
- Perm_N : constant Perm_Kind := Get_Perm (N);
+ ------------------------
+ -- Check_Not_Borrowed --
+ ------------------------
+ procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is
begin
+ -- An expression without root object cannot be borrowed
- case Current_Checking_Mode is
- -- Check permission R, do nothing
+ if No (Root) then
+ return;
+ end if;
- when Read =>
- if Perm_N not in Read_Perm then
- Perm_Error (N, Read_Only, Perm_N);
- end if;
+ -- Otherwise, try to match the expression with one of the borrowed
+ -- expressions.
- -- If shallow type no need for RW, only R
+ declare
+ Key : Variable_Maps.Key_Option :=
+ Get_First_Key (Current_Borrowers);
+ Var : Entity_Id;
+ Borrowed : Node_Id;
+ B_Pledge : Entity_Id := Empty;
- 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
+ begin
+ -- Search for a call to a pledge function or a global pragma in
+ -- the parents of Expr.
- if Perm_N /= Read_Write then
- Perm_Error (N, Read_Write, Perm_N);
+ declare
+ Call : Node_Id := Expr;
+ begin
+ while Present (Call)
+ and then
+ (Nkind (Call) /= N_Function_Call
+ or else not Is_Pledge_Function (Get_Called_Entity (Call)))
+ loop
+ -- Do not check for borrowed objects in global contracts
+ -- ??? However we should keep these objects in the borrowed
+ -- state when verifying the subprogram so that we can make
+ -- sure that they are only read inside pledges.
+ -- ??? There is probably a better way to disable checking of
+ -- borrows inside global contracts.
+
+ if Nkind (Call) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global
+ then
+ return;
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.
+ Call := Parent (Call);
+ end loop;
- return;
- end if;
+ if Present (Call)
+ and then Nkind (First_Actual (Call)) in N_Has_Entity
+ then
+ B_Pledge := Entity (First_Actual (Call));
+ end if;
+ end;
- -- 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
+ while Key.Present loop
+ Var := Key.K;
+ Borrowed := Get (Current_Borrowers, Var);
- Set_Perm_Extensions_Move (Tree, Etype (N));
- end;
+ if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
+ and then Var /= B_Pledge
+ and then Emit_Messages
+ then
+ Error_Msg_Sloc := Sloc (Borrowed);
+ Error_Msg_N ("object was borrowed #", Expr);
end if;
- -- Check permission RW
+ Key := Get_Next_Key (Current_Borrowers);
+ end loop;
+ end;
+ end Check_Not_Borrowed;
- when Super_Move =>
- if Perm_N /= Read_Write then
- Perm_Error (N, Read_Write, Perm_N);
- end if;
+ ------------------------
+ -- Check_Not_Observed --
+ ------------------------
- declare
- -- Set permission to No to the path and any of its prefix up
- -- to the first .all and then W.
+ procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is
+ begin
+ -- An expression without root object cannot be observed
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Move (N, Super_Move);
+ if No (Root) then
+ return;
+ end if;
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ -- Otherwise, try to match the expression with one of the observed
+ -- expressions.
- return;
- end if;
-
- -- Set permissions to No on any strict extension of the path
-
- Set_Perm_Extensions (Tree, No_Access);
- end;
+ declare
+ Key : Variable_Maps.Key_Option :=
+ Get_First_Key (Current_Observers);
+ Var : Entity_Id;
+ Observed : Node_Id;
- -- Check permission W
+ begin
+ while Key.Present loop
+ Var := Key.K;
+ Observed := Get (Current_Observers, Var);
- when Assign =>
- if Perm_N not in Write_Perm then
- Perm_Error (N, Write_Only, Perm_N);
+ if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr)
+ and then Emit_Messages
+ then
+ Error_Msg_Sloc := Sloc (Observed);
+ Error_Msg_N ("object was observed #", Expr);
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;
+ Key := Get_Next_Key (Current_Observers);
+ end loop;
+ end;
+ end Check_Not_Observed;
- -- Same if has function component
+ -- Local variables
- if Has_Function_Component (N) then
- return;
- end if;
+ Expr_Type : constant Entity_Id := Etype (Expr);
+ Root : Entity_Id := Get_Root_Object (Expr);
+ Perm : Perm_Kind_Option;
- declare
- -- Get the permission tree for the path
+ -- Start of processing for Process_Path
- Tree : constant Perm_Tree_Access :=
- Get_Perm_Tree (N);
+ begin
+ -- Nothing to do if the root type is not deep, or the path is not rooted
+ -- in an object.
- Dummy : Perm_Tree_Access;
+ if not Present (Root)
+ or else not Is_Deep (Etype (Root))
+ then
+ return;
+ end if;
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ -- Identify the root type for the path
- return;
- end if;
+ Root := Unique_Entity (Root);
- -- Set permission RW for it and all of its extensions
+ -- Except during elaboration, the root object should have been declared
+ -- and entered into the current permission environment.
- Tree.all.Tree.Permission := Read_Write;
+ if not Inside_Elaboration
+ and then Get (Current_Perm_Env, Root) = null
+ then
+ Illegal_Global_Usage (Expr, Root);
+ end if;
- Set_Perm_Extensions (Tree, Read_Write);
+ -- During elaboration, only the validity of operations is checked, no
+ -- need to compute the permission of Expr.
- -- Normalize the permission tree
+ if Inside_Elaboration then
+ Perm := None;
+ else
+ Perm := Get_Perm (Expr);
+ end if;
- Dummy := Set_Perm_Prefixes_Assign (N);
- end;
+ -- Check permissions
- -- Check permission W
+ case Mode is
- when Borrow_Out =>
- if Perm_N not in Write_Perm then
- Perm_Error (N, Write_Only, Perm_N);
- end if;
+ when Read =>
- declare
- -- Set permission to No to the path and any of its prefixes
+ -- No checking needed during elaboration
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow_Out (N);
+ if Inside_Elaboration then
+ return;
+ end if;
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ -- Check path is readable
- return;
- end if;
+ if Perm not in Read_Perm then
+ Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- -- Set permissions to No on any strict extension of the path
+ when Move =>
- Set_Perm_Extensions (Tree, No_Access);
- end;
+ -- Forbidden on deep path during elaboration, otherwise no
+ -- checking needed.
- when Observe =>
- if Perm_N not in Read_Perm then
- Perm_Error (N, Read_Only, Perm_N);
+ if Inside_Elaboration then
+ if Is_Deep (Expr_Type)
+ and then not Inside_Procedure_Call
+ and then Present (Get_Root_Object (Expr))
+ and then Emit_Messages
+ then
+ Error_Msg_N ("illegal move during elaboration", Expr);
end if;
- if Is_By_Copy_Type (Etype (N)) then
- return;
+ return;
+ end if;
+
+ -- For deep path, check RW permission, otherwise R permission
+
+ if not Is_Deep (Expr_Type) then
+ if Perm not in Read_Perm then
+ Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
end if;
+ return;
+ end if;
- declare
- -- Set permission to No on the path and any of its prefixes
+ -- SPARK RM 3.10(1): At the point of a move operation the state of
+ -- the source object (if any) shall be Unrestricted.
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Observe (N);
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- begin
- if Tree = null then
- -- We went through a function call, no permission to
- -- modify.
+ when Assign =>
- return;
- end if;
+ -- No checking needed during elaboration
- -- Set permissions to No on any strict extension of the path
+ if Inside_Elaboration then
+ return;
+ end if;
- Set_Perm_Extensions (Tree, Read_Only);
- end;
- end case;
- end;
- end Process_Path;
+ -- For assignment, check W permission
- -------------------------
- -- Return_Declarations --
- -------------------------
+ if Perm not in Write_Perm then
+ Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- procedure Return_Declarations (L : List_Id) is
+ when Borrow =>
- procedure Return_Declaration (Decl : Node_Id);
- -- Check correct permissions for every declared object
+ -- Forbidden during elaboration, an error is already issued in
+ -- Check_Declaration, just return.
- ------------------------
- -- Return_Declaration --
- ------------------------
+ if Inside_Elaboration then
+ return;
+ end if;
- 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.
+ -- For borrowing, check RW permission
- if Get (Current_Initialization_Map,
- Unique_Entity (Defining_Identifier (Decl))) = False
- then
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
return;
end if;
- -- We ignore shallow unaliased. They are checked in flow analysis,
- -- allowing backward compatibility.
+ when Observe =>
- if not Has_Alias (Defining_Identifier (Decl))
- and then Is_Shallow (Etype (Defining_Identifier (Decl)))
- then
+ -- Forbidden during elaboration, an error is already issued in
+ -- Check_Declaration, just return.
+
+ if Inside_Elaboration then
return;
end if;
- declare
- Elem : constant Perm_Tree_Access :=
- Get (Current_Perm_Env,
- Unique_Entity (Defining_Identifier (Decl)));
+ -- For borrowing, check R permission
- 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.
+ if Perm not in Read_Perm then
+ Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
+ end case;
- -- Hash_Table_Error
- raise Program_Error;
- end if;
+ -- Check path was not borrowed
- if Permission (Elem) /= Read_Write then
- Perm_Error (Decl, Read_Write, Permission (Elem));
- end if;
- end;
- end if;
- end Return_Declaration;
+ Check_Not_Borrowed (Expr, Root);
- -- Local Variables
+ -- For modes that require W permission, check path was not observed
- N : Node_Id;
+ case Mode is
+ when Read | Observe =>
+ null;
+ when Assign | Move | Borrow =>
+ Check_Not_Observed (Expr, Root);
+ end case;
- -- Start of processing for Return_Declarations
+ -- Do not update permission environment when handling calls
- begin
- N := First (L);
- while Present (N) loop
- Return_Declaration (N);
- Next (N);
- end loop;
- end Return_Declarations;
+ if Inside_Procedure_Call then
+ return;
+ end if;
- --------------------
- -- Return_Globals --
- --------------------
+ -- Update the permissions
- procedure Return_Globals (Subp : Entity_Id) is
+ case Mode is
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind);
- -- Return global items from the list starting at Item
+ when Read =>
+ null;
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
- -- Return global items for the mode Global_Mode
+ when Move =>
- ------------------------------
- -- Return_Globals_From_List --
- ------------------------------
+ -- SPARK RM 3.10(1): After a move operation, the state of the
+ -- source object (if any) becomes Moved.
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind)
- is
- Item : Node_Id := First_Item;
- E : Entity_Id;
+ if Present (Get_Root_Object (Expr)) then
+ declare
+ Tree : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr);
+ begin
+ pragma Assert (Tree /= null);
+ Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr);
+ end;
+ end if;
- begin
- while Present (Item) loop
- E := Entity (Item);
+ when Assign =>
- -- Ignore abstract states, which play no role in pointer aliasing
+ -- If there is no root object, or the tree has an array component,
+ -- then the permissions do not get modified by the assignment.
- if Ekind (E) = E_Abstract_State then
- null;
- else
- Return_Parameter_Or_Global (E, Kind, Subp);
+ if No (Get_Root_Object (Expr))
+ or else Has_Array_Component (Expr)
+ then
+ return;
end if;
- Next_Global (Item);
- end loop;
- end Return_Globals_From_List;
- ----------------------------
- -- Return_Globals_Of_Mode --
- ----------------------------
+ -- Set permission RW for the path and its extensions
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
- Kind : Formal_Kind;
+ declare
+ Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr);
+ begin
+ Tree.all.Tree.Permission := Read_Write;
+ Set_Perm_Extensions (Tree, Read_Write, Expl => Expr);
- 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;
+ -- Normalize the permission tree
+
+ Set_Perm_Prefixes_Assign (Expr);
+ end;
- -- Return both global items from Global and Refined_Global pragmas
+ -- Borrowing and observing of paths is handled by the variables
+ -- Current_Borrowers and Current_Observers.
- 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;
+ when Borrow | Observe =>
+ null;
+ end case;
+ end Process_Path;
+
+ --------------------
+ -- Return_Globals --
+ --------------------
+
+ procedure Return_Globals (Subp : Entity_Id) is
+
+ procedure Return_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean);
+ -- Proxy procedure to return globals, to adjust for the type of first
+ -- parameter expected by Return_Parameter_Or_Global.
+
+ -------------------
+ -- Return_Global --
+ -------------------
+
+ procedure Return_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean)
+ is
+ begin
+ Return_Parameter_Or_Global
+ (Id => Entity (Expr),
+ Typ => Typ,
+ Kind => Kind,
+ Subp => Subp,
+ Global_Var => Global_Var);
+ end Return_Global;
+
+ procedure Return_Globals_Inst is new Handle_Globals (Return_Global);
-- 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);
+ Return_Globals_Inst (Subp);
end Return_Globals;
--------------------------------
--------------------------------
procedure Return_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id)
+ (Id : Entity_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean)
is
- Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
- pragma Assert (Elem /= null);
-
begin
- -- Shallow unaliased parameters and globals cannot introduce pointer
- -- aliasing.
+ -- Shallow parameters and globals need not be considered
+
+ if not Is_Deep (Typ) then
+ return;
+
+ elsif Kind = E_In_Parameter then
+
+ -- Input global variables are observed only
+
+ if Global_Var then
+ return;
+
+ -- Anonymous access to constant is an observe
- if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then
- null;
+ elsif Is_Anonymous_Access_Type (Typ)
+ and then Is_Access_Constant (Typ)
+ then
+ return;
- -- Observed IN parameters and globals need not return a permission to
- -- the caller.
+ -- Deep types other than access types define an observe
- elsif Mode = E_In_Parameter and then not Is_Borrowed_In (Id) then
- null;
+ elsif not Is_Access_Type (Typ) then
+ return;
+ end if;
+ end if;
-- All other parameters and globals should return with mode RW to the
-- caller.
- else
- if Permission (Elem) /= Read_Write then
+ declare
+ Tree : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
+ begin
+ if Permission (Tree) /= Read_Write then
Perm_Error_Subprogram_End
(E => Id,
Subp => Subp,
Perm => Read_Write,
- Found_Perm => Permission (Elem));
+ Found_Perm => Permission (Tree),
+ Expl => Explanation (Tree));
end if;
- end if;
+ end;
end Return_Parameter_Or_Global;
-----------------------
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);
+ Return_Parameter_Or_Global
+ (Id => Formal,
+ Typ => Retysp (Etype (Formal)),
+ Kind => Ekind (Formal),
+ Subp => Subp,
+ Global_Var => False);
Next_Formal (Formal);
end loop;
end Return_Parameters;
-------------------------
procedure Set_Perm_Extensions
- (T : Perm_Tree_Access;
- P : Perm_Kind)
- is
+ (T : Perm_Tree_Access;
+ P : Perm_Kind;
+ Expl : Node_Id) is
+
procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
+ -- Free the permission tree of children if any, prio to replacing T
- procedure Free_Perm_Tree_Children (T : Perm_Tree_Access)
- is
+ -----------------------------
+ -- Free_Perm_Tree_Children --
+ -----------------------------
+
+ 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);
+ Free_Tree (T.all.Tree.Get_All);
when Array_Component =>
- Free_Perm_Tree (T.all.Tree.Get_Elem);
-
- -- Free every Component subtree
+ Free_Tree (T.all.Tree.Get_Elem);
when Record_Component =>
declare
- Comp : Perm_Tree_Access;
+ Hashtbl : Perm_Tree_Maps.Instance := Component (T);
+ Comp : Perm_Tree_Access;
begin
- Comp := Perm_Tree_Maps.Get_First (Component (T));
+ Comp := Perm_Tree_Maps.Get_First (Hashtbl);
while Comp /= null loop
- Free_Perm_Tree (Comp);
- Comp := Perm_Tree_Maps.Get_Next (Component (T));
+ Free_Tree (Comp);
+ Comp := Perm_Tree_Maps.Get_Next (Hashtbl);
end loop;
- Free_Perm_Tree (T.all.Tree.Other_Components);
+ Perm_Tree_Maps.Reset (Hashtbl);
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);
+ -- Start of processing for Set_Perm_Extensions
begin
Free_Perm_Tree_Children (T);
- T.all.Tree := Son;
+ T.all.Tree := Perm_Tree'(Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (T),
+ Explanation => Expl,
+ Permission => Permission (T),
+ Children_Permission => P);
end Set_Perm_Extensions;
------------------------------
------------------------------
procedure Set_Perm_Extensions_Move
- (T : Perm_Tree_Access;
- E : Entity_Id)
+ (T : Perm_Tree_Access;
+ E : Entity_Id;
+ Expl : Node_Id)
is
+ Check_Ty : constant Entity_Id := Retysp (E);
begin
- if not Is_Node_Deep (T) then
- -- We are a shallow extension with same number of .all
+ -- Shallow extensions are set to RW
- Set_Perm_Extensions (T, Read_Write);
+ if not Is_Node_Deep (T) then
+ Set_Perm_Extensions (T, Read_Write, Expl => Expl);
return;
end if;
- -- We are a deep extension here (or the moved deep path)
+ -- Deep extensions are set to W before .all and NO afterwards
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.
+ -- For a folded tree of composite type, unfold the tree for better
+ -- precision.
+ when Entire_Object =>
+ case Ekind (Check_Ty) is
when E_Array_Type
- | E_Array_Subtype =>
+ | E_Array_Subtype
+ =>
declare
- Son : Perm_Tree_Access;
-
+ C : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (T),
+ Explanation => Expl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
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));
-
+ Set_Perm_Extensions_Move
+ (C, Component_Type (Check_Ty), Expl);
T.all.Tree := (Kind => Array_Component,
Is_Node_Deep => Is_Node_Deep (T),
+ Explanation => Expl,
Permission => Write_Only,
- Get_Elem => Son);
+ Get_Elem => C);
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
- =>
+ when Record_Kind =>
declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
+ C : Perm_Tree_Access;
+ Comp : Entity_Id;
+ Hashtbl : Perm_Tree_Maps.Instance;
- Elem : Node_Id;
+ begin
+ Comp := First_Component_Or_Discriminant (Check_Ty);
+ while Present (Comp) loop
- Son : Perm_Tree_Access;
+ -- Unfold components which are visible in SPARK
- begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
+ if Component_Is_Visible_In_SPARK (Comp) then
+ C := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Comp)),
+ Explanation => Expl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
+
+ -- Hidden components are never deep
+
+ else
+ C := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => False,
+ Explanation => Expl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ Set_Perm_Extensions (C, Read_Write, Expl => Expl);
+ end if;
- pragma Assert (Is_Node_Deep (T));
+ Perm_Tree_Maps.Set
+ (Hashtbl, Original_Record_Component (Comp), C);
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
T.all.Tree :=
(Kind => Record_Component,
Is_Node_Deep => Is_Node_Deep (T),
+ Explanation => Expl,
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;
+ Component => Hashtbl);
end;
- when E_Private_Type
- | E_Private_Subtype
- | E_Limited_Private_Type
- | E_Limited_Private_Subtype
- =>
- Set_Perm_Extensions_Move (T, Underlying_Type (E));
+ -- Otherwise, extensions are set to NO
when others =>
- raise Program_Error;
+ Set_Perm_Extensions (T, No_Access, Expl);
end case;
when Reference =>
- -- Now the son does not have the same number of .all
- Set_Perm_Extensions (T, No_Access);
+ Set_Perm_Extensions (T, No_Access, Expl);
when Array_Component =>
- Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E));
+ Set_Perm_Extensions_Move
+ (Get_Elem (T), Component_Type (Check_Ty), Expl);
when Record_Component =>
declare
- Comp : Perm_Tree_Access;
- It : Node_Id;
+ C : Perm_Tree_Access;
+ Comp : Entity_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;
+ Comp := First_Component_Or_Discriminant (Check_Ty);
+ while Present (Comp) loop
+ C := Perm_Tree_Maps.Get
+ (Component (T), Original_Record_Component (Comp));
+ pragma Assert (C /= null);
- ------------------------------
- -- 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);
+ -- Move visible components
- -- 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;
+ if Component_Is_Visible_In_SPARK (Comp) then
+ Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
- when N_Function_Call =>
- return null;
+ -- Hidden components are never deep
- when others =>
- raise Program_Error;
- end case;
+ else
+ Set_Perm_Extensions (C, Read_Write, Expl => Expl);
+ end if;
- end Set_Perm_Prefixes_Move;
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
+ end;
+ end case;
+ end Set_Perm_Extensions_Move;
- -------------------------------
- -- Set_Perm_Prefixes_Observe --
- -------------------------------
+ -----------------------
+ -- Set_Perm_Prefixes --
+ -----------------------
- function Set_Perm_Prefixes_Observe
- (N : Node_Id)
- return Perm_Tree_Access
+ function Set_Perm_Prefixes
+ (N : Node_Id;
+ Perm : Perm_Kind_Option;
+ Expl : 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
+ when N_Expanded_Name
+ | N_Identifier
=>
declare
- P : Node_Id;
- C : Perm_Tree_Access;
+ E : constant Entity_Id := Unique_Entity (Entity (N));
+ C : constant Perm_Tree_Access := Get (Current_Perm_Env, E);
+ pragma Assert (C /= null);
begin
- if Nkind (N) = N_Defining_Identifier then
- P := N;
- else
- P := Entity (N);
+ if Perm /= None then
+ C.all.Tree.Permission := Glb (Perm, Permission (C));
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.
+ return C;
+ end;
- Set (Current_Initialization_Map, Unique_Entity (P), True);
+ -- For a nonterminal path, 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 one level.
- 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.
+ when N_Explicit_Dereference =>
+ declare
+ C : constant Perm_Tree_Access :=
+ Set_Perm_Prefixes (Prefix (N), Perm, Expl);
+ pragma Assert (C /= null);
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Reference);
+ begin
+ -- The tree is already unfolded. Replace the permission of the
+ -- dereference.
- Illegal_Global_Usage (N);
- end if;
+ if Kind (C) = Reference then
+ declare
+ D : constant Perm_Tree_Access := Get_All (C);
+ pragma Assert (D /= null);
- C.all.Tree.Permission := Glb (Read_Only, Permission (C));
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Glb (Perm, Permission (D));
+ end if;
- return C;
- end;
+ return D;
+ end;
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Set_Perm_Prefixes_Observe (Expression (N));
+ -- The tree is folded. Expand it.
- when N_Parameter_Specification =>
- raise Program_Error;
+ else
+ declare
+ pragma Assert (Kind (C) = Entire_Object);
+
+ Child_P : constant Perm_Kind := Children_Permission (C);
+ D : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (N)),
+ Explanation => Expl,
+ Permission => Child_P,
+ Children_Permission => Child_P));
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Perm;
+ end if;
- -- 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.
+ C.all.Tree := (Kind => Reference,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Explanation => Expl,
+ Permission => Permission (C),
+ Get_All => D);
+ return D;
+ end;
+ end if;
+ end;
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;
-
+ Set_Perm_Prefixes (Prefix (N), Perm, Expl);
+ pragma Assert (C /= null);
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Record_Component);
+ begin
+ -- The tree is already unfolded. Replace the permission of the
+ -- 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);
+ Comp : constant Entity_Id :=
+ Original_Record_Component
+ (Entity (Selector_Name (N)));
+ D : constant Perm_Tree_Access :=
+ Perm_Tree_Maps.Get (Component (C), Comp);
+ pragma Assert (D /= null);
begin
- if Selected_C = null then
- Selected_C := Other_Components (C);
+ if Perm /= None then
+ D.all.Tree.Permission := Glb (Perm, Permission (D));
end if;
- pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission :=
- Glb (Read_Only, Permission (Selected_C));
-
- return Selected_C;
+ return D;
end;
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
- Elem : Node_Id;
+ -- The tree is folded. Expand it.
- -- Create an empty hash table
+ else
+ declare
+ pragma Assert (Kind (C) = Entire_Object);
+ D : Perm_Tree_Access;
+ D_This : Perm_Tree_Access;
+ Comp : Node_Id;
+ P : Perm_Kind;
+ Child_P : constant Perm_Kind := Children_Permission (C);
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);
+ -- Create an empty hash table
begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
+ Comp :=
+ First_Component_Or_Discriminant
+ (Retysp (Etype (Prefix (N))));
+
+ while Present (Comp) loop
+ if Perm /= None
+ and then Original_Record_Component (Comp) =
+ Original_Record_Component
+ (Entity (Selector_Name (N)))
+ then
+ P := Perm;
+ else
+ P := Child_P;
+ end if;
- 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'
+ D := new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Elem)),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
-
+ Is_Node_Deep =>
+ -- Hidden components are never deep
+ Component_Is_Visible_In_SPARK (Comp)
+ and then Is_Deep (Etype (Comp)),
+ Explanation => Expl,
+ Permission => P,
+ Children_Permission => Child_P));
Perm_Tree_Maps.Set
- (C.all.Tree.Component, Elem, Son);
-
- Next_Component_Or_Discriminant (Elem);
- end loop;
+ (Hashtbl, Original_Record_Component (Comp), D);
- -- Now we set the right field to Read_Only. and then we
- -- return the tree to the sons, so that the recursion can
- -- continue.
+ -- Store the tree to return for this component
- 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);
+ if Original_Record_Component (Comp) =
+ Original_Record_Component
+ (Entity (Selector_Name (N)))
+ then
+ D_This := D;
end if;
- pragma Assert (Selected_C /= null);
-
- Selected_C.all.Tree.Permission :=
- Glb (Read_Only, Child_Perm);
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
- return Selected_C;
- end;
+ C.all.Tree := (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Explanation => Expl,
+ Permission => Permission (C),
+ Component => Hashtbl);
+ return D_This;
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;
-
+ Set_Perm_Prefixes (Prefix (N), Perm, Expl);
+ pragma Assert (C /= null);
pragma Assert (Kind (C) = Entire_Object
or else Kind (C) = Array_Component);
+ begin
+ -- The tree is already unfolded. Replace the permission of the
+ -- 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.
+ D : constant Perm_Tree_Access := Get_Elem (C);
+ pragma Assert (D /= null);
- Son : Perm_Tree_Access;
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Glb (Perm, Permission (D));
+ end if;
- Child_Perm : constant Perm_Kind :=
- Glb (Read_Only, Children_Permission (C));
+ return D;
+ end;
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
+ -- The tree is folded. Expand it.
- -- We change the current node from Entire_Object
- -- to Array_Component with same permission and the
- -- previously defined son.
+ else
+ declare
+ pragma Assert (Kind (C) = Entire_Object);
+
+ Child_P : constant Perm_Kind := Children_Permission (C);
+ D : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Explanation => Expl,
+ Permission => Child_P,
+ Children_Permission => Child_P));
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Perm;
+ end if;
C.all.Tree := (Kind => Array_Component,
Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
- Get_Elem => Son);
-
- return Get_Elem (C);
+ Explanation => Expl,
+ Permission => Permission (C),
+ Get_Elem => D);
+ return D;
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));
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Set_Perm_Prefixes (Expression (N), Perm, Expl);
- begin
- if C = null then
- -- We went through a function call, do nothing
+ when others =>
+ raise Program_Error;
+ end case;
+ end Set_Perm_Prefixes;
- return null;
- end if;
+ ------------------------------
+ -- Set_Perm_Prefixes_Assign --
+ ------------------------------
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Reference);
+ procedure Set_Perm_Prefixes_Assign (N : Node_Id) is
+ C : constant Perm_Tree_Access := Get_Perm_Tree (N);
- if Kind (C) = Reference then
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
+ begin
+ case Kind (C) is
+ when Entire_Object =>
+ pragma Assert (Children_Permission (C) = Read_Write);
+ C.all.Tree.Permission := Read_Write;
- pragma Assert (Get_All (C) /= null);
+ when Reference =>
+ C.all.Tree.Permission :=
+ Lub (Permission (C), Permission (Get_All (C)));
- C.all.Tree.Get_All.all.Tree.Permission :=
- Glb (Read_Only, Permission (Get_All (C)));
+ when Array_Component =>
+ null;
- return Get_All (C);
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with Reference.
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ Perm : Perm_Kind := Read_Write;
- Son : Perm_Tree_Access;
+ begin
+ -- We take the Glb of all the descendants, and then update the
+ -- permission of the node with it.
- Child_Perm : constant Perm_Kind :=
- Glb (Read_Only, Children_Permission (C));
+ 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;
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => Child_Perm,
- Children_Permission => Child_Perm));
+ C.all.Tree.Permission := Lub (Permission (C), Perm);
+ end;
+ end case;
- -- We change the current node from Entire_Object to
- -- Reference with Write_Only and the previous son.
+ case Nkind (N) is
- pragma Assert (Is_Node_Deep (C));
+ -- Base identifier end recursion
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Child_Perm,
- Get_All => Son);
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ null;
- return Get_All (C);
- end;
- else
- raise Program_Error;
- end if;
- end;
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ Set_Perm_Prefixes_Assign (Prefix (N));
- when N_Function_Call =>
- return null;
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ Set_Perm_Prefixes_Assign (Expression (N));
when others =>
raise Program_Error;
-
end case;
- end Set_Perm_Prefixes_Observe;
+ end Set_Perm_Prefixes_Assign;
-------------------
-- 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
+ procedure Setup_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean);
+ -- Proxy procedure to set up globals, to adjust for the type of first
+ -- parameter expected by Setup_Parameter_Or_Global.
- -----------------------------
- -- Setup_Globals_From_List --
- -----------------------------
+ ------------------
+ -- Setup_Global --
+ ------------------
- procedure Setup_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind)
+ procedure Setup_Global
+ (Expr : Node_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean)
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;
+ Setup_Parameter_Or_Global
+ (Id => Entity (Expr),
+ Typ => Typ,
+ Kind => Kind,
+ Subp => Subp,
+ Global_Var => Global_Var,
+ Expl => Expr);
+ end Setup_Global;
- -- 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;
+ procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global);
-- 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);
+ Setup_Globals_Inst (Subp);
end Setup_Globals;
-------------------------------
-------------------------------
procedure Setup_Parameter_Or_Global
- (Id : Entity_Id;
- Mode : Formal_Kind)
+ (Id : Entity_Id;
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean;
+ Expl : Node_Id)
is
- Elem : Perm_Tree_Access;
+ Perm : Perm_Kind_Option;
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
+ case Kind is
when E_In_Parameter =>
- -- Borrowed IN: RW for everybody
+ -- Shallow parameters and globals need not be considered
+
+ if not Is_Deep (Typ) then
+ Perm := None;
+
+ -- Inputs of functions have R permission only
+
+ elsif Ekind (Subp) = E_Function then
+ Perm := Read_Only;
+
+ -- Input global variables have R permission only
+
+ elsif Global_Var then
+ Perm := Read_Only;
- if Is_Borrowed_In (Id) then
- Elem.all.Tree.Permission := Read_Write;
- Elem.all.Tree.Children_Permission := Read_Write;
+ -- Anonymous access to constant is an observe
- -- Observed IN: R for everybody
+ elsif Is_Anonymous_Access_Type (Typ)
+ and then Is_Access_Constant (Typ)
+ then
+ Perm := Read_Only;
+
+ -- Other access types are a borrow
+
+ elsif Is_Access_Type (Typ) then
+ Perm := Read_Write;
+
+ -- Deep types other than access types define an observe
else
- Elem.all.Tree.Permission := Read_Only;
- Elem.all.Tree.Children_Permission := Read_Only;
+ Perm := Read_Only;
end if;
- -- OUT: borrow, but callee has W only
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
+ -- Shallow parameters and globals need not be considered
- when E_Out_Parameter =>
- Elem.all.Tree.Permission := Write_Only;
- Elem.all.Tree.Children_Permission := Write_Only;
+ if not Is_Deep (Typ) then
+ Perm := None;
- -- IN OUT: borrow and callee has RW
+ -- Functions cannot have outputs in SPARK
- when E_In_Out_Parameter =>
- Elem.all.Tree.Permission := Read_Write;
- Elem.all.Tree.Children_Permission := Read_Write;
+ elsif Ekind (Subp) = E_Function then
+ return;
+
+ -- Deep types define a borrow or a move
+
+ else
+ Perm := Read_Write;
+ end if;
end case;
- Set (Current_Perm_Env, Id, Elem);
+ if Perm /= None then
+ declare
+ Tree : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Id)),
+ Explanation => Expl,
+ Permission => Perm,
+ Children_Permission => Perm));
+ begin
+ Set (Current_Perm_Env, Id, Tree);
+ end;
+ end if;
end Setup_Parameter_Or_Global;
----------------------
procedure Setup_Parameters (Subp : Entity_Id) is
Formal : Entity_Id;
-
begin
Formal := First_Formal (Subp);
while Present (Formal) loop
- Setup_Parameter_Or_Global (Formal, Ekind (Formal));
+ Setup_Parameter_Or_Global
+ (Id => Formal,
+ Typ => Retysp (Etype (Formal)),
+ Kind => Ekind (Formal),
+ Subp => Subp,
+ Global_Var => False,
+ Expl => Formal);
Next_Formal (Formal);
end loop;
end Setup_Parameters;
+ --------------------------------
+ -- Setup_Protected_Components --
+ --------------------------------
+
+ procedure Setup_Protected_Components (Subp : Entity_Id) is
+ Typ : constant Entity_Id := Scope (Subp);
+ Comp : Entity_Id;
+ Kind : Formal_Kind;
+
+ begin
+ Comp := First_Component_Or_Discriminant (Typ);
+
+ -- The protected object is an implicit input of protected functions, and
+ -- an implicit input-output of protected procedures and entries.
+
+ if Ekind (Subp) = E_Function then
+ Kind := E_In_Parameter;
+ else
+ Kind := E_In_Out_Parameter;
+ end if;
+
+ while Present (Comp) loop
+ Setup_Parameter_Or_Global
+ (Id => Comp,
+ Typ => Retysp (Etype (Comp)),
+ Kind => Kind,
+ Subp => Subp,
+ Global_Var => False,
+ Expl => Comp);
+
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
+ end Setup_Protected_Components;
+
end Sem_SPARK;
projects / thirdparty / gcc.git / blobdiff