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
866 Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
867 Target_Typ : Node_Id renames Etype (Target_Ent);
869 Target_View_Typ : Entity_Id;
871 Check : Boolean := True;
873 if Present (Full_View (Target_Typ)) then
874 Target_View_Typ := Full_View (Target_Typ);
876 Target_View_Typ := Target_Typ;
879 case N_Declaration'(Nkind
(Decl
)) is
880 when N_Full_Type_Declaration
=>
881 if not Has_Ownership_Aspect_True
(Target_Ent
, "type declaration")
886 -- ??? What about component declarations with defaults.
888 when N_Object_Declaration
=>
889 if (Is_Access_Type
(Target_View_Typ
)
890 or else Is_Deep
(Target_Typ
))
891 and then not Has_Ownership_Aspect_True
892 (Target_Ent
, "Object declaration ")
897 if Is_Anonymous_Access_Type
(Target_View_Typ
)
898 and then not Present
(Expression
(Decl
))
901 -- ??? Check the case of default value (AI)
902 -- ??? How an anonymous access type can be with default exp?
904 Error_Msg_NE
("? object declaration & has OAF (Anonymous "
905 & "access-to-object with no initialization)",
908 -- If it it an initialization
910 elsif Present
(Expression
(Decl
)) and Check
then
912 -- Find out the operation to be done on the right-hand side
914 -- Initializing object, access type
916 if Is_Access_Type
(Target_View_Typ
) then
918 -- Initializing object, constant access type
920 if Is_Constant_Object
(Target_Ent
) then
922 -- Initializing object, constant access to variable type
924 if not Is_Access_Constant
(Target_View_Typ
) then
925 Current_Checking_Mode
:= Borrow
;
927 -- Initializing object, constant access to constant type
929 -- Initializing object,
930 -- constant access to constant anonymous type.
932 elsif Is_Anonymous_Access_Type
(Target_View_Typ
) then
934 -- This is an object declaration so the target
935 -- of the assignement is a stand-alone object.
937 Current_Checking_Mode
:= Observe
;
939 -- Initializing object, constant access to constant
943 -- If named then it is a general access type
944 -- Hence, Has_Ownership_Aspec_True is False.
949 -- Initializing object, variable access type
952 -- Initializing object, variable access to variable type
954 if not Is_Access_Constant
(Target_View_Typ
) then
956 -- Initializing object, variable named access to
959 if not Is_Anonymous_Access_Type
(Target_View_Typ
) then
960 Current_Checking_Mode
:= Move
;
962 -- Initializing object, variable anonymous access to
966 -- This is an object declaration so the target
967 -- object of the assignement is a stand-alone
970 Current_Checking_Mode
:= Borrow
;
973 -- Initializing object, variable access to constant type
976 -- Initializing object,
977 -- variable named access to constant type.
979 if not Is_Anonymous_Access_Type
(Target_View_Typ
) then
980 Error_Msg_N
("assignment not allowed, Ownership "
981 & "Aspect False (Anonymous Access "
985 -- Initializing object,
986 -- variable anonymous access to constant type.
989 -- This is an object declaration so the target
990 -- of the assignement is a stand-alone object.
992 Current_Checking_Mode
:= Observe
;
997 -- Initializing object, composite (deep) type
999 elsif Is_Deep
(Target_Typ
) then
1001 -- Initializing object, constant composite type
1003 if Is_Constant_Object
(Target_Ent
) then
1004 Current_Checking_Mode
:= Observe
;
1006 -- Initializing object, variable composite type
1010 -- Initializing object, variable anonymous composite type
1012 if Nkind
(Object_Definition
(Decl
)) =
1013 N_Constrained_Array_Definition
1015 -- An N_Constrained_Array_Definition is an anonymous
1016 -- array (to be checked). Record types are always
1017 -- named and are considered in the else part.
1021 Com_Ty
: constant Node_Id
:=
1022 Component_Type
(Etype
(Target_Typ
));
1025 if Is_Access_Type
(Com_Ty
) then
1027 -- If components are of anonymous type
1029 if Is_Anonymous_Access_Type
(Com_Ty
) then
1030 if Is_Access_Constant
(Com_Ty
) then
1031 Current_Checking_Mode
:= Observe
;
1034 Current_Checking_Mode
:= Borrow
;
1038 Current_Checking_Mode
:= Move
;
1041 elsif Is_Deep
(Com_Ty
) then
1043 -- This is certainly named so it is a move
1045 Current_Checking_Mode
:= Move
;
1050 Current_Checking_Mode
:= Move
;
1058 Check_Node
(Expression
(Decl
));
1061 -- If lhs is not a pointer, we still give it the unrestricted
1062 -- state which is useless but not harmful.
1065 Elem
: Perm_Tree_Access
;
1066 Deep
: constant Boolean := Is_Deep
(Target_Typ
);
1069 -- Note that all declared variables are set to the unrestricted
1072 -- If variables are not initialized:
1073 -- unrestricted to every declared object.
1078 -- The assignement R := S is not allowed in the new rules
1079 -- if R is not unrestricted.
1081 -- If variables are initialized:
1082 -- If it is a move, then the target is unrestricted
1083 -- If it is a borrow, then the target is unrestricted
1084 -- If it is an observe, then the target should be observed
1086 if Current_Checking_Mode
= Observe
then
1087 Elem
:= new Perm_Tree_Wrapper
'
1089 (Kind => Entire_Object,
1090 Is_Node_Deep => Deep,
1091 Permission => Observed,
1092 Children_Permission => Observed));
1094 Elem := new Perm_Tree_Wrapper'
1096 (Kind
=> Entire_Object
,
1097 Is_Node_Deep
=> Deep
,
1098 Permission
=> Unrestricted
,
1099 Children_Permission
=> Unrestricted
));
1102 -- Create new tree for defining identifier
1104 Set
(Current_Perm_Env
,
1105 Unique_Entity
(Defining_Identifier
(Decl
)),
1107 pragma Assert
(Get_First
(Current_Perm_Env
) /= null);
1110 when N_Subtype_Declaration
=>
1111 Check_Node
(Subtype_Indication
(Decl
));
1113 when N_Iterator_Specification
=>
1116 when N_Loop_Parameter_Specification
=>
1119 -- Checking should not be called directly on these nodes
1121 when N_Function_Specification
1122 | N_Entry_Declaration
1123 | N_Procedure_Specification
1124 | N_Component_Declaration
1126 raise Program_Error
;
1128 -- Ignored constructs for pointer checking
1130 when N_Formal_Object_Declaration
1131 | N_Formal_Type_Declaration
1132 | N_Incomplete_Type_Declaration
1133 | N_Private_Extension_Declaration
1134 | N_Private_Type_Declaration
1135 | N_Protected_Type_Declaration
1139 -- The following nodes are rewritten by semantic analysis
1141 when N_Expression_Function
=>
1142 raise Program_Error
;
1144 end Check_Declaration
;
1146 ----------------------
1147 -- Check_Expression --
1148 ----------------------
1150 procedure Check_Expression
(Expr
: Node_Id
) is
1151 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
1153 case N_Subexpr
'(Nkind (Expr)) is
1154 when N_Procedure_Call_Statement
1157 Check_Call_Statement (Expr);
1162 -- Check if identifier is pointing to nothing (On/Off/...)
1164 if not Present (Entity (Expr)) then
1168 -- Do not analyze things that are not of object Kind
1170 if Ekind (Entity (Expr)) not in Object_Kind then
1174 -- Consider as ident
1176 Process_Path (Expr);
1178 -- Switch to read mode and then check the readability of each operand
1181 Current_Checking_Mode := Read;
1182 Check_Node (Left_Opnd (Expr));
1183 Check_Node (Right_Opnd (Expr));
1185 -- Switch to read mode and then check the readability of each operand
1192 Current_Checking_Mode := Read;
1193 Check_Node (Right_Opnd (Expr));
1195 -- Forbid all deep expressions for Attribute ???
1196 -- What about generics? (formal parameters).
1198 when N_Attribute_Reference =>
1199 case Attribute_Name (Expr) is
1201 Error_Msg_N ("access attribute not allowed", Expr);
1206 Current_Checking_Mode := Read;
1207 Check_Node (Prefix (Expr));
1210 Current_Checking_Mode := Read;
1211 Check_Node (Prefix (Expr));
1214 Check_List (Expressions (Expr));
1217 Check_Node (Prefix (Expr));
1219 when Name_SPARK_Mode =>
1223 Current_Checking_Mode := Read;
1224 Check_Node (Prefix (Expr));
1227 Check_List (Expressions (Expr));
1228 Check_Node (Prefix (Expr));
1233 Check_List (Expressions (Expr));
1234 Check_Node (Prefix (Expr));
1237 Current_Checking_Mode := Read;
1238 Check_Node (Prefix (Expr));
1240 -- Any Attribute referring to the underlying memory is ignored
1241 -- in the analysis. This means that taking the address of a
1242 -- variable makes a silent alias that is not rejected by the
1247 | Name_Component_Size
1255 -- Attributes referring to types (get values from types), hence
1256 -- no need to check either for borrows or any loans.
1262 -- Other attributes that fall out of the scope of the analysis
1269 Current_Checking_Mode := Read;
1270 Check_Node (Left_Opnd (Expr));
1271 Check_Node (Right_Opnd (Expr));
1274 Current_Checking_Mode := Read;
1275 Check_Node (Left_Opnd (Expr));
1276 Check_Node (Right_Opnd (Expr));
1278 -- Switch to read mode and then check the readability of each operand
1283 Current_Checking_Mode := Read;
1284 Check_Node (Left_Opnd (Expr));
1285 Check_Node (Right_Opnd (Expr));
1287 -- Check the arguments of the call
1289 when N_Explicit_Dereference =>
1290 Process_Path (Expr);
1292 -- Copy environment, run on each branch, and then merge
1294 when N_If_Expression =>
1296 Saved_Env : Perm_Env;
1298 -- Accumulator for the different branches
1301 Elmt : Node_Id := First (Expressions (Expr));
1304 Current_Checking_Mode := Read;
1306 Current_Checking_Mode := Mode_Before;
1310 Copy_Env (Current_Perm_Env, Saved_Env);
1312 -- Here we have the original env in saved, current with a fresh
1313 -- copy, and new aliased.
1320 -- Here the new_environment contains curr env after then block
1323 -- Restore environment before if
1324 Copy_Env (Current_Perm_Env, New_Env);
1325 Free_Env (Current_Perm_Env);
1326 Copy_Env (Saved_Env, Current_Perm_Env);
1328 -- Here new environment contains the environment after then and
1329 -- current the fresh copy of old one.
1336 Copy_Env (New_Env, Current_Perm_Env);
1338 Free_Env (Saved_Env);
1341 when N_Indexed_Component =>
1342 Process_Path (Expr);
1344 -- Analyze the expression that is getting qualified
1346 when N_Qualified_Expression =>
1347 Check_Node (Expression (Expr));
1349 when N_Quantified_Expression =>
1351 Saved_Env : Perm_Env;
1354 Copy_Env (Current_Perm_Env, Saved_Env);
1355 Current_Checking_Mode := Read;
1356 Check_Node (Iterator_Specification (Expr));
1357 Check_Node (Loop_Parameter_Specification (Expr));
1359 Check_Node (Condition (Expr));
1360 Free_Env (Current_Perm_Env);
1361 Copy_Env (Saved_Env, Current_Perm_Env);
1362 Free_Env (Saved_Env);
1364 -- Analyze the list of associations in the aggregate
1367 Check_List (Expressions (Expr));
1368 Check_List (Component_Associations (Expr));
1371 Check_Node (Expression (Expr));
1373 when N_Case_Expression =>
1375 Saved_Env : Perm_Env;
1377 -- Accumulator for the different branches
1380 Elmt : Node_Id := First (Alternatives (Expr));
1383 Current_Checking_Mode := Read;
1384 Check_Node (Expression (Expr));
1385 Current_Checking_Mode := Mode_Before;
1389 Copy_Env (Current_Perm_Env, Saved_Env);
1391 -- Here we have the original env in saved, current with a fresh
1392 -- copy, and new aliased.
1394 -- First alternative
1398 Copy_Env (Current_Perm_Env, New_Env);
1399 Free_Env (Current_Perm_Env);
1401 -- Other alternatives
1403 while Present (Elmt) loop
1405 -- Restore environment
1407 Copy_Env (Saved_Env, Current_Perm_Env);
1413 Copy_Env (Saved_Env, Current_Perm_Env);
1415 Free_Env (Saved_Env);
1417 -- Analyze the list of associates in the aggregate as well as the
1420 when N_Extension_Aggregate =>
1421 Check_Node (Ancestor_Part (Expr));
1422 Check_List (Expressions (Expr));
1425 Check_Node (Low_Bound (Expr));
1426 Check_Node (High_Bound (Expr));
1428 -- We arrived at a path. Process it.
1430 when N_Selected_Component =>
1431 Process_Path (Expr);
1434 Process_Path (Expr);
1436 when N_Type_Conversion =>
1437 Check_Node (Expression (Expr));
1439 when N_Unchecked_Type_Conversion =>
1440 Check_Node (Expression (Expr));
1442 -- Checking should not be called directly on these nodes
1444 when N_Target_Name =>
1445 raise Program_Error;
1447 -- Unsupported constructs in SPARK
1449 when N_Delta_Aggregate =>
1450 Error_Msg_N ("unsupported construct in SPARK", Expr);
1452 -- Ignored constructs for pointer checking
1454 when N_Character_Literal
1456 | N_Numeric_Or_String_Literal
1458 | N_Raise_Expression
1462 -- The following nodes are never generated in GNATprove mode
1464 when N_Expression_With_Actions
1466 | N_Unchecked_Expression
1468 raise Program_Error;
1470 end Check_Expression;
1476 procedure Check_Globals (N : Node_Id) is
1478 if Nkind (N) = N_Empty then
1483 pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
1484 PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
1485 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1490 procedure Process (Mode : Name_Id; The_Global : Entity_Id);
1491 procedure Process (Mode : Name_Id; The_Global : Node_Id) is
1492 Ident_Elt : constant Entity_Id :=
1493 Unique_Entity (Entity (The_Global));
1494 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1497 if Ekind (Ident_Elt) = E_Abstract_State then
1504 Current_Checking_Mode := Observe;
1505 Check_Node (The_Global);
1510 -- ??? Borrow not Move?
1511 Current_Checking_Mode := Borrow;
1512 Check_Node (The_Global);
1515 raise Program_Error;
1517 Current_Checking_Mode := Mode_Before;
1521 if Nkind (Expression (PAA)) = N_Null then
1524 -- No globals, nothing to do
1528 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1533 Process (Name_Input, Expression (PAA));
1535 elsif Nkind (Expression (PAA)) = N_Aggregate
1536 and then Expressions (Expression (PAA)) /= No_List
1538 -- global => (foo, bar)
1541 RHS := First (Expressions (Expression (PAA)));
1542 while Present (RHS) loop
1547 Process (Name_Input, RHS);
1549 when N_Numeric_Or_String_Literal =>
1550 Process (Name_Input, Original_Node (RHS));
1553 raise Program_Error;
1558 elsif Nkind (Expression (PAA)) = N_Aggregate
1559 and then Component_Associations (Expression (PAA)) /= No_List
1561 -- global => (mode => foo,
1562 -- mode => (bar, baz))
1563 -- A mixture of things
1566 CA : constant List_Id :=
1567 Component_Associations (Expression (PAA));
1570 while Present (Row) loop
1571 pragma Assert (List_Length (Choices (Row)) = 1);
1572 The_Mode := Chars (First (Choices (Row)));
1573 RHS := Expression (Row);
1577 RHS := First (Expressions (RHS));
1578 while Present (RHS) loop
1580 when N_Numeric_Or_String_Literal =>
1581 Process (The_Mode, Original_Node (RHS));
1584 Process (The_Mode, RHS);
1592 Process (The_Mode, RHS);
1597 when N_Numeric_Or_String_Literal =>
1598 Process (The_Mode, Original_Node (RHS));
1601 raise Program_Error;
1608 raise Program_Error;
1617 procedure Check_List (L : List_Id) is
1621 while Present (N) loop
1627 --------------------------
1628 -- Check_Loop_Statement --
1629 --------------------------
1631 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1635 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
1636 Loop_Env : constant Perm_Env_Access := new Perm_Env;
1639 -- Save environment prior to the loop
1641 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
1643 -- Add saved environment to loop environment
1645 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
1647 -- If the loop is not a plain-loop, then it may either never be entered,
1648 -- or it may be exited after a number of iterations. Hence add the
1649 -- current permission environment as the initial loop exit environment.
1650 -- Otherwise, the loop exit environment remains empty until it is
1651 -- populated by analyzing exit statements.
1653 if Present (Iteration_Scheme (Loop_N)) then
1655 Exit_Env : constant Perm_Env_Access := new Perm_Env;
1658 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
1659 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
1665 Check_Node (Iteration_Scheme (Loop_N));
1666 Check_List (Statements (Loop_N));
1668 -- Set environment to the one for exiting the loop
1671 Exit_Env : constant Perm_Env_Access :=
1672 Get (Current_Loops_Accumulators, Loop_Name);
1674 Free_Env (Current_Perm_Env);
1676 -- In the normal case, Exit_Env is not null and we use it. In the
1677 -- degraded case of a plain-loop without exit statements, Exit_Env is
1678 -- null, and we use the initial permission environment at the start
1679 -- of the loop to continue analysis. Any environment would be fine
1680 -- here, since the code after the loop is dead code, but this way we
1681 -- avoid spurious errors by having at least variables in scope inside
1684 if Exit_Env /= null then
1685 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
1686 Free_Env (Loop_Env.all);
1687 Free_Env (Exit_Env.all);
1689 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
1690 Free_Env (Loop_Env.all);
1693 end Check_Loop_Statement;
1699 procedure Check_Node (N : Node_Id) is
1700 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1703 when N_Declaration =>
1704 Check_Declaration (N);
1707 Check_Expression (N);
1709 when N_Subtype_Indication =>
1710 Check_Node (Constraint (N));
1713 Check_Node (Get_Body_From_Stub (N));
1715 when N_Statement_Other_Than_Procedure_Call =>
1716 Check_Statement (N);
1718 when N_Package_Body =>
1719 Check_Package_Body (N);
1721 when N_Subprogram_Body
1725 Check_Callable_Body (N);
1727 when N_Protected_Body =>
1728 Check_List (Declarations (N));
1730 when N_Package_Declaration =>
1732 Spec : constant Node_Id := Specification (N);
1735 Current_Checking_Mode := Read;
1736 Check_List (Visible_Declarations (Spec));
1737 Check_List (Private_Declarations (Spec));
1739 Return_Declarations (Visible_Declarations (Spec));
1740 Return_Declarations (Private_Declarations (Spec));
1743 when N_Iteration_Scheme =>
1744 Current_Checking_Mode := Read;
1745 Check_Node (Condition (N));
1746 Check_Node (Iterator_Specification (N));
1747 Check_Node (Loop_Parameter_Specification (N));
1749 when N_Case_Expression_Alternative =>
1750 Current_Checking_Mode := Read;
1751 Check_List (Discrete_Choices (N));
1752 Current_Checking_Mode := Mode_Before;
1753 Check_Node (Expression (N));
1755 when N_Case_Statement_Alternative =>
1756 Current_Checking_Mode := Read;
1757 Check_List (Discrete_Choices (N));
1758 Current_Checking_Mode := Mode_Before;
1759 Check_List (Statements (N));
1761 when N_Component_Association =>
1762 Check_Node (Expression (N));
1764 when N_Handled_Sequence_Of_Statements =>
1765 Check_List (Statements (N));
1767 when N_Parameter_Association =>
1768 Check_Node (Explicit_Actual_Parameter (N));
1770 when N_Range_Constraint =>
1771 Check_Node (Range_Expression (N));
1773 when N_Index_Or_Discriminant_Constraint =>
1774 Check_List (Constraints (N));
1776 -- Checking should not be called directly on these nodes
1778 when N_Abortable_Part
1779 | N_Accept_Alternative
1780 | N_Access_Definition
1781 | N_Access_Function_Definition
1782 | N_Access_Procedure_Definition
1783 | N_Access_To_Object_Definition
1784 | N_Aspect_Specification
1785 | N_Compilation_Unit
1786 | N_Compilation_Unit_Aux
1787 | N_Component_Clause
1788 | N_Component_Definition
1790 | N_Constrained_Array_Definition
1792 | N_Decimal_Fixed_Point_Definition
1793 | N_Defining_Character_Literal
1794 | N_Defining_Identifier
1795 | N_Defining_Operator_Symbol
1796 | N_Defining_Program_Unit_Name
1797 | N_Delay_Alternative
1798 | N_Derived_Type_Definition
1800 | N_Discriminant_Specification
1802 | N_Entry_Body_Formal_Part
1803 | N_Enumeration_Type_Definition
1804 | N_Entry_Call_Alternative
1805 | N_Entry_Index_Specification
1807 | N_Exception_Handler
1808 | N_Floating_Point_Definition
1809 | N_Formal_Decimal_Fixed_Point_Definition
1810 | N_Formal_Derived_Type_Definition
1811 | N_Formal_Discrete_Type_Definition
1812 | N_Formal_Floating_Point_Definition
1813 | N_Formal_Incomplete_Type_Definition
1814 | N_Formal_Modular_Type_Definition
1815 | N_Formal_Ordinary_Fixed_Point_Definition
1816 | N_Formal_Private_Type_Definition
1817 | N_Formal_Signed_Integer_Type_Definition
1818 | N_Generic_Association
1820 | N_Modular_Type_Definition
1821 | N_Ordinary_Fixed_Point_Definition
1822 | N_Package_Specification
1823 | N_Parameter_Specification
1824 | N_Pragma_Argument_Association
1825 | N_Protected_Definition
1826 | N_Push_Pop_xxx_Label
1827 | N_Real_Range_Specification
1828 | N_Record_Definition
1829 | N_SCIL_Dispatch_Table_Tag_Init
1830 | N_SCIL_Dispatching_Call
1831 | N_SCIL_Membership_Test
1832 | N_Signed_Integer_Type_Definition
1835 | N_Terminate_Alternative
1836 | N_Triggering_Alternative
1837 | N_Unconstrained_Array_Definition
1843 raise Program_Error;
1845 -- Unsupported constructs in SPARK
1847 when N_Iterated_Component_Association =>
1848 Error_Msg_N ("unsupported construct in SPARK", N);
1850 -- Ignored constructs for pointer checking
1852 when N_Abstract_Subprogram_Declaration
1854 | N_Attribute_Definition_Clause
1856 | N_Delta_Constraint
1857 | N_Digits_Constraint
1859 | N_Enumeration_Representation_Clause
1860 | N_Exception_Declaration
1861 | N_Exception_Renaming_Declaration
1862 | N_Formal_Package_Declaration
1863 | N_Formal_Subprogram_Declaration
1865 | N_Freeze_Generic_Entity
1866 | N_Function_Instantiation
1867 | N_Generic_Function_Renaming_Declaration
1868 | N_Generic_Package_Declaration
1869 | N_Generic_Package_Renaming_Declaration
1870 | N_Generic_Procedure_Renaming_Declaration
1871 | N_Generic_Subprogram_Declaration
1872 | N_Implicit_Label_Declaration
1875 | N_Number_Declaration
1876 | N_Object_Renaming_Declaration
1878 | N_Package_Instantiation
1879 | N_Package_Renaming_Declaration
1881 | N_Procedure_Instantiation
1882 | N_Record_Representation_Clause
1883 | N_Subprogram_Declaration
1884 | N_Subprogram_Renaming_Declaration
1885 | N_Task_Type_Declaration
1886 | N_Use_Package_Clause
1889 | N_Validate_Unchecked_Conversion
1890 | N_Variable_Reference_Marker
1891 | N_Discriminant_Association
1893 -- ??? check whether we should do sth special for
1894 -- N_Discriminant_Association, or maybe raise a program error.
1897 -- The following nodes are rewritten by semantic analysis
1899 when N_Single_Protected_Declaration
1900 | N_Single_Task_Declaration
1902 raise Program_Error;
1905 Current_Checking_Mode := Mode_Before;
1908 ------------------------
1909 -- Check_Package_Body --
1910 ------------------------
1912 procedure Check_Package_Body (Pack : Node_Id) is
1913 Saved_Env : Perm_Env;
1917 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
1918 if Get_SPARK_Mode_From_Annotation
1919 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
1927 CorSp := Parent (Corresponding_Spec (Pack));
1928 while Nkind (CorSp) /= N_Package_Specification loop
1929 CorSp := Parent (CorSp);
1932 Check_List (Visible_Declarations (CorSp));
1936 Copy_Env (Current_Perm_Env, Saved_Env);
1937 Check_List (Private_Declarations (CorSp));
1939 -- Set mode to Read, and then analyze declarations and statements
1941 Current_Checking_Mode := Read;
1942 Check_List (Declarations (Pack));
1943 Check_Node (Handled_Statement_Sequence (Pack));
1945 -- Check RW for every stateful variable (i.e. in declarations)
1947 Return_Declarations (Private_Declarations (CorSp));
1948 Return_Declarations (Visible_Declarations (CorSp));
1949 Return_Declarations (Declarations (Pack));
1951 -- Restore previous environment (i.e. delete every nonvisible
1952 -- declaration) from environment.
1954 Free_Env (Current_Perm_Env);
1955 Copy_Env (Saved_Env, Current_Perm_Env);
1956 end Check_Package_Body;
1958 --------------------
1959 -- Check_Param_In --
1960 --------------------
1962 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
1963 Mode : constant Entity_Kind := Ekind (Formal);
1964 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1966 case Formal_Kind'(Mode
) is
1968 -- Formal IN parameter
1970 when E_In_Parameter
=>
1972 -- Formal IN parameter, access type
1974 if Is_Access_Type
(Etype
(Formal
)) then
1976 -- Formal IN parameter, access to variable type
1978 if not Is_Access_Constant
(Etype
(Formal
)) then
1980 -- Formal IN parameter, named/anonymous access-to-variable
1983 -- In SPARK, IN access-to-variable is an observe operation
1984 -- for a function, and a borrow operation for a procedure.
1986 if Ekind
(Scope
(Formal
)) = E_Function
then
1987 Current_Checking_Mode
:= Observe
;
1988 Check_Node
(Actual
);
1990 Current_Checking_Mode
:= Borrow
;
1991 Check_Node
(Actual
);
1994 -- Formal IN parameter, access-to-constant type
1995 -- Formal IN parameter, access-to-named-constant type
1997 elsif not Is_Anonymous_Access_Type
(Etype
(Formal
)) then
1998 Error_Msg_N
("assignment not allowed, Ownership Aspect"
1999 & " False (Named general access type)",
2002 -- Formal IN parameter, access to anonymous constant type
2005 Current_Checking_Mode
:= Observe
;
2006 Check_Node
(Actual
);
2009 -- Formal IN parameter, composite type
2011 elsif Is_Deep
(Etype
(Formal
)) then
2013 -- Composite formal types should be named
2014 -- Formal IN parameter, composite named type
2016 Current_Checking_Mode
:= Observe
;
2017 Check_Node
(Actual
);
2020 when E_Out_Parameter
2021 | E_In_Out_Parameter
2026 Current_Checking_Mode
:= Mode_Before
;
2029 ----------------------
2030 -- Check_Param_Out --
2031 ----------------------
2033 procedure Check_Param_Out
(Formal
: Entity_Id
; Actual
: Node_Id
) is
2034 Mode
: constant Entity_Kind
:= Ekind
(Formal
);
2035 Mode_Before
: constant Checking_Mode
:= Current_Checking_Mode
;
2038 case Formal_Kind
'(Mode) is
2040 -- Formal OUT/IN OUT parameter
2042 when E_Out_Parameter
2043 | E_In_Out_Parameter
2046 -- Formal OUT/IN OUT parameter, access type
2048 if Is_Access_Type (Etype (Formal)) then
2050 -- Formal OUT/IN OUT parameter, access to variable type
2052 if not Is_Access_Constant (Etype (Formal)) then
2054 -- Cannot have anonymous out access parameter
2055 -- Formal out/in out parameter, access to named variable
2058 Current_Checking_Mode := Move;
2059 Check_Node (Actual);
2061 -- Formal out/in out parameter, access to constant type
2064 Error_Msg_N ("assignment not allowed, Ownership Aspect False"
2065 & " (Named general access type)", Formal);
2069 -- Formal out/in out parameter, composite type
2071 elsif Is_Deep (Etype (Formal)) then
2073 -- Composite formal types should be named
2074 -- Formal out/in out Parameter, Composite Named type.
2076 Current_Checking_Mode := Borrow;
2077 Check_Node (Actual);
2080 when E_In_Parameter =>
2084 Current_Checking_Mode := Mode_Before;
2085 end Check_Param_Out;
2087 -------------------------
2088 -- Check_Safe_Pointers --
2089 -------------------------
2091 procedure Check_Safe_Pointers (N : Node_Id) is
2093 -- Local subprograms
2095 procedure Check_List (L : List_Id);
2096 -- Call the main analysis procedure on each element of the list
2098 procedure Initialize;
2099 -- Initialize global variables before starting the analysis of a body
2105 procedure Check_List (L : List_Id) is
2109 while Present (N) loop
2110 Check_Safe_Pointers (N);
2119 procedure Initialize is
2121 Reset (Current_Loops_Envs);
2122 Reset (Current_Loops_Accumulators);
2123 Reset (Current_Perm_Env);
2124 Reset (Current_Initialization_Map);
2131 -- SPARK_Mode pragma in application
2133 -- Start of processing for Check_Safe_Pointers
2138 when N_Compilation_Unit =>
2139 Check_Safe_Pointers (Unit (N));
2142 | N_Package_Declaration
2145 Prag := SPARK_Pragma (Defining_Entity (N));
2146 if Present (Prag) then
2147 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
2153 elsif Nkind (N) = N_Package_Body then
2154 Check_List (Declarations (N));
2156 elsif Nkind (N) = N_Package_Declaration then
2157 Check_List (Private_Declarations (Specification (N)));
2158 Check_List (Visible_Declarations (Specification (N)));
2164 end Check_Safe_Pointers;
2166 ---------------------
2167 -- Check_Statement --
2168 ---------------------
2170 procedure Check_Statement (Stmt : Node_Id) is
2171 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2172 State_N : Perm_Kind;
2173 Check : Boolean := True;
2175 Ty_St_Name : Node_Id;
2177 function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
2178 -- Return the root of the name given as input
2180 function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
2182 case Nkind (Comp_Stmt) is
2185 => return Comp_Stmt;
2187 when N_Type_Conversion
2188 | N_Unchecked_Type_Conversion
2189 | N_Qualified_Expression
2191 return Get_Root (Expression (Comp_Stmt));
2193 when N_Parameter_Specification =>
2194 return Get_Root (Defining_Identifier (Comp_Stmt));
2196 when N_Selected_Component
2197 | N_Indexed_Component
2199 | N_Explicit_Dereference
2201 return Get_Root (Prefix (Comp_Stmt));
2204 raise Program_Error;
2209 case N_Statement_Other_Than_Procedure_Call'(Nkind
(Stmt
)) is
2210 when N_Entry_Call_Statement
=>
2211 Check_Call_Statement
(Stmt
);
2213 -- Move right-hand side first, and then assign left-hand side
2215 when N_Assignment_Statement
=>
2217 St_Name
:= Name
(Stmt
);
2218 Ty_St_Name
:= Etype
(Name
(Stmt
));
2220 -- Check that is not a *general* access type
2222 if Has_Ownership_Aspect_True
(St_Name
, "assigning to") then
2224 -- Assigning to access type
2226 if Is_Access_Type
(Ty_St_Name
) then
2228 -- Assigning to access to variable type
2230 if not Is_Access_Constant
(Ty_St_Name
) then
2232 -- Assigning to named access to variable type
2234 if not Is_Anonymous_Access_Type
(Ty_St_Name
) then
2235 Current_Checking_Mode
:= Move
;
2237 -- Assigning to anonymous access to variable type
2240 -- Target /= source root
2242 if Nkind_In
(Expression
(Stmt
), N_Allocator
, N_Null
)
2243 or else Entity
(St_Name
) /=
2244 Entity
(Get_Root
(Expression
(Stmt
)))
2246 Error_Msg_N
("assignment not allowed, anonymous "
2247 & "access Object with Different Root",
2251 -- Target = source root
2254 -- Here we do nothing on the source nor on the
2255 -- target. However, we check the the legality rule:
2256 -- "The source shall be an owning access object
2257 -- denoted by a name that is not in the observed
2260 State_N
:= Get_Perm
(Expression
(Stmt
));
2261 if State_N
= Observed
then
2262 Error_Msg_N
("assignment not allowed, Anonymous "
2263 & "access object with the same root"
2264 & " but source Observed", Stmt
);
2270 -- else access-to-constant
2272 -- Assigning to anonymous access-to-constant type
2274 elsif Is_Anonymous_Access_Type
(Ty_St_Name
) then
2276 -- ??? Check the follwing condition. We may have to
2277 -- add that the root is in the observed state too.
2279 State_N
:= Get_Perm
(Expression
(Stmt
));
2280 if State_N
/= Observed
then
2281 Error_Msg_N
("assignment not allowed, anonymous "
2282 & "access-to-constant object not in "
2283 & "the observed state)", Stmt
);
2287 Error_Msg_N
("?here check accessibility level cited in"
2288 & " the second legality rule of assign",
2293 -- Assigning to named access-to-constant type:
2294 -- This case should have been detected when checking
2295 -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
2298 raise Program_Error
;
2301 -- Assigning to composite (deep) type.
2303 elsif Is_Deep
(Ty_St_Name
) then
2304 if Ekind_In
(Ty_St_Name
,
2310 First_Component_Or_Discriminant
(Ty_St_Name
);
2313 while Present
(Elmt
) loop
2314 if Is_Anonymous_Access_Type
(Etype
(Elmt
)) or
2315 Ekind
(Elmt
) = E_General_Access_Type
2317 Error_Msg_N
("assignment not allowed, Ownership "
2318 & "Aspect False (Components have "
2319 & "Ownership Aspect False)", Stmt
);
2324 Next_Component_Or_Discriminant
(Elmt
);
2328 -- Record types are always named so this is a move
2331 Current_Checking_Mode
:= Move
;
2334 elsif Ekind_In
(Ty_St_Name
,
2339 Current_Checking_Mode
:= Move
;
2342 -- Now handle legality rules of using a borrowed, observed,
2343 -- or moved name as a prefix in an assignment.
2346 if Nkind_In
(St_Name
,
2347 N_Attribute_Reference
,
2349 N_Explicit_Dereference
,
2350 N_Indexed_Component
,
2352 N_Selected_Component
,
2356 if Is_Access_Type
(Etype
(Prefix
(St_Name
))) or
2357 Is_Deep
(Etype
(Prefix
(St_Name
)))
2360 -- We set the Check variable to True so that we can
2361 -- Check_Node of the expression and the name first
2362 -- under the assumption of Current_Checking_Mode =
2363 -- Read => nothing to be done for the RHS if the
2364 -- following check on the expression fails, and
2365 -- Current_Checking_Mode := Assign => the name should
2366 -- not be borrowed or observed so that we can use it
2367 -- as a prefix in the target of an assignement.
2369 -- Note that we do not need to check the OA here
2370 -- because we are allowed to read and write "through"
2371 -- an object of OAF (example: traversing a DS).
2377 if Nkind_In
(Expression
(Stmt
),
2378 N_Attribute_Reference
,
2380 N_Explicit_Dereference
,
2381 N_Indexed_Component
,
2383 N_Selected_Component
,
2387 if Is_Access_Type
(Etype
(Prefix
(Expression
(Stmt
))))
2388 or else Is_Deep
(Etype
(Prefix
(Expression
(Stmt
))))
2390 Current_Checking_Mode
:= Observe
;
2397 Check_Node
(Expression
(Stmt
));
2398 Current_Checking_Mode
:= Assign
;
2399 Check_Node
(St_Name
);
2403 when N_Block_Statement
=>
2405 Saved_Env
: Perm_Env
;
2409 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2411 -- Analyze declarations and Handled_Statement_Sequences
2413 Current_Checking_Mode
:= Read
;
2414 Check_List
(Declarations
(Stmt
));
2415 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2417 -- Restore environment
2419 Free_Env
(Current_Perm_Env
);
2420 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2423 when N_Case_Statement
=>
2425 Saved_Env
: Perm_Env
;
2427 -- Accumulator for the different branches
2430 Elmt
: Node_Id
:= First
(Alternatives
(Stmt
));
2433 Current_Checking_Mode
:= Read
;
2434 Check_Node
(Expression
(Stmt
));
2435 Current_Checking_Mode
:= Mode_Before
;
2439 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2441 -- Here we have the original env in saved, current with a fresh
2442 -- copy, and new aliased.
2444 -- First alternative
2448 Copy_Env
(Current_Perm_Env
, New_Env
);
2449 Free_Env
(Current_Perm_Env
);
2451 -- Other alternatives
2453 while Present
(Elmt
) loop
2455 -- Restore environment
2457 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2462 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2464 Free_Env
(Saved_Env
);
2467 when N_Delay_Relative_Statement
=>
2468 Check_Node
(Expression
(Stmt
));
2470 when N_Delay_Until_Statement
=>
2471 Check_Node
(Expression
(Stmt
));
2473 when N_Loop_Statement
=>
2474 Check_Loop_Statement
(Stmt
);
2476 -- If deep type expression, then move, else read
2478 when N_Simple_Return_Statement
=>
2479 case Nkind
(Expression
(Stmt
)) is
2482 -- ??? This does not take into account the fact that
2483 -- a simple return inside an extended return statement
2484 -- applies to the extended return statement.
2485 Subp
: constant Entity_Id
:=
2486 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2488 Return_Globals
(Subp
);
2492 if Is_Deep
(Etype
(Expression
(Stmt
))) then
2493 Current_Checking_Mode
:= Move
;
2499 Check_Node
(Expression
(Stmt
));
2503 when N_Extended_Return_Statement
=>
2504 Check_List
(Return_Object_Declarations
(Stmt
));
2505 Check_Node
(Handled_Statement_Sequence
(Stmt
));
2506 Return_Declarations
(Return_Object_Declarations
(Stmt
));
2508 -- ??? This does not take into account the fact that a simple
2509 -- return inside an extended return statement applies to the
2510 -- extended return statement.
2511 Subp
: constant Entity_Id
:=
2512 Return_Applies_To
(Return_Statement_Entity
(Stmt
));
2515 Return_Globals
(Subp
);
2518 -- Nothing to do when exiting a loop. No merge needed
2520 when N_Exit_Statement
=>
2523 -- Copy environment, run on each branch
2525 when N_If_Statement
=>
2527 Saved_Env
: Perm_Env
;
2529 -- Accumulator for the different branches
2534 Check_Node
(Condition
(Stmt
));
2538 Copy_Env
(Current_Perm_Env
, Saved_Env
);
2540 -- Here we have the original env in saved, current with a fresh
2545 Check_List
(Then_Statements
(Stmt
));
2546 Copy_Env
(Current_Perm_Env
, New_Env
);
2547 Free_Env
(Current_Perm_Env
);
2549 -- Here the new_environment contains curr env after then block
2557 Elmt
:= First
(Elsif_Parts
(Stmt
));
2558 while Present
(Elmt
) loop
2560 -- Transfer into accumulator, and restore from save
2562 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2563 Check_Node
(Condition
(Elmt
));
2564 Check_List
(Then_Statements
(Stmt
));
2571 -- Restore environment before if
2573 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2575 -- Here new environment contains the environment after then and
2576 -- current the fresh copy of old one.
2578 Check_List
(Else_Statements
(Stmt
));
2582 Copy_Env
(Saved_Env
, Current_Perm_Env
);
2585 Free_Env
(Saved_Env
);
2588 -- Unsupported constructs in SPARK
2590 when N_Abort_Statement
2591 | N_Accept_Statement
2592 | N_Asynchronous_Select
2594 | N_Conditional_Entry_Call
2596 | N_Requeue_Statement
2597 | N_Selective_Accept
2598 | N_Timed_Entry_Call
2600 Error_Msg_N
("unsupported construct in SPARK", Stmt
);
2602 -- Ignored constructs for pointer checking
2604 when N_Null_Statement
2609 -- The following nodes are never generated in GNATprove mode
2611 when N_Compound_Statement
2614 raise Program_Error
;
2616 end Check_Statement
;
2622 function Get_Perm
(N
: Node_Id
) return Perm_Kind
is
2623 Tree_Or_Perm
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(N
);
2626 case Tree_Or_Perm
.R
is
2628 return Tree_Or_Perm
.Found_Permission
;
2631 pragma Assert
(Tree_Or_Perm
.Tree_Access
/= null);
2632 return Permission
(Tree_Or_Perm
.Tree_Access
);
2634 -- We encoutered a function call, hence the memory area is fresh,
2635 -- which means that the association permission is RW.
2637 when Function_Call
=>
2638 return Unrestricted
;
2642 ----------------------
2643 -- Get_Perm_Or_Tree --
2644 ----------------------
2646 function Get_Perm_Or_Tree
(N
: Node_Id
) return Perm_Or_Tree
is
2650 -- Base identifier. Normally those are the roots of the trees stored
2651 -- in the permission environment.
2653 when N_Defining_Identifier
=>
2654 raise Program_Error
;
2660 P
: constant Entity_Id
:= Entity
(N
);
2661 C
: constant Perm_Tree_Access
:=
2662 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2665 -- Setting the initialization map to True, so that this
2666 -- variable cannot be ignored anymore when looking at end
2667 -- of elaboration of package.
2669 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2671 -- No null possible here, there are no parents for the path.
2672 -- This means we are using a global variable without adding
2673 -- it in environment with a global aspect.
2675 Illegal_Global_Usage
(N
);
2678 return (R
=> Unfolded
, Tree_Access
=> C
);
2682 when N_Type_Conversion
2683 | N_Unchecked_Type_Conversion
2684 | N_Qualified_Expression
2686 return Get_Perm_Or_Tree
(Expression
(N
));
2688 -- Happening when we try to get the permission of a variable that
2689 -- is a formal parameter. We get instead the defining identifier
2690 -- associated with the parameter (which is the one that has been
2691 -- stored for indexing).
2693 when N_Parameter_Specification
=>
2694 return Get_Perm_Or_Tree
(Defining_Identifier
(N
));
2696 -- We get the permission tree of its prefix, and then get either the
2697 -- subtree associated with that specific selection, or if we have a
2698 -- leaf that folds its children, we take the children's permission
2699 -- and return it using the discriminant Folded.
2701 when N_Selected_Component
=>
2703 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2713 pragma Assert
(C
.Tree_Access
/= null);
2714 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2716 Kind
(C
.Tree_Access
) = Record_Component
);
2718 if Kind
(C
.Tree_Access
) = Record_Component
then
2720 Selected_Component
: constant Entity_Id
:=
2721 Entity
(Selector_Name
(N
));
2722 Selected_C
: constant Perm_Tree_Access
:=
2724 (Component
(C
.Tree_Access
), Selected_Component
);
2727 if Selected_C
= null then
2728 return (R
=> Unfolded
,
2730 Other_Components
(C
.Tree_Access
));
2733 return (R
=> Unfolded
,
2734 Tree_Access
=> Selected_C
);
2738 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2739 return (R
=> Folded
,
2741 Children_Permission
(C
.Tree_Access
));
2744 raise Program_Error
;
2748 -- We get the permission tree of its prefix, and then get either the
2749 -- subtree associated with that specific selection, or if we have a
2750 -- leaf that folds its children, we take the children's permission
2751 -- and return it using the discriminant Folded.
2753 when N_Indexed_Component
2757 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2767 pragma Assert
(C
.Tree_Access
/= null);
2768 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2770 Kind
(C
.Tree_Access
) = Array_Component
);
2772 if Kind
(C
.Tree_Access
) = Array_Component
then
2773 pragma Assert
(Get_Elem
(C
.Tree_Access
) /= null);
2774 return (R
=> Unfolded
,
2775 Tree_Access
=> Get_Elem
(C
.Tree_Access
));
2777 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2778 return (R
=> Folded
, Found_Permission
=>
2779 Children_Permission
(C
.Tree_Access
));
2782 raise Program_Error
;
2786 -- We get the permission tree of its prefix, and then get either the
2787 -- subtree associated with that specific selection, or if we have a
2788 -- leaf that folds its children, we take the children's permission
2789 -- and return it using the discriminant Folded.
2791 when N_Explicit_Dereference
=>
2793 C
: constant Perm_Or_Tree
:= Get_Perm_Or_Tree
(Prefix
(N
));
2803 pragma Assert
(C
.Tree_Access
/= null);
2804 pragma Assert
(Kind
(C
.Tree_Access
) = Entire_Object
2806 Kind
(C
.Tree_Access
) = Reference
);
2808 if Kind
(C
.Tree_Access
) = Reference
then
2809 if Get_All
(C
.Tree_Access
) = null then
2813 raise Program_Error
;
2818 Tree_Access
=> Get_All
(C
.Tree_Access
));
2821 elsif Kind
(C
.Tree_Access
) = Entire_Object
then
2822 return (R
=> Folded
, Found_Permission
=>
2823 Children_Permission
(C
.Tree_Access
));
2826 raise Program_Error
;
2830 -- The name contains a function call, hence the given path is always
2831 -- new. We do not have to check for anything.
2833 when N_Function_Call
=>
2834 return (R
=> Function_Call
);
2837 raise Program_Error
;
2839 end Get_Perm_Or_Tree
;
2845 function Get_Perm_Tree
(N
: Node_Id
) return Perm_Tree_Access
is
2849 -- Base identifier. Normally those are the roots of the trees stored
2850 -- in the permission environment.
2852 when N_Defining_Identifier
=>
2853 raise Program_Error
;
2859 P
: constant Node_Id
:= Entity
(N
);
2860 C
: constant Perm_Tree_Access
:=
2861 Get
(Current_Perm_Env
, Unique_Entity
(P
));
2864 -- Setting the initialization map to True, so that this
2865 -- variable cannot be ignored anymore when looking at end
2866 -- of elaboration of package.
2868 Set
(Current_Initialization_Map
, Unique_Entity
(P
), True);
2870 -- No null possible here, there are no parents for the path.
2871 -- This means we are using a global variable without adding
2872 -- it in environment with a global aspect.
2874 Illegal_Global_Usage
(N
);
2881 when N_Type_Conversion
2882 | N_Unchecked_Type_Conversion
2883 | N_Qualified_Expression
2885 return Get_Perm_Tree
(Expression
(N
));
2887 when N_Parameter_Specification
=>
2888 return Get_Perm_Tree
(Defining_Identifier
(N
));
2890 -- We get the permission tree of its prefix, and then get either the
2891 -- subtree associated with that specific selection, or if we have a
2892 -- leaf that folds its children, we unroll it in one step.
2894 when N_Selected_Component
=>
2896 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
2901 -- If null then it means we went through a function call
2906 pragma Assert
(Kind
(C
) = Entire_Object
2907 or else Kind
(C
) = Record_Component
);
2909 if Kind
(C
) = Record_Component
then
2911 -- The tree is unfolded. We just return the subtree.
2914 Selected_Component
: constant Entity_Id
:=
2915 Entity
(Selector_Name
(N
));
2916 Selected_C
: constant Perm_Tree_Access
:=
2918 (Component
(C
), Selected_Component
);
2921 if Selected_C
= null then
2922 return Other_Components
(C
);
2927 elsif Kind
(C
) = Entire_Object
then
2929 -- Expand the tree. Replace the node with
2930 -- Record_Component.
2934 -- Create the unrolled nodes
2936 Son
: Perm_Tree_Access
;
2938 Child_Perm
: constant Perm_Kind
:=
2939 Children_Permission
(C
);
2942 -- We change the current node from Entire_Object to
2943 -- Record_Component with same permission and an empty
2944 -- hash table as component list.
2947 (Kind
=> Record_Component
,
2948 Is_Node_Deep
=> Is_Node_Deep
(C
),
2949 Permission
=> Permission
(C
),
2950 Component
=> Perm_Tree_Maps
.Nil
,
2952 new Perm_Tree_Wrapper
'
2954 (Kind => Entire_Object,
2955 -- Is_Node_Deep is true, to be conservative
2956 Is_Node_Deep => True,
2957 Permission => Child_Perm,
2958 Children_Permission => Child_Perm)
2962 -- We fill the hash table with all sons of the record,
2963 -- with basic Entire_Objects nodes.
2965 Elem := First_Component_Or_Discriminant
2966 (Etype (Prefix (N)));
2968 while Present (Elem) loop
2969 Son := new Perm_Tree_Wrapper'
2971 (Kind
=> Entire_Object
,
2972 Is_Node_Deep
=> Is_Deep
(Etype
(Elem
)),
2973 Permission
=> Child_Perm
,
2974 Children_Permission
=> Child_Perm
));
2977 (C
.all.Tree
.Component
, Elem
, Son
);
2978 Next_Component_Or_Discriminant
(Elem
);
2980 -- we return the tree to the sons, so that the recursion
2984 Selected_Component
: constant Entity_Id
:=
2985 Entity
(Selector_Name
(N
));
2987 Selected_C
: constant Perm_Tree_Access
:=
2989 (Component
(C
), Selected_Component
);
2992 pragma Assert
(Selected_C
/= null);
2997 raise Program_Error
;
3000 -- We set the permission tree of its prefix, and then we extract from
3001 -- the returned pointer the subtree. If folded, we unroll the tree at
3004 when N_Indexed_Component
3008 C
: constant Perm_Tree_Access
:= Get_Perm_Tree
(Prefix
(N
));
3012 -- If null then we went through a function call
3016 pragma Assert
(Kind
(C
) = Entire_Object
3017 or else Kind
(C
) = Array_Component
);
3019 if Kind
(C
) = Array_Component
then
3021 -- The tree is unfolded. We just return the elem subtree
3023 pragma Assert
(Get_Elem
(C
) = null);
3024 return Get_Elem
(C
);
3026 elsif Kind
(C
) = Entire_Object
then
3028 -- Expand the tree. Replace node with Array_Component.
3030 Son
: Perm_Tree_Access
;
3033 Son
:= new Perm_Tree_Wrapper
'
3035 (Kind => Entire_Object,
3036 Is_Node_Deep => Is_Node_Deep (C),
3037 Permission => Children_Permission (C),
3038 Children_Permission => Children_Permission (C)));
3040 -- We change the current node from Entire_Object
3041 -- to Array_Component with same permission and the
3042 -- previously defined son.
3044 C.all.Tree := (Kind => Array_Component,
3045 Is_Node_Deep => Is_Node_Deep (C),
3046 Permission => Permission (C),
3048 return Get_Elem (C);
3051 raise Program_Error;
3054 -- We get the permission tree of its prefix, and then get either the
3055 -- subtree associated with that specific selection, or if we have a
3056 -- leaf that folds its children, we unroll the tree.
3058 when N_Explicit_Dereference =>
3060 C : Perm_Tree_Access;
3063 C := Get_Perm_Tree (Prefix (N));
3067 -- If null, we went through a function call
3072 pragma Assert (Kind (C) = Entire_Object
3073 or else Kind (C) = Reference);
3075 if Kind (C) = Reference then
3077 -- The tree is unfolded. We return the elem subtree
3079 if Get_All (C) = null then
3083 raise Program_Error;
3087 elsif Kind (C) = Entire_Object then
3089 -- Expand the tree. Replace the node with Reference.
3091 Son : Perm_Tree_Access;
3094 Son := new Perm_Tree_Wrapper'
3096 (Kind
=> Entire_Object
,
3097 Is_Node_Deep
=> Is_Deep
(Etype
(N
)),
3098 Permission
=> Children_Permission
(C
),
3099 Children_Permission
=> Children_Permission
(C
)));
3101 -- We change the current node from Entire_Object to
3102 -- Reference with same permission and the previous son.
3104 pragma Assert
(Is_Node_Deep
(C
));
3105 C
.all.Tree
:= (Kind
=> Reference
,
3106 Is_Node_Deep
=> Is_Node_Deep
(C
),
3107 Permission
=> Permission
(C
),
3112 raise Program_Error
;
3115 -- No permission tree for function calls
3117 when N_Function_Call
=>
3121 raise Program_Error
;
3129 procedure Hp
(P
: Perm_Env
) is
3130 Elem
: Perm_Tree_Maps
.Key_Option
;
3133 Elem
:= Get_First_Key
(P
);
3134 while Elem
.Present
loop
3135 Print_Node_Briefly
(Elem
.K
);
3136 Elem
:= Get_Next_Key
(P
);
3140 --------------------------
3141 -- Illegal_Global_Usage --
3142 --------------------------
3144 procedure Illegal_Global_Usage
(N
: Node_Or_Entity_Id
) is
3146 Error_Msg_NE
("cannot use global variable & of deep type", N
, N
);
3147 Error_Msg_N
("\without prior declaration in a Global aspect", N
);
3148 Errout
.Finalize
(Last_Call
=> True);
3149 Errout
.Output_Messages
;
3150 Exit_Program
(E_Errors
);
3151 end Illegal_Global_Usage
;
3157 function Is_Deep
(E
: Entity_Id
) return Boolean is
3158 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean;
3159 function Is_Private_Entity_Mode_Off
(E
: Entity_Id
) return Boolean is
3161 Pack_Decl
: Node_Id
;
3164 if Is_Itype
(E
) then
3165 Decl
:= Associated_Node_For_Itype
(E
);
3170 Pack_Decl
:= Parent
(Parent
(Decl
));
3172 if Nkind
(Pack_Decl
) /= N_Package_Declaration
then
3177 Present
(SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
)))
3178 and then Get_SPARK_Mode_From_Annotation
3179 (SPARK_Aux_Pragma
(Defining_Entity
(Pack_Decl
))) = Off
;
3180 end Is_Private_Entity_Mode_Off
;
3183 pragma Assert
(Is_Type
(E
));
3191 -- Just check the depth of its component type
3196 return Is_Deep
(Component_Type
(E
));
3198 when E_String_Literal_Subtype
=>
3201 -- Per RM 8.11 for class-wide types
3203 when E_Class_Wide_Subtype
3208 -- ??? What about hidden components
3217 Elmt
:= First_Component_Or_Discriminant
(E
);
3218 while Present
(Elmt
) loop
3219 if Is_Deep
(Etype
(Elmt
)) then
3222 Next_Component_Or_Discriminant
(Elmt
);
3228 when Private_Kind
=>
3229 if Is_Private_Entity_Mode_Off
(E
) then
3232 if Present
(Full_View
(E
)) then
3233 return Is_Deep
(Full_View
(E
));
3239 when E_Incomplete_Type
3240 | E_Incomplete_Subtype
3244 -- No problem with synchronized types
3246 when E_Protected_Type
3247 | E_Protected_Subtype
3253 when E_Exception_Type
=>
3257 raise Program_Error
;
3265 procedure Perm_Error
3268 Found_Perm
: Perm_Kind
)
3270 procedure Set_Root_Object
3272 Obj
: out Entity_Id
;
3273 Deref
: out Boolean);
3274 -- Set the root object Obj, and whether the path contains a dereference,
3275 -- from a path Path.
3277 ---------------------
3278 -- Set_Root_Object --
3279 ---------------------
3281 procedure Set_Root_Object
3283 Obj
: out Entity_Id
;
3284 Deref
: out Boolean)
3287 case Nkind
(Path
) is
3291 Obj
:= Entity
(Path
);
3294 when N_Type_Conversion
3295 | N_Unchecked_Type_Conversion
3296 | N_Qualified_Expression
3298 Set_Root_Object
(Expression
(Path
), Obj
, Deref
);
3300 when N_Indexed_Component
3301 | N_Selected_Component
3304 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3306 when N_Explicit_Dereference
=>
3307 Set_Root_Object
(Prefix
(Path
), Obj
, Deref
);
3311 raise Program_Error
;
3313 end Set_Root_Object
;
3319 -- Start of processing for Perm_Error
3322 Set_Root_Object
(N
, Root
, Is_Deref
);
3326 ("insufficient permission on dereference from &", N
, Root
);
3328 Error_Msg_NE
("insufficient permission for &", N
, Root
);
3331 Perm_Mismatch
(Perm
, Found_Perm
, N
);
3334 -------------------------------
3335 -- Perm_Error_Subprogram_End --
3336 -------------------------------
3338 procedure Perm_Error_Subprogram_End
3342 Found_Perm
: Perm_Kind
)
3345 Error_Msg_Node_2
:= Subp
;
3346 Error_Msg_NE
("insufficient permission for & when returning from &",
3348 Perm_Mismatch
(Perm
, Found_Perm
, Subp
);
3349 end Perm_Error_Subprogram_End
;
3355 procedure Process_Path
(N
: Node_Id
) is
3356 Root
: constant Entity_Id
:= Get_Enclosing_Object
(N
);
3357 State_N
: Perm_Kind
;
3359 -- We ignore if yielding to synchronized
3362 and then Is_Synchronized_Object
(Root
)
3367 State_N
:= Get_Perm
(N
);
3369 case Current_Checking_Mode
is
3371 -- Check permission R, do nothing
3375 -- This condition should be removed when removing the read
3382 -- The rhs object in an assignment statement (including copy in
3383 -- and copy back) should be in the Unrestricted or Moved state.
3384 -- Otherwise the move is not allowed.
3385 -- This applies to both stand-alone and composite objects.
3386 -- If the state of the source is Moved, then a warning message
3387 -- is prompt to make the user aware of reading a nullified
3390 if State_N
/= Unrestricted
and State_N
/= Moved
then
3391 Perm_Error
(N
, Unrestricted
, State_N
);
3395 -- In the AI, after moving a path nothing to do since the rhs
3396 -- object was in the Unrestricted state and it shall be
3397 -- refreshed to Unrestricted. The object should be nullified
3398 -- however. To avoid moving again a name that has already been
3399 -- moved, in this implementation we set the state of the moved
3400 -- object to "Moved". This shall be used to prompt a warning
3401 -- when manipulating a null pointer and also to implement
3402 -- the no aliasing parameter restriction.
3404 if State_N
= Moved
then
3405 Error_Msg_N
("?the source or one of its extensions has"
3406 & " already been moved", N
);
3410 -- Set state to Moved to the path and any of its prefixes
3412 Tree
: constant Perm_Tree_Access
:=
3413 Set_Perm_Prefixes
(N
, Moved
);
3418 -- We went through a function call, no permission to
3424 -- Set state to Moved on any strict extension of the path
3426 Set_Perm_Extensions
(Tree
, Moved
);
3431 -- The lhs object in an assignment statement (including copy in
3432 -- and copy back) should be in the Unrestricted state.
3433 -- Otherwise the move is not allowed.
3434 -- This applies to both stand-alone and composite objects.
3436 if State_N
/= Unrestricted
and State_N
/= Moved
then
3437 Perm_Error
(N
, Unrestricted
, State_N
);
3441 -- After assigning to a path nothing to do since it was in the
3442 -- Unrestricted state and it would be refreshed to
3447 -- Borrowing is only allowed on Unrestricted objects.
3449 if State_N
/= Unrestricted
and State_N
/= Moved
then
3450 Perm_Error
(N
, Unrestricted
, State_N
);
3453 if State_N
= Moved
then
3454 Error_Msg_N
("?the source or one of its extensions has"
3455 & " already been moved", N
);
3459 -- Set state to Borrowed to the path and any of its prefixes
3461 Tree
: constant Perm_Tree_Access
:=
3462 Set_Perm_Prefixes
(N
, Borrowed
);
3467 -- We went through a function call, no permission to
3473 -- Set state to Borrowed on any strict extension of the path
3475 Set_Perm_Extensions
(Tree
, Borrowed
);
3479 if State_N
/= Unrestricted
3480 and then State_N
/= Observed
3482 Perm_Error
(N
, Observed
, State_N
);
3486 -- Set permission to Observed on the path and any of its
3487 -- prefixes if it is of a deep type. Actually, some operation
3488 -- like reading from an object of access type is considered as
3489 -- observe while it should not affect the permissions of
3490 -- the considered tree.
3492 Tree
: Perm_Tree_Access
;
3495 if Is_Deep
(Etype
(N
)) then
3496 Tree
:= Set_Perm_Prefixes
(N
, Observed
);
3503 -- We went through a function call, no permission to
3509 -- Set permissions to No on any strict extension of the path
3511 Set_Perm_Extensions
(Tree
, Observed
);
3516 -------------------------
3517 -- Return_Declarations --
3518 -------------------------
3520 procedure Return_Declarations
(L
: List_Id
) is
3521 procedure Return_Declaration
(Decl
: Node_Id
);
3522 -- Check correct permissions for every declared object
3524 ------------------------
3525 -- Return_Declaration --
3526 ------------------------
3528 procedure Return_Declaration
(Decl
: Node_Id
) is
3530 if Nkind
(Decl
) = N_Object_Declaration
then
3532 -- Check RW for object declared, unless the object has never been
3535 if Get
(Current_Initialization_Map
,
3536 Unique_Entity
(Defining_Identifier
(Decl
))) = False
3542 Elem
: constant Perm_Tree_Access
:=
3543 Get
(Current_Perm_Env
,
3544 Unique_Entity
(Defining_Identifier
(Decl
)));
3549 -- Here we are on a declaration. Hence it should have been
3550 -- added in the environment when analyzing this node with
3551 -- mode Read. Hence it is not possible to find a null
3556 raise Program_Error
;
3559 if Permission
(Elem
) /= Unrestricted
then
3560 Perm_Error
(Decl
, Unrestricted
, Permission
(Elem
));
3564 end Return_Declaration
;
3569 -- Start of processing for Return_Declarations
3573 while Present
(N
) loop
3574 Return_Declaration
(N
);
3577 end Return_Declarations
;
3579 --------------------
3580 -- Return_Globals --
3581 --------------------
3583 procedure Return_Globals
(Subp
: Entity_Id
) is
3584 procedure Return_Globals_From_List
3585 (First_Item
: Node_Id
;
3586 Kind
: Formal_Kind
);
3587 -- Return global items from the list starting at Item
3589 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
);
3590 -- Return global items for the mode Global_Mode
3592 ------------------------------
3593 -- Return_Globals_From_List --
3594 ------------------------------
3596 procedure Return_Globals_From_List
3597 (First_Item
: Node_Id
;
3600 Item
: Node_Id
:= First_Item
;
3604 while Present
(Item
) loop
3607 -- Ignore abstract states, which play no role in pointer aliasing
3609 if Ekind
(E
) = E_Abstract_State
then
3612 Return_The_Global
(E
, Kind
, Subp
);
3616 end Return_Globals_From_List
;
3618 ----------------------------
3619 -- Return_Globals_Of_Mode --
3620 ----------------------------
3622 procedure Return_Globals_Of_Mode
(Global_Mode
: Name_Id
) is
3630 Kind
:= E_In_Parameter
;
3632 Kind
:= E_Out_Parameter
;
3634 Kind
:= E_In_Out_Parameter
;
3636 raise Program_Error
;
3639 -- Return both global items from Global and Refined_Global pragmas
3641 Return_Globals_From_List
(First_Global
(Subp
, Global_Mode
), Kind
);
3642 Return_Globals_From_List
3643 (First_Global
(Subp
, Global_Mode
, Refined
=> True), Kind
);
3644 end Return_Globals_Of_Mode
;
3646 -- Start of processing for Return_Globals
3649 Return_Globals_Of_Mode
(Name_Proof_In
);
3650 Return_Globals_Of_Mode
(Name_Input
);
3651 Return_Globals_Of_Mode
(Name_Output
);
3652 Return_Globals_Of_Mode
(Name_In_Out
);
3655 --------------------------------
3656 -- Return_Parameter_Or_Global --
3657 --------------------------------
3659 procedure Return_The_Global
3664 Elem
: constant Perm_Tree_Access
:= Get
(Current_Perm_Env
, Id
);
3665 pragma Assert
(Elem
/= null);
3668 -- Observed IN parameters and globals need not return a permission to
3671 if Mode
= E_In_Parameter
3673 -- Check this for read-only globals.
3676 if Permission
(Elem
) /= Unrestricted
3677 and then Permission
(Elem
) /= Observed
3679 Perm_Error_Subprogram_End
3683 Found_Perm
=> Permission
(Elem
));
3686 -- All globals of mode out or in/out should return with mode
3690 if Permission
(Elem
) /= Unrestricted
then
3691 Perm_Error_Subprogram_End
3694 Perm
=> Unrestricted
,
3695 Found_Perm
=> Permission
(Elem
));
3698 end Return_The_Global
;
3700 -------------------------
3701 -- Set_Perm_Extensions --
3702 -------------------------
3704 procedure Set_Perm_Extensions
(T
: Perm_Tree_Access
; P
: Perm_Kind
) is
3705 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
);
3706 procedure Free_Perm_Tree_Children
(T
: Perm_Tree_Access
) is
3709 when Entire_Object
=>
3713 Free_Perm_Tree
(T
.all.Tree
.Get_All
);
3715 when Array_Component
=>
3716 Free_Perm_Tree
(T
.all.Tree
.Get_Elem
);
3718 -- Free every Component subtree
3720 when Record_Component
=>
3722 Comp
: Perm_Tree_Access
;
3725 Comp
:= Perm_Tree_Maps
.Get_First
(Component
(T
));
3726 while Comp
/= null loop
3727 Free_Perm_Tree
(Comp
);
3728 Comp
:= Perm_Tree_Maps
.Get_Next
(Component
(T
));
3731 Free_Perm_Tree
(T
.all.Tree
.Other_Components
);
3734 end Free_Perm_Tree_Children
;
3736 Son
: constant Perm_Tree
:=
3738 (Kind => Entire_Object,
3739 Is_Node_Deep => Is_Node_Deep (T),
3740 Permission => Permission (T),
3741 Children_Permission => P);
3744 Free_Perm_Tree_Children (T);
3746 end Set_Perm_Extensions;
3748 ------------------------------
3749 -- Set_Perm_Prefixes --
3750 ------------------------------
3752 function Set_Perm_Prefixes
3754 New_Perm : Perm_Kind)
3755 return Perm_Tree_Access
3763 | N_Defining_Identifier
3765 if Nkind (N) = N_Defining_Identifier
3766 and then New_Perm = Borrowed
3768 raise Program_Error;
3773 C : Perm_Tree_Access;
3776 if Nkind (N) = N_Defining_Identifier then
3782 C := Get (Current_Perm_Env, Unique_Entity (P));
3783 pragma Assert (C /= null);
3785 -- Setting the initialization map to True, so that this
3786 -- variable cannot be ignored anymore when looking at end
3787 -- of elaboration of package.
3789 Set (Current_Initialization_Map, Unique_Entity (P), True);
3790 if New_Perm = Observed
3794 -- No null possible here, there are no parents for the path.
3795 -- This means we are using a global variable without adding
3796 -- it in environment with a global aspect.
3798 Illegal_Global_Usage (N);
3801 C.all.Tree.Permission := New_Perm;
3805 when N_Type_Conversion
3806 | N_Unchecked_Type_Conversion
3807 | N_Qualified_Expression
3809 return Set_Perm_Prefixes (Expression (N), New_Perm);
3811 when N_Parameter_Specification =>
3812 raise Program_Error;
3814 -- We set the permission tree of its prefix, and then we extract
3815 -- our subtree from the returned pointer and assign an adequate
3816 -- permission to it, if unfolded. If folded, we unroll the tree
3819 when N_Selected_Component =>
3821 C : constant Perm_Tree_Access :=
3822 Set_Perm_Prefixes (Prefix (N), New_Perm);
3827 -- We went through a function call, do nothing
3832 pragma Assert (Kind (C) = Entire_Object
3833 or else Kind (C) = Record_Component);
3835 if Kind (C) = Record_Component then
3836 -- The tree is unfolded. We just modify the permission and
3837 -- return the record subtree.
3840 Selected_Component : constant Entity_Id :=
3841 Entity (Selector_Name (N));
3843 Selected_C : Perm_Tree_Access :=
3845 (Component (C), Selected_Component);
3848 if Selected_C = null then
3849 Selected_C := Other_Components (C);
3852 pragma Assert (Selected_C /= null);
3853 Selected_C.all.Tree.Permission := New_Perm;
3857 elsif Kind (C) = Entire_Object then
3859 -- Expand the tree. Replace the node with
3860 -- Record_Component.
3864 -- Create an empty hash table
3866 Hashtbl : Perm_Tree_Maps.Instance;
3868 -- We create the unrolled nodes, that will all have same
3869 -- permission than parent.
3871 Son : Perm_Tree_Access;
3872 Children_Perm : constant Perm_Kind :=
3873 Children_Permission (C);
3876 -- We change the current node from Entire_Object to
3877 -- Record_Component with same permission and an empty
3878 -- hash table as component list.
3881 (Kind => Record_Component,
3882 Is_Node_Deep => Is_Node_Deep (C),
3883 Permission => Permission (C),
3884 Component => Hashtbl,
3886 new Perm_Tree_Wrapper'
3888 (Kind
=> Entire_Object
,
3889 Is_Node_Deep
=> True,
3890 Permission
=> Children_Perm
,
3891 Children_Permission
=> Children_Perm
)
3894 -- We fill the hash table with all sons of the record,
3895 -- with basic Entire_Objects nodes.
3897 Elem
:= First_Component_Or_Discriminant
3898 (Etype
(Prefix
(N
)));
3900 while Present
(Elem
) loop
3901 Son
:= new Perm_Tree_Wrapper
'
3903 (Kind => Entire_Object,
3904 Is_Node_Deep => Is_Deep (Etype (Elem)),
3905 Permission => Children_Perm,
3906 Children_Permission => Children_Perm));
3908 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
3909 Next_Component_Or_Discriminant (Elem);
3911 -- Now we set the right field to Borrowed, and then we
3912 -- return the tree to the sons, so that the recursion can
3916 Selected_Component : constant Entity_Id :=
3917 Entity (Selector_Name (N));
3918 Selected_C : Perm_Tree_Access :=
3920 (Component (C), Selected_Component);
3923 if Selected_C = null then
3924 Selected_C := Other_Components (C);
3927 pragma Assert (Selected_C /= null);
3928 Selected_C.all.Tree.Permission := New_Perm;
3933 raise Program_Error;
3937 -- We set the permission tree of its prefix, and then we extract
3938 -- from the returned pointer the subtree and assign an adequate
3939 -- permission to it, if unfolded. If folded, we unroll the tree in
3942 when N_Indexed_Component
3946 C : constant Perm_Tree_Access :=
3947 Set_Perm_Prefixes (Prefix (N), New_Perm);
3952 -- We went through a function call, do nothing
3957 pragma Assert (Kind (C) = Entire_Object
3958 or else Kind (C) = Array_Component);
3960 if Kind (C) = Array_Component then
3962 -- The tree is unfolded. We just modify the permission and
3963 -- return the elem subtree.
3965 pragma Assert (Get_Elem (C) /= null);
3966 C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
3967 return Get_Elem (C);
3969 elsif Kind (C) = Entire_Object then
3971 -- Expand the tree. Replace node with Array_Component.
3973 Son : Perm_Tree_Access;
3976 Son := new Perm_Tree_Wrapper'
3978 (Kind
=> Entire_Object
,
3979 Is_Node_Deep
=> Is_Node_Deep
(C
),
3980 Permission
=> New_Perm
,
3981 Children_Permission
=> Children_Permission
(C
)));
3983 -- Children_Permission => Children_Permission (C)
3984 -- this line should be checked maybe New_Perm
3985 -- instead of Children_Permission (C)
3987 -- We change the current node from Entire_Object
3988 -- to Array_Component with same permission and the
3989 -- previously defined son.
3991 C
.all.Tree
:= (Kind
=> Array_Component
,
3992 Is_Node_Deep
=> Is_Node_Deep
(C
),
3993 Permission
=> New_Perm
,
3995 return Get_Elem
(C
);
3998 raise Program_Error
;
4002 -- We set the permission tree of its prefix, and then we extract
4003 -- from the returned pointer the subtree and assign an adequate
4004 -- permission to it, if unfolded. If folded, we unroll the tree
4007 when N_Explicit_Dereference
=>
4009 C
: constant Perm_Tree_Access
:=
4010 Set_Perm_Prefixes
(Prefix
(N
), New_Perm
);
4015 -- We went through a function call. Do nothing.
4020 pragma Assert
(Kind
(C
) = Entire_Object
4021 or else Kind
(C
) = Reference
);
4023 if Kind
(C
) = Reference
then
4025 -- The tree is unfolded. We just modify the permission and
4026 -- return the elem subtree.
4028 pragma Assert
(Get_All
(C
) /= null);
4029 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= New_Perm
;
4032 elsif Kind
(C
) = Entire_Object
then
4034 -- Expand the tree. Replace the node with Reference.
4036 Son
: Perm_Tree_Access
;
4039 Son
:= new Perm_Tree_Wrapper
'
4041 (Kind => Entire_Object,
4042 Is_Node_Deep => Is_Deep (Etype (N)),
4043 Permission => New_Perm,
4044 Children_Permission => Children_Permission (C)));
4046 -- We change the current node from Entire_Object to
4047 -- Reference with Borrowed and the previous son.
4049 pragma Assert (Is_Node_Deep (C));
4050 C.all.Tree := (Kind => Reference,
4051 Is_Node_Deep => Is_Node_Deep (C),
4052 Permission => New_Perm,
4058 raise Program_Error;
4062 when N_Function_Call =>
4066 raise Program_Error;
4068 end Set_Perm_Prefixes;
4070 ------------------------------
4071 -- Set_Perm_Prefixes_Borrow --
4072 ------------------------------
4074 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
4077 pragma Assert (Current_Checking_Mode = Borrow);
4084 P : constant Node_Id := Entity (N);
4085 C : constant Perm_Tree_Access :=
4086 Get (Current_Perm_Env, Unique_Entity (P));
4087 pragma Assert (C /= null);
4090 -- Setting the initialization map to True, so that this
4091 -- variable cannot be ignored anymore when looking at end
4092 -- of elaboration of package.
4094 Set (Current_Initialization_Map, Unique_Entity (P), True);
4095 C.all.Tree.Permission := Borrowed;
4099 when N_Type_Conversion
4100 | N_Unchecked_Type_Conversion
4101 | N_Qualified_Expression
4103 return Set_Perm_Prefixes_Borrow (Expression (N));
4105 when N_Parameter_Specification
4106 | N_Defining_Identifier
4108 raise Program_Error;
4110 -- We set the permission tree of its prefix, and then we extract
4111 -- our subtree from the returned pointer and assign an adequate
4112 -- permission to it, if unfolded. If folded, we unroll the tree
4115 when N_Selected_Component =>
4117 C : constant Perm_Tree_Access :=
4118 Set_Perm_Prefixes_Borrow (Prefix (N));
4123 -- We went through a function call, do nothing
4128 -- The permission of the returned node should be No
4130 pragma Assert (Permission (C) = Borrowed);
4131 pragma Assert (Kind (C) = Entire_Object
4132 or else Kind (C) = Record_Component);
4134 if Kind (C) = Record_Component then
4136 -- The tree is unfolded. We just modify the permission and
4137 -- return the record subtree.
4140 Selected_Component : constant Entity_Id :=
4141 Entity (Selector_Name (N));
4142 Selected_C : Perm_Tree_Access :=
4144 (Component (C), Selected_Component);
4147 if Selected_C = null then
4148 Selected_C := Other_Components (C);
4151 pragma Assert (Selected_C /= null);
4152 Selected_C.all.Tree.Permission := Borrowed;
4156 elsif Kind (C) = Entire_Object then
4158 -- Expand the tree. Replace the node with
4159 -- Record_Component.
4163 -- Create an empty hash table
4165 Hashtbl : Perm_Tree_Maps.Instance;
4167 -- We create the unrolled nodes, that will all have same
4168 -- permission than parent.
4170 Son : Perm_Tree_Access;
4171 ChildrenPerm : constant Perm_Kind :=
4172 Children_Permission (C);
4175 -- We change the current node from Entire_Object to
4176 -- Record_Component with same permission and an empty
4177 -- hash table as component list.
4180 (Kind => Record_Component,
4181 Is_Node_Deep => Is_Node_Deep (C),
4182 Permission => Permission (C),
4183 Component => Hashtbl,
4185 new Perm_Tree_Wrapper'
4187 (Kind
=> Entire_Object
,
4188 Is_Node_Deep
=> True,
4189 Permission
=> ChildrenPerm
,
4190 Children_Permission
=> ChildrenPerm
)
4193 -- We fill the hash table with all sons of the record,
4194 -- with basic Entire_Objects nodes.
4196 Elem
:= First_Component_Or_Discriminant
4197 (Etype
(Prefix
(N
)));
4199 while Present
(Elem
) loop
4200 Son
:= new Perm_Tree_Wrapper
'
4202 (Kind => Entire_Object,
4203 Is_Node_Deep => Is_Deep (Etype (Elem)),
4204 Permission => ChildrenPerm,
4205 Children_Permission => ChildrenPerm));
4206 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
4207 Next_Component_Or_Discriminant (Elem);
4210 -- Now we set the right field to Borrowed, and then we
4211 -- return the tree to the sons, so that the recursion can
4215 Selected_Component : constant Entity_Id :=
4216 Entity (Selector_Name (N));
4217 Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
4218 (Component (C), Selected_Component);
4221 if Selected_C = null then
4222 Selected_C := Other_Components (C);
4225 pragma Assert (Selected_C /= null);
4226 Selected_C.all.Tree.Permission := Borrowed;
4232 raise Program_Error;
4236 -- We set the permission tree of its prefix, and then we extract
4237 -- from the returned pointer the subtree and assign an adequate
4238 -- permission to it, if unfolded. If folded, we unroll the tree in
4241 when N_Indexed_Component
4245 C : constant Perm_Tree_Access :=
4246 Set_Perm_Prefixes_Borrow (Prefix (N));
4251 -- We went through a function call, do nothing
4256 pragma Assert (Permission (C) = Borrowed);
4257 pragma Assert (Kind (C) = Entire_Object
4258 or else Kind (C) = Array_Component);
4260 if Kind (C) = Array_Component then
4262 -- The tree is unfolded. We just modify the permission and
4263 -- return the elem subtree.
4265 pragma Assert (Get_Elem (C) /= null);
4266 C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed;
4267 return Get_Elem (C);
4269 elsif Kind (C) = Entire_Object then
4271 -- Expand the tree. Replace node with Array_Component.
4273 Son : Perm_Tree_Access;
4276 Son := new Perm_Tree_Wrapper'
4278 (Kind
=> Entire_Object
,
4279 Is_Node_Deep
=> Is_Node_Deep
(C
),
4280 Permission
=> Borrowed
,
4281 Children_Permission
=> Children_Permission
(C
)));
4283 -- We change the current node from Entire_Object
4284 -- to Array_Component with same permission and the
4285 -- previously defined son.
4287 C
.all.Tree
:= (Kind
=> Array_Component
,
4288 Is_Node_Deep
=> Is_Node_Deep
(C
),
4289 Permission
=> Borrowed
,
4291 return Get_Elem
(C
);
4295 raise Program_Error
;
4299 -- We set the permission tree of its prefix, and then we extract
4300 -- from the returned pointer the subtree and assign an adequate
4301 -- permission to it, if unfolded. If folded, we unroll the tree
4304 when N_Explicit_Dereference
=>
4306 C
: constant Perm_Tree_Access
:=
4307 Set_Perm_Prefixes_Borrow
(Prefix
(N
));
4312 -- We went through a function call. Do nothing.
4317 -- The permission of the returned node should be No
4319 pragma Assert
(Permission
(C
) = Borrowed
);
4320 pragma Assert
(Kind
(C
) = Entire_Object
4321 or else Kind
(C
) = Reference
);
4323 if Kind
(C
) = Reference
then
4325 -- The tree is unfolded. We just modify the permission and
4326 -- return the elem subtree.
4328 pragma Assert
(Get_All
(C
) /= null);
4329 C
.all.Tree
.Get_All
.all.Tree
.Permission
:= Borrowed
;
4332 elsif Kind
(C
) = Entire_Object
then
4334 -- Expand the tree. Replace the node with Reference.
4336 Son
: Perm_Tree_Access
;
4339 Son
:= new Perm_Tree_Wrapper
'
4341 (Kind => Entire_Object,
4342 Is_Node_Deep => Is_Deep (Etype (N)),
4343 Permission => Borrowed,
4344 Children_Permission => Children_Permission (C)));
4346 -- We change the current node from Entire_Object to
4347 -- Reference with Borrowed and the previous son.
4349 pragma Assert (Is_Node_Deep (C));
4350 C.all.Tree := (Kind => Reference,
4351 Is_Node_Deep => Is_Node_Deep (C),
4352 Permission => Borrowed,
4358 raise Program_Error;
4362 when N_Function_Call =>
4366 raise Program_Error;
4368 end Set_Perm_Prefixes_Borrow;
4374 procedure Setup_Globals (Subp : Entity_Id) is
4375 procedure Setup_Globals_From_List
4376 (First_Item : Node_Id;
4377 Kind : Formal_Kind);
4378 -- Set up global items from the list starting at Item
4380 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
4381 -- Set up global items for the mode Global_Mode
4383 -----------------------------
4384 -- Setup_Globals_From_List --
4385 -----------------------------
4387 procedure Setup_Globals_From_List
4388 (First_Item : Node_Id;
4391 Item : Node_Id := First_Item;
4395 while Present (Item) loop
4398 -- Ignore abstract states, which play no role in pointer aliasing
4400 if Ekind (E) = E_Abstract_State then
4403 Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
4407 end Setup_Globals_From_List;
4409 ---------------------------
4410 -- Setup_Globals_Of_Mode --
4411 ---------------------------
4413 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
4421 Kind := E_In_Parameter;
4424 Kind := E_Out_Parameter;
4427 Kind := E_In_Out_Parameter;
4430 raise Program_Error;
4433 -- Set up both global items from Global and Refined_Global pragmas
4435 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
4436 Setup_Globals_From_List
4437 (First_Global (Subp, Global_Mode, Refined => True), Kind);
4438 end Setup_Globals_Of_Mode;
4440 -- Start of processing for Setup_Globals
4443 Setup_Globals_Of_Mode (Name_Proof_In);
4444 Setup_Globals_Of_Mode (Name_Input);
4445 Setup_Globals_Of_Mode (Name_Output);
4446 Setup_Globals_Of_Mode (Name_In_Out);
4449 -------------------------------
4450 -- Setup_Parameter_Or_Global --
4451 -------------------------------
4453 procedure Setup_Parameter_Or_Global
4456 Global_Var : Boolean)
4458 Elem : Perm_Tree_Access;
4459 View_Typ : Entity_Id;
4462 if Present (Full_View (Etype (Id))) then
4463 View_Typ := Full_View (Etype (Id));
4465 View_Typ := Etype (Id);
4468 Elem := new Perm_Tree_Wrapper'
4470 (Kind
=> Entire_Object
,
4471 Is_Node_Deep
=> Is_Deep
(Etype
(Id
)),
4472 Permission
=> Unrestricted
,
4473 Children_Permission
=> Unrestricted
));
4477 -- All out and in out parameters are considered to be unrestricted.
4478 -- They are whether borrowed or moved. Ada Rules would restrict
4479 -- these permissions further. For example an in parameter cannot
4482 -- In the following we deal with in parameters that can be observed.
4483 -- We only consider the observing cases.
4485 when E_In_Parameter
=>
4487 -- Handling global variables as IN parameters here.
4488 -- Remove the following condition once it's decided how globals
4489 -- should be considered. ???
4491 -- In SPARK, IN access-to-variable is an observe operation for
4492 -- a function, and a borrow operation for a procedure.
4494 if not Global_Var
then
4495 if (Is_Access_Type
(View_Typ
)
4496 and then Is_Access_Constant
(View_Typ
)
4497 and then Is_Anonymous_Access_Type
(View_Typ
))
4499 (Is_Access_Type
(View_Typ
)
4500 and then Ekind
(Scope
(Id
)) = E_Function
)
4502 (not Is_Access_Type
(View_Typ
)
4503 and then Is_Deep
(View_Typ
)
4504 and then not Is_Anonymous_Access_Type
(View_Typ
))
4506 Elem
.all.Tree
.Permission
:= Observed
;
4507 Elem
.all.Tree
.Children_Permission
:= Observed
;
4510 Elem
.all.Tree
.Permission
:= Unrestricted
;
4511 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4515 Elem
.all.Tree
.Permission
:= Observed
;
4516 Elem
.all.Tree
.Children_Permission
:= Observed
;
4519 -- When out or in/out formal or global parameters, we set them to
4520 -- the Unrestricted state. "We want to be able to assume that all
4521 -- relevant writable globals are unrestricted when a subprogram
4522 -- starts executing". Formal parameters of mode out or in/out
4523 -- are whether Borrowers or the targets of a move operation:
4524 -- they start theirs lives in the subprogram as Unrestricted.
4527 Elem
.all.Tree
.Permission
:= Unrestricted
;
4528 Elem
.all.Tree
.Children_Permission
:= Unrestricted
;
4531 Set
(Current_Perm_Env
, Id
, Elem
);
4532 end Setup_Parameter_Or_Global
;
4534 ----------------------
4535 -- Setup_Parameters --
4536 ----------------------
4538 procedure Setup_Parameters
(Subp
: Entity_Id
) is Formal
: Entity_Id
;
4540 Formal
:= First_Formal
(Subp
);
4541 while Present
(Formal
) loop
4542 Setup_Parameter_Or_Global
4543 (Formal
, Ekind
(Formal
), Global_Var
=> False);
4544 Next_Formal
(Formal
);
4546 end Setup_Parameters
;
4548 -------------------------------
4549 -- Has_Ownership_Aspect_True --
4550 -------------------------------
4552 function Has_Ownership_Aspect_True
4558 case Ekind
(Etype
(N
)) is
4560 if Ekind
(Etype
(N
)) = E_General_Access_Type
then
4561 Error_Msg_NE
(Msg
& " & not allowed " &
4562 "(Named General Access type)", N
, N
);
4573 Com_Ty
: constant Node_Id
:= Component_Type
(Etype
(N
));
4574 Ret
: Boolean := Has_Ownership_Aspect_True
(Com_Ty
, "");
4577 if Nkind
(Parent
(N
)) = N_Full_Type_Declaration
and
4578 Is_Anonymous_Access_Type
(Com_Ty
)
4584 Error_Msg_NE
(Msg
& " & not allowed "
4585 & "(Components of Named General Access type or"
4586 & " Anonymous type)", N
, N
);
4591 -- ??? What about hidden components
4598 Elmt_T_Perm
: Boolean := True;
4599 Elmt_Perm
, Elmt_Anonym
: Boolean;
4602 Elmt
:= First_Component_Or_Discriminant
(Etype
(N
));
4603 while Present
(Elmt
) loop
4604 Elmt_Perm
:= Has_Ownership_Aspect_True
(Elmt
,
4605 "type of component");
4606 Elmt_Anonym
:= Is_Anonymous_Access_Type
(Etype
(Elmt
));
4609 ("type of component & not allowed"
4610 & " (Components of Anonymous type)", Elmt
, Elmt
);
4612 Elmt_T_Perm
:= Elmt_T_Perm
and Elmt_Perm
and not Elmt_Anonym
;
4613 Next_Component_Or_Discriminant
(Elmt
);
4615 if not Elmt_T_Perm
then
4617 (Msg
& " & not allowed (One or "
4618 & "more components have Ownership Aspect False)",
4628 end Has_Ownership_Aspect_True
;