-- --
-- 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;
type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
- function Elaboration_Context_Hash (Key : Entity_Id)
- return Elaboration_Context_Index;
- -- Function to hash any node of the AST
+ function Elaboration_Context_Hash
+ (Key : Entity_Id) return Elaboration_Context_Index;
+ -- 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.
+ );
- type Perm_Kind is (Borrowed, Observed, Unrestricted, Moved);
- -- Permission type associated with paths. The Moved permission is
- -- equivalent to the Unrestricted one (same permissions). The Moved is
- -- however used to mark the RHS after a move (which still unrestricted).
- -- This way, we may generate warnings when manipulating the RHS
- -- afterwads since it is set to Null after the assignment.
+ 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;
type Perm_Tree_Wrapper;
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.
+
+ 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 =>
Children_Permission : Perm_Kind;
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 =>
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 Copy_Tree
- (From : Perm_Tree_Access;
- To : Perm_Tree_Access);
+ 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, 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.
-- 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;
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;
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));
end loop;
end;
end case;
-
end Copy_Tree;
------------------------------
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 --
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 --
-- Perm_Mismatch --
-------------------
- procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is
+ procedure Perm_Mismatch
+ (N : Node_Id;
+ Exp_Perm : Perm_Kind;
+ Act_Perm : Perm_Kind;
+ Expl : Node_Id;
+ Forbidden_Perm : Boolean := False)
+ is
begin
- Error_Msg_N ("\expected state `"
- & Perm_Kind'Image (Exp_Perm) & "` at least, 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,
+ (Read_Subexpr,
+ -- Special value used for assignment, to check that subexpressions of
+ -- the assigned path are readable.
+
+ Read,
-- Default mode
Move,
- -- Regular moving semantics. Checks that paths have Unrestricted
- -- permission. After moving a path, the permission of both it and
- -- its extensions are set to Unrestricted.
+ -- 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 Unrestricted permission. After
- -- assigning to a path, its permission is set to Unrestricted.
+ -- mode OUT. Checks that paths have Write_Perm permission. After
+ -- 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,
- -- Used for the source of an assignement when initializes a stand alone
- -- object of anonymous type, constant, or IN parameter and also OUT
- -- or IN OUT composite object.
- -- In the borrowed state, the access object is completely "dead".
+ -- 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 Observed.
- --
- -- 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 --
-----------------------
- -- 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.
+ function "<=" (P1, P2 : Perm_Kind) return Boolean;
+ function ">=" (P1, P2 : Perm_Kind) return Boolean;
+ function Glb (P1, P2 : Perm_Kind) return Perm_Kind;
+ function Lub (P1, P2 : Perm_Kind) return Perm_Kind;
+
+ 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 (unrestricted for borrowed and moved, observed
- -- for observed names).
+ -- 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);
- -- This procedure takes a global pragma and checks it
+ -- 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_In (Formal : Entity_Id; Actual : Node_Id);
- -- This procedure takes a formal and an actual parameter and checks the
- -- permission of every in-mode parameter. This includes Observing and
- -- Borrowing.
+ procedure Check_Package_Spec (Pack : Node_Id);
+
+ 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_Pragma (Prag : Node_Id);
- procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
- -- This procedure takes a formal and an actual parameter and checks the
- -- state of every out-mode and in out-mode parameter. This includes
- -- Moving and Borrowing.
+ 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;
+ 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_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_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 Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
-- The function that takes a name as input and returns a permission
- -- associated to it.
+ -- associated with it.
function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
- -- This function gets a Node_Id and looks recursively to find the
- -- appropriate subtree for that Node_Id. If the tree is folded on
- -- that node, then it returns the permission given at the right level.
+ 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 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.
+ 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_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_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_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_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_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 Unrestricted
- -- 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.
-
- procedure Return_The_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id);
- -- Auxiliary procedure to Return_Globals
- -- There is no need to return parameters because they will be reassigned
- -- their state once the subprogram returns. Local variables that have
- -- borrowed, observed, or moved an actual parameter go out of the scope.
-
- procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
+ -- of the subprogram indeed have Read_Write permission at the end of the
+ -- subprogram execution.
+
+ procedure Return_Parameter_Or_Global
+ (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 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;
+ 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.
- function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
- -- This function modifies the permissions of a given node_id in the
- -- permission environment as well as in all the prefixes of the path,
- -- given that the path is borrowed with mode out.
+ 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
- (N : Node_Id;
- New_Perm : Perm_Kind)
- return Perm_Tree_Access;
- -- This function sets the permissions of a given node_id in the
- -- permission environment as well as in all the prefixes of the path
- -- to the one given in parameter (P).
+ (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.
+ --
+ -- Case where we have to normalize a tree after the correct permissions
+ -- have been assigned already. We look for the right subtree at the given
+ -- path, actualize its permissions, and then call the normalization on its
+ -- parent.
+ --
+ -- Example: We assign x.y and x.z, and then Set_Perm_Prefixes_Assign will
+ -- change the permission of x to RW because all of its components have
+ -- permission RW.
procedure Setup_Globals (Subp : Entity_Id);
-- Takes a subprogram as input, and sets up the environment by adding
procedure Setup_Parameter_Or_Global
(Id : Entity_Id;
- Mode : Formal_Kind;
- Global_Var : Boolean);
+ 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.
- function Has_Ownership_Aspect_True
- (N : Node_Id;
- Msg : String)
- return Boolean;
- -- Takes a node as an input, and finds out whether it has ownership aspect
- -- True or False. This function is recursive whenever the node has a
- -- composite type. Access-to-objects have ownership aspect False if they
- -- have a general access type.
+ 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.
-
- --------------------------
- -- Check_Call_Statement --
- --------------------------
-
- procedure Check_Call_Statement (Call : Node_Id) is
- Saved_Env : Perm_Env;
-
- procedure Iterate_Call_In is new
- Iterate_Call_Parameters (Check_Param_In);
- procedure Iterate_Call_Out is new
- Iterate_Call_Parameters (Check_Param_Out);
+ Current_Borrowers : Variable_Mapping;
+ -- Mapping from borrowers to the path borrowed
- begin
- -- Save environment, so that the modifications done by analyzing the
- -- parameters are not kept at the end of the call.
-
- Copy_Env (Current_Perm_Env, Saved_Env);
-
- -- We first check the globals then parameters to handle the
- -- No_Parameter_Aliasing Restriction. An out or in-out global is
- -- considered as borrowing while a parameter with the same mode is
- -- a move. This order disallow passing a part of a variable to a
- -- subprogram if it is referenced as a global by the callable (when
- -- writable).
- -- For paremeters, we fisrt check in parameters and then the out ones.
- -- This is to avoid Observing or Borrowing objects that are already
- -- moved. This order is not mandatory but allows to catch runtime
- -- errors like null pointer dereferencement at the analysis time.
-
- Current_Checking_Mode := Read;
- Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
- Iterate_Call_In (Call);
- Iterate_Call_Out (Call);
-
- -- Restore environment, because after borrowing/observing actual
- -- parameters, they get their permission reverted to the ones before
- -- the call.
-
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
- Free_Env (Saved_Env);
- end Check_Call_Statement;
+ Current_Observers : Variable_Mapping;
+ -- Mapping from observers to the path observed
- -------------------------
- -- Check_Callable_Body --
- -------------------------
+ --------------------
+ -- Handle_Globals --
+ --------------------
- procedure Check_Callable_Body (Body_N : Node_Id) is
+ -- Generic procedure is defined first so that instantiations can be defined
+ -- anywhere afterwards.
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
- Saved_Env : Perm_Env;
- Saved_Init_Map : Initialization_Map;
- New_Env : Perm_Env;
- Body_Id : constant Entity_Id := Defining_Entity (Body_N);
- Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
+ procedure Handle_Globals (Subp : Entity_Id) is
- begin
- -- Check if SPARK pragma is not set to Off
+ -- Local subprograms
- if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
- if Get_SPARK_Mode_From_Annotation
- (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
- then
- return;
- end if;
- else
- return;
- end if;
+ procedure Handle_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind);
+ -- Handle global items from the list starting at Item
- -- Save environment and put a new one in place
+ procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id);
+ -- Handle global items for the mode Global_Mode
- Copy_Env (Current_Perm_Env, Saved_Env);
+ ------------------------------
+ -- Handle_Globals_From_List --
+ ------------------------------
- -- Save initialization map
+ procedure Handle_Globals_From_List
+ (First_Item : Node_Id;
+ Kind : Formal_Kind)
+ is
+ Item : Node_Id := First_Item;
+ E : Entity_Id;
- Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
- Current_Checking_Mode := Read;
- Current_Perm_Env := New_Env;
+ begin
+ while Present (Item) loop
+ E := Entity (Item);
- -- Add formals and globals to the environment with adequate permissions
+ -- Ignore abstract states, which play no role in pointer aliasing
- if Is_Subprogram_Or_Entry (Spec_Id) then
- Setup_Parameters (Spec_Id);
- Setup_Globals (Spec_Id);
- end if;
+ 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;
- -- Analyze the body of the function
+ Next_Global (Item);
+ end loop;
+ end Handle_Globals_From_List;
- Check_List (Declarations (Body_N));
- Check_Node (Handled_Statement_Sequence (Body_N));
+ ----------------------------
+ -- Handle_Globals_Of_Mode --
+ ----------------------------
- -- Check the read-write permissions of borrowed parameters/globals
+ procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id) is
+ Kind : Formal_Kind;
- if Ekind_In (Spec_Id, E_Procedure, E_Entry)
- and then not No_Return (Spec_Id)
- then
- Return_Globals (Spec_Id);
- end if;
+ begin
+ case Global_Mode is
+ when Name_Input
+ | Name_Proof_In
+ =>
+ Kind := E_In_Parameter;
- -- Free the environments
+ when Name_Output =>
+ Kind := E_Out_Parameter;
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
- Free_Env (Saved_Env);
+ when Name_In_Out =>
+ Kind := E_In_Out_Parameter;
- -- Restore initialization map
+ when others =>
+ raise Program_Error;
+ end case;
- Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
- Reset (Saved_Init_Map);
+ -- Check both global items from Global and Refined_Global pragmas
- -- The assignment of all out parameters will be done by caller
+ 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;
- Current_Checking_Mode := Mode_Before;
- end Check_Callable_Body;
+ -- Start of processing for Handle_Globals
- -----------------------
- -- Check_Declaration --
- -----------------------
+ 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;
- procedure Check_Declaration (Decl : Node_Id) is
+ ----------
+ -- "<=" --
+ ----------
- Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
- Target_Typ : Node_Id renames Etype (Target_Ent);
+ function "<=" (P1, P2 : Perm_Kind) return Boolean is
+ begin
+ return P2 >= P1;
+ end "<=";
- Target_View_Typ : Entity_Id;
+ ----------
+ -- ">=" --
+ ----------
- Check : Boolean := True;
+ function ">=" (P1, P2 : Perm_Kind) return Boolean is
begin
- if Present (Full_View (Target_Typ)) then
- Target_View_Typ := Full_View (Target_Typ);
- else
- Target_View_Typ := Target_Typ;
- end if;
+ case P2 is
+ when No_Access => return True;
+ when Read_Only => return P1 in Read_Perm;
+ when Write_Only => return P1 in Write_Perm;
+ when Read_Write => return P1 = Read_Write;
+ end case;
+ end ">=";
- case N_Declaration'(Nkind (Decl)) is
- when N_Full_Type_Declaration =>
- if not Has_Ownership_Aspect_True (Target_Ent, "type declaration")
- then
- Check := False;
- end if;
+ ----------------------
+ -- Check_Assignment --
+ ----------------------
- -- ??? What about component declarations with defaults.
+ procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is
- when N_Object_Declaration =>
- if (Is_Access_Type (Target_View_Typ)
- or else Is_Deep (Target_Typ))
- and then not Has_Ownership_Aspect_True
- (Target_Ent, "Object declaration ")
- then
- Check := False;
- end if;
+ -- Local subprograms
- if Is_Anonymous_Access_Type (Target_View_Typ)
- and then not Present (Expression (Decl))
- then
+ procedure Handle_Borrow
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean);
+ -- Update map of current borrowers
- -- ??? Check the case of default value (AI)
- -- ??? How an anonymous access type can be with default exp?
+ procedure Handle_Observe
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean);
+ -- Update map of current observers
- Error_Msg_NE ("? object declaration & has OAF (Anonymous "
- & "access-to-object with no initialization)",
- Decl, Target_Ent);
+ -------------------
+ -- Handle_Borrow --
+ -------------------
- -- If it it an initialization
+ procedure Handle_Borrow
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean)
+ is
+ Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
- elsif Present (Expression (Decl)) and Check then
+ 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.
- -- Find out the operation to be done on the right-hand side
+ -- ??? In fact we could be slightly more permissive in allowing even
+ -- a call to a traversal function of the right form.
- -- Initializing object, access type
+ 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;
- if Is_Access_Type (Target_View_Typ) then
+ Set (Current_Borrowers, Var, Borrowed);
+ end Handle_Borrow;
- -- Initializing object, constant access type
+ --------------------
+ -- Handle_Observe --
+ --------------------
- if Is_Constant_Object (Target_Ent) then
+ procedure Handle_Observe
+ (Var : Entity_Id;
+ Expr : Node_Id;
+ Is_Decl : Boolean)
+ is
+ Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
- -- Initializing object, constant access to variable type
+ 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.
- if not Is_Access_Constant (Target_View_Typ) then
- Current_Checking_Mode := Borrow;
+ 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;
- -- Initializing object, constant access to constant type
+ Set (Current_Observers, Var, Observed);
+ end Handle_Observe;
- -- Initializing object,
- -- constant access to constant anonymous type.
+ -- Local variables
- elsif Is_Anonymous_Access_Type (Target_View_Typ) then
+ 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;
- -- This is an object declaration so the target
- -- of the assignement is a stand-alone object.
+ -- Start of processing for Check_Assignment
- Current_Checking_Mode := Observe;
+ begin
+ Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
- -- Initializing object, constant access to constant
- -- named type.
+ if Is_Anonymous_Access_Type (Target_Typ) then
+ Check_Source_Of_Borrow_Or_Observe (Expr, Status);
- else
- -- If named then it is a general access type
- -- Hence, Has_Ownership_Aspec_True is False.
+ if Status /= OK then
+ return;
+ end if;
- raise Program_Error;
- end if;
+ if Is_Decl then
+ Target_Root := Target;
+ else
+ Target_Root := Get_Root_Object (Target);
+ end if;
- -- Initializing object, variable access type
+ Expr_Root := Get_Root_Object (Expr);
- else
- -- Initializing object, variable access to variable type
+ -- SPARK RM 3.10(7): For an assignment statement where the target is
+ -- a stand-alone object of an anonymous access-to-object type.
- if not Is_Access_Constant (Target_View_Typ) then
+ pragma Assert (Present (Target_Root));
- -- Initializing object, variable named access to
- -- variable type.
+ -- 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 not Is_Anonymous_Access_Type (Target_View_Typ) then
- Current_Checking_Mode := Move;
+ if Is_Access_Constant (Target_Typ) then
+ Perm := Get_Perm (Expr);
- -- Initializing object, variable anonymous access to
- -- variable type.
+ if Perm = No_Access then
+ Perm_Error (Expr, No_Access, No_Access,
+ Expl => Get_Expl (Expr),
+ Forbidden_Perm => True);
+ return;
+ end if;
- else
- -- This is an object declaration so the target
- -- object of the assignement is a stand-alone
- -- object.
+ Perm := Get_Perm (Expr_Root);
- Current_Checking_Mode := Borrow;
- end if;
+ if Perm = No_Access then
+ Perm_Error (Expr, No_Access, No_Access,
+ Expl => Get_Expl (Expr_Root),
+ Forbidden_Perm => True);
+ return;
+ end if;
- -- Initializing object, variable access to constant type
+ -- ??? check accessibility level
- else
- -- Initializing object,
- -- variable named access to constant type.
+ -- 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.
- if not Is_Anonymous_Access_Type (Target_View_Typ) then
- Error_Msg_N ("assignment not allowed, Ownership "
- & "Aspect False (Anonymous Access "
- & "Object)", Decl);
- Check := False;
+ Check_Expression (Expr, Observe);
+ Handle_Observe (Target_Root, Expr, Is_Decl);
- -- Initializing object,
- -- variable anonymous access to constant type.
+ else
+ Perm := Get_Perm (Expr);
- else
- -- This is an object declaration so the target
- -- of the assignement is a stand-alone object.
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- Current_Checking_Mode := Observe;
- end if;
- end if;
+ 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;
- -- Initializing object, composite (deep) type
+ 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;
- elsif Is_Deep (Target_Typ) then
+ Check_Expression (Expr, Borrow);
+ Handle_Borrow (Target_Root, Expr, Is_Decl);
+ end if;
- -- Initializing object, constant composite type
+ elsif Is_Deep (Target_Typ) then
- if Is_Constant_Object (Target_Ent) then
- Current_Checking_Mode := Observe;
+ if Is_Path_Expression (Expr) then
+ Check_Expression (Expr, Move);
- -- Initializing object, variable composite type
+ else
+ if Emit_Messages then
+ Error_Msg_N ("expression not allowed as source of move", Expr);
+ end if;
+ return;
+ end if;
- else
+ else
+ Check_Expression (Expr, Read);
+ end if;
+ end Check_Assignment;
- -- Initializing object, variable anonymous composite type
+ --------------------------
+ -- Check_Call_Statement --
+ --------------------------
- if Nkind (Object_Definition (Decl)) =
- N_Constrained_Array_Definition
+ procedure Check_Call_Statement (Call : Node_Id) is
- -- An N_Constrained_Array_Definition is an anonymous
- -- array (to be checked). Record types are always
- -- named and are considered in the else part.
+ Subp : constant Entity_Id := Get_Called_Entity (Call);
- then
- declare
- Com_Ty : constant Node_Id :=
- Component_Type (Etype (Target_Typ));
- begin
+ -- Local subprograms
- if Is_Access_Type (Com_Ty) then
+ procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Check the permission of every actual parameter
- -- If components are of anonymous type
+ procedure Update_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Update the permission of OUT actual parameters
- if Is_Anonymous_Access_Type (Com_Ty) then
- if Is_Access_Constant (Com_Ty) then
- Current_Checking_Mode := Observe;
+ -----------------
+ -- Check_Param --
+ -----------------
- else
- Current_Checking_Mode := Borrow;
- end if;
+ 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;
- else
- Current_Checking_Mode := Move;
- end if;
+ ------------------
+ -- Update_Param --
+ ------------------
- elsif Is_Deep (Com_Ty) then
+ procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is
+ Mode : constant Entity_Kind := Ekind (Formal);
- -- This is certainly named so it is a move
+ begin
+ case Formal_Kind'(Mode) is
+ when E_Out_Parameter =>
+ Check_Expression (Actual, Assign);
- Current_Checking_Mode := Move;
- end if;
- end;
+ when others =>
+ null;
+ end case;
+ end Update_Param;
- else
- Current_Checking_Mode := Move;
- end if;
- end if;
+ procedure Check_Params is new
+ Iterate_Call_Parameters (Check_Param);
- elsif Nkind_In (Expression (Decl),
- N_Attribute_Reference,
- N_Attribute_Reference,
- N_Expanded_Name,
- N_Explicit_Dereference,
- N_Indexed_Component,
- N_Reference,
- N_Selected_Component,
- N_Slice)
- then
- if Is_Access_Type (Etype (Prefix (Expression (Decl))))
- or else Is_Deep (Etype (Prefix (Expression (Decl))))
- then
- Current_Checking_Mode := Observe;
- Check := True;
- end if;
- end if;
- end if;
+ procedure Update_Params is new
+ Iterate_Call_Parameters (Update_Param);
- if Check then
- Check_Node (Expression (Decl));
- end if;
+ -- Start of processing for Check_Call_Statement
- -- If lhs is not a pointer, we still give it the appropriate
- -- state which is useless but not harmful.
+ 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;
- declare
- Elem : Perm_Tree_Access;
- Deep : constant Boolean := Is_Deep (Target_Typ);
+ Inside_Procedure_Call := False;
+ Update_Params (Call);
+ end Check_Call_Statement;
- begin
- -- Note that all declared variables are set to the unrestricted
- -- state.
- --
- -- If variables are not initialized:
- -- unrestricted to every declared object.
- -- Exp:
- -- R : Rec
- -- S : Rec := (...)
- -- R := S
- -- The assignement R := S is not allowed in the new rules
- -- if R is not unrestricted.
- --
- -- If variables are initialized:
- -- If it is a move, then the target is unrestricted
- -- If it is a borrow, then the target is unrestricted
- -- If it is an observe, then the target should be observed
-
- if Current_Checking_Mode = Observe then
- Elem := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Deep,
- Permission => Observed,
- Children_Permission => Observed));
- else
- Elem := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Deep,
- Permission => Unrestricted,
- Children_Permission => Unrestricted));
- end if;
+ -------------------------
+ -- 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);
- -- Create new tree for defining identifier
+ Saved_Env : Perm_Env;
+ Saved_Borrowers : Variable_Mapping;
+ Saved_Observers : Variable_Mapping;
- Set (Current_Perm_Env,
- Unique_Entity (Defining_Identifier (Decl)),
- Elem);
- pragma Assert (Get_First (Current_Perm_Env) /= null);
- end;
+ 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 =>
null;
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
- | N_Function_Call
- =>
- 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/...)
+ 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.
- if not Present (Entity (Expr)) then
- return;
- end if;
+ -------------------
+ -- Emit_Messages --
+ -------------------
- -- Do not analyze things that are not of object Kind
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
- if Ekind (Entity (Expr)) not in Object_Kind then
- return;
- end if;
+ -- Local variables
- -- Consider as ident
+ Target : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : constant Node_Id := Etype (Target);
+ Expr : Node_Id;
- Process_Path (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_Binary_Op =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ when N_Subtype_Declaration =>
+ null;
- -- Switch to read mode and then check the readability of each operand
+ when N_Object_Declaration =>
+ Expr := Expression (Decl);
- when N_Op_Abs
- | N_Op_Minus
- | N_Op_Not
- | N_Op_Plus
- =>
- Current_Checking_Mode := Read;
- Check_Node (Right_Opnd (Expr));
+ Check_Type_Legality (Target_Typ, Force, Legal);
- -- Forbid all deep expressions for Attribute ???
- -- What about generics? (formal parameters).
+ -- 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)).
- when N_Attribute_Reference =>
- case Attribute_Name (Expr) is
- when Name_Access =>
- Error_Msg_N ("access attribute not allowed in SPARK", Expr);
+ 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 Name_Last
- | Name_First
- =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ 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;
- when Name_Min =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ when N_Iterator_Specification =>
+ null;
- when Name_Image =>
- Check_List (Expressions (Expr));
+ when N_Loop_Parameter_Specification =>
+ null;
- when Name_Img =>
- Check_Node (Prefix (Expr));
+ -- Checking should not be called directly on these nodes
- when Name_SPARK_Mode =>
- null;
+ when N_Function_Specification
+ | N_Entry_Declaration
+ | N_Procedure_Specification
+ | N_Component_Declaration
+ =>
+ raise Program_Error;
- when Name_Value =>
- Current_Checking_Mode := Read;
- Check_Node (Prefix (Expr));
+ -- Ignored constructs for pointer checking
- when Name_Update =>
- Check_List (Expressions (Expr));
- 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_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;
+ -- The following nodes are rewritten by semantic analysis
- -- Attributes referring to types (get values from types), hence
- -- no need to check either for borrows or any loans.
+ when N_Expression_Function =>
+ raise Program_Error;
+ end case;
+ end Check_Declaration_Legality;
- when Name_Base
- | Name_Val
- =>
- null;
- -- Other attributes that fall out of the scope of the analysis
+ ----------------------
+ -- Check_Expression --
+ ----------------------
- when others =>
- null;
- end case;
+ procedure Check_Expression
+ (Expr : Node_Id;
+ Mode : Extended_Checking_Mode)
+ is
+ -- Local subprograms
- when N_In =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ function Is_Type_Name (Expr : Node_Id) return Boolean;
+ -- Detect when a path expression is in fact a type name
- when N_Not_In =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ 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.
- -- Switch to read mode and then check the readability of each operand
+ procedure Move_Expression_List (L : List_Id);
+ -- Call Move_Expression on every expression in the list L
- when N_And_Then
- | N_Or_Else
- =>
- Current_Checking_Mode := Read;
- Check_Node (Left_Opnd (Expr));
- Check_Node (Right_Opnd (Expr));
+ 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.
- -- Check the arguments of the call
+ procedure Read_Expression_List (L : List_Id);
+ -- Call Read_Expression on every expression in the list L
- when N_Explicit_Dereference =>
- Process_Path (Expr);
+ 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.
- -- Copy environment, run on each branch, and then merge
+ ------------------
+ -- Is_Type_Name --
+ ------------------
- when N_If_Expression =>
- declare
- Saved_Env : Perm_Env;
+ 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;
- -- Accumulator for the different branches
+ ---------------------
+ -- Move_Expression --
+ ---------------------
- New_Env : Perm_Env;
- Elmt : Node_Id := First (Expressions (Expr));
+ -- Distinguish the case where the argument is a path expression that
+ -- needs explicit moving.
- begin
- Current_Checking_Mode := Read;
- Check_Node (Elmt);
- Current_Checking_Mode := Mode_Before;
+ 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;
- -- Save environment
+ --------------------------
+ -- Move_Expression_List --
+ --------------------------
- Copy_Env (Current_Perm_Env, Saved_Env);
+ 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;
- -- Here we have the original env in saved, current with a fresh
- -- copy, and new aliased.
+ ---------------------
+ -- Read_Expression --
+ ---------------------
- -- THEN PART
+ procedure Read_Expression (Expr : Node_Id) is
+ begin
+ Check_Expression (Expr, Read);
+ end Read_Expression;
- Next (Elmt);
- Check_Node (Elmt);
+ --------------------------
+ -- Read_Expression_List --
+ --------------------------
- -- Here the new_environment contains curr env after then block
+ 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;
- -- ELSE part
- -- Restore environment before if
- Copy_Env (Current_Perm_Env, New_Env);
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
+ ------------------
+ -- Read_Indexes --
+ ------------------
- -- Here new environment contains the environment after then and
- -- current the fresh copy of old one.
+ procedure Read_Indexes (Expr : Node_Id) is
- Next (Elmt);
- Check_Node (Elmt);
+ -- Local subprograms
- -- CLEANUP
+ function Is_Singleton_Choice (Choices : List_Id) return Boolean;
+ -- Return whether Choices is a singleton choice
- Copy_Env (New_Env, Current_Perm_Env);
- Free_Env (New_Env);
- Free_Env (Saved_Env);
- end;
+ procedure Read_Param (Formal : Entity_Id; Actual : Node_Id);
+ -- Call Read_Expression on the actual
- when N_Indexed_Component =>
- Process_Path (Expr);
+ -------------------------
+ -- Is_Singleton_Choice --
+ -------------------------
- -- Analyze the expression that is getting qualified
+ 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;
- when N_Qualified_Expression =>
- Check_Node (Expression (Expr));
+ procedure Read_Params is new Iterate_Call_Parameters (Read_Param);
- when N_Quantified_Expression =>
- declare
- Saved_Env : Perm_Env;
+ -- Start of processing for Read_Indexes
- begin
- Copy_Env (Current_Perm_Env, Saved_Env);
- Current_Checking_Mode := Read;
- Check_Node (Iterator_Specification (Expr));
- Check_Node (Loop_Parameter_Specification (Expr));
+ 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;
- Check_Node (Condition (Expr));
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
- Free_Env (Saved_Env);
- end;
- -- Analyze the list of associations in the aggregate
+ case N_Subexpr'(Nkind (Expr)) is
+ when N_Identifier
+ | N_Expanded_Name
+ | N_Null
+ =>
+ null;
- when N_Aggregate =>
- Check_List (Expressions (Expr));
- Check_List (Component_Associations (Expr));
+ when N_Explicit_Dereference
+ | N_Selected_Component
+ =>
+ Read_Indexes (Prefix (Expr));
- when N_Allocator =>
- Check_Node (Expression (Expr));
+ when N_Indexed_Component =>
+ Read_Indexes (Prefix (Expr));
+ Read_Expression_List (Expressions (Expr));
- when N_Case_Expression =>
- declare
- Saved_Env : Perm_Env;
+ when N_Slice =>
+ Read_Indexes (Prefix (Expr));
+ Read_Expression (Discrete_Range (Expr));
- -- Accumulator for the different branches
+ -- The argument of an allocator is moved as part of the implicit
+ -- assignment.
- New_Env : Perm_Env;
- Elmt : Node_Id := First (Alternatives (Expr));
+ when N_Allocator =>
+ Move_Expression (Expression (Expr));
- begin
- Current_Checking_Mode := Read;
- Check_Node (Expression (Expr));
- Current_Checking_Mode := Mode_Before;
+ 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;
- -- Save environment
+ when N_Op_Concat =>
+ Read_Expression (Left_Opnd (Expr));
+ Read_Expression (Right_Opnd (Expr));
- Copy_Env (Current_Perm_Env, Saved_Env);
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ Read_Indexes (Expression (Expr));
- -- Here we have the original env in saved, current with a fresh
- -- copy, and new aliased.
+ when N_Aggregate =>
+ declare
+ Assocs : constant List_Id := Component_Associations (Expr);
+ CL : List_Id;
+ Assoc : Node_Id := Nlists.First (Assocs);
+ Choice : Node_Id;
- -- First alternative
+ begin
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments. Handle the positional
+ -- components first.
- Check_Node (Elmt);
- Next (Elmt);
- Copy_Env (Current_Perm_Env, New_Env);
- Free_Env (Current_Perm_Env);
+ Move_Expression_List (Expressions (Expr));
- -- Other alternatives
+ -- Handle the named components next
- while Present (Elmt) loop
+ while Present (Assoc) loop
+ CL := Choices (Assoc);
- -- Restore environment
+ -- For an array aggregate, we should also check that the
+ -- expressions used in choices are readable.
- Copy_Env (Saved_Env, Current_Perm_Env);
- Check_Node (Elmt);
- Next (Elmt);
- end loop;
- -- CLEANUP
+ 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;
- Copy_Env (Saved_Env, Current_Perm_Env);
- Free_Env (New_Env);
- Free_Env (Saved_Env);
- end;
- -- Analyze the list of associates in the aggregate as well as the
- -- ancestor part.
+ -- There can be only one element for a value of deep type
+ -- in order to avoid aliasing.
- when N_Extension_Aggregate =>
- Check_Node (Ancestor_Part (Expr));
- Check_List (Expressions (Expr));
+ 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_Range =>
- Check_Node (Low_Bound (Expr));
- Check_Node (High_Bound (Expr));
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments.
- -- We arrived at a path. Process it.
+ if not Box_Present (Assoc) then
+ Move_Expression (Expression (Assoc));
+ end if;
- when N_Selected_Component =>
- Process_Path (Expr);
+ Next (Assoc);
+ end loop;
+ end;
- when N_Slice =>
- Process_Path (Expr);
+ 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);
- when N_Type_Conversion =>
- Check_Node (Expression (Expr));
+ begin
+ Move_Expression (Ancestor_Part (Expr));
- when N_Unchecked_Type_Conversion =>
- Check_Node (Expression (Expr));
+ -- No positional components allowed at this stage
- -- Checking should not be called directly on these nodes
+ if Present (Exprs) then
+ raise Program_Error;
+ end if;
- when N_Target_Name =>
- raise Program_Error;
+ while Present (Assoc) loop
+ CL := Choices (Assoc);
- -- Unsupported constructs in SPARK
+ -- Only singleton components allowed at this stage
- when N_Delta_Aggregate =>
- Error_Msg_N ("unsupported construct in SPARK", Expr);
+ if not Is_Singleton_Choice (CL) then
+ raise Program_Error;
+ end if;
- -- Ignored constructs for pointer checking
+ -- The subexpressions of an aggregate are moved as part
+ -- of the implicit assignments.
- when N_Character_Literal
- | N_Null
- | N_Numeric_Or_String_Literal
- | N_Operator_Symbol
- | N_Raise_Expression
- | N_Raise_xxx_Error
- =>
- null;
- -- The following nodes are never generated in GNATprove mode
+ if not Box_Present (Assoc) then
+ Move_Expression (Expression (Assoc));
+ end if;
- when N_Expression_With_Actions
- | N_Reference
- | N_Unchecked_Expression
- =>
- raise Program_Error;
- end case;
- end Check_Expression;
+ Next (Assoc);
+ end loop;
+ end;
- -------------------
- -- Check_Globals --
- -------------------
+ 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_Case_Expression =>
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+
+ begin
+ Read_Expression (Expression (Expr));
+
+ while Present (Cur_Case) loop
+ Read_Indexes (Expression (Cur_Case));
+ Next (Cur_Case);
+ end loop;
+ end;
+
+ 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 others =>
+ raise Program_Error;
+ end case;
+ end Read_Indexes;
+
+ -- Start of processing for Check_Expression
- procedure Check_Globals (N : Node_Id) is
begin
- if Nkind (N) = N_Empty then
+ if Is_Type_Name (Expr) then
+ return;
+
+ elsif Is_Path_Expression (Expr) then
+ if Mode /= Assign then
+ Read_Indexes (Expr);
+ end if;
+
+ if Mode /= Read_Subexpr then
+ Process_Path (Expr, Mode);
+ 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);
- Row : Node_Id;
- The_Mode : Name_Id;
- RHS : Node_Id;
-
- procedure Process (Mode : Name_Id; The_Global : Entity_Id);
- procedure Process (Mode : Name_Id; The_Global : Node_Id) is
- Ident_Elt : constant Entity_Id :=
- Unique_Entity (Entity (The_Global));
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
+ -- Expressions that are not path expressions should only be analyzed in
+ -- Read mode.
- begin
- if Ekind (Ident_Elt) = E_Abstract_State then
- return;
- end if;
- case Mode is
- when Name_Input
- | Name_Proof_In
- =>
- Current_Checking_Mode := Observe;
- Check_Node (The_Global);
+ if Mode /= Read then
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+ end if;
+ return;
+ end if;
- when Name_Output
- | Name_In_Out
- =>
- -- ??? Borrow not Move?
- Current_Checking_Mode := Borrow;
- Check_Node (The_Global);
+ -- Special handling for nodes that may contain evaluated expressions in
+ -- the form of constraints.
- when others =>
- raise Program_Error;
- end case;
- Current_Checking_Mode := Mode_Before;
- end Process;
+ 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));
- begin
- if Nkind (Expression (PAA)) = N_Null then
+ when others =>
+ Read_Expression (Assn);
+ end case;
- -- global => null
- -- No globals, nothing to do
+ Next (Assn);
+ end loop;
+ end;
+ return;
+ when N_Range_Constraint =>
+ Read_Expression (Range_Expression (Expr));
return;
- elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
+ when N_Subtype_Indication =>
+ if Present (Constraint (Expr)) then
+ Read_Expression (Constraint (Expr));
+ end if;
+ return;
- -- global => foo
- -- A single input
+ when N_Digits_Constraint =>
+ Read_Expression (Digits_Expression (Expr));
+ if Present (Range_Constraint (Expr)) then
+ Read_Expression (Range_Constraint (Expr));
+ end if;
+ return;
- Process (Name_Input, Expression (PAA));
+ when N_Delta_Constraint =>
+ Read_Expression (Delta_Expression (Expr));
+ if Present (Range_Constraint (Expr)) then
+ Read_Expression (Range_Constraint (Expr));
+ end if;
+ return;
- 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
+ when others =>
+ null;
+ end case;
+
+ -- At this point Expr can only be a subexpression
+
+ case N_Subexpr'(Nkind (Expr)) is
+
+ when N_Binary_Op
+ | N_Short_Circuit
+ =>
+ Read_Expression (Left_Opnd (Expr));
+ Read_Expression (Right_Opnd (Expr));
+
+ 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);
+
+ begin
+ while Present (Cur_Case) loop
+ Read_Expression (Cur_Case);
+ Next (Cur_Case);
+ end loop;
+ end;
+ end if;
+
+ when N_Unary_Op =>
+ Read_Expression (Right_Opnd (Expr));
+
+ 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);
+
+ 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
=>
- Process (Name_Input, RHS);
+ 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 N_Numeric_Or_String_Literal =>
- Process (Name_Input, Original_Node (RHS));
+ -- 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.
- when others =>
+ when Attribute_Image
+ | Attribute_Img
+ =>
+ if No (Args) then
+ Read_Expression (Pref);
+ else
+ Read_Expression_List (Args);
+ end if;
+
+ -- Attribute Update takes expressions as both prefix and
+ -- arguments, so both need to be read.
+
+ when Attribute_Update =>
+ Read_Expression (Pref);
+ Read_Expression_List (Args);
+
+ -- Attribute Modulus does not reference the evaluated
+ -- expression, so it can be ignored for this analysis.
+
+ when Attribute_Modulus =>
+ null;
+
+ -- The following attributes apply to types; there are no
+ -- expressions to read.
+
+ when Attribute_Class
+ | Attribute_Storage_Size
+ =>
+ null;
+
+ -- Postconditions should not be analyzed
+
+ when Attribute_Old
+ | Attribute_Result
+ =>
raise Program_Error;
+
+ when others =>
+ null;
end case;
- RHS := Next (RHS);
- end loop;
+ end;
- 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
+ when N_Range =>
+ Read_Expression (Low_Bound (Expr));
+ Read_Expression (High_Bound (Expr));
+
+ when N_If_Expression =>
+ Read_Expression_List (Expressions (Expr));
+ when N_Case_Expression =>
declare
- CA : constant List_Id :=
- Component_Associations (Expression (PAA));
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
+
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;
+ while Present (Cur_Case) loop
+ Read_Expression (Expression (Cur_Case));
+ Next (Cur_Case);
+ end loop;
+
+ Read_Expression (Expression (Expr));
+ end;
- when N_Identifier
- | N_Expanded_Name
- =>
- Process (The_Mode, RHS);
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ Read_Expression (Expression (Expr));
- when N_Null =>
- null;
+ 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;
- when N_Numeric_Or_String_Literal =>
- Process (The_Mode, Original_Node (RHS));
+ 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;
- when others =>
- raise Program_Error;
- end case;
- Row := Next (Row);
- end loop;
+ Read_Expression (Condition (Expr));
end;
- else
+ when N_Character_Literal
+ | N_Numeric_Or_String_Literal
+ | N_Operator_Symbol
+ | N_Raise_Expression
+ | N_Raise_xxx_Error
+ =>
+ null;
+
+ when N_Delta_Aggregate
+ | N_Target_Name
+ =>
+ null;
+
+ -- Procedure calls are handled in Check_Node
+
+ when N_Procedure_Call_Statement =>
raise Program_Error;
- end if;
- end;
- end Check_Globals;
+
+ -- Path expressions are handled before this point
+
+ 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;
+
+ -- The following nodes are never generated in GNATprove mode
+
+ when N_Expression_With_Actions
+ | N_Reference
+ | N_Unchecked_Expression
+ =>
+ raise Program_Error;
+ end case;
+ end Check_Expression;
----------------
-- Check_List --
-- Check_Loop_Statement --
--------------------------
- procedure Check_Loop_Statement (Loop_N : Node_Id) is
+ procedure Check_Loop_Statement (Stmt : Node_Id) is
+
+ -- Local Subprograms
+
+ procedure Check_Is_Less_Restrictive_Env
+ (Exiting_Env : Perm_Env;
+ Entry_Env : Perm_Env);
+ -- This procedure checks that the Exiting_Env environment is less
+ -- restrictive than the Entry_Env environment.
+
+ procedure Check_Is_Less_Restrictive_Tree
+ (New_Tree : Perm_Tree_Access;
+ Orig_Tree : Perm_Tree_Access;
+ E : Entity_Id);
+ -- Auxiliary procedure to check that the tree New_Tree is less
+ -- restrictive than the tree Orig_Tree for the entity E.
+
+ procedure Perm_Error_Loop_Exit
+ (E : Entity_Id;
+ Loop_Id : Node_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind;
+ 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
+ -- an appropriate error message.
+
+ -----------------------------------
+ -- Check_Is_Less_Restrictive_Env --
+ -----------------------------------
+
+ procedure Check_Is_Less_Restrictive_Env
+ (Exiting_Env : Perm_Env;
+ Entry_Env : Perm_Env)
+ is
+ Comp_Entry : Perm_Tree_Maps.Key_Option;
+ Iter_Entry, Iter_Exit : Perm_Tree_Access;
- -- Local variables
+ begin
+ Comp_Entry := Get_First_Key (Entry_Env);
+ while Comp_Entry.Present loop
+ Iter_Entry := Get (Entry_Env, Comp_Entry.K);
+ pragma Assert (Iter_Entry /= null);
+ Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
+ pragma Assert (Iter_Exit /= null);
+ Check_Is_Less_Restrictive_Tree
+ (New_Tree => Iter_Exit,
+ Orig_Tree => Iter_Entry,
+ E => Comp_Entry.K);
+ Comp_Entry := Get_Next_Key (Entry_Env);
+ end loop;
+ end Check_Is_Less_Restrictive_Env;
- Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
- Loop_Env : constant Perm_Env_Access := new Perm_Env;
+ ------------------------------------
+ -- Check_Is_Less_Restrictive_Tree --
+ ------------------------------------
- begin
- -- Save environment prior to the loop
+ procedure Check_Is_Less_Restrictive_Tree
+ (New_Tree : Perm_Tree_Access;
+ Orig_Tree : Perm_Tree_Access;
+ E : Entity_Id)
+ is
+ -- Local subprograms
+
+ procedure Check_Is_Less_Restrictive_Tree_Than
+ (Tree : Perm_Tree_Access;
+ Perm : Perm_Kind;
+ E : Entity_Id);
+ -- Auxiliary procedure to check that the tree N is less restrictive
+ -- than the given permission P.
+
+ procedure Check_Is_More_Restrictive_Tree_Than
+ (Tree : Perm_Tree_Access;
+ Perm : Perm_Kind;
+ E : Entity_Id);
+ -- Auxiliary procedure to check that the tree N is more restrictive
+ -- than the given permission P.
+
+ -----------------------------------------
+ -- Check_Is_Less_Restrictive_Tree_Than --
+ -----------------------------------------
+
+ procedure Check_Is_Less_Restrictive_Tree_Than
+ (Tree : Perm_Tree_Access;
+ Perm : Perm_Kind;
+ E : Entity_Id)
+ is
+ begin
+ if not (Permission (Tree) >= Perm) then
+ Perm_Error_Loop_Exit
+ (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
+ end if;
- Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
+ case Kind (Tree) is
+ when Entire_Object =>
+ if not (Children_Permission (Tree) >= Perm) then
+ Perm_Error_Loop_Exit
+ (E, Stmt, Children_Permission (Tree), Perm,
+ Explanation (Tree));
- -- Add saved environment to loop environment
+ end if;
- Set (Current_Loops_Envs, Loop_Name, Loop_Env);
+ when Reference =>
+ Check_Is_Less_Restrictive_Tree_Than
+ (Get_All (Tree), Perm, E);
- -- If the loop is not a plain-loop, then it may either never be entered,
- -- or it may be exited after a number of iterations. Hence add the
- -- current permission environment as the initial loop exit environment.
- -- Otherwise, the loop exit environment remains empty until it is
- -- populated by analyzing exit statements.
+ when Array_Component =>
+ Check_Is_Less_Restrictive_Tree_Than
+ (Get_Elem (Tree), Perm, E);
- if Present (Iteration_Scheme (Loop_N)) then
- declare
- Exit_Env : constant Perm_Env_Access := new Perm_Env;
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ begin
+ Comp := Perm_Tree_Maps.Get_First (Component (Tree));
+ while Comp /= null loop
+ Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
+ Comp :=
+ Perm_Tree_Maps.Get_Next (Component (Tree));
+ end loop;
+ end;
+ end case;
+ end Check_Is_Less_Restrictive_Tree_Than;
+
+ -----------------------------------------
+ -- Check_Is_More_Restrictive_Tree_Than --
+ -----------------------------------------
+ procedure Check_Is_More_Restrictive_Tree_Than
+ (Tree : Perm_Tree_Access;
+ Perm : Perm_Kind;
+ E : Entity_Id)
+ is
begin
- Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
- Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
- end;
- end if;
+ if not (Perm >= Permission (Tree)) then
+ Perm_Error_Loop_Exit
+ (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
+ end if;
- -- Analyze loop
+ case Kind (Tree) is
+ when Entire_Object =>
+ if not (Perm >= Children_Permission (Tree)) then
+ Perm_Error_Loop_Exit
+ (E, Stmt, Children_Permission (Tree), Perm,
+ Explanation (Tree));
+ end if;
- Check_Node (Iteration_Scheme (Loop_N));
- Check_List (Statements (Loop_N));
+ when Reference =>
+ Check_Is_More_Restrictive_Tree_Than
+ (Get_All (Tree), Perm, E);
- -- Set environment to the one for exiting the loop
+ when Array_Component =>
+ Check_Is_More_Restrictive_Tree_Than
+ (Get_Elem (Tree), Perm, E);
- declare
- Exit_Env : constant Perm_Env_Access :=
- Get (Current_Loops_Accumulators, Loop_Name);
- begin
- Free_Env (Current_Perm_Env);
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ begin
+ Comp := Perm_Tree_Maps.Get_First (Component (Tree));
+ while Comp /= null loop
+ Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
+ Comp :=
+ Perm_Tree_Maps.Get_Next (Component (Tree));
+ end loop;
+ end;
+ end case;
+ end Check_Is_More_Restrictive_Tree_Than;
- -- In the normal case, Exit_Env is not null and we use it. In the
- -- degraded case of a plain-loop without exit statements, Exit_Env is
- -- null, and we use the initial permission environment at the start
- -- of the loop to continue analysis. Any environment would be fine
- -- here, since the code after the loop is dead code, but this way we
- -- avoid spurious errors by having at least variables in scope inside
- -- the environment.
+ -- Start of processing for Check_Is_Less_Restrictive_Tree
- 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);
+ begin
+ if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
+ Perm_Error_Loop_Exit
+ (E => E,
+ Loop_Id => Stmt,
+ Perm => Permission (New_Tree),
+ Found_Perm => Permission (Orig_Tree),
+ Expl => Explanation (New_Tree));
end if;
- end;
- end Check_Loop_Statement;
- ----------------
- -- Check_Node --
- ----------------
+ case Kind (New_Tree) is
- 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);
+ -- Potentially folded tree. We check the other tree Orig_Tree to
+ -- check whether it is folded or not. If folded we just compare
+ -- their Permission and Children_Permission, if not, then we
+ -- look at the Children_Permission of the folded tree against
+ -- the unfolded tree Orig_Tree.
- when N_Subexpr =>
- Check_Expression (N);
+ when Entire_Object =>
+ case Kind (Orig_Tree) is
+ when Entire_Object =>
+ if not (Children_Permission (New_Tree) <=
+ Children_Permission (Orig_Tree))
+ then
+ Perm_Error_Loop_Exit
+ (E, Stmt,
+ Children_Permission (New_Tree),
+ Children_Permission (Orig_Tree),
+ Explanation (New_Tree));
+ end if;
- when N_Subtype_Indication =>
- Check_Node (Constraint (N));
+ when Reference =>
+ Check_Is_More_Restrictive_Tree_Than
+ (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
- when N_Body_Stub =>
- Check_Node (Get_Body_From_Stub (N));
+ when Array_Component =>
+ Check_Is_More_Restrictive_Tree_Than
+ (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
- when N_Statement_Other_Than_Procedure_Call =>
- Check_Statement (N);
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ begin
+ Comp := Perm_Tree_Maps.Get_First
+ (Component (Orig_Tree));
+ while Comp /= null loop
+ Check_Is_More_Restrictive_Tree_Than
+ (Comp, Children_Permission (New_Tree), E);
+ Comp := Perm_Tree_Maps.Get_Next
+ (Component (Orig_Tree));
+ end loop;
+ end;
+ end case;
- when N_Package_Body =>
- Check_Package_Body (N);
+ when Reference =>
+ case Kind (Orig_Tree) is
+ when Entire_Object =>
+ Check_Is_Less_Restrictive_Tree_Than
+ (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
- when N_Subprogram_Body
- | N_Entry_Body
- | N_Task_Body
- =>
- Check_Callable_Body (N);
+ when Reference =>
+ Check_Is_Less_Restrictive_Tree
+ (Get_All (New_Tree), Get_All (Orig_Tree), E);
- when N_Protected_Body =>
- Check_List (Declarations (N));
+ when others =>
+ raise Program_Error;
+ end case;
- when N_Package_Declaration =>
+ when Array_Component =>
+ case Kind (Orig_Tree) is
+ when Entire_Object =>
+ Check_Is_Less_Restrictive_Tree_Than
+ (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
+
+ when Array_Component =>
+ Check_Is_Less_Restrictive_Tree
+ (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ when Record_Component =>
+ declare
+ CompN : Perm_Tree_Access;
+ begin
+ CompN :=
+ Perm_Tree_Maps.Get_First (Component (New_Tree));
+ case Kind (Orig_Tree) is
+ when Entire_Object =>
+ while CompN /= null loop
+ Check_Is_Less_Restrictive_Tree_Than
+ (CompN, Children_Permission (Orig_Tree), E);
+
+ CompN :=
+ Perm_Tree_Maps.Get_Next (Component (New_Tree));
+ end loop;
+
+ when Record_Component =>
+ declare
+
+ KeyO : Perm_Tree_Maps.Key_Option;
+ CompO : Perm_Tree_Access;
+ begin
+ KeyO := Perm_Tree_Maps.Get_First_Key
+ (Component (Orig_Tree));
+ while KeyO.Present loop
+ 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));
+ end loop;
+ end;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end;
+ end case;
+ end Check_Is_Less_Restrictive_Tree;
+
+ --------------------------
+ -- Perm_Error_Loop_Exit --
+ --------------------------
+
+ procedure Perm_Error_Loop_Exit
+ (E : Entity_Id;
+ Loop_Id : Node_Id;
+ Perm : Perm_Kind;
+ Found_Perm : Perm_Kind;
+ Expl : Node_Id)
+ is
+ begin
+ 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 (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
+
+ Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
+
+ -- Add saved environment to loop environment
+
+ Set (Current_Loops_Envs, Loop_Name, Loop_Env);
+
+ -- If the loop is not a plain-loop, then it may either never be entered,
+ -- or it may be exited after a number of iterations. Hence add the
+ -- current permission environment as the initial loop exit environment.
+ -- Otherwise, the loop exit environment remains empty until it is
+ -- populated by analyzing exit statements.
+
+ if Present (Iteration_Scheme (Stmt)) then
+ declare
+ Exit_Env : constant Perm_Env_Access := new Perm_Env;
+
+ begin
+ Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
+ Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
+ end;
+ end if;
+
+ -- Analyze loop
+
+ 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
- Spec : constant Node_Id := Specification (N);
+ 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
+
+ Check_Is_Less_Restrictive_Env
+ (Exiting_Env => Current_Perm_Env,
+ Entry_Env => Loop_Env.all);
+
+ -- Set environment to the one for exiting the loop
+
+ declare
+ Exit_Env : constant Perm_Env_Access :=
+ Get (Current_Loops_Accumulators, Loop_Name);
+ begin
+ Free_Env (Current_Perm_Env);
+
+ -- In the normal case, Exit_Env is not null and we use it. In the
+ -- degraded case of a plain-loop without exit statements, Exit_Env is
+ -- null, and we use the initial permission environment at the start
+ -- of the loop to continue analysis. Any environment would be fine
+ -- here, since the code after the loop is dead code, but this way we
+ -- avoid spurious errors by having at least variables in scope inside
+ -- the environment.
+
+ if Exit_Env /= null then
+ Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
+ 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;
+ end;
+ end Check_Loop_Statement;
+
+ ----------------
+ -- Check_Node --
+ ----------------
+
+ procedure Check_Node (N : Node_Id) is
+ procedure Check_Subprogram_Contract (N : Node_Id);
+ -- Check the postcondition-like contracts for use of 'Old
+
+ -------------------------------
+ -- Check_Subprogram_Contract --
+ -------------------------------
+
+ 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
- Current_Checking_Mode := Read;
- Check_List (Visible_Declarations (Spec));
- Check_List (Private_Declarations (Spec));
+ Check_Old_Loop_Entry (Post);
+ Check_Old_Loop_Entry (Cases);
+ end;
- Return_Declarations (Visible_Declarations (Spec));
- Return_Declarations (Private_Declarations (Spec));
+ 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;
- 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));
+ -- Start of processing for Check_Node
- when N_Component_Association =>
- Check_Node (Expression (N));
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration (N);
- when N_Handled_Sequence_Of_Statements =>
- Check_List (Statements (N));
+ when N_Body_Stub =>
+ Check_Node (Get_Body_From_Stub (N));
- when N_Parameter_Association =>
- Check_Node (Explicit_Actual_Parameter (N));
+ when N_Statement_Other_Than_Procedure_Call =>
+ Check_Statement (N);
- when N_Range_Constraint =>
- Check_Node (Range_Expression (N));
+ when N_Procedure_Call_Statement =>
+ Check_Call_Statement (N);
- when N_Index_Or_Discriminant_Constraint =>
- Check_List (Constraints (N));
+ when N_Package_Body =>
+ if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
+ Check_Package_Body (N);
+ end if;
- -- Checking should not be called directly on these nodes
+ 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_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_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
+ when N_Entry_Body
+ | N_Task_Body
=>
- raise Program_Error;
+ Check_Callable_Body (N);
- -- Unsupported constructs in SPARK
+ when N_Protected_Body =>
+ Check_List (Declarations (N));
+
+ when N_Package_Declaration =>
+ Check_Package_Spec (N);
+
+ when N_Handled_Sequence_Of_Statements =>
+ Check_List (Statements (N));
+
+ when N_Pragma =>
+ Check_Pragma (N);
+
+ when N_Subprogram_Declaration =>
+ Check_Subprogram_Contract (N);
+
+ -- 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_Variable_Reference_Marker
| N_Discriminant_Association
- -- ??? check whether we should do sth special for
- -- N_Discriminant_Association, or maybe raise a program error.
+ -- ??? 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
- when N_Single_Protected_Declaration
- | N_Single_Task_Declaration
- =>
+ -- Checking should not be called directly on these nodes
+
+ when others =>
raise Program_Error;
end case;
-
- Current_Checking_Mode := Mode_Before;
end Check_Node;
- ------------------------
- -- Check_Package_Body --
- ------------------------
+ --------------------------
+ -- Check_Old_Loop_Entry --
+ --------------------------
- procedure Check_Package_Body (Pack : Node_Id) is
- Saved_Env : Perm_Env;
- CorSp : Node_Id;
+ procedure Check_Old_Loop_Entry (N : Node_Id) is
- begin
- if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
- if Get_SPARK_Mode_From_Annotation
- (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
- then
- return;
- end if;
- else
- return;
- end if;
+ function Check_Attribute (N : Node_Id) return Traverse_Result;
- CorSp := Parent (Corresponding_Spec (Pack));
- while Nkind (CorSp) /= N_Package_Specification loop
- CorSp := Parent (CorSp);
- end loop;
+ ---------------------
+ -- Check_Attribute --
+ ---------------------
- Check_List (Visible_Declarations (CorSp));
+ function Check_Attribute (N : Node_Id) return Traverse_Result is
+ Attr_Id : Attribute_Id;
+ Aname : Name_Id;
+ Pref : Node_Id;
- -- Save environment
+ begin
+ if Nkind (N) = N_Attribute_Reference then
+ Attr_Id := Get_Attribute_Id (Attribute_Name (N));
+ Aname := Attribute_Name (N);
- Copy_Env (Current_Perm_Env, Saved_Env);
- Check_List (Private_Declarations (CorSp));
+ 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;
- -- Set mode to Read, and then analyze declarations and statements
+ 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;
- Current_Checking_Mode := Read;
- Check_List (Declarations (Pack));
- Check_Node (Handled_Statement_Sequence (Pack));
+ return OK;
+ end Check_Attribute;
- -- Check RW for every stateful variable (i.e. in declarations)
+ procedure Check_All is new Traverse_Proc (Check_Attribute);
- Return_Declarations (Private_Declarations (CorSp));
- Return_Declarations (Visible_Declarations (CorSp));
- Return_Declarations (Declarations (Pack));
+ -- Start of processing for Check_Old_Loop_Entry
- -- Restore previous environment (i.e. delete every nonvisible
- -- declaration) from environment.
+ begin
+ Check_All (N);
+ end Check_Old_Loop_Entry;
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
- end Check_Package_Body;
+ ------------------------
+ -- Check_Package_Body --
+ ------------------------
- --------------------
- -- Check_Param_In --
- --------------------
+ procedure Check_Package_Body (Pack : Node_Id) is
+ 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;
- procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
- Mode : constant Entity_Kind := Ekind (Formal);
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
begin
- case Formal_Kind'(Mode) is
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
+ then
+ Inside_Elaboration := True;
- -- Formal IN parameter
+ -- Save environment and put a new one in place
- when E_In_Parameter =>
+ Move_Env (Current_Perm_Env, Saved_Env);
- -- Formal IN parameter, access type
+ -- Reanalyze package spec to have its variables in the environment
- if Is_Access_Type (Etype (Formal)) then
+ Check_List (Visible_Declarations (Spec));
+ Check_List (Private_Declarations (Spec));
- -- Formal IN parameter, access to variable type
+ -- Check declarations and statements in the special mode for
+ -- elaboration.
- if not Is_Access_Constant (Etype (Formal)) then
+ Check_List (Declarations (Pack));
- -- Formal IN parameter, named/anonymous access-to-variable
- -- type.
- --
- -- In SPARK, IN access-to-variable is an observe operation
- -- for a function, and a borrow operation for a procedure.
+ if Present (Aux_Prag)
+ and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
+ then
+ Check_Node (Handled_Statement_Sequence (Pack));
+ end if;
- if Ekind (Scope (Formal)) = E_Function then
- Current_Checking_Mode := Observe;
- Check_Node (Actual);
- else
- Current_Checking_Mode := Borrow;
- Check_Node (Actual);
- end if;
+ -- Restore the saved environment and free the current one
- -- Formal IN parameter, access-to-constant type
- -- Formal IN parameter, access-to-named-constant type
+ Move_Env (Saved_Env, Current_Perm_Env);
- elsif not Is_Anonymous_Access_Type (Etype (Formal)) then
- Error_Msg_N ("assignment not allowed, Ownership Aspect"
- & " False (Named general access type)",
- Formal);
+ Inside_Elaboration := Save_In_Elab;
+ end if;
+ end Check_Package_Body;
- -- Formal IN parameter, access to anonymous constant type
+ ------------------------
+ -- Check_Package_Spec --
+ ------------------------
- else
- Current_Checking_Mode := Observe;
- Check_Node (Actual);
- end if;
+ 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;
- -- Formal IN parameter, composite type
+ begin
+ if Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
+ then
+ Inside_Elaboration := True;
- elsif Is_Deep (Etype (Formal)) then
+ -- Save environment and put a new one in place
- -- Composite formal types should be named
- -- Formal IN parameter, composite named type
+ Move_Env (Current_Perm_Env, Saved_Env);
- Current_Checking_Mode := Observe;
- Check_Node (Actual);
- end if;
+ -- Check declarations in the special mode for elaboration
- when E_Out_Parameter
- | E_In_Out_Parameter
- =>
- null;
- end case;
+ Check_List (Visible_Declarations (Spec));
- Current_Checking_Mode := Mode_Before;
- end Check_Param_In;
+ 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_Out --
- ----------------------
+ -- 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_Out (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 Formal_Kind'(Mode) is
+ Inside_Elaboration := Save_In_Elab;
+ end if;
+ end Check_Package_Spec;
- -- Formal OUT/IN OUT parameter
+ -------------------------------
+ -- Check_Parameter_Or_Global --
+ -------------------------------
- when E_Out_Parameter
- | E_In_Out_Parameter
- =>
+ 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;
- -- Formal OUT/IN OUT parameter, access type
+ begin
+ if not Global_Var
+ and then Is_Anonymous_Access_Type (Typ)
+ then
+ Check_Source_Of_Borrow_Or_Observe (Expr, Status);
- if Is_Access_Type (Etype (Formal)) then
+ if Status /= OK then
+ return;
+ end if;
+ end if;
- -- Formal OUT/IN OUT parameter, access to variable type
+ case Kind is
+ when E_In_Parameter =>
- if not Is_Access_Constant (Etype (Formal)) then
+ -- Inputs of functions have R permission only
- -- Cannot have anonymous out access parameter
- -- Formal out/in out parameter, access to named variable
- -- type.
+ if Ekind (Subp) = E_Function then
+ Mode := Read;
- Current_Checking_Mode := Move;
- Check_Node (Actual);
+ -- Input global variables have R permission only
- -- Formal out/in out parameter, access to constant type
+ elsif Global_Var then
+ Mode := Read;
- else
- Error_Msg_N ("assignment not allowed, Ownership Aspect False"
- & " (Named general access type)", Formal);
+ -- Anonymous access to constant is an observe
- end if;
+ elsif Is_Anonymous_Access_Type (Typ)
+ and then Is_Access_Constant (Typ)
+ then
+ Mode := Observe;
+
+ -- Other access types are a borrow
- -- Formal out/in out parameter, composite type
+ elsif Is_Access_Type (Typ) then
+ Mode := Borrow;
- elsif Is_Deep (Etype (Formal)) then
+ -- Deep types other than access types define an observe
- -- Composite formal types should be named
- -- Formal out/in out Parameter, Composite Named type.
+ elsif Is_Deep (Typ) then
+ Mode := Observe;
- Current_Checking_Mode := Borrow;
- Check_Node (Actual);
+ -- Otherwise the variable is read
+
+ else
+ Mode := Read;
end if;
- when E_In_Parameter =>
- null;
- end case;
+ when E_Out_Parameter =>
+ Mode := Assign;
- Current_Checking_Mode := Mode_Before;
- end Check_Param_Out;
+ when E_In_Out_Parameter =>
+ Mode := Move;
+ end case;
- -------------------------
- -- Check_Safe_Pointers --
- -------------------------
+ if Mode = Assign then
+ Check_Expression (Expr, Read_Subexpr);
+ end if;
- procedure Check_Safe_Pointers (N : Node_Id) is
+ Check_Expression (Expr, Mode);
+ end Check_Parameter_Or_Global;
- -- Local subprograms
+ procedure Check_Globals_Inst is
+ new Handle_Globals (Check_Parameter_Or_Global);
- procedure Check_List (L : List_Id);
- -- Call the main analysis procedure on each element of the list
+ procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst;
+
+ ------------------
+ -- Check_Pragma --
+ ------------------
+
+ 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;
+
+ begin
+ if Present (Arg1) then
+ Arg2 := Next (Arg1);
+ end if;
+
+ case Prag_Id is
+ when Pragma_Check =>
+ declare
+ Expr : constant Node_Id := Expression (Arg2);
+ begin
+ Check_Expression (Expr, Read);
+
+ -- Prefix of Loop_Entry should be checked inside any assertion
+ -- where it may appear.
+
+ Check_Old_Loop_Entry (Expr);
+ end;
+
+ -- Prefix of Loop_Entry should be checked inside a Loop_Variant
+
+ when Pragma_Loop_Variant =>
+ Check_Old_Loop_Entry (Prag);
+
+ -- 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_Pragma;
+
+ -------------------------
+ -- Check_Safe_Pointers --
+ -------------------------
+
+ procedure Check_Safe_Pointers (N : Node_Id) is
+
+ -- Local subprograms
+
+ procedure Check_List (L : List_Id);
+ -- Call the main analysis procedure on each element of the list
procedure Initialize;
-- Initialize global variables before starting the analysis of a body
Reset (Current_Loops_Envs);
Reset (Current_Loops_Accumulators);
Reset (Current_Perm_Env);
- Reset (Current_Initialization_Map);
end Initialize;
- -- Local variables
-
- Prag : Node_Id;
-
- -- SPARK_Mode pragma in application
-
-- Start of processing for Check_Safe_Pointers
begin
Initialize;
+
case Nkind (N) is
when N_Compilation_Unit =>
Check_Safe_Pointers (Unit (N));
when N_Package_Body
| N_Package_Declaration
+ | N_Subprogram_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
- elsif Nkind (N) = N_Package_Body then
- Check_List (Declarations (N));
+ begin
+ if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
+ null;
- elsif Nkind (N) = N_Package_Declaration then
- Check_List (Private_Declarations (Specification (N)));
- Check_List (Visible_Declarations (Specification (N)));
- end if;
+ elsif Present (Prag) then
+ if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
+ Check_Node (N);
+ end if;
+
+ elsif Nkind (N) = N_Package_Body then
+ Check_List (Declarations (N));
+
+ elsif Nkind (N) = N_Package_Declaration then
+ Check_List (Private_Declarations (Specification (N)));
+ Check_List (Visible_Declarations (Specification (N)));
+ end if;
+ end;
when others =>
null;
end case;
end Check_Safe_Pointers;
- ---------------------
- -- Check_Statement --
- ---------------------
-
- procedure Check_Statement (Stmt : Node_Id) is
- Mode_Before : constant Checking_Mode := Current_Checking_Mode;
- State_N : Perm_Kind;
- Check : Boolean := True;
- St_Name : Node_Id;
- Ty_St_Name : Node_Id;
-
- function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
- -- Return the root of the name given as input
+ ---------------------------------------
+ -- Check_Source_Of_Borrow_Or_Observe --
+ ---------------------------------------
- function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
- begin
- case Nkind (Comp_Stmt) is
- when N_Identifier
- | N_Expanded_Name
- => return Comp_Stmt;
+ procedure Check_Source_Of_Borrow_Or_Observe
+ (Expr : Node_Id;
+ Status : out Error_Status)
+ is
+ Root : Entity_Id;
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Get_Root (Expression (Comp_Stmt));
+ begin
+ if Is_Path_Expression (Expr) then
+ Root := Get_Root_Object (Expr);
+ else
+ Root := Empty;
+ end if;
- when N_Parameter_Specification =>
- return Get_Root (Defining_Identifier (Comp_Stmt));
+ 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;
- when N_Selected_Component
- | N_Indexed_Component
- | N_Slice
- | N_Explicit_Dereference
- =>
- return Get_Root (Prefix (Comp_Stmt));
+ Status := Error;
+ end if;
+ end Check_Source_Of_Borrow_Or_Observe;
- when others =>
- raise Program_Error;
- end case;
- end Get_Root;
+ ---------------------
+ -- Check_Statement --
+ ---------------------
+ procedure Check_Statement (Stmt : Node_Id) is
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 =>
+ declare
+ Target : constant Node_Id := Name (Stmt);
- St_Name := Name (Stmt);
- Ty_St_Name := Etype (Name (Stmt));
-
- -- Check that is not a *general* access type
-
- if Has_Ownership_Aspect_True (St_Name, "assigning to") then
-
- -- Assigning to access type
-
- if Is_Access_Type (Ty_St_Name) then
-
- -- Assigning to access to variable type
-
- if not Is_Access_Constant (Ty_St_Name) then
-
- -- Assigning to named access to variable type
-
- if not Is_Anonymous_Access_Type (Ty_St_Name) then
- Current_Checking_Mode := Move;
-
- -- Assigning to anonymous access to variable type
-
- else
- -- Target /= source root
-
- if Nkind_In (Expression (Stmt), N_Allocator, N_Null)
- or else Entity (St_Name) /=
- Entity (Get_Root (Expression (Stmt)))
- then
- Error_Msg_N ("assignment not allowed, anonymous "
- & "access Object with Different Root",
- Stmt);
- Check := False;
-
- -- Target = source root
-
- else
- -- Here we do nothing on the source nor on the
- -- target. However, we check the the legality rule:
- -- "The source shall be an owning access object
- -- denoted by a name that is not in the observed
- -- state".
-
- State_N := Get_Perm (Expression (Stmt));
- if State_N = Observed then
- Error_Msg_N ("assignment not allowed, Anonymous "
- & "access object with the same root"
- & " but source Observed", Stmt);
- Check := False;
- end if;
- end if;
- end if;
-
- -- else access-to-constant
-
- -- Assigning to anonymous access-to-constant type
-
- elsif Is_Anonymous_Access_Type (Ty_St_Name) then
-
- -- ??? Check the follwing condition. We may have to
- -- add that the root is in the observed state too.
-
- State_N := Get_Perm (Expression (Stmt));
- if State_N /= Observed then
- Error_Msg_N ("assignment not allowed, anonymous "
- & "access-to-constant object not in "
- & "the observed state)", Stmt);
- Check := False;
-
- else
- Error_Msg_N ("?here check accessibility level cited in"
- & " the second legality rule of assign",
- Stmt);
- Check := False;
- end if;
-
- -- Assigning to named access-to-constant type:
- -- This case should have been detected when checking
- -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
-
- else
- raise Program_Error;
- end if;
-
- -- Assigning to composite (deep) type.
-
- elsif Is_Deep (Ty_St_Name) then
- if Ekind_In (Ty_St_Name,
- E_Record_Type,
- E_Record_Subtype)
- then
- declare
- Elmt : Entity_Id :=
- First_Component_Or_Discriminant (Ty_St_Name);
-
- begin
- while Present (Elmt) loop
- if Is_Anonymous_Access_Type (Etype (Elmt)) or
- Ekind (Elmt) = E_General_Access_Type
- then
- Error_Msg_N ("assignment not allowed, Ownership "
- & "Aspect False (Components have "
- & "Ownership Aspect False)", Stmt);
- Check := False;
- exit;
- end if;
-
- Next_Component_Or_Discriminant (Elmt);
- end loop;
- end;
-
- -- Record types are always named so this is a move
-
- if Check then
- Current_Checking_Mode := Move;
- end if;
-
- elsif Ekind_In (Ty_St_Name,
- E_Array_Type,
- E_Array_Subtype)
- and then Check
- then
- Current_Checking_Mode := Move;
- end if;
-
- -- Now handle legality rules of using a borrowed, observed,
- -- or moved name as a prefix in an assignment.
-
- else
- if Nkind_In (St_Name,
- N_Attribute_Reference,
- N_Expanded_Name,
- N_Explicit_Dereference,
- N_Indexed_Component,
- N_Reference,
- N_Selected_Component,
- N_Slice)
- then
+ begin
+ -- Start with checking that the subexpressions of the target
+ -- path are readable, before possibly updating the permission
+ -- of these subexpressions in Check_Assignment.
- if Is_Access_Type (Etype (Prefix (St_Name))) or
- Is_Deep (Etype (Prefix (St_Name)))
- then
+ Check_Expression (Target, Read_Subexpr);
- -- We set the Check variable to True so that we can
- -- Check_Node of the expression and the name first
- -- under the assumption of Current_Checking_Mode =
- -- Read => nothing to be done for the RHS if the
- -- following check on the expression fails, and
- -- Current_Checking_Mode := Assign => the name should
- -- not be borrowed or observed so that we can use it
- -- as a prefix in the target of an assignement.
- --
- -- Note that we do not need to check the OA here
- -- because we are allowed to read and write "through"
- -- an object of OAF (example: traversing a DS).
-
- Check := True;
- end if;
- end if;
+ Check_Assignment (Target => Target,
+ Expr => Expression (Stmt));
- if Nkind_In (Expression (Stmt),
- N_Attribute_Reference,
- N_Expanded_Name,
- N_Explicit_Dereference,
- N_Indexed_Component,
- N_Reference,
- N_Selected_Component,
- N_Slice)
- then
+ -- ??? 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.
- if Is_Access_Type (Etype (Prefix (Expression (Stmt))))
- or else Is_Deep (Etype (Prefix (Expression (Stmt))))
- then
- Current_Checking_Mode := Observe;
- Check := True;
- end if;
+ 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;
- if Check then
- Check_Node (Expression (Stmt));
- Current_Checking_Mode := Assign;
- Check_Node (St_Name);
- end if;
- end if;
+ Check_Expression (Target, Assign);
+ end;
when N_Block_Statement =>
- declare
- Saved_Env : Perm_Env;
- begin
- -- Save environment
-
- Copy_Env (Current_Perm_Env, Saved_Env);
-
- -- Analyze declarations and Handled_Statement_Sequences
+ Check_List (Declarations (Stmt));
+ Check_Node (Handled_Statement_Sequence (Stmt));
- Current_Checking_Mode := Read;
- Check_List (Declarations (Stmt));
- Check_Node (Handled_Statement_Sequence (Stmt));
+ -- Remove local borrowers and observers
- -- Restore environment
+ 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;
- Free_Env (Current_Perm_Env);
- Copy_Env (Saved_Env, Current_Perm_Env);
+ Next (Decl);
+ end loop;
end;
when N_Case_Statement =>
declare
+ Alt : Node_Id;
Saved_Env : Perm_Env;
-
- -- Accumulator for the different branches
-
- New_Env : Perm_Env;
- Elmt : Node_Id := First (Alternatives (Stmt));
+ -- 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.
-
-- First alternative
- Check_Node (Elmt);
- Next (Elmt);
- Copy_Env (Current_Perm_Env, New_Env);
- Free_Env (Current_Perm_Env);
+ Alt := First (Alternatives (Stmt));
+ Check_List (Statements (Alt));
+ Next (Alt);
+
+ -- 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);
- Check_Node (Elmt);
- Next (Elmt);
+
+ -- Next alternative
+
+ Check_List (Statements (Alt));
+ Next (Alt);
+
+ -- Merge Current_Perm_Env into New_Env
+
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
end loop;
- Copy_Env (Saved_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));
+ Return_Typ : constant Entity_Id :=
+ Etype (Expression (Stmt));
+
begin
- Return_Globals (Subp);
- end;
+ -- 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;
- when others =>
- if Is_Deep (Etype (Expression (Stmt))) then
- Current_Checking_Mode := Move;
- else
- Check := False;
- end if;
+ -- Move expression to caller
- if Check then
- Check_Node (Expression (Stmt));
- end if;
- end case;
+ elsif Is_Deep (Return_Typ) then
+
+ if Is_Path_Expression (Expr) then
+ Check_Expression (Expr, Move);
+
+ 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 =>
- Check_List (Return_Object_Declarations (Stmt));
- Check_Node (Handled_Statement_Sequence (Stmt));
- Return_Declarations (Return_Object_Declarations (Stmt));
declare
- -- ??? This does not take into account the fact that a simple
- -- return inside an extended return statement applies to the
- -- extended return statement.
- Subp : constant Entity_Id :=
+ 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_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;
- -- Nothing to do when exiting a loop. No merge needed
+ -- On loop exit, merge the current permission environment with the
+ -- accumulator for the given loop.
when N_Exit_Statement =>
- null;
+ declare
+ Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
+ Saved_Accumulator : constant Perm_Env_Access :=
+ Get (Current_Loops_Accumulators, Loop_Name);
+ Environment_Copy : constant Perm_Env_Access :=
+ new Perm_Env;
+ begin
+ Copy_Env (Current_Perm_Env, Environment_Copy.all);
+
+ if Saved_Accumulator = null then
+ Set (Current_Loops_Accumulators,
+ Loop_Name, Environment_Copy);
+ else
+ Merge_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
+ -- 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.
-
- -- THEN PART
+ -- THEN branch
Check_List (Then_Statements (Stmt));
- Copy_Env (Current_Perm_Env, New_Env);
- Free_Env (Current_Perm_Env);
-
- -- Here the new_environment contains curr env after then block
+ Move_Env (Current_Perm_Env, New_Env);
- -- ELSIF part
+ -- ELSIF branches
declare
- Elmt : Node_Id;
-
+ Branch : Node_Id;
begin
- Elmt := First (Elsif_Parts (Stmt));
- while Present (Elmt) loop
+ Branch := First (Elsif_Parts (Stmt));
+ while Present (Branch) loop
- -- Transfer into accumulator, and restore from save
+ -- Restore current permission environment
Copy_Env (Saved_Env, Current_Perm_Env);
- Check_Node (Condition (Elmt));
- Check_List (Then_Statements (Stmt));
- Next (Elmt);
+ Check_Expression (Condition (Branch), Read);
+ Check_List (Then_Statements (Branch));
+
+ -- Merge current permission environment
+
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
+ Next (Branch);
end loop;
end;
- -- ELSE part
+ -- ELSE branch
- -- Restore environment before if
+ -- Restore current permission environment
Copy_Env (Saved_Env, Current_Perm_Env);
-
- -- Here new environment contains the environment after then and
- -- current the fresh copy of old one.
-
Check_List (Else_Statements (Stmt));
- -- CLEANUP
+ -- Merge current permission environment
- Copy_Env (Saved_Env, Current_Perm_Env);
+ Merge_Env (Source => Current_Perm_Env, Target => New_Env);
- Free_Env (New_Env);
+ -- Cleanup
+
+ 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_Selective_Accept
| N_Timed_Entry_Call
=>
- Error_Msg_N ("unsupported construct in SPARK", Stmt);
+ null;
+
+ -- The following nodes are never generated in GNATprove mode
+
+ when N_Compound_Statement
+ | N_Free_Statement
+ =>
+ raise Program_Error;
+ end case;
+ end Check_Statement;
+
+ -------------------------
+ -- 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);
+
+ -- Start of processing for Check_Type_Legality
+
+ begin
+ 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 E_Array_Type
+ | E_Array_Subtype
+ =>
+ Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
+
+ 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;
+
+ 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 Check_Type_Legality;
+
+ --------------
+ -- Get_Expl --
+ --------------
+
+ function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is
+ begin
+ -- Special case for the object declared in an extended return statement
+
+ 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;
+
+ -- The expression is a call to a traversal function
+
+ elsif Is_Traversal_Function_Call (N) then
+ return N;
+
+ -- The expression is directly rooted in an object
+
+ 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;
+
+ when Unfolded =>
+ pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+ return Explanation (Tree_Or_Perm.Tree_Access);
+ end case;
+ end;
+
+ -- The expression is a function call, an allocation, or null
+
+ else
+ return N;
+ end if;
+ end Get_Expl;
+
+ -----------------------------------
+ -- 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;
+
+ --------------
+ -- Get_Perm --
+ --------------
+
+ function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is
+ begin
+ -- Special case for the object declared in an extended return statement
+
+ 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;
+
+ -- The expression is a call to a traversal function
+
+ 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;
+
+ -- The expression is directly rooted in an object
+
+ 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 Unfolded =>
+ pragma Assert (Tree_Or_Perm.Tree_Access /= null);
+ return Permission (Tree_Or_Perm.Tree_Access);
+ end case;
+ end;
+
+ -- The expression is a function call, an allocation, or null
+
+ else
+ return Read_Write;
+ end if;
+ end Get_Perm;
+
+ ----------------------
+ -- Get_Perm_Or_Tree --
+ ----------------------
+
+ function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+ begin
+ case Nkind (N) is
+
+ 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.
+
+ if not Inside_Elaboration
+ and then C = null
+ then
+ Illegal_Global_Usage (N, N);
+ end if;
+
+ return (R => Unfolded, Tree_Access => C);
+ end;
+
+ -- 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
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ declare
+ C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
+ begin
+ case C.R is
+
+ -- Some earlier prefix was already folded, return the
+ -- permission found.
+
+ when Folded =>
+ return C;
+
+ 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;
+
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Get_Perm_Or_Tree (Expression (N));
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Perm_Or_Tree;
+
+ -------------------
+ -- Get_Perm_Tree --
+ -------------------
+
+ function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
+ begin
+ return Set_Perm_Prefixes (N, None, Empty);
+ end Get_Perm_Tree;
+
+ ---------------------
+ -- Get_Root_Object --
+ ---------------------
+
+ 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.
+
+ ---------
+ -- GRO --
+ ---------
+
+ function GRO (Expr : Node_Id) return Entity_Id is
+ begin
+ return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
+ end GRO;
+
+ 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.
+
+ -- Start of processing for Get_Root_Object
+
+ 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;
+
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ return Entity (Expr);
+
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ return GRO (Prefix (Expr));
+
+ -- There is no root object for an (extension) aggregate, allocator,
+ -- concat, or NULL.
+
+ when N_Aggregate
+ | N_Allocator
+ | N_Extension_Aggregate
+ | N_Null
+ | N_Op_Concat
+ =>
+ return Empty;
+
+ -- 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.
+
+ 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;
+
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return GRO (Expression (Expr));
+
+ 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;
+
+ 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 Empty;
+ end if;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ end if;
+
+ 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;
+
+ 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 Common_Root;
+ end;
+ else
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
+ return Empty;
+ end if;
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Root_Object;
+
+ ---------
+ -- Glb --
+ ---------
+
+ function Glb (P1, P2 : Perm_Kind) return Perm_Kind
+ is
+ begin
+ case P1 is
+ when No_Access =>
+ return No_Access;
+
+ when Read_Only =>
+ case P2 is
+ when No_Access
+ | Write_Only
+ =>
+ return No_Access;
+
+ when Read_Perm =>
+ return Read_Only;
+ end case;
+
+ when Write_Only =>
+ case P2 is
+ when No_Access
+ | Read_Only
+ =>
+ return No_Access;
+
+ when Write_Perm =>
+ return Write_Only;
+ end case;
+
+ when Read_Write =>
+ return P2;
+ end case;
+ end Glb;
+
+ -------------------------
+ -- Has_Array_Component --
+ -------------------------
+
+ function Has_Array_Component (Expr : Node_Id) return Boolean is
+ begin
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ return False;
+
+ when N_Explicit_Dereference
+ | N_Selected_Component
+ =>
+ return Has_Array_Component (Prefix (Expr));
+
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ return True;
+
+ when N_Allocator
+ | N_Null
+ | N_Function_Call
+ =>
+ return False;
+
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Has_Array_Component (Expression (Expr));
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Has_Array_Component;
+
+ --------
+ -- Hp --
+ --------
+
+ procedure Hp (P : Perm_Env) is
+ Elem : Perm_Tree_Maps.Key_Option;
+
+ begin
+ Elem := Get_First_Key (P);
+ while Elem.Present loop
+ Print_Node_Briefly (Elem.K);
+ Elem := Get_Next_Key (P);
+ end loop;
+ end Hp;
+
+ --------------------------
+ -- Illegal_Global_Usage --
+ --------------------------
+
+ procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id)
+ is
+ begin
+ 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_Deep --
+ -------------
+
+ function Is_Deep (Typ : Entity_Id) return Boolean is
+ begin
+ case Type_Kind'(Ekind (Retysp (Typ))) is
+ when Access_Kind =>
+ return True;
+
+ when E_Array_Type
+ | E_Array_Subtype
+ =>
+ return Is_Deep (Component_Type (Retysp (Typ)));
+
+ when Record_Kind =>
+ declare
+ Comp : Entity_Id;
+ begin
+ Comp := First_Component_Or_Discriminant (Retysp (Typ));
+ while Present (Comp) loop
+
+ -- Ignore components not visible in SPARK
- -- Ignored constructs for pointer checking
+ if Component_Is_Visible_In_SPARK (Comp)
+ and then Is_Deep (Etype (Comp))
+ then
+ return True;
+ end if;
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
+ end;
+ return False;
- when N_Null_Statement
- | N_Raise_Statement
+ when Scalar_Kind
+ | E_String_Literal_Subtype
+ | Protected_Kind
+ | Task_Kind
+ | Incomplete_Kind
+ | E_Exception_Type
+ | E_Subprogram_Type
=>
- null;
+ return False;
- -- The following nodes are never generated in GNATprove mode
+ -- Ignore full view of types if it is not in SPARK
- when N_Compound_Statement
- | N_Free_Statement
+ when E_Private_Type
+ | E_Private_Subtype
+ | E_Limited_Private_Type
+ | E_Limited_Private_Subtype
=>
- raise Program_Error;
+ return False;
end case;
- end Check_Statement;
+ end Is_Deep;
--------------
- -- Get_Perm --
+ -- Is_Legal --
--------------
- function Get_Perm (N : Node_Id) return Perm_Kind is
- Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
+ function Is_Legal (N : Node_Id) return Boolean is
+ Legal : Boolean := True;
begin
- case Tree_Or_Perm.R is
- when Folded =>
- return Tree_Or_Perm.Found_Permission;
-
- when Unfolded =>
- pragma Assert (Tree_Or_Perm.Tree_Access /= null);
- return Permission (Tree_Or_Perm.Tree_Access);
-
- -- We encoutered a function call, hence the memory area is fresh,
- -- which means that the association permission is RW.
-
- when Function_Call =>
- return Unrestricted;
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration_Legality (N, Force => False, Legal => Legal);
+ when others =>
+ null;
end case;
- end Get_Perm;
+
+ return Legal;
+ end Is_Legal;
----------------------
- -- Get_Perm_Or_Tree --
+ -- Is_Local_Context --
----------------------
- function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
+ function Is_Local_Context (Scop : Entity_Id) return Boolean is
begin
- case Nkind (N) is
+ return Is_Subprogram_Or_Entry (Scop)
+ or else Ekind (Scop) = E_Block;
+ end Is_Local_Context;
- -- Base identifier. Normally those are the roots of the trees stored
- -- in the permission environment.
-
- when N_Defining_Identifier =>
- raise Program_Error;
+ ------------------------
+ -- Is_Path_Expression --
+ ------------------------
- when N_Identifier
- | N_Expanded_Name
- =>
- declare
- P : constant Entity_Id := Entity (N);
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
+ 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.
- begin
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
+ ---------
+ -- IPE --
+ ---------
- 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.
+ function IPE (Expr : Node_Id) return Boolean is
+ begin
+ return Is_Path_Expression (Expr, Is_Traversal);
+ end IPE;
- Illegal_Global_Usage (N);
+ 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.
- else
- return (R => Unfolded, Tree_Access => C);
- end if;
- end;
+ -- Start of processing for Is_Path_Expression
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
+ begin
+ case Nkind (Expr) is
+ when N_Expanded_Name
+ | N_Explicit_Dereference
+ | N_Identifier
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
=>
- return Get_Perm_Or_Tree (Expression (N));
-
- -- Happening when we try to get the permission of a variable that
- -- is a formal parameter. We get instead the defining identifier
- -- associated with the parameter (which is the one that has been
- -- stored for indexing).
-
- when N_Parameter_Specification =>
- return Get_Perm_Or_Tree (Defining_Identifier (N));
-
- -- We get the permission tree of its prefix, and then get either the
- -- subtree associated with that specific selection, or if we have a
- -- leaf that folds its children, we take the children's permission
- -- and return it using the discriminant Folded.
-
- when N_Selected_Component =>
- declare
- C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
-
- begin
- case C.R is
- when Folded
- | Function_Call
- =>
- return C;
+ return True;
- 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));
+ -- Special value NULL corresponds to an empty path
- else
- return (R => Unfolded,
- Tree_Access => Selected_C);
- end if;
- end;
+ when N_Null =>
+ return True;
- elsif Kind (C.Tree_Access) = Entire_Object then
- return (R => Folded,
- Found_Permission =>
- Children_Permission (C.Tree_Access));
+ -- Object returned by an (extension) aggregate, an allocator, or
+ -- a function call corresponds to a path.
- else
- raise Program_Error;
- end if;
- end case;
- end;
- -- We get the permission tree of its prefix, and then get either the
- -- subtree associated with that specific selection, or if we have a
- -- leaf that folds its children, we take the children's permission
- -- and return it using the discriminant Folded.
+ when N_Aggregate
+ | N_Allocator
+ | N_Extension_Aggregate
+ | N_Function_Call
+ =>
+ return True;
- when N_Indexed_Component
- | N_Slice
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
=>
- declare
- C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
+ return IPE (Expression (Expr));
- begin
- case C.R is
- when Folded
- | Function_Call
- =>
- return C;
+ -- When returning from a traversal function, consider an
+ -- if-expression as a possible path expression.
- when Unfolded =>
- pragma Assert (C.Tree_Access /= null);
- pragma Assert (Kind (C.Tree_Access) = Entire_Object
- or else
- Kind (C.Tree_Access) = Array_Component);
+ 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;
- if Kind (C.Tree_Access) = Array_Component then
- pragma Assert (Get_Elem (C.Tree_Access) /= null);
- return (R => Unfolded,
- Tree_Access => Get_Elem (C.Tree_Access));
+ -- When returning from a traversal function, consider
+ -- a case-expression as a possible path expression.
- elsif Kind (C.Tree_Access) = Entire_Object then
- return (R => Folded, Found_Permission =>
- Children_Permission (C.Tree_Access));
+ when N_Case_Expression =>
+ if Is_Traversal then
+ declare
+ Cases : constant List_Id := Alternatives (Expr);
+ Cur_Case : Node_Id := First (Cases);
- else
- raise Program_Error;
+ begin
+ while Present (Cur_Case) loop
+ if not IPE (Expression (Cur_Case)) then
+ return False;
end if;
- end case;
- end;
- -- We get the permission tree of its prefix, and then get either the
- -- subtree associated with that specific selection, or if we have a
- -- leaf that folds its children, we take the children's permission
- -- and return it using the discriminant Folded.
-
- when N_Explicit_Dereference =>
- declare
- C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
-
- begin
- case C.R is
- when Folded
- | Function_Call
- =>
- return C;
+ Next (Cur_Case);
+ end loop;
- when Unfolded =>
- pragma Assert (C.Tree_Access /= null);
- pragma Assert (Kind (C.Tree_Access) = Entire_Object
- or else
- Kind (C.Tree_Access) = Reference);
+ return True;
+ end;
+ else
+ return False;
+ end if;
- if Kind (C.Tree_Access) = Reference then
- if Get_All (C.Tree_Access) = null then
+ when others =>
+ return False;
+ end case;
+ end Is_Path_Expression;
- -- Hash_Table_Error
+ -------------------------
+ -- Is_Prefix_Or_Almost --
+ -------------------------
- raise Program_Error;
+ function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is
- else
- return
- (R => Unfolded,
- Tree_Access => Get_All (C.Tree_Access));
- end if;
+ type Expr_Array is array (Positive range <>) of Node_Id;
+ -- Sequence of expressions that make up a path
- elsif Kind (C.Tree_Access) = Entire_Object then
- return (R => Folded, Found_Permission =>
- Children_Permission (C.Tree_Access));
+ 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
- else
- raise Program_Error;
- end if;
- end case;
- end;
- -- The name contains a function call, hence the given path is always
- -- new. We do not have to check for anything.
+ --------------------
+ -- Get_Expr_Array --
+ --------------------
- when N_Function_Call =>
- return (R => Function_Call);
+ 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 others =>
- raise Program_Error;
- end case;
- end Get_Perm_Or_Tree;
+ when N_Explicit_Dereference
+ | N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ =>
+ return Get_Expr_Array (Prefix (Expr)) & Expr;
- -------------------
- -- Get_Perm_Tree --
- -------------------
+ when N_Qualified_Expression
+ | N_Type_Conversion
+ | N_Unchecked_Type_Conversion
+ =>
+ return Get_Expr_Array (Expression (Expr));
- function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
- begin
- case Nkind (N) is
+ when others =>
+ raise Program_Error;
+ end case;
+ end Get_Expr_Array;
- -- Base identifier. Normally those are the roots of the trees stored
- -- in the permission environment.
+ -- Local variables
- when N_Defining_Identifier =>
- raise Program_Error;
+ Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref);
+ Expr_Path : constant Expr_Array := Get_Expr_Array (Expr);
- 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));
+ Prefix_Root : constant Node_Id := Prefix_Path (1);
+ Expr_Root : constant Node_Id := Expr_Path (1);
- begin
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
+ Common_Len : constant Positive :=
+ Positive'Min (Prefix_Path'Length, Expr_Path'Length);
- 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.
+ -- Start of processing for Is_Prefix_Or_Almost
- Illegal_Global_Usage (N);
+ begin
+ if Entity (Prefix_Root) /= Entity (Expr_Root) then
+ return False;
+ end if;
- else
- return C;
- end if;
- end;
+ 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_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Get_Perm_Tree (Expression (N));
+ 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_Parameter_Specification =>
- return Get_Perm_Tree (Defining_Identifier (N));
+ when N_Indexed_Component
+ | N_Slice
+ =>
+ if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then
+ return False;
+ end if;
- -- 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 others =>
+ raise Program_Error;
+ end case;
+ end;
+ end loop;
- when N_Selected_Component =>
- declare
- C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
+ -- If the expression path is longer than the prefix one, then at this
+ -- point the prefix property holds.
- begin
- if C = null then
+ if Expr_Path'Length > Prefix_Path'Length then
+ return True;
- -- If null then it means we went through a function call
+ -- Otherwise check if none of the remaining path elements in the
+ -- candidate prefix involve a dereference.
- return null;
- end if;
+ 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;
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Record_Component);
+ return True;
+ end if;
+ end Is_Prefix_Or_Almost;
- if Kind (C) = Record_Component then
+ ---------------------------
+ -- Is_Subpath_Expression --
+ ---------------------------
- -- The tree is unfolded. We just return the subtree.
+ 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
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
- Selected_C : constant Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ -- A function is said to be a traversal function if the result type of
+ -- the function is an anonymous access-to-object type,
- begin
- if Selected_C = null then
- return Other_Components (C);
- end if;
- return Selected_C;
- end;
+ and then Is_Anonymous_Access_Type (Etype (E))
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
+ -- the function has at least one formal parameter,
- Elem : Node_Id;
+ and then Present (First_Formal (E))
- -- Create the unrolled nodes
+ -- and the function's first parameter is of an access type.
- Son : Perm_Tree_Access;
+ and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
+ end Is_Traversal_Function;
- Child_Perm : constant Perm_Kind :=
- Children_Permission (C);
+ --------------------------------
+ -- Is_Traversal_Function_Call --
+ --------------------------------
- begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
+ function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is
+ begin
+ 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;
- 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));
+ ------------------
+ -- Loop_Of_Exit --
+ ------------------
- 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.
+ function Loop_Of_Exit (N : Node_Id) return Entity_Id is
+ Nam : Node_Id := Name (N);
+ Stmt : Node_Id := N;
+ begin
+ if No (Nam) then
+ while Present (Stmt) loop
+ Stmt := Parent (Stmt);
+ if Nkind (Stmt) = N_Loop_Statement then
+ Nam := Identifier (Stmt);
+ exit;
+ end if;
+ end loop;
+ end if;
+ return Entity (Nam);
+ end Loop_Of_Exit;
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
+ ---------
+ -- Lub --
+ ---------
- Selected_C : constant Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ function Lub (P1, P2 : Perm_Kind) return Perm_Kind is
+ begin
+ case P1 is
+ when No_Access =>
+ return P2;
+
+ when Read_Only =>
+ case P2 is
+ when No_Access
+ | Read_Only
+ =>
+ return Read_Only;
- 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 Write_Perm =>
+ return Read_Write;
+ end case;
- when N_Indexed_Component
- | N_Slice
- =>
- declare
- C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
+ when Write_Only =>
+ case P2 is
+ when No_Access
+ | Write_Only
+ =>
+ return Write_Only;
- begin
- if C = null then
- -- If null then we went through a function call
+ when Read_Perm =>
+ return Read_Write;
+ end case;
- return null;
- end if;
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Array_Component);
+ when Read_Write =>
+ return Read_Write;
+ end case;
+ end Lub;
- if Kind (C) = Array_Component then
+ ---------------
+ -- Merge_Env --
+ ---------------
- -- The tree is unfolded. We just return the elem subtree
+ procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is
- pragma Assert (Get_Elem (C) = null);
- return Get_Elem (C);
+ -- Local subprograms
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace node with Array_Component.
+ procedure Apply_Glb_Tree
+ (A : Perm_Tree_Access;
+ P : Perm_Kind);
- Son : Perm_Tree_Access;
+ procedure Merge_Trees
+ (Target : Perm_Tree_Access;
+ Source : 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)));
+ --------------------
+ -- Apply_Glb_Tree --
+ --------------------
- -- We change the current node from Entire_Object
- -- to Array_Component with same permission and the
- -- previously defined son.
+ procedure Apply_Glb_Tree
+ (A : Perm_Tree_Access;
+ P : Perm_Kind)
+ is
+ begin
+ A.all.Tree.Permission := Glb (Permission (A), P);
- 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.
+ case Kind (A) is
+ when Entire_Object =>
+ A.all.Tree.Children_Permission :=
+ Glb (Children_Permission (A), P);
- when N_Explicit_Dereference =>
- declare
- C : Perm_Tree_Access;
+ when Reference =>
+ Apply_Glb_Tree (Get_All (A), P);
- begin
- C := Get_Perm_Tree (Prefix (N));
+ when Array_Component =>
+ Apply_Glb_Tree (Get_Elem (A), P);
- if C = null then
+ 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;
- -- If null, we went through a function call
+ -----------------
+ -- Merge_Trees --
+ -----------------
- return null;
- end if;
+ procedure Merge_Trees
+ (Target : Perm_Tree_Access;
+ Source : Perm_Tree_Access)
+ is
+ Perm : constant Perm_Kind :=
+ Glb (Permission (Target), Permission (Source));
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Reference);
+ begin
+ pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
+ Target.all.Tree.Permission := Perm;
- if Kind (C) = Reference then
+ case Kind (Target) is
+ when Entire_Object =>
+ declare
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (Target);
- -- The tree is unfolded. We return the elem subtree
+ begin
+ case Kind (Source) is
+ when Entire_Object =>
+ Target.all.Tree.Children_Permission :=
+ Glb (Child_Perm, Children_Permission (Source));
+
+ when Reference =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ Apply_Glb_Tree (Get_All (Target), Child_Perm);
+
+ when Array_Component =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
+
+ when Record_Component =>
+ Copy_Tree (Source, Target);
+ Target.all.Tree.Permission := Perm;
+ declare
+ Comp : Perm_Tree_Access;
- if Get_All (C) = null then
+ begin
+ Comp :=
+ Perm_Tree_Maps.Get_First (Component (Target));
+ while Comp /= null loop
+ -- Apply glb tree on every component subtree
+
+ Apply_Glb_Tree (Comp, Child_Perm);
+ Comp := Perm_Tree_Maps.Get_Next
+ (Component (Target));
+ end loop;
+ end;
+ end case;
+ end;
- -- Hash_Table_Error
+ when Reference =>
+ case Kind (Source) is
+ when Entire_Object =>
+ Apply_Glb_Tree (Get_All (Target),
+ Children_Permission (Source));
- raise Program_Error;
- end if;
- return Get_All (C);
+ when Reference =>
+ Merge_Trees (Get_All (Target), Get_All (Source));
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with Reference.
+ when others =>
+ raise Program_Error;
- Son : Perm_Tree_Access;
+ end case;
- 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)));
+ when Array_Component =>
+ case Kind (Source) is
+ when Entire_Object =>
+ Apply_Glb_Tree (Get_Elem (Target),
+ Children_Permission (Source));
- -- We change the current node from Entire_Object to
- -- Reference with same permission and the previous son.
+ when Array_Component =>
+ Merge_Trees (Get_Elem (Target), Get_Elem (Source));
- pragma Assert (Is_Node_Deep (C));
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Get_All => Son);
- return Get_All (C);
- end;
- else
+ when others =>
raise Program_Error;
- end if;
- end;
- -- No permission tree for function calls
- when N_Function_Call =>
- return null;
+ end case;
- when others =>
- raise Program_Error;
- end case;
- end Get_Perm_Tree;
+ when Record_Component =>
+ case Kind (Source) is
+ when Entire_Object =>
+ declare
+ Child_Perm : constant Perm_Kind :=
+ Children_Permission (Source);
- --------
- -- Hp --
- --------
+ Comp : Perm_Tree_Access;
- procedure Hp (P : Perm_Env) is
- Elem : Perm_Tree_Maps.Key_Option;
+ begin
+ Comp := Perm_Tree_Maps.Get_First
+ (Component (Target));
+ while Comp /= null loop
+ -- Apply glb tree on every component subtree
+
+ Apply_Glb_Tree (Comp, Child_Perm);
+ Comp :=
+ Perm_Tree_Maps.Get_Next (Component (Target));
+ end loop;
+ end;
- begin
- Elem := Get_First_Key (P);
- while Elem.Present loop
- Print_Node_Briefly (Elem.K);
- Elem := Get_Next_Key (P);
- end loop;
- end Hp;
+ when Record_Component =>
+ declare
+ Key_Source : Perm_Tree_Maps.Key_Option;
+ CompTarget : Perm_Tree_Access;
+ CompSource : Perm_Tree_Access;
- --------------------------
- -- Illegal_Global_Usage --
- --------------------------
+ begin
+ Key_Source := Perm_Tree_Maps.Get_First_Key
+ (Component (Source));
- procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
- begin
- Error_Msg_NE ("cannot use global variable & of deep type", N, N);
- Error_Msg_N ("\without prior declaration in a Global aspect", N);
- Errout.Finalize (Last_Call => True);
- Errout.Output_Messages;
- Exit_Program (E_Errors);
- end Illegal_Global_Usage;
+ while Key_Source.Present loop
+ CompSource := Perm_Tree_Maps.Get
+ (Component (Source), Key_Source.K);
+ CompTarget := Perm_Tree_Maps.Get
+ (Component (Target), Key_Source.K);
- -------------
- -- Is_Deep --
- -------------
+ pragma Assert (CompSource /= null);
+ Merge_Trees (CompTarget, CompSource);
- 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;
+ Key_Source := Perm_Tree_Maps.Get_Next_Key
+ (Component (Source));
+ end loop;
+ end;
- begin
- if Is_Itype (E) then
- Decl := Associated_Node_For_Itype (E);
- else
- Decl := Parent (E);
- end if;
+ when others =>
+ raise Program_Error;
+ end case;
+ end case;
+ end Merge_Trees;
- Pack_Decl := Parent (Parent (Decl));
+ -- Local variables
- if Nkind (Pack_Decl) /= N_Package_Declaration then
- return False;
- end if;
+ CompTarget : Perm_Tree_Access;
+ CompSource : Perm_Tree_Access;
+ KeyTarget : Perm_Tree_Maps.Key_Option;
- 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;
+ -- Start of processing for Merge_Env
begin
- pragma Assert (Is_Type (E));
- case Ekind (E) is
- when Scalar_Kind =>
- return False;
-
- when Access_Kind =>
- return True;
-
- -- Just check the depth of its component type
+ KeyTarget := Get_First_Key (Target);
+ -- Iterate over every tree of the environment in the target, and merge
+ -- it with the source if there is such a similar one that exists. If
+ -- there is none, then skip.
+ while KeyTarget.Present loop
- when E_Array_Type
- | E_Array_Subtype
- =>
- return Is_Deep (Component_Type (E));
-
- when E_String_Literal_Subtype =>
- return False;
+ CompSource := Get (Source, KeyTarget.K);
+ CompTarget := Get (Target, KeyTarget.K);
- -- Per RM 8.11 for class-wide types
+ pragma Assert (CompTarget /= null);
- when E_Class_Wide_Subtype
- | E_Class_Wide_Type
- =>
- return True;
+ if CompSource /= null then
+ Merge_Trees (CompTarget, CompSource);
+ Remove (Source, KeyTarget.K);
+ end if;
- -- ??? What about hidden components
+ KeyTarget := Get_Next_Key (Target);
+ end loop;
- when E_Record_Type
- | E_Record_Subtype
- =>
- declare
- Elmt : Entity_Id;
+ -- Iterate over every tree of the environment of the source. And merge
+ -- again. If there is not any tree of the target then just copy the tree
+ -- from source to target.
+ declare
+ KeySource : Perm_Tree_Maps.Key_Option;
+ begin
+ KeySource := Get_First_Key (Source);
+ while KeySource.Present loop
- begin
- Elmt := First_Component_Or_Discriminant (E);
- while Present (Elmt) loop
- if Is_Deep (Etype (Elmt)) then
- return True;
- else
- Next_Component_Or_Discriminant (Elmt);
- end if;
- end loop;
- return False;
- end;
+ CompSource := Get (Source, KeySource.K);
+ CompTarget := Get (Target, KeySource.K);
- when Private_Kind =>
- if Is_Private_Entity_Mode_Off (E) then
- return False;
+ if CompTarget = null then
+ CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
+ Copy_Tree (CompSource, CompTarget);
+ Set (Target, KeySource.K, CompTarget);
else
- if Present (Full_View (E)) then
- return Is_Deep (Full_View (E));
- else
- return True;
- end if;
+ Merge_Trees (CompTarget, CompSource);
end if;
- when E_Incomplete_Type
- | E_Incomplete_Subtype
- =>
- return True;
-
- -- No problem with synchronized types
-
- when E_Protected_Type
- | E_Protected_Subtype
- | E_Task_Subtype
- | E_Task_Type
- =>
- return False;
-
- when E_Exception_Type =>
- return False;
+ KeySource := Get_Next_Key (Source);
+ end loop;
+ end;
- when others =>
- raise Program_Error;
- end case;
- end Is_Deep;
+ Free_Env (Source);
+ 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;
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);
- State_N : Perm_Kind;
+ procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is
+
+ procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id);
+ -- Check expression Expr originating in Root was not borrowed
+
+ procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id);
+ -- Check expression Expr originating in Root was not observed
+
+ ------------------------
+ -- Check_Not_Borrowed --
+ ------------------------
+
+ procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is
+ begin
+ -- An expression without root object cannot be borrowed
+
+ if No (Root) then
+ return;
+ end if;
+
+ -- Otherwise, try to match the expression with one of the borrowed
+ -- expressions.
+
+ declare
+ Key : Variable_Maps.Key_Option :=
+ Get_First_Key (Current_Borrowers);
+ Var : Entity_Id;
+ Borrowed : Node_Id;
+ B_Pledge : Entity_Id := Empty;
+
+ begin
+ -- Search for a call to a pledge function or a global pragma in
+ -- the parents of Expr.
+
+ 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;
+
+ Call := Parent (Call);
+ end loop;
+
+ if Present (Call)
+ and then Nkind (First_Actual (Call)) in N_Has_Entity
+ then
+ B_Pledge := Entity (First_Actual (Call));
+ end if;
+ end;
+
+ while Key.Present loop
+ Var := Key.K;
+ Borrowed := Get (Current_Borrowers, Var);
+
+ 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;
+
+ Key := Get_Next_Key (Current_Borrowers);
+ end loop;
+ end;
+ end Check_Not_Borrowed;
+
+ ------------------------
+ -- Check_Not_Observed --
+ ------------------------
+
+ procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is
+ begin
+ -- An expression without root object cannot be observed
+
+ if No (Root) then
+ return;
+ end if;
+
+ -- Otherwise, try to match the expression with one of the observed
+ -- expressions.
+
+ declare
+ Key : Variable_Maps.Key_Option :=
+ Get_First_Key (Current_Observers);
+ Var : Entity_Id;
+ Observed : Node_Id;
+
+ begin
+ while Key.Present loop
+ Var := Key.K;
+ Observed := Get (Current_Observers, Var);
+
+ 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;
+
+ Key := Get_Next_Key (Current_Observers);
+ end loop;
+ end;
+ end Check_Not_Observed;
+
+ -- Local variables
+
+ Expr_Type : constant Entity_Id := Etype (Expr);
+ Root : Entity_Id := Get_Root_Object (Expr);
+ Perm : Perm_Kind_Option;
+
+ -- Start of processing for Process_Path
+
begin
- -- We ignore if yielding to synchronized
+ -- Nothing to do if the root type is not deep, or the path is not rooted
+ -- in an object.
- if Present (Root)
- and then Is_Synchronized_Object (Root)
+ if not Present (Root)
+ or else not Is_Deep (Etype (Root))
then
return;
end if;
- State_N := Get_Perm (N);
+ -- Identify the root type for the path
- case Current_Checking_Mode is
+ Root := Unique_Entity (Root);
- -- Check permission R, do nothing
+ -- Except during elaboration, the root object should have been declared
+ -- and entered into the current permission environment.
- when Read =>
+ if not Inside_Elaboration
+ and then Get (Current_Perm_Env, Root) = null
+ then
+ Illegal_Global_Usage (Expr, Root);
+ end if;
- -- This condition should be removed when removing the read
- -- checking mode.
+ -- During elaboration, only the validity of operations is checked, no
+ -- need to compute the permission of Expr.
- return;
+ if Inside_Elaboration then
+ Perm := None;
+ else
+ Perm := Get_Perm (Expr);
+ end if;
- when Move =>
+ -- Check permissions
+
+ case Mode is
+
+ when Read =>
- -- The rhs object in an assignment statement (including copy in
- -- and copy back) should be in the Unrestricted or Moved state.
- -- Otherwise the move is not allowed.
- -- This applies to both stand-alone and composite objects.
- -- If the state of the source is Moved, then a warning message
- -- is prompt to make the user aware of reading a nullified
- -- object.
+ -- No checking needed during elaboration
- if State_N /= Unrestricted and State_N /= Moved then
- Perm_Error (N, Unrestricted, State_N);
+ if Inside_Elaboration then
return;
end if;
- -- In the AI, after moving a path nothing to do since the rhs
- -- object was in the Unrestricted state and it shall be
- -- refreshed to Unrestricted. The object should be nullified
- -- however. To avoid moving again a name that has already been
- -- moved, in this implementation we set the state of the moved
- -- object to "Moved". This shall be used to prompt a warning
- -- when manipulating a null pointer and also to implement
- -- the no aliasing parameter restriction.
-
- if State_N = Moved then
- Error_Msg_N ("?the source or one of its extensions has"
- & " already been moved", N);
+ -- Check path is readable
+
+ if Perm not in Read_Perm then
+ Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
+ return;
end if;
- declare
- -- Set state to Moved to the path and any of its prefixes
+ when Move =>
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes (N, Moved);
+ -- Forbidden on deep path during elaboration, otherwise no
+ -- checking needed.
- begin
- if Tree = null then
+ 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;
+
+ return;
+ end if;
- -- We went through a function call, no permission to
- -- modify.
+ -- For deep path, check RW permission, otherwise R permission
- return;
+ 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;
- -- Set state to Moved on any strict extension of the path
+ -- SPARK RM 3.10(1): At the point of a move operation the state of
+ -- the source object (if any) shall be Unrestricted.
- Set_Perm_Extensions (Tree, Moved);
- end;
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
when Assign =>
- -- The lhs object in an assignment statement (including copy in
- -- and copy back) should be in the Unrestricted state.
- -- Otherwise the move is not allowed.
- -- This applies to both stand-alone and composite objects.
+ -- No checking needed during elaboration
- if State_N /= Unrestricted and State_N /= Moved then
- Perm_Error (N, Unrestricted, State_N);
+ if Inside_Elaboration then
return;
end if;
- -- After assigning to a path nothing to do since it was in the
- -- Unrestricted state and it would be refreshed to
- -- Unrestricted.
+ -- For assignment, check W permission
- when Borrow =>
+ if Perm not in Write_Perm then
+ Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- -- Borrowing is only allowed on Unrestricted objects.
+ when Borrow =>
- if State_N /= Unrestricted and State_N /= Moved then
- Perm_Error (N, Unrestricted, State_N);
- end if;
+ -- Forbidden during elaboration, an error is already issued in
+ -- Check_Declaration, just return.
- if State_N = Moved then
- Error_Msg_N ("?the source or one of its extensions has"
- & " already been moved", N);
+ if Inside_Elaboration then
+ return;
end if;
- declare
- -- Set state to Borrowed to the path and any of its prefixes
-
- Tree : constant Perm_Tree_Access :=
- Set_Perm_Prefixes (N, Borrowed);
+ -- For borrowing, check RW permission
- begin
- if Tree = null then
+ if Perm /= Read_Write then
+ Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
+ return;
+ end if;
- -- We went through a function call, no permission to
- -- modify.
+ when Observe =>
- return;
- end if;
+ -- Forbidden during elaboration, an error is already issued in
+ -- Check_Declaration, just return.
- -- Set state to Borrowed on any strict extension of the path
+ if Inside_Elaboration then
+ return;
+ end if;
- Set_Perm_Extensions (Tree, Borrowed);
- end;
+ -- For borrowing, check R permission
- when Observe =>
- if State_N /= Unrestricted
- and then State_N /= Observed
- then
- Perm_Error (N, Observed, State_N);
+ if Perm not in Read_Perm then
+ Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
+ return;
end if;
+ end case;
- declare
- -- Set permission to Observed on the path and any of its
- -- prefixes if it is of a deep type. Actually, some operation
- -- like reading from an object of access type is considered as
- -- observe while it should not affect the permissions of
- -- the considered tree.
+ -- Check path was not borrowed
- Tree : Perm_Tree_Access;
+ Check_Not_Borrowed (Expr, Root);
- begin
- if Is_Deep (Etype (N)) then
- Tree := Set_Perm_Prefixes (N, Observed);
- else
- Tree := null;
- end if;
+ -- For modes that require W permission, check path was not observed
- if Tree = null then
+ case Mode is
+ when Read | Observe =>
+ null;
+ when Assign | Move | Borrow =>
+ Check_Not_Observed (Expr, Root);
+ end case;
- -- We went through a function call, no permission to
- -- modify.
+ -- Do not update permission environment when handling calls
- return;
- end if;
+ if Inside_Procedure_Call then
+ return;
+ end if;
+
+ -- Update the permissions
- -- Set permissions to No on any strict extension of the path
+ case Mode is
- Set_Perm_Extensions (Tree, Observed);
- end;
- end case;
- end Process_Path;
+ when Read =>
+ null;
- -------------------------
- -- Return_Declarations --
- -------------------------
+ when Move =>
- procedure Return_Declarations (L : List_Id) is
- procedure Return_Declaration (Decl : Node_Id);
- -- Check correct permissions for every declared object
+ -- SPARK RM 3.10(1): After a move operation, the state of the
+ -- source object (if any) becomes Moved.
- ------------------------
- -- Return_Declaration --
- ------------------------
+ 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;
- procedure Return_Declaration (Decl : Node_Id) is
- begin
- if Nkind (Decl) = N_Object_Declaration then
+ when Assign =>
- -- Check RW for object declared, unless the object has never been
- -- initialized.
+ -- If there is no root object, or the tree has an array component,
+ -- then the permissions do not get modified by the assignment.
- if Get (Current_Initialization_Map,
- Unique_Entity (Defining_Identifier (Decl))) = False
+ if No (Get_Root_Object (Expr))
+ or else Has_Array_Component (Expr)
then
return;
end if;
- declare
- Elem : constant Perm_Tree_Access :=
- Get (Current_Perm_Env,
- Unique_Entity (Defining_Identifier (Decl)));
+ -- Set permission RW for the path and its extensions
+ declare
+ Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr);
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.
+ Tree.all.Tree.Permission := Read_Write;
+ Set_Perm_Extensions (Tree, Read_Write, Expl => Expr);
- -- Hash_Table_Error
+ -- Normalize the permission tree
- raise Program_Error;
- end if;
-
- if Permission (Elem) /= Unrestricted then
- Perm_Error (Decl, Unrestricted, Permission (Elem));
- end if;
+ Set_Perm_Prefixes_Assign (Expr);
end;
- end if;
- end Return_Declaration;
- -- Local Variables
-
- N : Node_Id;
- -- Start of processing for Return_Declarations
+ -- Borrowing and observing of paths is handled by the variables
+ -- Current_Borrowers and Current_Observers.
- begin
- N := First (L);
- while Present (N) loop
- Return_Declaration (N);
- Next (N);
- end loop;
- end Return_Declarations;
+ when Borrow | Observe =>
+ null;
+ end case;
+ end Process_Path;
--------------------
-- Return_Globals --
--------------------
procedure Return_Globals (Subp : Entity_Id) is
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind);
- -- Return global items from the list starting at Item
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
- -- Return global items for the mode Global_Mode
+ 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_Globals_From_List --
- ------------------------------
+ -------------------
+ -- Return_Global --
+ -------------------
- procedure Return_Globals_From_List
- (First_Item : Node_Id;
- Kind : Formal_Kind)
+ procedure Return_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
- Return_The_Global (E, Kind, Subp);
- end if;
- Next_Global (Item);
- end loop;
- end Return_Globals_From_List;
-
- ----------------------------
- -- Return_Globals_Of_Mode --
- ----------------------------
-
- procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
- Kind : Formal_Kind;
-
begin
- case Global_Mode is
- when Name_Input
- | Name_Proof_In
- =>
- Kind := E_In_Parameter;
- when Name_Output =>
- Kind := E_Out_Parameter;
- when Name_In_Out =>
- Kind := E_In_Out_Parameter;
- when others =>
- raise Program_Error;
- end case;
-
- -- Return both global items from Global and Refined_Global pragmas
+ Return_Parameter_Or_Global
+ (Id => Entity (Expr),
+ Typ => Typ,
+ Kind => Kind,
+ Subp => Subp,
+ Global_Var => Global_Var);
+ end Return_Global;
- 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;
+ 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;
--------------------------------
-- Return_Parameter_Or_Global --
--------------------------------
- procedure Return_The_Global
- (Id : Entity_Id;
- Mode : Formal_Kind;
- Subp : Entity_Id)
+ procedure Return_Parameter_Or_Global
+ (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
- -- Observed IN parameters and globals need not return a permission to
- -- the caller.
+ -- Shallow parameters and globals need not be considered
+
+ if not Is_Deep (Typ) then
+ return;
- if Mode = E_In_Parameter
+ elsif Kind = E_In_Parameter then
- -- Check this for read-only globals.
+ -- Input global variables are observed only
- then
- if Permission (Elem) /= Unrestricted
- and then Permission (Elem) /= Observed
+ if Global_Var then
+ return;
+
+ -- Anonymous access to constant is an observe
+
+ elsif Is_Anonymous_Access_Type (Typ)
+ and then Is_Access_Constant (Typ)
then
- Perm_Error_Subprogram_End
- (E => Id,
- Subp => Subp,
- Perm => Observed,
- Found_Perm => Permission (Elem));
+ return;
+
+ -- Deep types other than access types define an observe
+
+ elsif not Is_Access_Type (Typ) then
+ return;
end if;
+ end if;
- -- All globals of mode out or in/out should return with mode
- -- Unrestricted.
+ -- All other parameters and globals should return with mode RW to the
+ -- caller.
- else
- if Permission (Elem) /= Unrestricted 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 => Unrestricted,
- Found_Perm => Permission (Elem));
+ Perm => Read_Write,
+ Found_Perm => Permission (Tree),
+ Expl => Explanation (Tree));
end if;
- end if;
- end Return_The_Global;
+ end;
+ end Return_Parameter_Or_Global;
+
+ -----------------------
+ -- Return_Parameters --
+ -----------------------
+
+ procedure Return_Parameters (Subp : Entity_Id) is
+ Formal : Entity_Id;
+ begin
+ Formal := First_Formal (Subp);
+ while Present (Formal) loop
+ Return_Parameter_Or_Global
+ (Id => Formal,
+ Typ => Retysp (Etype (Formal)),
+ Kind => Ekind (Formal),
+ Subp => Subp,
+ Global_Var => False);
+ Next_Formal (Formal);
+ end loop;
+ end Return_Parameters;
-------------------------
-- Set_Perm_Extensions --
-------------------------
- procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is
+ procedure Set_Perm_Extensions
+ (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
+
+ -----------------------------
+ -- Free_Perm_Tree_Children --
+ -----------------------------
+
procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
begin
case Kind (T) is
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;
------------------------------
- -- Set_Perm_Prefixes --
+ -- Set_Perm_Extensions_Move --
------------------------------
- function Set_Perm_Prefixes
- (N : Node_Id;
- New_Perm : Perm_Kind)
- return Perm_Tree_Access
+ procedure Set_Perm_Extensions_Move
+ (T : Perm_Tree_Access;
+ E : Entity_Id;
+ Expl : Node_Id)
is
+ Check_Ty : constant Entity_Id := Retysp (E);
begin
+ -- Shallow extensions are set to RW
- case Nkind (N) is
-
- when N_Identifier
- | N_Expanded_Name
- | N_Defining_Identifier
- =>
- if Nkind (N) = N_Defining_Identifier
- and then New_Perm = Borrowed
- then
- raise Program_Error;
- end if;
-
- declare
- P : Node_Id;
- C : Perm_Tree_Access;
-
- begin
- if Nkind (N) = N_Defining_Identifier then
- P := N;
- else
- P := Entity (N);
- end if;
-
- C := Get (Current_Perm_Env, Unique_Entity (P));
- pragma Assert (C /= null);
-
- -- Setting the initialization map to True, so that this
- -- variable cannot be ignored anymore when looking at end
- -- of elaboration of package.
-
- Set (Current_Initialization_Map, Unique_Entity (P), True);
- if New_Perm = Observed
- and then C = null
- then
-
- -- No null possible here, there are no parents for the path.
- -- This means we are using a global variable without adding
- -- it in environment with a global aspect.
-
- Illegal_Global_Usage (N);
- end if;
-
- C.all.Tree.Permission := New_Perm;
- return C;
- end;
-
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Set_Perm_Prefixes (Expression (N), New_Perm);
-
- when N_Parameter_Specification =>
- 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 (Prefix (N), New_Perm);
-
- begin
- if C = null then
+ if not Is_Node_Deep (T) then
+ Set_Perm_Extensions (T, Read_Write, Expl => Expl);
+ return;
+ end if;
- -- We went through a function call, do nothing
+ -- Deep extensions are set to W before .all and NO afterwards
- return null;
- end if;
+ T.all.Tree.Permission := Write_Only;
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Record_Component);
+ case T.all.Tree.Kind is
- if Kind (C) = Record_Component then
- -- The tree is unfolded. We just modify the permission and
- -- return the record subtree.
+ -- 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
+ =>
declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
-
- Selected_C : Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
-
+ 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
- if Selected_C = null then
- Selected_C := Other_Components (C);
- end if;
-
- pragma Assert (Selected_C /= null);
- Selected_C.all.Tree.Permission := New_Perm;
- return Selected_C;
+ 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 => C);
end;
- elsif Kind (C) = Entire_Object then
+ when Record_Kind =>
declare
- -- Expand the tree. Replace the node with
- -- Record_Component.
-
- Elem : Node_Id;
-
- -- Create an empty hash table
-
+ C : Perm_Tree_Access;
+ Comp : Entity_Id;
Hashtbl : Perm_Tree_Maps.Instance;
- -- We create the unrolled nodes, that will all have same
- -- permission than parent.
-
- Son : Perm_Tree_Access;
- Children_Perm : constant Perm_Kind :=
- Children_Permission (C);
-
begin
- -- We change the current node from Entire_Object to
- -- Record_Component with same permission and an empty
- -- hash table as component list.
-
- C.all.Tree :=
- (Kind => Record_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Permission (C),
- Component => Hashtbl,
- Other_Components =>
- new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => True,
- Permission => Children_Perm,
- Children_Permission => Children_Perm)
- ));
-
- -- We fill the hash table with all sons of the record,
- -- with basic Entire_Objects nodes.
+ Comp := First_Component_Or_Discriminant (Check_Ty);
+ while Present (Comp) loop
- 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 => Children_Perm,
- Children_Permission => Children_Perm));
+ -- Unfold components which are visible in SPARK
- Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
- Next_Component_Or_Discriminant (Elem);
- end loop;
- -- Now we set the right field to Borrowed, and then we
- -- return the tree to the sons, so that the recursion can
- -- continue.
+ 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);
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
- Selected_C : Perm_Tree_Access :=
- Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ -- Hidden components are never deep
- begin
- if Selected_C = null then
- Selected_C := Other_Components (C);
+ 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 (Selected_C /= null);
- Selected_C.all.Tree.Permission := New_Perm;
- return Selected_C;
- end;
- end;
- else
- raise Program_Error;
- end if;
- end;
-
- -- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer the subtree and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree in
- -- one step.
-
- when N_Indexed_Component
- | N_Slice
- =>
- declare
- C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes (Prefix (N), New_Perm);
-
- begin
- if C = null then
-
- -- We went through a function call, do nothing
-
- return null;
- end if;
-
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Array_Component);
-
- if Kind (C) = Array_Component then
-
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
-
- pragma Assert (Get_Elem (C) /= null);
- C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
- return Get_Elem (C);
-
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace node with Array_Component.
-
- Son : Perm_Tree_Access;
+ Perm_Tree_Maps.Set
+ (Hashtbl, Original_Record_Component (Comp), C);
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => New_Perm,
- Children_Permission => Children_Permission (C)));
+ T.all.Tree :=
+ (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (T),
+ Explanation => Expl,
+ Permission => Write_Only,
+ Component => Hashtbl);
+ end;
- -- Children_Permission => Children_Permission (C)
- -- this line should be checked maybe New_Perm
- -- instead of Children_Permission (C)
+ -- Otherwise, extensions are set to NO
- -- We change the current node from Entire_Object
- -- to Array_Component with same permission and the
- -- previously defined son.
+ when others =>
+ Set_Perm_Extensions (T, No_Access, Expl);
+ end case;
- C.all.Tree := (Kind => Array_Component,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => New_Perm,
- Get_Elem => Son);
- return Get_Elem (C);
- end;
- else
- raise Program_Error;
- end if;
- end;
+ when Reference =>
+ Set_Perm_Extensions (T, No_Access, Expl);
- -- 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 Array_Component =>
+ Set_Perm_Extensions_Move
+ (Get_Elem (T), Component_Type (Check_Ty), Expl);
- when N_Explicit_Dereference =>
+ when Record_Component =>
declare
- C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes (Prefix (N), New_Perm);
+ C : Perm_Tree_Access;
+ Comp : Entity_Id;
begin
- if C = null then
-
- -- We went through a function call. Do nothing.
-
- return null;
- end if;
-
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Reference);
-
- if Kind (C) = Reference then
-
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
-
- pragma Assert (Get_All (C) /= null);
- C.all.Tree.Get_All.all.Tree.Permission := New_Perm;
- return Get_All (C);
-
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with Reference.
+ 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);
- Son : Perm_Tree_Access;
+ -- Move visible components
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => New_Perm,
- Children_Permission => Children_Permission (C)));
+ if Component_Is_Visible_In_SPARK (Comp) then
+ Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
- -- We change the current node from Entire_Object to
- -- Reference with Borrowed and the previous son.
+ -- Hidden components are never deep
- pragma Assert (Is_Node_Deep (C));
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => New_Perm,
- Get_All => Son);
- return Get_All (C);
- end;
+ else
+ Set_Perm_Extensions (C, Read_Write, Expl => Expl);
+ end if;
- else
- raise Program_Error;
- end if;
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
end;
-
- when N_Function_Call =>
- return null;
-
- when others =>
- raise Program_Error;
end case;
- end Set_Perm_Prefixes;
-
- ------------------------------
- -- Set_Perm_Prefixes_Borrow --
- ------------------------------
+ end Set_Perm_Extensions_Move;
- function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
+ -----------------------
+ -- Set_Perm_Prefixes --
+ -----------------------
+
+ 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 = Borrow);
case Nkind (N) is
-
- when N_Identifier
- | N_Expanded_Name
+ when N_Expanded_Name
+ | N_Identifier
=>
declare
- P : constant Node_Id := Entity (N);
- C : constant Perm_Tree_Access :=
- Get (Current_Perm_Env, Unique_Entity (P));
+ E : constant Entity_Id := Unique_Entity (Entity (N));
+ C : constant Perm_Tree_Access := Get (Current_Perm_Env, E);
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.
+ if Perm /= None then
+ C.all.Tree.Permission := Glb (Perm, Permission (C));
+ end if;
- Set (Current_Initialization_Map, Unique_Entity (P), True);
- C.all.Tree.Permission := Borrowed;
return C;
end;
- when N_Type_Conversion
- | N_Unchecked_Type_Conversion
- | N_Qualified_Expression
- =>
- return Set_Perm_Prefixes_Borrow (Expression (N));
-
- when N_Parameter_Specification
- | N_Defining_Identifier
- =>
- raise Program_Error;
+ -- 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.
- -- 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 =>
+ when N_Explicit_Dereference =>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow (Prefix (N));
-
+ Set_Perm_Prefixes (Prefix (N), Perm, Expl);
+ pragma Assert (C /= null);
+ pragma Assert (Kind (C) = Entire_Object
+ or else Kind (C) = Reference);
begin
- if C = null then
+ -- The tree is already unfolded. Replace the permission of the
+ -- dereference.
- -- We went through a function call, do nothing
+ if Kind (C) = Reference then
+ declare
+ D : constant Perm_Tree_Access := Get_All (C);
+ pragma Assert (D /= null);
- return null;
- end if;
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Glb (Perm, Permission (D));
+ end if;
+
+ return D;
+ end;
+
+ -- The tree is folded. Expand it.
+
+ 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;
- -- The permission of the returned node should be No
+ 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;
- pragma Assert (Permission (C) = Borrowed);
+ when N_Selected_Component =>
+ 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) = 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.
-
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 := Borrowed;
- 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 same
- -- permission than parent.
-
- Son : Perm_Tree_Access;
- ChildrenPerm : 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.
-
- 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)));
+ 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;
- 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 => 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 Borrowed, and then we
- -- return the tree to the sons, so that the recursion can
- -- continue.
+ 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
+ (Hashtbl, Original_Record_Component (Comp), D);
- declare
- Selected_Component : constant Entity_Id :=
- Entity (Selector_Name (N));
- Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
- (Component (C), Selected_Component);
+ -- Store the tree to return for this 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 := Borrowed;
- return Selected_C;
- end;
- end;
+ Next_Component_Or_Discriminant (Comp);
+ end loop;
- else
- raise Program_Error;
+ C.all.Tree := (Kind => Record_Component,
+ Is_Node_Deep => Is_Node_Deep (C),
+ Explanation => Expl,
+ Permission => Permission (C),
+ Component => Hashtbl);
+ return D_This;
+ end;
end if;
end;
- -- We set the permission tree of its prefix, and then we extract
- -- from the returned pointer the subtree and assign an adequate
- -- permission to it, if unfolded. If folded, we unroll the tree in
- -- one step.
-
when N_Indexed_Component
| N_Slice
=>
declare
C : constant Perm_Tree_Access :=
- Set_Perm_Prefixes_Borrow (Prefix (N));
-
- begin
- if C = null then
-
- -- We went through a function call, do nothing
-
- return null;
- end if;
-
- pragma Assert (Permission (C) = Borrowed);
+ 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
+ declare
+ D : constant Perm_Tree_Access := Get_Elem (C);
+ pragma Assert (D /= null);
- -- 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 := Borrowed;
- return Get_Elem (C);
+ begin
+ if Perm /= None then
+ D.all.Tree.Permission := Glb (Perm, Permission (D));
+ end if;
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace node with Array_Component.
+ return D;
+ end;
- Son : Perm_Tree_Access;
+ -- The tree is folded. Expand it.
+ 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
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Borrowed,
- Children_Permission => Children_Permission (C)));
-
- -- We change the current node from Entire_Object
- -- to Array_Component with same permission and the
- -- previously defined son.
+ 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 => Borrowed,
- 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_Borrow (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
+ when others =>
+ raise Program_Error;
+ end case;
+ end Set_Perm_Prefixes;
- -- We went through a function call. Do nothing.
+ ------------------------------
+ -- Set_Perm_Prefixes_Assign --
+ ------------------------------
- return null;
- end if;
+ procedure Set_Perm_Prefixes_Assign (N : Node_Id) is
+ C : constant Perm_Tree_Access := Get_Perm_Tree (N);
- -- The permission of the returned node should be No
+ begin
+ case Kind (C) is
+ when Entire_Object =>
+ pragma Assert (Children_Permission (C) = Read_Write);
+ C.all.Tree.Permission := Read_Write;
- pragma Assert (Permission (C) = Borrowed);
- pragma Assert (Kind (C) = Entire_Object
- or else Kind (C) = Reference);
+ when Reference =>
+ C.all.Tree.Permission :=
+ Lub (Permission (C), Permission (Get_All (C)));
- if Kind (C) = Reference then
+ when Array_Component =>
+ null;
- -- The tree is unfolded. We just modify the permission and
- -- return the elem subtree.
+ when Record_Component =>
+ declare
+ Comp : Perm_Tree_Access;
+ Perm : Perm_Kind := Read_Write;
- pragma Assert (Get_All (C) /= null);
- C.all.Tree.Get_All.all.Tree.Permission := Borrowed;
- return Get_All (C);
+ begin
+ -- We take the Glb of all the descendants, and then update the
+ -- permission of the node with it.
- elsif Kind (C) = Entire_Object then
- declare
- -- Expand the tree. Replace the node with Reference.
+ 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;
- Son : Perm_Tree_Access;
+ C.all.Tree.Permission := Lub (Permission (C), Perm);
+ end;
+ end case;
- begin
- Son := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (N)),
- Permission => Borrowed,
- Children_Permission => Children_Permission (C)));
+ case Nkind (N) is
- -- We change the current node from Entire_Object to
- -- Reference with Borrowed and the previous son.
+ -- Base identifier end recursion
- pragma Assert (Is_Node_Deep (C));
- C.all.Tree := (Kind => Reference,
- Is_Node_Deep => Is_Node_Deep (C),
- Permission => Borrowed,
- Get_All => Son);
- return Get_All (C);
- end;
+ when N_Expanded_Name
+ | N_Identifier
+ =>
+ null;
- 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_Borrow;
+ 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, Global_Var => True);
- end if;
- Next_Global (Item);
- end loop;
- end Setup_Globals_From_List;
-
- ---------------------------
- -- Setup_Globals_Of_Mode --
- ---------------------------
-
- procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
- Kind : Formal_Kind;
-
begin
- case Global_Mode is
- when Name_Input
- | Name_Proof_In
- =>
- Kind := E_In_Parameter;
-
- when Name_Output =>
- Kind := E_Out_Parameter;
-
- when Name_In_Out =>
- Kind := E_In_Out_Parameter;
-
- when others =>
- raise Program_Error;
- end case;
-
- -- Set up both global items from Global and Refined_Global pragmas
+ Setup_Parameter_Or_Global
+ (Id => Entity (Expr),
+ Typ => Typ,
+ Kind => Kind,
+ Subp => Subp,
+ Global_Var => Global_Var,
+ Expl => Expr);
+ end Setup_Global;
- 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;
- Global_Var : Boolean)
+ Typ : Entity_Id;
+ Kind : Formal_Kind;
+ Subp : Entity_Id;
+ Global_Var : Boolean;
+ Expl : Node_Id)
is
- Elem : Perm_Tree_Access;
- View_Typ : Entity_Id;
+ Perm : Perm_Kind_Option;
begin
- if Present (Full_View (Etype (Id))) then
- View_Typ := Full_View (Etype (Id));
- else
- View_Typ := Etype (Id);
- end if;
+ case Kind is
+ when E_In_Parameter =>
- Elem := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Id)),
- Permission => Unrestricted,
- Children_Permission => Unrestricted));
+ -- Shallow parameters and globals need not be considered
- case Mode is
+ if not Is_Deep (Typ) then
+ Perm := None;
- -- All out and in out parameters are considered to be unrestricted.
- -- They are whether borrowed or moved. Ada Rules would restrict
- -- these permissions further. For example an in parameter cannot
- -- be written.
+ -- Inputs of functions have R permission only
- -- In the following we deal with in parameters that can be observed.
- -- We only consider the observing cases.
+ elsif Ekind (Subp) = E_Function then
+ Perm := Read_Only;
- when E_In_Parameter =>
+ -- Input global variables have R permission only
- -- Handling global variables as IN parameters here.
- -- Remove the following condition once it's decided how globals
- -- should be considered. ???
- --
- -- In SPARK, IN access-to-variable is an observe operation for
- -- a function, and a borrow operation for a procedure.
-
- if not Global_Var then
- if (Is_Access_Type (View_Typ)
- and then Is_Access_Constant (View_Typ)
- and then Is_Anonymous_Access_Type (View_Typ))
- or else
- (Is_Access_Type (View_Typ)
- and then Ekind (Scope (Id)) = E_Function)
- or else
- (not Is_Access_Type (View_Typ)
- and then Is_Deep (View_Typ)
- and then not Is_Anonymous_Access_Type (View_Typ))
- then
- Elem.all.Tree.Permission := Observed;
- Elem.all.Tree.Children_Permission := Observed;
+ elsif Global_Var then
+ Perm := Read_Only;
- else
- Elem.all.Tree.Permission := Unrestricted;
- Elem.all.Tree.Children_Permission := Unrestricted;
- end if;
+ -- Anonymous access to constant is an observe
+
+ 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 := Observed;
- Elem.all.Tree.Children_Permission := Observed;
+ Perm := Read_Only;
end if;
- -- When out or in/out formal or global parameters, we set them to
- -- the Unrestricted state. "We want to be able to assume that all
- -- relevant writable globals are unrestricted when a subprogram
- -- starts executing". Formal parameters of mode out or in/out
- -- are whether Borrowers or the targets of a move operation:
- -- they start theirs lives in the subprogram as Unrestricted.
+ when E_Out_Parameter
+ | E_In_Out_Parameter
+ =>
+ -- Shallow parameters and globals need not be considered
+
+ if not Is_Deep (Typ) then
+ Perm := None;
- when others =>
- Elem.all.Tree.Permission := Unrestricted;
- Elem.all.Tree.Children_Permission := Unrestricted;
+ -- Functions cannot have outputs in SPARK
+
+ 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;
----------------------
-- Setup_Parameters --
----------------------
- procedure Setup_Parameters (Subp : Entity_Id) is Formal : Entity_Id;
+ procedure Setup_Parameters (Subp : Entity_Id) is
+ Formal : Entity_Id;
begin
Formal := First_Formal (Subp);
while Present (Formal) loop
Setup_Parameter_Or_Global
- (Formal, Ekind (Formal), Global_Var => False);
+ (Id => Formal,
+ Typ => Retysp (Etype (Formal)),
+ Kind => Ekind (Formal),
+ Subp => Subp,
+ Global_Var => False,
+ Expl => Formal);
Next_Formal (Formal);
end loop;
end Setup_Parameters;
- -------------------------------
- -- Has_Ownership_Aspect_True --
- -------------------------------
-
- function Has_Ownership_Aspect_True
- (N : Entity_Id;
- Msg : String)
- return Boolean
- is
- begin
- case Ekind (Etype (N)) is
- when Access_Kind =>
- if Ekind (Etype (N)) = E_General_Access_Type then
- Error_Msg_NE (Msg & " & not allowed " &
- "(Named General Access type)", N, N);
- return False;
-
- else
- return True;
- end if;
-
- when E_Array_Type
- | E_Array_Subtype
- =>
- declare
- Com_Ty : constant Node_Id := Component_Type (Etype (N));
- Ret : Boolean := Has_Ownership_Aspect_True (Com_Ty, "");
-
- begin
- if Nkind (Parent (N)) = N_Full_Type_Declaration and
- Is_Anonymous_Access_Type (Com_Ty)
- then
- Ret := False;
- end if;
+ --------------------------------
+ -- Setup_Protected_Components --
+ --------------------------------
- if not Ret then
- Error_Msg_NE (Msg & " & not allowed "
- & "(Components of Named General Access type or"
- & " Anonymous type)", N, N);
- end if;
- return Ret;
- end;
+ procedure Setup_Protected_Components (Subp : Entity_Id) is
+ Typ : constant Entity_Id := Scope (Subp);
+ Comp : Entity_Id;
+ Kind : Formal_Kind;
- -- ??? What about hidden components
+ begin
+ Comp := First_Component_Or_Discriminant (Typ);
- when E_Record_Type
- | E_Record_Subtype
- =>
- declare
- Elmt : Entity_Id;
- Elmt_T_Perm : Boolean := True;
- Elmt_Perm, Elmt_Anonym : Boolean;
+ -- The protected object is an implicit input of protected functions, and
+ -- an implicit input-output of protected procedures and entries.
- begin
- Elmt := First_Component_Or_Discriminant (Etype (N));
- while Present (Elmt) loop
- Elmt_Perm := Has_Ownership_Aspect_True (Elmt,
- "type of component");
- Elmt_Anonym := Is_Anonymous_Access_Type (Etype (Elmt));
- if Elmt_Anonym then
- Error_Msg_NE
- ("type of component & not allowed"
- & " (Components of Anonymous type)", Elmt, Elmt);
- end if;
- Elmt_T_Perm := Elmt_T_Perm and Elmt_Perm and not Elmt_Anonym;
- Next_Component_Or_Discriminant (Elmt);
- end loop;
- if not Elmt_T_Perm then
- Error_Msg_NE
- (Msg & " & not allowed (One or "
- & "more components have Ownership Aspect False)",
- N, N);
- end if;
- return Elmt_T_Perm;
- end;
+ if Ekind (Subp) = E_Function then
+ Kind := E_In_Parameter;
+ else
+ Kind := E_In_Out_Parameter;
+ end if;
- when others =>
- return True;
- end case;
+ 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 Has_Ownership_Aspect_True;
end Sem_SPARK;
projects / thirdparty / gcc.git / blobdiff