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
2317 | N_Delta_Constraint
2318 | N_Digits_Constraint
2320 | N_Enumeration_Representation_Clause
2321 | N_Exception_Declaration
2322 | N_Exception_Renaming_Declaration
2323 | N_Formal_Package_Declaration
2324 | N_Formal_Subprogram_Declaration
2326 | N_Freeze_Generic_Entity
2327 | N_Function_Instantiation
2328 | N_Generic_Function_Renaming_Declaration
2329 | N_Generic_Package_Declaration
2330 | N_Generic_Package_Renaming_Declaration
2331 | N_Generic_Procedure_Renaming_Declaration
2332 | N_Generic_Subprogram_Declaration
2333 | N_Implicit_Label_Declaration
2336 | N_Number_Declaration
2337 | N_Object_Renaming_Declaration
2339 | N_Package_Instantiation
2340 | N_Package_Renaming_Declaration
2342 | N_Procedure_Instantiation
2343 | N_Record_Representation_Clause
2344 | N_Subprogram_Declaration
2345 | N_Subprogram_Renaming_Declaration
2346 | N_Task_Type_Declaration
2347 | N_Use_Package_Clause
2350 | N_Validate_Unchecked_Conversion
2354 -- The following nodes are rewritten by semantic analysis
2356 when N_Single_Protected_Declaration
2357 | N_Single_Task_Declaration
2359 raise Program_Error;
2362 Current_Checking_Mode := Mode_Before;
2365 ------------------------
2366 -- Check_Package_Body --
2367 ------------------------
2369 procedure Check_Package_Body (Pack : Node_Id) is
2370 Saved_Env : Perm_Env;
2374 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
2375 if Get_SPARK_Mode_From_Annotation
2376 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
2384 CorSp := Parent (Corresponding_Spec (Pack));
2385 while Nkind (CorSp) /= N_Package_Specification loop
2386 CorSp := Parent (CorSp);
2389 Check_List (Visible_Declarations (CorSp));
2393 Copy_Env (Current_Perm_Env,
2396 Check_List (Private_Declarations (CorSp));
2398 -- Set mode to Read, and then analyze declarations and statements
2400 Current_Checking_Mode := Read;
2402 Check_List (Declarations (Pack));
2403 Check_Node (Handled_Statement_Sequence (Pack));
2405 -- Check RW for every stateful variable (i.e. in declarations)
2407 Return_Declarations (Private_Declarations (CorSp));
2408 Return_Declarations (Visible_Declarations (CorSp));
2409 Return_Declarations (Declarations (Pack));
2411 -- Restore previous environment (i.e. delete every nonvisible
2412 -- declaration) from environment.
2414 Free_Env (Current_Perm_Env);
2415 Copy_Env (Saved_Env,
2417 end Check_Package_Body;
2423 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
2424 Mode : constant Entity_Kind := Ekind (Formal);
2425 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2428 case Current_Checking_Mode is
2430 case Formal_Kind'(Mode
) is
2431 when E_In_Parameter
=>
2432 if Is_Borrowed_In
(Formal
) then
2435 Current_Checking_Mode
:= Move
;
2442 when E_Out_Parameter
=>
2445 when E_In_Out_Parameter
=>
2448 Current_Checking_Mode
:= Move
;
2452 Check_Node
(Actual
);
2455 case Formal_Kind
'(Mode) is
2456 when E_In_Parameter =>
2459 when E_Out_Parameter
2460 | E_In_Out_Parameter
2462 -- Borrowed out or in out
2464 Process_Path (Actual);
2469 raise Program_Error;
2472 Current_Checking_Mode := Mode_Before;
2475 --------------------------
2476 -- Check_Param_Observes --
2477 --------------------------
2479 procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is
2480 Mode : constant Entity_Kind := Ekind (Formal);
2481 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2485 when E_In_Parameter =>
2486 if not Is_Borrowed_In (Formal) then
2489 Current_Checking_Mode := Observe;
2490 Check_Node (Actual);
2498 Current_Checking_Mode := Mode_Before;
2499 end Check_Param_Observes;
2501 ----------------------
2502 -- Check_Param_Outs --
2503 ----------------------
2505 procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is
2506 Mode : constant Entity_Kind := Ekind (Formal);
2507 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2512 when E_Out_Parameter =>
2514 Current_Checking_Mode := Borrow_Out;
2515 Check_Node (Actual);
2522 Current_Checking_Mode := Mode_Before;
2523 end Check_Param_Outs;
2525 ----------------------
2526 -- Check_Param_Read --
2527 ----------------------
2529 procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is
2530 Mode : constant Entity_Kind := Ekind (Formal);
2533 pragma Assert (Current_Checking_Mode = Read);
2535 case Formal_Kind'(Mode
) is
2536 when E_In_Parameter
=>
2537 Check_Node
(Actual
);
2539 when E_Out_Parameter
2540 | E_In_Out_Parameter
2545 end Check_Param_Read
;
2547 -------------------------
2548 -- Check_Safe_Pointers --
2549 -------------------------
2551 procedure Check_Safe_Pointers
(N
: Node_Id
) is
2553 -- Local subprograms
2555 procedure Check_List
(L
: List_Id
);
2556 -- Call the main analysis procedure on each element of the list
2558 procedure Initialize
;
2559 -- Initialize global variables before starting the analysis of a body
2565 procedure Check_List
(L
: List_Id
) is
2569 while Present
(N
) loop
2570 Check_Safe_Pointers
(N
);
2579 procedure Initialize
is
2581 Reset
(Current_Loops_Envs
);
2582 Reset
(Current_Loops_Accumulators
);
2583 Reset
(Current_Perm_Env
);
2584 Reset
(Current_Initialization_Map
);
2590 -- SPARK_Mode pragma in application
2592 -- Start of processing for Check_Safe_Pointers
2598 when N_Compilation_Unit
=>
2599 Check_Safe_Pointers
(Unit
(N
));
2602 | N_Package_Declaration
2605 Prag
:= SPARK_Pragma
(Defining_Entity
(N
));
2606 if Present
(Prag
) then
2607 if Get_SPARK_Mode_From_Annotation
(Prag
) = Opt
.Off
then
2613 elsif Nkind
(N
) = N_Package_Body
then
2614 Check_List
(Declarations
(N
));
2616 elsif Nkind
(N
) = N_Package_Declaration
then
2617 Check_List
(Private_Declarations
(Specification
(N
)));
2618 Check_List
(Visible_Declarations
(Specification
(N
)));
2624 end Check_Safe_Pointers
;
2626 ---------------------
2627 -- Check_Statement --
2628 ---------------------
2630 procedure Check_Statement
(Stmt
: Node_Id
) is
2631 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2633 case N_Statement_Other_Than_Procedure_Call
'(Nkind (Stmt)) is
2634 when N_Entry_Call_Statement =>
2635 Check_Call_Statement (Stmt);
2637 -- Move right-hand side first, and then assign left-hand side
2639 when N_Assignment_Statement =>
2640 if Is_Deep (Etype (Expression (Stmt))) then
2641 Current_Checking_Mode := Move;
2643 Current_Checking_Mode := Read;
2646 Check_Node (Expression (Stmt));
2647 Current_Checking_Mode := Assign;
2648 Check_Node (Name (Stmt));
2650 when N_Block_Statement =>
2652 Saved_Env : Perm_Env;
2657 Copy_Env (Current_Perm_Env,
2660 -- Analyze declarations and Handled_Statement_Sequences
2662 Current_Checking_Mode := Read;
2663 Check_List (Declarations (Stmt));
2664 Check_Node (Handled_Statement_Sequence (Stmt));
2666 -- Restore environment
2668 Free_Env (Current_Perm_Env);
2669 Copy_Env (Saved_Env,
2673 when N_Case_Statement =>
2675 Saved_Env : Perm_Env;
2677 -- Accumulator for the different branches
2681 Elmt : Node_Id := First (Alternatives (Stmt));
2684 Current_Checking_Mode := Read;
2685 Check_Node (Expression (Stmt));
2686 Current_Checking_Mode := Mode_Before;
2690 Copy_Env (Current_Perm_Env,
2693 -- Here we have the original env in saved, current with a fresh
2694 -- copy, and new aliased.
2696 -- First alternative
2701 Copy_Env (Current_Perm_Env,
2703 Free_Env (Current_Perm_Env);
2705 -- Other alternatives
2707 while Present (Elmt) loop
2708 -- Restore environment
2710 Copy_Env (Saved_Env,
2715 -- Merge Current_Perm_Env into New_Env
2717 Merge_Envs (New_Env,
2728 Free_Env (Saved_Env);
2731 when N_Delay_Relative_Statement =>
2732 Check_Node (Expression (Stmt));
2734 when N_Delay_Until_Statement =>
2735 Check_Node (Expression (Stmt));
2737 when N_Loop_Statement =>
2738 Check_Loop_Statement (Stmt);
2740 -- If deep type expression, then move, else read
2742 when N_Simple_Return_Statement =>
2743 case Nkind (Expression (Stmt)) is
2746 -- ??? This does not take into account the fact that
2747 -- a simple return inside an extended return statement
2748 -- applies to the extended return statement.
2749 Subp : constant Entity_Id :=
2750 Return_Applies_To (Return_Statement_Entity (Stmt));
2752 Return_Parameters (Subp);
2753 Return_Globals (Subp);
2757 if Is_Deep (Etype (Expression (Stmt))) then
2758 Current_Checking_Mode := Move;
2759 elsif Is_Shallow (Etype (Expression (Stmt))) then
2760 Current_Checking_Mode := Read;
2762 raise Program_Error;
2765 Check_Node (Expression (Stmt));
2768 when N_Extended_Return_Statement =>
2769 Check_List (Return_Object_Declarations (Stmt));
2770 Check_Node (Handled_Statement_Sequence (Stmt));
2772 Return_Declarations (Return_Object_Declarations (Stmt));
2775 -- ??? This does not take into account the fact that a simple
2776 -- return inside an extended return statement applies to the
2777 -- extended return statement.
2778 Subp : constant Entity_Id :=
2779 Return_Applies_To (Return_Statement_Entity (Stmt));
2781 Return_Parameters (Subp);
2782 Return_Globals (Subp);
2785 -- Merge the current_Perm_Env with the accumulator for the given loop
2787 when N_Exit_Statement =>
2789 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
2791 Saved_Accumulator : constant Perm_Env_Access :=
2792 Get (Current_Loops_Accumulators, Loop_Name);
2794 Environment_Copy : constant Perm_Env_Access :=
2798 Copy_Env (Current_Perm_Env,
2799 Environment_Copy.all);
2801 if Saved_Accumulator = null then
2802 Set (Current_Loops_Accumulators,
2803 Loop_Name, Environment_Copy);
2805 Merge_Envs (Saved_Accumulator.all,
2806 Environment_Copy.all);
2810 -- Copy environment, run on each branch, and then merge
2812 when N_If_Statement =>
2814 Saved_Env : Perm_Env;
2816 -- Accumulator for the different branches
2822 Check_Node (Condition (Stmt));
2826 Copy_Env (Current_Perm_Env,
2829 -- Here we have the original env in saved, current with a fresh
2834 Check_List (Then_Statements (Stmt));
2836 Copy_Env (Current_Perm_Env,
2839 Free_Env (Current_Perm_Env);
2841 -- Here the new_environment contains curr env after then block
2848 Elmt := First (Elsif_Parts (Stmt));
2849 while Present (Elmt) loop
2850 -- Transfer into accumulator, and restore from save
2852 Copy_Env (Saved_Env,
2855 Check_Node (Condition (Elmt));
2856 Check_List (Then_Statements (Stmt));
2858 -- Merge Current_Perm_Env into New_Env
2860 Merge_Envs (New_Env,
2869 -- Restore environment before if
2871 Copy_Env (Saved_Env,
2874 -- Here new environment contains the environment after then and
2875 -- current the fresh copy of old one.
2877 Check_List (Else_Statements (Stmt));
2879 Merge_Envs (New_Env,
2888 Free_Env (Saved_Env);
2891 -- Unsupported constructs in SPARK
2893 when N_Abort_Statement
2894 | N_Accept_Statement
2895 | N_Asynchronous_Select
2897 | N_Conditional_Entry_Call
2899 | N_Requeue_Statement
2900 | N_Selective_Accept
2901 | N_Timed_Entry_Call
2903 Error_Msg_N ("unsupported construct in SPARK", Stmt);
2905 -- Ignored constructs for pointer checking
2907 when N_Null_Statement
2912 -- The following nodes are never generated in GNATprove mode
2914 when N_Compound_Statement
2917 raise Program_Error;
2919 end Check_Statement;
2925 function Get_Perm (N : Node_Id) return Perm_Kind is
2926 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
2929 case Tree_Or_Perm.R is
2931 return Tree_Or_Perm.Found_Permission;
2934 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
2935 return Permission (Tree_Or_Perm.Tree_Access);
2937 -- We encoutered a function call, hence the memory area is fresh,
2938 -- which means that the association permission is RW.
2940 when Function_Call =>
2946 ----------------------
2947 -- Get_Perm_Or_Tree --
2948 ----------------------
2950 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
2954 -- Base identifier. Normally those are the roots of the trees stored
2955 -- in the permission environment.
2957 when N_Defining_Identifier =>
2958 raise Program_Error;
2964 P : constant Entity_Id := Entity (N);
2966 C : constant Perm_Tree_Access :=
2967 Get (Current_Perm_Env, Unique_Entity (P));
2970 -- Setting the initialization map to True, so that this
2971 -- variable cannot be ignored anymore when looking at end
2972 -- of elaboration of package.
2974 Set (Current_Initialization_Map, Unique_Entity (P), True);
2977 -- No null possible here, there are no parents for the path.
2978 -- This means we are using a global variable without adding
2979 -- it in environment with a global aspect.
2981 Illegal_Global_Usage (N);
2983 return (R => Unfolded, Tree_Access => C);
2987 when N_Type_Conversion
2988 | N_Unchecked_Type_Conversion
2989 | N_Qualified_Expression
2991 return Get_Perm_Or_Tree (Expression (N));
2993 -- Happening when we try to get the permission of a variable that
2994 -- is a formal parameter. We get instead the defining identifier
2995 -- associated with the parameter (which is the one that has been
2996 -- stored for indexing).
2998 when N_Parameter_Specification =>
2999 return Get_Perm_Or_Tree (Defining_Identifier (N));
3001 -- We get the permission tree of its prefix, and then get either the
3002 -- subtree associated with that specific selection, or if we have a
3003 -- leaf that folds its children, we take the children's permission
3004 -- and return it using the discriminant Folded.
3006 when N_Selected_Component =>
3008 C : constant Perm_Or_Tree :=
3009 Get_Perm_Or_Tree (Prefix (N));
3019 pragma Assert (C.Tree_Access /= null);
3021 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3023 Kind (C.Tree_Access) = Record_Component);
3025 if Kind (C.Tree_Access) = Record_Component then
3027 Selected_Component : constant Entity_Id :=
3028 Entity (Selector_Name (N));
3030 Selected_C : constant Perm_Tree_Access :=
3032 (Component (C.Tree_Access), Selected_Component);
3035 if Selected_C = null then
3036 return (R => Unfolded,
3038 Other_Components (C.Tree_Access));
3040 return (R => Unfolded,
3041 Tree_Access => Selected_C);
3044 elsif Kind (C.Tree_Access) = Entire_Object then
3045 return (R => Folded, Found_Permission =>
3046 Children_Permission (C.Tree_Access));
3048 raise Program_Error;
3053 -- We get the permission tree of its prefix, and then get either the
3054 -- subtree associated with that specific selection, or if we have a
3055 -- leaf that folds its children, we take the children's permission
3056 -- and return it using the discriminant Folded.
3058 when N_Indexed_Component
3062 C : constant Perm_Or_Tree :=
3063 Get_Perm_Or_Tree (Prefix (N));
3073 pragma Assert (C.Tree_Access /= null);
3075 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3077 Kind (C.Tree_Access) = Array_Component);
3079 if Kind (C.Tree_Access) = Array_Component then
3080 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3082 return (R => Unfolded,
3083 Tree_Access => Get_Elem (C.Tree_Access));
3084 elsif Kind (C.Tree_Access) = Entire_Object then
3085 return (R => Folded, Found_Permission =>
3086 Children_Permission (C.Tree_Access));
3088 raise Program_Error;
3093 -- We get the permission tree of its prefix, and then get either the
3094 -- subtree associated with that specific selection, or if we have a
3095 -- leaf that folds its children, we take the children's permission
3096 -- and return it using the discriminant Folded.
3098 when N_Explicit_Dereference =>
3100 C : constant Perm_Or_Tree :=
3101 Get_Perm_Or_Tree (Prefix (N));
3111 pragma Assert (C.Tree_Access /= null);
3113 pragma Assert (Kind (C.Tree_Access) = Entire_Object
3115 Kind (C.Tree_Access) = Reference);
3117 if Kind (C.Tree_Access) = Reference then
3118 if Get_All (C.Tree_Access) = null then
3120 raise Program_Error;
3124 Tree_Access => Get_All (C.Tree_Access));
3126 elsif Kind (C.Tree_Access) = Entire_Object then
3127 return (R => Folded, Found_Permission =>
3128 Children_Permission (C.Tree_Access));
3130 raise Program_Error;
3135 -- The name contains a function call, hence the given path is always
3136 -- new. We do not have to check for anything.
3138 when N_Function_Call =>
3139 return (R => Function_Call);
3142 raise Program_Error;
3144 end Get_Perm_Or_Tree;
3150 function Get_Perm_Tree
3152 return Perm_Tree_Access
3157 -- Base identifier. Normally those are the roots of the trees stored
3158 -- in the permission environment.
3160 when N_Defining_Identifier =>
3161 raise Program_Error;
3167 P : constant Node_Id := Entity (N);
3169 C : constant Perm_Tree_Access :=
3170 Get (Current_Perm_Env, Unique_Entity (P));
3173 -- Setting the initialization map to True, so that this
3174 -- variable cannot be ignored anymore when looking at end
3175 -- of elaboration of package.
3177 Set (Current_Initialization_Map, Unique_Entity (P), True);
3180 -- No null possible here, there are no parents for the path.
3181 -- This means we are using a global variable without adding
3182 -- it in environment with a global aspect.
3184 Illegal_Global_Usage (N);
3190 when N_Type_Conversion
3191 | N_Unchecked_Type_Conversion
3192 | N_Qualified_Expression
3194 return Get_Perm_Tree (Expression (N));
3196 when N_Parameter_Specification =>
3197 return Get_Perm_Tree (Defining_Identifier (N));
3199 -- We get the permission tree of its prefix, and then get either the
3200 -- subtree associated with that specific selection, or if we have a
3201 -- leaf that folds its children, we unroll it in one step.
3203 when N_Selected_Component =>
3205 C : constant Perm_Tree_Access :=
3206 Get_Perm_Tree (Prefix (N));
3210 -- If null then it means we went through a function call
3215 pragma Assert (Kind (C) = Entire_Object
3216 or else Kind (C) = Record_Component);
3218 if Kind (C) = Record_Component then
3219 -- The tree is unfolded. We just return the subtree.
3222 Selected_Component : constant Entity_Id :=
3223 Entity (Selector_Name (N));
3224 Selected_C : constant Perm_Tree_Access :=
3226 (Component (C), Selected_Component);
3229 if Selected_C = null then
3230 return Other_Components (C);
3235 elsif Kind (C) = Entire_Object then
3237 -- Expand the tree. Replace the node with
3238 -- Record_Component.
3242 -- Create the unrolled nodes
3244 Son : Perm_Tree_Access;
3246 Child_Perm : constant Perm_Kind :=
3247 Children_Permission (C);
3251 -- We change the current node from Entire_Object to
3252 -- Record_Component with same permission and an empty
3253 -- hash table as component list.
3256 (Kind => Record_Component,
3257 Is_Node_Deep => Is_Node_Deep (C),
3258 Permission => Permission (C),
3259 Component => Perm_Tree_Maps.Nil,
3261 new Perm_Tree_Wrapper'
3263 (Kind
=> Entire_Object
,
3264 -- Is_Node_Deep is true, to be conservative
3265 Is_Node_Deep
=> True,
3266 Permission
=> Child_Perm
,
3267 Children_Permission
=> Child_Perm
)
3271 -- We fill the hash table with all sons of the record,
3272 -- with basic Entire_Objects nodes.
3273 Elem
:= First_Component_Or_Discriminant
3274 (Etype
(Prefix
(N
)));
3276 while Present
(Elem
) loop
3277 Son
:= new Perm_Tree_Wrapper
'
3279 (Kind => Entire_Object,
3280 Is_Node_Deep => Is_Deep (Etype (Elem)),
3281 Permission => Child_Perm,
3282 Children_Permission => Child_Perm));
3285 (C.all.Tree.Component, Elem, Son);
3287 Next_Component_Or_Discriminant (Elem);
3290 -- we return the tree to the sons, so that the recursion
3294 Selected_Component : constant Entity_Id :=
3295 Entity (Selector_Name (N));
3297 Selected_C : constant Perm_Tree_Access :=
3299 (Component (C), Selected_Component);
3302 pragma Assert (Selected_C /= null);
3309 raise Program_Error;
3313 -- We set the permission tree of its prefix, and then we extract from
3314 -- the returned pointer the subtree. If folded, we unroll the tree at
3317 when N_Indexed_Component
3321 C : constant Perm_Tree_Access :=
3322 Get_Perm_Tree (Prefix (N));
3326 -- If null then we went through a function call
3331 pragma Assert (Kind (C) = Entire_Object
3332 or else Kind (C) = Array_Component);
3334 if Kind (C) = Array_Component then
3335 -- The tree is unfolded. We just return the elem subtree
3337 pragma Assert (Get_Elem (C) = null);
3339 return Get_Elem (C);
3340 elsif Kind (C) = Entire_Object then
3342 -- Expand the tree. Replace node with Array_Component.
3344 Son : Perm_Tree_Access;
3347 Son := new Perm_Tree_Wrapper'
3349 (Kind
=> Entire_Object
,
3350 Is_Node_Deep
=> Is_Node_Deep
(C
),
3351 Permission
=> Children_Permission
(C
),
3352 Children_Permission
=> Children_Permission
(C
)));
3354 -- We change the current node from Entire_Object
3355 -- to Array_Component with same permission and the
3356 -- previously defined son.
3358 C
.all.Tree
:= (Kind
=> Array_Component
,
3359 Is_Node_Deep
=> Is_Node_Deep
(C
),
3360 Permission
=> Permission
(C
),
3363 return Get_Elem
(C
);
3366 raise Program_Error
;
3370 -- We get the permission tree of its prefix, and then get either the
3371 -- subtree associated with that specific selection, or if we have a
3372 -- leaf that folds its children, we unroll the tree.
3374 when N_Explicit_Dereference
=>
3376 C
: Perm_Tree_Access
;
3379 C
:= Get_Perm_Tree
(Prefix
(N
));
3382 -- If null, we went through a function call
3387 pragma Assert
(Kind
(C
) = Entire_Object
3388 or else Kind
(C
) = Reference
);
3390 if Kind
(C
) = Reference
then
3391 -- The tree is unfolded. We return the elem subtree
3393 if Get_All
(C
) = null then
3395 raise Program_Error
;
3399 elsif Kind
(C
) = Entire_Object
then
3401 -- Expand the tree. Replace the node with Reference.
3403 Son
: Perm_Tree_Access
;
3406 Son
:= new Perm_Tree_Wrapper
'
3408 (Kind => Entire_Object,
3409 Is_Node_Deep => Is_Deep (Etype (N)),
3410 Permission => Children_Permission (C),
3411 Children_Permission => Children_Permission (C)));
3413 -- We change the current node from Entire_Object to
3414 -- Reference with same permission and the previous son.
3416 pragma Assert (Is_Node_Deep (C));
3418 C.all.Tree := (Kind => Reference,
3419 Is_Node_Deep => Is_Node_Deep (C),
3420 Permission => Permission (C),
3426 raise Program_Error;
3430 -- No permission tree for function calls
3432 when N_Function_Call =>
3436 raise Program_Error;
3444 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
3486 function Has_Alias_Deep (Typ : Entity_Id) return Boolean;
3487 function Has_Alias_Deep (Typ : Entity_Id) return Boolean
3492 if Is_Array_Type (Typ)
3493 and then Has_Aliased_Components (Typ)
3497 -- Note: Has_Aliased_Components applies only to arrays
3499 elsif Is_Record_Type (Typ) then
3500 -- It is possible to have an aliased discriminant, so they must be
3501 -- checked along with normal components.
3503 Comp := First_Component_Or_Discriminant (Typ);
3504 while Present (Comp) loop
3505 if Is_Aliased (Comp)
3506 or else Is_Aliased (Etype (Comp))
3511 if Has_Alias_Deep (Etype (Comp)) then
3515 Next_Component_Or_Discriminant (Comp);
3519 return Is_Aliased (Typ);
3529 return Has_Alias_Deep (Etype (N));
3531 when N_Defining_Identifier =>
3532 return Has_Alias_Deep (Etype (N));
3534 when N_Type_Conversion
3535 | N_Unchecked_Type_Conversion
3536 | N_Qualified_Expression
3538 return Has_Alias (Expression (N));
3540 when N_Parameter_Specification =>
3541 return Has_Alias (Defining_Identifier (N));
3543 when N_Selected_Component =>
3544 case Nkind (Selector_Name (N)) is
3545 when N_Identifier =>
3546 if Is_Aliased (Entity (Selector_Name (N))) then
3550 when others => null;
3554 return Has_Alias (Prefix (N));
3556 when N_Indexed_Component
3559 return Has_Alias (Prefix (N));
3561 when N_Explicit_Dereference =>
3564 when N_Function_Call =>
3567 when N_Attribute_Reference =>
3568 if Is_Deep (Etype (Prefix (N))) then
3569 raise Program_Error;
3578 -------------------------
3579 -- Has_Array_Component --
3580 -------------------------
3582 function Has_Array_Component (N : Node_Id) return Boolean is
3585 -- Base identifier. There is no array component here.
3589 | N_Defining_Identifier
3593 -- We check if the expression inside the conversion has an array
3596 when N_Type_Conversion
3597 | N_Unchecked_Type_Conversion
3598 | N_Qualified_Expression
3600 return Has_Array_Component (Expression (N));
3602 -- We check if the prefix has an array component
3604 when N_Selected_Component =>
3605 return Has_Array_Component (Prefix (N));
3607 -- We found the array component, return True
3609 when N_Indexed_Component
3614 -- We check if the prefix has an array component
3616 when N_Explicit_Dereference =>
3617 return Has_Array_Component (Prefix (N));
3619 when N_Function_Call =>
3623 raise Program_Error;
3625 end Has_Array_Component;
3627 ----------------------------
3628 -- Has_Function_Component --
3629 ----------------------------
3631 function Has_Function_Component (N : Node_Id) return Boolean is
3634 -- Base identifier. There is no function component here.
3638 | N_Defining_Identifier
3642 -- We check if the expression inside the conversion has a function
3645 when N_Type_Conversion
3646 | N_Unchecked_Type_Conversion
3647 | N_Qualified_Expression
3649 return Has_Function_Component (Expression (N));
3651 -- We check if the prefix has a function component
3653 when N_Selected_Component =>
3654 return Has_Function_Component (Prefix (N));
3656 -- We check if the prefix has a function component
3658 when N_Indexed_Component
3661 return Has_Function_Component (Prefix (N));
3663 -- We check if the prefix has a function component
3665 when N_Explicit_Dereference =>
3666 return Has_Function_Component (Prefix (N));
3668 -- We found the function component, return True
3670 when N_Function_Call =>
3674 raise Program_Error;
3677 end Has_Function_Component;
3683 procedure Hp (P : Perm_Env) is
3684 Elem : Perm_Tree_Maps.Key_Option;
3687 Elem := Get_First_Key (P);
3688 while Elem.Present loop
3689 Print_Node_Briefly (Elem.K);
3690 Elem := Get_Next_Key (P);
3694 --------------------------
3695 -- Illegal_Global_Usage --
3696 --------------------------
3698 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
3700 Error_Msg_NE ("cannot use global variable & of deep type", N, N);
3701 Error_Msg_N ("\without prior declaration in a Global aspect", N);
3703 Errout.Finalize (Last_Call => True);
3704 Errout.Output_Messages;
3705 Exit_Program (E_Errors);
3706 end Illegal_Global_Usage;
3708 --------------------
3709 -- Is_Borrowed_In --
3710 --------------------
3712 function Is_Borrowed_In (E : Entity_Id) return Boolean is
3714 return Is_Access_Type (Etype (E))
3715 and then not Is_Access_Constant (Etype (E));
3722 function Is_Deep (E : Entity_Id) return Boolean is
3723 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
3725 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
3727 Pack_Decl : Node_Id;
3730 if Is_Itype (E) then
3731 Decl := Associated_Node_For_Itype (E);
3736 Pack_Decl := Parent (Parent (Decl));
3738 if Nkind (Pack_Decl) /= N_Package_Declaration then
3743 Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
3744 and then Get_SPARK_Mode_From_Annotation
3745 (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
3746 end Is_Private_Entity_Mode_Off;
3748 pragma Assert (Is_Type (E));
3757 -- Just check the depth of its component type
3762 return Is_Deep (Component_Type (E));
3764 when E_String_Literal_Subtype =>
3767 -- Per RM 8.11 for class-wide types
3769 when E_Class_Wide_Subtype
3774 -- ??? What about hidden components
3783 Elmt := First_Component_Or_Discriminant (E);
3784 while Present (Elmt) loop
3785 if Is_Deep (Etype (Elmt)) then
3788 Next_Component_Or_Discriminant (Elmt);
3795 when Private_Kind =>
3796 if Is_Private_Entity_Mode_Off (E) then
3799 if Present (Full_View (E)) then
3800 return Is_Deep (Full_View (E));
3806 when E_Incomplete_Type =>
3809 when E_Incomplete_Subtype =>
3812 -- No problem with synchronized types
3814 when E_Protected_Type
3815 | E_Protected_Subtype
3821 when E_Exception_Type =>
3825 raise Program_Error;
3833 function Is_Shallow (E : Entity_Id) return Boolean is
3835 pragma Assert (Is_Type (E));
3836 return not Is_Deep (E);
3843 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
3844 Nam : Node_Id := Name (N);
3845 Stmt : Node_Id := N;
3848 while Present (Stmt) loop
3849 Stmt := Parent (Stmt);
3850 if Nkind (Stmt) = N_Loop_Statement then
3851 Nam := Identifier (Stmt);
3856 return Entity (Nam);
3862 function Lub (P1, P2 : Perm_Kind) return Perm_Kind
3900 procedure Merge_Envs
3901 (Target : in out Perm_Env;
3902 Source : in out Perm_Env)
3904 procedure Merge_Trees
3905 (Target : Perm_Tree_Access;
3906 Source : Perm_Tree_Access);
3908 procedure Merge_Trees
3909 (Target : Perm_Tree_Access;
3910 Source : Perm_Tree_Access)
3912 procedure Apply_Glb_Tree
3913 (A : Perm_Tree_Access;
3916 procedure Apply_Glb_Tree
3917 (A : Perm_Tree_Access;
3921 A.all.Tree.Permission := Glb (Permission (A), P);
3924 when Entire_Object =>
3925 A.all.Tree.Children_Permission :=
3926 Glb (Children_Permission (A), P);
3929 Apply_Glb_Tree (Get_All (A), P);
3931 when Array_Component =>
3932 Apply_Glb_Tree (Get_Elem (A), P);
3934 when Record_Component =>
3936 Comp : Perm_Tree_Access;
3938 Comp := Perm_Tree_Maps.Get_First (Component (A));
3939 while Comp /= null loop
3940 Apply_Glb_Tree (Comp, P);
3941 Comp := Perm_Tree_Maps.Get_Next (Component (A));
3944 Apply_Glb_Tree (Other_Components (A), P);
3949 Perm : constant Perm_Kind :=
3950 Glb (Permission (Target), Permission (Source));
3953 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
3954 Target.all.Tree.Permission := Perm;
3956 case Kind (Target) is
3957 when Entire_Object =>
3959 Child_Perm : constant Perm_Kind :=
3960 Children_Permission (Target);
3963 case Kind (Source) is
3964 when Entire_Object =>
3965 Target.all.Tree.Children_Permission :=
3966 Glb (Child_Perm, Children_Permission (Source));
3969 Copy_Tree (Source, Target);
3970 Target.all.Tree.Permission := Perm;
3971 Apply_Glb_Tree (Get_All (Target), Child_Perm);
3973 when Array_Component =>
3974 Copy_Tree (Source, Target);
3975 Target.all.Tree.Permission := Perm;
3976 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
3978 when Record_Component =>
3979 Copy_Tree (Source, Target);
3980 Target.all.Tree.Permission := Perm;
3982 Comp : Perm_Tree_Access;
3986 Perm_Tree_Maps.Get_First (Component (Target));
3987 while Comp /= null loop
3988 -- Apply glb tree on every component subtree
3990 Apply_Glb_Tree (Comp, Child_Perm);
3991 Comp := Perm_Tree_Maps.Get_Next
3992 (Component (Target));
3995 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4000 case Kind (Source) is
4001 when Entire_Object =>
4002 Apply_Glb_Tree (Get_All (Target),
4003 Children_Permission (Source));
4006 Merge_Trees (Get_All (Target), Get_All (Source));
4009 raise Program_Error;
4013 when Array_Component =>
4014 case Kind (Source) is
4015 when Entire_Object =>
4016 Apply_Glb_Tree (Get_Elem (Target),
4017 Children_Permission (Source));
4019 when Array_Component =>
4020 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4023 raise Program_Error;
4027 when Record_Component =>
4028 case Kind (Source) is
4029 when Entire_Object =>
4031 Child_Perm : constant Perm_Kind :=
4032 Children_Permission (Source);
4034 Comp : Perm_Tree_Access;
4037 Comp := Perm_Tree_Maps.Get_First
4038 (Component (Target));
4039 while Comp /= null loop
4040 -- Apply glb tree on every component subtree
4042 Apply_Glb_Tree (Comp, Child_Perm);
4044 Perm_Tree_Maps.Get_Next (Component (Target));
4046 Apply_Glb_Tree (Other_Components (Target), Child_Perm);
4049 when Record_Component =>
4051 Key_Source : Perm_Tree_Maps.Key_Option;
4052 CompTarget : Perm_Tree_Access;
4053 CompSource : Perm_Tree_Access;
4056 Key_Source := Perm_Tree_Maps.Get_First_Key
4057 (Component (Source));
4059 while Key_Source.Present loop
4060 CompSource := Perm_Tree_Maps.Get
4061 (Component (Source), Key_Source.K);
4062 CompTarget := Perm_Tree_Maps.Get
4063 (Component (Target), Key_Source.K);
4065 pragma Assert (CompSource /= null);
4066 Merge_Trees (CompTarget, CompSource);
4068 Key_Source := Perm_Tree_Maps.Get_Next_Key
4069 (Component (Source));
4072 Merge_Trees (Other_Components (Target),
4073 Other_Components (Source));
4077 raise Program_Error;
4083 CompTarget : Perm_Tree_Access;
4084 CompSource : Perm_Tree_Access;
4085 KeyTarget : Perm_Tree_Maps.Key_Option;
4088 KeyTarget := Get_First_Key (Target);
4089 -- Iterate over every tree of the environment in the target, and merge
4090 -- it with the source if there is such a similar one that exists. If
4091 -- there is none, then skip.
4092 while KeyTarget.Present loop
4094 CompSource := Get (Source, KeyTarget.K);
4095 CompTarget := Get (Target, KeyTarget.K);
4097 pragma Assert (CompTarget /= null);
4099 if CompSource /= null then
4100 Merge_Trees (CompTarget, CompSource);
4101 Remove (Source, KeyTarget.K);
4104 KeyTarget := Get_Next_Key (Target);
4107 -- Iterate over every tree of the environment of the source. And merge
4108 -- again. If there is not any tree of the target then just copy the tree
4109 -- from source to target.
4111 KeySource : Perm_Tree_Maps.Key_Option;
4113 KeySource := Get_First_Key (Source);
4114 while KeySource.Present loop
4116 CompSource := Get (Source, KeySource.K);
4117 CompTarget := Get (Target, KeySource.K);
4119 if CompTarget = null then
4120 CompTarget := new Perm_Tree_Wrapper'(CompSource
.all);
4121 Copy_Tree
(CompSource
, CompTarget
);
4122 Set
(Target
, KeySource
.K
, CompTarget
);
4124 Merge_Trees
(CompTarget
, CompSource
);
4127 KeySource
:= Get_Next_Key
(Source
);
4138 procedure Perm_Error
4141 Found_Perm
: Perm_Kind
)
4143 procedure Set_Root_Object
4145 Obj
: out Entity_Id
;
4146 Deref
: out Boolean);
4147 -- Set the root object Obj, and whether the path contains a dereference,
4148 -- from a path Path.
4150 ---------------------
4151 -- Set_Root_Object --
4152 ---------------------
4154 procedure Set_Root_Object
4156 Obj
: out Entity_Id
;
4157 Deref
: out Boolean)
4160 case Nkind
(Path
) is
4164 Obj
:= Entity
(Path
);
4167 when N_Type_Conversion
4168 | N_Unchecked_Type_Conversion
4169 | N_Qualified_Expression
4171 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
4173 when N_Indexed_Component
4174 | N_Selected_Component
4177 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4179 when N_Explicit_Dereference
=>
4180 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
4184 raise Program_Error
;
4186 end Set_Root_Object
;
4193 -- Start of processing for Perm_Error
4196 Set_Root_Object
(N
, Root
, Is_Deref
);
4200 ("insufficient permission on dereference from &", N
, Root
);
4202 Error_Msg_NE
("insufficient permission for &", N
, Root
);
4205 Perm_Mismatch
(Perm
, Found_Perm
, N
);
4208 -------------------------------
4209 -- Perm_Error_Subprogram_End --
4210 -------------------------------
4212 procedure Perm_Error_Subprogram_End
4216 Found_Perm
: Perm_Kind
)
4219 Error_Msg_Node_2
:= Subp
;
4220 Error_Msg_NE
("insufficient permission for & when returning from &",
4222 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
4223 end Perm_Error_Subprogram_End
;
4229 procedure Process_Path
(N
: Node_Id
) is
4230 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
4232 -- We ignore if yielding to synchronized
4235 and then Is_Synchronized_Object
(Root
)
4240 -- We ignore shallow unaliased. They are checked in flow analysis,
4241 -- allowing backward compatibility.
4243 if not Has_Alias
(N
)
4244 and then Is_Shallow
(Etype
(N
))
4250 Perm_N
: constant Perm_Kind
:= Get_Perm
(N
);
4254 case Current_Checking_Mode
is
4255 -- Check permission R, do nothing
4258 if Perm_N
not in Read_Perm
then
4259 Perm_Error
(N
, Read_Only
, Perm_N
);
4262 -- If shallow type no need for RW, only R
4265 if Is_Shallow
(Etype
(N
)) then
4266 if Perm_N
not in Read_Perm
then
4267 Perm_Error
(N
, Read_Only
, Perm_N
);
4270 -- Check permission RW if deep
4272 if Perm_N
/= Read_Write
then
4273 Perm_Error
(N
, Read_Write
, Perm_N
);
4277 -- Set permission to W to the path and any of its prefix
4279 Tree
: constant Perm_Tree_Access
:=
4280 Set_Perm_Prefixes_Move
(N
, Move
);
4284 -- We went through a function call, no permission to
4290 -- Set permissions to
4291 -- No for any extension with more .all
4292 -- W for any deep extension with same number of .all
4293 -- RW for any shallow extension with same number of .all
4295 Set_Perm_Extensions_Move
(Tree
, Etype
(N
));
4299 -- Check permission RW
4302 if Perm_N
/= Read_Write
then
4303 Perm_Error
(N
, Read_Write
, Perm_N
);
4307 -- Set permission to No to the path and any of its prefix up
4308 -- to the first .all and then W.
4310 Tree
: constant Perm_Tree_Access
:=
4311 Set_Perm_Prefixes_Move
(N
, Super_Move
);
4315 -- We went through a function call, no permission to
4321 -- Set permissions to No on any strict extension of the path
4323 Set_Perm_Extensions
(Tree
, No_Access
);
4326 -- Check permission W
4329 if Perm_N
not in Write_Perm
then
4330 Perm_Error
(N
, Write_Only
, Perm_N
);
4333 -- If the tree has an array component, then the permissions do
4334 -- not get modified by the assignment.
4336 if Has_Array_Component
(N
) then
4340 -- Same if has function component
4342 if Has_Function_Component
(N
) then
4347 -- Get the permission tree for the path
4349 Tree
: constant Perm_Tree_Access
:=
4352 Dummy
: Perm_Tree_Access
;
4356 -- We went through a function call, no permission to
4362 -- Set permission RW for it and all of its extensions
4364 Tree
.all.Tree
.Permission
:= Read_Write
;
4366 Set_Perm_Extensions
(Tree
, Read_Write
);
4368 -- Normalize the permission tree
4370 Dummy
:= Set_Perm_Prefixes_Assign
(N
);
4373 -- Check permission W
4376 if Perm_N
not in Write_Perm
then
4377 Perm_Error
(N
, Write_Only
, Perm_N
);
4381 -- Set permission to No to the path and any of its prefixes
4383 Tree
: constant Perm_Tree_Access
:=
4384 Set_Perm_Prefixes_Borrow_Out
(N
);
4388 -- We went through a function call, no permission to
4394 -- Set permissions to No on any strict extension of the path
4396 Set_Perm_Extensions
(Tree
, No_Access
);
4400 if Perm_N
not in Read_Perm
then
4401 Perm_Error
(N
, Read_Only
, Perm_N
);
4404 if Is_By_Copy_Type
(Etype
(N
)) then
4409 -- Set permission to No on the path and any of its prefixes
4411 Tree
: constant Perm_Tree_Access
:=
4412 Set_Perm_Prefixes_Observe
(N
);
4416 -- We went through a function call, no permission to
4422 -- Set permissions to No on any strict extension of the path
4424 Set_Perm_Extensions
(Tree
, Read_Only
);
4430 -------------------------
4431 -- Return_Declarations --
4432 -------------------------
4434 procedure Return_Declarations
(L
: List_Id
) is
4436 procedure Return_Declaration
(Decl
: Node_Id
);
4437 -- Check correct permissions for every declared object
4439 ------------------------
4440 -- Return_Declaration --
4441 ------------------------
4443 procedure Return_Declaration
(Decl
: Node_Id
) is
4445 if Nkind
(Decl
) = N_Object_Declaration
then
4446 -- Check RW for object declared, unless the object has never been
4449 if Get
(Current_Initialization_Map
,
4450 Unique_Entity
(Defining_Identifier
(Decl
))) = False
4455 -- We ignore shallow unaliased. They are checked in flow analysis,
4456 -- allowing backward compatibility.
4458 if not Has_Alias
(Defining_Identifier
(Decl
))
4459 and then Is_Shallow
(Etype
(Defining_Identifier
(Decl
)))
4465 Elem
: constant Perm_Tree_Access
:=
4466 Get
(Current_Perm_Env
,
4467 Unique_Entity
(Defining_Identifier
(Decl
)));
4471 -- Here we are on a declaration. Hence it should have been
4472 -- added in the environment when analyzing this node with
4473 -- mode Read. Hence it is not possible to find a null
4477 raise Program_Error
;
4480 if Permission
(Elem
) /= Read_Write
then
4481 Perm_Error
(Decl
, Read_Write
, Permission
(Elem
));
4485 end Return_Declaration
;
4491 -- Start of processing for Return_Declarations
4495 while Present
(N
) loop
4496 Return_Declaration
(N
);
4499 end Return_Declarations
;
4501 --------------------
4502 -- Return_Globals --
4503 --------------------
4505 procedure Return_Globals
(Subp
: Entity_Id
) is
4507 procedure Return_Globals_From_List
4508 (First_Item
: Node_Id
;
4509 Kind
: Formal_Kind
);
4510 -- Return global items from the list starting at Item
4512 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
4513 -- Return global items for the mode Global_Mode
4515 ------------------------------
4516 -- Return_Globals_From_List --
4517 ------------------------------
4519 procedure Return_Globals_From_List
4520 (First_Item
: Node_Id
;
4523 Item
: Node_Id
:= First_Item
;
4527 while Present
(Item
) loop
4530 -- Ignore abstract states, which play no role in pointer aliasing
4532 if Ekind
(E
) = E_Abstract_State
then
4535 Return_Parameter_Or_Global
(E
, Kind
, Subp
);
4539 end Return_Globals_From_List
;
4541 ----------------------------
4542 -- Return_Globals_Of_Mode --
4543 ----------------------------
4545 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
4550 when Name_Input | Name_Proof_In
=>
4551 Kind
:= E_In_Parameter
;
4553 Kind
:= E_Out_Parameter
;
4555 Kind
:= E_In_Out_Parameter
;
4557 raise Program_Error
;
4560 -- Return both global items from Global and Refined_Global pragmas
4562 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
4563 Return_Globals_From_List
4564 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
4565 end Return_Globals_Of_Mode
;
4567 -- Start of processing for Return_Globals
4570 Return_Globals_Of_Mode
(Name_Proof_In
);
4571 Return_Globals_Of_Mode
(Name_Input
);
4572 Return_Globals_Of_Mode
(Name_Output
);
4573 Return_Globals_Of_Mode
(Name_In_Out
);
4576 --------------------------------
4577 -- Return_Parameter_Or_Global --
4578 --------------------------------
4580 procedure Return_Parameter_Or_Global
4585 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
4586 pragma Assert
(Elem
/= null);
4589 -- Shallow unaliased parameters and globals cannot introduce pointer
4592 if not Has_Alias
(Id
) and then Is_Shallow
(Etype
(Id
)) then
4595 -- Observed IN parameters and globals need not return a permission to
4598 elsif Mode
= E_In_Parameter
and then not Is_Borrowed_In
(Id
) then
4601 -- All other parameters and globals should return with mode RW to the
4605 if Permission
(Elem
) /= Read_Write
then
4606 Perm_Error_Subprogram_End
4610 Found_Perm
=> Permission
(Elem
));
4613 end Return_Parameter_Or_Global
;
4615 -----------------------
4616 -- Return_Parameters --
4617 -----------------------
4619 procedure Return_Parameters
(Subp
: Entity_Id
) is
4623 Formal
:= First_Formal
(Subp
);
4624 while Present
(Formal
) loop
4625 Return_Parameter_Or_Global
(Formal
, Ekind
(Formal
), Subp
);
4626 Next_Formal
(Formal
);
4628 end Return_Parameters
;
4630 -------------------------
4631 -- Set_Perm_Extensions --
4632 -------------------------
4634 procedure Set_Perm_Extensions
4635 (T
: Perm_Tree_Access
;
4638 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
4640 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
)
4644 when Entire_Object
=>
4648 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
4650 when Array_Component
=>
4651 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
4653 -- Free every Component subtree
4655 when Record_Component
=>
4657 Comp
: Perm_Tree_Access
;
4660 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
4661 while Comp
/= null loop
4662 Free_Perm_Tree
(Comp
);
4663 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
4666 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
4669 end Free_Perm_Tree_Children
;
4671 Son
: constant Perm_Tree
:=
4673 (Kind => Entire_Object,
4674 Is_Node_Deep => Is_Node_Deep (T),
4675 Permission => Permission (T),
4676 Children_Permission => P);
4679 Free_Perm_Tree_Children (T);
4681 end Set_Perm_Extensions;
4683 ------------------------------
4684 -- Set_Perm_Extensions_Move --
4685 ------------------------------
4687 procedure Set_Perm_Extensions_Move
4688 (T : Perm_Tree_Access;
4692 if not Is_Node_Deep (T) then
4693 -- We are a shallow extension with same number of .all
4695 Set_Perm_Extensions (T, Read_Write);
4699 -- We are a deep extension here (or the moved deep path)
4701 T.all.Tree.Permission := Write_Only;
4703 case T.all.Tree.Kind is
4704 -- Unroll the tree depending on the type
4706 when Entire_Object =>
4709 | E_String_Literal_Subtype
4711 Set_Perm_Extensions (T, No_Access);
4713 -- No need to unroll here, directly put sons to No_Access
4716 if Ekind (E) in Access_Subprogram_Kind then
4719 Set_Perm_Extensions (T, No_Access);
4722 -- No unrolling done, too complicated
4724 when E_Class_Wide_Subtype
4727 | E_Incomplete_Subtype
4732 Set_Perm_Extensions (T, No_Access);
4734 -- Expand the tree. Replace the node with Array component.
4737 | E_Array_Subtype =>
4739 Son : Perm_Tree_Access;
4742 Son := new Perm_Tree_Wrapper'
4744 (Kind
=> Entire_Object
,
4745 Is_Node_Deep
=> Is_Node_Deep
(T
),
4746 Permission
=> Read_Write
,
4747 Children_Permission
=> Read_Write
));
4749 Set_Perm_Extensions_Move
(Son
, Component_Type
(E
));
4751 -- We change the current node from Entire_Object to
4752 -- Reference with Write_Only and the previous son.
4754 pragma Assert
(Is_Node_Deep
(T
));
4756 T
.all.Tree
:= (Kind
=> Array_Component
,
4757 Is_Node_Deep
=> Is_Node_Deep
(T
),
4758 Permission
=> Write_Only
,
4762 -- Unroll, and set permission extensions with component type
4766 | E_Record_Type_With_Private
4767 | E_Record_Subtype_With_Private
4769 | E_Protected_Subtype
4772 -- Expand the tree. Replace the node with
4773 -- Record_Component.
4777 Son
: Perm_Tree_Access
;
4780 -- We change the current node from Entire_Object to
4781 -- Record_Component with same permission and an empty
4782 -- hash table as component list.
4784 pragma Assert
(Is_Node_Deep
(T
));
4787 (Kind
=> Record_Component
,
4788 Is_Node_Deep
=> Is_Node_Deep
(T
),
4789 Permission
=> Write_Only
,
4790 Component
=> Perm_Tree_Maps
.Nil
,
4792 new Perm_Tree_Wrapper
'
4794 (Kind => Entire_Object,
4795 Is_Node_Deep => True,
4796 Permission => Read_Write,
4797 Children_Permission => Read_Write)
4801 -- We fill the hash table with all sons of the record,
4802 -- with basic Entire_Objects nodes.
4803 Elem := First_Component_Or_Discriminant (E);
4804 while Present (Elem) loop
4805 Son := new Perm_Tree_Wrapper'
4807 (Kind
=> Entire_Object
,
4808 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
4809 Permission
=> Read_Write
,
4810 Children_Permission
=> Read_Write
));
4812 Set_Perm_Extensions_Move
(Son
, Etype
(Elem
));
4815 (T
.all.Tree
.Component
, Elem
, Son
);
4817 Next_Component_Or_Discriminant
(Elem
);
4823 | E_Limited_Private_Type
4824 | E_Limited_Private_Subtype
4826 Set_Perm_Extensions_Move
(T
, Underlying_Type
(E
));
4829 raise Program_Error
;
4833 -- Now the son does not have the same number of .all
4834 Set_Perm_Extensions
(T
, No_Access
);
4836 when Array_Component
=>
4837 Set_Perm_Extensions_Move
(Get_Elem
(T
), Component_Type
(E
));
4839 when Record_Component
=>
4841 Comp
: Perm_Tree_Access
;
4845 It
:= First_Component_Or_Discriminant
(E
);
4846 while It
/= Empty
loop
4847 Comp
:= Perm_Tree_Maps
.Get
(Component
(T
), It
);
4848 pragma Assert
(Comp
/= null);
4849 Set_Perm_Extensions_Move
(Comp
, It
);
4850 It
:= Next_Component_Or_Discriminant
(E
);
4853 Set_Perm_Extensions
(Other_Components
(T
), No_Access
);
4856 end Set_Perm_Extensions_Move
;
4858 ------------------------------
4859 -- Set_Perm_Prefixes_Assign --
4860 ------------------------------
4862 function Set_Perm_Prefixes_Assign
4864 return Perm_Tree_Access
4866 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(N
);
4869 pragma Assert
(Current_Checking_Mode
= Assign
);
4871 -- The function should not be called if has_function_component
4873 pragma Assert
(C
/= null);
4876 when Entire_Object
=>
4877 pragma Assert
(Children_Permission
(C
) = Read_Write
);
4878 C
.all.Tree
.Permission
:= Read_Write
;
4881 pragma Assert
(Get_All
(C
) /= null);
4883 C
.all.Tree
.Permission
:=
4884 Lub
(Permission
(C
), Permission
(Get_All
(C
)));
4886 when Array_Component
=>
4887 pragma Assert
(C
.all.Tree
.Get_Elem
/= null);
4889 -- Given that it is not possible to know which element has been
4890 -- assigned, then the permissions do not get changed in case of
4895 when Record_Component
=>
4897 Perm
: Perm_Kind
:= Read_Write
;
4899 Comp
: Perm_Tree_Access
;
4902 -- We take the Glb of all the descendants, and then update the
4903 -- permission of the node with it.
4904 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(C
));
4905 while Comp
/= null loop
4906 Perm
:= Glb
(Perm
, Permission
(Comp
));
4907 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(C
));
4910 Perm
:= Glb
(Perm
, Permission
(Other_Components
(C
)));
4912 C
.all.Tree
.Permission
:= Lub
(Permission
(C
), Perm
);
4917 -- Base identifier. End recursion here.
4921 | N_Defining_Identifier
4925 when N_Type_Conversion
4926 | N_Unchecked_Type_Conversion
4927 | N_Qualified_Expression
4929 return Set_Perm_Prefixes_Assign
(Expression
(N
));
4931 when N_Parameter_Specification
=>
4932 raise Program_Error
;
4934 -- Continue recursion on prefix
4936 when N_Selected_Component
=>
4937 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4939 -- Continue recursion on prefix
4941 when N_Indexed_Component
4944 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4946 -- Continue recursion on prefix
4948 when N_Explicit_Dereference
=>
4949 return Set_Perm_Prefixes_Assign
(Prefix
(N
));
4951 when N_Function_Call
=>
4952 raise Program_Error
;
4955 raise Program_Error
;
4958 end Set_Perm_Prefixes_Assign
;
4960 ----------------------------------
4961 -- Set_Perm_Prefixes_Borrow_Out --
4962 ----------------------------------
4964 function Set_Perm_Prefixes_Borrow_Out
4966 return Perm_Tree_Access
4969 pragma Assert
(Current_Checking_Mode
= Borrow_Out
);
4972 -- Base identifier. Set permission to No.
4978 P
: constant Node_Id
:= Entity
(N
);
4980 C
: constant Perm_Tree_Access
:=
4981 Get
(Current_Perm_Env
, Unique_Entity
(P
));
4983 pragma Assert
(C
/= null);
4986 -- Setting the initialization map to True, so that this
4987 -- variable cannot be ignored anymore when looking at end
4988 -- of elaboration of package.
4990 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
4992 C
.all.Tree
.Permission
:= No_Access
;
4996 when N_Type_Conversion
4997 | N_Unchecked_Type_Conversion
4998 | N_Qualified_Expression
5000 return Set_Perm_Prefixes_Borrow_Out
(Expression
(N
));
5002 when N_Parameter_Specification
5003 | N_Defining_Identifier
5005 raise Program_Error
;
5007 -- We set the permission tree of its prefix, and then we extract
5008 -- our subtree from the returned pointer and assign an adequate
5009 -- permission to it, if unfolded. If folded, we unroll the tree
5012 when N_Selected_Component
=>
5014 C
: constant Perm_Tree_Access
:=
5015 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5019 -- We went through a function call, do nothing
5024 -- The permission of the returned node should be No
5026 pragma Assert
(Permission
(C
) = No_Access
);
5028 pragma Assert
(Kind
(C
) = Entire_Object
5029 or else Kind
(C
) = Record_Component
);
5031 if Kind
(C
) = Record_Component
then
5032 -- The tree is unfolded. We just modify the permission and
5033 -- return the record subtree.
5036 Selected_Component
: constant Entity_Id
:=
5037 Entity
(Selector_Name
(N
));
5039 Selected_C
: Perm_Tree_Access
:=
5041 (Component
(C
), Selected_Component
);
5044 if Selected_C
= null then
5045 Selected_C
:= Other_Components
(C
);
5048 pragma Assert
(Selected_C
/= null);
5050 Selected_C
.all.Tree
.Permission
:= No_Access
;
5054 elsif Kind
(C
) = Entire_Object
then
5056 -- Expand the tree. Replace the node with
5057 -- Record_Component.
5061 -- Create an empty hash table
5063 Hashtbl
: Perm_Tree_Maps
.Instance
;
5065 -- We create the unrolled nodes, that will all have same
5066 -- permission than parent.
5068 Son
: Perm_Tree_Access
;
5070 ChildrenPerm
: constant Perm_Kind
:=
5071 Children_Permission
(C
);
5074 -- We change the current node from Entire_Object to
5075 -- Record_Component with same permission and an empty
5076 -- hash table as component list.
5079 (Kind
=> Record_Component
,
5080 Is_Node_Deep
=> Is_Node_Deep
(C
),
5081 Permission
=> Permission
(C
),
5082 Component
=> Hashtbl
,
5084 new Perm_Tree_Wrapper
'
5086 (Kind => Entire_Object,
5087 Is_Node_Deep => True,
5088 Permission => ChildrenPerm,
5089 Children_Permission => ChildrenPerm)
5092 -- We fill the hash table with all sons of the record,
5093 -- with basic Entire_Objects nodes.
5094 Elem := First_Component_Or_Discriminant
5095 (Etype (Prefix (N)));
5097 while Present (Elem) loop
5098 Son := new Perm_Tree_Wrapper'
5100 (Kind
=> Entire_Object
,
5101 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5102 Permission
=> ChildrenPerm
,
5103 Children_Permission
=> ChildrenPerm
));
5106 (C
.all.Tree
.Component
, Elem
, Son
);
5108 Next_Component_Or_Discriminant
(Elem
);
5111 -- Now we set the right field to No_Access, and then we
5112 -- return the tree to the sons, so that the recursion can
5116 Selected_Component
: constant Entity_Id
:=
5117 Entity
(Selector_Name
(N
));
5119 Selected_C
: Perm_Tree_Access
:=
5121 (Component
(C
), Selected_Component
);
5124 if Selected_C
= null then
5125 Selected_C
:= Other_Components
(C
);
5128 pragma Assert
(Selected_C
/= null);
5130 Selected_C
.all.Tree
.Permission
:= No_Access
;
5136 raise Program_Error
;
5140 -- We set the permission tree of its prefix, and then we extract
5141 -- from the returned pointer the subtree and assign an adequate
5142 -- permission to it, if unfolded. If folded, we unroll the tree in
5145 when N_Indexed_Component
5149 C
: constant Perm_Tree_Access
:=
5150 Set_Perm_Prefixes_Borrow_Out
(Prefix
(N
));
5154 -- We went through a function call, do nothing
5159 -- The permission of the returned node should be either W
5160 -- (because the recursive call sets <= Write_Only) or No
5161 -- (if another path has been moved with 'Access).
5163 pragma Assert
(Permission
(C
) = No_Access
);
5165 pragma Assert
(Kind
(C
) = Entire_Object
5166 or else Kind
(C
) = Array_Component
);
5168 if Kind
(C
) = Array_Component
then
5169 -- The tree is unfolded. We just modify the permission and
5170 -- return the elem subtree.
5172 pragma Assert
(Get_Elem
(C
) /= null);
5174 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5176 return Get_Elem
(C
);
5177 elsif Kind
(C
) = Entire_Object
then
5179 -- Expand the tree. Replace node with Array_Component.
5181 Son
: Perm_Tree_Access
;
5184 Son
:= new Perm_Tree_Wrapper
'
5186 (Kind => Entire_Object,
5187 Is_Node_Deep => Is_Node_Deep (C),
5188 Permission => No_Access,
5189 Children_Permission => Children_Permission (C)));
5191 -- We change the current node from Entire_Object
5192 -- to Array_Component with same permission and the
5193 -- previously defined son.
5195 C.all.Tree := (Kind => Array_Component,
5196 Is_Node_Deep => Is_Node_Deep (C),
5197 Permission => No_Access,
5200 return Get_Elem (C);
5203 raise Program_Error;
5207 -- We set the permission tree of its prefix, and then we extract
5208 -- from the returned pointer the subtree and assign an adequate
5209 -- permission to it, if unfolded. If folded, we unroll the tree
5212 when N_Explicit_Dereference =>
5214 C : constant Perm_Tree_Access :=
5215 Set_Perm_Prefixes_Borrow_Out (Prefix (N));
5219 -- We went through a function call. Do nothing.
5224 -- The permission of the returned node should be No
5226 pragma Assert (Permission (C) = No_Access);
5227 pragma Assert (Kind (C) = Entire_Object
5228 or else Kind (C) = Reference);
5230 if Kind (C) = Reference then
5231 -- The tree is unfolded. We just modify the permission and
5232 -- return the elem subtree.
5234 pragma Assert (Get_All (C) /= null);
5236 C.all.Tree.Get_All.all.Tree.Permission := No_Access;
5239 elsif Kind (C) = Entire_Object then
5241 -- Expand the tree. Replace the node with Reference.
5243 Son : Perm_Tree_Access;
5246 Son := new Perm_Tree_Wrapper'
5248 (Kind
=> Entire_Object
,
5249 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
5250 Permission
=> No_Access
,
5251 Children_Permission
=> Children_Permission
(C
)));
5253 -- We change the current node from Entire_Object to
5254 -- Reference with No_Access and the previous son.
5256 pragma Assert
(Is_Node_Deep
(C
));
5258 C
.all.Tree
:= (Kind
=> Reference
,
5259 Is_Node_Deep
=> Is_Node_Deep
(C
),
5260 Permission
=> No_Access
,
5266 raise Program_Error
;
5270 when N_Function_Call
=>
5274 raise Program_Error
;
5276 end Set_Perm_Prefixes_Borrow_Out
;
5278 ----------------------------
5279 -- Set_Perm_Prefixes_Move --
5280 ----------------------------
5282 function Set_Perm_Prefixes_Move
5283 (N
: Node_Id
; Mode
: Checking_Mode
)
5284 return Perm_Tree_Access
5288 -- Base identifier. Set permission to W or No depending on Mode.
5294 P
: constant Node_Id
:= Entity
(N
);
5296 C
: constant Perm_Tree_Access
:=
5297 Get
(Current_Perm_Env
, Unique_Entity
(P
));
5300 -- The base tree can be RW (first move from this base path) or
5301 -- W (already some extensions values moved), or even No_Access
5302 -- (extensions moved with 'Access). But it cannot be Read_Only
5303 -- (we get an error).
5305 if Permission
(C
) = Read_Only
then
5306 raise Unrecoverable_Error
;
5309 -- Setting the initialization map to True, so that this
5310 -- variable cannot be ignored anymore when looking at end
5311 -- of elaboration of package.
5313 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
5316 -- No null possible here, there are no parents for the path.
5317 -- This means we are using a global variable without adding
5318 -- it in environment with a global aspect.
5320 Illegal_Global_Usage
(N
);
5323 if Mode
= Super_Move
then
5324 C
.all.Tree
.Permission
:= No_Access
;
5326 C
.all.Tree
.Permission
:= Glb
(Write_Only
, Permission
(C
));
5332 when N_Type_Conversion
5333 | N_Unchecked_Type_Conversion
5334 | N_Qualified_Expression
5336 return Set_Perm_Prefixes_Move
(Expression
(N
), Mode
);
5338 when N_Parameter_Specification
5339 | N_Defining_Identifier
5341 raise Program_Error
;
5343 -- We set the permission tree of its prefix, and then we extract
5344 -- from the returned pointer our subtree and assign an adequate
5345 -- permission to it, if unfolded. If folded, we unroll the tree
5348 when N_Selected_Component
=>
5350 C
: constant Perm_Tree_Access
:=
5351 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5355 -- We went through a function call, do nothing
5360 -- The permission of the returned node should be either W
5361 -- (because the recursive call sets <= Write_Only) or No
5362 -- (if another path has been moved with 'Access).
5364 pragma Assert
(Permission
(C
) = No_Access
5365 or else Permission
(C
) = Write_Only
);
5367 if Mode
= Super_Move
then
5368 -- The permission of the returned node should be No (thanks
5369 -- to the recursion).
5371 pragma Assert
(Permission
(C
) = No_Access
);
5375 pragma Assert
(Kind
(C
) = Entire_Object
5376 or else Kind
(C
) = Record_Component
);
5378 if Kind
(C
) = Record_Component
then
5379 -- The tree is unfolded. We just modify the permission and
5380 -- return the record subtree.
5383 Selected_Component
: constant Entity_Id
:=
5384 Entity
(Selector_Name
(N
));
5386 Selected_C
: Perm_Tree_Access
:=
5388 (Component
(C
), Selected_Component
);
5391 if Selected_C
= null then
5392 -- If the hash table returns no element, then we fall
5393 -- into the part of Other_Components.
5394 pragma Assert
(Is_Tagged_Type
(Etype
(Prefix
(N
))));
5396 Selected_C
:= Other_Components
(C
);
5399 pragma Assert
(Selected_C
/= null);
5401 -- The Selected_C can have permissions:
5402 -- RW : first move in this path
5403 -- W : Already other moves in this path
5404 -- No : Already other moves with 'Access
5406 pragma Assert
(Permission
(Selected_C
) /= Read_Only
);
5407 if Mode
= Super_Move
then
5408 Selected_C
.all.Tree
.Permission
:= No_Access
;
5410 Selected_C
.all.Tree
.Permission
:=
5411 Glb
(Write_Only
, Permission
(Selected_C
));
5417 elsif Kind
(C
) = Entire_Object
then
5419 -- Expand the tree. Replace the node with
5420 -- Record_Component.
5424 -- Create an empty hash table
5426 Hashtbl
: Perm_Tree_Maps
.Instance
;
5428 -- We are in Move or Super_Move mode, hence we can assume
5429 -- that the Children_permission is RW, given that there
5430 -- are no other paths that could have been moved.
5432 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5434 -- We create the unrolled nodes, that will all have RW
5435 -- permission given that we are in move mode. We will
5436 -- then set the right node to W.
5438 Son
: Perm_Tree_Access
;
5441 -- We change the current node from Entire_Object to
5442 -- Record_Component with same permission and an empty
5443 -- hash table as component list.
5446 (Kind
=> Record_Component
,
5447 Is_Node_Deep
=> Is_Node_Deep
(C
),
5448 Permission
=> Permission
(C
),
5449 Component
=> Hashtbl
,
5451 new Perm_Tree_Wrapper
'
5453 (Kind => Entire_Object,
5454 Is_Node_Deep => True,
5455 Permission => Read_Write,
5456 Children_Permission => Read_Write)
5459 -- We fill the hash table with all sons of the record,
5460 -- with basic Entire_Objects nodes.
5461 Elem := First_Component_Or_Discriminant
5462 (Etype (Prefix (N)));
5464 while Present (Elem) loop
5465 Son := new Perm_Tree_Wrapper'
5467 (Kind
=> Entire_Object
,
5468 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
5469 Permission
=> Read_Write
,
5470 Children_Permission
=> Read_Write
));
5473 (C
.all.Tree
.Component
, Elem
, Son
);
5475 Next_Component_Or_Discriminant
(Elem
);
5478 -- Now we set the right field to Write_Only or No_Access
5479 -- depending on mode, and then we return the tree to the
5480 -- sons, so that the recursion can continue.
5483 Selected_Component
: constant Entity_Id
:=
5484 Entity
(Selector_Name
(N
));
5486 Selected_C
: Perm_Tree_Access
:=
5488 (Component
(C
), Selected_Component
);
5491 if Selected_C
= null then
5492 Selected_C
:= Other_Components
(C
);
5495 pragma Assert
(Selected_C
/= null);
5497 -- Given that this is a newly created Select_C, we can
5498 -- safely assume that its permission is Read_Write.
5500 pragma Assert
(Permission
(Selected_C
) =
5503 if Mode
= Super_Move
then
5504 Selected_C
.all.Tree
.Permission
:= No_Access
;
5506 Selected_C
.all.Tree
.Permission
:= Write_Only
;
5513 raise Program_Error
;
5517 -- We set the permission tree of its prefix, and then we extract
5518 -- from the returned pointer the subtree and assign an adequate
5519 -- permission to it, if unfolded. If folded, we unroll the tree
5522 when N_Indexed_Component
5526 C
: constant Perm_Tree_Access
:=
5527 Set_Perm_Prefixes_Move
(Prefix
(N
), Mode
);
5531 -- We went through a function call, do nothing
5536 -- The permission of the returned node should be either
5537 -- W (because the recursive call sets <= Write_Only)
5538 -- or No (if another path has been moved with 'Access)
5540 if Mode
= Super_Move
then
5541 pragma Assert
(Permission
(C
) = No_Access
);
5544 pragma Assert
(Permission
(C
) = Write_Only
5545 or else Permission
(C
) = No_Access
);
5549 pragma Assert
(Kind
(C
) = Entire_Object
5550 or else Kind
(C
) = Array_Component
);
5552 if Kind
(C
) = Array_Component
then
5553 -- The tree is unfolded. We just modify the permission and
5554 -- return the elem subtree.
5556 if Get_Elem
(C
) = null then
5558 raise Program_Error
;
5561 -- The Get_Elem can have permissions :
5562 -- RW : first move in this path
5563 -- W : Already other moves in this path
5564 -- No : Already other moves with 'Access
5566 pragma Assert
(Permission
(Get_Elem
(C
)) /= Read_Only
);
5568 if Mode
= Super_Move
then
5569 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:= No_Access
;
5571 C
.all.Tree
.Get_Elem
.all.Tree
.Permission
:=
5572 Glb
(Write_Only
, Permission
(Get_Elem
(C
)));
5575 return Get_Elem
(C
);
5576 elsif Kind
(C
) = Entire_Object
then
5578 -- Expand the tree. Replace node with Array_Component.
5580 -- We are in move mode, hence we can assume that the
5581 -- Children_permission is RW.
5583 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5585 Son
: Perm_Tree_Access
;
5588 Son
:= new Perm_Tree_Wrapper
'
5590 (Kind => Entire_Object,
5591 Is_Node_Deep => Is_Node_Deep (C),
5592 Permission => Read_Write,
5593 Children_Permission => Read_Write));
5595 if Mode = Super_Move then
5596 Son.all.Tree.Permission := No_Access;
5598 Son.all.Tree.Permission := Write_Only;
5601 -- We change the current node from Entire_Object
5602 -- to Array_Component with same permission and the
5603 -- previously defined son.
5605 C.all.Tree := (Kind => Array_Component,
5606 Is_Node_Deep => Is_Node_Deep (C),
5607 Permission => Permission (C),
5610 return Get_Elem (C);
5613 raise Program_Error;
5617 -- We set the permission tree of its prefix, and then we extract
5618 -- from the returned pointer the subtree and assign an adequate
5619 -- permission to it, if unfolded. If folded, we unroll the tree
5622 when N_Explicit_Dereference =>
5624 C : constant Perm_Tree_Access :=
5625 Set_Perm_Prefixes_Move (Prefix (N), Move);
5629 -- We went through a function call: do nothing
5634 -- The permission of the returned node should be only
5635 -- W (because the recursive call sets <= Write_Only)
5636 -- No is NOT POSSIBLE here
5638 pragma Assert (Permission (C) = Write_Only);
5640 pragma Assert (Kind (C) = Entire_Object
5641 or else Kind (C) = Reference);
5643 if Kind (C) = Reference then
5644 -- The tree is unfolded. We just modify the permission and
5645 -- return the elem subtree.
5647 if Get_All (C) = null then
5649 raise Program_Error;
5652 -- The Get_All can have permissions :
5653 -- RW : first move in this path
5654 -- W : Already other moves in this path
5655 -- No : Already other moves with 'Access
5657 pragma Assert
(Permission
(Get_All
(C
)) /= Read_Only
);
5659 if Mode
= Super_Move
then
5660 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= No_Access
;
5662 Get_All
(C
).all.Tree
.Permission
:=
5663 Glb
(Write_Only
, Permission
(Get_All
(C
)));
5666 elsif Kind
(C
) = Entire_Object
then
5668 -- Expand the tree. Replace the node with Reference.
5670 -- We are in Move or Super_Move mode, hence we can assume
5671 -- that the Children_permission is RW.
5673 pragma Assert
(Children_Permission
(C
) = Read_Write
);
5675 Son
: Perm_Tree_Access
;
5678 Son
:= new Perm_Tree_Wrapper
'
5680 (Kind => Entire_Object,
5681 Is_Node_Deep => Is_Deep (Etype (N)),
5682 Permission => Read_Write,
5683 Children_Permission => Read_Write));
5685 if Mode = Super_Move then
5686 Son.all.Tree.Permission := No_Access;
5688 Son.all.Tree.Permission := Write_Only;
5691 -- We change the current node from Entire_Object to
5692 -- Reference with Write_Only and the previous son.
5694 pragma Assert (Is_Node_Deep (C));
5696 C.all.Tree := (Kind => Reference,
5697 Is_Node_Deep => Is_Node_Deep (C),
5698 Permission => Write_Only,
5699 -- Write_only is equal to C.Permission
5705 raise Program_Error;
5709 when N_Function_Call =>
5713 raise Program_Error;
5716 end Set_Perm_Prefixes_Move;
5718 -------------------------------
5719 -- Set_Perm_Prefixes_Observe --
5720 -------------------------------
5722 function Set_Perm_Prefixes_Observe
5724 return Perm_Tree_Access
5727 pragma Assert (Current_Checking_Mode = Observe);
5730 -- Base identifier. Set permission to R.
5734 | N_Defining_Identifier
5738 C : Perm_Tree_Access;
5741 if Nkind (N) = N_Defining_Identifier then
5747 C := Get (Current_Perm_Env, Unique_Entity (P));
5748 -- Setting the initialization map to True, so that this
5749 -- variable cannot be ignored anymore when looking at end
5750 -- of elaboration of package.
5752 Set (Current_Initialization_Map, Unique_Entity (P), True);
5755 -- No null possible here, there are no parents for the path.
5756 -- This means we are using a global variable without adding
5757 -- it in environment with a global aspect.
5759 Illegal_Global_Usage (N);
5762 C.all.Tree.Permission := Glb (Read_Only, Permission (C));
5767 when N_Type_Conversion
5768 | N_Unchecked_Type_Conversion
5769 | N_Qualified_Expression
5771 return Set_Perm_Prefixes_Observe (Expression (N));
5773 when N_Parameter_Specification =>
5774 raise Program_Error;
5776 -- We set the permission tree of its prefix, and then we extract
5777 -- from the returned pointer our subtree and assign an adequate
5778 -- permission to it, if unfolded. If folded, we unroll the tree
5781 when N_Selected_Component =>
5783 C : constant Perm_Tree_Access :=
5784 Set_Perm_Prefixes_Observe (Prefix (N));
5788 -- We went through a function call, do nothing
5793 pragma Assert (Kind (C) = Entire_Object
5794 or else Kind (C) = Record_Component);
5796 if Kind (C) = Record_Component then
5797 -- The tree is unfolded. We just modify the permission and
5798 -- return the record subtree. We put the permission to the
5799 -- glb of read_only and its current permission, to consider
5800 -- the case of observing x.y while x.z has been moved. Then
5801 -- x should be No_Access.
5804 Selected_Component : constant Entity_Id :=
5805 Entity (Selector_Name (N));
5807 Selected_C : Perm_Tree_Access :=
5809 (Component (C), Selected_Component);
5812 if Selected_C = null then
5813 Selected_C := Other_Components (C);
5816 pragma Assert (Selected_C /= null);
5818 Selected_C.all.Tree.Permission :=
5819 Glb (Read_Only, Permission (Selected_C));
5823 elsif Kind (C) = Entire_Object then
5825 -- Expand the tree. Replace the node with
5826 -- Record_Component.
5830 -- Create an empty hash table
5832 Hashtbl : Perm_Tree_Maps.Instance;
5834 -- We create the unrolled nodes, that will all have RW
5835 -- permission given that we are in move mode. We will
5836 -- then set the right node to W.
5838 Son : Perm_Tree_Access;
5840 Child_Perm : constant Perm_Kind :=
5841 Children_Permission (C);
5844 -- We change the current node from Entire_Object to
5845 -- Record_Component with same permission and an empty
5846 -- hash table as component list.
5849 (Kind => Record_Component,
5850 Is_Node_Deep => Is_Node_Deep (C),
5851 Permission => Permission (C),
5852 Component => Hashtbl,
5854 new Perm_Tree_Wrapper'
5856 (Kind
=> Entire_Object
,
5857 Is_Node_Deep
=> True,
5858 Permission
=> Child_Perm
,
5859 Children_Permission
=> Child_Perm
)
5862 -- We fill the hash table with all sons of the record,
5863 -- with basic Entire_Objects nodes.
5864 Elem
:= First_Component_Or_Discriminant
5865 (Etype
(Prefix
(N
)));
5867 while Present
(Elem
) loop
5868 Son
:= new Perm_Tree_Wrapper
'
5870 (Kind => Entire_Object,
5871 Is_Node_Deep => Is_Deep (Etype (Elem)),
5872 Permission => Child_Perm,
5873 Children_Permission => Child_Perm));
5876 (C.all.Tree.Component, Elem, Son);
5878 Next_Component_Or_Discriminant (Elem);
5881 -- Now we set the right field to Read_Only. and then we
5882 -- return the tree to the sons, so that the recursion can
5886 Selected_Component : constant Entity_Id :=
5887 Entity (Selector_Name (N));
5889 Selected_C : Perm_Tree_Access :=
5891 (Component (C), Selected_Component);
5894 if Selected_C = null then
5895 Selected_C := Other_Components (C);
5898 pragma Assert (Selected_C /= null);
5900 Selected_C.all.Tree.Permission :=
5901 Glb (Read_Only, Child_Perm);
5907 raise Program_Error;
5911 -- We set the permission tree of its prefix, and then we extract from
5912 -- the returned pointer the subtree and assign an adequate permission
5913 -- to it, if unfolded. If folded, we unroll the tree at one step.
5915 when N_Indexed_Component
5919 C : constant Perm_Tree_Access :=
5920 Set_Perm_Prefixes_Observe (Prefix (N));
5924 -- We went through a function call, do nothing
5929 pragma Assert (Kind (C) = Entire_Object
5930 or else Kind (C) = Array_Component);
5932 if Kind (C) = Array_Component then
5933 -- The tree is unfolded. We just modify the permission and
5934 -- return the elem subtree.
5936 pragma Assert (Get_Elem (C) /= null);
5938 C.all.Tree.Get_Elem.all.Tree.Permission :=
5939 Glb (Read_Only, Permission (Get_Elem (C)));
5941 return Get_Elem (C);
5942 elsif Kind (C) = Entire_Object then
5944 -- Expand the tree. Replace node with Array_Component.
5946 Son : Perm_Tree_Access;
5948 Child_Perm : constant Perm_Kind :=
5949 Glb (Read_Only, Children_Permission (C));
5952 Son := new Perm_Tree_Wrapper'
5954 (Kind
=> Entire_Object
,
5955 Is_Node_Deep
=> Is_Node_Deep
(C
),
5956 Permission
=> Child_Perm
,
5957 Children_Permission
=> Child_Perm
));
5959 -- We change the current node from Entire_Object
5960 -- to Array_Component with same permission and the
5961 -- previously defined son.
5963 C
.all.Tree
:= (Kind
=> Array_Component
,
5964 Is_Node_Deep
=> Is_Node_Deep
(C
),
5965 Permission
=> Child_Perm
,
5968 return Get_Elem
(C
);
5972 raise Program_Error
;
5976 -- We set the permission tree of its prefix, and then we extract from
5977 -- the returned pointer the subtree and assign an adequate permission
5978 -- to it, if unfolded. If folded, we unroll the tree at one step.
5980 when N_Explicit_Dereference
=>
5982 C
: constant Perm_Tree_Access
:=
5983 Set_Perm_Prefixes_Observe
(Prefix
(N
));
5987 -- We went through a function call, do nothing
5992 pragma Assert
(Kind
(C
) = Entire_Object
5993 or else Kind
(C
) = Reference
);
5995 if Kind
(C
) = Reference
then
5996 -- The tree is unfolded. We just modify the permission and
5997 -- return the elem subtree.
5999 pragma Assert
(Get_All
(C
) /= null);
6001 C
.all.Tree
.Get_All
.all.Tree
.Permission
:=
6002 Glb
(Read_Only
, Permission
(Get_All
(C
)));
6005 elsif Kind
(C
) = Entire_Object
then
6007 -- Expand the tree. Replace the node with Reference.
6009 Son
: Perm_Tree_Access
;
6011 Child_Perm
: constant Perm_Kind
:=
6012 Glb
(Read_Only
, Children_Permission
(C
));
6015 Son
:= new Perm_Tree_Wrapper
'
6017 (Kind => Entire_Object,
6018 Is_Node_Deep => Is_Deep (Etype (N)),
6019 Permission => Child_Perm,
6020 Children_Permission => Child_Perm));
6022 -- We change the current node from Entire_Object to
6023 -- Reference with Write_Only and the previous son.
6025 pragma Assert (Is_Node_Deep (C));
6027 C.all.Tree := (Kind => Reference,
6028 Is_Node_Deep => Is_Node_Deep (C),
6029 Permission => Child_Perm,
6035 raise Program_Error;
6039 when N_Function_Call =>
6043 raise Program_Error;
6046 end Set_Perm_Prefixes_Observe;
6052 procedure Setup_Globals (Subp : Entity_Id) is
6054 procedure Setup_Globals_From_List
6055 (First_Item : Node_Id;
6056 Kind : Formal_Kind);
6057 -- Set up global items from the list starting at Item
6059 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
6060 -- Set up global items for the mode Global_Mode
6062 -----------------------------
6063 -- Setup_Globals_From_List --
6064 -----------------------------
6066 procedure Setup_Globals_From_List
6067 (First_Item : Node_Id;
6070 Item : Node_Id := First_Item;
6074 while Present (Item) loop
6077 -- Ignore abstract states, which play no role in pointer aliasing
6079 if Ekind (E) = E_Abstract_State then
6082 Setup_Parameter_Or_Global (E, Kind);
6086 end Setup_Globals_From_List;
6088 ---------------------------
6089 -- Setup_Globals_Of_Mode --
6090 ---------------------------
6092 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
6097 when Name_Input | Name_Proof_In =>
6098 Kind := E_In_Parameter;
6100 Kind := E_Out_Parameter;
6102 Kind := E_In_Out_Parameter;
6104 raise Program_Error;
6107 -- Set up both global items from Global and Refined_Global pragmas
6109 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
6110 Setup_Globals_From_List
6111 (First_Global (Subp, Global_Mode, Refined => True), Kind);
6112 end Setup_Globals_Of_Mode;
6114 -- Start of processing for Setup_Globals
6117 Setup_Globals_Of_Mode (Name_Proof_In);
6118 Setup_Globals_Of_Mode (Name_Input);
6119 Setup_Globals_Of_Mode (Name_Output);
6120 Setup_Globals_Of_Mode (Name_In_Out);
6123 -------------------------------
6124 -- Setup_Parameter_Or_Global --
6125 -------------------------------
6127 procedure Setup_Parameter_Or_Global
6131 Elem : Perm_Tree_Access;
6134 Elem := new Perm_Tree_Wrapper'
6136 (Kind
=> Entire_Object
,
6137 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
6138 Permission
=> Read_Write
,
6139 Children_Permission
=> Read_Write
));
6142 when E_In_Parameter
=>
6144 -- Borrowed IN: RW for everybody
6146 if Is_Borrowed_In
(Id
) then
6147 Elem
.all.Tree
.Permission
:= Read_Write
;
6148 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6150 -- Observed IN: R for everybody
6153 Elem
.all.Tree
.Permission
:= Read_Only
;
6154 Elem
.all.Tree
.Children_Permission
:= Read_Only
;
6157 -- OUT: borrow, but callee has W only
6159 when E_Out_Parameter
=>
6160 Elem
.all.Tree
.Permission
:= Write_Only
;
6161 Elem
.all.Tree
.Children_Permission
:= Write_Only
;
6163 -- IN OUT: borrow and callee has RW
6165 when E_In_Out_Parameter
=>
6166 Elem
.all.Tree
.Permission
:= Read_Write
;
6167 Elem
.all.Tree
.Children_Permission
:= Read_Write
;
6170 Set
(Current_Perm_Env
, Id
, Elem
);
6171 end Setup_Parameter_Or_Global
;
6173 ----------------------
6174 -- Setup_Parameters --
6175 ----------------------
6177 procedure Setup_Parameters
(Subp
: Entity_Id
) is
6181 Formal
:= First_Formal
(Subp
);
6182 while Present
(Formal
) loop
6183 Setup_Parameter_Or_Global
(Formal
, Ekind
(Formal
));
6184 Next_Formal
(Formal
);
6186 end Setup_Parameters
;