1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Atree
; use Atree
;
27 with Einfo
; use Einfo
;
28 with Errout
; use Errout
;
29 with Namet
; use Namet
;
30 with Nlists
; use Nlists
;
32 with Osint
; use Osint
;
33 with Sem_Prag
; use Sem_Prag
;
34 with Sem_Util
; use Sem_Util
;
35 with Sem_Aux
; use Sem_Aux
;
36 with Sinfo
; use Sinfo
;
37 with Snames
; use Snames
;
38 with Treepr
; use Treepr
;
40 with Ada
.Unchecked_Deallocation
;
41 with GNAT
.Dynamic_HTables
; use GNAT
.Dynamic_HTables
;
43 package body Sem_SPARK
is
45 -------------------------------------------------
46 -- Handling of Permissions Associated to Paths --
47 -------------------------------------------------
49 package Permissions
is
50 Elaboration_Context_Max
: constant := 1009;
53 type Elaboration_Context_Index
is range 0 .. Elaboration_Context_Max
- 1;
55 function Elaboration_Context_Hash
56 (Key
: Entity_Id
) return Elaboration_Context_Index
;
57 -- Function to hash any node of the AST
59 type Perm_Kind
is (No_Access
, Read_Only
, Read_Write
, Write_Only
);
60 -- Permission type associated with paths
62 subtype Read_Perm
is Perm_Kind
range Read_Only
.. Read_Write
;
63 subtype Write_Perm
is Perm_Kind
range Read_Write
.. Write_Only
;
65 type Perm_Tree_Wrapper
;
67 type Perm_Tree_Access
is access Perm_Tree_Wrapper
;
68 -- A tree of permissions is defined, where the root is a whole object
69 -- and tree branches follow access paths in memory. As Perm_Tree is a
70 -- discriminated record, a wrapper type is used for the access type
71 -- designating a subtree, to make it unconstrained so that it can be
74 -- Nodes in the permission tree are of different kinds
77 (Entire_Object
, -- Scalar object, or folded object of any type
78 Reference
, -- Unfolded object of access type
79 Array_Component
, -- Unfolded object of array type
80 Record_Component
-- Unfolded object of record type
83 package Perm_Tree_Maps
is new Simple_HTable
84 (Header_Num
=> Elaboration_Context_Index
,
86 Element
=> Perm_Tree_Access
,
88 Hash
=> Elaboration_Context_Hash
,
90 -- The instantation of a hash table, with keys being nodes and values
91 -- being pointers to trees. This is used to reference easily all
92 -- extensions of a Record_Component node (that can have name x, y, ...).
94 -- The definition of permission trees. This is a tree, which has a
95 -- permission at each node, and depending on the type of the node,
96 -- can have zero, one, or more children pointed to by an access to tree.
97 type Perm_Tree
(Kind
: Path_Kind
:= Entire_Object
) is record
98 Permission
: Perm_Kind
;
99 -- Permission at this level in the path
101 Is_Node_Deep
: Boolean;
102 -- Whether this node is of a deep type, to be used when moving the
107 -- An entire object is either a leaf (an object which cannot be
108 -- extended further in a path) or a subtree in folded form (which
109 -- could later be unfolded further in another kind of node). The
110 -- field Children_Permission specifies a permission for every
111 -- extension of that node if that permission is different from
112 -- the node's permission.
114 when Entire_Object
=>
115 Children_Permission
: Perm_Kind
;
117 -- Unfolded path of access type. The permission of the object
118 -- pointed to is given in Get_All.
121 Get_All
: Perm_Tree_Access
;
123 -- Unfolded path of array type. The permission of the elements is
124 -- given in Get_Elem.
126 when Array_Component
=>
127 Get_Elem
: Perm_Tree_Access
;
129 -- Unfolded path of record type. The permission of the regular
130 -- components is given in Component. The permission of unknown
131 -- components (for objects of tagged type) is given in
134 when Record_Component
=>
135 Component
: Perm_Tree_Maps
.Instance
;
136 Other_Components
: Perm_Tree_Access
;
140 type Perm_Tree_Wrapper
is record
143 -- We use this wrapper in order to have unconstrained discriminants
145 type Perm_Env
is new Perm_Tree_Maps
.Instance
;
146 -- The definition of a permission environment for the analysis. This
147 -- is just a hash table of permission trees, each of them rooted with
148 -- an Identifier/Expanded_Name.
150 type Perm_Env_Access
is access Perm_Env
;
151 -- Access to permission environments
153 package Env_Maps
is new Simple_HTable
154 (Header_Num
=> Elaboration_Context_Index
,
156 Element
=> Perm_Env_Access
,
158 Hash
=> Elaboration_Context_Hash
,
160 -- The instantiation of a hash table whose elements are permission
161 -- environments. This hash table is used to save the environments at
162 -- the entry of each loop, with the key being the loop label.
164 type Env_Backups
is new Env_Maps
.Instance
;
165 -- The type defining the hash table saving the environments at the entry
168 package Boolean_Variables_Maps
is new Simple_HTable
169 (Header_Num
=> Elaboration_Context_Index
,
173 Hash
=> Elaboration_Context_Hash
,
175 -- These maps allow tracking the variables that have been declared but
176 -- never used anywhere in the source code. Especially, we do not raise
177 -- an error if the variable stays write-only and is declared at package
178 -- level, because there is no risk that the variable has been moved,
179 -- because it has never been used.
181 type Initialization_Map
is new Boolean_Variables_Maps
.Instance
;
187 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
188 -- that's only for the top access, as otherwise this reverses the order
189 -- in accesses visually.
191 function Children_Permission
(T
: Perm_Tree_Access
) return Perm_Kind
;
192 function Component
(T
: Perm_Tree_Access
) return Perm_Tree_Maps
.Instance
;
193 function Get_All
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
194 function Get_Elem
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
195 function Is_Node_Deep
(T
: Perm_Tree_Access
) return Boolean;
196 function Kind
(T
: Perm_Tree_Access
) return Path_Kind
;
197 function Other_Components
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
198 function Permission
(T
: Perm_Tree_Access
) return Perm_Kind
;
200 -----------------------
201 -- Memory Management --
202 -----------------------
206 To
: in out Perm_Env
);
207 -- Procedure to copy a permission environment
209 procedure Copy_Init_Map
210 (From
: Initialization_Map
;
211 To
: in out Initialization_Map
);
212 -- Procedure to copy an initialization map
215 (From
: Perm_Tree_Access
;
216 To
: Perm_Tree_Access
);
217 -- Procedure to copy a permission tree
220 (PE
: in out Perm_Env
);
221 -- Procedure to free a permission environment
223 procedure Free_Perm_Tree
224 (PT
: in out Perm_Tree_Access
);
225 -- Procedure to free a permission tree
231 procedure Perm_Mismatch
232 (Exp_Perm
, Act_Perm
: Perm_Kind
;
234 -- Issues a continuation error message about a mismatch between a
235 -- desired permission Exp_Perm and a permission obtained Act_Perm. N
236 -- is the node on which the error is reported.
240 package body Permissions
is
242 -------------------------
243 -- Children_Permission --
244 -------------------------
246 function Children_Permission
247 (T
: Perm_Tree_Access
)
251 return T
.all.Tree
.Children_Permission
;
252 end Children_Permission
;
259 (T
: Perm_Tree_Access
)
260 return Perm_Tree_Maps
.Instance
263 return T
.all.Tree
.Component
;
272 To
: in out Perm_Env
)
274 Comp_From
: Perm_Tree_Access
;
275 Key_From
: Perm_Tree_Maps
.Key_Option
;
276 Son
: Perm_Tree_Access
;
280 Key_From
:= Get_First_Key
(From
);
281 while Key_From
.Present
loop
282 Comp_From
:= Get
(From
, Key_From
.K
);
283 pragma Assert
(Comp_From
/= null);
285 Son
:= new Perm_Tree_Wrapper
;
286 Copy_Tree
(Comp_From
, Son
);
288 Set
(To
, Key_From
.K
, Son
);
289 Key_From
:= Get_Next_Key
(From
);
297 procedure Copy_Init_Map
298 (From
: Initialization_Map
;
299 To
: in out Initialization_Map
)
302 Key_From
: Boolean_Variables_Maps
.Key_Option
;
306 Key_From
:= Get_First_Key
(From
);
307 while Key_From
.Present
loop
308 Comp_From
:= Get
(From
, Key_From
.K
);
309 Set
(To
, Key_From
.K
, Comp_From
);
310 Key_From
:= Get_Next_Key
(From
);
319 (From
: Perm_Tree_Access
;
320 To
: Perm_Tree_Access
)
326 when Entire_Object
=>
330 To
.all.Tree
.Get_All
:= new Perm_Tree_Wrapper
;
332 Copy_Tree
(Get_All
(From
), Get_All
(To
));
334 when Array_Component
=>
335 To
.all.Tree
.Get_Elem
:= new Perm_Tree_Wrapper
;
337 Copy_Tree
(Get_Elem
(From
), Get_Elem
(To
));
339 when Record_Component
=>
341 Comp_From
: Perm_Tree_Access
;
342 Key_From
: Perm_Tree_Maps
.Key_Option
;
343 Son
: Perm_Tree_Access
;
344 Hash_Table
: Perm_Tree_Maps
.Instance
;
346 -- We put a new hash table, so that it gets dealiased from the
347 -- Component (From) hash table.
348 To
.all.Tree
.Component
:= Hash_Table
;
350 To
.all.Tree
.Other_Components
:=
351 new Perm_Tree_Wrapper
'(Other_Components (From).all);
353 Copy_Tree (Other_Components (From), Other_Components (To));
355 Key_From := Perm_Tree_Maps.Get_First_Key
357 while Key_From.Present loop
358 Comp_From := Perm_Tree_Maps.Get
359 (Component (From), Key_From.K);
361 pragma Assert (Comp_From /= null);
362 Son := new Perm_Tree_Wrapper;
364 Copy_Tree (Comp_From, Son);
367 (To.all.Tree.Component, Key_From.K, Son);
369 Key_From := Perm_Tree_Maps.Get_Next_Key
376 ------------------------------
377 -- Elaboration_Context_Hash --
378 ------------------------------
380 function Elaboration_Context_Hash
381 (Key : Entity_Id) return Elaboration_Context_Index
384 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
385 end Elaboration_Context_Hash;
391 procedure Free_Env (PE : in out Perm_Env) is
392 CompO : Perm_Tree_Access;
394 CompO := Get_First (PE);
395 while CompO /= null loop
396 Free_Perm_Tree (CompO);
397 CompO := Get_Next (PE);
405 procedure Free_Perm_Tree
406 (PT : in out Perm_Tree_Access)
408 procedure Free_Perm_Tree_Dealloc is
409 new Ada.Unchecked_Deallocation
410 (Perm_Tree_Wrapper, Perm_Tree_Access);
411 -- The deallocator for permission_trees
415 when Entire_Object =>
416 Free_Perm_Tree_Dealloc (PT);
419 Free_Perm_Tree (PT.all.Tree.Get_All);
420 Free_Perm_Tree_Dealloc (PT);
422 when Array_Component =>
423 Free_Perm_Tree (PT.all.Tree.Get_Elem);
425 when Record_Component =>
427 Comp : Perm_Tree_Access;
430 Free_Perm_Tree (PT.all.Tree.Other_Components);
431 Comp := Perm_Tree_Maps.Get_First (Component (PT));
432 while Comp /= null loop
433 -- Free every Component subtree
435 Free_Perm_Tree (Comp);
436 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
439 Free_Perm_Tree_Dealloc (PT);
448 (T : Perm_Tree_Access)
449 return Perm_Tree_Access
452 return T.all.Tree.Get_All;
460 (T : Perm_Tree_Access)
461 return Perm_Tree_Access
464 return T.all.Tree.Get_Elem;
471 function Is_Node_Deep
472 (T : Perm_Tree_Access)
476 return T.all.Tree.Is_Node_Deep;
484 (T : Perm_Tree_Access)
488 return T.all.Tree.Kind;
491 ----------------------
492 -- Other_Components --
493 ----------------------
495 function Other_Components
496 (T : Perm_Tree_Access)
497 return Perm_Tree_Access
500 return T.all.Tree.Other_Components;
501 end Other_Components;
508 (T : Perm_Tree_Access)
512 return T.all.Tree.Permission;
519 procedure Perm_Mismatch
520 (Exp_Perm, Act_Perm : Perm_Kind;
524 Error_Msg_N ("\expected at least `"
525 & Perm_Kind'Image (Exp_Perm) & "`, got `"
526 & Perm_Kind'Image (Act_Perm) & "`", N);
533 --------------------------------------
534 -- Analysis modes for AST traversal --
535 --------------------------------------
537 -- The different modes for analysis. This allows to checking whether a path
538 -- found in the code should be moved, borrowed, or observed.
540 type Checking_Mode is
543 -- Default mode. Checks that paths have Read_Perm permission.
546 -- Regular moving semantics (not under 'Access). Checks that paths have
547 -- Read_Write permission. After moving a path, its permission is set to
548 -- Write_Only and the permission of its extensions is set to No_Access.
551 -- Used for the target of an assignment, or an actual parameter with
552 -- mode OUT. Checks that paths have Write_Perm permission. After
553 -- assigning to a path, its permission is set to Read_Write.
556 -- Enhanced moving semantics (under 'Access). Checks that paths have
557 -- Read_Write permission. After moving a path, its permission is set
558 -- to No_Access, as well as the permission of its extensions and the
559 -- permission of its prefixes up to the first Reference node.
562 -- Used for actual OUT parameters. Checks that paths have Write_Perm
563 -- permission. After checking a path, its permission is set to Read_Only
564 -- when of a by-copy type, to No_Access otherwise. After the call, its
565 -- permission is set to Read_Write.
568 -- Used for actual IN parameters of a scalar type. Checks that paths
569 -- have Read_Perm permission. After checking a path, its permission
570 -- is set to Read_Only.
572 -- Also used for formal IN parameters
575 type Result_Kind
is (Folded
, Unfolded
, Function_Call
);
576 -- The type declaration to discriminate in the Perm_Or_Tree type
578 -- The result type of the function Get_Perm_Or_Tree. This returns either a
579 -- tree when it found the appropriate tree, or a permission when the search
580 -- finds a leaf and the subtree we are looking for is folded. In the last
581 -- case, we return instead the Children_Permission field of the leaf.
583 type Perm_Or_Tree
(R
: Result_Kind
) is record
585 when Folded
=> Found_Permission
: Perm_Kind
;
586 when Unfolded
=> Tree_Access
: Perm_Tree_Access
;
587 when Function_Call
=> null;
591 -----------------------
592 -- Local subprograms --
593 -----------------------
595 function "<=" (P1
, P2
: Perm_Kind
) return Boolean;
596 function ">=" (P1
, P2
: Perm_Kind
) return Boolean;
597 function Glb
(P1
, P2
: Perm_Kind
) return Perm_Kind
;
598 function Lub
(P1
, P2
: Perm_Kind
) return Perm_Kind
;
600 -- Checking proceduress for safe pointer usage. These procedures traverse
601 -- the AST, check nodes for correct permissions according to SPARK RM
602 -- 6.4.2, and update permissions depending on the node kind.
604 procedure Check_Call_Statement
(Call
: Node_Id
);
606 procedure Check_Callable_Body
(Body_N
: Node_Id
);
607 -- We are not in End_Of_Callee mode, hence we will save the environment
608 -- and start from a new one. We will add in the environment all formal
609 -- parameters as well as global used during the subprogram, with the
610 -- appropriate permissions (write-only for out, read-only for observed,
611 -- read-write for others).
613 -- After that we analyze the body of the function, and finaly, we check
614 -- that each borrowed parameter and global has read-write permission. We
615 -- then clean up the environment and put back the saved environment.
617 procedure Check_Declaration
(Decl
: Node_Id
);
619 procedure Check_Expression
(Expr
: Node_Id
);
621 procedure Check_Globals
(N
: Node_Id
; Check_Mode
: Checking_Mode
);
622 -- This procedure takes a global pragma and checks depending on mode:
623 -- Mode Read: every in global is readable
624 -- Mode Observe: same as Check_Param_Observes but on globals
625 -- Mode Borrow_Out: Check_Param_Outs for globals
626 -- Mode Move: Check_Param for globals with mode Read
627 -- Mode Assign: Check_Param for globals with mode Assign
629 procedure Check_List
(L
: List_Id
);
630 -- Calls Check_Node on each element of the list
632 procedure Check_Loop_Statement
(Loop_N
: Node_Id
);
634 procedure Check_Node
(N
: Node_Id
);
635 -- Main traversal procedure to check safe pointer usage. This procedure is
636 -- mutually recursive with the specialized procedures that follow.
638 procedure Check_Package_Body
(Pack
: Node_Id
);
640 procedure Check_Param
(Formal
: Entity_Id
; Actual
: Node_Id
);
641 -- This procedure takes a formal and an actual parameter and calls the
642 -- analyze node if the parameter is borrowed with mode in out, with the
643 -- appropriate Checking_Mode (Move).
645 procedure Check_Param_Observes
(Formal
: Entity_Id
; Actual
: Node_Id
);
646 -- This procedure takes a formal and an actual parameter and calls
647 -- the analyze node if the parameter is observed, with the appropriate
650 procedure Check_Param_Outs
(Formal
: Entity_Id
; Actual
: Node_Id
);
651 -- This procedure takes a formal and an actual parameter and calls the
652 -- analyze node if the parameter is of mode out, with the appropriate
655 procedure Check_Param_Read
(Formal
: Entity_Id
; Actual
: Node_Id
);
656 -- This procedure takes a formal and an actual parameter and checks the
657 -- readability of every in-mode parameter. This includes observed in, and
658 -- also borrowed in, that are then checked afterwards.
660 procedure Check_Statement
(Stmt
: Node_Id
);
662 function Get_Perm
(N
: Node_Id
) return Perm_Kind
;
663 -- The function that takes a name as input and returns a permission
666 function Get_Perm_Or_Tree
(N
: Node_Id
) return Perm_Or_Tree
;
667 -- This function gets a Node_Id and looks recursively to find the
668 -- appropriate subtree for that Node_Id. If the tree is folded on
669 -- that node, then it returns the permission given at the right level.
671 function Get_Perm_Tree
(N
: Node_Id
) return Perm_Tree_Access
;
672 -- This function gets a Node_Id and looks recursively to find the
673 -- appropriate subtree for that Node_Id. If the tree is folded, then
674 -- it unrolls the tree up to the appropriate level.
679 -- Function that returns whether the path given as parameter contains an
680 -- extension that is declared as aliased.
682 function Has_Array_Component
(N
: Node_Id
) return Boolean;
683 -- This function gets a Node_Id and looks recursively to find if the given
684 -- path has any array component.
686 function Has_Function_Component
(N
: Node_Id
) return Boolean;
687 -- This function gets a Node_Id and looks recursively to find if the given
688 -- path has any function component.
690 procedure Hp
(P
: Perm_Env
);
691 -- A procedure that outputs the hash table. This function is used only in
692 -- the debugger to look into a hash table.
693 pragma Unreferenced
(Hp
);
695 procedure Illegal_Global_Usage
(N
: Node_Or_Entity_Id
);
696 pragma No_Return
(Illegal_Global_Usage
);
697 -- A procedure that is called when deep globals or aliased globals are used
698 -- without any global aspect.
700 function Is_Borrowed_In
(E
: Entity_Id
) return Boolean;
701 -- Function that tells if the given entity is a borrowed in a formal
702 -- parameter, that is, if it is an access-to-variable type.
704 function Is_Deep
(E
: Entity_Id
) return Boolean;
705 -- A function that can tell if a type is deep or not. Returns true if the
706 -- type passed as argument is deep.
708 function Is_Shallow
(E
: Entity_Id
) return Boolean;
709 -- A function that can tell if a type is shallow or not. Returns true if
710 -- the type passed as argument is shallow.
712 function Loop_Of_Exit
(N
: Node_Id
) return Entity_Id
;
713 -- A function that takes an exit statement node and returns the entity of
714 -- the loop that this statement is exiting from.
716 procedure Merge_Envs
(Target
: in out Perm_Env
; Source
: in out Perm_Env
);
717 -- Merge Target and Source into Target, and then deallocate the Source
722 Found_Perm
: Perm_Kind
);
723 -- A procedure that is called when the permissions found contradict the
724 -- rules established by the RM. This function is called with the node, its
725 -- entity and the permission that was expected, and adds an error message
726 -- with the appropriate values.
728 procedure Perm_Error_Subprogram_End
732 Found_Perm
: Perm_Kind
);
733 -- A procedure that is called when the permissions found contradict the
734 -- rules established by the RM at the end of subprograms. This function
735 -- is called with the node, its entity, the node of the returning function
736 -- and the permission that was expected, and adds an error message with the
737 -- appropriate values.
739 procedure Process_Path
(N
: Node_Id
);
741 procedure Return_Declarations
(L
: List_Id
);
742 -- Check correct permissions on every declared object at the end of a
743 -- callee. Used at the end of the body of a callable entity. Checks that
744 -- paths of all borrowed formal parameters and global have Read_Write
747 procedure Return_Globals
(Subp
: Entity_Id
);
748 -- Takes a subprogram as input, and checks that all borrowed global items
749 -- of the subprogram indeed have RW permission at the end of the subprogram
752 procedure Return_Parameter_Or_Global
756 -- Auxiliary procedure to Return_Parameters and Return_Globals
758 procedure Return_Parameters
(Subp
: Entity_Id
);
759 -- Takes a subprogram as input, and checks that all borrowed parameters of
760 -- the subprogram indeed have RW permission at the end of the subprogram
763 procedure Set_Perm_Extensions
(T
: Perm_Tree_Access
; P
: Perm_Kind
);
764 -- This procedure takes an access to a permission tree and modifies the
765 -- tree so that any strict extensions of the given tree become of the
766 -- access specified by parameter P.
768 procedure Set_Perm_Extensions_Move
(T
: Perm_Tree_Access
; E
: Entity_Id
);
769 -- Set permissions to
770 -- No for any extension with more .all
771 -- W for any deep extension with same number of .all
772 -- RW for any shallow extension with same number of .all
774 function Set_Perm_Prefixes_Assign
(N
: Node_Id
) return Perm_Tree_Access
;
775 -- This function takes a name as an input and sets in the permission
776 -- tree the given permission to the given name. The general rule here is
777 -- that everybody updates the permission of the subtree it is returning.
778 -- The permission of the assigned path has been set to RW by the caller.
780 -- Case where we have to normalize a tree after the correct permissions
781 -- have been assigned already. We look for the right subtree at the given
782 -- path, actualize its permissions, and then call the normalization on its
785 -- Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will
786 -- change the permission of x to RW because all of its components have
787 -- permission have permission RW.
789 function Set_Perm_Prefixes_Borrow_Out
(N
: Node_Id
) return Perm_Tree_Access
;
790 -- This function modifies the permissions of a given node_id in the
791 -- permission environment as well as in all the prefixes of the path,
792 -- given that the path is borrowed with mode out.
794 function Set_Perm_Prefixes_Move
795 (N
: Node_Id
; Mode
: Checking_Mode
)
796 return Perm_Tree_Access
;
797 pragma Precondition
(Mode
= Move
or Mode
= Super_Move
);
798 -- Given a node and a mode (that can be either Move or Super_Move), this
799 -- function modifies the permissions of a given node_id in the permission
800 -- environment as well as all the prefixes of the path, given that the path
801 -- is moved with or without 'Access. The general rule here is everybody
802 -- updates the permission of the subtree they are returning.
804 -- This case describes a move either under 'Access or without 'Access.
806 function Set_Perm_Prefixes_Observe
(N
: Node_Id
) return Perm_Tree_Access
;
807 -- This function modifies the permissions of a given node_id in the
808 -- permission environment as well as all the prefixes of the path,
809 -- given that the path is observed.
811 procedure Setup_Globals
(Subp
: Entity_Id
);
812 -- Takes a subprogram as input, and sets up the environment by adding
813 -- global items with appropriate permissions.
815 procedure Setup_Parameter_Or_Global
818 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
820 procedure Setup_Parameters
(Subp
: Entity_Id
);
821 -- Takes a subprogram as input, and sets up the environment by adding
822 -- formal parameters with appropriate permissions.
824 ----------------------
825 -- Global Variables --
826 ----------------------
828 Current_Perm_Env
: Perm_Env
;
829 -- The permission environment that is used for the analysis. This
830 -- environment can be saved, modified, reinitialized, but should be the
831 -- only one valid from which to extract the permissions of the paths in
832 -- scope. The analysis ensures at each point that this variables contains
833 -- a valid permission environment with all bindings in scope.
835 Current_Checking_Mode
: Checking_Mode
:= Read
;
836 -- The current analysis mode. This global variable indicates at each point
837 -- of the analysis whether the node being analyzed is moved, borrowed,
838 -- assigned, read, ... The full list of possible values can be found in
839 -- the declaration of type Checking_Mode.
841 Current_Loops_Envs
: Env_Backups
;
842 -- This variable contains saves of permission environments at each loop the
843 -- analysis entered. Each saved environment can be reached with the label
846 Current_Loops_Accumulators
: Env_Backups
;
847 -- This variable contains the environments used as accumulators for loops,
848 -- that consist of the merge of all environments at each exit point of
849 -- the loop (which can also be the entry point of the loop in the case of
850 -- non-infinite loops), each of them reachable from the label of the loop.
851 -- We require that the environment stored in the accumulator be less
852 -- restrictive than the saved environment at the beginning of the loop, and
853 -- the permission environment after the loop is equal to the accumulator.
855 Current_Initialization_Map
: Initialization_Map
;
856 -- This variable contains a map that binds each variable of the analyzed
857 -- source code to a boolean that becomes true whenever the variable is used
858 -- after declaration. Hence we can exclude from analysis variables that
859 -- are just declared and never accessed, typically at package declaration.
865 function "<=" (P1
, P2
: Perm_Kind
) return Boolean
875 function ">=" (P1
, P2
: Perm_Kind
) return Boolean
879 when No_Access
=> return True;
880 when Read_Only
=> return P1
in Read_Perm
;
881 when Write_Only
=> return P1
in Write_Perm
;
882 when Read_Write
=> return P1
= Read_Write
;
886 --------------------------
887 -- Check_Call_Statement --
888 --------------------------
890 procedure Check_Call_Statement
(Call
: Node_Id
) is
891 Saved_Env
: Perm_Env
;
893 procedure Iterate_Call
is new
894 Iterate_Call_Parameters
(Check_Param
);
895 procedure Iterate_Call_Observes
is new
896 Iterate_Call_Parameters
(Check_Param_Observes
);
897 procedure Iterate_Call_Outs
is new
898 Iterate_Call_Parameters
(Check_Param_Outs
);
899 procedure Iterate_Call_Read
is new
900 Iterate_Call_Parameters
(Check_Param_Read
);
903 -- Save environment, so that the modifications done by analyzing the
904 -- parameters are not kept at the end of the call.
905 Copy_Env
(Current_Perm_Env
,
908 -- We first check the Read access on every in parameter
910 Current_Checking_Mode
:= Read
;
911 Iterate_Call_Read
(Call
);
912 Check_Globals
(Get_Pragma
913 (Get_Called_Entity
(Call
), Pragma_Global
), Read
);
915 -- We first observe, then borrow with mode out, and then with other
916 -- modes. This ensures that we do not have to check for by-copy types
917 -- specially, because we read them before borrowing them.
919 Iterate_Call_Observes
(Call
);
920 Check_Globals
(Get_Pragma
921 (Get_Called_Entity
(Call
), Pragma_Global
),
924 Iterate_Call_Outs
(Call
);
925 Check_Globals
(Get_Pragma
926 (Get_Called_Entity
(Call
), Pragma_Global
),
930 Check_Globals
(Get_Pragma
931 (Get_Called_Entity
(Call
), Pragma_Global
), Move
);
933 -- Restore environment, because after borrowing/observing actual
934 -- parameters, they get their permission reverted to the ones before
937 Free_Env
(Current_Perm_Env
);
942 Free_Env
(Saved_Env
);
944 -- We assign the out parameters (necessarily borrowed per RM)
945 Current_Checking_Mode
:= Assign
;
947 Check_Globals
(Get_Pragma
948 (Get_Called_Entity
(Call
), Pragma_Global
),
951 end Check_Call_Statement
;
953 -------------------------
954 -- Check_Callable_Body --
955 -------------------------
957 procedure Check_Callable_Body
(Body_N
: Node_Id
) is
959 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
961 Saved_Env
: Perm_Env
;
962 Saved_Init_Map
: Initialization_Map
;
966 Body_Id
: constant Entity_Id
:= Defining_Entity
(Body_N
);
967 Spec_Id
: constant Entity_Id
:= Unique_Entity
(Body_Id
);
970 -- Check if SPARK pragma is not set to Off
972 if Present
(SPARK_Pragma
(Defining_Entity
(Body_N
))) then
973 if Get_SPARK_Mode_From_Annotation
974 (SPARK_Pragma
(Defining_Entity
(Body_N
, False))) /= Opt
.On
982 -- Save environment and put a new one in place
984 Copy_Env
(Current_Perm_Env
, Saved_Env
);
986 -- Save initialization map
988 Copy_Init_Map
(Current_Initialization_Map
, Saved_Init_Map
);
990 Current_Checking_Mode
:= Read
;
991 Current_Perm_Env
:= New_Env
;
993 -- Add formals and globals to the environment with adequate permissions
995 if Is_Subprogram_Or_Entry
(Spec_Id
) then
996 Setup_Parameters
(Spec_Id
);
997 Setup_Globals
(Spec_Id
);
1000 -- Analyze the body of the function
1002 Check_List
(Declarations
(Body_N
));
1003 Check_Node
(Handled_Statement_Sequence
(Body_N
));
1005 -- Check the read-write permissions of borrowed parameters/globals
1007 if Ekind_In
(Spec_Id
, E_Procedure
, E_Entry
)
1008 and then not No_Return
(Spec_Id
)
1010 Return_Parameters
(Spec_Id
);
1011 Return_Globals
(Spec_Id
);
1014 -- Free the environments
1016 Free_Env
(Current_Perm_Env
);
1018 Copy_Env
(Saved_Env
,
1021 Free_Env
(Saved_Env
);
1023 -- Restore initialization map
1025 Copy_Init_Map
(Saved_Init_Map
, Current_Initialization_Map
);
1027 Reset
(Saved_Init_Map
);
1029 -- The assignment of all out parameters will be done by caller
1031 Current_Checking_Mode
:= Mode_Before
;
1032 end Check_Callable_Body
;
1034 -----------------------
1035 -- Check_Declaration --
1036 -----------------------
1038 procedure Check_Declaration
(Decl
: Node_Id
) is
1040 case N_Declaration
'(Nkind (Decl)) is
1041 when N_Full_Type_Declaration =>
1042 -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE
1045 when N_Object_Declaration =>
1046 -- First move the right-hand side
1047 Current_Checking_Mode := Move;
1048 Check_Node (Expression (Decl));
1051 Elem : Perm_Tree_Access;
1054 Elem := new Perm_Tree_Wrapper'
1056 (Kind
=> Entire_Object
,
1058 Is_Deep
(Etype
(Defining_Identifier
(Decl
))),
1059 Permission
=> Read_Write
,
1060 Children_Permission
=> Read_Write
));
1062 -- If unitialized declaration, then set to Write_Only. If a
1063 -- pointer declaration, it has a null default initialization.
1064 if Nkind
(Expression
(Decl
)) = N_Empty
1065 and then not Has_Full_Default_Initialization
1066 (Etype
(Defining_Identifier
(Decl
)))
1067 and then not Is_Access_Type
1068 (Etype
(Defining_Identifier
(Decl
)))
1070 Elem
.all.Tree
.Permission
:= Write_Only
;
1071 Elem
.all.Tree
.Children_Permission
:= Write_Only
;
1074 -- Create new tree for defining identifier
1076 Set
(Current_Perm_Env
,
1077 Unique_Entity
(Defining_Identifier
(Decl
)),
1080 pragma Assert
(Get_First
(Current_Perm_Env
)
1085 when N_Subtype_Declaration
=>
1086 Check_Node
(Subtype_Indication
(Decl
));
1088 when N_Iterator_Specification
=>
1089 pragma Assert
(Is_Shallow
(Etype
(Defining_Identifier
(Decl
))));
1092 when N_Loop_Parameter_Specification
=>
1093 pragma Assert
(Is_Shallow
(Etype
(Defining_Identifier
(Decl
))));
1096 -- Checking should not be called directly on these nodes
1098 when N_Component_Declaration
1099 | N_Function_Specification
1100 | N_Entry_Declaration
1101 | N_Procedure_Specification
1103 raise Program_Error
;
1105 -- Ignored constructs for pointer checking
1107 when N_Formal_Object_Declaration
1108 | N_Formal_Type_Declaration
1109 | N_Incomplete_Type_Declaration
1110 | N_Private_Extension_Declaration
1111 | N_Private_Type_Declaration
1112 | N_Protected_Type_Declaration
1116 -- The following nodes are rewritten by semantic analysis
1118 when N_Expression_Function
=>
1119 raise Program_Error
;
1121 end Check_Declaration
;
1123 ----------------------
1124 -- Check_Expression --
1125 ----------------------
1127 procedure Check_Expression
(Expr
: Node_Id
) is
1128 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
1130 case N_Subexpr
'(Nkind (Expr)) is
1131 when N_Procedure_Call_Statement =>
1132 Check_Call_Statement (Expr);
1137 -- Check if identifier is pointing to nothing (On/Off/...)
1138 if not Present (Entity (Expr)) then
1142 -- Do not analyze things that are not of object Kind
1143 if Ekind (Entity (Expr)) not in Object_Kind then
1147 -- Consider as ident
1148 Process_Path (Expr);
1150 -- Switch to read mode and then check the readability of each operand
1154 Current_Checking_Mode := Read;
1155 Check_Node (Left_Opnd (Expr));
1156 Check_Node (Right_Opnd (Expr));
1158 -- Switch to read mode and then check the readability of each operand
1165 pragma Assert (Is_Shallow (Etype (Expr)));
1166 Current_Checking_Mode := Read;
1167 Check_Node (Right_Opnd (Expr));
1169 -- Forbid all deep expressions for Attribute ???
1171 when N_Attribute_Reference =>
1172 case Attribute_Name (Expr) is
1174 case Current_Checking_Mode is
1176 Check_Node (Prefix (Expr));
1179 Current_Checking_Mode := Super_Move;
1180 Check_Node (Prefix (Expr));
1182 -- Only assign names, not expressions
1185 raise Program_Error;
1187 -- Prefix in Super_Move should be a name, error here
1190 raise Program_Error;
1192 -- Could only borrow names of mode out, not n'Access
1195 raise Program_Error;
1198 Check_Node (Prefix (Expr));
1204 Current_Checking_Mode := Read;
1205 Check_Node (Prefix (Expr));
1208 Current_Checking_Mode := Read;
1209 Check_Node (Prefix (Expr));
1212 Check_Node (Prefix (Expr));
1214 when Name_SPARK_Mode =>
1218 Current_Checking_Mode := Read;
1219 Check_Node (Prefix (Expr));
1222 Check_List (Expressions (Expr));
1223 Check_Node (Prefix (Expr));
1228 Check_List (Expressions (Expr));
1229 Check_Node (Prefix (Expr));
1232 Current_Checking_Mode := Read;
1233 Check_Node (Prefix (Expr));
1235 -- Any Attribute referring to the underlying memory is ignored
1236 -- in the analysis. This means that taking the address of a
1237 -- variable makes a silent alias that is not rejected by the
1242 | Name_Component_Size
1250 -- Attributes referring to types (get values from types), hence
1251 -- no need to check either for borrows or any loans.
1258 -- Other attributes that fall out of the scope of the analysis
1265 Current_Checking_Mode := Read;
1266 Check_Node (Left_Opnd (Expr));
1267 Check_Node (Right_Opnd (Expr));
1270 Current_Checking_Mode := Read;
1271 Check_Node (Left_Opnd (Expr));
1272 Check_Node (Right_Opnd (Expr));
1274 -- Switch to read mode and then check the readability of each operand
1279 pragma Assert (Is_Shallow (Etype (Expr)));
1280 Current_Checking_Mode := Read;
1281 Check_Node (Left_Opnd (Expr));
1282 Check_Node (Right_Opnd (Expr));
1284 -- Check the arguments of the call
1286 when N_Function_Call =>
1287 Current_Checking_Mode := Read;
1288 Check_List (Parameter_Associations (Expr));
1290 when N_Explicit_Dereference =>
1291 Process_Path (Expr);
1293 -- Copy environment, run on each branch, and then merge
1295 when N_If_Expression =>
1297 Saved_Env : Perm_Env;
1299 -- Accumulator for the different branches
1303 Elmt : Node_Id := First (Expressions (Expr));
1306 Current_Checking_Mode := Read;
1310 Current_Checking_Mode := Mode_Before;
1314 Copy_Env (Current_Perm_Env,
1317 -- Here we have the original env in saved, current with a fresh
1318 -- copy, and new aliased.
1325 -- Here the new_environment contains curr env after then block
1329 -- Restore environment before if
1330 Copy_Env (Current_Perm_Env,
1333 Free_Env (Current_Perm_Env);
1335 Copy_Env (Saved_Env,
1338 -- Here new environment contains the environment after then and
1339 -- current the fresh copy of old one.
1344 Merge_Envs (New_Env,
1353 Free_Env (Saved_Env);
1356 when N_Indexed_Component =>
1357 Process_Path (Expr);
1359 -- Analyze the expression that is getting qualified
1361 when N_Qualified_Expression =>
1362 Check_Node (Expression (Expr));
1364 when N_Quantified_Expression =>
1366 Saved_Env : Perm_Env;
1368 Copy_Env (Current_Perm_Env, Saved_Env);
1369 Current_Checking_Mode := Read;
1370 Check_Node (Iterator_Specification (Expr));
1371 Check_Node (Loop_Parameter_Specification (Expr));
1373 Check_Node (Condition (Expr));
1374 Free_Env (Current_Perm_Env);
1375 Copy_Env (Saved_Env, Current_Perm_Env);
1376 Free_Env (Saved_Env);
1379 -- Analyze the list of associations in the aggregate
1382 Check_List (Expressions (Expr));
1383 Check_List (Component_Associations (Expr));
1386 Check_Node (Expression (Expr));
1388 when N_Case_Expression =>
1390 Saved_Env : Perm_Env;
1392 -- Accumulator for the different branches
1396 Elmt : Node_Id := First (Alternatives (Expr));
1399 Current_Checking_Mode := Read;
1400 Check_Node (Expression (Expr));
1402 Current_Checking_Mode := Mode_Before;
1406 Copy_Env (Current_Perm_Env,
1409 -- Here we have the original env in saved, current with a fresh
1410 -- copy, and new aliased.
1412 -- First alternative
1417 Copy_Env (Current_Perm_Env,
1420 Free_Env (Current_Perm_Env);
1422 -- Other alternatives
1424 while Present (Elmt) loop
1425 -- Restore environment
1427 Copy_Env (Saved_Env,
1432 -- Merge Current_Perm_Env into New_Env
1434 Merge_Envs (New_Env,
1445 Free_Env (Saved_Env);
1448 -- Analyze the list of associates in the aggregate as well as the
1451 when N_Extension_Aggregate =>
1453 Check_Node (Ancestor_Part (Expr));
1454 Check_List (Expressions (Expr));
1457 Check_Node (Low_Bound (Expr));
1458 Check_Node (High_Bound (Expr));
1460 -- We arrived at a path. Process it.
1462 when N_Selected_Component =>
1463 Process_Path (Expr);
1466 Process_Path (Expr);
1468 when N_Type_Conversion =>
1469 Check_Node (Expression (Expr));
1471 when N_Unchecked_Type_Conversion =>
1472 Check_Node (Expression (Expr));
1474 -- Checking should not be called directly on these nodes
1476 when N_Target_Name =>
1477 raise Program_Error;
1479 -- Unsupported constructs in SPARK
1481 when N_Delta_Aggregate =>
1482 Error_Msg_N ("unsupported construct in SPARK", Expr);
1484 -- Ignored constructs for pointer checking
1486 when N_Character_Literal
1488 | N_Numeric_Or_String_Literal
1490 | N_Raise_Expression
1495 -- The following nodes are never generated in GNATprove mode
1497 when N_Expression_With_Actions
1499 | N_Unchecked_Expression
1501 raise Program_Error;
1504 end Check_Expression;
1510 procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is
1512 if Nkind (N) = N_Empty then
1518 (List_Length (Pragma_Argument_Associations (N)) = 1);
1520 PAA : constant Node_Id :=
1521 First (Pragma_Argument_Associations (N));
1522 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1528 procedure Process (Mode : Name_Id;
1529 The_Global : Entity_Id);
1531 procedure Process (Mode : Name_Id;
1532 The_Global : Node_Id)
1534 Ident_Elt : constant Entity_Id :=
1535 Unique_Entity (Entity (The_Global));
1537 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1540 if Ekind (Ident_Elt) = E_Abstract_State then
1550 Check_Node (The_Global);
1558 raise Program_Error;
1567 if not Is_Borrowed_In (Ident_Elt) then
1570 Current_Checking_Mode := Observe;
1571 Check_Node (The_Global);
1584 Current_Checking_Mode := Borrow_Out;
1585 Check_Node (The_Global);
1597 if Is_Borrowed_In (Ident_Elt) then
1600 Current_Checking_Mode := Move;
1613 Current_Checking_Mode := Move;
1616 raise Program_Error;
1619 Check_Node (The_Global);
1630 -- Borrowed out or in out
1632 Process_Path (The_Global);
1635 raise Program_Error;
1639 raise Program_Error;
1642 Current_Checking_Mode := Mode_Before;
1646 if Nkind (Expression (PAA)) = N_Null then
1648 -- No globals, nothing to do
1651 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1654 Process (Name_Input, Expression (PAA));
1656 elsif Nkind (Expression (PAA)) = N_Aggregate
1657 and then Expressions (Expression (PAA)) /= No_List
1659 -- global => (foo, bar)
1661 RHS := First (Expressions (Expression (PAA)));
1662 while Present (RHS) loop
1667 Process (Name_Input, RHS);
1669 when N_Numeric_Or_String_Literal =>
1670 Process (Name_Input, Original_Node (RHS));
1673 raise Program_Error;
1679 elsif Nkind (Expression (PAA)) = N_Aggregate
1680 and then Component_Associations (Expression (PAA)) /= No_List
1682 -- global => (mode => foo,
1683 -- mode => (bar, baz))
1684 -- A mixture of things
1687 CA : constant List_Id :=
1688 Component_Associations (Expression (PAA));
1691 while Present (Row) loop
1692 pragma Assert (List_Length (Choices (Row)) = 1);
1693 The_Mode := Chars (First (Choices (Row)));
1695 RHS := Expression (Row);
1698 RHS := First (Expressions (RHS));
1699 while Present (RHS) loop
1701 when N_Numeric_Or_String_Literal =>
1702 Process (The_Mode, Original_Node (RHS));
1705 Process (The_Mode, RHS);
1714 Process (The_Mode, RHS);
1719 when N_Numeric_Or_String_Literal =>
1720 Process (The_Mode, Original_Node (RHS));
1723 raise Program_Error;
1732 raise Program_Error;
1741 procedure Check_List (L : List_Id) is
1745 while Present (N) loop
1751 --------------------------
1752 -- Check_Loop_Statement --
1753 --------------------------
1755 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1757 -- Local Subprograms
1759 procedure Check_Is_Less_Restrictive_Env
1760 (Exiting_Env : Perm_Env;
1761 Entry_Env : Perm_Env);
1762 -- This procedure checks that the Exiting_Env environment is less
1763 -- restrictive than the Entry_Env environment.
1765 procedure Check_Is_Less_Restrictive_Tree
1766 (New_Tree : Perm_Tree_Access;
1767 Orig_Tree : Perm_Tree_Access;
1769 -- Auxiliary procedure to check that the tree New_Tree is less
1770 -- restrictive than the tree Orig_Tree for the entity E.
1772 procedure Perm_Error_Loop_Exit
1776 Found_Perm : Perm_Kind);
1777 -- A procedure that is called when the permissions found contradict
1778 -- the rules established by the RM at the exit of loops. This function
1779 -- is called with the entity, the node of the enclosing loop, the
1780 -- permission that was expected and the permission found, and issues
1781 -- an appropriate error message.
1783 -----------------------------------
1784 -- Check_Is_Less_Restrictive_Env --
1785 -----------------------------------
1787 procedure Check_Is_Less_Restrictive_Env
1788 (Exiting_Env : Perm_Env;
1789 Entry_Env : Perm_Env)
1791 Comp_Entry : Perm_Tree_Maps.Key_Option;
1792 Iter_Entry, Iter_Exit : Perm_Tree_Access;
1795 Comp_Entry := Get_First_Key (Entry_Env);
1796 while Comp_Entry.Present loop
1797 Iter_Entry := Get (Entry_Env, Comp_Entry.K);
1798 pragma Assert (Iter_Entry /= null);
1799 Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
1800 pragma Assert (Iter_Exit /= null);
1801 Check_Is_Less_Restrictive_Tree
1802 (New_Tree => Iter_Exit,
1803 Orig_Tree => Iter_Entry,
1805 Comp_Entry := Get_Next_Key (Entry_Env);
1807 end Check_Is_Less_Restrictive_Env;
1809 ------------------------------------
1810 -- Check_Is_Less_Restrictive_Tree --
1811 ------------------------------------
1813 procedure Check_Is_Less_Restrictive_Tree
1814 (New_Tree : Perm_Tree_Access;
1815 Orig_Tree : Perm_Tree_Access;
1818 -----------------------
1819 -- Local Subprograms --
1820 -----------------------
1822 procedure Check_Is_Less_Restrictive_Tree_Than
1823 (Tree : Perm_Tree_Access;
1826 -- Auxiliary procedure to check that the tree N is less restrictive
1827 -- than the given permission P.
1829 procedure Check_Is_More_Restrictive_Tree_Than
1830 (Tree : Perm_Tree_Access;
1833 -- Auxiliary procedure to check that the tree N is more restrictive
1834 -- than the given permission P.
1836 -----------------------------------------
1837 -- Check_Is_Less_Restrictive_Tree_Than --
1838 -----------------------------------------
1840 procedure Check_Is_Less_Restrictive_Tree_Than
1841 (Tree : Perm_Tree_Access;
1846 if not (Permission (Tree) >= Perm) then
1847 Perm_Error_Loop_Exit
1848 (E, Loop_N, Permission (Tree), Perm);
1852 when Entire_Object =>
1853 if not (Children_Permission (Tree) >= Perm) then
1854 Perm_Error_Loop_Exit
1855 (E, Loop_N, Children_Permission (Tree), Perm);
1860 Check_Is_Less_Restrictive_Tree_Than
1861 (Get_All (Tree), Perm, E);
1863 when Array_Component =>
1864 Check_Is_Less_Restrictive_Tree_Than
1865 (Get_Elem (Tree), Perm, E);
1867 when Record_Component =>
1869 Comp : Perm_Tree_Access;
1871 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1872 while Comp /= null loop
1873 Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
1875 Perm_Tree_Maps.Get_Next (Component (Tree));
1878 Check_Is_Less_Restrictive_Tree_Than
1879 (Other_Components (Tree), Perm, E);
1882 end Check_Is_Less_Restrictive_Tree_Than;
1884 -----------------------------------------
1885 -- Check_Is_More_Restrictive_Tree_Than --
1886 -----------------------------------------
1888 procedure Check_Is_More_Restrictive_Tree_Than
1889 (Tree : Perm_Tree_Access;
1894 if not (Perm >= Permission (Tree)) then
1895 Perm_Error_Loop_Exit
1896 (E, Loop_N, Permission (Tree), Perm);
1900 when Entire_Object =>
1901 if not (Perm >= Children_Permission (Tree)) then
1902 Perm_Error_Loop_Exit
1903 (E, Loop_N, Children_Permission (Tree), Perm);
1907 Check_Is_More_Restrictive_Tree_Than
1908 (Get_All (Tree), Perm, E);
1910 when Array_Component =>
1911 Check_Is_More_Restrictive_Tree_Than
1912 (Get_Elem (Tree), Perm, E);
1914 when Record_Component =>
1916 Comp : Perm_Tree_Access;
1918 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
1919 while Comp /= null loop
1920 Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
1922 Perm_Tree_Maps.Get_Next (Component (Tree));
1925 Check_Is_More_Restrictive_Tree_Than
1926 (Other_Components (Tree), Perm, E);
1929 end Check_Is_More_Restrictive_Tree_Than;
1931 -- Start of processing for Check_Is_Less_Restrictive_Tree
1934 if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
1935 Perm_Error_Loop_Exit
1938 Perm => Permission (New_Tree),
1939 Found_Perm => Permission (Orig_Tree));
1942 case Kind (New_Tree) is
1944 -- Potentially folded tree. We check the other tree Orig_Tree to
1945 -- check whether it is folded or not. If folded we just compare
1946 -- their Permission and Children_Permission, if not, then we
1947 -- look at the Children_Permission of the folded tree against
1948 -- the unfolded tree Orig_Tree.
1950 when Entire_Object =>
1951 case Kind (Orig_Tree) is
1952 when Entire_Object =>
1953 if not (Children_Permission (New_Tree) <=
1954 Children_Permission (Orig_Tree))
1956 Perm_Error_Loop_Exit
1958 Children_Permission (New_Tree),
1959 Children_Permission (Orig_Tree));
1963 Check_Is_More_Restrictive_Tree_Than
1964 (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
1966 when Array_Component =>
1967 Check_Is_More_Restrictive_Tree_Than
1968 (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
1970 when Record_Component =>
1972 Comp : Perm_Tree_Access;
1974 Comp := Perm_Tree_Maps.Get_First
1975 (Component (Orig_Tree));
1976 while Comp /= null loop
1977 Check_Is_More_Restrictive_Tree_Than
1978 (Comp, Children_Permission (New_Tree), E);
1979 Comp := Perm_Tree_Maps.Get_Next
1980 (Component (Orig_Tree));
1983 Check_Is_More_Restrictive_Tree_Than
1984 (Other_Components (Orig_Tree),
1985 Children_Permission (New_Tree), E);
1990 case Kind (Orig_Tree) is
1991 when Entire_Object =>
1992 Check_Is_Less_Restrictive_Tree_Than
1993 (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
1996 Check_Is_Less_Restrictive_Tree
1997 (Get_All (New_Tree), Get_All (Orig_Tree), E);
2000 raise Program_Error;
2003 when Array_Component =>
2004 case Kind (Orig_Tree) is
2005 when Entire_Object =>
2006 Check_Is_Less_Restrictive_Tree_Than
2007 (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2009 when Array_Component =>
2010 Check_Is_Less_Restrictive_Tree
2011 (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2014 raise Program_Error;
2017 when Record_Component =>
2019 CompN : Perm_Tree_Access;
2022 Perm_Tree_Maps.Get_First (Component (New_Tree));
2023 case Kind (Orig_Tree) is
2024 when Entire_Object =>
2025 while CompN /= null loop
2026 Check_Is_Less_Restrictive_Tree_Than
2027 (CompN, Children_Permission (Orig_Tree), E);
2030 Perm_Tree_Maps.Get_Next (Component (New_Tree));
2033 Check_Is_Less_Restrictive_Tree_Than
2034 (Other_Components (New_Tree),
2035 Children_Permission (Orig_Tree),
2038 when Record_Component =>
2041 KeyO : Perm_Tree_Maps.Key_Option;
2042 CompO : Perm_Tree_Access;
2044 KeyO := Perm_Tree_Maps.Get_First_Key
2045 (Component (Orig_Tree));
2046 while KeyO.Present loop
2047 pragma Assert (CompO /= null);
2049 Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2051 KeyO := Perm_Tree_Maps.Get_Next_Key
2052 (Component (Orig_Tree));
2053 CompN := Perm_Tree_Maps.Get
2054 (Component (New_Tree), KeyO.K);
2055 CompO := Perm_Tree_Maps.Get
2056 (Component (Orig_Tree), KeyO.K);
2059 Check_Is_Less_Restrictive_Tree
2060 (Other_Components (New_Tree),
2061 Other_Components (Orig_Tree),
2066 raise Program_Error;
2070 end Check_Is_Less_Restrictive_Tree;
2072 --------------------------
2073 -- Perm_Error_Loop_Exit --
2074 --------------------------
2076 procedure Perm_Error_Loop_Exit
2080 Found_Perm : Perm_Kind)
2083 Error_Msg_Node_2 := Loop_Id;
2084 Error_Msg_N ("insufficient permission for & when exiting loop &", E);
2085 Perm_Mismatch (Exp_Perm => Perm,
2086 Act_Perm => Found_Perm,
2088 end Perm_Error_Loop_Exit;
2092 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
2093 Loop_Env : constant Perm_Env_Access := new Perm_Env;
2096 -- Save environment prior to the loop
2098 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2100 -- Add saved environment to loop environment
2102 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2104 -- If the loop is not a plain-loop, then it may either never be entered,
2105 -- or it may be exited after a number of iterations. Hence add the
2106 -- current permission environment as the initial loop exit environment.
2107 -- Otherwise, the loop exit environment remains empty until it is
2108 -- populated by analyzing exit statements.
2110 if Present (Iteration_Scheme (Loop_N)) then
2112 Exit_Env : constant Perm_Env_Access := new Perm_Env;
2114 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2115 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2121 Check_Node (Iteration_Scheme (Loop_N));
2122 Check_List (Statements (Loop_N));
2124 -- Check that environment gets less restrictive at end of loop
2126 Check_Is_Less_Restrictive_Env
2127 (Exiting_Env => Current_Perm_Env,
2128 Entry_Env => Loop_Env.all);
2130 -- Set environment to the one for exiting the loop
2133 Exit_Env : constant Perm_Env_Access :=
2134 Get (Current_Loops_Accumulators, Loop_Name);
2136 Free_Env (Current_Perm_Env);
2138 -- In the normal case, Exit_Env is not null and we use it. In the
2139 -- degraded case of a plain-loop without exit statements, Exit_Env is
2140 -- null, and we use the initial permission environment at the start
2141 -- of the loop to continue analysis. Any environment would be fine
2142 -- here, since the code after the loop is dead code, but this way we
2143 -- avoid spurious errors by having at least variables in scope inside
2146 if Exit_Env /= null then
2147 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2149 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2152 Free_Env (Loop_Env.all);
2153 Free_Env (Exit_Env.all);
2155 end Check_Loop_Statement;
2161 procedure Check_Node (N : Node_Id) is
2162 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2165 when N_Declaration =>
2166 Check_Declaration (N);
2169 Check_Expression (N);
2171 when N_Subtype_Indication =>
2172 Check_Node (Constraint (N));
2175 Check_Node (Get_Body_From_Stub (N));
2177 when N_Statement_Other_Than_Procedure_Call =>
2178 Check_Statement (N);
2180 when N_Package_Body =>
2181 Check_Package_Body (N);
2183 when N_Subprogram_Body
2187 Check_Callable_Body (N);
2189 when N_Protected_Body =>
2190 Check_List (Declarations (N));
2192 when N_Package_Declaration =>
2194 Spec : constant Node_Id := Specification (N);
2196 Current_Checking_Mode := Read;
2197 Check_List (Visible_Declarations (Spec));
2198 Check_List (Private_Declarations (Spec));
2200 Return_Declarations (Visible_Declarations (Spec));
2201 Return_Declarations (Private_Declarations (Spec));
2204 when N_Iteration_Scheme =>
2205 Current_Checking_Mode := Read;
2206 Check_Node (Condition (N));
2207 Check_Node (Iterator_Specification (N));
2208 Check_Node (Loop_Parameter_Specification (N));
2210 when N_Case_Expression_Alternative =>
2211 Current_Checking_Mode := Read;
2212 Check_List (Discrete_Choices (N));
2213 Current_Checking_Mode := Mode_Before;
2214 Check_Node (Expression (N));
2216 when N_Case_Statement_Alternative =>
2217 Current_Checking_Mode := Read;
2218 Check_List (Discrete_Choices (N));
2219 Current_Checking_Mode := Mode_Before;
2220 Check_List (Statements (N));
2222 when N_Component_Association =>
2223 Check_Node (Expression (N));
2225 when N_Handled_Sequence_Of_Statements =>
2226 Check_List (Statements (N));
2228 when N_Parameter_Association =>
2229 Check_Node (Explicit_Actual_Parameter (N));
2231 when N_Range_Constraint =>
2232 Check_Node (Range_Expression (N));
2234 when N_Index_Or_Discriminant_Constraint =>
2235 Check_List (Constraints (N));
2237 -- Checking should not be called directly on these nodes
2239 when N_Abortable_Part
2240 | N_Accept_Alternative
2241 | N_Access_Definition
2242 | N_Access_Function_Definition
2243 | N_Access_Procedure_Definition
2244 | N_Access_To_Object_Definition
2245 | N_Aspect_Specification
2246 | N_Compilation_Unit
2247 | N_Compilation_Unit_Aux
2248 | N_Component_Clause
2249 | N_Component_Definition
2251 | N_Constrained_Array_Definition
2253 | N_Decimal_Fixed_Point_Definition
2254 | N_Defining_Character_Literal
2255 | N_Defining_Identifier
2256 | N_Defining_Operator_Symbol
2257 | N_Defining_Program_Unit_Name
2258 | N_Delay_Alternative
2259 | N_Derived_Type_Definition
2261 | N_Discriminant_Association
2262 | N_Discriminant_Specification
2264 | N_Entry_Body_Formal_Part
2265 | N_Enumeration_Type_Definition
2266 | N_Entry_Call_Alternative
2267 | N_Entry_Index_Specification
2269 | N_Exception_Handler
2270 | N_Floating_Point_Definition
2271 | N_Formal_Decimal_Fixed_Point_Definition
2272 | N_Formal_Derived_Type_Definition
2273 | N_Formal_Discrete_Type_Definition
2274 | N_Formal_Floating_Point_Definition
2275 | N_Formal_Incomplete_Type_Definition
2276 | N_Formal_Modular_Type_Definition
2277 | N_Formal_Ordinary_Fixed_Point_Definition
2278 | N_Formal_Private_Type_Definition
2279 | N_Formal_Signed_Integer_Type_Definition
2280 | N_Generic_Association
2282 | N_Modular_Type_Definition
2283 | N_Ordinary_Fixed_Point_Definition
2284 | N_Package_Specification
2285 | N_Parameter_Specification
2286 | N_Pragma_Argument_Association
2287 | N_Protected_Definition
2288 | N_Push_Pop_xxx_Label
2289 | N_Real_Range_Specification
2290 | N_Record_Definition
2291 | N_SCIL_Dispatch_Table_Tag_Init
2292 | N_SCIL_Dispatching_Call
2293 | N_SCIL_Membership_Test
2294 | N_Signed_Integer_Type_Definition
2297 | N_Terminate_Alternative
2298 | N_Triggering_Alternative
2299 | N_Unconstrained_Array_Definition
2305 raise Program_Error;
2307 -- Unsupported constructs in SPARK
2309 when N_Iterated_Component_Association =>
2310 Error_Msg_N ("unsupported construct in SPARK", N);
2312 -- Ignored constructs for pointer checking
2314 when N_Abstract_Subprogram_Declaration
2316 | N_Attribute_Definition_Clause
2318 | N_Delta_Constraint
2319 | N_Digits_Constraint
2321 | N_Enumeration_Representation_Clause
2322 | N_Exception_Declaration
2323 | N_Exception_Renaming_Declaration
2324 | N_Formal_Package_Declaration
2325 | N_Formal_Subprogram_Declaration
2327 | N_Freeze_Generic_Entity
2328 | N_Function_Instantiation
2329 | N_Generic_Function_Renaming_Declaration
2330 | N_Generic_Package_Declaration
2331 | N_Generic_Package_Renaming_Declaration
2332 | N_Generic_Procedure_Renaming_Declaration
2333 | N_Generic_Subprogram_Declaration
2334 | N_Implicit_Label_Declaration
2337 | N_Number_Declaration
2338 | N_Object_Renaming_Declaration
2340 | N_Package_Instantiation
2341 | N_Package_Renaming_Declaration
2343 | N_Procedure_Instantiation
2344 | N_Record_Representation_Clause
2345 | N_Subprogram_Declaration
2346 | N_Subprogram_Renaming_Declaration
2347 | N_Task_Type_Declaration
2348 | N_Use_Package_Clause
2351 | N_Validate_Unchecked_Conversion
2355 -- The following nodes are rewritten by semantic analysis
2357 when N_Single_Protected_Declaration
2358 | N_Single_Task_Declaration
2360 raise Program_Error;
2363 Current_Checking_Mode := Mode_Before;
2366 ------------------------
2367 -- Check_Package_Body --
2368 ------------------------
2370 procedure Check_Package_Body (Pack : Node_Id) is
2371 Saved_Env : Perm_Env;
2375 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
2376 if Get_SPARK_Mode_From_Annotation
2377 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
2385 CorSp := Parent (Corresponding_Spec (Pack));
2386 while Nkind (CorSp) /= N_Package_Specification loop
2387 CorSp := Parent (CorSp);
2390 Check_List (Visible_Declarations (CorSp));
2394 Copy_Env (Current_Perm_Env,
2397 Check_List (Private_Declarations (CorSp));
2399 -- Set mode to Read, and then analyze declarations and statements
2401 Current_Checking_Mode := Read;
2403 Check_List (Declarations (Pack));
2404 Check_Node (Handled_Statement_Sequence (Pack));
2406 -- Check RW for every stateful variable (i.e. in declarations)
2408 Return_Declarations (Private_Declarations (CorSp));
2409 Return_Declarations (Visible_Declarations (CorSp));
2410 Return_Declarations (Declarations (Pack));
2412 -- Restore previous environment (i.e. delete every nonvisible
2413 -- declaration) from environment.
2415 Free_Env (Current_Perm_Env);
2416 Copy_Env (Saved_Env,
2418 end Check_Package_Body;
2424 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
2425 Mode : constant Entity_Kind := Ekind (Formal);
2426 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2429 case Current_Checking_Mode is
2431 case Formal_Kind'(Mode
) is
2432 when E_In_Parameter
=>
2433 if Is_Borrowed_In
(Formal
) then
2436 Current_Checking_Mode
:= Move
;
2443 when E_Out_Parameter
=>
2446 when E_In_Out_Parameter
=>
2449 Current_Checking_Mode
:= Move
;
2453 Check_Node
(Actual
);
2456 case Formal_Kind
'(Mode) is
2457 when E_In_Parameter =>
2460 when E_Out_Parameter
2461 | E_In_Out_Parameter
2463 -- Borrowed out or in out
2465 Process_Path (Actual);
2470 raise Program_Error;
2473 Current_Checking_Mode := Mode_Before;
2476 --------------------------
2477 -- Check_Param_Observes --
2478 --------------------------
2480 procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
2481 Mode : constant Entity_Kind := Ekind (Formal);
2482 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2486 when E_In_Parameter =>
2487 if not Is_Borrowed_In (Formal) then
2490 Current_Checking_Mode := Observe;
2491 Check_Node (Actual);
2499 Current_Checking_Mode := Mode_Before;
2500 end Check_Param_Observes;
2502 ----------------------
2503 -- Check_Param_Outs --
2504 ----------------------
2506 procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
2507 Mode : constant Entity_Kind := Ekind (Formal);
2508 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2513 when E_Out_Parameter =>
2515 Current_Checking_Mode := Borrow_Out;
2516 Check_Node (Actual);
2523 Current_Checking_Mode := Mode_Before;
2524 end Check_Param_Outs;
2526 ----------------------
2527 -- Check_Param_Read --
2528 ----------------------
2530 procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
2531 Mode : constant Entity_Kind := Ekind (Formal);
2534 pragma Assert (Current_Checking_Mode = Read);
2536 case Formal_Kind'(Mode
) is
2537 when E_In_Parameter
=>
2538 Check_Node
(Actual
);
2540 when E_Out_Parameter
2541 | E_In_Out_Parameter
2546 end Check_Param_Read
;
2548 -------------------------
2549 -- Check_Safe_Pointers --
2550 -------------------------
2552 procedure Check_Safe_Pointers
(N
: Node_Id
) is
2554 -- Local subprograms
2556 procedure Check_List
(L
: List_Id
);
2557 -- Call the main analysis procedure on each element of the list
2559 procedure Initialize
;
2560 -- Initialize global variables before starting the analysis of a body
2566 procedure Check_List
(L
: List_Id
) is
2570 while Present
(N
) loop
2571 Check_Safe_Pointers
(N
);
2580 procedure Initialize
is
2582 Reset
(Current_Loops_Envs
);
2583 Reset
(Current_Loops_Accumulators
);
2584 Reset
(Current_Perm_Env
);
2585 Reset
(Current_Initialization_Map
);
2591 -- SPARK_Mode pragma in application
2593 -- Start of processing for Check_Safe_Pointers
2599 when N_Compilation_Unit
=>
2600 Check_Safe_Pointers
(Unit
(N
));
2603 | N_Package_Declaration
2606 Prag
:= SPARK_Pragma
(Defining_Entity
(N
));
2607 if Present
(Prag
) then
2608 if Get_SPARK_Mode_From_Annotation
(Prag
) = Opt
.Off
then
2614 elsif Nkind
(N
) = N_Package_Body
then
2615 Check_List
(Declarations
(N
));
2617 elsif Nkind
(N
) = N_Package_Declaration
then
2618 Check_List
(Private_Declarations
(Specification
(N
)));
2619 Check_List
(Visible_Declarations
(Specification
(N
)));
2625 end Check_Safe_Pointers
;
2627 ---------------------
2628 -- Check_Statement --
2629 ---------------------
2631 procedure Check_Statement
(Stmt
: Node_Id
) is
2632 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2634 case N_Statement_Other_Than_Procedure_Call
'(Nkind (Stmt)) is
2635 when N_Entry_Call_Statement =>
2636 Check_Call_Statement (Stmt);
2638 -- Move right-hand side first, and then assign left-hand side
2640 when N_Assignment_Statement =>
2641 if Is_Deep (Etype (Expression (Stmt))) then
2642 Current_Checking_Mode := Move;
2644 Current_Checking_Mode := Read;
2647 Check_Node (Expression (Stmt));
2648 Current_Checking_Mode := Assign;
2649 Check_Node (Name (Stmt));
2651 when N_Block_Statement =>
2653 Saved_Env : Perm_Env;
2658 Copy_Env (Current_Perm_Env,
2661 -- Analyze declarations and Handled_Statement_Sequences
2663 Current_Checking_Mode := Read;
2664 Check_List (Declarations (Stmt));
2665 Check_Node (Handled_Statement_Sequence (Stmt));
2667 -- Restore environment
2669 Free_Env (Current_Perm_Env);
2670 Copy_Env (Saved_Env,
2674 when N_Case_Statement =>
2676 Saved_Env : Perm_Env;
2678 -- Accumulator for the different branches
2682 Elmt : Node_Id := First (Alternatives (Stmt));
2685 Current_Checking_Mode := Read;
2686 Check_Node (Expression (Stmt));
2687 Current_Checking_Mode := Mode_Before;
2691 Copy_Env (Current_Perm_Env,
2694 -- Here we have the original env in saved, current with a fresh
2695 -- copy, and new aliased.
2697 -- First alternative
2702 Copy_Env (Current_Perm_Env,
2704 Free_Env (Current_Perm_Env);
2706 -- Other alternatives
2708 while Present (Elmt) loop
2709 -- Restore environment
2711 Copy_Env (Saved_Env,
2716 -- Merge Current_Perm_Env into New_Env
2718 Merge_Envs (New_Env,
2729 Free_Env (Saved_Env);
2732 when N_Delay_Relative_Statement =>
2733 Check_Node (Expression (Stmt));
2735 when N_Delay_Until_Statement =>
2736 Check_Node (Expression (Stmt));
2738 when N_Loop_Statement =>
2739 Check_Loop_Statement (Stmt);
2741 -- If deep type expression, then move, else read
2743 when N_Simple_Return_Statement =>
2744 case Nkind (Expression (Stmt)) is
2747 -- ??? This does not take into account the fact that
2748 -- a simple return inside an extended return statement
2749 -- applies to the extended return statement.
2750 Subp : constant Entity_Id :=
2751 Return_Applies_To (Return_Statement_Entity (Stmt));
2753 Return_Parameters (Subp);
2754 Return_Globals (Subp);
2758 if Is_Deep (Etype (Expression (Stmt))) then
2759 Current_Checking_Mode := Move;
2760 elsif Is_Shallow (Etype (Expression (Stmt))) then
2761 Current_Checking_Mode := Read;
2763 raise Program_Error;
2766 Check_Node (Expression (Stmt));
2769 when N_Extended_Return_Statement =>
2770 Check_List (Return_Object_Declarations (Stmt));
2771 Check_Node (Handled_Statement_Sequence (Stmt));
2773 Return_Declarations (Return_Object_Declarations (Stmt));
2776 -- ??? This does not take into account the fact that a simple
2777 -- return inside an extended return statement applies to the
2778 -- extended return statement.
2779 Subp : constant Entity_Id :=
2780 Return_Applies_To (Return_Statement_Entity (Stmt));
2782 Return_Parameters (Subp);
2783 Return_Globals (Subp);
2786 -- Merge the current_Perm_Env with the accumulator for the given loop
2788 when N_Exit_Statement =>
2790 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
2792 Saved_Accumulator : constant Perm_Env_Access :=
2793 Get (Current_Loops_Accumulators, Loop_Name);
2795 Environment_Copy : constant Perm_Env_Access :=
2799 Copy_Env (Current_Perm_Env,
2800 Environment_Copy.all);
2802 if Saved_Accumulator = null then
2803 Set (Current_Loops_Accumulators,
2804 Loop_Name, Environment_Copy);
2806 Merge_Envs (Saved_Accumulator.all,
2807 Environment_Copy.all);
2811 -- Copy environment, run on each branch, and then merge
2813 when N_If_Statement =>
2815 Saved_Env : Perm_Env;
2817 -- Accumulator for the different branches
2823 Check_Node (Condition (Stmt));
2827 Copy_Env (Current_Perm_Env,
2830 -- Here we have the original env in saved, current with a fresh
2835 Check_List (Then_Statements (Stmt));
2837 Copy_Env (Current_Perm_Env,
2840 Free_Env (Current_Perm_Env);
2842 -- Here the new_environment contains curr env after then block
2849 Elmt := First (Elsif_Parts (Stmt));
2850 while Present (Elmt) loop
2851 -- Transfer into accumulator, and restore from save
2853 Copy_Env (Saved_Env,
2856 Check_Node (Condition (Elmt));
2857 Check_List (Then_Statements (Stmt));
2859 -- Merge Current_Perm_Env into New_Env
2861 Merge_Envs (New_Env,
2870 -- Restore environment before if
2872 Copy_Env (Saved_Env,
2875 -- Here new environment contains the environment after then and
2876 -- current the fresh copy of old one.
2878 Check_List (Else_Statements (Stmt));
2880 Merge_Envs (New_Env,
2889 Free_Env (Saved_Env);
2892 -- Unsupported constructs in SPARK
2894 when N_Abort_Statement
2895 | N_Accept_Statement
2896 | N_Asynchronous_Select
2898 | N_Conditional_Entry_Call
2900 | N_Requeue_Statement
2901 | N_Selective_Accept
2902 | N_Timed_Entry_Call
2904 Error_Msg_N ("unsupported construct in SPARK", Stmt);
2906 -- Ignored constructs for pointer checking
2908 when N_Null_Statement
2913 -- The following nodes are never generated in GNATprove mode
2915 when N_Compound_Statement
2918 raise Program_Error;
2920 end Check_Statement;
2926 function Get_Perm (N : Node_Id) return Perm_Kind is
2927 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
2930 case Tree_Or_Perm.R is
2932 return Tree_Or_Perm.Found_Permission;
2935 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
2936 return Permission (Tree_Or_Perm.Tree_Access);
2938 -- We encoutered a function call, hence the memory area is fresh,
2939 -- which means that the association permission is RW.
2941 when Function_Call =>
2947 ----------------------
2948 -- Get_Perm_Or_Tree --
2949 ----------------------
2951 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
2955 -- Base identifier. Normally those are the roots of the trees stored
2956 -- in the permission environment.
2958 when N_Defining_Identifier =>
2959 raise Program_Error;
2965 P : constant Entity_Id := Entity (N);
2967 C : constant Perm_Tree_Access :=
2968 Get (Current_Perm_Env, Unique_Entity (P));
2971 -- Setting the initialization map to True, so that this
2972 -- variable cannot be ignored anymore when looking at end
2973 -- of elaboration of package.
2975 Set (Current_Initialization_Map, Unique_Entity (P), True);
2978 -- No null possible here, there are no parents for the path.
2979 -- This means we are using a global variable without adding
2980 -- it in environment with a global aspect.
2982 Illegal_Global_Usage (N);
2984 return (R => Unfolded, Tree_Access => C);
2988 when N_Type_Conversion
2989 | N_Unchecked_Type_Conversion
2990 | N_Qualified_Expression
2992 return Get_Perm_Or_Tree (Expression (N));
2994 -- Happening when we try to get the permission of a variable that
2995 -- is a formal parameter. We get instead the defining identifier
2996 -- associated with the parameter (which is the one that has been
2997 -- stored for indexing).
2999 when N_Parameter_Specification =>
3000 return Get_Perm_Or_Tree (Defining_Identifier (N));
3002 -- We get the permission tree of its prefix, and then get either the
3003 -- subtree associated with that specific selection, or if we have a
3004 -- leaf that folds its children, we take the children's permission
3005 -- and return it using the discriminant Folded.
3007 when N_Selected_Component =>
3009 C : constant Perm_Or_Tree :=
3010 Get_Perm_Or_Tree (Prefix (N));
3020 pragma Assert (C.Tree_Access /= null);
3022 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3024 Kind (C.Tree_Access) = Record_Component);
3026 if Kind (C.Tree_Access) = Record_Component then
3028 Selected_Component : constant Entity_Id :=
3029 Entity (Selector_Name (N));
3031 Selected_C : constant Perm_Tree_Access :=
3033 (Component (C.Tree_Access), Selected_Component);
3036 if Selected_C = null then
3037 return (R => Unfolded,
3039 Other_Components (C.Tree_Access));
3041 return (R => Unfolded,
3042 Tree_Access => Selected_C);
3045 elsif Kind (C.Tree_Access) = Entire_Object then
3046 return (R => Folded, Found_Permission =>
3047 Children_Permission (C.Tree_Access));
3049 raise Program_Error;
3054 -- We get the permission tree of its prefix, and then get either the
3055 -- subtree associated with that specific selection, or if we have a
3056 -- leaf that folds its children, we take the children's permission
3057 -- and return it using the discriminant Folded.
3059 when N_Indexed_Component
3063 C : constant Perm_Or_Tree :=
3064 Get_Perm_Or_Tree (Prefix (N));
3074 pragma Assert (C.Tree_Access /= null);
3076 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3078 Kind (C.Tree_Access) = Array_Component);
3080 if Kind (C.Tree_Access) = Array_Component then
3081 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3083 return (R => Unfolded,
3084 Tree_Access => Get_Elem (C.Tree_Access));
3085 elsif Kind (C.Tree_Access) = Entire_Object then
3086 return (R => Folded, Found_Permission =>
3087 Children_Permission (C.Tree_Access));
3089 raise Program_Error;
3094 -- We get the permission tree of its prefix, and then get either the
3095 -- subtree associated with that specific selection, or if we have a
3096 -- leaf that folds its children, we take the children's permission
3097 -- and return it using the discriminant Folded.
3099 when N_Explicit_Dereference =>
3101 C : constant Perm_Or_Tree :=
3102 Get_Perm_Or_Tree (Prefix (N));
3112 pragma Assert (C.Tree_Access /= null);
3114 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3116 Kind (C.Tree_Access) = Reference);
3118 if Kind (C.Tree_Access) = Reference then
3119 if Get_All (C.Tree_Access) = null then
3121 raise Program_Error;
3125 Tree_Access => Get_All (C.Tree_Access));
3127 elsif Kind (C.Tree_Access) = Entire_Object then
3128 return (R => Folded, Found_Permission =>
3129 Children_Permission (C.Tree_Access));
3131 raise Program_Error;
3136 -- The name contains a function call, hence the given path is always
3137 -- new. We do not have to check for anything.
3139 when N_Function_Call =>
3140 return (R => Function_Call);
3143 raise Program_Error;
3145 end Get_Perm_Or_Tree;
3151 function Get_Perm_Tree
3153 return Perm_Tree_Access
3158 -- Base identifier. Normally those are the roots of the trees stored
3159 -- in the permission environment.
3161 when N_Defining_Identifier =>
3162 raise Program_Error;
3168 P : constant Node_Id := Entity (N);
3170 C : constant Perm_Tree_Access :=
3171 Get (Current_Perm_Env, Unique_Entity (P));
3174 -- Setting the initialization map to True, so that this
3175 -- variable cannot be ignored anymore when looking at end
3176 -- of elaboration of package.
3178 Set (Current_Initialization_Map, Unique_Entity (P), True);
3181 -- No null possible here, there are no parents for the path.
3182 -- This means we are using a global variable without adding
3183 -- it in environment with a global aspect.
3185 Illegal_Global_Usage (N);
3191 when N_Type_Conversion
3192 | N_Unchecked_Type_Conversion
3193 | N_Qualified_Expression
3195 return Get_Perm_Tree (Expression (N));
3197 when N_Parameter_Specification =>
3198 return Get_Perm_Tree (Defining_Identifier (N));
3200 -- We get the permission tree of its prefix, and then get either the
3201 -- subtree associated with that specific selection, or if we have a
3202 -- leaf that folds its children, we unroll it in one step.
3204 when N_Selected_Component =>
3206 C : constant Perm_Tree_Access :=
3207 Get_Perm_Tree (Prefix (N));
3211 -- If null then it means we went through a function call
3216 pragma Assert (Kind (C) = Entire_Object
3217 or else Kind (C) = Record_Component);
3219 if Kind (C) = Record_Component then
3220 -- The tree is unfolded. We just return the subtree.
3223 Selected_Component : constant Entity_Id :=
3224 Entity (Selector_Name (N));
3225 Selected_C : constant Perm_Tree_Access :=
3227 (Component (C), Selected_Component);
3230 if Selected_C = null then
3231 return Other_Components (C);
3236 elsif Kind (C) = Entire_Object then
3238 -- Expand the tree. Replace the node with
3239 -- Record_Component.
3243 -- Create the unrolled nodes
3245 Son : Perm_Tree_Access;
3247 Child_Perm : constant Perm_Kind :=
3248 Children_Permission (C);
3252 -- We change the current node from Entire_Object to
3253 -- Record_Component with same permission and an empty
3254 -- hash table as component list.
3257 (Kind => Record_Component,
3258 Is_Node_Deep => Is_Node_Deep (C),
3259 Permission => Permission (C),
3260 Component => Perm_Tree_Maps.Nil,
3262 new Perm_Tree_Wrapper'
3264 (Kind
=> Entire_Object
,
3265 -- Is_Node_Deep is true, to be conservative
3266 Is_Node_Deep
=> True,
3267 Permission
=> Child_Perm
,
3268 Children_Permission
=> Child_Perm
)
3272 -- We fill the hash table with all sons of the record,
3273 -- with basic Entire_Objects nodes.
3274 Elem
:= First_Component_Or_Discriminant
3275 (Etype
(Prefix
(N
)));
3277 while Present
(Elem
) loop
3278 Son
:= new Perm_Tree_Wrapper
'
3280 (Kind => Entire_Object,
3281 Is_Node_Deep => Is_Deep (Etype (Elem)),
3282 Permission => Child_Perm,
3283 Children_Permission => Child_Perm));
3286 (C.all.Tree.Component, Elem, Son);
3288 Next_Component_Or_Discriminant (Elem);
3291 -- we return the tree to the sons, so that the recursion
3295 Selected_Component : constant Entity_Id :=
3296 Entity (Selector_Name (N));
3298 Selected_C : constant Perm_Tree_Access :=
3300 (Component (C), Selected_Component);
3303 pragma Assert (Selected_C /= null);
3310 raise Program_Error;
3314 -- We set the permission tree of its prefix, and then we extract from
3315 -- the returned pointer the subtree. If folded, we unroll the tree at
3318 when N_Indexed_Component
3322 C : constant Perm_Tree_Access :=
3323 Get_Perm_Tree (Prefix (N));
3327 -- If null then we went through a function call
3332 pragma Assert (Kind (C) = Entire_Object
3333 or else Kind (C) = Array_Component);
3335 if Kind (C) = Array_Component then
3336 -- The tree is unfolded. We just return the elem subtree
3338 pragma Assert (Get_Elem (C) = null);
3340 return Get_Elem (C);
3341 elsif Kind (C) = Entire_Object then
3343 -- Expand the tree. Replace node with Array_Component.
3345 Son : Perm_Tree_Access;
3348 Son := new Perm_Tree_Wrapper'
3350 (Kind
=> Entire_Object
,
3351 Is_Node_Deep
=> Is_Node_Deep
(C
),
3352 Permission
=> Children_Permission
(C
),
3353 Children_Permission
=> Children_Permission
(C
)));
3355 -- We change the current node from Entire_Object
3356 -- to Array_Component with same permission and the
3357 -- previously defined son.
3359 C
.all.Tree
:= (Kind
=> Array_Component
,
3360 Is_Node_Deep
=> Is_Node_Deep
(C
),
3361 Permission
=> Permission
(C
),
3364 return Get_Elem
(C
);
3367 raise Program_Error
;
3371 -- We get the permission tree of its prefix, and then get either the
3372 -- subtree associated with that specific selection, or if we have a
3373 -- leaf that folds its children, we unroll the tree.
3375 when N_Explicit_Dereference
=>
3377 C
: Perm_Tree_Access
;
3380 C
:= Get_Perm_Tree
(Prefix
(N
));
3383 -- If null, we went through a function call
3388 pragma Assert
(Kind
(C
) = Entire_Object
3389 or else Kind
(C
) = Reference
);
3391 if Kind
(C
) = Reference
then
3392 -- The tree is unfolded. We return the elem subtree
3394 if Get_All
(C
) = null then
3396 raise Program_Error
;
3400 elsif Kind
(C
) = Entire_Object
then
3402 -- Expand the tree. Replace the node with Reference.
3404 Son
: Perm_Tree_Access
;
3407 Son
:= new Perm_Tree_Wrapper
'
3409 (Kind => Entire_Object,
3410 Is_Node_Deep => Is_Deep (Etype (N)),
3411 Permission => Children_Permission (C),
3412 Children_Permission => Children_Permission (C)));
3414 -- We change the current node from Entire_Object to
3415 -- Reference with same permission and the previous son.
3417 pragma Assert (Is_Node_Deep (C));
3419 C.all.Tree := (Kind => Reference,
3420 Is_Node_Deep => Is_Node_Deep (C),
3421 Permission => Permission (C),
3427 raise Program_Error;
3431 -- No permission tree for function calls
3433 when N_Function_Call =>
3437 raise Program_Error;
3445 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
3487 function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
3488 function Has_Alias_Deep (Typ : Entity_Id) return Boolean
3493 if Is_Array_Type (Typ)
3494 and then Has_Aliased_Components (Typ)
3498 -- Note: Has_Aliased_Components applies only to arrays
3500 elsif Is_Record_Type (Typ) then
3501 -- It is possible to have an aliased discriminant, so they must be
3502 -- checked along with normal components.
3504 Comp := First_Component_Or_Discriminant (Typ);
3505 while Present (Comp) loop
3506 if Is_Aliased (Comp)
3507 or else Is_Aliased (Etype (Comp))
3512 if Has_Alias_Deep (Etype (Comp)) then
3516 Next_Component_Or_Discriminant (Comp);
3520 return Is_Aliased (Typ);
3530 return Has_Alias_Deep (Etype (N));
3532 when N_Defining_Identifier =>
3533 return Has_Alias_Deep (Etype (N));
3535 when N_Type_Conversion
3536 | N_Unchecked_Type_Conversion
3537 | N_Qualified_Expression
3539 return Has_Alias (Expression (N));
3541 when N_Parameter_Specification =>
3542 return Has_Alias (Defining_Identifier (N));
3544 when N_Selected_Component =>
3545 case Nkind (Selector_Name (N)) is
3546 when N_Identifier =>
3547 if Is_Aliased (Entity (Selector_Name (N))) then
3551 when others => null;
3555 return Has_Alias (Prefix (N));
3557 when N_Indexed_Component
3560 return Has_Alias (Prefix (N));
3562 when N_Explicit_Dereference =>
3565 when N_Function_Call =>
3568 when N_Attribute_Reference =>
3569 if Is_Deep (Etype (Prefix (N))) then
3570 raise Program_Error;
3579 -------------------------
3580 -- Has_Array_Component --
3581 -------------------------
3583 function Has_Array_Component (N : Node_Id) return Boolean is
3586 -- Base identifier. There is no array component here.
3590 | N_Defining_Identifier
3594 -- We check if the expression inside the conversion has an array
3597 when N_Type_Conversion
3598 | N_Unchecked_Type_Conversion
3599 | N_Qualified_Expression
3601 return Has_Array_Component (Expression (N));
3603 -- We check if the prefix has an array component
3605 when N_Selected_Component =>
3606 return Has_Array_Component (Prefix (N));
3608 -- We found the array component, return True
3610 when N_Indexed_Component
3615 -- We check if the prefix has an array component
3617 when N_Explicit_Dereference =>
3618 return Has_Array_Component (Prefix (N));
3620 when N_Function_Call =>
3624 raise Program_Error;
3626 end Has_Array_Component;
3628 ----------------------------
3629 -- Has_Function_Component --
3630 ----------------------------
3632 function Has_Function_Component (N : Node_Id) return Boolean is
3635 -- Base identifier. There is no function component here.
3639 | N_Defining_Identifier
3643 -- We check if the expression inside the conversion has a function
3646 when N_Type_Conversion
3647 | N_Unchecked_Type_Conversion
3648 | N_Qualified_Expression
3650 return Has_Function_Component (Expression (N));
3652 -- We check if the prefix has a function component
3654 when N_Selected_Component =>
3655 return Has_Function_Component (Prefix (N));
3657 -- We check if the prefix has a function component
3659 when N_Indexed_Component
3662 return Has_Function_Component (Prefix (N));
3664 -- We check if the prefix has a function component
3666 when N_Explicit_Dereference =>
3667 return Has_Function_Component (Prefix (N));
3669 -- We found the function component, return True
3671 when N_Function_Call =>
3675 raise Program_Error;
3678 end Has_Function_Component;
3684 procedure Hp (P : Perm_Env) is
3685 Elem : Perm_Tree_Maps.Key_Option;
3688 Elem := Get_First_Key (P);
3689 while Elem.Present loop
3690 Print_Node_Briefly (Elem.K);
3691 Elem := Get_Next_Key (P);
3695 --------------------------
3696 -- Illegal_Global_Usage --
3697 --------------------------
3699 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
3701 Error_Msg_NE ("cannot use global variable & of deep type", N, N);
3702 Error_Msg_N ("\without prior declaration in a Global aspect", N);
3704 Errout.Finalize (Last_Call => True);
3705 Errout.Output_Messages;
3706 Exit_Program (E_Errors);
3707 end Illegal_Global_Usage;
3709 --------------------
3710 -- Is_Borrowed_In --
3711 --------------------
3713 function Is_Borrowed_In (E : Entity_Id) return Boolean is
3715 return Is_Access_Type (Etype (E))
3716 and then not Is_Access_Constant (Etype (E));
3723 function Is_Deep (E : Entity_Id) return Boolean is
3724 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
3726 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
3728 Pack_Decl : Node_Id;
3731 if Is_Itype (E) then
3732 Decl := Associated_Node_For_Itype (E);
3737 Pack_Decl := Parent (Parent (Decl));
3739 if Nkind (Pack_Decl) /= N_Package_Declaration then
3744 Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
3745 and then Get_SPARK_Mode_From_Annotation
3746 (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
3747 end Is_Private_Entity_Mode_Off;
3749 pragma Assert (Is_Type (E));
3758 -- Just check the depth of its component type
3763 return Is_Deep (Component_Type (E));
3765 when E_String_Literal_Subtype =>
3768 -- Per RM 8.11 for class-wide types
3770 when E_Class_Wide_Subtype
3775 -- ??? What about hidden components
3784 Elmt := First_Component_Or_Discriminant (E);
3785 while Present (Elmt) loop
3786 if Is_Deep (Etype (Elmt)) then
3789 Next_Component_Or_Discriminant (Elmt);
3796 when Private_Kind =>
3797 if Is_Private_Entity_Mode_Off (E) then
3800 if Present (Full_View (E)) then
3801 return Is_Deep (Full_View (E));
3807 when E_Incomplete_Type =>
3810 when E_Incomplete_Subtype =>
3813 -- No problem with synchronized types
3815 when E_Protected_Type
3816 | E_Protected_Subtype
3822 when E_Exception_Type =>
3826 raise Program_Error;
3834 function Is_Shallow (E : Entity_Id) return Boolean is
3836 pragma Assert (Is_Type (E));
3837 return not Is_Deep (E);
3844 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
3845 Nam : Node_Id := Name (N);
3846 Stmt : Node_Id := N;
3849 while Present (Stmt) loop
3850 Stmt := Parent (Stmt);
3851 if Nkind (Stmt) = N_Loop_Statement then
3852 Nam := Identifier (Stmt);
3857 return Entity (Nam);
3863 function Lub (P1, P2 : Perm_Kind) return Perm_Kind
3901 procedure Merge_Envs
3902 (Target : in out Perm_Env;
3903 Source : in out Perm_Env)
3905 procedure Merge_Trees
3906 (Target : Perm_Tree_Access;
3907 Source : Perm_Tree_Access);
3909 procedure Merge_Trees
3910 (Target : Perm_Tree_Access;
3911 Source : Perm_Tree_Access)
3913 procedure Apply_Glb_Tree
3914 (A : Perm_Tree_Access;
3917 procedure Apply_Glb_Tree
3918 (A : Perm_Tree_Access;
3922 A.all.Tree.Permission := Glb (Permission (A), P);
3925 when Entire_Object =>
3926 A.all.Tree.Children_Permission :=
3927 Glb (Children_Permission (A), P);
3930 Apply_Glb_Tree (Get_All (A), P);
3932 when Array_Component =>
3933 Apply_Glb_Tree (Get_Elem (A), P);
3935 when Record_Component =>
3937 Comp : Perm_Tree_Access;
3939 Comp := Perm_Tree_Maps.Get_First (Component (A));
3940 while Comp /= null loop
3941 Apply_Glb_Tree (Comp, P);
3942 Comp := Perm_Tree_Maps.Get_Next (Component (A));
3945 Apply_Glb_Tree (Other_Components (A), P);
3950 Perm : constant Perm_Kind :=
3951 Glb (Permission (Target), Permission (Source));
3954 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
3955 Target.all.Tree.Permission := Perm;
3957 case Kind (Target) is
3958 when Entire_Object =>
3960 Child_Perm : constant Perm_Kind :=
3961 Children_Permission (Target);
3964 case Kind (Source) is
3965 when Entire_Object =>
3966 Target.all.Tree.Children_Permission :=
3967 Glb (Child_Perm, Children_Permission (Source));
3970 Copy_Tree (Source, Target);
3971 Target.all.Tree.Permission := Perm;
3972 Apply_Glb_Tree (Get_All (Target), Child_Perm);
3974 when Array_Component =>
3975 Copy_Tree (Source, Target);
3976 Target.all.Tree.Permission := Perm;
3977 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
3979 when Record_Component =>
3980 Copy_Tree (Source, Target);
3981 Target.all.Tree.Permission := Perm;
3983 Comp : Perm_Tree_Access;
3987 Perm_Tree_Maps.Get_First (Component (Target));
3988 while Comp /= null loop
3989 -- Apply glb tree on every component subtree
3991 Apply_Glb_Tree (Comp, Child_Perm);
3992 Comp := Perm_Tree_Maps.Get_Next
3993 (Component (Target));
3996 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4001 case Kind (Source) is
4002 when Entire_Object =>
4003 Apply_Glb_Tree (Get_All (Target),
4004 Children_Permission (Source));
4007 Merge_Trees (Get_All (Target), Get_All (Source));
4010 raise Program_Error;
4014 when Array_Component =>
4015 case Kind (Source) is
4016 when Entire_Object =>
4017 Apply_Glb_Tree (Get_Elem (Target),
4018 Children_Permission (Source));
4020 when Array_Component =>
4021 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4024 raise Program_Error;
4028 when Record_Component =>
4029 case Kind (Source) is
4030 when Entire_Object =>
4032 Child_Perm : constant Perm_Kind :=
4033 Children_Permission (Source);
4035 Comp : Perm_Tree_Access;
4038 Comp := Perm_Tree_Maps.Get_First
4039 (Component (Target));
4040 while Comp /= null loop
4041 -- Apply glb tree on every component subtree
4043 Apply_Glb_Tree (Comp, Child_Perm);
4045 Perm_Tree_Maps.Get_Next (Component (Target));
4047 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4050 when Record_Component =>
4052 Key_Source : Perm_Tree_Maps.Key_Option;
4053 CompTarget : Perm_Tree_Access;
4054 CompSource : Perm_Tree_Access;
4057 Key_Source := Perm_Tree_Maps.Get_First_Key
4058 (Component (Source));
4060 while Key_Source.Present loop
4061 CompSource := Perm_Tree_Maps.Get
4062 (Component (Source), Key_Source.K);
4063 CompTarget := Perm_Tree_Maps.Get
4064 (Component (Target), Key_Source.K);
4066 pragma Assert (CompSource /= null);
4067 Merge_Trees (CompTarget, CompSource);
4069 Key_Source := Perm_Tree_Maps.Get_Next_Key
4070 (Component (Source));
4073 Merge_Trees (Other_Components (Target),
4074 Other_Components (Source));
4078 raise Program_Error;
4084 CompTarget : Perm_Tree_Access;
4085 CompSource : Perm_Tree_Access;
4086 KeyTarget : Perm_Tree_Maps.Key_Option;
4089 KeyTarget := Get_First_Key (Target);
4090 -- Iterate over every tree of the environment in the target, and merge
4091 -- it with the source if there is such a similar one that exists. If
4092 -- there is none, then skip.
4093 while KeyTarget.Present loop
4095 CompSource := Get (Source, KeyTarget.K);
4096 CompTarget := Get (Target, KeyTarget.K);
4098 pragma Assert (CompTarget /= null);
4100 if CompSource /= null then
4101 Merge_Trees (CompTarget, CompSource);
4102 Remove (Source, KeyTarget.K);
4105 KeyTarget := Get_Next_Key (Target);
4108 -- Iterate over every tree of the environment of the source. And merge
4109 -- again. If there is not any tree of the target then just copy the tree
4110 -- from source to target.
4112 KeySource : Perm_Tree_Maps.Key_Option;
4114 KeySource := Get_First_Key (Source);
4115 while KeySource.Present loop
4117 CompSource := Get (Source, KeySource.K);
4118 CompTarget := Get (Target, KeySource.K);
4120 if CompTarget = null then
4121 CompTarget := new Perm_Tree_Wrapper'(CompSource
.all);
4122 Copy_Tree
(CompSource
, CompTarget
);
4123 Set
(Target
, KeySource
.K
, CompTarget
);
4125 Merge_Trees
(CompTarget
, CompSource
);
4128 KeySource
:= Get_Next_Key
(Source
);
4139 procedure Perm_Error
4142 Found_Perm
: Perm_Kind
)
4144 procedure Set_Root_Object
4146 Obj
: out Entity_Id
;
4147 Deref
: out Boolean);
4148 -- Set the root object Obj, and whether the path contains a dereference,
4149 -- from a path Path.
4151 ---------------------
4152 -- Set_Root_Object --
4153 ---------------------
4155 procedure Set_Root_Object
4157 Obj
: out Entity_Id
;
4158 Deref
: out Boolean)
4161 case Nkind
(Path
) is
4165 Obj
:= Entity
(Path
);
4168 when N_Type_Conversion
4169 | N_Unchecked_Type_Conversion
4170 | N_Qualified_Expression
4172 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
4174 when N_Indexed_Component
4175 | N_Selected_Component
4178 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4180 when N_Explicit_Dereference
=>
4181 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4185 raise Program_Error
;
4187 end Set_Root_Object
;
4194 -- Start of processing for Perm_Error
4197 Set_Root_Object
(N
, Root
, Is_Deref
);
4201 ("insufficient permission on dereference from &", N
, Root
);
4203 Error_Msg_NE
("insufficient permission for &", N
, Root
);
4206 Perm_Mismatch
(Perm
, Found_Perm
, N
);
4209 -------------------------------
4210 -- Perm_Error_Subprogram_End --
4211 -------------------------------
4213 procedure Perm_Error_Subprogram_End
4217 Found_Perm
: Perm_Kind
)
4220 Error_Msg_Node_2
:= Subp
;
4221 Error_Msg_NE
("insufficient permission for & when returning from &",
4223 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
4224 end Perm_Error_Subprogram_End
;
4230 procedure Process_Path
(N
: Node_Id
) is
4231 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
4233 -- We ignore if yielding to synchronized
4236 and then Is_Synchronized_Object
(Root
)
4241 -- We ignore shallow unaliased. They are checked in flow analysis,
4242 -- allowing backward compatibility.
4244 if not Has_Alias
(N
)
4245 and then Is_Shallow
(Etype
(N
))
4251 Perm_N
: constant Perm_Kind
:= Get_Perm
(N
);
4255 case Current_Checking_Mode
is
4256 -- Check permission R, do nothing
4259 if Perm_N
not in Read_Perm
then
4260 Perm_Error
(N
, Read_Only
, Perm_N
);
4263 -- If shallow type no need for RW, only R
4266 if Is_Shallow
(Etype
(N
)) then
4267 if Perm_N
not in Read_Perm
then
4268 Perm_Error
(N
, Read_Only
, Perm_N
);
4271 -- Check permission RW if deep
4273 if Perm_N
/= Read_Write
then
4274 Perm_Error
(N
, Read_Write
, Perm_N
);
4278 -- Set permission to W to the path and any of its prefix
4280 Tree
: constant Perm_Tree_Access
:=
4281 Set_Perm_Prefixes_Move
(N
, Move
);
4285 -- We went through a function call, no permission to
4291 -- Set permissions to
4292 -- No for any extension with more .all
4293 -- W for any deep extension with same number of .all
4294 -- RW for any shallow extension with same number of .all
4296 Set_Perm_Extensions_Move
(Tree
, Etype
(N
));
4300 -- Check permission RW
4303 if Perm_N
/= Read_Write
then
4304 Perm_Error
(N
, Read_Write
, Perm_N
);
4308 -- Set permission to No to the path and any of its prefix up
4309 -- to the first .all and then W.
4311 Tree
: constant Perm_Tree_Access
:=
4312 Set_Perm_Prefixes_Move
(N
, Super_Move
);
4316 -- We went through a function call, no permission to
4322 -- Set permissions to No on any strict extension of the path
4324 Set_Perm_Extensions
(Tree
, No_Access
);
4327 -- Check permission W
4330 if Perm_N
not in Write_Perm
then
4331 Perm_Error
(N
, Write_Only
, Perm_N
);
4334 -- If the tree has an array component, then the permissions do
4335 -- not get modified by the assignment.
4337 if Has_Array_Component
(N
) then
4341 -- Same if has function component
4343 if Has_Function_Component
(N
) then
4348 -- Get the permission tree for the path
4350 Tree
: constant Perm_Tree_Access
:=
4353 Dummy
: Perm_Tree_Access
;
4357 -- We went through a function call, no permission to
4363 -- Set permission RW for it and all of its extensions
4365 Tree
.all.Tree
.Permission
:= Read_Write
;
4367 Set_Perm_Extensions
(Tree
, Read_Write
);
4369 -- Normalize the permission tree
4371 Dummy
:= Set_Perm_Prefixes_Assign
(N
);
4374 -- Check permission W
4377 if Perm_N
not in Write_Perm
then
4378 Perm_Error
(N
, Write_Only
, Perm_N
);
4382 -- Set permission to No to the path and any of its prefixes
4384 Tree
: constant Perm_Tree_Access
:=
4385 Set_Perm_Prefixes_Borrow_Out
(N
);
4389 -- We went through a function call, no permission to
4395 -- Set permissions to No on any strict extension of the path
4397 Set_Perm_Extensions
(Tree
, No_Access
);
4401 if Perm_N
not in Read_Perm
then
4402 Perm_Error
(N
, Read_Only
, Perm_N
);
4405 if Is_By_Copy_Type
(Etype
(N
)) then
4410 -- Set permission to No on the path and any of its prefixes
4412 Tree
: constant Perm_Tree_Access
:=
4413 Set_Perm_Prefixes_Observe
(N
);
4417 -- We went through a function call, no permission to
4423 -- Set permissions to No on any strict extension of the path
4425 Set_Perm_Extensions
(Tree
, Read_Only
);
4431 -------------------------
4432 -- Return_Declarations --
4433 -------------------------
4435 procedure Return_Declarations
(L
: List_Id
) is
4437 procedure Return_Declaration
(Decl
: Node_Id
);
4438 -- Check correct permissions for every declared object
4440 ------------------------
4441 -- Return_Declaration --
4442 ------------------------
4444 procedure Return_Declaration
(Decl
: Node_Id
) is
4446 if Nkind
(Decl
) = N_Object_Declaration
then
4447 -- Check RW for object declared, unless the object has never been
4450 if Get
(Current_Initialization_Map
,
4451 Unique_Entity
(Defining_Identifier
(Decl
))) = False
4456 -- We ignore shallow unaliased. They are checked in flow analysis,
4457 -- allowing backward compatibility.
4459 if not Has_Alias
(Defining_Identifier
(Decl
))
4460 and then Is_Shallow
(Etype
(Defining_Identifier
(Decl
)))
4466 Elem
: constant Perm_Tree_Access
:=
4467 Get
(Current_Perm_Env
,
4468 Unique_Entity
(Defining_Identifier
(Decl
)));
4472 -- Here we are on a declaration. Hence it should have been
4473 -- added in the environment when analyzing this node with
4474 -- mode Read. Hence it is not possible to find a null
4478 raise Program_Error
;
4481 if Permission
(Elem
) /= Read_Write
then
4482 Perm_Error
(Decl
, Read_Write
, Permission
(Elem
));
4486 end Return_Declaration
;
4492 -- Start of processing for Return_Declarations
4496 while Present
(N
) loop
4497 Return_Declaration
(N
);
4500 end Return_Declarations
;
4502 --------------------
4503 -- Return_Globals --
4504 --------------------
4506 procedure Return_Globals
(Subp
: Entity_Id
) is
4508 procedure Return_Globals_From_List
4509 (First_Item
: Node_Id
;
4510 Kind
: Formal_Kind
);
4511 -- Return global items from the list starting at Item
4513 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
4514 -- Return global items for the mode Global_Mode
4516 ------------------------------
4517 -- Return_Globals_From_List --
4518 ------------------------------
4520 procedure Return_Globals_From_List
4521 (First_Item
: Node_Id
;
4524 Item
: Node_Id
:= First_Item
;
4528 while Present
(Item
) loop
4531 -- Ignore abstract states, which play no role in pointer aliasing
4533 if Ekind
(E
) = E_Abstract_State
then
4536 Return_Parameter_Or_Global
(E
, Kind
, Subp
);
4540 end Return_Globals_From_List
;
4542 ----------------------------
4543 -- Return_Globals_Of_Mode --
4544 ----------------------------
4546 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
4551 when Name_Input | Name_Proof_In
=>
4552 Kind
:= E_In_Parameter
;
4554 Kind
:= E_Out_Parameter
;
4556 Kind
:= E_In_Out_Parameter
;
4558 raise Program_Error
;
4561 -- Return both global items from Global and Refined_Global pragmas
4563 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
4564 Return_Globals_From_List
4565 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
4566 end Return_Globals_Of_Mode
;
4568 -- Start of processing for Return_Globals
4571 Return_Globals_Of_Mode
(Name_Proof_In
);
4572 Return_Globals_Of_Mode
(Name_Input
);
4573 Return_Globals_Of_Mode
(Name_Output
);
4574 Return_Globals_Of_Mode
(Name_In_Out
);
4577 --------------------------------
4578 -- Return_Parameter_Or_Global --
4579 --------------------------------
4581 procedure Return_Parameter_Or_Global
4586 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
4587 pragma Assert
(Elem
/= null);
4590 -- Shallow unaliased parameters and globals cannot introduce pointer
4593 if not Has_Alias
(Id
) and then Is_Shallow
(Etype
(Id
)) then
4596 -- Observed IN parameters and globals need not return a permission to
4599 elsif Mode
= E_In_Parameter
and then not Is_Borrowed_In
(Id
) then
4602 -- All other parameters and globals should return with mode RW to the
4606 if Permission
(Elem
) /= Read_Write
then
4607 Perm_Error_Subprogram_End
4611 Found_Perm
=> Permission
(Elem
));
4614 end Return_Parameter_Or_Global
;
4616 -----------------------
4617 -- Return_Parameters --
4618 -----------------------
4620 procedure Return_Parameters
(Subp
: Entity_Id
) is
4624 Formal
:= First_Formal
(Subp
);
4625 while Present
(Formal
) loop
4626 Return_Parameter_Or_Global
(Formal
, Ekind
(Formal
), Subp
);
4627 Next_Formal
(Formal
);
4629 end Return_Parameters
;
4631 -------------------------
4632 -- Set_Perm_Extensions --
4633 -------------------------
4635 procedure Set_Perm_Extensions
4636 (T
: Perm_Tree_Access
;
4639 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
4641 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
)
4645 when Entire_Object
=>
4649 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
4651 when Array_Component
=>
4652 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
4654 -- Free every Component subtree
4656 when Record_Component
=>
4658 Comp
: Perm_Tree_Access
;
4661 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
4662 while Comp
/= null loop
4663 Free_Perm_Tree
(Comp
);
4664 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
4667 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
4670 end Free_Perm_Tree_Children
;
4672 Son
: constant Perm_Tree
:=
4674 (Kind => Entire_Object,
4675 Is_Node_Deep => Is_Node_Deep (T),
4676 Permission => Permission (T),
4677 Children_Permission => P);
4680 Free_Perm_Tree_Children (T);
4682 end Set_Perm_Extensions;
4684 ------------------------------
4685 -- Set_Perm_Extensions_Move --
4686 ------------------------------
4688 procedure Set_Perm_Extensions_Move
4689 (T : Perm_Tree_Access;
4693 if not Is_Node_Deep (T) then
4694 -- We are a shallow extension with same number of .all
4696 Set_Perm_Extensions (T, Read_Write);
4700 -- We are a deep extension here (or the moved deep path)
4702 T.all.Tree.Permission := Write_Only;
4704 case T.all.Tree.Kind is
4705 -- Unroll the tree depending on the type
4707 when Entire_Object =>
4710 | E_String_Literal_Subtype
4712 Set_Perm_Extensions (T, No_Access);
4714 -- No need to unroll here, directly put sons to No_Access
4717 if Ekind (E) in Access_Subprogram_Kind then
4720 Set_Perm_Extensions (T, No_Access);
4723 -- No unrolling done, too complicated
4725 when E_Class_Wide_Subtype
4728 | E_Incomplete_Subtype
4733 Set_Perm_Extensions (T, No_Access);
4735 -- Expand the tree. Replace the node with Array component.
4738 | E_Array_Subtype =>
4740 Son : Perm_Tree_Access;
4743 Son := new Perm_Tree_Wrapper'
4745 (Kind
=> Entire_Object
,
4746 Is_Node_Deep
=> Is_Node_Deep
(T
),
4747 Permission
=> Read_Write
,
4748 Children_Permission
=> Read_Write
));
4750 Set_Perm_Extensions_Move
(Son
, Component_Type
(E
));
4752 -- We change the current node from Entire_Object to
4753 -- Reference with Write_Only and the previous son.
4755 pragma Assert
(Is_Node_Deep
(T
));
4757 T
.all.Tree
:= (Kind
=> Array_Component
,
4758 Is_Node_Deep
=> Is_Node_Deep
(T
),
4759 Permission
=> Write_Only
,
4763 -- Unroll, and set permission extensions with component type
4767 | E_Record_Type_With_Private
4768 | E_Record_Subtype_With_Private
4770 | E_Protected_Subtype
4773 -- Expand the tree. Replace the node with
4774 -- Record_Component.
4778 Son
: Perm_Tree_Access
;
4781 -- We change the current node from Entire_Object to
4782 -- Record_Component with same permission and an empty
4783 -- hash table as component list.
4785 pragma Assert
(Is_Node_Deep
(T
));
4788 (Kind
=> Record_Component
,
4789 Is_Node_Deep
=> Is_Node_Deep
(T
),
4790 Permission
=> Write_Only
,
4791 Component
=> Perm_Tree_Maps
.Nil
,
4793 new Perm_Tree_Wrapper
'
4795 (Kind => Entire_Object,
4796 Is_Node_Deep => True,
4797 Permission => Read_Write,
4798 Children_Permission => Read_Write)
4802 -- We fill the hash table with all sons of the record,
4803 -- with basic Entire_Objects nodes.
4804 Elem := First_Component_Or_Discriminant (E);
4805 while Present (Elem) loop
4806 Son := new Perm_Tree_Wrapper'
4808 (Kind
=> Entire_Object
,
4809 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
4810 Permission
=> Read_Write
,
4811 Children_Permission
=> Read_Write
));
4813 Set_Perm_Extensions_Move
(Son
, Etype
(Elem
));
4816 (T
.all.Tree
.Component
, Elem
, Son
);
4818 Next_Component_Or_Discriminant
(Elem
);
4824 | E_Limited_Private_Type
4825 | E_Limited_Private_Subtype
4827 Set_Perm_Extensions_Move
(T
, Underlying_Type
(E
));
4830 raise Program_Error
;
4834 -- Now the son does not have the same number of .all
4835 Set_Perm_Extensions
(T
, No_Access
);
4837 when Array_Component
=>
4838 Set_Perm_Extensions_Move
(Get_Elem
(T
), Component_Type
(E
));
4840 when Record_Component
=>
4842 Comp
: Perm_Tree_Access
;
4846 It
:= First_Component_Or_Discriminant
(E
);
4847 while It
/= Empty
loop
4848 Comp
:= Perm_Tree_Maps
.Get
(Component
(T
), It
);
4849 pragma Assert
(Comp
/= null);
4850 Set_Perm_Extensions_Move
(Comp
, It
);
4851 It
:= Next_Component_Or_Discriminant
(E
);
4854 Set_Perm_Extensions
(Other_Components
(T
), No_Access
);
4857 end Set_Perm_Extensions_Move
;
4859 ------------------------------
4860 -- Set_Perm_Prefixes_Assign --
4861 ------------------------------
4863 function Set_Perm_Prefixes_Assign
4865 return Perm_Tree_Access
4867 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(N
);
4870 pragma Assert
(Current_Checking_Mode
= Assign
);
4872 -- The function should not be called if has_function_component
4874 pragma Assert
(C
/= null);
4877 when Entire_Object
=>
4878 pragma Assert
(Children_Permission
(C
) = Read_Write
);
4879 C
.all.Tree
.Permission
:= Read_Write
;
4882 pragma Assert
(Get_All
(C
) /= null);
4884 C
.all.Tree
.Permission
:=
4885 Lub
(Permission
(C
), Permission
(Get_All
(C
)));
4887 when Array_Component
=>
4888 pragma Assert
(C
.all.Tree
.Get_Elem
/= null);
4890 -- Given that it is not possible to know which element has been
4891 -- assigned, then the permissions do not get changed in case of
4896 when Record_Component
=>
4898 Perm
: Perm_Kind
:= Read_Write
;
4900 Comp
: Perm_Tree_Access
;
4903 -- We take the Glb of all the descendants, and then update the
4904 -- permission of the node with it.
4905 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(C
));
4906 while Comp
/= null loop
4907 Perm
:= Glb
(Perm
, Permission
(Comp
));
4908 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(C
));
4911 Perm
:= Glb
(Perm
, Permission
(Other_Components
(C
)));
4913 C
.all.Tree
.Permission
:= Lub
(Permission
(C
), Perm
);
4918 -- Base identifier. End recursion here.
4922 | N_Defining_Identifier
4926 when N_Type_Conversion
4927 | N_Unchecked_Type_Conversion
4928 | N_Qualified_Expression
4930 return Set_Perm_Prefixes_Assign
(Expression
(N
));
4932 when N_Parameter_Specification
=>
4933 raise Program_Error
;
4935 -- Continue recursion on prefix
4937 when N_Selected_Component
=>
4938 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4940 -- Continue recursion on prefix
4942 when N_Indexed_Component
4945 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4947 -- Continue recursion on prefix
4949 when N_Explicit_Dereference
=>
4950 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4952 when N_Function_Call
=>
4953 raise Program_Error
;
4956 raise Program_Error
;
4959 end Set_Perm_Prefixes_Assign
;
4961 ----------------------------------
4962 -- Set_Perm_Prefixes_Borrow_Out --
4963 ----------------------------------
4965 function Set_Perm_Prefixes_Borrow_Out
4967 return Perm_Tree_Access
4970 pragma Assert
(Current_Checking_Mode
= Borrow_Out
);
4973 -- Base identifier. Set permission to No.
4979 P
: constant Node_Id
:= Entity
(N
);
4981 C
: constant Perm_Tree_Access
:=
4982 Get
(Current_Perm_Env
, Unique_Entity
(P
));
4984 pragma Assert
(C
/= null);
4987 -- Setting the initialization map to True, so that this
4988 -- variable cannot be ignored anymore when looking at end
4989 -- of elaboration of package.
4991 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
4993 C
.all.Tree
.Permission
:= No_Access
;
4997 when N_Type_Conversion
4998 | N_Unchecked_Type_Conversion
4999 | N_Qualified_Expression
5001 return Set_Perm_Prefixes_Borrow_Out
(Expression
(N
));
5003 when N_Parameter_Specification
5004 | N_Defining_Identifier
5006 raise Program_Error
;
5008 -- We set the permission tree of its prefix, and then we extract
5009 -- our subtree from the returned pointer and assign an adequate
5010 -- permission to it, if unfolded. If folded, we unroll the tree
5013 when N_Selected_Component
=>
5015 C
: constant Perm_Tree_Access
:=
5016 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5020 -- We went through a function call, do nothing
5025 -- The permission of the returned node should be No
5027 pragma Assert
(Permission
(C
) = No_Access
);
5029 pragma Assert
(Kind
(C
) = Entire_Object
5030 or else Kind
(C
) = Record_Component
);
5032 if Kind
(C
) = Record_Component
then
5033 -- The tree is unfolded. We just modify the permission and
5034 -- return the record subtree.
5037 Selected_Component
: constant Entity_Id
:=
5038 Entity
(Selector_Name
(N
));
5040 Selected_C
: Perm_Tree_Access
:=
5042 (Component
(C
), Selected_Component
);
5045 if Selected_C
= null then
5046 Selected_C
:= Other_Components
(C
);
5049 pragma Assert
(Selected_C
/= null);
5051 Selected_C
.all.Tree
.Permission
:= No_Access
;
5055 elsif Kind
(C
) = Entire_Object
then
5057 -- Expand the tree. Replace the node with
5058 -- Record_Component.
5062 -- Create an empty hash table
5064 Hashtbl
: Perm_Tree_Maps
.Instance
;
5066 -- We create the unrolled nodes, that will all have same
5067 -- permission than parent.
5069 Son
: Perm_Tree_Access
;
5071 ChildrenPerm
: constant Perm_Kind
:=
5072 Children_Permission
(C
);
5075 -- We change the current node from Entire_Object to
5076 -- Record_Component with same permission and an empty
5077 -- hash table as component list.
5080 (Kind
=> Record_Component
,
5081 Is_Node_Deep
=> Is_Node_Deep
(C
),
5082 Permission
=> Permission
(C
),
5083 Component
=> Hashtbl
,
5085 new Perm_Tree_Wrapper
'
5087 (Kind => Entire_Object,
5088 Is_Node_Deep => True,
5089 Permission => ChildrenPerm,
5090 Children_Permission => ChildrenPerm)
5093 -- We fill the hash table with all sons of the record,
5094 -- with basic Entire_Objects nodes.
5095 Elem := First_Component_Or_Discriminant
5096 (Etype (Prefix (N)));
5098 while Present (Elem) loop
5099 Son := new Perm_Tree_Wrapper'
5101 (Kind
=> Entire_Object
,
5102 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5103 Permission
=> ChildrenPerm
,
5104 Children_Permission
=> ChildrenPerm
));
5107 (C
.all.Tree
.Component
, Elem
, Son
);
5109 Next_Component_Or_Discriminant
(Elem
);
5112 -- Now we set the right field to No_Access, and then we
5113 -- return the tree to the sons, so that the recursion can
5117 Selected_Component
: constant Entity_Id
:=
5118 Entity
(Selector_Name
(N
));
5120 Selected_C
: Perm_Tree_Access
:=
5122 (Component
(C
), Selected_Component
);
5125 if Selected_C
= null then
5126 Selected_C
:= Other_Components
(C
);
5129 pragma Assert
(Selected_C
/= null);
5131 Selected_C
.all.Tree
.Permission
:= No_Access
;
5137 raise Program_Error
;
5141 -- We set the permission tree of its prefix, and then we extract
5142 -- from the returned pointer the subtree and assign an adequate
5143 -- permission to it, if unfolded. If folded, we unroll the tree in
5146 when N_Indexed_Component
5150 C
: constant Perm_Tree_Access
:=
5151 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5155 -- We went through a function call, do nothing
5160 -- The permission of the returned node should be either W
5161 -- (because the recursive call sets <= Write_Only) or No
5162 -- (if another path has been moved with 'Access).
5164 pragma Assert
(Permission
(C
) = No_Access
);
5166 pragma Assert
(Kind
(C
) = Entire_Object
5167 or else Kind
(C
) = Array_Component
);
5169 if Kind
(C
) = Array_Component
then
5170 -- The tree is unfolded. We just modify the permission and
5171 -- return the elem subtree.
5173 pragma Assert
(Get_Elem
(C
) /= null);
5175 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5177 return Get_Elem
(C
);
5178 elsif Kind
(C
) = Entire_Object
then
5180 -- Expand the tree. Replace node with Array_Component.
5182 Son
: Perm_Tree_Access
;
5185 Son
:= new Perm_Tree_Wrapper
'
5187 (Kind => Entire_Object,
5188 Is_Node_Deep => Is_Node_Deep (C),
5189 Permission => No_Access,
5190 Children_Permission => Children_Permission (C)));
5192 -- We change the current node from Entire_Object
5193 -- to Array_Component with same permission and the
5194 -- previously defined son.
5196 C.all.Tree := (Kind => Array_Component,
5197 Is_Node_Deep => Is_Node_Deep (C),
5198 Permission => No_Access,
5201 return Get_Elem (C);
5204 raise Program_Error;
5208 -- We set the permission tree of its prefix, and then we extract
5209 -- from the returned pointer the subtree and assign an adequate
5210 -- permission to it, if unfolded. If folded, we unroll the tree
5213 when N_Explicit_Dereference =>
5215 C : constant Perm_Tree_Access :=
5216 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5220 -- We went through a function call. Do nothing.
5225 -- The permission of the returned node should be No
5227 pragma Assert (Permission (C) = No_Access);
5228 pragma Assert (Kind (C) = Entire_Object
5229 or else Kind (C) = Reference);
5231 if Kind (C) = Reference then
5232 -- The tree is unfolded. We just modify the permission and
5233 -- return the elem subtree.
5235 pragma Assert (Get_All (C) /= null);
5237 C.all.Tree.Get_All.all.Tree.Permission := No_Access;
5240 elsif Kind (C) = Entire_Object then
5242 -- Expand the tree. Replace the node with Reference.
5244 Son : Perm_Tree_Access;
5247 Son := new Perm_Tree_Wrapper'
5249 (Kind
=> Entire_Object
,
5250 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
5251 Permission
=> No_Access
,
5252 Children_Permission
=> Children_Permission
(C
)));
5254 -- We change the current node from Entire_Object to
5255 -- Reference with No_Access and the previous son.
5257 pragma Assert
(Is_Node_Deep
(C
));
5259 C
.all.Tree
:= (Kind
=> Reference
,
5260 Is_Node_Deep
=> Is_Node_Deep
(C
),
5261 Permission
=> No_Access
,
5267 raise Program_Error
;
5271 when N_Function_Call
=>
5275 raise Program_Error
;
5277 end Set_Perm_Prefixes_Borrow_Out
;
5279 ----------------------------
5280 -- Set_Perm_Prefixes_Move --
5281 ----------------------------
5283 function Set_Perm_Prefixes_Move
5284 (N
: Node_Id
; Mode
: Checking_Mode
)
5285 return Perm_Tree_Access
5290 -- Base identifier. Set permission to W or No depending on Mode.
5296 P
: constant Node_Id
:= Entity
(N
);
5297 C
: constant Perm_Tree_Access
:=
5298 Get
(Current_Perm_Env
, Unique_Entity
(P
));
5301 -- The base tree can be RW (first move from this base path) or
5302 -- W (already some extensions values moved), or even No_Access
5303 -- (extensions moved with 'Access). But it cannot be Read_Only
5304 -- (we get an error).
5306 if Permission
(C
) = Read_Only
then
5307 raise Unrecoverable_Error
;
5310 -- Setting the initialization map to True, so that this
5311 -- variable cannot be ignored anymore when looking at end
5312 -- of elaboration of package.
5314 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
5317 -- No null possible here, there are no parents for the path.
5318 -- This means we are using a global variable without adding
5319 -- it in environment with a global aspect.
5321 Illegal_Global_Usage
(N
);
5324 if Mode
= Super_Move
then
5325 C
.all.Tree
.Permission
:= No_Access
;
5327 C
.all.Tree
.Permission
:= Glb
(Write_Only
, Permission
(C
));
5333 when N_Type_Conversion
5334 | N_Unchecked_Type_Conversion
5335 | N_Qualified_Expression
5337 return Set_Perm_Prefixes_Move
(Expression
(N
), Mode
);
5339 when N_Parameter_Specification
5340 | N_Defining_Identifier
5342 raise Program_Error
;
5344 -- We set the permission tree of its prefix, and then we extract
5345 -- from the returned pointer our subtree and assign an adequate
5346 -- permission to it, if unfolded. If folded, we unroll the tree
5349 when N_Selected_Component
=>
5351 C
: constant Perm_Tree_Access
:=
5352 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5356 -- We went through a function call, do nothing
5361 -- The permission of the returned node should be either W
5362 -- (because the recursive call sets <= Write_Only) or No
5363 -- (if another path has been moved with 'Access).
5365 pragma Assert
(Permission
(C
) = No_Access
5366 or else Permission
(C
) = Write_Only
);
5368 if Mode
= Super_Move
then
5369 -- The permission of the returned node should be No (thanks
5370 -- to the recursion).
5372 pragma Assert
(Permission
(C
) = No_Access
);
5376 pragma Assert
(Kind
(C
) = Entire_Object
5377 or else Kind
(C
) = Record_Component
);
5379 if Kind
(C
) = Record_Component
then
5380 -- The tree is unfolded. We just modify the permission and
5381 -- return the record subtree.
5384 Selected_Component
: constant Entity_Id
:=
5385 Entity
(Selector_Name
(N
));
5387 Selected_C
: Perm_Tree_Access
:=
5389 (Component
(C
), Selected_Component
);
5392 if Selected_C
= null then
5393 -- If the hash table returns no element, then we fall
5394 -- into the part of Other_Components.
5395 pragma Assert
(Is_Tagged_Type
(Etype
(Prefix
(N
))));
5397 Selected_C
:= Other_Components
(C
);
5400 pragma Assert
(Selected_C
/= null);
5402 -- The Selected_C can have permissions:
5403 -- RW : first move in this path
5404 -- W : Already other moves in this path
5405 -- No : Already other moves with 'Access
5407 pragma Assert
(Permission
(Selected_C
) /= Read_Only
);
5408 if Mode
= Super_Move
then
5409 Selected_C
.all.Tree
.Permission
:= No_Access
;
5411 Selected_C
.all.Tree
.Permission
:=
5412 Glb
(Write_Only
, Permission
(Selected_C
));
5418 elsif Kind
(C
) = Entire_Object
then
5420 -- Expand the tree. Replace the node with
5421 -- Record_Component.
5425 -- Create an empty hash table
5427 Hashtbl
: Perm_Tree_Maps
.Instance
;
5429 -- We are in Move or Super_Move mode, hence we can assume
5430 -- that the Children_permission is RW, given that there
5431 -- are no other paths that could have been moved.
5433 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5435 -- We create the unrolled nodes, that will all have RW
5436 -- permission given that we are in move mode. We will
5437 -- then set the right node to W.
5439 Son
: Perm_Tree_Access
;
5442 -- We change the current node from Entire_Object to
5443 -- Record_Component with same permission and an empty
5444 -- hash table as component list.
5447 (Kind
=> Record_Component
,
5448 Is_Node_Deep
=> Is_Node_Deep
(C
),
5449 Permission
=> Permission
(C
),
5450 Component
=> Hashtbl
,
5452 new Perm_Tree_Wrapper
'
5454 (Kind => Entire_Object,
5455 Is_Node_Deep => True,
5456 Permission => Read_Write,
5457 Children_Permission => Read_Write)
5460 -- We fill the hash table with all sons of the record,
5461 -- with basic Entire_Objects nodes.
5462 Elem := First_Component_Or_Discriminant
5463 (Etype (Prefix (N)));
5465 while Present (Elem) loop
5466 Son := new Perm_Tree_Wrapper'
5468 (Kind
=> Entire_Object
,
5469 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5470 Permission
=> Read_Write
,
5471 Children_Permission
=> Read_Write
));
5474 (C
.all.Tree
.Component
, Elem
, Son
);
5476 Next_Component_Or_Discriminant
(Elem
);
5479 -- Now we set the right field to Write_Only or No_Access
5480 -- depending on mode, and then we return the tree to the
5481 -- sons, so that the recursion can continue.
5484 Selected_Component
: constant Entity_Id
:=
5485 Entity
(Selector_Name
(N
));
5487 Selected_C
: Perm_Tree_Access
:=
5489 (Component
(C
), Selected_Component
);
5492 if Selected_C
= null then
5493 Selected_C
:= Other_Components
(C
);
5496 pragma Assert
(Selected_C
/= null);
5498 -- Given that this is a newly created Select_C, we can
5499 -- safely assume that its permission is Read_Write.
5501 pragma Assert
(Permission
(Selected_C
) =
5504 if Mode
= Super_Move
then
5505 Selected_C
.all.Tree
.Permission
:= No_Access
;
5507 Selected_C
.all.Tree
.Permission
:= Write_Only
;
5514 raise Program_Error
;
5518 -- We set the permission tree of its prefix, and then we extract
5519 -- from the returned pointer the subtree and assign an adequate
5520 -- permission to it, if unfolded. If folded, we unroll the tree
5523 when N_Indexed_Component
5527 C
: constant Perm_Tree_Access
:=
5528 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5532 -- We went through a function call, do nothing
5537 -- The permission of the returned node should be either
5538 -- W (because the recursive call sets <= Write_Only)
5539 -- or No (if another path has been moved with 'Access)
5541 if Mode
= Super_Move
then
5542 pragma Assert
(Permission
(C
) = No_Access
);
5545 pragma Assert
(Permission
(C
) = Write_Only
5546 or else Permission
(C
) = No_Access
);
5550 pragma Assert
(Kind
(C
) = Entire_Object
5551 or else Kind
(C
) = Array_Component
);
5553 if Kind
(C
) = Array_Component
then
5554 -- The tree is unfolded. We just modify the permission and
5555 -- return the elem subtree.
5557 if Get_Elem
(C
) = null then
5559 raise Program_Error
;
5562 -- The Get_Elem can have permissions :
5563 -- RW : first move in this path
5564 -- W : Already other moves in this path
5565 -- No : Already other moves with 'Access
5567 pragma Assert
(Permission
(Get_Elem
(C
)) /= Read_Only
);
5569 if Mode
= Super_Move
then
5570 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5572 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:=
5573 Glb
(Write_Only
, Permission
(Get_Elem
(C
)));
5576 return Get_Elem
(C
);
5577 elsif Kind
(C
) = Entire_Object
then
5579 -- Expand the tree. Replace node with Array_Component.
5581 -- We are in move mode, hence we can assume that the
5582 -- Children_permission is RW.
5584 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5586 Son
: Perm_Tree_Access
;
5589 Son
:= new Perm_Tree_Wrapper
'
5591 (Kind => Entire_Object,
5592 Is_Node_Deep => Is_Node_Deep (C),
5593 Permission => Read_Write,
5594 Children_Permission => Read_Write));
5596 if Mode = Super_Move then
5597 Son.all.Tree.Permission := No_Access;
5599 Son.all.Tree.Permission := Write_Only;
5602 -- We change the current node from Entire_Object
5603 -- to Array_Component with same permission and the
5604 -- previously defined son.
5606 C.all.Tree := (Kind => Array_Component,
5607 Is_Node_Deep => Is_Node_Deep (C),
5608 Permission => Permission (C),
5611 return Get_Elem (C);
5614 raise Program_Error;
5618 -- We set the permission tree of its prefix, and then we extract
5619 -- from the returned pointer the subtree and assign an adequate
5620 -- permission to it, if unfolded. If folded, we unroll the tree
5623 when N_Explicit_Dereference =>
5625 C : constant Perm_Tree_Access :=
5626 Set_Perm_Prefixes_Move (Prefix (N), Move);
5630 -- We went through a function call: do nothing
5635 -- The permission of the returned node should be only
5636 -- W (because the recursive call sets <= Write_Only)
5637 -- No is NOT POSSIBLE here
5639 pragma Assert (Permission (C) = Write_Only);
5641 pragma Assert (Kind (C) = Entire_Object
5642 or else Kind (C) = Reference);
5644 if Kind (C) = Reference then
5645 -- The tree is unfolded. We just modify the permission and
5646 -- return the elem subtree.
5648 if Get_All (C) = null then
5650 raise Program_Error;
5653 -- The Get_All can have permissions :
5654 -- RW : first move in this path
5655 -- W : Already other moves in this path
5656 -- No : Already other moves with 'Access
5658 pragma Assert
(Permission
(Get_All
(C
)) /= Read_Only
);
5660 if Mode
= Super_Move
then
5661 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= No_Access
;
5663 Get_All
(C
).all.Tree
.Permission
:=
5664 Glb
(Write_Only
, Permission
(Get_All
(C
)));
5667 elsif Kind
(C
) = Entire_Object
then
5669 -- Expand the tree. Replace the node with Reference.
5671 -- We are in Move or Super_Move mode, hence we can assume
5672 -- that the Children_permission is RW.
5674 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5676 Son
: Perm_Tree_Access
;
5679 Son
:= new Perm_Tree_Wrapper
'
5681 (Kind => Entire_Object,
5682 Is_Node_Deep => Is_Deep (Etype (N)),
5683 Permission => Read_Write,
5684 Children_Permission => Read_Write));
5686 if Mode = Super_Move then
5687 Son.all.Tree.Permission := No_Access;
5689 Son.all.Tree.Permission := Write_Only;
5692 -- We change the current node from Entire_Object to
5693 -- Reference with Write_Only and the previous son.
5695 pragma Assert (Is_Node_Deep (C));
5697 C.all.Tree := (Kind => Reference,
5698 Is_Node_Deep => Is_Node_Deep (C),
5699 Permission => Write_Only,
5700 -- Write_only is equal to C.Permission
5706 raise Program_Error;
5710 when N_Function_Call =>
5714 raise Program_Error;
5717 end Set_Perm_Prefixes_Move;
5719 -------------------------------
5720 -- Set_Perm_Prefixes_Observe --
5721 -------------------------------
5723 function Set_Perm_Prefixes_Observe
5725 return Perm_Tree_Access
5728 pragma Assert (Current_Checking_Mode = Observe);
5731 -- Base identifier. Set permission to R.
5735 | N_Defining_Identifier
5739 C : Perm_Tree_Access;
5742 if Nkind (N) = N_Defining_Identifier then
5748 C := Get (Current_Perm_Env, Unique_Entity (P));
5749 -- Setting the initialization map to True, so that this
5750 -- variable cannot be ignored anymore when looking at end
5751 -- of elaboration of package.
5753 Set (Current_Initialization_Map, Unique_Entity (P), True);
5756 -- No null possible here, there are no parents for the path.
5757 -- This means we are using a global variable without adding
5758 -- it in environment with a global aspect.
5760 Illegal_Global_Usage (N);
5763 C.all.Tree.Permission := Glb (Read_Only, Permission (C));
5768 when N_Type_Conversion
5769 | N_Unchecked_Type_Conversion
5770 | N_Qualified_Expression
5772 return Set_Perm_Prefixes_Observe (Expression (N));
5774 when N_Parameter_Specification =>
5775 raise Program_Error;
5777 -- We set the permission tree of its prefix, and then we extract
5778 -- from the returned pointer our subtree and assign an adequate
5779 -- permission to it, if unfolded. If folded, we unroll the tree
5782 when N_Selected_Component =>
5784 C : constant Perm_Tree_Access :=
5785 Set_Perm_Prefixes_Observe (Prefix (N));
5789 -- We went through a function call, do nothing
5794 pragma Assert (Kind (C) = Entire_Object
5795 or else Kind (C) = Record_Component);
5797 if Kind (C) = Record_Component then
5798 -- The tree is unfolded. We just modify the permission and
5799 -- return the record subtree. We put the permission to the
5800 -- glb of read_only and its current permission, to consider
5801 -- the case of observing x.y while x.z has been moved. Then
5802 -- x should be No_Access.
5805 Selected_Component : constant Entity_Id :=
5806 Entity (Selector_Name (N));
5808 Selected_C : Perm_Tree_Access :=
5810 (Component (C), Selected_Component);
5813 if Selected_C = null then
5814 Selected_C := Other_Components (C);
5817 pragma Assert (Selected_C /= null);
5819 Selected_C.all.Tree.Permission :=
5820 Glb (Read_Only, Permission (Selected_C));
5824 elsif Kind (C) = Entire_Object then
5826 -- Expand the tree. Replace the node with
5827 -- Record_Component.
5831 -- Create an empty hash table
5833 Hashtbl : Perm_Tree_Maps.Instance;
5835 -- We create the unrolled nodes, that will all have RW
5836 -- permission given that we are in move mode. We will
5837 -- then set the right node to W.
5839 Son : Perm_Tree_Access;
5841 Child_Perm : constant Perm_Kind :=
5842 Children_Permission (C);
5845 -- We change the current node from Entire_Object to
5846 -- Record_Component with same permission and an empty
5847 -- hash table as component list.
5850 (Kind => Record_Component,
5851 Is_Node_Deep => Is_Node_Deep (C),
5852 Permission => Permission (C),
5853 Component => Hashtbl,
5855 new Perm_Tree_Wrapper'
5857 (Kind
=> Entire_Object
,
5858 Is_Node_Deep
=> True,
5859 Permission
=> Child_Perm
,
5860 Children_Permission
=> Child_Perm
)
5863 -- We fill the hash table with all sons of the record,
5864 -- with basic Entire_Objects nodes.
5865 Elem
:= First_Component_Or_Discriminant
5866 (Etype
(Prefix
(N
)));
5868 while Present
(Elem
) loop
5869 Son
:= new Perm_Tree_Wrapper
'
5871 (Kind => Entire_Object,
5872 Is_Node_Deep => Is_Deep (Etype (Elem)),
5873 Permission => Child_Perm,
5874 Children_Permission => Child_Perm));
5877 (C.all.Tree.Component, Elem, Son);
5879 Next_Component_Or_Discriminant (Elem);
5882 -- Now we set the right field to Read_Only. and then we
5883 -- return the tree to the sons, so that the recursion can
5887 Selected_Component : constant Entity_Id :=
5888 Entity (Selector_Name (N));
5890 Selected_C : Perm_Tree_Access :=
5892 (Component (C), Selected_Component);
5895 if Selected_C = null then
5896 Selected_C := Other_Components (C);
5899 pragma Assert (Selected_C /= null);
5901 Selected_C.all.Tree.Permission :=
5902 Glb (Read_Only, Child_Perm);
5908 raise Program_Error;
5912 -- We set the permission tree of its prefix, and then we extract from
5913 -- the returned pointer the subtree and assign an adequate permission
5914 -- to it, if unfolded. If folded, we unroll the tree at one step.
5916 when N_Indexed_Component
5920 C : constant Perm_Tree_Access :=
5921 Set_Perm_Prefixes_Observe (Prefix (N));
5925 -- We went through a function call, do nothing
5930 pragma Assert (Kind (C) = Entire_Object
5931 or else Kind (C) = Array_Component);
5933 if Kind (C) = Array_Component then
5934 -- The tree is unfolded. We just modify the permission and
5935 -- return the elem subtree.
5937 pragma Assert (Get_Elem (C) /= null);
5939 C.all.Tree.Get_Elem.all.Tree.Permission :=
5940 Glb (Read_Only, Permission (Get_Elem (C)));
5942 return Get_Elem (C);
5943 elsif Kind (C) = Entire_Object then
5945 -- Expand the tree. Replace node with Array_Component.
5947 Son : Perm_Tree_Access;
5949 Child_Perm : constant Perm_Kind :=
5950 Glb (Read_Only, Children_Permission (C));
5953 Son := new Perm_Tree_Wrapper'
5955 (Kind
=> Entire_Object
,
5956 Is_Node_Deep
=> Is_Node_Deep
(C
),
5957 Permission
=> Child_Perm
,
5958 Children_Permission
=> Child_Perm
));
5960 -- We change the current node from Entire_Object
5961 -- to Array_Component with same permission and the
5962 -- previously defined son.
5964 C
.all.Tree
:= (Kind
=> Array_Component
,
5965 Is_Node_Deep
=> Is_Node_Deep
(C
),
5966 Permission
=> Child_Perm
,
5969 return Get_Elem
(C
);
5973 raise Program_Error
;
5977 -- We set the permission tree of its prefix, and then we extract from
5978 -- the returned pointer the subtree and assign an adequate permission
5979 -- to it, if unfolded. If folded, we unroll the tree at one step.
5981 when N_Explicit_Dereference
=>
5983 C
: constant Perm_Tree_Access
:=
5984 Set_Perm_Prefixes_Observe
(Prefix
(N
));
5988 -- We went through a function call, do nothing
5993 pragma Assert
(Kind
(C
) = Entire_Object
5994 or else Kind
(C
) = Reference
);
5996 if Kind
(C
) = Reference
then
5997 -- The tree is unfolded. We just modify the permission and
5998 -- return the elem subtree.
6000 pragma Assert
(Get_All
(C
) /= null);
6002 C
.all.Tree
.Get_All
.all.Tree
.Permission
:=
6003 Glb
(Read_Only
, Permission
(Get_All
(C
)));
6006 elsif Kind
(C
) = Entire_Object
then
6008 -- Expand the tree. Replace the node with Reference.
6010 Son
: Perm_Tree_Access
;
6012 Child_Perm
: constant Perm_Kind
:=
6013 Glb
(Read_Only
, Children_Permission
(C
));
6016 Son
:= new Perm_Tree_Wrapper
'
6018 (Kind => Entire_Object,
6019 Is_Node_Deep => Is_Deep (Etype (N)),
6020 Permission => Child_Perm,
6021 Children_Permission => Child_Perm));
6023 -- We change the current node from Entire_Object to
6024 -- Reference with Write_Only and the previous son.
6026 pragma Assert (Is_Node_Deep (C));
6028 C.all.Tree := (Kind => Reference,
6029 Is_Node_Deep => Is_Node_Deep (C),
6030 Permission => Child_Perm,
6036 raise Program_Error;
6040 when N_Function_Call =>
6044 raise Program_Error;
6047 end Set_Perm_Prefixes_Observe;
6053 procedure Setup_Globals (Subp : Entity_Id) is
6055 procedure Setup_Globals_From_List
6056 (First_Item : Node_Id;
6057 Kind : Formal_Kind);
6058 -- Set up global items from the list starting at Item
6060 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
6061 -- Set up global items for the mode Global_Mode
6063 -----------------------------
6064 -- Setup_Globals_From_List --
6065 -----------------------------
6067 procedure Setup_Globals_From_List
6068 (First_Item : Node_Id;
6071 Item : Node_Id := First_Item;
6075 while Present (Item) loop
6078 -- Ignore abstract states, which play no role in pointer aliasing
6080 if Ekind (E) = E_Abstract_State then
6083 Setup_Parameter_Or_Global (E, Kind);
6087 end Setup_Globals_From_List;
6089 ---------------------------
6090 -- Setup_Globals_Of_Mode --
6091 ---------------------------
6093 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
6098 when Name_Input | Name_Proof_In =>
6099 Kind := E_In_Parameter;
6101 Kind := E_Out_Parameter;
6103 Kind := E_In_Out_Parameter;
6105 raise Program_Error;
6108 -- Set up both global items from Global and Refined_Global pragmas
6110 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
6111 Setup_Globals_From_List
6112 (First_Global (Subp, Global_Mode, Refined => True), Kind);
6113 end Setup_Globals_Of_Mode;
6115 -- Start of processing for Setup_Globals
6118 Setup_Globals_Of_Mode (Name_Proof_In);
6119 Setup_Globals_Of_Mode (Name_Input);
6120 Setup_Globals_Of_Mode (Name_Output);
6121 Setup_Globals_Of_Mode (Name_In_Out);
6124 -------------------------------
6125 -- Setup_Parameter_Or_Global --
6126 -------------------------------
6128 procedure Setup_Parameter_Or_Global
6132 Elem : Perm_Tree_Access;
6135 Elem := new Perm_Tree_Wrapper'
6137 (Kind
=> Entire_Object
,
6138 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
6139 Permission
=> Read_Write
,
6140 Children_Permission
=> Read_Write
));
6143 when E_In_Parameter
=>
6145 -- Borrowed IN: RW for everybody
6147 if Is_Borrowed_In
(Id
) then
6148 Elem
.all.Tree
.Permission
:= Read_Write
;
6149 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6151 -- Observed IN: R for everybody
6154 Elem
.all.Tree
.Permission
:= Read_Only
;
6155 Elem
.all.Tree
.Children_Permission
:= Read_Only
;
6158 -- OUT: borrow, but callee has W only
6160 when E_Out_Parameter
=>
6161 Elem
.all.Tree
.Permission
:= Write_Only
;
6162 Elem
.all.Tree
.Children_Permission
:= Write_Only
;
6164 -- IN OUT: borrow and callee has RW
6166 when E_In_Out_Parameter
=>
6167 Elem
.all.Tree
.Permission
:= Read_Write
;
6168 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6171 Set
(Current_Perm_Env
, Id
, Elem
);
6172 end Setup_Parameter_Or_Global
;
6174 ----------------------
6175 -- Setup_Parameters --
6176 ----------------------
6178 procedure Setup_Parameters
(Subp
: Entity_Id
) is
6182 Formal
:= First_Formal
(Subp
);
6183 while Present
(Formal
) loop
6184 Setup_Parameter_Or_Global
(Formal
, Ekind
(Formal
));
6185 Next_Formal
(Formal
);
6187 end Setup_Parameters
;