1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017-2018, 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
(Key
: Entity_Id
)
56 return Elaboration_Context_Index
;
57 -- Function to hash any node of the AST
59 type Perm_Kind
is (Borrowed
, Observed
, Unrestricted
, Moved
);
60 -- Permission type associated with paths. The Moved permission is
61 -- equivalent to the Unrestricted one (same permissions). The Moved is
62 -- however used to mark the RHS after a move (which still unrestricted).
63 -- This way, we may generate warnings when manipulating the RHS
64 -- afterwads since it is set to Null after the assignment.
66 type Perm_Tree_Wrapper
;
68 type Perm_Tree_Access
is access Perm_Tree_Wrapper
;
69 -- A tree of permissions is defined, where the root is a whole object
70 -- and tree branches follow access paths in memory. As Perm_Tree is a
71 -- discriminated record, a wrapper type is used for the access type
72 -- designating a subtree, to make it unconstrained so that it can be
75 -- Nodes in the permission tree are of different kinds
78 (Entire_Object
, -- Scalar object, or folded object of any type
79 Reference
, -- Unfolded object of access type
80 Array_Component
, -- Unfolded object of array type
81 Record_Component
-- Unfolded object of record type
84 package Perm_Tree_Maps
is new Simple_HTable
85 (Header_Num
=> Elaboration_Context_Index
,
87 Element
=> Perm_Tree_Access
,
89 Hash
=> Elaboration_Context_Hash
,
91 -- The instantation of a hash table, with keys being nodes and values
92 -- being pointers to trees. This is used to reference easily all
93 -- extensions of a Record_Component node (that can have name x, y, ...).
95 -- The definition of permission trees. This is a tree, which has a
96 -- permission at each node, and depending on the type of the node,
97 -- can have zero, one, or more children pointed to by an access to tree.
99 type Perm_Tree
(Kind
: Path_Kind
:= Entire_Object
) is record
100 Permission
: Perm_Kind
;
101 -- Permission at this level in the path
103 Is_Node_Deep
: Boolean;
104 -- Whether this node is of a deep type, to be used when moving the
108 -- An entire object is either a leaf (an object which cannot be
109 -- extended further in a path) or a subtree in folded form (which
110 -- could later be unfolded further in another kind of node). The
111 -- field Children_Permission specifies a permission for every
112 -- extension of that node if that permission is different from
113 -- the node's permission.
115 when Entire_Object
=>
116 Children_Permission
: Perm_Kind
;
118 -- Unfolded path of access type. The permission of the object
119 -- pointed to is given in Get_All.
122 Get_All
: Perm_Tree_Access
;
124 -- Unfolded path of array type. The permission of the elements is
125 -- given in Get_Elem.
127 when Array_Component
=>
128 Get_Elem
: Perm_Tree_Access
;
130 -- Unfolded path of record type. The permission of the regular
131 -- components is given in Component. The permission of unknown
132 -- components (for objects of tagged type) is given in
135 when Record_Component
=>
136 Component
: Perm_Tree_Maps
.Instance
;
137 Other_Components
: Perm_Tree_Access
;
141 type Perm_Tree_Wrapper
is record
144 -- We use this wrapper in order to have unconstrained discriminants
146 type Perm_Env
is new Perm_Tree_Maps
.Instance
;
147 -- The definition of a permission environment for the analysis. This
148 -- is just a hash table of permission trees, each of them rooted with
149 -- an Identifier/Expanded_Name.
151 type Perm_Env_Access
is access Perm_Env
;
152 -- Access to permission environments
154 package Env_Maps
is new Simple_HTable
155 (Header_Num
=> Elaboration_Context_Index
,
157 Element
=> Perm_Env_Access
,
159 Hash
=> Elaboration_Context_Hash
,
161 -- The instantiation of a hash table whose elements are permission
162 -- environments. This hash table is used to save the environments at
163 -- the entry of each loop, with the key being the loop label.
165 type Env_Backups
is new Env_Maps
.Instance
;
166 -- The type defining the hash table saving the environments at the entry
169 package Boolean_Variables_Maps
is new Simple_HTable
170 (Header_Num
=> Elaboration_Context_Index
,
174 Hash
=> Elaboration_Context_Hash
,
176 -- These maps allow tracking the variables that have been declared but
177 -- never used anywhere in the source code. Especially, we do not raise
178 -- an error if the variable stays write-only and is declared at package
179 -- level, because there is no risk that the variable has been moved,
180 -- because it has never been used.
182 type Initialization_Map
is new Boolean_Variables_Maps
.Instance
;
188 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
189 -- that's only for the top access, as otherwise this reverses the order
190 -- in accesses visually.
192 function Children_Permission
(T
: Perm_Tree_Access
) return Perm_Kind
;
193 function Component
(T
: Perm_Tree_Access
) return Perm_Tree_Maps
.Instance
;
194 function Get_All
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
195 function Get_Elem
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
196 function Is_Node_Deep
(T
: Perm_Tree_Access
) return Boolean;
197 function Kind
(T
: Perm_Tree_Access
) return Path_Kind
;
198 function Other_Components
(T
: Perm_Tree_Access
) return Perm_Tree_Access
;
199 function Permission
(T
: Perm_Tree_Access
) return Perm_Kind
;
201 -----------------------
202 -- Memory Management --
203 -----------------------
207 To
: in out Perm_Env
);
208 -- Procedure to copy a permission environment
210 procedure Copy_Init_Map
211 (From
: Initialization_Map
;
212 To
: in out Initialization_Map
);
213 -- Procedure to copy an initialization map
216 (From
: Perm_Tree_Access
;
217 To
: Perm_Tree_Access
);
218 -- Procedure to copy a permission tree
221 (PE
: in out Perm_Env
);
222 -- Procedure to free a permission environment
224 procedure Free_Perm_Tree
225 (PT
: in out Perm_Tree_Access
);
226 -- Procedure to free a permission tree
232 procedure Perm_Mismatch
233 (Exp_Perm
, Act_Perm
: Perm_Kind
;
235 -- Issues a continuation error message about a mismatch between a
236 -- desired permission Exp_Perm and a permission obtained Act_Perm. N
237 -- is the node on which the error is reported.
241 package body Permissions
is
243 -------------------------
244 -- Children_Permission --
245 -------------------------
247 function Children_Permission
(T
: Perm_Tree_Access
) return Perm_Kind
is
249 return T
.all.Tree
.Children_Permission
;
250 end Children_Permission
;
257 (T
: Perm_Tree_Access
)
258 return Perm_Tree_Maps
.Instance
261 return T
.all.Tree
.Component
;
268 procedure Copy_Env
(From
: Perm_Env
; To
: in out Perm_Env
) is
269 Comp_From
: Perm_Tree_Access
;
270 Key_From
: Perm_Tree_Maps
.Key_Option
;
271 Son
: Perm_Tree_Access
;
275 Key_From
:= Get_First_Key
(From
);
276 while Key_From
.Present
loop
277 Comp_From
:= Get
(From
, Key_From
.K
);
278 pragma Assert
(Comp_From
/= null);
280 Son
:= new Perm_Tree_Wrapper
;
281 Copy_Tree
(Comp_From
, Son
);
283 Set
(To
, Key_From
.K
, Son
);
284 Key_From
:= Get_Next_Key
(From
);
292 procedure Copy_Init_Map
293 (From
: Initialization_Map
;
294 To
: in out Initialization_Map
)
297 Key_From
: Boolean_Variables_Maps
.Key_Option
;
301 Key_From
:= Get_First_Key
(From
);
302 while Key_From
.Present
loop
303 Comp_From
:= Get
(From
, Key_From
.K
);
304 Set
(To
, Key_From
.K
, Comp_From
);
305 Key_From
:= Get_Next_Key
(From
);
313 procedure Copy_Tree
(From
: Perm_Tree_Access
; To
: Perm_Tree_Access
) is
317 when Entire_Object
=>
321 To
.all.Tree
.Get_All
:= new Perm_Tree_Wrapper
;
322 Copy_Tree
(Get_All
(From
), Get_All
(To
));
324 when Array_Component
=>
325 To
.all.Tree
.Get_Elem
:= new Perm_Tree_Wrapper
;
326 Copy_Tree
(Get_Elem
(From
), Get_Elem
(To
));
328 when Record_Component
=>
330 Comp_From
: Perm_Tree_Access
;
331 Key_From
: Perm_Tree_Maps
.Key_Option
;
332 Son
: Perm_Tree_Access
;
333 Hash_Table
: Perm_Tree_Maps
.Instance
;
335 -- We put a new hash table, so that it gets dealiased from the
336 -- Component (From) hash table.
337 To
.all.Tree
.Component
:= Hash_Table
;
338 To
.all.Tree
.Other_Components
:=
339 new Perm_Tree_Wrapper
'(Other_Components (From).all);
340 Copy_Tree (Other_Components (From), Other_Components (To));
341 Key_From := Perm_Tree_Maps.Get_First_Key
344 while Key_From.Present loop
345 Comp_From := Perm_Tree_Maps.Get
346 (Component (From), Key_From.K);
347 pragma Assert (Comp_From /= null);
348 Son := new Perm_Tree_Wrapper;
349 Copy_Tree (Comp_From, Son);
351 (To.all.Tree.Component, Key_From.K, Son);
352 Key_From := Perm_Tree_Maps.Get_Next_Key
360 ------------------------------
361 -- Elaboration_Context_Hash --
362 ------------------------------
364 function Elaboration_Context_Hash
365 (Key : Entity_Id) return Elaboration_Context_Index
368 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
369 end Elaboration_Context_Hash;
375 procedure Free_Env (PE : in out Perm_Env) is
376 CompO : Perm_Tree_Access;
378 CompO := Get_First (PE);
379 while CompO /= null loop
380 Free_Perm_Tree (CompO);
381 CompO := Get_Next (PE);
389 procedure Free_Perm_Tree (PT : in out Perm_Tree_Access) is
390 procedure Free_Perm_Tree_Dealloc is
391 new Ada.Unchecked_Deallocation
392 (Perm_Tree_Wrapper, Perm_Tree_Access);
393 -- The deallocator for permission_trees
397 when Entire_Object =>
398 Free_Perm_Tree_Dealloc (PT);
401 Free_Perm_Tree (PT.all.Tree.Get_All);
402 Free_Perm_Tree_Dealloc (PT);
404 when Array_Component =>
405 Free_Perm_Tree (PT.all.Tree.Get_Elem);
407 when Record_Component =>
409 Comp : Perm_Tree_Access;
412 Free_Perm_Tree (PT.all.Tree.Other_Components);
413 Comp := Perm_Tree_Maps.Get_First (Component (PT));
414 while Comp /= null loop
416 -- Free every Component subtree
418 Free_Perm_Tree (Comp);
419 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
422 Free_Perm_Tree_Dealloc (PT);
430 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
432 return T.all.Tree.Get_All;
439 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
441 return T.all.Tree.Get_Elem;
448 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
450 return T.all.Tree.Is_Node_Deep;
457 function Kind (T : Perm_Tree_Access) return Path_Kind is
459 return T.all.Tree.Kind;
462 ----------------------
463 -- Other_Components --
464 ----------------------
466 function Other_Components
467 (T : Perm_Tree_Access)
468 return Perm_Tree_Access
471 return T.all.Tree.Other_Components;
472 end Other_Components;
478 function Permission (T : Perm_Tree_Access) return Perm_Kind is
480 return T.all.Tree.Permission;
487 procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is
489 Error_Msg_N ("\expected state `"
490 & Perm_Kind'Image (Exp_Perm) & "` at least, got `"
491 & Perm_Kind'Image (Act_Perm) & "`", N);
498 --------------------------------------
499 -- Analysis modes for AST traversal --
500 --------------------------------------
502 -- The different modes for analysis. This allows to checking whether a path
503 -- found in the code should be moved, borrowed, or observed.
505 type Checking_Mode is
508 -- Default mode. Checks that paths have Read_Perm permission.
511 -- Regular moving semantics. Checks that paths have
512 -- Unrestricted permission. After moving a path, its permission is set
513 -- to Unrestricted and the permission of its extensions is set
517 -- Used for the target of an assignment, or an actual parameter with
518 -- mode OUT. Checks that paths have Unrestricted permission. After
519 -- assigning to a path, its permission is set to Unrestricted.
522 -- Used for the source of an assignement when initializes a stand alone
523 -- object of anonymous type, constant, or IN parameter and also OUT
524 -- or IN OUT composite object.
525 -- In the borrowed state, the access object is completely "dead".
528 -- Used for actual IN parameters of a scalar type. Checks that paths
529 -- have Read_Perm permission. After checking a path, its permission
530 -- is set to Observed.
532 -- Also used for formal IN parameters
536 type Result_Kind is (Folded, Unfolded, Function_Call);
537 -- The type declaration to discriminate in the Perm_Or_Tree type
539 -- The result type of the function Get_Perm_Or_Tree. This returns either a
540 -- tree when it found the appropriate tree, or a permission when the search
541 -- finds a leaf and the subtree we are looking for is folded. In the last
542 -- case, we return instead the Children_Permission field of the leaf.
544 type Perm_Or_Tree (R : Result_Kind) is record
546 when Folded => Found_Permission : Perm_Kind;
547 when Unfolded => Tree_Access : Perm_Tree_Access;
548 when Function_Call => null;
552 -----------------------
553 -- Local subprograms --
554 -----------------------
556 -- Checking proceduress for safe pointer usage. These procedures traverse
557 -- the AST, check nodes for correct permissions according to SPARK RM
558 -- 6.4.2, and update permissions depending on the node kind.
560 procedure Check_Call_Statement (Call : Node_Id);
562 procedure Check_Callable_Body (Body_N : Node_Id);
563 -- We are not in End_Of_Callee mode, hence we will save the environment
564 -- and start from a new one. We will add in the environment all formal
565 -- parameters as well as global used during the subprogram, with the
566 -- appropriate permissions (unrestricted for borrowed and moved, observed
567 -- for observed names).
569 procedure Check_Declaration (Decl : Node_Id);
571 procedure Check_Expression (Expr : Node_Id);
573 procedure Check_Globals (N : Node_Id);
574 -- This procedure takes a global pragma and checks it
576 procedure Check_List (L : List_Id);
577 -- Calls Check_Node on each element of the list
579 procedure Check_Loop_Statement (Loop_N : Node_Id);
581 procedure Check_Node (N : Node_Id);
582 -- Main traversal procedure to check safe pointer usage. This procedure is
583 -- mutually recursive with the specialized procedures that follow.
585 procedure Check_Package_Body (Pack : Node_Id);
587 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id);
588 -- This procedure takes a formal and an actual parameter and checks the
589 -- permission of every in-mode parameter. This includes Observing and
592 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
593 -- This procedure takes a formal and an actual parameter and checks the
594 -- state of every out-mode and in out-mode parameter. This includes
595 -- Moving and Borrowing.
597 procedure Check_Statement (Stmt : Node_Id);
599 function Get_Perm (N : Node_Id) return Perm_Kind;
600 -- The function that takes a name as input and returns a permission
603 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
604 -- This function gets a Node_Id and looks recursively to find the
605 -- appropriate subtree for that Node_Id. If the tree is folded on
606 -- that node, then it returns the permission given at the right level.
608 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
609 -- This function gets a Node_Id and looks recursively to find the
610 -- appropriate subtree for that Node_Id. If the tree is folded, then
611 -- it unrolls the tree up to the appropriate level.
613 procedure Hp (P : Perm_Env);
614 -- A procedure that outputs the hash table. This function is used only in
615 -- the debugger to look into a hash table.
616 pragma Unreferenced (Hp);
618 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
619 pragma No_Return (Illegal_Global_Usage);
620 -- A procedure that is called when deep globals or aliased globals are used
621 -- without any global aspect.
623 function Is_Deep (E : Entity_Id) return Boolean;
624 -- A function that can tell if a type is deep or not. Returns true if the
625 -- type passed as argument is deep.
630 Found_Perm : Perm_Kind);
631 -- A procedure that is called when the permissions found contradict the
632 -- rules established by the RM. This function is called with the node, its
633 -- entity and the permission that was expected, and adds an error message
634 -- with the appropriate values.
636 procedure Perm_Error_Subprogram_End
640 Found_Perm : Perm_Kind);
641 -- A procedure that is called when the permissions found contradict the
642 -- rules established by the RM at the end of subprograms. This function
643 -- is called with the node, its entity, the node of the returning function
644 -- and the permission that was expected, and adds an error message with the
645 -- appropriate values.
647 procedure Process_Path (N : Node_Id);
649 procedure Return_Declarations (L : List_Id);
650 -- Check correct permissions on every declared object at the end of a
651 -- callee. Used at the end of the body of a callable entity. Checks that
652 -- paths of all borrowed formal parameters and global have Unrestricted
655 procedure Return_Globals (Subp : Entity_Id);
656 -- Takes a subprogram as input, and checks that all borrowed global items
657 -- of the subprogram indeed have RW permission at the end of the subprogram
660 procedure Return_The_Global
664 -- Auxiliary procedure to Return_Globals
665 -- There is no need to return parameters because they will be reassigned
666 -- their state once the subprogram returns. Local variables that have
667 -- borrowed, observed, or moved an actual parameter go out of the scope.
669 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
670 -- This procedure takes an access to a permission tree and modifies the
671 -- tree so that any strict extensions of the given tree become of the
672 -- access specified by parameter P.
674 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
675 -- This function modifies the permissions of a given node_id in the
676 -- permission environment as well as in all the prefixes of the path,
677 -- given that the path is borrowed with mode out.
679 function Set_Perm_Prefixes
681 New_Perm : Perm_Kind)
682 return Perm_Tree_Access;
683 -- This function sets the permissions of a given node_id in the
684 -- permission environment as well as in all the prefixes of the path
685 -- to the one given in parameter (P).
687 procedure Setup_Globals (Subp : Entity_Id);
688 -- Takes a subprogram as input, and sets up the environment by adding
689 -- global items with appropriate permissions.
691 procedure Setup_Parameter_Or_Global
694 Global_Var : Boolean);
695 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
697 procedure Setup_Parameters (Subp : Entity_Id);
698 -- Takes a subprogram as input, and sets up the environment by adding
699 -- formal parameters with appropriate permissions.
701 function Has_Ownership_Aspect_True
705 -- Takes a node as an input, and finds out whether it has ownership aspect
706 -- True or False. This function is recursive whenever the node has a
707 -- composite type. Access-to-objects have ownership aspect False if they
708 -- have a general access type.
710 ----------------------
711 -- Global Variables --
712 ----------------------
714 Current_Perm_Env : Perm_Env;
715 -- The permission environment that is used for the analysis. This
716 -- environment can be saved, modified, reinitialized, but should be the
717 -- only one valid from which to extract the permissions of the paths in
718 -- scope. The analysis ensures at each point that this variables contains
719 -- a valid permission environment with all bindings in scope.
721 Current_Checking_Mode : Checking_Mode := Read;
722 -- The current analysis mode. This global variable indicates at each point
723 -- of the analysis whether the node being analyzed is moved, borrowed,
724 -- assigned, read, ... The full list of possible values can be found in
725 -- the declaration of type Checking_Mode.
727 Current_Loops_Envs : Env_Backups;
728 -- This variable contains saves of permission environments at each loop the
729 -- analysis entered. Each saved environment can be reached with the label
732 Current_Loops_Accumulators : Env_Backups;
733 -- This variable contains the environments used as accumulators for loops,
734 -- that consist of the merge of all environments at each exit point of
735 -- the loop (which can also be the entry point of the loop in the case of
736 -- non-infinite loops), each of them reachable from the label of the loop.
737 -- We require that the environment stored in the accumulator be less
738 -- restrictive than the saved environment at the beginning of the loop, and
739 -- the permission environment after the loop is equal to the accumulator.
741 Current_Initialization_Map : Initialization_Map;
742 -- This variable contains a map that binds each variable of the analyzed
743 -- source code to a boolean that becomes true whenever the variable is used
744 -- after declaration. Hence we can exclude from analysis variables that
745 -- are just declared and never accessed, typically at package declaration.
747 --------------------------
748 -- Check_Call_Statement --
749 --------------------------
751 procedure Check_Call_Statement (Call : Node_Id) is
752 Saved_Env : Perm_Env;
754 procedure Iterate_Call_In is new
755 Iterate_Call_Parameters (Check_Param_In);
756 procedure Iterate_Call_Out is new
757 Iterate_Call_Parameters (Check_Param_Out);
760 -- Save environment, so that the modifications done by analyzing the
761 -- parameters are not kept at the end of the call.
763 Copy_Env (Current_Perm_Env, Saved_Env);
765 -- We first check the globals then parameters to handle the
766 -- No_Parameter_Aliasing Restriction. An out or in-out global is
767 -- considered as borrowing while a parameter with the same mode is
768 -- a move. This order disallow passing a part of a variable to a
769 -- subprogram if it is referenced as a global by the callable (when
771 -- For paremeters, we fisrt check in parameters and then the out ones.
772 -- This is to avoid Observing or Borrowing objects that are already
773 -- moved. This order is not mandatory but allows to catch runtime
774 -- errors like null pointer dereferencement at the analysis time.
776 Current_Checking_Mode := Read;
777 Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
778 Iterate_Call_In (Call);
779 Iterate_Call_Out (Call);
781 -- Restore environment, because after borrowing/observing actual
782 -- parameters, they get their permission reverted to the ones before
785 Free_Env (Current_Perm_Env);
786 Copy_Env (Saved_Env, Current_Perm_Env);
787 Free_Env (Saved_Env);
788 end Check_Call_Statement;
790 -------------------------
791 -- Check_Callable_Body --
792 -------------------------
794 procedure Check_Callable_Body (Body_N : Node_Id) is
796 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
797 Saved_Env : Perm_Env;
798 Saved_Init_Map : Initialization_Map;
800 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
801 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
804 -- Check if SPARK pragma is not set to Off
806 if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
807 if Get_SPARK_Mode_From_Annotation
808 (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
816 -- Save environment and put a new one in place
818 Copy_Env (Current_Perm_Env, Saved_Env);
820 -- Save initialization map
822 Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
823 Current_Checking_Mode := Read;
824 Current_Perm_Env := New_Env;
826 -- Add formals and globals to the environment with adequate permissions
828 if Is_Subprogram_Or_Entry (Spec_Id) then
829 Setup_Parameters (Spec_Id);
830 Setup_Globals (Spec_Id);
833 -- Analyze the body of the function
835 Check_List (Declarations (Body_N));
836 Check_Node (Handled_Statement_Sequence (Body_N));
838 -- Check the read-write permissions of borrowed parameters/globals
840 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
841 and then not No_Return (Spec_Id)
843 Return_Globals (Spec_Id);
846 -- Free the environments
848 Free_Env (Current_Perm_Env);
849 Copy_Env (Saved_Env, Current_Perm_Env);
850 Free_Env (Saved_Env);
852 -- Restore initialization map
854 Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
855 Reset (Saved_Init_Map);
857 -- The assignment of all out parameters will be done by caller
859 Current_Checking_Mode := Mode_Before;
860 end Check_Callable_Body;
862 -----------------------
863 -- Check_Declaration --
864 -----------------------
866 procedure Check_Declaration (Decl : Node_Id) is
868 Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
869 Target_Typ : Node_Id renames Etype (Target_Ent);
870 Check : Boolean := True;
872 case N_Declaration'(Nkind
(Decl
)) is
873 when N_Full_Type_Declaration
=>
874 if not Has_Ownership_Aspect_True
(Target_Ent
, "type declaration")
879 -- ??? What about component declarations with defaults.
881 when N_Object_Declaration
=>
882 if (Is_Access_Type
(Target_Typ
)
883 or else Is_Deep
(Target_Typ
))
884 and then not Has_Ownership_Aspect_True
885 (Target_Ent
, "Object declaration ")
890 if Is_Anonymous_Access_Type
(Target_Typ
)
891 and then not Present
(Expression
(Decl
))
894 -- ??? Check the case of default value (AI)
895 -- ??? How an anonymous access type can be with default exp?
897 Error_Msg_NE
("? object declaration & has OAF (Anonymous "
898 & "access-to-object with no initialization)",
901 -- If it it an initialization
903 elsif Present
(Expression
(Decl
)) and Check
then
905 -- Find out the operation to be done on the right-hand side
907 -- Initializing object, access type
909 if Is_Access_Type
(Target_Typ
) then
911 -- Initializing object, constant access type
913 if Is_Constant_Object
(Target_Ent
) then
915 -- Initializing object, constant access to variable type
917 if not Is_Access_Constant
(Target_Typ
) then
918 Current_Checking_Mode
:= Borrow
;
920 -- Initializing object, constant access to constant type
922 -- Initializing object,
923 -- constant access to constant anonymous type.
925 elsif Is_Anonymous_Access_Type
(Target_Typ
) then
927 -- This is an object declaration so the target
928 -- of the assignement is a stand-alone object.
930 Current_Checking_Mode
:= Observe
;
932 -- Initializing object, constant access to constant
936 -- If named then it is a general access type
937 -- Hence, Has_Ownership_Aspec_True is False.
942 -- Initializing object, variable access type
945 -- Initializing object, variable access to variable type
947 if not Is_Access_Constant
(Target_Typ
) then
949 -- Initializing object, variable named access to
952 if not Is_Anonymous_Access_Type
(Target_Typ
) then
953 Current_Checking_Mode
:= Move
;
955 -- Initializing object, variable anonymous access to
959 -- This is an object declaration so the target
960 -- object of the assignement is a stand-alone
963 Current_Checking_Mode
:= Borrow
;
966 -- Initializing object, variable access to constant type
969 -- Initializing object,
970 -- variable named access to constant type.
972 if not Is_Anonymous_Access_Type
(Target_Typ
) then
973 Error_Msg_N
("assignment not allowed, Ownership "
974 & "Aspect False (Anonymous Access "
978 -- Initializing object,
979 -- variable anonymous access to constant type.
982 -- This is an object declaration so the target
983 -- of the assignement is a stand-alone object.
985 Current_Checking_Mode
:= Observe
;
990 -- Initializing object, composite (deep) type
992 elsif Is_Deep
(Target_Typ
) then
994 -- Initializing object, constant composite type
996 if Is_Constant_Object
(Target_Ent
) then
997 Current_Checking_Mode
:= Observe
;
999 -- Initializing object, variable composite type
1003 -- Initializing object, variable anonymous composite type
1005 if Nkind
(Object_Definition
(Decl
)) =
1006 N_Constrained_Array_Definition
1008 -- An N_Constrained_Array_Definition is an anonymous
1009 -- array (to be checked). Record types are always
1010 -- named and are considered in the else part.
1014 Com_Ty
: constant Node_Id
:=
1015 Component_Type
(Etype
(Target_Typ
));
1018 if Is_Access_Type
(Com_Ty
) then
1020 -- If components are of anonymous type
1022 if Is_Anonymous_Access_Type
(Com_Ty
) then
1023 if Is_Access_Constant
(Com_Ty
) then
1024 Current_Checking_Mode
:= Observe
;
1027 Current_Checking_Mode
:= Borrow
;
1031 Current_Checking_Mode
:= Move
;
1034 elsif Is_Deep
(Com_Ty
) then
1036 -- This is certainly named so it is a move
1038 Current_Checking_Mode
:= Move
;
1043 Current_Checking_Mode
:= Move
;
1047 elsif Nkind_In
(Expression
(Decl
),
1048 N_Attribute_Reference
,
1049 N_Attribute_Reference
,
1051 N_Explicit_Dereference
,
1052 N_Indexed_Component
,
1054 N_Selected_Component
,
1057 if Is_Access_Type
(Etype
(Prefix
(Expression
(Decl
))))
1058 or else Is_Deep
(Etype
(Prefix
(Expression
(Decl
))))
1060 Current_Checking_Mode
:= Observe
;
1067 Check_Node
(Expression
(Decl
));
1070 -- If lhs is not a pointer, we still give it the appropriate
1071 -- state which is useless but not harmful.
1074 Elem
: Perm_Tree_Access
;
1075 Deep
: constant Boolean := Is_Deep
(Target_Typ
);
1078 -- Note that all declared variables are set to the unrestricted
1081 -- If variables are not initialized:
1082 -- unrestricted to every declared object.
1087 -- The assignement R := S is not allowed in the new rules
1088 -- if R is not unrestricted.
1090 -- If variables are initialized:
1091 -- If it is a move, then the target is unrestricted
1092 -- If it is a borrow, then the target is unrestricted
1093 -- If it is an observe, then the target should be observed
1095 if Current_Checking_Mode
= Observe
then
1096 Elem
:= new Perm_Tree_Wrapper
'
1098 (Kind => Entire_Object,
1099 Is_Node_Deep => Deep,
1100 Permission => Observed,
1101 Children_Permission => Observed));
1103 Elem := new Perm_Tree_Wrapper'
1105 (Kind
=> Entire_Object
,
1106 Is_Node_Deep
=> Deep
,
1107 Permission
=> Unrestricted
,
1108 Children_Permission
=> Unrestricted
));
1111 -- Create new tree for defining identifier
1113 Set
(Current_Perm_Env
,
1114 Unique_Entity
(Defining_Identifier
(Decl
)),
1116 pragma Assert
(Get_First
(Current_Perm_Env
) /= null);
1119 when N_Subtype_Declaration
=>
1120 Check_Node
(Subtype_Indication
(Decl
));
1122 when N_Iterator_Specification
=>
1125 when N_Loop_Parameter_Specification
=>
1128 -- Checking should not be called directly on these nodes
1130 when N_Function_Specification
1131 | N_Entry_Declaration
1132 | N_Procedure_Specification
1133 | N_Component_Declaration
1135 raise Program_Error
;
1137 -- Ignored constructs for pointer checking
1139 when N_Formal_Object_Declaration
1140 | N_Formal_Type_Declaration
1141 | N_Incomplete_Type_Declaration
1142 | N_Private_Extension_Declaration
1143 | N_Private_Type_Declaration
1144 | N_Protected_Type_Declaration
1148 -- The following nodes are rewritten by semantic analysis
1150 when N_Expression_Function
=>
1151 raise Program_Error
;
1153 end Check_Declaration
;
1155 ----------------------
1156 -- Check_Expression --
1157 ----------------------
1159 procedure Check_Expression
(Expr
: Node_Id
) is
1160 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
1162 case N_Subexpr
'(Nkind (Expr)) is
1163 when N_Procedure_Call_Statement
1166 Check_Call_Statement (Expr);
1171 -- Check if identifier is pointing to nothing (On/Off/...)
1173 if not Present (Entity (Expr)) then
1177 -- Do not analyze things that are not of object Kind
1179 if Ekind (Entity (Expr)) not in Object_Kind then
1183 -- Consider as ident
1185 Process_Path (Expr);
1187 -- Switch to read mode and then check the readability of each operand
1190 Current_Checking_Mode := Read;
1191 Check_Node (Left_Opnd (Expr));
1192 Check_Node (Right_Opnd (Expr));
1194 -- Switch to read mode and then check the readability of each operand
1201 Current_Checking_Mode := Read;
1202 Check_Node (Right_Opnd (Expr));
1204 -- Forbid all deep expressions for Attribute ???
1206 when N_Attribute_Reference =>
1207 case Attribute_Name (Expr) is
1209 Error_Msg_N ("access attribute not allowed in SPARK", Expr);
1214 Current_Checking_Mode := Read;
1215 Check_Node (Prefix (Expr));
1218 Current_Checking_Mode := Read;
1219 Check_Node (Prefix (Expr));
1222 Check_List (Expressions (Expr));
1225 Check_Node (Prefix (Expr));
1227 when Name_SPARK_Mode =>
1231 Current_Checking_Mode := Read;
1232 Check_Node (Prefix (Expr));
1235 Check_List (Expressions (Expr));
1236 Check_Node (Prefix (Expr));
1241 Check_List (Expressions (Expr));
1242 Check_Node (Prefix (Expr));
1245 Current_Checking_Mode := Read;
1246 Check_Node (Prefix (Expr));
1248 -- Any Attribute referring to the underlying memory is ignored
1249 -- in the analysis. This means that taking the address of a
1250 -- variable makes a silent alias that is not rejected by the
1255 | Name_Component_Size
1263 -- Attributes referring to types (get values from types), hence
1264 -- no need to check either for borrows or any loans.
1270 -- Other attributes that fall out of the scope of the analysis
1277 Current_Checking_Mode := Read;
1278 Check_Node (Left_Opnd (Expr));
1279 Check_Node (Right_Opnd (Expr));
1282 Current_Checking_Mode := Read;
1283 Check_Node (Left_Opnd (Expr));
1284 Check_Node (Right_Opnd (Expr));
1286 -- Switch to read mode and then check the readability of each operand
1291 Current_Checking_Mode := Read;
1292 Check_Node (Left_Opnd (Expr));
1293 Check_Node (Right_Opnd (Expr));
1295 -- Check the arguments of the call
1297 when N_Explicit_Dereference =>
1298 Process_Path (Expr);
1300 -- Copy environment, run on each branch, and then merge
1302 when N_If_Expression =>
1304 Saved_Env : Perm_Env;
1306 -- Accumulator for the different branches
1309 Elmt : Node_Id := First (Expressions (Expr));
1312 Current_Checking_Mode := Read;
1314 Current_Checking_Mode := Mode_Before;
1318 Copy_Env (Current_Perm_Env, Saved_Env);
1320 -- Here we have the original env in saved, current with a fresh
1321 -- copy, and new aliased.
1328 -- Here the new_environment contains curr env after then block
1331 -- Restore environment before if
1332 Copy_Env (Current_Perm_Env, New_Env);
1333 Free_Env (Current_Perm_Env);
1334 Copy_Env (Saved_Env, Current_Perm_Env);
1336 -- Here new environment contains the environment after then and
1337 -- current the fresh copy of old one.
1344 Copy_Env (New_Env, Current_Perm_Env);
1346 Free_Env (Saved_Env);
1349 when N_Indexed_Component =>
1350 Process_Path (Expr);
1352 -- Analyze the expression that is getting qualified
1354 when N_Qualified_Expression =>
1355 Check_Node (Expression (Expr));
1357 when N_Quantified_Expression =>
1359 Saved_Env : Perm_Env;
1362 Copy_Env (Current_Perm_Env, Saved_Env);
1363 Current_Checking_Mode := Read;
1364 Check_Node (Iterator_Specification (Expr));
1365 Check_Node (Loop_Parameter_Specification (Expr));
1367 Check_Node (Condition (Expr));
1368 Free_Env (Current_Perm_Env);
1369 Copy_Env (Saved_Env, Current_Perm_Env);
1370 Free_Env (Saved_Env);
1372 -- Analyze the list of associations in the aggregate
1375 Check_List (Expressions (Expr));
1376 Check_List (Component_Associations (Expr));
1379 Check_Node (Expression (Expr));
1381 when N_Case_Expression =>
1383 Saved_Env : Perm_Env;
1385 -- Accumulator for the different branches
1388 Elmt : Node_Id := First (Alternatives (Expr));
1391 Current_Checking_Mode := Read;
1392 Check_Node (Expression (Expr));
1393 Current_Checking_Mode := Mode_Before;
1397 Copy_Env (Current_Perm_Env, Saved_Env);
1399 -- Here we have the original env in saved, current with a fresh
1400 -- copy, and new aliased.
1402 -- First alternative
1406 Copy_Env (Current_Perm_Env, New_Env);
1407 Free_Env (Current_Perm_Env);
1409 -- Other alternatives
1411 while Present (Elmt) loop
1413 -- Restore environment
1415 Copy_Env (Saved_Env, Current_Perm_Env);
1421 Copy_Env (Saved_Env, Current_Perm_Env);
1423 Free_Env (Saved_Env);
1425 -- Analyze the list of associates in the aggregate as well as the
1428 when N_Extension_Aggregate =>
1429 Check_Node (Ancestor_Part (Expr));
1430 Check_List (Expressions (Expr));
1433 Check_Node (Low_Bound (Expr));
1434 Check_Node (High_Bound (Expr));
1436 -- We arrived at a path. Process it.
1438 when N_Selected_Component =>
1439 Process_Path (Expr);
1442 Process_Path (Expr);
1444 when N_Type_Conversion =>
1445 Check_Node (Expression (Expr));
1447 when N_Unchecked_Type_Conversion =>
1448 Check_Node (Expression (Expr));
1450 -- Checking should not be called directly on these nodes
1452 when N_Target_Name =>
1453 raise Program_Error;
1455 -- Unsupported constructs in SPARK
1457 when N_Delta_Aggregate =>
1458 Error_Msg_N ("unsupported construct in SPARK", Expr);
1460 -- Ignored constructs for pointer checking
1462 when N_Character_Literal
1464 | N_Numeric_Or_String_Literal
1466 | N_Raise_Expression
1470 -- The following nodes are never generated in GNATprove mode
1472 when N_Expression_With_Actions
1474 | N_Unchecked_Expression
1476 raise Program_Error;
1478 end Check_Expression;
1484 procedure Check_Globals (N : Node_Id) is
1486 if Nkind (N) = N_Empty then
1491 pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
1492 PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
1493 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1498 procedure Process (Mode : Name_Id; The_Global : Entity_Id);
1499 procedure Process (Mode : Name_Id; The_Global : Node_Id) is
1500 Ident_Elt : constant Entity_Id :=
1501 Unique_Entity (Entity (The_Global));
1502 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1505 if Ekind (Ident_Elt) = E_Abstract_State then
1512 Current_Checking_Mode := Observe;
1513 Check_Node (The_Global);
1518 -- ??? Borrow not Move?
1519 Current_Checking_Mode := Borrow;
1520 Check_Node (The_Global);
1523 raise Program_Error;
1525 Current_Checking_Mode := Mode_Before;
1529 if Nkind (Expression (PAA)) = N_Null then
1532 -- No globals, nothing to do
1536 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1541 Process (Name_Input, Expression (PAA));
1543 elsif Nkind (Expression (PAA)) = N_Aggregate
1544 and then Expressions (Expression (PAA)) /= No_List
1546 -- global => (foo, bar)
1549 RHS := First (Expressions (Expression (PAA)));
1550 while Present (RHS) loop
1555 Process (Name_Input, RHS);
1557 when N_Numeric_Or_String_Literal =>
1558 Process (Name_Input, Original_Node (RHS));
1561 raise Program_Error;
1566 elsif Nkind (Expression (PAA)) = N_Aggregate
1567 and then Component_Associations (Expression (PAA)) /= No_List
1569 -- global => (mode => foo,
1570 -- mode => (bar, baz))
1571 -- A mixture of things
1574 CA : constant List_Id :=
1575 Component_Associations (Expression (PAA));
1578 while Present (Row) loop
1579 pragma Assert (List_Length (Choices (Row)) = 1);
1580 The_Mode := Chars (First (Choices (Row)));
1581 RHS := Expression (Row);
1585 RHS := First (Expressions (RHS));
1586 while Present (RHS) loop
1588 when N_Numeric_Or_String_Literal =>
1589 Process (The_Mode, Original_Node (RHS));
1592 Process (The_Mode, RHS);
1600 Process (The_Mode, RHS);
1605 when N_Numeric_Or_String_Literal =>
1606 Process (The_Mode, Original_Node (RHS));
1609 raise Program_Error;
1616 raise Program_Error;
1625 procedure Check_List (L : List_Id) is
1629 while Present (N) loop
1635 --------------------------
1636 -- Check_Loop_Statement --
1637 --------------------------
1639 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1643 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
1644 Loop_Env : constant Perm_Env_Access := new Perm_Env;
1647 -- Save environment prior to the loop
1649 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
1651 -- Add saved environment to loop environment
1653 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
1655 -- If the loop is not a plain-loop, then it may either never be entered,
1656 -- or it may be exited after a number of iterations. Hence add the
1657 -- current permission environment as the initial loop exit environment.
1658 -- Otherwise, the loop exit environment remains empty until it is
1659 -- populated by analyzing exit statements.
1661 if Present (Iteration_Scheme (Loop_N)) then
1663 Exit_Env : constant Perm_Env_Access := new Perm_Env;
1666 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
1667 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
1673 Check_Node (Iteration_Scheme (Loop_N));
1674 Check_List (Statements (Loop_N));
1676 -- Set environment to the one for exiting the loop
1679 Exit_Env : constant Perm_Env_Access :=
1680 Get (Current_Loops_Accumulators, Loop_Name);
1682 Free_Env (Current_Perm_Env);
1684 -- In the normal case, Exit_Env is not null and we use it. In the
1685 -- degraded case of a plain-loop without exit statements, Exit_Env is
1686 -- null, and we use the initial permission environment at the start
1687 -- of the loop to continue analysis. Any environment would be fine
1688 -- here, since the code after the loop is dead code, but this way we
1689 -- avoid spurious errors by having at least variables in scope inside
1692 if Exit_Env /= null then
1693 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
1695 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
1698 Free_Env (Loop_Env.all);
1699 Free_Env (Exit_Env.all);
1701 end Check_Loop_Statement;
1707 procedure Check_Node (N : Node_Id) is
1708 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1711 when N_Declaration =>
1712 Check_Declaration (N);
1715 Check_Expression (N);
1717 when N_Subtype_Indication =>
1718 Check_Node (Constraint (N));
1721 Check_Node (Get_Body_From_Stub (N));
1723 when N_Statement_Other_Than_Procedure_Call =>
1724 Check_Statement (N);
1726 when N_Package_Body =>
1727 Check_Package_Body (N);
1729 when N_Subprogram_Body
1733 Check_Callable_Body (N);
1735 when N_Protected_Body =>
1736 Check_List (Declarations (N));
1738 when N_Package_Declaration =>
1740 Spec : constant Node_Id := Specification (N);
1743 Current_Checking_Mode := Read;
1744 Check_List (Visible_Declarations (Spec));
1745 Check_List (Private_Declarations (Spec));
1747 Return_Declarations (Visible_Declarations (Spec));
1748 Return_Declarations (Private_Declarations (Spec));
1751 when N_Iteration_Scheme =>
1752 Current_Checking_Mode := Read;
1753 Check_Node (Condition (N));
1754 Check_Node (Iterator_Specification (N));
1755 Check_Node (Loop_Parameter_Specification (N));
1757 when N_Case_Expression_Alternative =>
1758 Current_Checking_Mode := Read;
1759 Check_List (Discrete_Choices (N));
1760 Current_Checking_Mode := Mode_Before;
1761 Check_Node (Expression (N));
1763 when N_Case_Statement_Alternative =>
1764 Current_Checking_Mode := Read;
1765 Check_List (Discrete_Choices (N));
1766 Current_Checking_Mode := Mode_Before;
1767 Check_List (Statements (N));
1769 when N_Component_Association =>
1770 Check_Node (Expression (N));
1772 when N_Handled_Sequence_Of_Statements =>
1773 Check_List (Statements (N));
1775 when N_Parameter_Association =>
1776 Check_Node (Explicit_Actual_Parameter (N));
1778 when N_Range_Constraint =>
1779 Check_Node (Range_Expression (N));
1781 when N_Index_Or_Discriminant_Constraint =>
1782 Check_List (Constraints (N));
1784 -- Checking should not be called directly on these nodes
1786 when N_Abortable_Part
1787 | N_Accept_Alternative
1788 | N_Access_Definition
1789 | N_Access_Function_Definition
1790 | N_Access_Procedure_Definition
1791 | N_Access_To_Object_Definition
1792 | N_Aspect_Specification
1793 | N_Compilation_Unit
1794 | N_Compilation_Unit_Aux
1795 | N_Component_Clause
1796 | N_Component_Definition
1798 | N_Constrained_Array_Definition
1800 | N_Decimal_Fixed_Point_Definition
1801 | N_Defining_Character_Literal
1802 | N_Defining_Identifier
1803 | N_Defining_Operator_Symbol
1804 | N_Defining_Program_Unit_Name
1805 | N_Delay_Alternative
1806 | N_Derived_Type_Definition
1808 | N_Discriminant_Specification
1810 | N_Entry_Body_Formal_Part
1811 | N_Enumeration_Type_Definition
1812 | N_Entry_Call_Alternative
1813 | N_Entry_Index_Specification
1815 | N_Exception_Handler
1816 | N_Floating_Point_Definition
1817 | N_Formal_Decimal_Fixed_Point_Definition
1818 | N_Formal_Derived_Type_Definition
1819 | N_Formal_Discrete_Type_Definition
1820 | N_Formal_Floating_Point_Definition
1821 | N_Formal_Incomplete_Type_Definition
1822 | N_Formal_Modular_Type_Definition
1823 | N_Formal_Ordinary_Fixed_Point_Definition
1824 | N_Formal_Private_Type_Definition
1825 | N_Formal_Signed_Integer_Type_Definition
1826 | N_Generic_Association
1828 | N_Modular_Type_Definition
1829 | N_Ordinary_Fixed_Point_Definition
1830 | N_Package_Specification
1831 | N_Parameter_Specification
1832 | N_Pragma_Argument_Association
1833 | N_Protected_Definition
1834 | N_Push_Pop_xxx_Label
1835 | N_Real_Range_Specification
1836 | N_Record_Definition
1837 | N_SCIL_Dispatch_Table_Tag_Init
1838 | N_SCIL_Dispatching_Call
1839 | N_SCIL_Membership_Test
1840 | N_Signed_Integer_Type_Definition
1843 | N_Terminate_Alternative
1844 | N_Triggering_Alternative
1845 | N_Unconstrained_Array_Definition
1851 raise Program_Error;
1853 -- Unsupported constructs in SPARK
1855 when N_Iterated_Component_Association =>
1856 Error_Msg_N ("unsupported construct in SPARK", N);
1858 -- Ignored constructs for pointer checking
1860 when N_Abstract_Subprogram_Declaration
1862 | N_Attribute_Definition_Clause
1864 | N_Delta_Constraint
1865 | N_Digits_Constraint
1867 | N_Enumeration_Representation_Clause
1868 | N_Exception_Declaration
1869 | N_Exception_Renaming_Declaration
1870 | N_Formal_Package_Declaration
1871 | N_Formal_Subprogram_Declaration
1873 | N_Freeze_Generic_Entity
1874 | N_Function_Instantiation
1875 | N_Generic_Function_Renaming_Declaration
1876 | N_Generic_Package_Declaration
1877 | N_Generic_Package_Renaming_Declaration
1878 | N_Generic_Procedure_Renaming_Declaration
1879 | N_Generic_Subprogram_Declaration
1880 | N_Implicit_Label_Declaration
1883 | N_Number_Declaration
1884 | N_Object_Renaming_Declaration
1886 | N_Package_Instantiation
1887 | N_Package_Renaming_Declaration
1889 | N_Procedure_Instantiation
1890 | N_Record_Representation_Clause
1891 | N_Subprogram_Declaration
1892 | N_Subprogram_Renaming_Declaration
1893 | N_Task_Type_Declaration
1894 | N_Use_Package_Clause
1897 | N_Validate_Unchecked_Conversion
1898 | N_Variable_Reference_Marker
1899 | N_Discriminant_Association
1901 -- ??? check whether we should do sth special for
1902 -- N_Discriminant_Association, or maybe raise a program error.
1905 -- The following nodes are rewritten by semantic analysis
1907 when N_Single_Protected_Declaration
1908 | N_Single_Task_Declaration
1910 raise Program_Error;
1913 Current_Checking_Mode := Mode_Before;
1916 ------------------------
1917 -- Check_Package_Body --
1918 ------------------------
1920 procedure Check_Package_Body (Pack : Node_Id) is
1921 Saved_Env : Perm_Env;
1925 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
1926 if Get_SPARK_Mode_From_Annotation
1927 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
1935 CorSp := Parent (Corresponding_Spec (Pack));
1936 while Nkind (CorSp) /= N_Package_Specification loop
1937 CorSp := Parent (CorSp);
1940 Check_List (Visible_Declarations (CorSp));
1944 Copy_Env (Current_Perm_Env, Saved_Env);
1945 Check_List (Private_Declarations (CorSp));
1947 -- Set mode to Read, and then analyze declarations and statements
1949 Current_Checking_Mode := Read;
1950 Check_List (Declarations (Pack));
1951 Check_Node (Handled_Statement_Sequence (Pack));
1953 -- Check RW for every stateful variable (i.e. in declarations)
1955 Return_Declarations (Private_Declarations (CorSp));
1956 Return_Declarations (Visible_Declarations (CorSp));
1957 Return_Declarations (Declarations (Pack));
1959 -- Restore previous environment (i.e. delete every nonvisible
1960 -- declaration) from environment.
1962 Free_Env (Current_Perm_Env);
1963 Copy_Env (Saved_Env, Current_Perm_Env);
1964 end Check_Package_Body;
1966 --------------------
1967 -- Check_Param_In --
1968 --------------------
1970 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
1971 Mode : constant Entity_Kind := Ekind (Formal);
1972 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1974 case Formal_Kind'(Mode
) is
1976 -- Formal IN parameter
1978 when E_In_Parameter
=>
1980 -- Formal IN parameter, access type
1982 if Is_Access_Type
(Etype
(Formal
)) then
1984 -- Formal IN parameter, access to variable type
1986 if not Is_Access_Constant
(Etype
(Formal
)) then
1988 -- Formal IN parameter, named/anonymous access to variable
1991 Current_Checking_Mode
:= Borrow
;
1992 Check_Node
(Actual
);
1994 -- Formal IN parameter, access to constant type
1995 -- Formal IN parameter, access to named constant type
1997 elsif not Is_Anonymous_Access_Type
(Etype
(Formal
)) then
1998 Error_Msg_N
("assignment not allowed, Ownership Aspect"
1999 & " False (Named general access type)",
2002 -- Formal IN parameter, access to anonymous constant type
2005 Current_Checking_Mode
:= Observe
;
2006 Check_Node
(Actual
);
2009 -- Formal IN parameter, composite type
2011 elsif Is_Deep
(Etype
(Formal
)) then
2013 -- Composite formal types should be named
2014 -- Formal IN parameter, composite named type
2016 Current_Checking_Mode
:= Observe
;
2017 Check_Node
(Actual
);
2020 when E_Out_Parameter
2021 | E_In_Out_Parameter
2026 Current_Checking_Mode
:= Mode_Before
;
2029 ----------------------
2030 -- Check_Param_Out --
2031 ----------------------
2033 procedure Check_Param_Out
(Formal
: Entity_Id
; Actual
: Node_Id
) is
2034 Mode
: constant Entity_Kind
:= Ekind
(Formal
);
2035 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2038 case Formal_Kind
'(Mode) is
2040 -- Formal OUT/IN OUT parameter
2042 when E_Out_Parameter
2043 | E_In_Out_Parameter
2046 -- Formal OUT/IN OUT parameter, access type
2048 if Is_Access_Type (Etype (Formal)) then
2050 -- Formal OUT/IN OUT parameter, access to variable type
2052 if not Is_Access_Constant (Etype (Formal)) then
2054 -- Cannot have anonymous out access parameter
2055 -- Formal out/in out parameter, access to named variable
2058 Current_Checking_Mode := Move;
2059 Check_Node (Actual);
2061 -- Formal out/in out parameter, access to constant type
2064 Error_Msg_N ("assignment not allowed, Ownership Aspect False"
2065 & " (Named general access type)", Formal);
2069 -- Formal out/in out parameter, composite type
2071 elsif Is_Deep (Etype (Formal)) then
2073 -- Composite formal types should be named
2074 -- Formal out/in out Parameter, Composite Named type.
2076 Current_Checking_Mode := Borrow;
2077 Check_Node (Actual);
2080 when E_In_Parameter =>
2084 Current_Checking_Mode := Mode_Before;
2085 end Check_Param_Out;
2087 -------------------------
2088 -- Check_Safe_Pointers --
2089 -------------------------
2091 procedure Check_Safe_Pointers (N : Node_Id) is
2093 -- Local subprograms
2095 procedure Check_List (L : List_Id);
2096 -- Call the main analysis procedure on each element of the list
2098 procedure Initialize;
2099 -- Initialize global variables before starting the analysis of a body
2105 procedure Check_List (L : List_Id) is
2109 while Present (N) loop
2110 Check_Safe_Pointers (N);
2119 procedure Initialize is
2121 Reset (Current_Loops_Envs);
2122 Reset (Current_Loops_Accumulators);
2123 Reset (Current_Perm_Env);
2124 Reset (Current_Initialization_Map);
2131 -- SPARK_Mode pragma in application
2133 -- Start of processing for Check_Safe_Pointers
2138 when N_Compilation_Unit =>
2139 Check_Safe_Pointers (Unit (N));
2142 | N_Package_Declaration
2145 Prag := SPARK_Pragma (Defining_Entity (N));
2146 if Present (Prag) then
2147 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
2153 elsif Nkind (N) = N_Package_Body then
2154 Check_List (Declarations (N));
2156 elsif Nkind (N) = N_Package_Declaration then
2157 Check_List (Private_Declarations (Specification (N)));
2158 Check_List (Visible_Declarations (Specification (N)));
2164 end Check_Safe_Pointers;
2166 ---------------------
2167 -- Check_Statement --
2168 ---------------------
2170 procedure Check_Statement (Stmt : Node_Id) is
2171 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2172 State_N : Perm_Kind;
2173 Check : Boolean := True;
2175 Ty_St_Name : Node_Id;
2177 function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
2178 -- Return the root of the name given as input
2180 function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
2182 case Nkind (Comp_Stmt) is
2185 => return Comp_Stmt;
2187 when N_Type_Conversion
2188 | N_Unchecked_Type_Conversion
2189 | N_Qualified_Expression
2191 return Get_Root (Expression (Comp_Stmt));
2193 when N_Parameter_Specification =>
2194 return Get_Root (Defining_Identifier (Comp_Stmt));
2196 when N_Selected_Component
2197 | N_Indexed_Component
2199 | N_Explicit_Dereference
2201 return Get_Root (Prefix (Comp_Stmt));
2204 raise Program_Error;
2209 case N_Statement_Other_Than_Procedure_Call'(Nkind
(Stmt
)) is
2210 when N_Entry_Call_Statement
=>
2211 Check_Call_Statement
(Stmt
);
2213 -- Move right-hand side first, and then assign left-hand side
2215 when N_Assignment_Statement
=>
2217 St_Name
:= Name
(Stmt
);
2218 Ty_St_Name
:= Etype
(Name
(Stmt
));
2220 -- Check that is not a *general* access type
2222 if Has_Ownership_Aspect_True
(St_Name
, "assigning to") then
2224 -- Assigning to access type
2226 if Is_Access_Type
(Ty_St_Name
) then
2228 -- Assigning to access to variable type
2230 if not Is_Access_Constant
(Ty_St_Name
) then
2232 -- Assigning to named access to variable type
2234 if not Is_Anonymous_Access_Type
(Ty_St_Name
) then
2235 Current_Checking_Mode
:= Move
;
2237 -- Assigning to anonymous access to variable type
2240 -- Target /= source root
2242 if Nkind_In
(Expression
(Stmt
), N_Allocator
, N_Null
)
2243 or else St_Name
/= Get_Root
(Expression
(Stmt
))
2245 Error_Msg_N
("assignment not allowed, anonymous "
2246 & "access Object with Different Root",
2250 -- Target = source root
2253 -- Here we do nothing on the source nor on the
2254 -- target. However, we check the the legality rule:
2255 -- "The source shall be an owning access object
2256 -- denoted by a name that is not in the observed
2259 State_N
:= Get_Perm
(Expression
(Stmt
));
2260 if State_N
= Observed
then
2261 Error_Msg_N
("assignment not allowed, Anonymous "
2262 & "access object with the same root"
2263 & " but source Observed", Stmt
);
2269 -- else access-to-constant
2271 -- Assigning to anonymous access-to-constant type
2273 elsif Is_Anonymous_Access_Type
(Ty_St_Name
) then
2275 -- ??? Check the follwing condition. We may have to
2276 -- add that the root is in the observed state too.
2278 State_N
:= Get_Perm
(Expression
(Stmt
));
2279 if State_N
/= Observed
then
2280 Error_Msg_N
("assignment not allowed, anonymous "
2281 & "access-to-constant object not in "
2282 & "the observed state)", Stmt
);
2286 Error_Msg_N
("?here check accessibility level cited in"
2287 & " the second legality rule of assign",
2292 -- Assigning to named access-to-constant type:
2293 -- This case should have been detected when checking
2294 -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
2297 raise Program_Error
;
2300 -- Assigning to composite (deep) type.
2302 elsif Is_Deep
(Ty_St_Name
) then
2303 if Ekind
(Ty_St_Name
) = E_Record_Type
then
2306 First_Component_Or_Discriminant
(Ty_St_Name
);
2309 while Present
(Elmt
) loop
2310 if Is_Anonymous_Access_Type
(Etype
(Elmt
)) or
2311 Ekind
(Elmt
) = E_General_Access_Type
2313 Error_Msg_N
("assignment not allowed, Ownership "
2314 & "Aspect False (Components have "
2315 & "Ownership Aspect False)", Stmt
);
2320 Next_Component_Or_Discriminant
(Elmt
);
2324 -- Record types are always named so this is a move
2327 Current_Checking_Mode
:= Move
;
2331 -- Now handle legality rules of using a borrowed, observed,
2332 -- or moved name as a prefix in an assignment.
2335 if Nkind_In
(St_Name
,
2336 N_Attribute_Reference
,
2338 N_Explicit_Dereference
,
2339 N_Indexed_Component
,
2341 N_Selected_Component
,
2345 if Is_Access_Type
(Etype
(Prefix
(St_Name
))) or
2346 Is_Deep
(Etype
(Prefix
(St_Name
)))
2349 -- We set the Check variable to True so that we can
2350 -- Check_Node of the expression and the name first
2351 -- under the assumption of Current_Checking_Mode =
2352 -- Read => nothing to be done for the RHS if the
2353 -- following check on the expression fails, and
2354 -- Current_Checking_Mode := Assign => the name should
2355 -- not be borrowed or observed so that we can use it
2356 -- as a prefix in the target of an assignement.
2358 -- Note that we do not need to check the OA here
2359 -- because we are allowed to read and write "through"
2360 -- an object of OAF (example: traversing a DS).
2366 if Nkind_In
(Expression
(Stmt
),
2367 N_Attribute_Reference
,
2369 N_Explicit_Dereference
,
2370 N_Indexed_Component
,
2372 N_Selected_Component
,
2376 if Is_Access_Type
(Etype
(Prefix
(Expression
(Stmt
))))
2377 or else Is_Deep
(Etype
(Prefix
(Expression
(Stmt
))))
2379 Current_Checking_Mode
:= Observe
;
2386 Check_Node
(Expression
(Stmt
));
2387 Current_Checking_Mode
:= Assign
;
2388 Check_Node
(St_Name
);
2392 when N_Block_Statement
=>
2394 Saved_Env
: Perm_Env
;
2398 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2400 -- Analyze declarations and Handled_Statement_Sequences
2402 Current_Checking_Mode
:= Read
;
2403 Check_List
(Declarations
(Stmt
));
2404 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2406 -- Restore environment
2408 Free_Env
(Current_Perm_Env
);
2409 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2412 when N_Case_Statement
=>
2414 Saved_Env
: Perm_Env
;
2416 -- Accumulator for the different branches
2419 Elmt
: Node_Id
:= First
(Alternatives
(Stmt
));
2422 Current_Checking_Mode
:= Read
;
2423 Check_Node
(Expression
(Stmt
));
2424 Current_Checking_Mode
:= Mode_Before
;
2428 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2430 -- Here we have the original env in saved, current with a fresh
2431 -- copy, and new aliased.
2433 -- First alternative
2437 Copy_Env
(Current_Perm_Env
, New_Env
);
2438 Free_Env
(Current_Perm_Env
);
2440 -- Other alternatives
2442 while Present
(Elmt
) loop
2444 -- Restore environment
2446 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2451 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2453 Free_Env
(Saved_Env
);
2456 when N_Delay_Relative_Statement
=>
2457 Check_Node
(Expression
(Stmt
));
2459 when N_Delay_Until_Statement
=>
2460 Check_Node
(Expression
(Stmt
));
2462 when N_Loop_Statement
=>
2463 Check_Loop_Statement
(Stmt
);
2465 -- If deep type expression, then move, else read
2467 when N_Simple_Return_Statement
=>
2468 case Nkind
(Expression
(Stmt
)) is
2471 -- ??? This does not take into account the fact that
2472 -- a simple return inside an extended return statement
2473 -- applies to the extended return statement.
2474 Subp
: constant Entity_Id
:=
2475 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2477 Return_Globals
(Subp
);
2481 if Is_Deep
(Etype
(Expression
(Stmt
))) then
2482 Current_Checking_Mode
:= Move
;
2488 Check_Node
(Expression
(Stmt
));
2492 when N_Extended_Return_Statement
=>
2493 Check_List
(Return_Object_Declarations
(Stmt
));
2494 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2495 Return_Declarations
(Return_Object_Declarations
(Stmt
));
2497 -- ??? This does not take into account the fact that a simple
2498 -- return inside an extended return statement applies to the
2499 -- extended return statement.
2500 Subp
: constant Entity_Id
:=
2501 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2504 Return_Globals
(Subp
);
2507 -- Nothing to do when exiting a loop. No merge needed
2509 when N_Exit_Statement
=>
2512 -- Copy environment, run on each branch
2514 when N_If_Statement
=>
2516 Saved_Env
: Perm_Env
;
2518 -- Accumulator for the different branches
2523 Check_Node
(Condition
(Stmt
));
2527 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2529 -- Here we have the original env in saved, current with a fresh
2534 Check_List
(Then_Statements
(Stmt
));
2535 Copy_Env
(Current_Perm_Env
, New_Env
);
2536 Free_Env
(Current_Perm_Env
);
2538 -- Here the new_environment contains curr env after then block
2546 Elmt
:= First
(Elsif_Parts
(Stmt
));
2547 while Present
(Elmt
) loop
2549 -- Transfer into accumulator, and restore from save
2551 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2552 Check_Node
(Condition
(Elmt
));
2553 Check_List
(Then_Statements
(Stmt
));
2560 -- Restore environment before if
2562 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2564 -- Here new environment contains the environment after then and
2565 -- current the fresh copy of old one.
2567 Check_List
(Else_Statements
(Stmt
));
2571 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2574 Free_Env
(Saved_Env
);
2577 -- Unsupported constructs in SPARK
2579 when N_Abort_Statement
2580 | N_Accept_Statement
2581 | N_Asynchronous_Select
2583 | N_Conditional_Entry_Call
2585 | N_Requeue_Statement
2586 | N_Selective_Accept
2587 | N_Timed_Entry_Call
2589 Error_Msg_N
("unsupported construct in SPARK", Stmt
);
2591 -- Ignored constructs for pointer checking
2593 when N_Null_Statement
2598 -- The following nodes are never generated in GNATprove mode
2600 when N_Compound_Statement
2603 raise Program_Error
;
2605 end Check_Statement
;
2611 function Get_Perm
(N
: Node_Id
) return Perm_Kind
is
2612 Tree_Or_Perm
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(N
);
2615 case Tree_Or_Perm
.R
is
2617 return Tree_Or_Perm
.Found_Permission
;
2620 pragma Assert
(Tree_Or_Perm
.Tree_Access
/= null);
2621 return Permission
(Tree_Or_Perm
.Tree_Access
);
2623 -- We encoutered a function call, hence the memory area is fresh,
2624 -- which means that the association permission is RW.
2626 when Function_Call
=>
2627 return Unrestricted
;
2631 ----------------------
2632 -- Get_Perm_Or_Tree --
2633 ----------------------
2635 function Get_Perm_Or_Tree
(N
: Node_Id
) return Perm_Or_Tree
is
2639 -- Base identifier. Normally those are the roots of the trees stored
2640 -- in the permission environment.
2642 when N_Defining_Identifier
=>
2643 raise Program_Error
;
2649 P
: constant Entity_Id
:= Entity
(N
);
2650 C
: constant Perm_Tree_Access
:=
2651 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2654 -- Setting the initialization map to True, so that this
2655 -- variable cannot be ignored anymore when looking at end
2656 -- of elaboration of package.
2658 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2660 -- No null possible here, there are no parents for the path.
2661 -- This means we are using a global variable without adding
2662 -- it in environment with a global aspect.
2664 Illegal_Global_Usage
(N
);
2667 return (R
=> Unfolded
, Tree_Access
=> C
);
2671 when N_Type_Conversion
2672 | N_Unchecked_Type_Conversion
2673 | N_Qualified_Expression
2675 return Get_Perm_Or_Tree
(Expression
(N
));
2677 -- Happening when we try to get the permission of a variable that
2678 -- is a formal parameter. We get instead the defining identifier
2679 -- associated with the parameter (which is the one that has been
2680 -- stored for indexing).
2682 when N_Parameter_Specification
=>
2683 return Get_Perm_Or_Tree
(Defining_Identifier
(N
));
2685 -- We get the permission tree of its prefix, and then get either the
2686 -- subtree associated with that specific selection, or if we have a
2687 -- leaf that folds its children, we take the children's permission
2688 -- and return it using the discriminant Folded.
2690 when N_Selected_Component
=>
2692 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2702 pragma Assert
(C
.Tree_Access
/= null);
2703 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2705 Kind
(C
.Tree_Access
) = Record_Component
);
2707 if Kind
(C
.Tree_Access
) = Record_Component
then
2709 Selected_Component
: constant Entity_Id
:=
2710 Entity
(Selector_Name
(N
));
2711 Selected_C
: constant Perm_Tree_Access
:=
2713 (Component
(C
.Tree_Access
), Selected_Component
);
2716 if Selected_C
= null then
2717 return (R
=> Unfolded
,
2719 Other_Components
(C
.Tree_Access
));
2722 return (R
=> Unfolded
,
2723 Tree_Access
=> Selected_C
);
2727 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2728 return (R
=> Folded
,
2730 Children_Permission
(C
.Tree_Access
));
2733 raise Program_Error
;
2737 -- We get the permission tree of its prefix, and then get either the
2738 -- subtree associated with that specific selection, or if we have a
2739 -- leaf that folds its children, we take the children's permission
2740 -- and return it using the discriminant Folded.
2742 when N_Indexed_Component
2746 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2756 pragma Assert
(C
.Tree_Access
/= null);
2757 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2759 Kind
(C
.Tree_Access
) = Array_Component
);
2761 if Kind
(C
.Tree_Access
) = Array_Component
then
2762 pragma Assert
(Get_Elem
(C
.Tree_Access
) /= null);
2763 return (R
=> Unfolded
,
2764 Tree_Access
=> Get_Elem
(C
.Tree_Access
));
2766 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2767 return (R
=> Folded
, Found_Permission
=>
2768 Children_Permission
(C
.Tree_Access
));
2771 raise Program_Error
;
2775 -- We get the permission tree of its prefix, and then get either the
2776 -- subtree associated with that specific selection, or if we have a
2777 -- leaf that folds its children, we take the children's permission
2778 -- and return it using the discriminant Folded.
2780 when N_Explicit_Dereference
=>
2782 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2792 pragma Assert
(C
.Tree_Access
/= null);
2793 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2795 Kind
(C
.Tree_Access
) = Reference
);
2797 if Kind
(C
.Tree_Access
) = Reference
then
2798 if Get_All
(C
.Tree_Access
) = null then
2802 raise Program_Error
;
2807 Tree_Access
=> Get_All
(C
.Tree_Access
));
2810 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2811 return (R
=> Folded
, Found_Permission
=>
2812 Children_Permission
(C
.Tree_Access
));
2815 raise Program_Error
;
2819 -- The name contains a function call, hence the given path is always
2820 -- new. We do not have to check for anything.
2822 when N_Function_Call
=>
2823 return (R
=> Function_Call
);
2826 raise Program_Error
;
2828 end Get_Perm_Or_Tree
;
2834 function Get_Perm_Tree
(N
: Node_Id
) return Perm_Tree_Access
is
2838 -- Base identifier. Normally those are the roots of the trees stored
2839 -- in the permission environment.
2841 when N_Defining_Identifier
=>
2842 raise Program_Error
;
2848 P
: constant Node_Id
:= Entity
(N
);
2849 C
: constant Perm_Tree_Access
:=
2850 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2853 -- Setting the initialization map to True, so that this
2854 -- variable cannot be ignored anymore when looking at end
2855 -- of elaboration of package.
2857 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2859 -- No null possible here, there are no parents for the path.
2860 -- This means we are using a global variable without adding
2861 -- it in environment with a global aspect.
2863 Illegal_Global_Usage
(N
);
2870 when N_Type_Conversion
2871 | N_Unchecked_Type_Conversion
2872 | N_Qualified_Expression
2874 return Get_Perm_Tree
(Expression
(N
));
2876 when N_Parameter_Specification
=>
2877 return Get_Perm_Tree
(Defining_Identifier
(N
));
2879 -- We get the permission tree of its prefix, and then get either the
2880 -- subtree associated with that specific selection, or if we have a
2881 -- leaf that folds its children, we unroll it in one step.
2883 when N_Selected_Component
=>
2885 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
2890 -- If null then it means we went through a function call
2895 pragma Assert
(Kind
(C
) = Entire_Object
2896 or else Kind
(C
) = Record_Component
);
2898 if Kind
(C
) = Record_Component
then
2900 -- The tree is unfolded. We just return the subtree.
2903 Selected_Component
: constant Entity_Id
:=
2904 Entity
(Selector_Name
(N
));
2905 Selected_C
: constant Perm_Tree_Access
:=
2907 (Component
(C
), Selected_Component
);
2910 if Selected_C
= null then
2911 return Other_Components
(C
);
2916 elsif Kind
(C
) = Entire_Object
then
2918 -- Expand the tree. Replace the node with
2919 -- Record_Component.
2923 -- Create the unrolled nodes
2925 Son
: Perm_Tree_Access
;
2927 Child_Perm
: constant Perm_Kind
:=
2928 Children_Permission
(C
);
2931 -- We change the current node from Entire_Object to
2932 -- Record_Component with same permission and an empty
2933 -- hash table as component list.
2936 (Kind
=> Record_Component
,
2937 Is_Node_Deep
=> Is_Node_Deep
(C
),
2938 Permission
=> Permission
(C
),
2939 Component
=> Perm_Tree_Maps
.Nil
,
2941 new Perm_Tree_Wrapper
'
2943 (Kind => Entire_Object,
2944 -- Is_Node_Deep is true, to be conservative
2945 Is_Node_Deep => True,
2946 Permission => Child_Perm,
2947 Children_Permission => Child_Perm)
2951 -- We fill the hash table with all sons of the record,
2952 -- with basic Entire_Objects nodes.
2954 Elem := First_Component_Or_Discriminant
2955 (Etype (Prefix (N)));
2957 while Present (Elem) loop
2958 Son := new Perm_Tree_Wrapper'
2960 (Kind
=> Entire_Object
,
2961 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
2962 Permission
=> Child_Perm
,
2963 Children_Permission
=> Child_Perm
));
2966 (C
.all.Tree
.Component
, Elem
, Son
);
2967 Next_Component_Or_Discriminant
(Elem
);
2969 -- we return the tree to the sons, so that the recursion
2973 Selected_Component
: constant Entity_Id
:=
2974 Entity
(Selector_Name
(N
));
2976 Selected_C
: constant Perm_Tree_Access
:=
2978 (Component
(C
), Selected_Component
);
2981 pragma Assert
(Selected_C
/= null);
2986 raise Program_Error
;
2989 -- We set the permission tree of its prefix, and then we extract from
2990 -- the returned pointer the subtree. If folded, we unroll the tree at
2993 when N_Indexed_Component
2997 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
3001 -- If null then we went through a function call
3005 pragma Assert
(Kind
(C
) = Entire_Object
3006 or else Kind
(C
) = Array_Component
);
3008 if Kind
(C
) = Array_Component
then
3010 -- The tree is unfolded. We just return the elem subtree
3012 pragma Assert
(Get_Elem
(C
) = null);
3013 return Get_Elem
(C
);
3015 elsif Kind
(C
) = Entire_Object
then
3017 -- Expand the tree. Replace node with Array_Component.
3019 Son
: Perm_Tree_Access
;
3022 Son
:= new Perm_Tree_Wrapper
'
3024 (Kind => Entire_Object,
3025 Is_Node_Deep => Is_Node_Deep (C),
3026 Permission => Children_Permission (C),
3027 Children_Permission => Children_Permission (C)));
3029 -- We change the current node from Entire_Object
3030 -- to Array_Component with same permission and the
3031 -- previously defined son.
3033 C.all.Tree := (Kind => Array_Component,
3034 Is_Node_Deep => Is_Node_Deep (C),
3035 Permission => Permission (C),
3037 return Get_Elem (C);
3040 raise Program_Error;
3043 -- We get the permission tree of its prefix, and then get either the
3044 -- subtree associated with that specific selection, or if we have a
3045 -- leaf that folds its children, we unroll the tree.
3047 when N_Explicit_Dereference =>
3049 C : Perm_Tree_Access;
3052 C := Get_Perm_Tree (Prefix (N));
3056 -- If null, we went through a function call
3061 pragma Assert (Kind (C) = Entire_Object
3062 or else Kind (C) = Reference);
3064 if Kind (C) = Reference then
3066 -- The tree is unfolded. We return the elem subtree
3068 if Get_All (C) = null then
3072 raise Program_Error;
3076 elsif Kind (C) = Entire_Object then
3078 -- Expand the tree. Replace the node with Reference.
3080 Son : Perm_Tree_Access;
3083 Son := new Perm_Tree_Wrapper'
3085 (Kind
=> Entire_Object
,
3086 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
3087 Permission
=> Children_Permission
(C
),
3088 Children_Permission
=> Children_Permission
(C
)));
3090 -- We change the current node from Entire_Object to
3091 -- Reference with same permission and the previous son.
3093 pragma Assert
(Is_Node_Deep
(C
));
3094 C
.all.Tree
:= (Kind
=> Reference
,
3095 Is_Node_Deep
=> Is_Node_Deep
(C
),
3096 Permission
=> Permission
(C
),
3101 raise Program_Error
;
3104 -- No permission tree for function calls
3106 when N_Function_Call
=>
3110 raise Program_Error
;
3118 procedure Hp
(P
: Perm_Env
) is
3119 Elem
: Perm_Tree_Maps
.Key_Option
;
3122 Elem
:= Get_First_Key
(P
);
3123 while Elem
.Present
loop
3124 Print_Node_Briefly
(Elem
.K
);
3125 Elem
:= Get_Next_Key
(P
);
3129 --------------------------
3130 -- Illegal_Global_Usage --
3131 --------------------------
3133 procedure Illegal_Global_Usage
(N
: Node_Or_Entity_Id
) is
3135 Error_Msg_NE
("cannot use global variable & of deep type", N
, N
);
3136 Error_Msg_N
("\without prior declaration in a Global aspect", N
);
3137 Errout
.Finalize
(Last_Call
=> True);
3138 Errout
.Output_Messages
;
3139 Exit_Program
(E_Errors
);
3140 end Illegal_Global_Usage
;
3146 function Is_Deep
(E
: Entity_Id
) return Boolean is
3147 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean;
3148 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean is
3150 Pack_Decl
: Node_Id
;
3153 if Is_Itype
(E
) then
3154 Decl
:= Associated_Node_For_Itype
(E
);
3159 Pack_Decl
:= Parent
(Parent
(Decl
));
3161 if Nkind
(Pack_Decl
) /= N_Package_Declaration
then
3166 Present
(SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
)))
3167 and then Get_SPARK_Mode_From_Annotation
3168 (SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
))) = Off
;
3169 end Is_Private_Entity_Mode_Off
;
3172 pragma Assert
(Is_Type
(E
));
3180 -- Just check the depth of its component type
3185 return Is_Deep
(Component_Type
(E
));
3187 when E_String_Literal_Subtype
=>
3190 -- Per RM 8.11 for class-wide types
3192 when E_Class_Wide_Subtype
3197 -- ??? What about hidden components
3206 Elmt
:= First_Component_Or_Discriminant
(E
);
3207 while Present
(Elmt
) loop
3208 if Is_Deep
(Etype
(Elmt
)) then
3211 Next_Component_Or_Discriminant
(Elmt
);
3217 when Private_Kind
=>
3218 if Is_Private_Entity_Mode_Off
(E
) then
3221 if Present
(Full_View
(E
)) then
3222 return Is_Deep
(Full_View
(E
));
3228 when E_Incomplete_Type
3229 | E_Incomplete_Subtype
3233 -- No problem with synchronized types
3235 when E_Protected_Type
3236 | E_Protected_Subtype
3242 when E_Exception_Type
=>
3246 raise Program_Error
;
3254 procedure Perm_Error
3257 Found_Perm
: Perm_Kind
)
3259 procedure Set_Root_Object
3261 Obj
: out Entity_Id
;
3262 Deref
: out Boolean);
3263 -- Set the root object Obj, and whether the path contains a dereference,
3264 -- from a path Path.
3266 ---------------------
3267 -- Set_Root_Object --
3268 ---------------------
3270 procedure Set_Root_Object
3272 Obj
: out Entity_Id
;
3273 Deref
: out Boolean)
3276 case Nkind
(Path
) is
3280 Obj
:= Entity
(Path
);
3283 when N_Type_Conversion
3284 | N_Unchecked_Type_Conversion
3285 | N_Qualified_Expression
3287 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
3289 when N_Indexed_Component
3290 | N_Selected_Component
3293 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3295 when N_Explicit_Dereference
=>
3296 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3300 raise Program_Error
;
3302 end Set_Root_Object
;
3308 -- Start of processing for Perm_Error
3311 Set_Root_Object
(N
, Root
, Is_Deref
);
3315 ("insufficient permission on dereference from &", N
, Root
);
3317 Error_Msg_NE
("insufficient permission for &", N
, Root
);
3320 Perm_Mismatch
(Perm
, Found_Perm
, N
);
3323 -------------------------------
3324 -- Perm_Error_Subprogram_End --
3325 -------------------------------
3327 procedure Perm_Error_Subprogram_End
3331 Found_Perm
: Perm_Kind
)
3334 Error_Msg_Node_2
:= Subp
;
3335 Error_Msg_NE
("insufficient permission for & when returning from &",
3337 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
3338 end Perm_Error_Subprogram_End
;
3344 procedure Process_Path
(N
: Node_Id
) is
3345 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
3346 State_N
: Perm_Kind
;
3348 -- We ignore if yielding to synchronized
3351 and then Is_Synchronized_Object
(Root
)
3356 State_N
:= Get_Perm
(N
);
3358 case Current_Checking_Mode
is
3360 -- Check permission R, do nothing
3364 -- This condition should be removed when removing the read
3371 -- The rhs object in an assignment statement (including copy in
3372 -- and copy back) should be in the Unrestricted or Moved state.
3373 -- Otherwise the move is not allowed.
3374 -- This applies to both stand-alone and composite objects.
3375 -- If the state of the source is Moved, then a warning message
3376 -- is prompt to make the user aware of reading a nullified
3379 if State_N
/= Unrestricted
and State_N
/= Moved
then
3380 Perm_Error
(N
, Unrestricted
, State_N
);
3384 -- In the AI, after moving a path nothing to do since the rhs
3385 -- object was in the Unrestricted state and it shall be
3386 -- refreshed to Unrestricted. The object should be nullified
3387 -- however. To avoid moving again a name that has already been
3388 -- moved, in this implementation we set the state of the moved
3389 -- object to "Moved". This shall be used to prompt a warning
3390 -- when manipulating a null pointer and also to implement
3391 -- the no aliasing parameter restriction.
3393 if State_N
= Moved
then
3394 Error_Msg_N
("?the source or one of its extensions has"
3395 & " already been moved", N
);
3399 -- Set state to Borrowed to the path and any of its prefixes
3401 Tree
: constant Perm_Tree_Access
:=
3402 Set_Perm_Prefixes
(N
, Moved
);
3407 -- We went through a function call, no permission to
3413 -- Set state to Borrowed on any strict extension of the path
3415 Set_Perm_Extensions
(Tree
, Moved
);
3420 -- The lhs object in an assignment statement (including copy in
3421 -- and copy back) should be in the Unrestricted state.
3422 -- Otherwise the move is not allowed.
3423 -- This applies to both stand-alone and composite objects.
3425 if State_N
/= Unrestricted
and State_N
/= Moved
then
3426 Perm_Error
(N
, Unrestricted
, State_N
);
3430 -- After assigning to a path nothing to do since it was in the
3431 -- Unrestricted state and it would be refreshed to
3436 -- Borrowing is only allowed on Unrestricted objects.
3438 if State_N
/= Unrestricted
and State_N
/= Moved
then
3439 Perm_Error
(N
, Unrestricted
, State_N
);
3442 if State_N
= Moved
then
3443 Error_Msg_N
("?the source or one of its extensions has"
3444 & " already been moved", N
);
3448 -- Set state to Borrowed to the path and any of its prefixes
3450 Tree
: constant Perm_Tree_Access
:=
3451 Set_Perm_Prefixes
(N
, Borrowed
);
3456 -- We went through a function call, no permission to
3462 -- Set state to Borrowed on any strict extension of the path
3464 Set_Perm_Extensions
(Tree
, Borrowed
);
3468 if State_N
/= Unrestricted
3469 and then State_N
/= Observed
3471 Perm_Error
(N
, Observed
, State_N
);
3475 -- Set permission to Observed on the path and any of its
3476 -- prefixes if it is of a deep type. Actually, some operation
3477 -- like reading from an object of access type is considered as
3478 -- observe while it should not affect the permissions of
3479 -- the considered tree.
3481 Tree
: Perm_Tree_Access
;
3484 if Is_Deep
(Etype
(N
)) then
3485 Tree
:= Set_Perm_Prefixes
(N
, Observed
);
3492 -- We went through a function call, no permission to
3498 -- Set permissions to No on any strict extension of the path
3500 Set_Perm_Extensions
(Tree
, Observed
);
3505 -------------------------
3506 -- Return_Declarations --
3507 -------------------------
3509 procedure Return_Declarations
(L
: List_Id
) is
3510 procedure Return_Declaration
(Decl
: Node_Id
);
3511 -- Check correct permissions for every declared object
3513 ------------------------
3514 -- Return_Declaration --
3515 ------------------------
3517 procedure Return_Declaration
(Decl
: Node_Id
) is
3519 if Nkind
(Decl
) = N_Object_Declaration
then
3521 -- Check RW for object declared, unless the object has never been
3524 if Get
(Current_Initialization_Map
,
3525 Unique_Entity
(Defining_Identifier
(Decl
))) = False
3531 Elem
: constant Perm_Tree_Access
:=
3532 Get
(Current_Perm_Env
,
3533 Unique_Entity
(Defining_Identifier
(Decl
)));
3538 -- Here we are on a declaration. Hence it should have been
3539 -- added in the environment when analyzing this node with
3540 -- mode Read. Hence it is not possible to find a null
3545 raise Program_Error
;
3548 if Permission
(Elem
) /= Unrestricted
then
3549 Perm_Error
(Decl
, Unrestricted
, Permission
(Elem
));
3553 end Return_Declaration
;
3558 -- Start of processing for Return_Declarations
3562 while Present
(N
) loop
3563 Return_Declaration
(N
);
3566 end Return_Declarations
;
3568 --------------------
3569 -- Return_Globals --
3570 --------------------
3572 procedure Return_Globals
(Subp
: Entity_Id
) is
3573 procedure Return_Globals_From_List
3574 (First_Item
: Node_Id
;
3575 Kind
: Formal_Kind
);
3576 -- Return global items from the list starting at Item
3578 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
3579 -- Return global items for the mode Global_Mode
3581 ------------------------------
3582 -- Return_Globals_From_List --
3583 ------------------------------
3585 procedure Return_Globals_From_List
3586 (First_Item
: Node_Id
;
3589 Item
: Node_Id
:= First_Item
;
3593 while Present
(Item
) loop
3596 -- Ignore abstract states, which play no role in pointer aliasing
3598 if Ekind
(E
) = E_Abstract_State
then
3601 Return_The_Global
(E
, Kind
, Subp
);
3605 end Return_Globals_From_List
;
3607 ----------------------------
3608 -- Return_Globals_Of_Mode --
3609 ----------------------------
3611 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
3619 Kind
:= E_In_Parameter
;
3621 Kind
:= E_Out_Parameter
;
3623 Kind
:= E_In_Out_Parameter
;
3625 raise Program_Error
;
3628 -- Return both global items from Global and Refined_Global pragmas
3630 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
3631 Return_Globals_From_List
3632 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
3633 end Return_Globals_Of_Mode
;
3635 -- Start of processing for Return_Globals
3638 Return_Globals_Of_Mode
(Name_Proof_In
);
3639 Return_Globals_Of_Mode
(Name_Input
);
3640 Return_Globals_Of_Mode
(Name_Output
);
3641 Return_Globals_Of_Mode
(Name_In_Out
);
3644 --------------------------------
3645 -- Return_Parameter_Or_Global --
3646 --------------------------------
3648 procedure Return_The_Global
3653 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
3654 pragma Assert
(Elem
/= null);
3657 -- Observed IN parameters and globals need not return a permission to
3660 if Mode
= E_In_Parameter
3662 -- Check this for read-only globals.
3665 if Permission
(Elem
) /= Unrestricted
3666 and then Permission
(Elem
) /= Observed
3668 Perm_Error_Subprogram_End
3672 Found_Perm
=> Permission
(Elem
));
3675 -- All globals of mode out or in/out should return with mode
3679 if Permission
(Elem
) /= Unrestricted
then
3680 Perm_Error_Subprogram_End
3683 Perm
=> Unrestricted
,
3684 Found_Perm
=> Permission
(Elem
));
3687 end Return_The_Global
;
3689 -------------------------
3690 -- Set_Perm_Extensions --
3691 -------------------------
3693 procedure Set_Perm_Extensions
(T
: Perm_Tree_Access
; P
: Perm_Kind
) is
3694 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
3695 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
) is
3698 when Entire_Object
=>
3702 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
3704 when Array_Component
=>
3705 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
3707 -- Free every Component subtree
3709 when Record_Component
=>
3711 Comp
: Perm_Tree_Access
;
3714 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
3715 while Comp
/= null loop
3716 Free_Perm_Tree
(Comp
);
3717 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
3720 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
3723 end Free_Perm_Tree_Children
;
3725 Son
: constant Perm_Tree
:=
3727 (Kind => Entire_Object,
3728 Is_Node_Deep => Is_Node_Deep (T),
3729 Permission => Permission (T),
3730 Children_Permission => P);
3733 Free_Perm_Tree_Children (T);
3735 end Set_Perm_Extensions;
3737 ------------------------------
3738 -- Set_Perm_Prefixes --
3739 ------------------------------
3741 function Set_Perm_Prefixes
3743 New_Perm : Perm_Kind)
3744 return Perm_Tree_Access
3752 | N_Defining_Identifier
3754 if Nkind (N) = N_Defining_Identifier
3755 and then New_Perm = Borrowed
3757 raise Program_Error;
3762 C : Perm_Tree_Access;
3765 if Nkind (N) = N_Defining_Identifier then
3771 C := Get (Current_Perm_Env, Unique_Entity (P));
3772 pragma Assert (C /= null);
3774 -- Setting the initialization map to True, so that this
3775 -- variable cannot be ignored anymore when looking at end
3776 -- of elaboration of package.
3778 Set (Current_Initialization_Map, Unique_Entity (P), True);
3779 if New_Perm = Observed
3783 -- No null possible here, there are no parents for the path.
3784 -- This means we are using a global variable without adding
3785 -- it in environment with a global aspect.
3787 Illegal_Global_Usage (N);
3790 C.all.Tree.Permission := New_Perm;
3794 when N_Type_Conversion
3795 | N_Unchecked_Type_Conversion
3796 | N_Qualified_Expression
3798 return Set_Perm_Prefixes (Expression (N), New_Perm);
3800 when N_Parameter_Specification =>
3801 raise Program_Error;
3803 -- We set the permission tree of its prefix, and then we extract
3804 -- our subtree from the returned pointer and assign an adequate
3805 -- permission to it, if unfolded. If folded, we unroll the tree
3808 when N_Selected_Component =>
3810 C : constant Perm_Tree_Access :=
3811 Set_Perm_Prefixes (Prefix (N), New_Perm);
3816 -- We went through a function call, do nothing
3821 pragma Assert (Kind (C) = Entire_Object
3822 or else Kind (C) = Record_Component);
3824 if Kind (C) = Record_Component then
3825 -- The tree is unfolded. We just modify the permission and
3826 -- return the record subtree.
3829 Selected_Component : constant Entity_Id :=
3830 Entity (Selector_Name (N));
3832 Selected_C : Perm_Tree_Access :=
3834 (Component (C), Selected_Component);
3837 if Selected_C = null then
3838 Selected_C := Other_Components (C);
3841 pragma Assert (Selected_C /= null);
3842 Selected_C.all.Tree.Permission := New_Perm;
3846 elsif Kind (C) = Entire_Object then
3848 -- Expand the tree. Replace the node with
3849 -- Record_Component.
3853 -- Create an empty hash table
3855 Hashtbl : Perm_Tree_Maps.Instance;
3857 -- We create the unrolled nodes, that will all have same
3858 -- permission than parent.
3860 Son : Perm_Tree_Access;
3861 Children_Perm : constant Perm_Kind :=
3862 Children_Permission (C);
3865 -- We change the current node from Entire_Object to
3866 -- Record_Component with same permission and an empty
3867 -- hash table as component list.
3870 (Kind => Record_Component,
3871 Is_Node_Deep => Is_Node_Deep (C),
3872 Permission => Permission (C),
3873 Component => Hashtbl,
3875 new Perm_Tree_Wrapper'
3877 (Kind
=> Entire_Object
,
3878 Is_Node_Deep
=> True,
3879 Permission
=> Children_Perm
,
3880 Children_Permission
=> Children_Perm
)
3883 -- We fill the hash table with all sons of the record,
3884 -- with basic Entire_Objects nodes.
3886 Elem
:= First_Component_Or_Discriminant
3887 (Etype
(Prefix
(N
)));
3889 while Present
(Elem
) loop
3890 Son
:= new Perm_Tree_Wrapper
'
3892 (Kind => Entire_Object,
3893 Is_Node_Deep => Is_Deep (Etype (Elem)),
3894 Permission => Children_Perm,
3895 Children_Permission => Children_Perm));
3897 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
3898 Next_Component_Or_Discriminant (Elem);
3900 -- Now we set the right field to Borrowed, and then we
3901 -- return the tree to the sons, so that the recursion can
3905 Selected_Component : constant Entity_Id :=
3906 Entity (Selector_Name (N));
3907 Selected_C : Perm_Tree_Access :=
3909 (Component (C), Selected_Component);
3912 if Selected_C = null then
3913 Selected_C := Other_Components (C);
3916 pragma Assert (Selected_C /= null);
3917 Selected_C.all.Tree.Permission := New_Perm;
3922 raise Program_Error;
3926 -- We set the permission tree of its prefix, and then we extract
3927 -- from the returned pointer the subtree and assign an adequate
3928 -- permission to it, if unfolded. If folded, we unroll the tree in
3931 when N_Indexed_Component
3935 C : constant Perm_Tree_Access :=
3936 Set_Perm_Prefixes (Prefix (N), New_Perm);
3941 -- We went through a function call, do nothing
3946 pragma Assert (Kind (C) = Entire_Object
3947 or else Kind (C) = Array_Component);
3949 if Kind (C) = Array_Component then
3951 -- The tree is unfolded. We just modify the permission and
3952 -- return the elem subtree.
3954 pragma Assert (Get_Elem (C) /= null);
3955 C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
3956 return Get_Elem (C);
3958 elsif Kind (C) = Entire_Object then
3960 -- Expand the tree. Replace node with Array_Component.
3962 Son : Perm_Tree_Access;
3965 Son := new Perm_Tree_Wrapper'
3967 (Kind
=> Entire_Object
,
3968 Is_Node_Deep
=> Is_Node_Deep
(C
),
3969 Permission
=> New_Perm
,
3970 Children_Permission
=> Children_Permission
(C
)));
3972 -- Children_Permission => Children_Permission (C)
3973 -- this line should be checked maybe New_Perm
3974 -- instead of Children_Permission (C)
3976 -- We change the current node from Entire_Object
3977 -- to Array_Component with same permission and the
3978 -- previously defined son.
3980 C
.all.Tree
:= (Kind
=> Array_Component
,
3981 Is_Node_Deep
=> Is_Node_Deep
(C
),
3982 Permission
=> New_Perm
,
3984 return Get_Elem
(C
);
3987 raise Program_Error
;
3991 -- We set the permission tree of its prefix, and then we extract
3992 -- from the returned pointer the subtree and assign an adequate
3993 -- permission to it, if unfolded. If folded, we unroll the tree
3996 when N_Explicit_Dereference
=>
3998 C
: constant Perm_Tree_Access
:=
3999 Set_Perm_Prefixes
(Prefix
(N
), New_Perm
);
4004 -- We went through a function call. Do nothing.
4009 pragma Assert
(Kind
(C
) = Entire_Object
4010 or else Kind
(C
) = Reference
);
4012 if Kind
(C
) = Reference
then
4014 -- The tree is unfolded. We just modify the permission and
4015 -- return the elem subtree.
4017 pragma Assert
(Get_All
(C
) /= null);
4018 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= New_Perm
;
4021 elsif Kind
(C
) = Entire_Object
then
4023 -- Expand the tree. Replace the node with Reference.
4025 Son
: Perm_Tree_Access
;
4028 Son
:= new Perm_Tree_Wrapper
'
4030 (Kind => Entire_Object,
4031 Is_Node_Deep => Is_Deep (Etype (N)),
4032 Permission => New_Perm,
4033 Children_Permission => Children_Permission (C)));
4035 -- We change the current node from Entire_Object to
4036 -- Reference with Borrowed and the previous son.
4038 pragma Assert (Is_Node_Deep (C));
4039 C.all.Tree := (Kind => Reference,
4040 Is_Node_Deep => Is_Node_Deep (C),
4041 Permission => New_Perm,
4047 raise Program_Error;
4051 when N_Function_Call =>
4055 raise Program_Error;
4057 end Set_Perm_Prefixes;
4059 ------------------------------
4060 -- Set_Perm_Prefixes_Borrow --
4061 ------------------------------
4063 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
4066 pragma Assert (Current_Checking_Mode = Borrow);
4073 P : constant Node_Id := Entity (N);
4074 C : constant Perm_Tree_Access :=
4075 Get (Current_Perm_Env, Unique_Entity (P));
4076 pragma Assert (C /= null);
4079 -- Setting the initialization map to True, so that this
4080 -- variable cannot be ignored anymore when looking at end
4081 -- of elaboration of package.
4083 Set (Current_Initialization_Map, Unique_Entity (P), True);
4084 C.all.Tree.Permission := Borrowed;
4088 when N_Type_Conversion
4089 | N_Unchecked_Type_Conversion
4090 | N_Qualified_Expression
4092 return Set_Perm_Prefixes_Borrow (Expression (N));
4094 when N_Parameter_Specification
4095 | N_Defining_Identifier
4097 raise Program_Error;
4099 -- We set the permission tree of its prefix, and then we extract
4100 -- our subtree from the returned pointer and assign an adequate
4101 -- permission to it, if unfolded. If folded, we unroll the tree
4104 when N_Selected_Component =>
4106 C : constant Perm_Tree_Access :=
4107 Set_Perm_Prefixes_Borrow (Prefix (N));
4112 -- We went through a function call, do nothing
4117 -- The permission of the returned node should be No
4119 pragma Assert (Permission (C) = Borrowed);
4120 pragma Assert (Kind (C) = Entire_Object
4121 or else Kind (C) = Record_Component);
4123 if Kind (C) = Record_Component then
4125 -- The tree is unfolded. We just modify the permission and
4126 -- return the record subtree.
4129 Selected_Component : constant Entity_Id :=
4130 Entity (Selector_Name (N));
4131 Selected_C : Perm_Tree_Access :=
4133 (Component (C), Selected_Component);
4136 if Selected_C = null then
4137 Selected_C := Other_Components (C);
4140 pragma Assert (Selected_C /= null);
4141 Selected_C.all.Tree.Permission := Borrowed;
4145 elsif Kind (C) = Entire_Object then
4147 -- Expand the tree. Replace the node with
4148 -- Record_Component.
4152 -- Create an empty hash table
4154 Hashtbl : Perm_Tree_Maps.Instance;
4156 -- We create the unrolled nodes, that will all have same
4157 -- permission than parent.
4159 Son : Perm_Tree_Access;
4160 ChildrenPerm : constant Perm_Kind :=
4161 Children_Permission (C);
4164 -- We change the current node from Entire_Object to
4165 -- Record_Component with same permission and an empty
4166 -- hash table as component list.
4169 (Kind => Record_Component,
4170 Is_Node_Deep => Is_Node_Deep (C),
4171 Permission => Permission (C),
4172 Component => Hashtbl,
4174 new Perm_Tree_Wrapper'
4176 (Kind
=> Entire_Object
,
4177 Is_Node_Deep
=> True,
4178 Permission
=> ChildrenPerm
,
4179 Children_Permission
=> ChildrenPerm
)
4182 -- We fill the hash table with all sons of the record,
4183 -- with basic Entire_Objects nodes.
4185 Elem
:= First_Component_Or_Discriminant
4186 (Etype
(Prefix
(N
)));
4188 while Present
(Elem
) loop
4189 Son
:= new Perm_Tree_Wrapper
'
4191 (Kind => Entire_Object,
4192 Is_Node_Deep => Is_Deep (Etype (Elem)),
4193 Permission => ChildrenPerm,
4194 Children_Permission => ChildrenPerm));
4195 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
4196 Next_Component_Or_Discriminant (Elem);
4199 -- Now we set the right field to Borrowed, and then we
4200 -- return the tree to the sons, so that the recursion can
4204 Selected_Component : constant Entity_Id :=
4205 Entity (Selector_Name (N));
4206 Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
4207 (Component (C), Selected_Component);
4210 if Selected_C = null then
4211 Selected_C := Other_Components (C);
4214 pragma Assert (Selected_C /= null);
4215 Selected_C.all.Tree.Permission := Borrowed;
4221 raise Program_Error;
4225 -- We set the permission tree of its prefix, and then we extract
4226 -- from the returned pointer the subtree and assign an adequate
4227 -- permission to it, if unfolded. If folded, we unroll the tree in
4230 when N_Indexed_Component
4234 C : constant Perm_Tree_Access :=
4235 Set_Perm_Prefixes_Borrow (Prefix (N));
4240 -- We went through a function call, do nothing
4245 pragma Assert (Permission (C) = Borrowed);
4246 pragma Assert (Kind (C) = Entire_Object
4247 or else Kind (C) = Array_Component);
4249 if Kind (C) = Array_Component then
4251 -- The tree is unfolded. We just modify the permission and
4252 -- return the elem subtree.
4254 pragma Assert (Get_Elem (C) /= null);
4255 C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed;
4256 return Get_Elem (C);
4258 elsif Kind (C) = Entire_Object then
4260 -- Expand the tree. Replace node with Array_Component.
4262 Son : Perm_Tree_Access;
4265 Son := new Perm_Tree_Wrapper'
4267 (Kind
=> Entire_Object
,
4268 Is_Node_Deep
=> Is_Node_Deep
(C
),
4269 Permission
=> Borrowed
,
4270 Children_Permission
=> Children_Permission
(C
)));
4272 -- We change the current node from Entire_Object
4273 -- to Array_Component with same permission and the
4274 -- previously defined son.
4276 C
.all.Tree
:= (Kind
=> Array_Component
,
4277 Is_Node_Deep
=> Is_Node_Deep
(C
),
4278 Permission
=> Borrowed
,
4280 return Get_Elem
(C
);
4284 raise Program_Error
;
4288 -- We set the permission tree of its prefix, and then we extract
4289 -- from the returned pointer the subtree and assign an adequate
4290 -- permission to it, if unfolded. If folded, we unroll the tree
4293 when N_Explicit_Dereference
=>
4295 C
: constant Perm_Tree_Access
:=
4296 Set_Perm_Prefixes_Borrow
(Prefix
(N
));
4301 -- We went through a function call. Do nothing.
4306 -- The permission of the returned node should be No
4308 pragma Assert
(Permission
(C
) = Borrowed
);
4309 pragma Assert
(Kind
(C
) = Entire_Object
4310 or else Kind
(C
) = Reference
);
4312 if Kind
(C
) = Reference
then
4314 -- The tree is unfolded. We just modify the permission and
4315 -- return the elem subtree.
4317 pragma Assert
(Get_All
(C
) /= null);
4318 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= Borrowed
;
4321 elsif Kind
(C
) = Entire_Object
then
4323 -- Expand the tree. Replace the node with Reference.
4325 Son
: Perm_Tree_Access
;
4328 Son
:= new Perm_Tree_Wrapper
'
4330 (Kind => Entire_Object,
4331 Is_Node_Deep => Is_Deep (Etype (N)),
4332 Permission => Borrowed,
4333 Children_Permission => Children_Permission (C)));
4335 -- We change the current node from Entire_Object to
4336 -- Reference with Borrowed and the previous son.
4338 pragma Assert (Is_Node_Deep (C));
4339 C.all.Tree := (Kind => Reference,
4340 Is_Node_Deep => Is_Node_Deep (C),
4341 Permission => Borrowed,
4347 raise Program_Error;
4351 when N_Function_Call =>
4355 raise Program_Error;
4357 end Set_Perm_Prefixes_Borrow;
4363 procedure Setup_Globals (Subp : Entity_Id) is
4364 procedure Setup_Globals_From_List
4365 (First_Item : Node_Id;
4366 Kind : Formal_Kind);
4367 -- Set up global items from the list starting at Item
4369 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
4370 -- Set up global items for the mode Global_Mode
4372 -----------------------------
4373 -- Setup_Globals_From_List --
4374 -----------------------------
4376 procedure Setup_Globals_From_List
4377 (First_Item : Node_Id;
4380 Item : Node_Id := First_Item;
4384 while Present (Item) loop
4387 -- Ignore abstract states, which play no role in pointer aliasing
4389 if Ekind (E) = E_Abstract_State then
4392 Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
4396 end Setup_Globals_From_List;
4398 ---------------------------
4399 -- Setup_Globals_Of_Mode --
4400 ---------------------------
4402 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
4410 Kind := E_In_Parameter;
4413 Kind := E_Out_Parameter;
4416 Kind := E_In_Out_Parameter;
4419 raise Program_Error;
4422 -- Set up both global items from Global and Refined_Global pragmas
4424 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
4425 Setup_Globals_From_List
4426 (First_Global (Subp, Global_Mode, Refined => True), Kind);
4427 end Setup_Globals_Of_Mode;
4429 -- Start of processing for Setup_Globals
4432 Setup_Globals_Of_Mode (Name_Proof_In);
4433 Setup_Globals_Of_Mode (Name_Input);
4434 Setup_Globals_Of_Mode (Name_Output);
4435 Setup_Globals_Of_Mode (Name_In_Out);
4438 -------------------------------
4439 -- Setup_Parameter_Or_Global --
4440 -------------------------------
4442 procedure Setup_Parameter_Or_Global
4445 Global_Var : Boolean)
4447 Elem : Perm_Tree_Access;
4450 Elem := new Perm_Tree_Wrapper'
4452 (Kind
=> Entire_Object
,
4453 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
4454 Permission
=> Unrestricted
,
4455 Children_Permission
=> Unrestricted
));
4459 -- All out and in out parameters are considered to be unrestricted.
4460 -- They are whether borrowed or moved. Ada Rules would restrict
4461 -- these permissions further. For example an in parameter cannot
4464 -- In the following we deal with in parameters that can be observed.
4465 -- We only consider the observing cases.
4467 when E_In_Parameter
=>
4469 -- Handling global variables as in parameters here
4470 -- Remove the following condition once decided how globals
4471 -- should be considered.
4473 if not Global_Var
then
4474 if (Is_Access_Type
(Etype
(Id
))
4475 and then Is_Access_Constant
(Etype
(Id
))
4476 and then Is_Anonymous_Access_Type
(Etype
(Id
)))
4478 (not Is_Access_Type
(Etype
(Id
))
4479 and then Is_Deep
(Etype
(Id
))
4480 and then not Is_Anonymous_Access_Type
(Etype
(Id
)))
4482 Elem
.all.Tree
.Permission
:= Observed
;
4483 Elem
.all.Tree
.Children_Permission
:= Observed
;
4486 Elem
.all.Tree
.Permission
:= Unrestricted
;
4487 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4491 Elem
.all.Tree
.Permission
:= Observed
;
4492 Elem
.all.Tree
.Children_Permission
:= Observed
;
4495 -- When out or in/out formal or global parameters, we set them to
4496 -- the Unrestricted state. "We want to be able to assume that all
4497 -- relevant writable globals are unrestricted when a subprogram
4498 -- starts executing". Formal parameters of mode out or in/out
4499 -- are whether Borrowers or the targets of a move operation:
4500 -- they start theirs lives in the subprogram as Unrestricted.
4503 Elem
.all.Tree
.Permission
:= Unrestricted
;
4504 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4507 Set
(Current_Perm_Env
, Id
, Elem
);
4508 end Setup_Parameter_Or_Global
;
4510 ----------------------
4511 -- Setup_Parameters --
4512 ----------------------
4514 procedure Setup_Parameters
(Subp
: Entity_Id
) is Formal
: Entity_Id
;
4516 Formal
:= First_Formal
(Subp
);
4517 while Present
(Formal
) loop
4518 Setup_Parameter_Or_Global
4519 (Formal
, Ekind
(Formal
), Global_Var
=> False);
4520 Next_Formal
(Formal
);
4522 end Setup_Parameters
;
4524 -------------------------------
4525 -- Has_Ownership_Aspect_True --
4526 -------------------------------
4528 function Has_Ownership_Aspect_True
4534 case Ekind
(Etype
(N
)) is
4536 if Ekind
(Etype
(N
)) = E_General_Access_Type
then
4537 Error_Msg_NE
(Msg
& " & not allowed " &
4538 "(Named General Access type)", N
, N
);
4549 Com_Ty
: constant Node_Id
:= Component_Type
(Etype
(N
));
4550 Ret
: Boolean := Has_Ownership_Aspect_True
(Com_Ty
, "");
4553 if Nkind
(Parent
(N
)) = N_Full_Type_Declaration
and
4554 Is_Anonymous_Access_Type
(Com_Ty
)
4560 Error_Msg_NE
(Msg
& " & not allowed "
4561 & "(Components of Named General Access type or"
4562 & " Anonymous type)", N
, N
);
4567 -- ??? What about hidden components
4574 Elmt_T_Perm
: Boolean := True;
4575 Elmt_Perm
, Elmt_Anonym
: Boolean;
4578 Elmt
:= First_Component_Or_Discriminant
(Etype
(N
));
4579 while Present
(Elmt
) loop
4580 Elmt_Perm
:= Has_Ownership_Aspect_True
(Elmt
,
4581 "type of component");
4582 Elmt_Anonym
:= Is_Anonymous_Access_Type
(Etype
(Elmt
));
4585 ("type of component & not allowed"
4586 & " (Components of Anonymous type)", Elmt
, Elmt
);
4588 Elmt_T_Perm
:= Elmt_T_Perm
and Elmt_Perm
and not Elmt_Anonym
;
4589 Next_Component_Or_Discriminant
(Elmt
);
4591 if not Elmt_T_Perm
then
4593 (Msg
& " & not allowed (One or "
4594 & "more components have Ownership Aspect False)",
4604 end Has_Ownership_Aspect_True
;