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
511 -- Regular moving semantics. Checks that paths have Unrestricted
512 -- permission. After moving a path, the permission of both it and
513 -- its extensions are set to Unrestricted.
516 -- Used for the target of an assignment, or an actual parameter with
517 -- mode OUT. Checks that paths have Unrestricted permission. After
518 -- assigning to a path, its permission is set to Unrestricted.
521 -- Used for the source of an assignement when initializes a stand alone
522 -- object of anonymous type, constant, or IN parameter and also OUT
523 -- or IN OUT composite object.
524 -- In the borrowed state, the access object is completely "dead".
527 -- Used for actual IN parameters of a scalar type. Checks that paths
528 -- have Read_Perm permission. After checking a path, its permission
529 -- is set to Observed.
531 -- Also used for formal IN parameters
535 type Result_Kind is (Folded, Unfolded, Function_Call);
536 -- The type declaration to discriminate in the Perm_Or_Tree type
538 -- The result type of the function Get_Perm_Or_Tree. This returns either a
539 -- tree when it found the appropriate tree, or a permission when the search
540 -- finds a leaf and the subtree we are looking for is folded. In the last
541 -- case, we return instead the Children_Permission field of the leaf.
543 type Perm_Or_Tree (R : Result_Kind) is record
545 when Folded => Found_Permission : Perm_Kind;
546 when Unfolded => Tree_Access : Perm_Tree_Access;
547 when Function_Call => null;
551 -----------------------
552 -- Local subprograms --
553 -----------------------
555 -- Checking proceduress for safe pointer usage. These procedures traverse
556 -- the AST, check nodes for correct permissions according to SPARK RM
557 -- 6.4.2, and update permissions depending on the node kind.
559 procedure Check_Call_Statement (Call : Node_Id);
561 procedure Check_Callable_Body (Body_N : Node_Id);
562 -- We are not in End_Of_Callee mode, hence we will save the environment
563 -- and start from a new one. We will add in the environment all formal
564 -- parameters as well as global used during the subprogram, with the
565 -- appropriate permissions (unrestricted for borrowed and moved, observed
566 -- for observed names).
568 procedure Check_Declaration (Decl : Node_Id);
570 procedure Check_Expression (Expr : Node_Id);
572 procedure Check_Globals (N : Node_Id);
573 -- This procedure takes a global pragma and checks it
575 procedure Check_List (L : List_Id);
576 -- Calls Check_Node on each element of the list
578 procedure Check_Loop_Statement (Loop_N : Node_Id);
580 procedure Check_Node (N : Node_Id);
581 -- Main traversal procedure to check safe pointer usage. This procedure is
582 -- mutually recursive with the specialized procedures that follow.
584 procedure Check_Package_Body (Pack : Node_Id);
586 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id);
587 -- This procedure takes a formal and an actual parameter and checks the
588 -- permission of every in-mode parameter. This includes Observing and
591 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
592 -- This procedure takes a formal and an actual parameter and checks the
593 -- state of every out-mode and in out-mode parameter. This includes
594 -- Moving and Borrowing.
596 procedure Check_Statement (Stmt : Node_Id);
598 function Get_Perm (N : Node_Id) return Perm_Kind;
599 -- The function that takes a name as input and returns a permission
602 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
603 -- This function gets a Node_Id and looks recursively to find the
604 -- appropriate subtree for that Node_Id. If the tree is folded on
605 -- that node, then it returns the permission given at the right level.
607 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
608 -- This function gets a Node_Id and looks recursively to find the
609 -- appropriate subtree for that Node_Id. If the tree is folded, then
610 -- it unrolls the tree up to the appropriate level.
612 procedure Hp (P : Perm_Env);
613 -- A procedure that outputs the hash table. This function is used only in
614 -- the debugger to look into a hash table.
615 pragma Unreferenced (Hp);
617 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
618 pragma No_Return (Illegal_Global_Usage);
619 -- A procedure that is called when deep globals or aliased globals are used
620 -- without any global aspect.
622 function Is_Deep (E : Entity_Id) return Boolean;
623 -- A function that can tell if a type is deep or not. Returns true if the
624 -- type passed as argument is deep.
629 Found_Perm : Perm_Kind);
630 -- A procedure that is called when the permissions found contradict the
631 -- rules established by the RM. This function is called with the node, its
632 -- entity and the permission that was expected, and adds an error message
633 -- with the appropriate values.
635 procedure Perm_Error_Subprogram_End
639 Found_Perm : Perm_Kind);
640 -- A procedure that is called when the permissions found contradict the
641 -- rules established by the RM at the end of subprograms. This function
642 -- is called with the node, its entity, the node of the returning function
643 -- and the permission that was expected, and adds an error message with the
644 -- appropriate values.
646 procedure Process_Path (N : Node_Id);
648 procedure Return_Declarations (L : List_Id);
649 -- Check correct permissions on every declared object at the end of a
650 -- callee. Used at the end of the body of a callable entity. Checks that
651 -- paths of all borrowed formal parameters and global have Unrestricted
654 procedure Return_Globals (Subp : Entity_Id);
655 -- Takes a subprogram as input, and checks that all borrowed global items
656 -- of the subprogram indeed have RW permission at the end of the subprogram
659 procedure Return_The_Global
663 -- Auxiliary procedure to Return_Globals
664 -- There is no need to return parameters because they will be reassigned
665 -- their state once the subprogram returns. Local variables that have
666 -- borrowed, observed, or moved an actual parameter go out of the scope.
668 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
669 -- This procedure takes an access to a permission tree and modifies the
670 -- tree so that any strict extensions of the given tree become of the
671 -- access specified by parameter P.
673 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
674 -- This function modifies the permissions of a given node_id in the
675 -- permission environment as well as in all the prefixes of the path,
676 -- given that the path is borrowed with mode out.
678 function Set_Perm_Prefixes
680 New_Perm : Perm_Kind)
681 return Perm_Tree_Access;
682 -- This function sets the permissions of a given node_id in the
683 -- permission environment as well as in all the prefixes of the path
684 -- to the one given in parameter (P).
686 procedure Setup_Globals (Subp : Entity_Id);
687 -- Takes a subprogram as input, and sets up the environment by adding
688 -- global items with appropriate permissions.
690 procedure Setup_Parameter_Or_Global
693 Global_Var : Boolean);
694 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
696 procedure Setup_Parameters (Subp : Entity_Id);
697 -- Takes a subprogram as input, and sets up the environment by adding
698 -- formal parameters with appropriate permissions.
700 function Has_Ownership_Aspect_True
704 -- Takes a node as an input, and finds out whether it has ownership aspect
705 -- True or False. This function is recursive whenever the node has a
706 -- composite type. Access-to-objects have ownership aspect False if they
707 -- have a general access type.
709 ----------------------
710 -- Global Variables --
711 ----------------------
713 Current_Perm_Env : Perm_Env;
714 -- The permission environment that is used for the analysis. This
715 -- environment can be saved, modified, reinitialized, but should be the
716 -- only one valid from which to extract the permissions of the paths in
717 -- scope. The analysis ensures at each point that this variables contains
718 -- a valid permission environment with all bindings in scope.
720 Current_Checking_Mode : Checking_Mode := Read;
721 -- The current analysis mode. This global variable indicates at each point
722 -- of the analysis whether the node being analyzed is moved, borrowed,
723 -- assigned, read, ... The full list of possible values can be found in
724 -- the declaration of type Checking_Mode.
726 Current_Loops_Envs : Env_Backups;
727 -- This variable contains saves of permission environments at each loop the
728 -- analysis entered. Each saved environment can be reached with the label
731 Current_Loops_Accumulators : Env_Backups;
732 -- This variable contains the environments used as accumulators for loops,
733 -- that consist of the merge of all environments at each exit point of
734 -- the loop (which can also be the entry point of the loop in the case of
735 -- non-infinite loops), each of them reachable from the label of the loop.
736 -- We require that the environment stored in the accumulator be less
737 -- restrictive than the saved environment at the beginning of the loop, and
738 -- the permission environment after the loop is equal to the accumulator.
740 Current_Initialization_Map : Initialization_Map;
741 -- This variable contains a map that binds each variable of the analyzed
742 -- source code to a boolean that becomes true whenever the variable is used
743 -- after declaration. Hence we can exclude from analysis variables that
744 -- are just declared and never accessed, typically at package declaration.
746 --------------------------
747 -- Check_Call_Statement --
748 --------------------------
750 procedure Check_Call_Statement (Call : Node_Id) is
751 Saved_Env : Perm_Env;
753 procedure Iterate_Call_In is new
754 Iterate_Call_Parameters (Check_Param_In);
755 procedure Iterate_Call_Out is new
756 Iterate_Call_Parameters (Check_Param_Out);
759 -- Save environment, so that the modifications done by analyzing the
760 -- parameters are not kept at the end of the call.
762 Copy_Env (Current_Perm_Env, Saved_Env);
764 -- We first check the globals then parameters to handle the
765 -- No_Parameter_Aliasing Restriction. An out or in-out global is
766 -- considered as borrowing while a parameter with the same mode is
767 -- a move. This order disallow passing a part of a variable to a
768 -- subprogram if it is referenced as a global by the callable (when
770 -- For paremeters, we fisrt check in parameters and then the out ones.
771 -- This is to avoid Observing or Borrowing objects that are already
772 -- moved. This order is not mandatory but allows to catch runtime
773 -- errors like null pointer dereferencement at the analysis time.
775 Current_Checking_Mode := Read;
776 Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
777 Iterate_Call_In (Call);
778 Iterate_Call_Out (Call);
780 -- Restore environment, because after borrowing/observing actual
781 -- parameters, they get their permission reverted to the ones before
784 Free_Env (Current_Perm_Env);
785 Copy_Env (Saved_Env, Current_Perm_Env);
786 Free_Env (Saved_Env);
787 end Check_Call_Statement;
789 -------------------------
790 -- Check_Callable_Body --
791 -------------------------
793 procedure Check_Callable_Body (Body_N : Node_Id) is
795 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
796 Saved_Env : Perm_Env;
797 Saved_Init_Map : Initialization_Map;
799 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
800 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
803 -- Check if SPARK pragma is not set to Off
805 if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
806 if Get_SPARK_Mode_From_Annotation
807 (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
815 -- Save environment and put a new one in place
817 Copy_Env (Current_Perm_Env, Saved_Env);
819 -- Save initialization map
821 Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
822 Current_Checking_Mode := Read;
823 Current_Perm_Env := New_Env;
825 -- Add formals and globals to the environment with adequate permissions
827 if Is_Subprogram_Or_Entry (Spec_Id) then
828 Setup_Parameters (Spec_Id);
829 Setup_Globals (Spec_Id);
832 -- Analyze the body of the function
834 Check_List (Declarations (Body_N));
835 Check_Node (Handled_Statement_Sequence (Body_N));
837 -- Check the read-write permissions of borrowed parameters/globals
839 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
840 and then not No_Return (Spec_Id)
842 Return_Globals (Spec_Id);
845 -- Free the environments
847 Free_Env (Current_Perm_Env);
848 Copy_Env (Saved_Env, Current_Perm_Env);
849 Free_Env (Saved_Env);
851 -- Restore initialization map
853 Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
854 Reset (Saved_Init_Map);
856 -- The assignment of all out parameters will be done by caller
858 Current_Checking_Mode := Mode_Before;
859 end Check_Callable_Body;
861 -----------------------
862 -- Check_Declaration --
863 -----------------------
865 procedure Check_Declaration (Decl : Node_Id) is
867 Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
868 Target_Typ : Node_Id renames Etype (Target_Ent);
870 Target_View_Typ : Entity_Id;
872 Check : Boolean := True;
874 if Present (Full_View (Target_Typ)) then
875 Target_View_Typ := Full_View (Target_Typ);
877 Target_View_Typ := Target_Typ;
880 case N_Declaration'(Nkind
(Decl
)) is
881 when N_Full_Type_Declaration
=>
882 if not Has_Ownership_Aspect_True
(Target_Ent
, "type declaration")
887 -- ??? What about component declarations with defaults.
889 when N_Object_Declaration
=>
890 if (Is_Access_Type
(Target_View_Typ
)
891 or else Is_Deep
(Target_Typ
))
892 and then not Has_Ownership_Aspect_True
893 (Target_Ent
, "Object declaration ")
898 if Is_Anonymous_Access_Type
(Target_View_Typ
)
899 and then not Present
(Expression
(Decl
))
902 -- ??? Check the case of default value (AI)
903 -- ??? How an anonymous access type can be with default exp?
905 Error_Msg_NE
("? object declaration & has OAF (Anonymous "
906 & "access-to-object with no initialization)",
909 -- If it it an initialization
911 elsif Present
(Expression
(Decl
)) and Check
then
913 -- Find out the operation to be done on the right-hand side
915 -- Initializing object, access type
917 if Is_Access_Type
(Target_View_Typ
) then
919 -- Initializing object, constant access type
921 if Is_Constant_Object
(Target_Ent
) then
923 -- Initializing object, constant access to variable type
925 if not Is_Access_Constant
(Target_View_Typ
) then
926 Current_Checking_Mode
:= Borrow
;
928 -- Initializing object, constant access to constant type
930 -- Initializing object,
931 -- constant access to constant anonymous type.
933 elsif Is_Anonymous_Access_Type
(Target_View_Typ
) then
935 -- This is an object declaration so the target
936 -- of the assignement is a stand-alone object.
938 Current_Checking_Mode
:= Observe
;
940 -- Initializing object, constant access to constant
944 -- If named then it is a general access type
945 -- Hence, Has_Ownership_Aspec_True is False.
950 -- Initializing object, variable access type
953 -- Initializing object, variable access to variable type
955 if not Is_Access_Constant
(Target_View_Typ
) then
957 -- Initializing object, variable named access to
960 if not Is_Anonymous_Access_Type
(Target_View_Typ
) then
961 Current_Checking_Mode
:= Move
;
963 -- Initializing object, variable anonymous access to
967 -- This is an object declaration so the target
968 -- object of the assignement is a stand-alone
971 Current_Checking_Mode
:= Borrow
;
974 -- Initializing object, variable access to constant type
977 -- Initializing object,
978 -- variable named access to constant type.
980 if not Is_Anonymous_Access_Type
(Target_View_Typ
) then
981 Error_Msg_N
("assignment not allowed, Ownership "
982 & "Aspect False (Anonymous Access "
986 -- Initializing object,
987 -- variable anonymous access to constant type.
990 -- This is an object declaration so the target
991 -- of the assignement is a stand-alone object.
993 Current_Checking_Mode
:= Observe
;
998 -- Initializing object, composite (deep) type
1000 elsif Is_Deep
(Target_Typ
) then
1002 -- Initializing object, constant composite type
1004 if Is_Constant_Object
(Target_Ent
) then
1005 Current_Checking_Mode
:= Observe
;
1007 -- Initializing object, variable composite type
1011 -- Initializing object, variable anonymous composite type
1013 if Nkind
(Object_Definition
(Decl
)) =
1014 N_Constrained_Array_Definition
1016 -- An N_Constrained_Array_Definition is an anonymous
1017 -- array (to be checked). Record types are always
1018 -- named and are considered in the else part.
1022 Com_Ty
: constant Node_Id
:=
1023 Component_Type
(Etype
(Target_Typ
));
1026 if Is_Access_Type
(Com_Ty
) then
1028 -- If components are of anonymous type
1030 if Is_Anonymous_Access_Type
(Com_Ty
) then
1031 if Is_Access_Constant
(Com_Ty
) then
1032 Current_Checking_Mode
:= Observe
;
1035 Current_Checking_Mode
:= Borrow
;
1039 Current_Checking_Mode
:= Move
;
1042 elsif Is_Deep
(Com_Ty
) then
1044 -- This is certainly named so it is a move
1046 Current_Checking_Mode
:= Move
;
1051 Current_Checking_Mode
:= Move
;
1059 Check_Node
(Expression
(Decl
));
1062 -- If lhs is not a pointer, we still give it the unrestricted
1063 -- state which is useless but not harmful.
1066 Elem
: Perm_Tree_Access
;
1067 Deep
: constant Boolean := Is_Deep
(Target_Typ
);
1070 -- Note that all declared variables are set to the unrestricted
1073 -- If variables are not initialized:
1074 -- unrestricted to every declared object.
1079 -- The assignement R := S is not allowed in the new rules
1080 -- if R is not unrestricted.
1082 -- If variables are initialized:
1083 -- If it is a move, then the target is unrestricted
1084 -- If it is a borrow, then the target is unrestricted
1085 -- If it is an observe, then the target should be observed
1087 if Current_Checking_Mode
= Observe
then
1088 Elem
:= new Perm_Tree_Wrapper
'
1090 (Kind => Entire_Object,
1091 Is_Node_Deep => Deep,
1092 Permission => Observed,
1093 Children_Permission => Observed));
1095 Elem := new Perm_Tree_Wrapper'
1097 (Kind
=> Entire_Object
,
1098 Is_Node_Deep
=> Deep
,
1099 Permission
=> Unrestricted
,
1100 Children_Permission
=> Unrestricted
));
1103 -- Create new tree for defining identifier
1105 Set
(Current_Perm_Env
,
1106 Unique_Entity
(Defining_Identifier
(Decl
)),
1108 pragma Assert
(Get_First
(Current_Perm_Env
) /= null);
1111 when N_Subtype_Declaration
=>
1112 Check_Node
(Subtype_Indication
(Decl
));
1114 when N_Iterator_Specification
=>
1117 when N_Loop_Parameter_Specification
=>
1120 -- Checking should not be called directly on these nodes
1122 when N_Function_Specification
1123 | N_Entry_Declaration
1124 | N_Procedure_Specification
1125 | N_Component_Declaration
1127 raise Program_Error
;
1129 -- Ignored constructs for pointer checking
1131 when N_Formal_Object_Declaration
1132 | N_Formal_Type_Declaration
1133 | N_Incomplete_Type_Declaration
1134 | N_Private_Extension_Declaration
1135 | N_Private_Type_Declaration
1136 | N_Protected_Type_Declaration
1140 -- The following nodes are rewritten by semantic analysis
1142 when N_Expression_Function
=>
1143 raise Program_Error
;
1145 end Check_Declaration
;
1147 ----------------------
1148 -- Check_Expression --
1149 ----------------------
1151 procedure Check_Expression
(Expr
: Node_Id
) is
1152 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
1154 case N_Subexpr
'(Nkind (Expr)) is
1155 when N_Procedure_Call_Statement
1158 Check_Call_Statement (Expr);
1163 -- Check if identifier is pointing to nothing (On/Off/...)
1165 if not Present (Entity (Expr)) then
1169 -- Do not analyze things that are not of object Kind
1171 if Ekind (Entity (Expr)) not in Object_Kind then
1175 -- Consider as ident
1177 Process_Path (Expr);
1179 -- Switch to read mode and then check the readability of each operand
1182 Current_Checking_Mode := Read;
1183 Check_Node (Left_Opnd (Expr));
1184 Check_Node (Right_Opnd (Expr));
1186 -- Switch to read mode and then check the readability of each operand
1193 Current_Checking_Mode := Read;
1194 Check_Node (Right_Opnd (Expr));
1196 -- Forbid all deep expressions for Attribute ???
1197 -- What about generics? (formal parameters).
1199 when N_Attribute_Reference =>
1200 case Attribute_Name (Expr) is
1202 Error_Msg_N ("access attribute not allowed", Expr);
1207 Current_Checking_Mode := Read;
1208 Check_Node (Prefix (Expr));
1211 Current_Checking_Mode := Read;
1212 Check_Node (Prefix (Expr));
1215 Check_List (Expressions (Expr));
1218 Check_Node (Prefix (Expr));
1220 when Name_SPARK_Mode =>
1224 Current_Checking_Mode := Read;
1225 Check_Node (Prefix (Expr));
1228 Check_List (Expressions (Expr));
1229 Check_Node (Prefix (Expr));
1234 Check_List (Expressions (Expr));
1235 Check_Node (Prefix (Expr));
1238 Current_Checking_Mode := Read;
1239 Check_Node (Prefix (Expr));
1241 -- Any Attribute referring to the underlying memory is ignored
1242 -- in the analysis. This means that taking the address of a
1243 -- variable makes a silent alias that is not rejected by the
1248 | Name_Component_Size
1256 -- Attributes referring to types (get values from types), hence
1257 -- no need to check either for borrows or any loans.
1263 -- Other attributes that fall out of the scope of the analysis
1270 Current_Checking_Mode := Read;
1271 Check_Node (Left_Opnd (Expr));
1272 Check_Node (Right_Opnd (Expr));
1275 Current_Checking_Mode := Read;
1276 Check_Node (Left_Opnd (Expr));
1277 Check_Node (Right_Opnd (Expr));
1279 -- Switch to read mode and then check the readability of each operand
1284 Current_Checking_Mode := Read;
1285 Check_Node (Left_Opnd (Expr));
1286 Check_Node (Right_Opnd (Expr));
1288 -- Check the arguments of the call
1290 when N_Explicit_Dereference =>
1291 Process_Path (Expr);
1293 -- Copy environment, run on each branch, and then merge
1295 when N_If_Expression =>
1297 Saved_Env : Perm_Env;
1299 -- Accumulator for the different branches
1302 Elmt : Node_Id := First (Expressions (Expr));
1305 Current_Checking_Mode := Read;
1307 Current_Checking_Mode := Mode_Before;
1311 Copy_Env (Current_Perm_Env, Saved_Env);
1313 -- Here we have the original env in saved, current with a fresh
1314 -- copy, and new aliased.
1321 -- Here the new_environment contains curr env after then block
1324 -- Restore environment before if
1325 Copy_Env (Current_Perm_Env, New_Env);
1326 Free_Env (Current_Perm_Env);
1327 Copy_Env (Saved_Env, Current_Perm_Env);
1329 -- Here new environment contains the environment after then and
1330 -- current the fresh copy of old one.
1337 Copy_Env (New_Env, Current_Perm_Env);
1339 Free_Env (Saved_Env);
1342 when N_Indexed_Component =>
1343 Process_Path (Expr);
1345 -- Analyze the expression that is getting qualified
1347 when N_Qualified_Expression =>
1348 Check_Node (Expression (Expr));
1350 when N_Quantified_Expression =>
1352 Saved_Env : Perm_Env;
1355 Copy_Env (Current_Perm_Env, Saved_Env);
1356 Current_Checking_Mode := Read;
1357 Check_Node (Iterator_Specification (Expr));
1358 Check_Node (Loop_Parameter_Specification (Expr));
1360 Check_Node (Condition (Expr));
1361 Free_Env (Current_Perm_Env);
1362 Copy_Env (Saved_Env, Current_Perm_Env);
1363 Free_Env (Saved_Env);
1365 -- Analyze the list of associations in the aggregate
1368 Check_List (Expressions (Expr));
1369 Check_List (Component_Associations (Expr));
1372 Check_Node (Expression (Expr));
1374 when N_Case_Expression =>
1376 Saved_Env : Perm_Env;
1378 -- Accumulator for the different branches
1381 Elmt : Node_Id := First (Alternatives (Expr));
1384 Current_Checking_Mode := Read;
1385 Check_Node (Expression (Expr));
1386 Current_Checking_Mode := Mode_Before;
1390 Copy_Env (Current_Perm_Env, Saved_Env);
1392 -- Here we have the original env in saved, current with a fresh
1393 -- copy, and new aliased.
1395 -- First alternative
1399 Copy_Env (Current_Perm_Env, New_Env);
1400 Free_Env (Current_Perm_Env);
1402 -- Other alternatives
1404 while Present (Elmt) loop
1406 -- Restore environment
1408 Copy_Env (Saved_Env, Current_Perm_Env);
1414 Copy_Env (Saved_Env, Current_Perm_Env);
1416 Free_Env (Saved_Env);
1418 -- Analyze the list of associates in the aggregate as well as the
1421 when N_Extension_Aggregate =>
1422 Check_Node (Ancestor_Part (Expr));
1423 Check_List (Expressions (Expr));
1426 Check_Node (Low_Bound (Expr));
1427 Check_Node (High_Bound (Expr));
1429 -- We arrived at a path. Process it.
1431 when N_Selected_Component =>
1432 Process_Path (Expr);
1435 Process_Path (Expr);
1437 when N_Type_Conversion =>
1438 Check_Node (Expression (Expr));
1440 when N_Unchecked_Type_Conversion =>
1441 Check_Node (Expression (Expr));
1443 -- Checking should not be called directly on these nodes
1445 when N_Target_Name =>
1446 raise Program_Error;
1448 -- Unsupported constructs in SPARK
1450 when N_Delta_Aggregate =>
1451 Error_Msg_N ("unsupported construct in SPARK", Expr);
1453 -- Ignored constructs for pointer checking
1455 when N_Character_Literal
1457 | N_Numeric_Or_String_Literal
1459 | N_Raise_Expression
1463 -- The following nodes are never generated in GNATprove mode
1465 when N_Expression_With_Actions
1467 | N_Unchecked_Expression
1469 raise Program_Error;
1471 end Check_Expression;
1477 procedure Check_Globals (N : Node_Id) is
1479 if Nkind (N) = N_Empty then
1484 pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
1485 PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
1486 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1491 procedure Process (Mode : Name_Id; The_Global : Entity_Id);
1492 procedure Process (Mode : Name_Id; The_Global : Node_Id) is
1493 Ident_Elt : constant Entity_Id :=
1494 Unique_Entity (Entity (The_Global));
1495 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1498 if Ekind (Ident_Elt) = E_Abstract_State then
1505 Current_Checking_Mode := Observe;
1506 Check_Node (The_Global);
1511 -- ??? Borrow not Move?
1512 Current_Checking_Mode := Borrow;
1513 Check_Node (The_Global);
1516 raise Program_Error;
1518 Current_Checking_Mode := Mode_Before;
1522 if Nkind (Expression (PAA)) = N_Null then
1525 -- No globals, nothing to do
1529 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1534 Process (Name_Input, Expression (PAA));
1536 elsif Nkind (Expression (PAA)) = N_Aggregate
1537 and then Expressions (Expression (PAA)) /= No_List
1539 -- global => (foo, bar)
1542 RHS := First (Expressions (Expression (PAA)));
1543 while Present (RHS) loop
1548 Process (Name_Input, RHS);
1550 when N_Numeric_Or_String_Literal =>
1551 Process (Name_Input, Original_Node (RHS));
1554 raise Program_Error;
1559 elsif Nkind (Expression (PAA)) = N_Aggregate
1560 and then Component_Associations (Expression (PAA)) /= No_List
1562 -- global => (mode => foo,
1563 -- mode => (bar, baz))
1564 -- A mixture of things
1567 CA : constant List_Id :=
1568 Component_Associations (Expression (PAA));
1571 while Present (Row) loop
1572 pragma Assert (List_Length (Choices (Row)) = 1);
1573 The_Mode := Chars (First (Choices (Row)));
1574 RHS := Expression (Row);
1578 RHS := First (Expressions (RHS));
1579 while Present (RHS) loop
1581 when N_Numeric_Or_String_Literal =>
1582 Process (The_Mode, Original_Node (RHS));
1585 Process (The_Mode, RHS);
1593 Process (The_Mode, RHS);
1598 when N_Numeric_Or_String_Literal =>
1599 Process (The_Mode, Original_Node (RHS));
1602 raise Program_Error;
1609 raise Program_Error;
1618 procedure Check_List (L : List_Id) is
1622 while Present (N) loop
1628 --------------------------
1629 -- Check_Loop_Statement --
1630 --------------------------
1632 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1636 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
1637 Loop_Env : constant Perm_Env_Access := new Perm_Env;
1640 -- Save environment prior to the loop
1642 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
1644 -- Add saved environment to loop environment
1646 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
1648 -- If the loop is not a plain-loop, then it may either never be entered,
1649 -- or it may be exited after a number of iterations. Hence add the
1650 -- current permission environment as the initial loop exit environment.
1651 -- Otherwise, the loop exit environment remains empty until it is
1652 -- populated by analyzing exit statements.
1654 if Present (Iteration_Scheme (Loop_N)) then
1656 Exit_Env : constant Perm_Env_Access := new Perm_Env;
1659 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
1660 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
1666 Check_Node (Iteration_Scheme (Loop_N));
1667 Check_List (Statements (Loop_N));
1669 -- Set environment to the one for exiting the loop
1672 Exit_Env : constant Perm_Env_Access :=
1673 Get (Current_Loops_Accumulators, Loop_Name);
1675 Free_Env (Current_Perm_Env);
1677 -- In the normal case, Exit_Env is not null and we use it. In the
1678 -- degraded case of a plain-loop without exit statements, Exit_Env is
1679 -- null, and we use the initial permission environment at the start
1680 -- of the loop to continue analysis. Any environment would be fine
1681 -- here, since the code after the loop is dead code, but this way we
1682 -- avoid spurious errors by having at least variables in scope inside
1685 if Exit_Env /= null then
1686 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
1687 Free_Env (Loop_Env.all);
1688 Free_Env (Exit_Env.all);
1690 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
1691 Free_Env (Loop_Env.all);
1694 end Check_Loop_Statement;
1700 procedure Check_Node (N : Node_Id) is
1701 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1704 when N_Declaration =>
1705 Check_Declaration (N);
1708 Check_Expression (N);
1710 when N_Subtype_Indication =>
1711 Check_Node (Constraint (N));
1714 Check_Node (Get_Body_From_Stub (N));
1716 when N_Statement_Other_Than_Procedure_Call =>
1717 Check_Statement (N);
1719 when N_Package_Body =>
1720 Check_Package_Body (N);
1722 when N_Subprogram_Body
1726 Check_Callable_Body (N);
1728 when N_Protected_Body =>
1729 Check_List (Declarations (N));
1731 when N_Package_Declaration =>
1733 Spec : constant Node_Id := Specification (N);
1736 Current_Checking_Mode := Read;
1737 Check_List (Visible_Declarations (Spec));
1738 Check_List (Private_Declarations (Spec));
1740 Return_Declarations (Visible_Declarations (Spec));
1741 Return_Declarations (Private_Declarations (Spec));
1744 when N_Iteration_Scheme =>
1745 Current_Checking_Mode := Read;
1746 Check_Node (Condition (N));
1747 Check_Node (Iterator_Specification (N));
1748 Check_Node (Loop_Parameter_Specification (N));
1750 when N_Case_Expression_Alternative =>
1751 Current_Checking_Mode := Read;
1752 Check_List (Discrete_Choices (N));
1753 Current_Checking_Mode := Mode_Before;
1754 Check_Node (Expression (N));
1756 when N_Case_Statement_Alternative =>
1757 Current_Checking_Mode := Read;
1758 Check_List (Discrete_Choices (N));
1759 Current_Checking_Mode := Mode_Before;
1760 Check_List (Statements (N));
1762 when N_Component_Association =>
1763 Check_Node (Expression (N));
1765 when N_Handled_Sequence_Of_Statements =>
1766 Check_List (Statements (N));
1768 when N_Parameter_Association =>
1769 Check_Node (Explicit_Actual_Parameter (N));
1771 when N_Range_Constraint =>
1772 Check_Node (Range_Expression (N));
1774 when N_Index_Or_Discriminant_Constraint =>
1775 Check_List (Constraints (N));
1777 -- Checking should not be called directly on these nodes
1779 when N_Abortable_Part
1780 | N_Accept_Alternative
1781 | N_Access_Definition
1782 | N_Access_Function_Definition
1783 | N_Access_Procedure_Definition
1784 | N_Access_To_Object_Definition
1785 | N_Aspect_Specification
1786 | N_Compilation_Unit
1787 | N_Compilation_Unit_Aux
1788 | N_Component_Clause
1789 | N_Component_Definition
1791 | N_Constrained_Array_Definition
1793 | N_Decimal_Fixed_Point_Definition
1794 | N_Defining_Character_Literal
1795 | N_Defining_Identifier
1796 | N_Defining_Operator_Symbol
1797 | N_Defining_Program_Unit_Name
1798 | N_Delay_Alternative
1799 | N_Derived_Type_Definition
1801 | N_Discriminant_Specification
1803 | N_Entry_Body_Formal_Part
1804 | N_Enumeration_Type_Definition
1805 | N_Entry_Call_Alternative
1806 | N_Entry_Index_Specification
1808 | N_Exception_Handler
1809 | N_Floating_Point_Definition
1810 | N_Formal_Decimal_Fixed_Point_Definition
1811 | N_Formal_Derived_Type_Definition
1812 | N_Formal_Discrete_Type_Definition
1813 | N_Formal_Floating_Point_Definition
1814 | N_Formal_Incomplete_Type_Definition
1815 | N_Formal_Modular_Type_Definition
1816 | N_Formal_Ordinary_Fixed_Point_Definition
1817 | N_Formal_Private_Type_Definition
1818 | N_Formal_Signed_Integer_Type_Definition
1819 | N_Generic_Association
1821 | N_Modular_Type_Definition
1822 | N_Ordinary_Fixed_Point_Definition
1823 | N_Package_Specification
1824 | N_Parameter_Specification
1825 | N_Pragma_Argument_Association
1826 | N_Protected_Definition
1827 | N_Push_Pop_xxx_Label
1828 | N_Real_Range_Specification
1829 | N_Record_Definition
1830 | N_SCIL_Dispatch_Table_Tag_Init
1831 | N_SCIL_Dispatching_Call
1832 | N_SCIL_Membership_Test
1833 | N_Signed_Integer_Type_Definition
1836 | N_Terminate_Alternative
1837 | N_Triggering_Alternative
1838 | N_Unconstrained_Array_Definition
1844 raise Program_Error;
1846 -- Unsupported constructs in SPARK
1848 when N_Iterated_Component_Association =>
1849 Error_Msg_N ("unsupported construct in SPARK", N);
1851 -- Ignored constructs for pointer checking
1853 when N_Abstract_Subprogram_Declaration
1855 | N_Attribute_Definition_Clause
1857 | N_Delta_Constraint
1858 | N_Digits_Constraint
1860 | N_Enumeration_Representation_Clause
1861 | N_Exception_Declaration
1862 | N_Exception_Renaming_Declaration
1863 | N_Formal_Package_Declaration
1864 | N_Formal_Subprogram_Declaration
1866 | N_Freeze_Generic_Entity
1867 | N_Function_Instantiation
1868 | N_Generic_Function_Renaming_Declaration
1869 | N_Generic_Package_Declaration
1870 | N_Generic_Package_Renaming_Declaration
1871 | N_Generic_Procedure_Renaming_Declaration
1872 | N_Generic_Subprogram_Declaration
1873 | N_Implicit_Label_Declaration
1876 | N_Number_Declaration
1877 | N_Object_Renaming_Declaration
1879 | N_Package_Instantiation
1880 | N_Package_Renaming_Declaration
1882 | N_Procedure_Instantiation
1883 | N_Record_Representation_Clause
1884 | N_Subprogram_Declaration
1885 | N_Subprogram_Renaming_Declaration
1886 | N_Task_Type_Declaration
1887 | N_Use_Package_Clause
1890 | N_Validate_Unchecked_Conversion
1891 | N_Variable_Reference_Marker
1892 | N_Discriminant_Association
1894 -- ??? check whether we should do sth special for
1895 -- N_Discriminant_Association, or maybe raise a program error.
1898 -- The following nodes are rewritten by semantic analysis
1900 when N_Single_Protected_Declaration
1901 | N_Single_Task_Declaration
1903 raise Program_Error;
1906 Current_Checking_Mode := Mode_Before;
1909 ------------------------
1910 -- Check_Package_Body --
1911 ------------------------
1913 procedure Check_Package_Body (Pack : Node_Id) is
1914 Saved_Env : Perm_Env;
1918 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
1919 if Get_SPARK_Mode_From_Annotation
1920 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
1928 CorSp := Parent (Corresponding_Spec (Pack));
1929 while Nkind (CorSp) /= N_Package_Specification loop
1930 CorSp := Parent (CorSp);
1933 Check_List (Visible_Declarations (CorSp));
1937 Copy_Env (Current_Perm_Env, Saved_Env);
1938 Check_List (Private_Declarations (CorSp));
1940 -- Set mode to Read, and then analyze declarations and statements
1942 Current_Checking_Mode := Read;
1943 Check_List (Declarations (Pack));
1944 Check_Node (Handled_Statement_Sequence (Pack));
1946 -- Check RW for every stateful variable (i.e. in declarations)
1948 Return_Declarations (Private_Declarations (CorSp));
1949 Return_Declarations (Visible_Declarations (CorSp));
1950 Return_Declarations (Declarations (Pack));
1952 -- Restore previous environment (i.e. delete every nonvisible
1953 -- declaration) from environment.
1955 Free_Env (Current_Perm_Env);
1956 Copy_Env (Saved_Env, Current_Perm_Env);
1957 end Check_Package_Body;
1959 --------------------
1960 -- Check_Param_In --
1961 --------------------
1963 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
1964 Mode : constant Entity_Kind := Ekind (Formal);
1965 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1967 case Formal_Kind'(Mode
) is
1969 -- Formal IN parameter
1971 when E_In_Parameter
=>
1973 -- Formal IN parameter, access type
1975 if Is_Access_Type
(Etype
(Formal
)) then
1977 -- Formal IN parameter, access to variable type
1979 if not Is_Access_Constant
(Etype
(Formal
)) then
1981 -- Formal IN parameter, named/anonymous access-to-variable
1984 -- In SPARK, IN access-to-variable is an observe operation
1985 -- for a function, and a borrow operation for a procedure.
1987 if Ekind
(Scope
(Formal
)) = E_Function
then
1988 Current_Checking_Mode
:= Observe
;
1989 Check_Node
(Actual
);
1991 Current_Checking_Mode
:= Borrow
;
1992 Check_Node
(Actual
);
1995 -- Formal IN parameter, access-to-constant type
1996 -- Formal IN parameter, access-to-named-constant type
1998 elsif not Is_Anonymous_Access_Type
(Etype
(Formal
)) then
1999 Error_Msg_N
("assignment not allowed, Ownership Aspect"
2000 & " False (Named general access type)",
2003 -- Formal IN parameter, access to anonymous constant type
2006 Current_Checking_Mode
:= Observe
;
2007 Check_Node
(Actual
);
2010 -- Formal IN parameter, composite type
2012 elsif Is_Deep
(Etype
(Formal
)) then
2014 -- Composite formal types should be named
2015 -- Formal IN parameter, composite named type
2017 Current_Checking_Mode
:= Observe
;
2018 Check_Node
(Actual
);
2021 when E_Out_Parameter
2022 | E_In_Out_Parameter
2027 Current_Checking_Mode
:= Mode_Before
;
2030 ----------------------
2031 -- Check_Param_Out --
2032 ----------------------
2034 procedure Check_Param_Out
(Formal
: Entity_Id
; Actual
: Node_Id
) is
2035 Mode
: constant Entity_Kind
:= Ekind
(Formal
);
2036 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2039 case Formal_Kind
'(Mode) is
2041 -- Formal OUT/IN OUT parameter
2043 when E_Out_Parameter
2044 | E_In_Out_Parameter
2047 -- Formal OUT/IN OUT parameter, access type
2049 if Is_Access_Type (Etype (Formal)) then
2051 -- Formal OUT/IN OUT parameter, access to variable type
2053 if not Is_Access_Constant (Etype (Formal)) then
2055 -- Cannot have anonymous out access parameter
2056 -- Formal out/in out parameter, access to named variable
2059 Current_Checking_Mode := Move;
2060 Check_Node (Actual);
2062 -- Formal out/in out parameter, access to constant type
2065 Error_Msg_N ("assignment not allowed, Ownership Aspect False"
2066 & " (Named general access type)", Formal);
2070 -- Formal out/in out parameter, composite type
2072 elsif Is_Deep (Etype (Formal)) then
2074 -- Composite formal types should be named
2075 -- Formal out/in out Parameter, Composite Named type.
2077 Current_Checking_Mode := Borrow;
2078 Check_Node (Actual);
2081 when E_In_Parameter =>
2085 Current_Checking_Mode := Mode_Before;
2086 end Check_Param_Out;
2088 -------------------------
2089 -- Check_Safe_Pointers --
2090 -------------------------
2092 procedure Check_Safe_Pointers (N : Node_Id) is
2094 -- Local subprograms
2096 procedure Check_List (L : List_Id);
2097 -- Call the main analysis procedure on each element of the list
2099 procedure Initialize;
2100 -- Initialize global variables before starting the analysis of a body
2106 procedure Check_List (L : List_Id) is
2110 while Present (N) loop
2111 Check_Safe_Pointers (N);
2120 procedure Initialize is
2122 Reset (Current_Loops_Envs);
2123 Reset (Current_Loops_Accumulators);
2124 Reset (Current_Perm_Env);
2125 Reset (Current_Initialization_Map);
2132 -- SPARK_Mode pragma in application
2134 -- Start of processing for Check_Safe_Pointers
2139 when N_Compilation_Unit =>
2140 Check_Safe_Pointers (Unit (N));
2143 | N_Package_Declaration
2146 Prag := SPARK_Pragma (Defining_Entity (N));
2147 if Present (Prag) then
2148 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
2154 elsif Nkind (N) = N_Package_Body then
2155 Check_List (Declarations (N));
2157 elsif Nkind (N) = N_Package_Declaration then
2158 Check_List (Private_Declarations (Specification (N)));
2159 Check_List (Visible_Declarations (Specification (N)));
2165 end Check_Safe_Pointers;
2167 ---------------------
2168 -- Check_Statement --
2169 ---------------------
2171 procedure Check_Statement (Stmt : Node_Id) is
2172 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2173 State_N : Perm_Kind;
2174 Check : Boolean := True;
2176 Ty_St_Name : Node_Id;
2178 function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
2179 -- Return the root of the name given as input
2181 function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
2183 case Nkind (Comp_Stmt) is
2186 => return Comp_Stmt;
2188 when N_Type_Conversion
2189 | N_Unchecked_Type_Conversion
2190 | N_Qualified_Expression
2192 return Get_Root (Expression (Comp_Stmt));
2194 when N_Parameter_Specification =>
2195 return Get_Root (Defining_Identifier (Comp_Stmt));
2197 when N_Selected_Component
2198 | N_Indexed_Component
2200 | N_Explicit_Dereference
2202 return Get_Root (Prefix (Comp_Stmt));
2205 raise Program_Error;
2210 case N_Statement_Other_Than_Procedure_Call'(Nkind
(Stmt
)) is
2211 when N_Entry_Call_Statement
=>
2212 Check_Call_Statement
(Stmt
);
2214 -- Move right-hand side first, and then assign left-hand side
2216 when N_Assignment_Statement
=>
2218 St_Name
:= Name
(Stmt
);
2219 Ty_St_Name
:= Etype
(Name
(Stmt
));
2221 -- Check that is not a *general* access type
2223 if Has_Ownership_Aspect_True
(St_Name
, "assigning to") then
2225 -- Assigning to access type
2227 if Is_Access_Type
(Ty_St_Name
) then
2229 -- Assigning to access to variable type
2231 if not Is_Access_Constant
(Ty_St_Name
) then
2233 -- Assigning to named access to variable type
2235 if not Is_Anonymous_Access_Type
(Ty_St_Name
) then
2236 Current_Checking_Mode
:= Move
;
2238 -- Assigning to anonymous access to variable type
2241 -- Target /= source root
2243 if Nkind_In
(Expression
(Stmt
), N_Allocator
, N_Null
)
2244 or else Entity
(St_Name
) /=
2245 Entity
(Get_Root
(Expression
(Stmt
)))
2247 Error_Msg_N
("assignment not allowed, anonymous "
2248 & "access Object with Different Root",
2252 -- Target = source root
2255 -- Here we do nothing on the source nor on the
2256 -- target. However, we check the the legality rule:
2257 -- "The source shall be an owning access object
2258 -- denoted by a name that is not in the observed
2261 State_N
:= Get_Perm
(Expression
(Stmt
));
2262 if State_N
= Observed
then
2263 Error_Msg_N
("assignment not allowed, Anonymous "
2264 & "access object with the same root"
2265 & " but source Observed", Stmt
);
2271 -- else access-to-constant
2273 -- Assigning to anonymous access-to-constant type
2275 elsif Is_Anonymous_Access_Type
(Ty_St_Name
) then
2277 -- ??? Check the follwing condition. We may have to
2278 -- add that the root is in the observed state too.
2280 State_N
:= Get_Perm
(Expression
(Stmt
));
2281 if State_N
/= Observed
then
2282 Error_Msg_N
("assignment not allowed, anonymous "
2283 & "access-to-constant object not in "
2284 & "the observed state)", Stmt
);
2288 Error_Msg_N
("?here check accessibility level cited in"
2289 & " the second legality rule of assign",
2294 -- Assigning to named access-to-constant type:
2295 -- This case should have been detected when checking
2296 -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
2299 raise Program_Error
;
2302 -- Assigning to composite (deep) type.
2304 elsif Is_Deep
(Ty_St_Name
) then
2305 if Ekind_In
(Ty_St_Name
,
2311 First_Component_Or_Discriminant
(Ty_St_Name
);
2314 while Present
(Elmt
) loop
2315 if Is_Anonymous_Access_Type
(Etype
(Elmt
)) or
2316 Ekind
(Elmt
) = E_General_Access_Type
2318 Error_Msg_N
("assignment not allowed, Ownership "
2319 & "Aspect False (Components have "
2320 & "Ownership Aspect False)", Stmt
);
2325 Next_Component_Or_Discriminant
(Elmt
);
2329 -- Record types are always named so this is a move
2332 Current_Checking_Mode
:= Move
;
2335 elsif Ekind_In
(Ty_St_Name
,
2340 Current_Checking_Mode
:= Move
;
2343 -- Now handle legality rules of using a borrowed, observed,
2344 -- or moved name as a prefix in an assignment.
2347 if Nkind_In
(St_Name
,
2348 N_Attribute_Reference
,
2350 N_Explicit_Dereference
,
2351 N_Indexed_Component
,
2353 N_Selected_Component
,
2357 if Is_Access_Type
(Etype
(Prefix
(St_Name
))) or
2358 Is_Deep
(Etype
(Prefix
(St_Name
)))
2361 -- We set the Check variable to True so that we can
2362 -- Check_Node of the expression and the name first
2363 -- under the assumption of Current_Checking_Mode =
2364 -- Read => nothing to be done for the RHS if the
2365 -- following check on the expression fails, and
2366 -- Current_Checking_Mode := Assign => the name should
2367 -- not be borrowed or observed so that we can use it
2368 -- as a prefix in the target of an assignement.
2370 -- Note that we do not need to check the OA here
2371 -- because we are allowed to read and write "through"
2372 -- an object of OAF (example: traversing a DS).
2378 if Nkind_In
(Expression
(Stmt
),
2379 N_Attribute_Reference
,
2381 N_Explicit_Dereference
,
2382 N_Indexed_Component
,
2384 N_Selected_Component
,
2388 if Is_Access_Type
(Etype
(Prefix
(Expression
(Stmt
))))
2389 or else Is_Deep
(Etype
(Prefix
(Expression
(Stmt
))))
2391 Current_Checking_Mode
:= Observe
;
2398 Check_Node
(Expression
(Stmt
));
2399 Current_Checking_Mode
:= Assign
;
2400 Check_Node
(St_Name
);
2404 when N_Block_Statement
=>
2406 Saved_Env
: Perm_Env
;
2410 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2412 -- Analyze declarations and Handled_Statement_Sequences
2414 Current_Checking_Mode
:= Read
;
2415 Check_List
(Declarations
(Stmt
));
2416 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2418 -- Restore environment
2420 Free_Env
(Current_Perm_Env
);
2421 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2424 when N_Case_Statement
=>
2426 Saved_Env
: Perm_Env
;
2428 -- Accumulator for the different branches
2431 Elmt
: Node_Id
:= First
(Alternatives
(Stmt
));
2434 Current_Checking_Mode
:= Read
;
2435 Check_Node
(Expression
(Stmt
));
2436 Current_Checking_Mode
:= Mode_Before
;
2440 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2442 -- Here we have the original env in saved, current with a fresh
2443 -- copy, and new aliased.
2445 -- First alternative
2449 Copy_Env
(Current_Perm_Env
, New_Env
);
2450 Free_Env
(Current_Perm_Env
);
2452 -- Other alternatives
2454 while Present
(Elmt
) loop
2456 -- Restore environment
2458 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2463 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2465 Free_Env
(Saved_Env
);
2468 when N_Delay_Relative_Statement
=>
2469 Check_Node
(Expression
(Stmt
));
2471 when N_Delay_Until_Statement
=>
2472 Check_Node
(Expression
(Stmt
));
2474 when N_Loop_Statement
=>
2475 Check_Loop_Statement
(Stmt
);
2477 -- If deep type expression, then move, else read
2479 when N_Simple_Return_Statement
=>
2480 case Nkind
(Expression
(Stmt
)) is
2483 -- ??? This does not take into account the fact that
2484 -- a simple return inside an extended return statement
2485 -- applies to the extended return statement.
2486 Subp
: constant Entity_Id
:=
2487 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2489 Return_Globals
(Subp
);
2493 if Is_Deep
(Etype
(Expression
(Stmt
))) then
2494 Current_Checking_Mode
:= Move
;
2500 Check_Node
(Expression
(Stmt
));
2504 when N_Extended_Return_Statement
=>
2505 Check_List
(Return_Object_Declarations
(Stmt
));
2506 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2507 Return_Declarations
(Return_Object_Declarations
(Stmt
));
2509 -- ??? This does not take into account the fact that a simple
2510 -- return inside an extended return statement applies to the
2511 -- extended return statement.
2512 Subp
: constant Entity_Id
:=
2513 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2516 Return_Globals
(Subp
);
2519 -- Nothing to do when exiting a loop. No merge needed
2521 when N_Exit_Statement
=>
2524 -- Copy environment, run on each branch
2526 when N_If_Statement
=>
2528 Saved_Env
: Perm_Env
;
2530 -- Accumulator for the different branches
2535 Check_Node
(Condition
(Stmt
));
2539 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2541 -- Here we have the original env in saved, current with a fresh
2546 Check_List
(Then_Statements
(Stmt
));
2547 Copy_Env
(Current_Perm_Env
, New_Env
);
2548 Free_Env
(Current_Perm_Env
);
2550 -- Here the new_environment contains curr env after then block
2558 Elmt
:= First
(Elsif_Parts
(Stmt
));
2559 while Present
(Elmt
) loop
2561 -- Transfer into accumulator, and restore from save
2563 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2564 Check_Node
(Condition
(Elmt
));
2565 Check_List
(Then_Statements
(Stmt
));
2572 -- Restore environment before if
2574 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2576 -- Here new environment contains the environment after then and
2577 -- current the fresh copy of old one.
2579 Check_List
(Else_Statements
(Stmt
));
2583 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2586 Free_Env
(Saved_Env
);
2589 -- Unsupported constructs in SPARK
2591 when N_Abort_Statement
2592 | N_Accept_Statement
2593 | N_Asynchronous_Select
2595 | N_Conditional_Entry_Call
2597 | N_Requeue_Statement
2598 | N_Selective_Accept
2599 | N_Timed_Entry_Call
2601 Error_Msg_N
("unsupported construct in SPARK", Stmt
);
2603 -- Ignored constructs for pointer checking
2605 when N_Null_Statement
2610 -- The following nodes are never generated in GNATprove mode
2612 when N_Compound_Statement
2615 raise Program_Error
;
2617 end Check_Statement
;
2623 function Get_Perm
(N
: Node_Id
) return Perm_Kind
is
2624 Tree_Or_Perm
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(N
);
2627 case Tree_Or_Perm
.R
is
2629 return Tree_Or_Perm
.Found_Permission
;
2632 pragma Assert
(Tree_Or_Perm
.Tree_Access
/= null);
2633 return Permission
(Tree_Or_Perm
.Tree_Access
);
2635 -- We encoutered a function call, hence the memory area is fresh,
2636 -- which means that the association permission is RW.
2638 when Function_Call
=>
2639 return Unrestricted
;
2643 ----------------------
2644 -- Get_Perm_Or_Tree --
2645 ----------------------
2647 function Get_Perm_Or_Tree
(N
: Node_Id
) return Perm_Or_Tree
is
2651 -- Base identifier. Normally those are the roots of the trees stored
2652 -- in the permission environment.
2654 when N_Defining_Identifier
=>
2655 raise Program_Error
;
2661 P
: constant Entity_Id
:= Entity
(N
);
2662 C
: constant Perm_Tree_Access
:=
2663 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2666 -- Setting the initialization map to True, so that this
2667 -- variable cannot be ignored anymore when looking at end
2668 -- of elaboration of package.
2670 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2672 -- No null possible here, there are no parents for the path.
2673 -- This means we are using a global variable without adding
2674 -- it in environment with a global aspect.
2676 Illegal_Global_Usage
(N
);
2679 return (R
=> Unfolded
, Tree_Access
=> C
);
2683 when N_Type_Conversion
2684 | N_Unchecked_Type_Conversion
2685 | N_Qualified_Expression
2687 return Get_Perm_Or_Tree
(Expression
(N
));
2689 -- Happening when we try to get the permission of a variable that
2690 -- is a formal parameter. We get instead the defining identifier
2691 -- associated with the parameter (which is the one that has been
2692 -- stored for indexing).
2694 when N_Parameter_Specification
=>
2695 return Get_Perm_Or_Tree
(Defining_Identifier
(N
));
2697 -- We get the permission tree of its prefix, and then get either the
2698 -- subtree associated with that specific selection, or if we have a
2699 -- leaf that folds its children, we take the children's permission
2700 -- and return it using the discriminant Folded.
2702 when N_Selected_Component
=>
2704 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2714 pragma Assert
(C
.Tree_Access
/= null);
2715 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2717 Kind
(C
.Tree_Access
) = Record_Component
);
2719 if Kind
(C
.Tree_Access
) = Record_Component
then
2721 Selected_Component
: constant Entity_Id
:=
2722 Entity
(Selector_Name
(N
));
2723 Selected_C
: constant Perm_Tree_Access
:=
2725 (Component
(C
.Tree_Access
), Selected_Component
);
2728 if Selected_C
= null then
2729 return (R
=> Unfolded
,
2731 Other_Components
(C
.Tree_Access
));
2734 return (R
=> Unfolded
,
2735 Tree_Access
=> Selected_C
);
2739 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2740 return (R
=> Folded
,
2742 Children_Permission
(C
.Tree_Access
));
2745 raise Program_Error
;
2749 -- We get the permission tree of its prefix, and then get either the
2750 -- subtree associated with that specific selection, or if we have a
2751 -- leaf that folds its children, we take the children's permission
2752 -- and return it using the discriminant Folded.
2754 when N_Indexed_Component
2758 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2768 pragma Assert
(C
.Tree_Access
/= null);
2769 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2771 Kind
(C
.Tree_Access
) = Array_Component
);
2773 if Kind
(C
.Tree_Access
) = Array_Component
then
2774 pragma Assert
(Get_Elem
(C
.Tree_Access
) /= null);
2775 return (R
=> Unfolded
,
2776 Tree_Access
=> Get_Elem
(C
.Tree_Access
));
2778 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2779 return (R
=> Folded
, Found_Permission
=>
2780 Children_Permission
(C
.Tree_Access
));
2783 raise Program_Error
;
2787 -- We get the permission tree of its prefix, and then get either the
2788 -- subtree associated with that specific selection, or if we have a
2789 -- leaf that folds its children, we take the children's permission
2790 -- and return it using the discriminant Folded.
2792 when N_Explicit_Dereference
=>
2794 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2804 pragma Assert
(C
.Tree_Access
/= null);
2805 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2807 Kind
(C
.Tree_Access
) = Reference
);
2809 if Kind
(C
.Tree_Access
) = Reference
then
2810 if Get_All
(C
.Tree_Access
) = null then
2814 raise Program_Error
;
2819 Tree_Access
=> Get_All
(C
.Tree_Access
));
2822 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2823 return (R
=> Folded
, Found_Permission
=>
2824 Children_Permission
(C
.Tree_Access
));
2827 raise Program_Error
;
2831 -- The name contains a function call, hence the given path is always
2832 -- new. We do not have to check for anything.
2834 when N_Function_Call
=>
2835 return (R
=> Function_Call
);
2838 raise Program_Error
;
2840 end Get_Perm_Or_Tree
;
2846 function Get_Perm_Tree
(N
: Node_Id
) return Perm_Tree_Access
is
2850 -- Base identifier. Normally those are the roots of the trees stored
2851 -- in the permission environment.
2853 when N_Defining_Identifier
=>
2854 raise Program_Error
;
2860 P
: constant Node_Id
:= Entity
(N
);
2861 C
: constant Perm_Tree_Access
:=
2862 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2865 -- Setting the initialization map to True, so that this
2866 -- variable cannot be ignored anymore when looking at end
2867 -- of elaboration of package.
2869 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2871 -- No null possible here, there are no parents for the path.
2872 -- This means we are using a global variable without adding
2873 -- it in environment with a global aspect.
2875 Illegal_Global_Usage
(N
);
2882 when N_Type_Conversion
2883 | N_Unchecked_Type_Conversion
2884 | N_Qualified_Expression
2886 return Get_Perm_Tree
(Expression
(N
));
2888 when N_Parameter_Specification
=>
2889 return Get_Perm_Tree
(Defining_Identifier
(N
));
2891 -- We get the permission tree of its prefix, and then get either the
2892 -- subtree associated with that specific selection, or if we have a
2893 -- leaf that folds its children, we unroll it in one step.
2895 when N_Selected_Component
=>
2897 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
2902 -- If null then it means we went through a function call
2907 pragma Assert
(Kind
(C
) = Entire_Object
2908 or else Kind
(C
) = Record_Component
);
2910 if Kind
(C
) = Record_Component
then
2912 -- The tree is unfolded. We just return the subtree.
2915 Selected_Component
: constant Entity_Id
:=
2916 Entity
(Selector_Name
(N
));
2917 Selected_C
: constant Perm_Tree_Access
:=
2919 (Component
(C
), Selected_Component
);
2922 if Selected_C
= null then
2923 return Other_Components
(C
);
2928 elsif Kind
(C
) = Entire_Object
then
2930 -- Expand the tree. Replace the node with
2931 -- Record_Component.
2935 -- Create the unrolled nodes
2937 Son
: Perm_Tree_Access
;
2939 Child_Perm
: constant Perm_Kind
:=
2940 Children_Permission
(C
);
2943 -- We change the current node from Entire_Object to
2944 -- Record_Component with same permission and an empty
2945 -- hash table as component list.
2948 (Kind
=> Record_Component
,
2949 Is_Node_Deep
=> Is_Node_Deep
(C
),
2950 Permission
=> Permission
(C
),
2951 Component
=> Perm_Tree_Maps
.Nil
,
2953 new Perm_Tree_Wrapper
'
2955 (Kind => Entire_Object,
2956 -- Is_Node_Deep is true, to be conservative
2957 Is_Node_Deep => True,
2958 Permission => Child_Perm,
2959 Children_Permission => Child_Perm)
2963 -- We fill the hash table with all sons of the record,
2964 -- with basic Entire_Objects nodes.
2966 Elem := First_Component_Or_Discriminant
2967 (Etype (Prefix (N)));
2969 while Present (Elem) loop
2970 Son := new Perm_Tree_Wrapper'
2972 (Kind
=> Entire_Object
,
2973 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
2974 Permission
=> Child_Perm
,
2975 Children_Permission
=> Child_Perm
));
2978 (C
.all.Tree
.Component
, Elem
, Son
);
2979 Next_Component_Or_Discriminant
(Elem
);
2981 -- we return the tree to the sons, so that the recursion
2985 Selected_Component
: constant Entity_Id
:=
2986 Entity
(Selector_Name
(N
));
2988 Selected_C
: constant Perm_Tree_Access
:=
2990 (Component
(C
), Selected_Component
);
2993 pragma Assert
(Selected_C
/= null);
2998 raise Program_Error
;
3001 -- We set the permission tree of its prefix, and then we extract from
3002 -- the returned pointer the subtree. If folded, we unroll the tree at
3005 when N_Indexed_Component
3009 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
3013 -- If null then we went through a function call
3017 pragma Assert
(Kind
(C
) = Entire_Object
3018 or else Kind
(C
) = Array_Component
);
3020 if Kind
(C
) = Array_Component
then
3022 -- The tree is unfolded. We just return the elem subtree
3024 pragma Assert
(Get_Elem
(C
) = null);
3025 return Get_Elem
(C
);
3027 elsif Kind
(C
) = Entire_Object
then
3029 -- Expand the tree. Replace node with Array_Component.
3031 Son
: Perm_Tree_Access
;
3034 Son
:= new Perm_Tree_Wrapper
'
3036 (Kind => Entire_Object,
3037 Is_Node_Deep => Is_Node_Deep (C),
3038 Permission => Children_Permission (C),
3039 Children_Permission => Children_Permission (C)));
3041 -- We change the current node from Entire_Object
3042 -- to Array_Component with same permission and the
3043 -- previously defined son.
3045 C.all.Tree := (Kind => Array_Component,
3046 Is_Node_Deep => Is_Node_Deep (C),
3047 Permission => Permission (C),
3049 return Get_Elem (C);
3052 raise Program_Error;
3055 -- We get the permission tree of its prefix, and then get either the
3056 -- subtree associated with that specific selection, or if we have a
3057 -- leaf that folds its children, we unroll the tree.
3059 when N_Explicit_Dereference =>
3061 C : Perm_Tree_Access;
3064 C := Get_Perm_Tree (Prefix (N));
3068 -- If null, we went through a function call
3073 pragma Assert (Kind (C) = Entire_Object
3074 or else Kind (C) = Reference);
3076 if Kind (C) = Reference then
3078 -- The tree is unfolded. We return the elem subtree
3080 if Get_All (C) = null then
3084 raise Program_Error;
3088 elsif Kind (C) = Entire_Object then
3090 -- Expand the tree. Replace the node with Reference.
3092 Son : Perm_Tree_Access;
3095 Son := new Perm_Tree_Wrapper'
3097 (Kind
=> Entire_Object
,
3098 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
3099 Permission
=> Children_Permission
(C
),
3100 Children_Permission
=> Children_Permission
(C
)));
3102 -- We change the current node from Entire_Object to
3103 -- Reference with same permission and the previous son.
3105 pragma Assert
(Is_Node_Deep
(C
));
3106 C
.all.Tree
:= (Kind
=> Reference
,
3107 Is_Node_Deep
=> Is_Node_Deep
(C
),
3108 Permission
=> Permission
(C
),
3113 raise Program_Error
;
3116 -- No permission tree for function calls
3118 when N_Function_Call
=>
3122 raise Program_Error
;
3130 procedure Hp
(P
: Perm_Env
) is
3131 Elem
: Perm_Tree_Maps
.Key_Option
;
3134 Elem
:= Get_First_Key
(P
);
3135 while Elem
.Present
loop
3136 Print_Node_Briefly
(Elem
.K
);
3137 Elem
:= Get_Next_Key
(P
);
3141 --------------------------
3142 -- Illegal_Global_Usage --
3143 --------------------------
3145 procedure Illegal_Global_Usage
(N
: Node_Or_Entity_Id
) is
3147 Error_Msg_NE
("cannot use global variable & of deep type", N
, N
);
3148 Error_Msg_N
("\without prior declaration in a Global aspect", N
);
3149 Errout
.Finalize
(Last_Call
=> True);
3150 Errout
.Output_Messages
;
3151 Exit_Program
(E_Errors
);
3152 end Illegal_Global_Usage
;
3158 function Is_Deep
(E
: Entity_Id
) return Boolean is
3159 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean;
3160 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean is
3162 Pack_Decl
: Node_Id
;
3165 if Is_Itype
(E
) then
3166 Decl
:= Associated_Node_For_Itype
(E
);
3171 Pack_Decl
:= Parent
(Parent
(Decl
));
3173 if Nkind
(Pack_Decl
) /= N_Package_Declaration
then
3178 Present
(SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
)))
3179 and then Get_SPARK_Mode_From_Annotation
3180 (SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
))) = Off
;
3181 end Is_Private_Entity_Mode_Off
;
3184 pragma Assert
(Is_Type
(E
));
3192 -- Just check the depth of its component type
3197 return Is_Deep
(Component_Type
(E
));
3199 when E_String_Literal_Subtype
=>
3202 -- Per RM 8.11 for class-wide types
3204 when E_Class_Wide_Subtype
3209 -- ??? What about hidden components
3218 Elmt
:= First_Component_Or_Discriminant
(E
);
3219 while Present
(Elmt
) loop
3220 if Is_Deep
(Etype
(Elmt
)) then
3223 Next_Component_Or_Discriminant
(Elmt
);
3229 when Private_Kind
=>
3230 if Is_Private_Entity_Mode_Off
(E
) then
3233 if Present
(Full_View
(E
)) then
3234 return Is_Deep
(Full_View
(E
));
3240 when E_Incomplete_Type
3241 | E_Incomplete_Subtype
3245 -- No problem with synchronized types
3247 when E_Protected_Type
3248 | E_Protected_Subtype
3254 when E_Exception_Type
=>
3258 raise Program_Error
;
3266 procedure Perm_Error
3269 Found_Perm
: Perm_Kind
)
3271 procedure Set_Root_Object
3273 Obj
: out Entity_Id
;
3274 Deref
: out Boolean);
3275 -- Set the root object Obj, and whether the path contains a dereference,
3276 -- from a path Path.
3278 ---------------------
3279 -- Set_Root_Object --
3280 ---------------------
3282 procedure Set_Root_Object
3284 Obj
: out Entity_Id
;
3285 Deref
: out Boolean)
3288 case Nkind
(Path
) is
3292 Obj
:= Entity
(Path
);
3295 when N_Type_Conversion
3296 | N_Unchecked_Type_Conversion
3297 | N_Qualified_Expression
3299 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
3301 when N_Indexed_Component
3302 | N_Selected_Component
3305 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3307 when N_Explicit_Dereference
=>
3308 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3312 raise Program_Error
;
3314 end Set_Root_Object
;
3320 -- Start of processing for Perm_Error
3323 Set_Root_Object
(N
, Root
, Is_Deref
);
3327 ("insufficient permission on dereference from &", N
, Root
);
3329 Error_Msg_NE
("insufficient permission for &", N
, Root
);
3332 Perm_Mismatch
(Perm
, Found_Perm
, N
);
3335 -------------------------------
3336 -- Perm_Error_Subprogram_End --
3337 -------------------------------
3339 procedure Perm_Error_Subprogram_End
3343 Found_Perm
: Perm_Kind
)
3346 Error_Msg_Node_2
:= Subp
;
3347 Error_Msg_NE
("insufficient permission for & when returning from &",
3349 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
3350 end Perm_Error_Subprogram_End
;
3356 procedure Process_Path
(N
: Node_Id
) is
3357 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
3358 State_N
: Perm_Kind
;
3360 -- We ignore if yielding to synchronized
3363 and then Is_Synchronized_Object
(Root
)
3368 State_N
:= Get_Perm
(N
);
3370 case Current_Checking_Mode
is
3372 -- Check permission R, do nothing
3376 -- This condition should be removed when removing the read
3383 -- The rhs object in an assignment statement (including copy in
3384 -- and copy back) should be in the Unrestricted or Moved state.
3385 -- Otherwise the move is not allowed.
3386 -- This applies to both stand-alone and composite objects.
3387 -- If the state of the source is Moved, then a warning message
3388 -- is prompt to make the user aware of reading a nullified
3391 if State_N
/= Unrestricted
and State_N
/= Moved
then
3392 Perm_Error
(N
, Unrestricted
, State_N
);
3396 -- In the AI, after moving a path nothing to do since the rhs
3397 -- object was in the Unrestricted state and it shall be
3398 -- refreshed to Unrestricted. The object should be nullified
3399 -- however. To avoid moving again a name that has already been
3400 -- moved, in this implementation we set the state of the moved
3401 -- object to "Moved". This shall be used to prompt a warning
3402 -- when manipulating a null pointer and also to implement
3403 -- the no aliasing parameter restriction.
3405 if State_N
= Moved
then
3406 Error_Msg_N
("?the source or one of its extensions has"
3407 & " already been moved", N
);
3411 -- Set state to Moved to the path and any of its prefixes
3413 Tree
: constant Perm_Tree_Access
:=
3414 Set_Perm_Prefixes
(N
, Moved
);
3419 -- We went through a function call, no permission to
3425 -- Set state to Moved on any strict extension of the path
3427 Set_Perm_Extensions
(Tree
, Moved
);
3432 -- The lhs object in an assignment statement (including copy in
3433 -- and copy back) should be in the Unrestricted state.
3434 -- Otherwise the move is not allowed.
3435 -- This applies to both stand-alone and composite objects.
3437 if State_N
/= Unrestricted
and State_N
/= Moved
then
3438 Perm_Error
(N
, Unrestricted
, State_N
);
3442 -- After assigning to a path nothing to do since it was in the
3443 -- Unrestricted state and it would be refreshed to
3448 -- Borrowing is only allowed on Unrestricted objects.
3450 if State_N
/= Unrestricted
and State_N
/= Moved
then
3451 Perm_Error
(N
, Unrestricted
, State_N
);
3454 if State_N
= Moved
then
3455 Error_Msg_N
("?the source or one of its extensions has"
3456 & " already been moved", N
);
3460 -- Set state to Borrowed to the path and any of its prefixes
3462 Tree
: constant Perm_Tree_Access
:=
3463 Set_Perm_Prefixes
(N
, Borrowed
);
3468 -- We went through a function call, no permission to
3474 -- Set state to Borrowed on any strict extension of the path
3476 Set_Perm_Extensions
(Tree
, Borrowed
);
3480 if State_N
/= Unrestricted
3481 and then State_N
/= Observed
3483 Perm_Error
(N
, Observed
, State_N
);
3487 -- Set permission to Observed on the path and any of its
3488 -- prefixes if it is of a deep type. Actually, some operation
3489 -- like reading from an object of access type is considered as
3490 -- observe while it should not affect the permissions of
3491 -- the considered tree.
3493 Tree
: Perm_Tree_Access
;
3496 if Is_Deep
(Etype
(N
)) then
3497 Tree
:= Set_Perm_Prefixes
(N
, Observed
);
3504 -- We went through a function call, no permission to
3510 -- Set permissions to No on any strict extension of the path
3512 Set_Perm_Extensions
(Tree
, Observed
);
3517 -------------------------
3518 -- Return_Declarations --
3519 -------------------------
3521 procedure Return_Declarations
(L
: List_Id
) is
3522 procedure Return_Declaration
(Decl
: Node_Id
);
3523 -- Check correct permissions for every declared object
3525 ------------------------
3526 -- Return_Declaration --
3527 ------------------------
3529 procedure Return_Declaration
(Decl
: Node_Id
) is
3531 if Nkind
(Decl
) = N_Object_Declaration
then
3533 -- Check RW for object declared, unless the object has never been
3536 if Get
(Current_Initialization_Map
,
3537 Unique_Entity
(Defining_Identifier
(Decl
))) = False
3543 Elem
: constant Perm_Tree_Access
:=
3544 Get
(Current_Perm_Env
,
3545 Unique_Entity
(Defining_Identifier
(Decl
)));
3550 -- Here we are on a declaration. Hence it should have been
3551 -- added in the environment when analyzing this node with
3552 -- mode Read. Hence it is not possible to find a null
3557 raise Program_Error
;
3560 if Permission
(Elem
) /= Unrestricted
then
3561 Perm_Error
(Decl
, Unrestricted
, Permission
(Elem
));
3565 end Return_Declaration
;
3570 -- Start of processing for Return_Declarations
3574 while Present
(N
) loop
3575 Return_Declaration
(N
);
3578 end Return_Declarations
;
3580 --------------------
3581 -- Return_Globals --
3582 --------------------
3584 procedure Return_Globals
(Subp
: Entity_Id
) is
3585 procedure Return_Globals_From_List
3586 (First_Item
: Node_Id
;
3587 Kind
: Formal_Kind
);
3588 -- Return global items from the list starting at Item
3590 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
3591 -- Return global items for the mode Global_Mode
3593 ------------------------------
3594 -- Return_Globals_From_List --
3595 ------------------------------
3597 procedure Return_Globals_From_List
3598 (First_Item
: Node_Id
;
3601 Item
: Node_Id
:= First_Item
;
3605 while Present
(Item
) loop
3608 -- Ignore abstract states, which play no role in pointer aliasing
3610 if Ekind
(E
) = E_Abstract_State
then
3613 Return_The_Global
(E
, Kind
, Subp
);
3617 end Return_Globals_From_List
;
3619 ----------------------------
3620 -- Return_Globals_Of_Mode --
3621 ----------------------------
3623 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
3631 Kind
:= E_In_Parameter
;
3633 Kind
:= E_Out_Parameter
;
3635 Kind
:= E_In_Out_Parameter
;
3637 raise Program_Error
;
3640 -- Return both global items from Global and Refined_Global pragmas
3642 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
3643 Return_Globals_From_List
3644 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
3645 end Return_Globals_Of_Mode
;
3647 -- Start of processing for Return_Globals
3650 Return_Globals_Of_Mode
(Name_Proof_In
);
3651 Return_Globals_Of_Mode
(Name_Input
);
3652 Return_Globals_Of_Mode
(Name_Output
);
3653 Return_Globals_Of_Mode
(Name_In_Out
);
3656 --------------------------------
3657 -- Return_Parameter_Or_Global --
3658 --------------------------------
3660 procedure Return_The_Global
3665 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
3666 pragma Assert
(Elem
/= null);
3669 -- Observed IN parameters and globals need not return a permission to
3672 if Mode
= E_In_Parameter
3674 -- Check this for read-only globals.
3677 if Permission
(Elem
) /= Unrestricted
3678 and then Permission
(Elem
) /= Observed
3680 Perm_Error_Subprogram_End
3684 Found_Perm
=> Permission
(Elem
));
3687 -- All globals of mode out or in/out should return with mode
3691 if Permission
(Elem
) /= Unrestricted
then
3692 Perm_Error_Subprogram_End
3695 Perm
=> Unrestricted
,
3696 Found_Perm
=> Permission
(Elem
));
3699 end Return_The_Global
;
3701 -------------------------
3702 -- Set_Perm_Extensions --
3703 -------------------------
3705 procedure Set_Perm_Extensions
(T
: Perm_Tree_Access
; P
: Perm_Kind
) is
3706 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
3707 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
) is
3710 when Entire_Object
=>
3714 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
3716 when Array_Component
=>
3717 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
3719 -- Free every Component subtree
3721 when Record_Component
=>
3723 Comp
: Perm_Tree_Access
;
3726 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
3727 while Comp
/= null loop
3728 Free_Perm_Tree
(Comp
);
3729 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
3732 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
3735 end Free_Perm_Tree_Children
;
3737 Son
: constant Perm_Tree
:=
3739 (Kind => Entire_Object,
3740 Is_Node_Deep => Is_Node_Deep (T),
3741 Permission => Permission (T),
3742 Children_Permission => P);
3745 Free_Perm_Tree_Children (T);
3747 end Set_Perm_Extensions;
3749 ------------------------------
3750 -- Set_Perm_Prefixes --
3751 ------------------------------
3753 function Set_Perm_Prefixes
3755 New_Perm : Perm_Kind)
3756 return Perm_Tree_Access
3764 | N_Defining_Identifier
3766 if Nkind (N) = N_Defining_Identifier
3767 and then New_Perm = Borrowed
3769 raise Program_Error;
3774 C : Perm_Tree_Access;
3777 if Nkind (N) = N_Defining_Identifier then
3783 C := Get (Current_Perm_Env, Unique_Entity (P));
3784 pragma Assert (C /= null);
3786 -- Setting the initialization map to True, so that this
3787 -- variable cannot be ignored anymore when looking at end
3788 -- of elaboration of package.
3790 Set (Current_Initialization_Map, Unique_Entity (P), True);
3791 if New_Perm = Observed
3795 -- No null possible here, there are no parents for the path.
3796 -- This means we are using a global variable without adding
3797 -- it in environment with a global aspect.
3799 Illegal_Global_Usage (N);
3802 C.all.Tree.Permission := New_Perm;
3806 when N_Type_Conversion
3807 | N_Unchecked_Type_Conversion
3808 | N_Qualified_Expression
3810 return Set_Perm_Prefixes (Expression (N), New_Perm);
3812 when N_Parameter_Specification =>
3813 raise Program_Error;
3815 -- We set the permission tree of its prefix, and then we extract
3816 -- our subtree from the returned pointer and assign an adequate
3817 -- permission to it, if unfolded. If folded, we unroll the tree
3820 when N_Selected_Component =>
3822 C : constant Perm_Tree_Access :=
3823 Set_Perm_Prefixes (Prefix (N), New_Perm);
3828 -- We went through a function call, do nothing
3833 pragma Assert (Kind (C) = Entire_Object
3834 or else Kind (C) = Record_Component);
3836 if Kind (C) = Record_Component then
3837 -- The tree is unfolded. We just modify the permission and
3838 -- return the record subtree.
3841 Selected_Component : constant Entity_Id :=
3842 Entity (Selector_Name (N));
3844 Selected_C : Perm_Tree_Access :=
3846 (Component (C), Selected_Component);
3849 if Selected_C = null then
3850 Selected_C := Other_Components (C);
3853 pragma Assert (Selected_C /= null);
3854 Selected_C.all.Tree.Permission := New_Perm;
3858 elsif Kind (C) = Entire_Object then
3860 -- Expand the tree. Replace the node with
3861 -- Record_Component.
3865 -- Create an empty hash table
3867 Hashtbl : Perm_Tree_Maps.Instance;
3869 -- We create the unrolled nodes, that will all have same
3870 -- permission than parent.
3872 Son : Perm_Tree_Access;
3873 Children_Perm : constant Perm_Kind :=
3874 Children_Permission (C);
3877 -- We change the current node from Entire_Object to
3878 -- Record_Component with same permission and an empty
3879 -- hash table as component list.
3882 (Kind => Record_Component,
3883 Is_Node_Deep => Is_Node_Deep (C),
3884 Permission => Permission (C),
3885 Component => Hashtbl,
3887 new Perm_Tree_Wrapper'
3889 (Kind
=> Entire_Object
,
3890 Is_Node_Deep
=> True,
3891 Permission
=> Children_Perm
,
3892 Children_Permission
=> Children_Perm
)
3895 -- We fill the hash table with all sons of the record,
3896 -- with basic Entire_Objects nodes.
3898 Elem
:= First_Component_Or_Discriminant
3899 (Etype
(Prefix
(N
)));
3901 while Present
(Elem
) loop
3902 Son
:= new Perm_Tree_Wrapper
'
3904 (Kind => Entire_Object,
3905 Is_Node_Deep => Is_Deep (Etype (Elem)),
3906 Permission => Children_Perm,
3907 Children_Permission => Children_Perm));
3909 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
3910 Next_Component_Or_Discriminant (Elem);
3912 -- Now we set the right field to Borrowed, and then we
3913 -- return the tree to the sons, so that the recursion can
3917 Selected_Component : constant Entity_Id :=
3918 Entity (Selector_Name (N));
3919 Selected_C : Perm_Tree_Access :=
3921 (Component (C), Selected_Component);
3924 if Selected_C = null then
3925 Selected_C := Other_Components (C);
3928 pragma Assert (Selected_C /= null);
3929 Selected_C.all.Tree.Permission := New_Perm;
3934 raise Program_Error;
3938 -- We set the permission tree of its prefix, and then we extract
3939 -- from the returned pointer the subtree and assign an adequate
3940 -- permission to it, if unfolded. If folded, we unroll the tree in
3943 when N_Indexed_Component
3947 C : constant Perm_Tree_Access :=
3948 Set_Perm_Prefixes (Prefix (N), New_Perm);
3953 -- We went through a function call, do nothing
3958 pragma Assert (Kind (C) = Entire_Object
3959 or else Kind (C) = Array_Component);
3961 if Kind (C) = Array_Component then
3963 -- The tree is unfolded. We just modify the permission and
3964 -- return the elem subtree.
3966 pragma Assert (Get_Elem (C) /= null);
3967 C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
3968 return Get_Elem (C);
3970 elsif Kind (C) = Entire_Object then
3972 -- Expand the tree. Replace node with Array_Component.
3974 Son : Perm_Tree_Access;
3977 Son := new Perm_Tree_Wrapper'
3979 (Kind
=> Entire_Object
,
3980 Is_Node_Deep
=> Is_Node_Deep
(C
),
3981 Permission
=> New_Perm
,
3982 Children_Permission
=> Children_Permission
(C
)));
3984 -- Children_Permission => Children_Permission (C)
3985 -- this line should be checked maybe New_Perm
3986 -- instead of Children_Permission (C)
3988 -- We change the current node from Entire_Object
3989 -- to Array_Component with same permission and the
3990 -- previously defined son.
3992 C
.all.Tree
:= (Kind
=> Array_Component
,
3993 Is_Node_Deep
=> Is_Node_Deep
(C
),
3994 Permission
=> New_Perm
,
3996 return Get_Elem
(C
);
3999 raise Program_Error
;
4003 -- We set the permission tree of its prefix, and then we extract
4004 -- from the returned pointer the subtree and assign an adequate
4005 -- permission to it, if unfolded. If folded, we unroll the tree
4008 when N_Explicit_Dereference
=>
4010 C
: constant Perm_Tree_Access
:=
4011 Set_Perm_Prefixes
(Prefix
(N
), New_Perm
);
4016 -- We went through a function call. Do nothing.
4021 pragma Assert
(Kind
(C
) = Entire_Object
4022 or else Kind
(C
) = Reference
);
4024 if Kind
(C
) = Reference
then
4026 -- The tree is unfolded. We just modify the permission and
4027 -- return the elem subtree.
4029 pragma Assert
(Get_All
(C
) /= null);
4030 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= New_Perm
;
4033 elsif Kind
(C
) = Entire_Object
then
4035 -- Expand the tree. Replace the node with Reference.
4037 Son
: Perm_Tree_Access
;
4040 Son
:= new Perm_Tree_Wrapper
'
4042 (Kind => Entire_Object,
4043 Is_Node_Deep => Is_Deep (Etype (N)),
4044 Permission => New_Perm,
4045 Children_Permission => Children_Permission (C)));
4047 -- We change the current node from Entire_Object to
4048 -- Reference with Borrowed and the previous son.
4050 pragma Assert (Is_Node_Deep (C));
4051 C.all.Tree := (Kind => Reference,
4052 Is_Node_Deep => Is_Node_Deep (C),
4053 Permission => New_Perm,
4059 raise Program_Error;
4063 when N_Function_Call =>
4067 raise Program_Error;
4069 end Set_Perm_Prefixes;
4071 ------------------------------
4072 -- Set_Perm_Prefixes_Borrow --
4073 ------------------------------
4075 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
4078 pragma Assert (Current_Checking_Mode = Borrow);
4085 P : constant Node_Id := Entity (N);
4086 C : constant Perm_Tree_Access :=
4087 Get (Current_Perm_Env, Unique_Entity (P));
4088 pragma Assert (C /= null);
4091 -- Setting the initialization map to True, so that this
4092 -- variable cannot be ignored anymore when looking at end
4093 -- of elaboration of package.
4095 Set (Current_Initialization_Map, Unique_Entity (P), True);
4096 C.all.Tree.Permission := Borrowed;
4100 when N_Type_Conversion
4101 | N_Unchecked_Type_Conversion
4102 | N_Qualified_Expression
4104 return Set_Perm_Prefixes_Borrow (Expression (N));
4106 when N_Parameter_Specification
4107 | N_Defining_Identifier
4109 raise Program_Error;
4111 -- We set the permission tree of its prefix, and then we extract
4112 -- our subtree from the returned pointer and assign an adequate
4113 -- permission to it, if unfolded. If folded, we unroll the tree
4116 when N_Selected_Component =>
4118 C : constant Perm_Tree_Access :=
4119 Set_Perm_Prefixes_Borrow (Prefix (N));
4124 -- We went through a function call, do nothing
4129 -- The permission of the returned node should be No
4131 pragma Assert (Permission (C) = Borrowed);
4132 pragma Assert (Kind (C) = Entire_Object
4133 or else Kind (C) = Record_Component);
4135 if Kind (C) = Record_Component then
4137 -- The tree is unfolded. We just modify the permission and
4138 -- return the record subtree.
4141 Selected_Component : constant Entity_Id :=
4142 Entity (Selector_Name (N));
4143 Selected_C : Perm_Tree_Access :=
4145 (Component (C), Selected_Component);
4148 if Selected_C = null then
4149 Selected_C := Other_Components (C);
4152 pragma Assert (Selected_C /= null);
4153 Selected_C.all.Tree.Permission := Borrowed;
4157 elsif Kind (C) = Entire_Object then
4159 -- Expand the tree. Replace the node with
4160 -- Record_Component.
4164 -- Create an empty hash table
4166 Hashtbl : Perm_Tree_Maps.Instance;
4168 -- We create the unrolled nodes, that will all have same
4169 -- permission than parent.
4171 Son : Perm_Tree_Access;
4172 ChildrenPerm : constant Perm_Kind :=
4173 Children_Permission (C);
4176 -- We change the current node from Entire_Object to
4177 -- Record_Component with same permission and an empty
4178 -- hash table as component list.
4181 (Kind => Record_Component,
4182 Is_Node_Deep => Is_Node_Deep (C),
4183 Permission => Permission (C),
4184 Component => Hashtbl,
4186 new Perm_Tree_Wrapper'
4188 (Kind
=> Entire_Object
,
4189 Is_Node_Deep
=> True,
4190 Permission
=> ChildrenPerm
,
4191 Children_Permission
=> ChildrenPerm
)
4194 -- We fill the hash table with all sons of the record,
4195 -- with basic Entire_Objects nodes.
4197 Elem
:= First_Component_Or_Discriminant
4198 (Etype
(Prefix
(N
)));
4200 while Present
(Elem
) loop
4201 Son
:= new Perm_Tree_Wrapper
'
4203 (Kind => Entire_Object,
4204 Is_Node_Deep => Is_Deep (Etype (Elem)),
4205 Permission => ChildrenPerm,
4206 Children_Permission => ChildrenPerm));
4207 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
4208 Next_Component_Or_Discriminant (Elem);
4211 -- Now we set the right field to Borrowed, and then we
4212 -- return the tree to the sons, so that the recursion can
4216 Selected_Component : constant Entity_Id :=
4217 Entity (Selector_Name (N));
4218 Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
4219 (Component (C), Selected_Component);
4222 if Selected_C = null then
4223 Selected_C := Other_Components (C);
4226 pragma Assert (Selected_C /= null);
4227 Selected_C.all.Tree.Permission := Borrowed;
4233 raise Program_Error;
4237 -- We set the permission tree of its prefix, and then we extract
4238 -- from the returned pointer the subtree and assign an adequate
4239 -- permission to it, if unfolded. If folded, we unroll the tree in
4242 when N_Indexed_Component
4246 C : constant Perm_Tree_Access :=
4247 Set_Perm_Prefixes_Borrow (Prefix (N));
4252 -- We went through a function call, do nothing
4257 pragma Assert (Permission (C) = Borrowed);
4258 pragma Assert (Kind (C) = Entire_Object
4259 or else Kind (C) = Array_Component);
4261 if Kind (C) = Array_Component then
4263 -- The tree is unfolded. We just modify the permission and
4264 -- return the elem subtree.
4266 pragma Assert (Get_Elem (C) /= null);
4267 C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed;
4268 return Get_Elem (C);
4270 elsif Kind (C) = Entire_Object then
4272 -- Expand the tree. Replace node with Array_Component.
4274 Son : Perm_Tree_Access;
4277 Son := new Perm_Tree_Wrapper'
4279 (Kind
=> Entire_Object
,
4280 Is_Node_Deep
=> Is_Node_Deep
(C
),
4281 Permission
=> Borrowed
,
4282 Children_Permission
=> Children_Permission
(C
)));
4284 -- We change the current node from Entire_Object
4285 -- to Array_Component with same permission and the
4286 -- previously defined son.
4288 C
.all.Tree
:= (Kind
=> Array_Component
,
4289 Is_Node_Deep
=> Is_Node_Deep
(C
),
4290 Permission
=> Borrowed
,
4292 return Get_Elem
(C
);
4296 raise Program_Error
;
4300 -- We set the permission tree of its prefix, and then we extract
4301 -- from the returned pointer the subtree and assign an adequate
4302 -- permission to it, if unfolded. If folded, we unroll the tree
4305 when N_Explicit_Dereference
=>
4307 C
: constant Perm_Tree_Access
:=
4308 Set_Perm_Prefixes_Borrow
(Prefix
(N
));
4313 -- We went through a function call. Do nothing.
4318 -- The permission of the returned node should be No
4320 pragma Assert
(Permission
(C
) = Borrowed
);
4321 pragma Assert
(Kind
(C
) = Entire_Object
4322 or else Kind
(C
) = Reference
);
4324 if Kind
(C
) = Reference
then
4326 -- The tree is unfolded. We just modify the permission and
4327 -- return the elem subtree.
4329 pragma Assert
(Get_All
(C
) /= null);
4330 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= Borrowed
;
4333 elsif Kind
(C
) = Entire_Object
then
4335 -- Expand the tree. Replace the node with Reference.
4337 Son
: Perm_Tree_Access
;
4340 Son
:= new Perm_Tree_Wrapper
'
4342 (Kind => Entire_Object,
4343 Is_Node_Deep => Is_Deep (Etype (N)),
4344 Permission => Borrowed,
4345 Children_Permission => Children_Permission (C)));
4347 -- We change the current node from Entire_Object to
4348 -- Reference with Borrowed and the previous son.
4350 pragma Assert (Is_Node_Deep (C));
4351 C.all.Tree := (Kind => Reference,
4352 Is_Node_Deep => Is_Node_Deep (C),
4353 Permission => Borrowed,
4359 raise Program_Error;
4363 when N_Function_Call =>
4367 raise Program_Error;
4369 end Set_Perm_Prefixes_Borrow;
4375 procedure Setup_Globals (Subp : Entity_Id) is
4376 procedure Setup_Globals_From_List
4377 (First_Item : Node_Id;
4378 Kind : Formal_Kind);
4379 -- Set up global items from the list starting at Item
4381 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
4382 -- Set up global items for the mode Global_Mode
4384 -----------------------------
4385 -- Setup_Globals_From_List --
4386 -----------------------------
4388 procedure Setup_Globals_From_List
4389 (First_Item : Node_Id;
4392 Item : Node_Id := First_Item;
4396 while Present (Item) loop
4399 -- Ignore abstract states, which play no role in pointer aliasing
4401 if Ekind (E) = E_Abstract_State then
4404 Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
4408 end Setup_Globals_From_List;
4410 ---------------------------
4411 -- Setup_Globals_Of_Mode --
4412 ---------------------------
4414 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
4422 Kind := E_In_Parameter;
4425 Kind := E_Out_Parameter;
4428 Kind := E_In_Out_Parameter;
4431 raise Program_Error;
4434 -- Set up both global items from Global and Refined_Global pragmas
4436 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
4437 Setup_Globals_From_List
4438 (First_Global (Subp, Global_Mode, Refined => True), Kind);
4439 end Setup_Globals_Of_Mode;
4441 -- Start of processing for Setup_Globals
4444 Setup_Globals_Of_Mode (Name_Proof_In);
4445 Setup_Globals_Of_Mode (Name_Input);
4446 Setup_Globals_Of_Mode (Name_Output);
4447 Setup_Globals_Of_Mode (Name_In_Out);
4450 -------------------------------
4451 -- Setup_Parameter_Or_Global --
4452 -------------------------------
4454 procedure Setup_Parameter_Or_Global
4457 Global_Var : Boolean)
4459 Elem : Perm_Tree_Access;
4460 View_Typ : Entity_Id;
4463 if Present (Full_View (Etype (Id))) then
4464 View_Typ := Full_View (Etype (Id));
4466 View_Typ := Etype (Id);
4469 Elem := new Perm_Tree_Wrapper'
4471 (Kind
=> Entire_Object
,
4472 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
4473 Permission
=> Unrestricted
,
4474 Children_Permission
=> Unrestricted
));
4478 -- All out and in out parameters are considered to be unrestricted.
4479 -- They are whether borrowed or moved. Ada Rules would restrict
4480 -- these permissions further. For example an in parameter cannot
4483 -- In the following we deal with in parameters that can be observed.
4484 -- We only consider the observing cases.
4486 when E_In_Parameter
=>
4488 -- Handling global variables as IN parameters here.
4489 -- Remove the following condition once it's decided how globals
4490 -- should be considered. ???
4492 -- In SPARK, IN access-to-variable is an observe operation for
4493 -- a function, and a borrow operation for a procedure.
4495 if not Global_Var
then
4496 if (Is_Access_Type
(View_Typ
)
4497 and then Is_Access_Constant
(View_Typ
)
4498 and then Is_Anonymous_Access_Type
(View_Typ
))
4500 (Is_Access_Type
(View_Typ
)
4501 and then Ekind
(Scope
(Id
)) = E_Function
)
4503 (not Is_Access_Type
(View_Typ
)
4504 and then Is_Deep
(View_Typ
)
4505 and then not Is_Anonymous_Access_Type
(View_Typ
))
4507 Elem
.all.Tree
.Permission
:= Observed
;
4508 Elem
.all.Tree
.Children_Permission
:= Observed
;
4511 Elem
.all.Tree
.Permission
:= Unrestricted
;
4512 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4516 Elem
.all.Tree
.Permission
:= Observed
;
4517 Elem
.all.Tree
.Children_Permission
:= Observed
;
4520 -- When out or in/out formal or global parameters, we set them to
4521 -- the Unrestricted state. "We want to be able to assume that all
4522 -- relevant writable globals are unrestricted when a subprogram
4523 -- starts executing". Formal parameters of mode out or in/out
4524 -- are whether Borrowers or the targets of a move operation:
4525 -- they start theirs lives in the subprogram as Unrestricted.
4528 Elem
.all.Tree
.Permission
:= Unrestricted
;
4529 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4532 Set
(Current_Perm_Env
, Id
, Elem
);
4533 end Setup_Parameter_Or_Global
;
4535 ----------------------
4536 -- Setup_Parameters --
4537 ----------------------
4539 procedure Setup_Parameters
(Subp
: Entity_Id
) is Formal
: Entity_Id
;
4541 Formal
:= First_Formal
(Subp
);
4542 while Present
(Formal
) loop
4543 Setup_Parameter_Or_Global
4544 (Formal
, Ekind
(Formal
), Global_Var
=> False);
4545 Next_Formal
(Formal
);
4547 end Setup_Parameters
;
4549 -------------------------------
4550 -- Has_Ownership_Aspect_True --
4551 -------------------------------
4553 function Has_Ownership_Aspect_True
4559 case Ekind
(Etype
(N
)) is
4561 if Ekind
(Etype
(N
)) = E_General_Access_Type
then
4562 Error_Msg_NE
(Msg
& " & not allowed " &
4563 "(Named General Access type)", N
, N
);
4574 Com_Ty
: constant Node_Id
:= Component_Type
(Etype
(N
));
4575 Ret
: Boolean := Has_Ownership_Aspect_True
(Com_Ty
, "");
4578 if Nkind
(Parent
(N
)) = N_Full_Type_Declaration
and
4579 Is_Anonymous_Access_Type
(Com_Ty
)
4585 Error_Msg_NE
(Msg
& " & not allowed "
4586 & "(Components of Named General Access type or"
4587 & " Anonymous type)", N
, N
);
4592 -- ??? What about hidden components
4599 Elmt_T_Perm
: Boolean := True;
4600 Elmt_Perm
, Elmt_Anonym
: Boolean;
4603 Elmt
:= First_Component_Or_Discriminant
(Etype
(N
));
4604 while Present
(Elmt
) loop
4605 Elmt_Perm
:= Has_Ownership_Aspect_True
(Elmt
,
4606 "type of component");
4607 Elmt_Anonym
:= Is_Anonymous_Access_Type
(Etype
(Elmt
));
4610 ("type of component & not allowed"
4611 & " (Components of Anonymous type)", Elmt
, Elmt
);
4613 Elmt_T_Perm
:= Elmt_T_Perm
and Elmt_Perm
and not Elmt_Anonym
;
4614 Next_Component_Or_Discriminant
(Elmt
);
4616 if not Elmt_T_Perm
then
4618 (Msg
& " & not allowed (One or "
4619 & "more components have Ownership Aspect False)",
4629 end Has_Ownership_Aspect_True
;