1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017-2018, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
24 ------------------------------------------------------------------------------
26 with Atree; use Atree;
27 with Einfo; use Einfo;
28 with Errout; use Errout;
29 with Namet; use Namet;
30 with Nlists; use Nlists;
32 with Osint; use Osint;
33 with Sem_Prag; use Sem_Prag;
34 with Sem_Util; use Sem_Util;
35 with Sem_Aux; use Sem_Aux;
36 with Sinfo; use Sinfo;
37 with Snames; use Snames;
38 with Treepr; use Treepr;
40 with Ada.Unchecked_Deallocation;
41 with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
43 package body Sem_SPARK is
45 -------------------------------------------------
46 -- Handling of Permissions Associated to Paths --
47 -------------------------------------------------
49 package Permissions is
50 Elaboration_Context_Max : constant := 1009;
53 type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
55 function Elaboration_Context_Hash (Key : Entity_Id)
56 return Elaboration_Context_Index;
57 -- Function to hash any node of the AST
59 type Perm_Kind is (Borrowed, Observed, Unrestricted, Moved);
60 -- Permission type associated with paths. The Moved permission is
61 -- equivalent to the Unrestricted one (same permissions). The Moved is
62 -- however used to mark the RHS after a move (which still unrestricted).
63 -- This way, we may generate warnings when manipulating the RHS
64 -- afterwads since it is set to Null after the assignment.
66 type Perm_Tree_Wrapper;
68 type Perm_Tree_Access is access Perm_Tree_Wrapper;
69 -- A tree of permissions is defined, where the root is a whole object
70 -- and tree branches follow access paths in memory. As Perm_Tree is a
71 -- discriminated record, a wrapper type is used for the access type
72 -- designating a subtree, to make it unconstrained so that it can be
75 -- Nodes in the permission tree are of different kinds
78 (Entire_Object, -- Scalar object, or folded object of any type
79 Reference, -- Unfolded object of access type
80 Array_Component, -- Unfolded object of array type
81 Record_Component -- Unfolded object of record type
84 package Perm_Tree_Maps is new Simple_HTable
85 (Header_Num => Elaboration_Context_Index,
87 Element => Perm_Tree_Access,
89 Hash => Elaboration_Context_Hash,
91 -- The instantation of a hash table, with keys being nodes and values
92 -- being pointers to trees. This is used to reference easily all
93 -- extensions of a Record_Component node (that can have name x, y, ...).
95 -- The definition of permission trees. This is a tree, which has a
96 -- permission at each node, and depending on the type of the node,
97 -- can have zero, one, or more children pointed to by an access to tree.
99 type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
100 Permission : Perm_Kind;
101 -- Permission at this level in the path
103 Is_Node_Deep : Boolean;
104 -- Whether this node is of a deep type, to be used when moving the
108 -- An entire object is either a leaf (an object which cannot be
109 -- extended further in a path) or a subtree in folded form (which
110 -- could later be unfolded further in another kind of node). The
111 -- field Children_Permission specifies a permission for every
112 -- extension of that node if that permission is different from
113 -- the node's permission.
115 when Entire_Object =>
116 Children_Permission : Perm_Kind;
118 -- Unfolded path of access type. The permission of the object
119 -- pointed to is given in Get_All.
122 Get_All : Perm_Tree_Access;
124 -- Unfolded path of array type. The permission of the elements is
125 -- given in Get_Elem.
127 when Array_Component =>
128 Get_Elem : Perm_Tree_Access;
130 -- Unfolded path of record type. The permission of the regular
131 -- components is given in Component. The permission of unknown
132 -- components (for objects of tagged type) is given in
135 when Record_Component =>
136 Component : Perm_Tree_Maps.Instance;
137 Other_Components : Perm_Tree_Access;
141 type Perm_Tree_Wrapper is record
144 -- We use this wrapper in order to have unconstrained discriminants
146 type Perm_Env is new Perm_Tree_Maps.Instance;
147 -- The definition of a permission environment for the analysis. This
148 -- is just a hash table of permission trees, each of them rooted with
149 -- an Identifier/Expanded_Name.
151 type Perm_Env_Access is access Perm_Env;
152 -- Access to permission environments
154 package Env_Maps is new Simple_HTable
155 (Header_Num => Elaboration_Context_Index,
157 Element => Perm_Env_Access,
159 Hash => Elaboration_Context_Hash,
161 -- The instantiation of a hash table whose elements are permission
162 -- environments. This hash table is used to save the environments at
163 -- the entry of each loop, with the key being the loop label.
165 type Env_Backups is new Env_Maps.Instance;
166 -- The type defining the hash table saving the environments at the entry
169 package Boolean_Variables_Maps is new Simple_HTable
170 (Header_Num => Elaboration_Context_Index,
174 Hash => Elaboration_Context_Hash,
176 -- These maps allow tracking the variables that have been declared but
177 -- never used anywhere in the source code. Especially, we do not raise
178 -- an error if the variable stays write-only and is declared at package
179 -- level, because there is no risk that the variable has been moved,
180 -- because it has never been used.
182 type Initialization_Map is new Boolean_Variables_Maps.Instance;
188 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
189 -- that's only for the top access, as otherwise this reverses the order
190 -- in accesses visually.
192 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
193 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
194 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
195 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
196 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
197 function Kind (T : Perm_Tree_Access) return Path_Kind;
198 function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access;
199 function Permission (T : Perm_Tree_Access) return Perm_Kind;
201 -----------------------
202 -- Memory Management --
203 -----------------------
207 To : in out Perm_Env);
208 -- Procedure to copy a permission environment
210 procedure Copy_Init_Map
211 (From : Initialization_Map;
212 To : in out Initialization_Map);
213 -- Procedure to copy an initialization map
216 (From : Perm_Tree_Access;
217 To : Perm_Tree_Access);
218 -- Procedure to copy a permission tree
221 (PE : in out Perm_Env);
222 -- Procedure to free a permission environment
224 procedure Free_Perm_Tree
225 (PT : in out Perm_Tree_Access);
226 -- Procedure to free a permission tree
232 procedure Perm_Mismatch
233 (Exp_Perm, Act_Perm : Perm_Kind;
235 -- Issues a continuation error message about a mismatch between a
236 -- desired permission Exp_Perm and a permission obtained Act_Perm. N
237 -- is the node on which the error is reported.
241 package body Permissions is
243 -------------------------
244 -- Children_Permission --
245 -------------------------
247 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
249 return T.all.Tree.Children_Permission;
250 end Children_Permission;
257 (T : Perm_Tree_Access)
258 return Perm_Tree_Maps.Instance
261 return T.all.Tree.Component;
268 procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is
269 Comp_From : Perm_Tree_Access;
270 Key_From : Perm_Tree_Maps.Key_Option;
271 Son : Perm_Tree_Access;
275 Key_From := Get_First_Key (From);
276 while Key_From.Present loop
277 Comp_From := Get (From, Key_From.K);
278 pragma Assert (Comp_From /= null);
280 Son := new Perm_Tree_Wrapper;
281 Copy_Tree (Comp_From, Son);
283 Set (To, Key_From.K, Son);
284 Key_From := Get_Next_Key (From);
292 procedure Copy_Init_Map
293 (From : Initialization_Map;
294 To : in out Initialization_Map)
297 Key_From : Boolean_Variables_Maps.Key_Option;
301 Key_From := Get_First_Key (From);
302 while Key_From.Present loop
303 Comp_From := Get (From, Key_From.K);
304 Set (To, Key_From.K, Comp_From);
305 Key_From := Get_Next_Key (From);
313 procedure Copy_Tree (From : Perm_Tree_Access; To : Perm_Tree_Access) is
317 when Entire_Object =>
321 To.all.Tree.Get_All := new Perm_Tree_Wrapper;
322 Copy_Tree (Get_All (From), Get_All (To));
324 when Array_Component =>
325 To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
326 Copy_Tree (Get_Elem (From), Get_Elem (To));
328 when Record_Component =>
330 Comp_From : Perm_Tree_Access;
331 Key_From : Perm_Tree_Maps.Key_Option;
332 Son : Perm_Tree_Access;
333 Hash_Table : Perm_Tree_Maps.Instance;
335 -- We put a new hash table, so that it gets dealiased from the
336 -- Component (From) hash table.
337 To.all.Tree.Component := Hash_Table;
338 To.all.Tree.Other_Components :=
339 new Perm_Tree_Wrapper'(Other_Components (From).all);
340 Copy_Tree (Other_Components (From), Other_Components (To));
341 Key_From := Perm_Tree_Maps.Get_First_Key
344 while Key_From.Present loop
345 Comp_From := Perm_Tree_Maps.Get
346 (Component (From), Key_From.K);
347 pragma Assert (Comp_From /= null);
348 Son := new Perm_Tree_Wrapper;
349 Copy_Tree (Comp_From, Son);
351 (To.all.Tree.Component, Key_From.K, Son);
352 Key_From := Perm_Tree_Maps.Get_Next_Key
360 ------------------------------
361 -- Elaboration_Context_Hash --
362 ------------------------------
364 function Elaboration_Context_Hash
365 (Key : Entity_Id) return Elaboration_Context_Index
368 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
369 end Elaboration_Context_Hash;
375 procedure Free_Env (PE : in out Perm_Env) is
376 CompO : Perm_Tree_Access;
378 CompO := Get_First (PE);
379 while CompO /= null loop
380 Free_Perm_Tree (CompO);
381 CompO := Get_Next (PE);
389 procedure Free_Perm_Tree (PT : in out Perm_Tree_Access) is
390 procedure Free_Perm_Tree_Dealloc is
391 new Ada.Unchecked_Deallocation
392 (Perm_Tree_Wrapper, Perm_Tree_Access);
393 -- The deallocator for permission_trees
397 when Entire_Object =>
398 Free_Perm_Tree_Dealloc (PT);
401 Free_Perm_Tree (PT.all.Tree.Get_All);
402 Free_Perm_Tree_Dealloc (PT);
404 when Array_Component =>
405 Free_Perm_Tree (PT.all.Tree.Get_Elem);
407 when Record_Component =>
409 Comp : Perm_Tree_Access;
412 Free_Perm_Tree (PT.all.Tree.Other_Components);
413 Comp := Perm_Tree_Maps.Get_First (Component (PT));
414 while Comp /= null loop
416 -- Free every Component subtree
418 Free_Perm_Tree (Comp);
419 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
422 Free_Perm_Tree_Dealloc (PT);
430 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
432 return T.all.Tree.Get_All;
439 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
441 return T.all.Tree.Get_Elem;
448 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
450 return T.all.Tree.Is_Node_Deep;
457 function Kind (T : Perm_Tree_Access) return Path_Kind is
459 return T.all.Tree.Kind;
462 ----------------------
463 -- Other_Components --
464 ----------------------
466 function Other_Components
467 (T : Perm_Tree_Access)
468 return Perm_Tree_Access
471 return T.all.Tree.Other_Components;
472 end Other_Components;
478 function Permission (T : Perm_Tree_Access) return Perm_Kind is
480 return T.all.Tree.Permission;
487 procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is
489 Error_Msg_N ("\expected state `"
490 & Perm_Kind'Image (Exp_Perm) & "` at least, got `"
491 & Perm_Kind'Image (Act_Perm) & "`", N);
498 --------------------------------------
499 -- Analysis modes for AST traversal --
500 --------------------------------------
502 -- The different modes for analysis. This allows to checking whether a path
503 -- found in the code should be moved, borrowed, or observed.
505 type Checking_Mode is
511 -- Regular moving semantics. Checks that paths have Unrestricted
512 -- permission. After moving a path, the permission of both it and
513 -- its extensions are set to Unrestricted.
516 -- Used for the target of an assignment, or an actual parameter with
517 -- mode OUT. Checks that paths have Unrestricted permission. After
518 -- assigning to a path, its permission is set to Unrestricted.
521 -- Used for the source of an assignement when initializes a stand alone
522 -- object of anonymous type, constant, or IN parameter and also OUT
523 -- or IN OUT composite object.
524 -- In the borrowed state, the access object is completely "dead".
527 -- Used for actual IN parameters of a scalar type. Checks that paths
528 -- have Read_Perm permission. After checking a path, its permission
529 -- is set to Observed.
531 -- Also used for formal IN parameters
535 type Result_Kind is (Folded, Unfolded, Function_Call);
536 -- The type declaration to discriminate in the Perm_Or_Tree type
538 -- The result type of the function Get_Perm_Or_Tree. This returns either a
539 -- tree when it found the appropriate tree, or a permission when the search
540 -- finds a leaf and the subtree we are looking for is folded. In the last
541 -- case, we return instead the Children_Permission field of the leaf.
543 type Perm_Or_Tree (R : Result_Kind) is record
545 when Folded => Found_Permission : Perm_Kind;
546 when Unfolded => Tree_Access : Perm_Tree_Access;
547 when Function_Call => null;
551 -----------------------
552 -- Local subprograms --
553 -----------------------
555 -- Checking proceduress for safe pointer usage. These procedures traverse
556 -- the AST, check nodes for correct permissions according to SPARK RM
557 -- 6.4.2, and update permissions depending on the node kind.
559 procedure Check_Call_Statement (Call : Node_Id);
561 procedure Check_Callable_Body (Body_N : Node_Id);
562 -- We are not in End_Of_Callee mode, hence we will save the environment
563 -- and start from a new one. We will add in the environment all formal
564 -- parameters as well as global used during the subprogram, with the
565 -- appropriate permissions (unrestricted for borrowed and moved, observed
566 -- for observed names).
568 procedure Check_Declaration (Decl : Node_Id);
570 procedure Check_Expression (Expr : Node_Id);
572 procedure Check_Globals (N : Node_Id);
573 -- This procedure takes a global pragma and checks it
575 procedure Check_List (L : List_Id);
576 -- Calls Check_Node on each element of the list
578 procedure Check_Loop_Statement (Loop_N : Node_Id);
580 procedure Check_Node (N : Node_Id);
581 -- Main traversal procedure to check safe pointer usage. This procedure is
582 -- mutually recursive with the specialized procedures that follow.
584 procedure Check_Package_Body (Pack : Node_Id);
586 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id);
587 -- This procedure takes a formal and an actual parameter and checks the
588 -- permission of every in-mode parameter. This includes Observing and
591 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id);
592 -- This procedure takes a formal and an actual parameter and checks the
593 -- state of every out-mode and in out-mode parameter. This includes
594 -- Moving and Borrowing.
596 procedure Check_Statement (Stmt : Node_Id);
598 function Get_Perm (N : Node_Id) return Perm_Kind;
599 -- The function that takes a name as input and returns a permission
602 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
603 -- This function gets a Node_Id and looks recursively to find the
604 -- appropriate subtree for that Node_Id. If the tree is folded on
605 -- that node, then it returns the permission given at the right level.
607 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
608 -- This function gets a Node_Id and looks recursively to find the
609 -- appropriate subtree for that Node_Id. If the tree is folded, then
610 -- it unrolls the tree up to the appropriate level.
612 procedure Hp (P : Perm_Env);
613 -- A procedure that outputs the hash table. This function is used only in
614 -- the debugger to look into a hash table.
615 pragma Unreferenced (Hp);
617 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id);
618 pragma No_Return (Illegal_Global_Usage);
619 -- A procedure that is called when deep globals or aliased globals are used
620 -- without any global aspect.
622 function Is_Deep (E : Entity_Id) return Boolean;
623 -- A function that can tell if a type is deep or not. Returns true if the
624 -- type passed as argument is deep.
629 Found_Perm : Perm_Kind);
630 -- A procedure that is called when the permissions found contradict the
631 -- rules established by the RM. This function is called with the node, its
632 -- entity and the permission that was expected, and adds an error message
633 -- with the appropriate values.
635 procedure Perm_Error_Subprogram_End
639 Found_Perm : Perm_Kind);
640 -- A procedure that is called when the permissions found contradict the
641 -- rules established by the RM at the end of subprograms. This function
642 -- is called with the node, its entity, the node of the returning function
643 -- and the permission that was expected, and adds an error message with the
644 -- appropriate values.
646 procedure Process_Path (N : Node_Id);
648 procedure Return_Declarations (L : List_Id);
649 -- Check correct permissions on every declared object at the end of a
650 -- callee. Used at the end of the body of a callable entity. Checks that
651 -- paths of all borrowed formal parameters and global have Unrestricted
654 procedure Return_Globals (Subp : Entity_Id);
655 -- Takes a subprogram as input, and checks that all borrowed global items
656 -- of the subprogram indeed have RW permission at the end of the subprogram
659 procedure Return_The_Global
663 -- Auxiliary procedure to Return_Globals
664 -- There is no need to return parameters because they will be reassigned
665 -- their state once the subprogram returns. Local variables that have
666 -- borrowed, observed, or moved an actual parameter go out of the scope.
668 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind);
669 -- This procedure takes an access to a permission tree and modifies the
670 -- tree so that any strict extensions of the given tree become of the
671 -- access specified by parameter P.
673 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access;
674 -- This function modifies the permissions of a given node_id in the
675 -- permission environment as well as in all the prefixes of the path,
676 -- given that the path is borrowed with mode out.
678 function Set_Perm_Prefixes
680 New_Perm : Perm_Kind)
681 return Perm_Tree_Access;
682 -- This function sets the permissions of a given node_id in the
683 -- permission environment as well as in all the prefixes of the path
684 -- to the one given in parameter (P).
686 procedure Setup_Globals (Subp : Entity_Id);
687 -- Takes a subprogram as input, and sets up the environment by adding
688 -- global items with appropriate permissions.
690 procedure Setup_Parameter_Or_Global
693 Global_Var : Boolean);
694 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
696 procedure Setup_Parameters (Subp : Entity_Id);
697 -- Takes a subprogram as input, and sets up the environment by adding
698 -- formal parameters with appropriate permissions.
700 function Has_Ownership_Aspect_True
704 -- Takes a node as an input, and finds out whether it has ownership aspect
705 -- True or False. This function is recursive whenever the node has a
706 -- composite type. Access-to-objects have ownership aspect False if they
707 -- have a general access type.
709 ----------------------
710 -- Global Variables --
711 ----------------------
713 Current_Perm_Env : Perm_Env;
714 -- The permission environment that is used for the analysis. This
715 -- environment can be saved, modified, reinitialized, but should be the
716 -- only one valid from which to extract the permissions of the paths in
717 -- scope. The analysis ensures at each point that this variables contains
718 -- a valid permission environment with all bindings in scope.
720 Current_Checking_Mode : Checking_Mode := Read;
721 -- The current analysis mode. This global variable indicates at each point
722 -- of the analysis whether the node being analyzed is moved, borrowed,
723 -- assigned, read, ... The full list of possible values can be found in
724 -- the declaration of type Checking_Mode.
726 Current_Loops_Envs : Env_Backups;
727 -- This variable contains saves of permission environments at each loop the
728 -- analysis entered. Each saved environment can be reached with the label
731 Current_Loops_Accumulators : Env_Backups;
732 -- This variable contains the environments used as accumulators for loops,
733 -- that consist of the merge of all environments at each exit point of
734 -- the loop (which can also be the entry point of the loop in the case of
735 -- non-infinite loops), each of them reachable from the label of the loop.
736 -- We require that the environment stored in the accumulator be less
737 -- restrictive than the saved environment at the beginning of the loop, and
738 -- the permission environment after the loop is equal to the accumulator.
740 Current_Initialization_Map : Initialization_Map;
741 -- This variable contains a map that binds each variable of the analyzed
742 -- source code to a boolean that becomes true whenever the variable is used
743 -- after declaration. Hence we can exclude from analysis variables that
744 -- are just declared and never accessed, typically at package declaration.
746 --------------------------
747 -- Check_Call_Statement --
748 --------------------------
750 procedure Check_Call_Statement (Call : Node_Id) is
751 Saved_Env : Perm_Env;
753 procedure Iterate_Call_In is new
754 Iterate_Call_Parameters (Check_Param_In);
755 procedure Iterate_Call_Out is new
756 Iterate_Call_Parameters (Check_Param_Out);
759 -- Save environment, so that the modifications done by analyzing the
760 -- parameters are not kept at the end of the call.
762 Copy_Env (Current_Perm_Env, Saved_Env);
764 -- We first check the globals then parameters to handle the
765 -- No_Parameter_Aliasing Restriction. An out or in-out global is
766 -- considered as borrowing while a parameter with the same mode is
767 -- a move. This order disallow passing a part of a variable to a
768 -- subprogram if it is referenced as a global by the callable (when
770 -- For paremeters, we fisrt check in parameters and then the out ones.
771 -- This is to avoid Observing or Borrowing objects that are already
772 -- moved. This order is not mandatory but allows to catch runtime
773 -- errors like null pointer dereferencement at the analysis time.
775 Current_Checking_Mode := Read;
776 Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global));
777 Iterate_Call_In (Call);
778 Iterate_Call_Out (Call);
780 -- Restore environment, because after borrowing/observing actual
781 -- parameters, they get their permission reverted to the ones before
784 Free_Env (Current_Perm_Env);
785 Copy_Env (Saved_Env, Current_Perm_Env);
786 Free_Env (Saved_Env);
787 end Check_Call_Statement;
789 -------------------------
790 -- Check_Callable_Body --
791 -------------------------
793 procedure Check_Callable_Body (Body_N : Node_Id) is
795 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
796 Saved_Env : Perm_Env;
797 Saved_Init_Map : Initialization_Map;
799 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
800 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
803 -- Check if SPARK pragma is not set to Off
805 if Present (SPARK_Pragma (Defining_Entity (Body_N))) then
806 if Get_SPARK_Mode_From_Annotation
807 (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On
815 -- Save environment and put a new one in place
817 Copy_Env (Current_Perm_Env, Saved_Env);
819 -- Save initialization map
821 Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map);
822 Current_Checking_Mode := Read;
823 Current_Perm_Env := New_Env;
825 -- Add formals and globals to the environment with adequate permissions
827 if Is_Subprogram_Or_Entry (Spec_Id) then
828 Setup_Parameters (Spec_Id);
829 Setup_Globals (Spec_Id);
832 -- Analyze the body of the function
834 Check_List (Declarations (Body_N));
835 Check_Node (Handled_Statement_Sequence (Body_N));
837 -- Check the read-write permissions of borrowed parameters/globals
839 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
840 and then not No_Return (Spec_Id)
842 Return_Globals (Spec_Id);
845 -- Free the environments
847 Free_Env (Current_Perm_Env);
848 Copy_Env (Saved_Env, Current_Perm_Env);
849 Free_Env (Saved_Env);
851 -- Restore initialization map
853 Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map);
854 Reset (Saved_Init_Map);
856 -- The assignment of all out parameters will be done by caller
858 Current_Checking_Mode := Mode_Before;
859 end Check_Callable_Body;
861 -----------------------
862 -- Check_Declaration --
863 -----------------------
865 procedure Check_Declaration (Decl : Node_Id) is
867 Target_Ent : constant Entity_Id := Defining_Identifier (Decl);
868 Target_Typ : Node_Id renames Etype (Target_Ent);
870 Target_View_Typ : Entity_Id;
872 Check : Boolean := True;
874 if Present (Full_View (Target_Typ)) then
875 Target_View_Typ := Full_View (Target_Typ);
877 Target_View_Typ := Target_Typ;
880 case N_Declaration'(Nkind (Decl)) is
881 when N_Full_Type_Declaration =>
882 if not Has_Ownership_Aspect_True (Target_Ent, "type declaration")
887 -- ??? What about component declarations with defaults.
889 when N_Object_Declaration =>
890 if (Is_Access_Type (Target_View_Typ)
891 or else Is_Deep (Target_Typ))
892 and then not Has_Ownership_Aspect_True
893 (Target_Ent, "Object declaration ")
898 if Is_Anonymous_Access_Type (Target_View_Typ)
899 and then not Present (Expression (Decl))
902 -- ??? Check the case of default value (AI)
903 -- ??? How an anonymous access type can be with default exp?
905 Error_Msg_NE ("? object declaration & has OAF (Anonymous "
906 & "access-to-object with no initialization)",
909 -- If it it an initialization
911 elsif Present (Expression (Decl)) and Check then
913 -- Find out the operation to be done on the right-hand side
915 -- Initializing object, access type
917 if Is_Access_Type (Target_View_Typ) then
919 -- Initializing object, constant access type
921 if Is_Constant_Object (Target_Ent) then
923 -- Initializing object, constant access to variable type
925 if not Is_Access_Constant (Target_View_Typ) then
926 Current_Checking_Mode := Borrow;
928 -- Initializing object, constant access to constant type
930 -- Initializing object,
931 -- constant access to constant anonymous type.
933 elsif Is_Anonymous_Access_Type (Target_View_Typ) then
935 -- This is an object declaration so the target
936 -- of the assignement is a stand-alone object.
938 Current_Checking_Mode := Observe;
940 -- Initializing object, constant access to constant
944 -- If named then it is a general access type
945 -- Hence, Has_Ownership_Aspec_True is False.
950 -- Initializing object, variable access type
953 -- Initializing object, variable access to variable type
955 if not Is_Access_Constant (Target_View_Typ) then
957 -- Initializing object, variable named access to
960 if not Is_Anonymous_Access_Type (Target_View_Typ) then
961 Current_Checking_Mode := Move;
963 -- Initializing object, variable anonymous access to
967 -- This is an object declaration so the target
968 -- object of the assignement is a stand-alone
971 Current_Checking_Mode := Borrow;
974 -- Initializing object, variable access to constant type
977 -- Initializing object,
978 -- variable named access to constant type.
980 if not Is_Anonymous_Access_Type (Target_View_Typ) then
981 Error_Msg_N ("assignment not allowed, Ownership "
982 & "Aspect False (Anonymous Access "
986 -- Initializing object,
987 -- variable anonymous access to constant type.
990 -- This is an object declaration so the target
991 -- of the assignement is a stand-alone object.
993 Current_Checking_Mode := Observe;
998 -- Initializing object, composite (deep) type
1000 elsif Is_Deep (Target_Typ) then
1002 -- Initializing object, constant composite type
1004 if Is_Constant_Object (Target_Ent) then
1005 Current_Checking_Mode := Observe;
1007 -- Initializing object, variable composite type
1011 -- Initializing object, variable anonymous composite type
1013 if Nkind (Object_Definition (Decl)) =
1014 N_Constrained_Array_Definition
1016 -- An N_Constrained_Array_Definition is an anonymous
1017 -- array (to be checked). Record types are always
1018 -- named and are considered in the else part.
1022 Com_Ty : constant Node_Id :=
1023 Component_Type (Etype (Target_Typ));
1026 if Is_Access_Type (Com_Ty) then
1028 -- If components are of anonymous type
1030 if Is_Anonymous_Access_Type (Com_Ty) then
1031 if Is_Access_Constant (Com_Ty) then
1032 Current_Checking_Mode := Observe;
1035 Current_Checking_Mode := Borrow;
1039 Current_Checking_Mode := Move;
1042 elsif Is_Deep (Com_Ty) then
1044 -- This is certainly named so it is a move
1046 Current_Checking_Mode := Move;
1051 Current_Checking_Mode := Move;
1055 elsif Nkind_In (Expression (Decl),
1056 N_Attribute_Reference,
1057 N_Attribute_Reference,
1059 N_Explicit_Dereference,
1060 N_Indexed_Component,
1062 N_Selected_Component,
1065 if Is_Access_Type (Etype (Prefix (Expression (Decl))))
1066 or else Is_Deep (Etype (Prefix (Expression (Decl))))
1068 Current_Checking_Mode := Observe;
1075 Check_Node (Expression (Decl));
1078 -- If lhs is not a pointer, we still give it the appropriate
1079 -- state which is useless but not harmful.
1082 Elem : Perm_Tree_Access;
1083 Deep : constant Boolean := Is_Deep (Target_Typ);
1086 -- Note that all declared variables are set to the unrestricted
1089 -- If variables are not initialized:
1090 -- unrestricted to every declared object.
1095 -- The assignement R := S is not allowed in the new rules
1096 -- if R is not unrestricted.
1098 -- If variables are initialized:
1099 -- If it is a move, then the target is unrestricted
1100 -- If it is a borrow, then the target is unrestricted
1101 -- If it is an observe, then the target should be observed
1103 if Current_Checking_Mode = Observe then
1104 Elem := new Perm_Tree_Wrapper'
1106 (Kind => Entire_Object,
1107 Is_Node_Deep => Deep,
1108 Permission => Observed,
1109 Children_Permission => Observed));
1111 Elem := new Perm_Tree_Wrapper'
1113 (Kind => Entire_Object,
1114 Is_Node_Deep => Deep,
1115 Permission => Unrestricted,
1116 Children_Permission => Unrestricted));
1119 -- Create new tree for defining identifier
1121 Set (Current_Perm_Env,
1122 Unique_Entity (Defining_Identifier (Decl)),
1124 pragma Assert (Get_First (Current_Perm_Env) /= null);
1127 when N_Subtype_Declaration =>
1128 Check_Node (Subtype_Indication (Decl));
1130 when N_Iterator_Specification =>
1133 when N_Loop_Parameter_Specification =>
1136 -- Checking should not be called directly on these nodes
1138 when N_Function_Specification
1139 | N_Entry_Declaration
1140 | N_Procedure_Specification
1141 | N_Component_Declaration
1143 raise Program_Error;
1145 -- Ignored constructs for pointer checking
1147 when N_Formal_Object_Declaration
1148 | N_Formal_Type_Declaration
1149 | N_Incomplete_Type_Declaration
1150 | N_Private_Extension_Declaration
1151 | N_Private_Type_Declaration
1152 | N_Protected_Type_Declaration
1156 -- The following nodes are rewritten by semantic analysis
1158 when N_Expression_Function =>
1159 raise Program_Error;
1161 end Check_Declaration;
1163 ----------------------
1164 -- Check_Expression --
1165 ----------------------
1167 procedure Check_Expression (Expr : Node_Id) is
1168 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1170 case N_Subexpr'(Nkind (Expr)) is
1171 when N_Procedure_Call_Statement
1174 Check_Call_Statement (Expr);
1179 -- Check if identifier is pointing to nothing (On/Off/...)
1181 if not Present (Entity (Expr)) then
1185 -- Do not analyze things that are not of object Kind
1187 if Ekind (Entity (Expr)) not in Object_Kind then
1191 -- Consider as ident
1193 Process_Path (Expr);
1195 -- Switch to read mode and then check the readability of each operand
1198 Current_Checking_Mode := Read;
1199 Check_Node (Left_Opnd (Expr));
1200 Check_Node (Right_Opnd (Expr));
1202 -- Switch to read mode and then check the readability of each operand
1209 Current_Checking_Mode := Read;
1210 Check_Node (Right_Opnd (Expr));
1212 -- Forbid all deep expressions for Attribute ???
1213 -- What about generics? (formal parameters).
1215 when N_Attribute_Reference =>
1216 case Attribute_Name (Expr) is
1218 Error_Msg_N ("access attribute not allowed in SPARK", Expr);
1223 Current_Checking_Mode := Read;
1224 Check_Node (Prefix (Expr));
1227 Current_Checking_Mode := Read;
1228 Check_Node (Prefix (Expr));
1231 Check_List (Expressions (Expr));
1234 Check_Node (Prefix (Expr));
1236 when Name_SPARK_Mode =>
1240 Current_Checking_Mode := Read;
1241 Check_Node (Prefix (Expr));
1244 Check_List (Expressions (Expr));
1245 Check_Node (Prefix (Expr));
1250 Check_List (Expressions (Expr));
1251 Check_Node (Prefix (Expr));
1254 Current_Checking_Mode := Read;
1255 Check_Node (Prefix (Expr));
1257 -- Any Attribute referring to the underlying memory is ignored
1258 -- in the analysis. This means that taking the address of a
1259 -- variable makes a silent alias that is not rejected by the
1264 | Name_Component_Size
1272 -- Attributes referring to types (get values from types), hence
1273 -- no need to check either for borrows or any loans.
1279 -- Other attributes that fall out of the scope of the analysis
1286 Current_Checking_Mode := Read;
1287 Check_Node (Left_Opnd (Expr));
1288 Check_Node (Right_Opnd (Expr));
1291 Current_Checking_Mode := Read;
1292 Check_Node (Left_Opnd (Expr));
1293 Check_Node (Right_Opnd (Expr));
1295 -- Switch to read mode and then check the readability of each operand
1300 Current_Checking_Mode := Read;
1301 Check_Node (Left_Opnd (Expr));
1302 Check_Node (Right_Opnd (Expr));
1304 -- Check the arguments of the call
1306 when N_Explicit_Dereference =>
1307 Process_Path (Expr);
1309 -- Copy environment, run on each branch, and then merge
1311 when N_If_Expression =>
1313 Saved_Env : Perm_Env;
1315 -- Accumulator for the different branches
1318 Elmt : Node_Id := First (Expressions (Expr));
1321 Current_Checking_Mode := Read;
1323 Current_Checking_Mode := Mode_Before;
1327 Copy_Env (Current_Perm_Env, Saved_Env);
1329 -- Here we have the original env in saved, current with a fresh
1330 -- copy, and new aliased.
1337 -- Here the new_environment contains curr env after then block
1340 -- Restore environment before if
1341 Copy_Env (Current_Perm_Env, New_Env);
1342 Free_Env (Current_Perm_Env);
1343 Copy_Env (Saved_Env, Current_Perm_Env);
1345 -- Here new environment contains the environment after then and
1346 -- current the fresh copy of old one.
1353 Copy_Env (New_Env, Current_Perm_Env);
1355 Free_Env (Saved_Env);
1358 when N_Indexed_Component =>
1359 Process_Path (Expr);
1361 -- Analyze the expression that is getting qualified
1363 when N_Qualified_Expression =>
1364 Check_Node (Expression (Expr));
1366 when N_Quantified_Expression =>
1368 Saved_Env : Perm_Env;
1371 Copy_Env (Current_Perm_Env, Saved_Env);
1372 Current_Checking_Mode := Read;
1373 Check_Node (Iterator_Specification (Expr));
1374 Check_Node (Loop_Parameter_Specification (Expr));
1376 Check_Node (Condition (Expr));
1377 Free_Env (Current_Perm_Env);
1378 Copy_Env (Saved_Env, Current_Perm_Env);
1379 Free_Env (Saved_Env);
1381 -- Analyze the list of associations in the aggregate
1384 Check_List (Expressions (Expr));
1385 Check_List (Component_Associations (Expr));
1388 Check_Node (Expression (Expr));
1390 when N_Case_Expression =>
1392 Saved_Env : Perm_Env;
1394 -- Accumulator for the different branches
1397 Elmt : Node_Id := First (Alternatives (Expr));
1400 Current_Checking_Mode := Read;
1401 Check_Node (Expression (Expr));
1402 Current_Checking_Mode := Mode_Before;
1406 Copy_Env (Current_Perm_Env, Saved_Env);
1408 -- Here we have the original env in saved, current with a fresh
1409 -- copy, and new aliased.
1411 -- First alternative
1415 Copy_Env (Current_Perm_Env, New_Env);
1416 Free_Env (Current_Perm_Env);
1418 -- Other alternatives
1420 while Present (Elmt) loop
1422 -- Restore environment
1424 Copy_Env (Saved_Env, Current_Perm_Env);
1430 Copy_Env (Saved_Env, Current_Perm_Env);
1432 Free_Env (Saved_Env);
1434 -- Analyze the list of associates in the aggregate as well as the
1437 when N_Extension_Aggregate =>
1438 Check_Node (Ancestor_Part (Expr));
1439 Check_List (Expressions (Expr));
1442 Check_Node (Low_Bound (Expr));
1443 Check_Node (High_Bound (Expr));
1445 -- We arrived at a path. Process it.
1447 when N_Selected_Component =>
1448 Process_Path (Expr);
1451 Process_Path (Expr);
1453 when N_Type_Conversion =>
1454 Check_Node (Expression (Expr));
1456 when N_Unchecked_Type_Conversion =>
1457 Check_Node (Expression (Expr));
1459 -- Checking should not be called directly on these nodes
1461 when N_Target_Name =>
1462 raise Program_Error;
1464 -- Unsupported constructs in SPARK
1466 when N_Delta_Aggregate =>
1467 Error_Msg_N ("unsupported construct in SPARK", Expr);
1469 -- Ignored constructs for pointer checking
1471 when N_Character_Literal
1473 | N_Numeric_Or_String_Literal
1475 | N_Raise_Expression
1479 -- The following nodes are never generated in GNATprove mode
1481 when N_Expression_With_Actions
1483 | N_Unchecked_Expression
1485 raise Program_Error;
1487 end Check_Expression;
1493 procedure Check_Globals (N : Node_Id) is
1495 if Nkind (N) = N_Empty then
1500 pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1);
1501 PAA : constant Node_Id := First (Pragma_Argument_Associations (N));
1502 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association);
1507 procedure Process (Mode : Name_Id; The_Global : Entity_Id);
1508 procedure Process (Mode : Name_Id; The_Global : Node_Id) is
1509 Ident_Elt : constant Entity_Id :=
1510 Unique_Entity (Entity (The_Global));
1511 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1514 if Ekind (Ident_Elt) = E_Abstract_State then
1521 Current_Checking_Mode := Observe;
1522 Check_Node (The_Global);
1527 -- ??? Borrow not Move?
1528 Current_Checking_Mode := Borrow;
1529 Check_Node (The_Global);
1532 raise Program_Error;
1534 Current_Checking_Mode := Mode_Before;
1538 if Nkind (Expression (PAA)) = N_Null then
1541 -- No globals, nothing to do
1545 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then
1550 Process (Name_Input, Expression (PAA));
1552 elsif Nkind (Expression (PAA)) = N_Aggregate
1553 and then Expressions (Expression (PAA)) /= No_List
1555 -- global => (foo, bar)
1558 RHS := First (Expressions (Expression (PAA)));
1559 while Present (RHS) loop
1564 Process (Name_Input, RHS);
1566 when N_Numeric_Or_String_Literal =>
1567 Process (Name_Input, Original_Node (RHS));
1570 raise Program_Error;
1575 elsif Nkind (Expression (PAA)) = N_Aggregate
1576 and then Component_Associations (Expression (PAA)) /= No_List
1578 -- global => (mode => foo,
1579 -- mode => (bar, baz))
1580 -- A mixture of things
1583 CA : constant List_Id :=
1584 Component_Associations (Expression (PAA));
1587 while Present (Row) loop
1588 pragma Assert (List_Length (Choices (Row)) = 1);
1589 The_Mode := Chars (First (Choices (Row)));
1590 RHS := Expression (Row);
1594 RHS := First (Expressions (RHS));
1595 while Present (RHS) loop
1597 when N_Numeric_Or_String_Literal =>
1598 Process (The_Mode, Original_Node (RHS));
1601 Process (The_Mode, RHS);
1609 Process (The_Mode, RHS);
1614 when N_Numeric_Or_String_Literal =>
1615 Process (The_Mode, Original_Node (RHS));
1618 raise Program_Error;
1625 raise Program_Error;
1634 procedure Check_List (L : List_Id) is
1638 while Present (N) loop
1644 --------------------------
1645 -- Check_Loop_Statement --
1646 --------------------------
1648 procedure Check_Loop_Statement (Loop_N : Node_Id) is
1652 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N));
1653 Loop_Env : constant Perm_Env_Access := new Perm_Env;
1656 -- Save environment prior to the loop
1658 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
1660 -- Add saved environment to loop environment
1662 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
1664 -- If the loop is not a plain-loop, then it may either never be entered,
1665 -- or it may be exited after a number of iterations. Hence add the
1666 -- current permission environment as the initial loop exit environment.
1667 -- Otherwise, the loop exit environment remains empty until it is
1668 -- populated by analyzing exit statements.
1670 if Present (Iteration_Scheme (Loop_N)) then
1672 Exit_Env : constant Perm_Env_Access := new Perm_Env;
1675 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
1676 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
1682 Check_Node (Iteration_Scheme (Loop_N));
1683 Check_List (Statements (Loop_N));
1685 -- Set environment to the one for exiting the loop
1688 Exit_Env : constant Perm_Env_Access :=
1689 Get (Current_Loops_Accumulators, Loop_Name);
1691 Free_Env (Current_Perm_Env);
1693 -- In the normal case, Exit_Env is not null and we use it. In the
1694 -- degraded case of a plain-loop without exit statements, Exit_Env is
1695 -- null, and we use the initial permission environment at the start
1696 -- of the loop to continue analysis. Any environment would be fine
1697 -- here, since the code after the loop is dead code, but this way we
1698 -- avoid spurious errors by having at least variables in scope inside
1701 if Exit_Env /= null then
1702 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
1703 Free_Env (Loop_Env.all);
1704 Free_Env (Exit_Env.all);
1706 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
1707 Free_Env (Loop_Env.all);
1710 end Check_Loop_Statement;
1716 procedure Check_Node (N : Node_Id) is
1717 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1720 when N_Declaration =>
1721 Check_Declaration (N);
1724 Check_Expression (N);
1726 when N_Subtype_Indication =>
1727 Check_Node (Constraint (N));
1730 Check_Node (Get_Body_From_Stub (N));
1732 when N_Statement_Other_Than_Procedure_Call =>
1733 Check_Statement (N);
1735 when N_Package_Body =>
1736 Check_Package_Body (N);
1738 when N_Subprogram_Body
1742 Check_Callable_Body (N);
1744 when N_Protected_Body =>
1745 Check_List (Declarations (N));
1747 when N_Package_Declaration =>
1749 Spec : constant Node_Id := Specification (N);
1752 Current_Checking_Mode := Read;
1753 Check_List (Visible_Declarations (Spec));
1754 Check_List (Private_Declarations (Spec));
1756 Return_Declarations (Visible_Declarations (Spec));
1757 Return_Declarations (Private_Declarations (Spec));
1760 when N_Iteration_Scheme =>
1761 Current_Checking_Mode := Read;
1762 Check_Node (Condition (N));
1763 Check_Node (Iterator_Specification (N));
1764 Check_Node (Loop_Parameter_Specification (N));
1766 when N_Case_Expression_Alternative =>
1767 Current_Checking_Mode := Read;
1768 Check_List (Discrete_Choices (N));
1769 Current_Checking_Mode := Mode_Before;
1770 Check_Node (Expression (N));
1772 when N_Case_Statement_Alternative =>
1773 Current_Checking_Mode := Read;
1774 Check_List (Discrete_Choices (N));
1775 Current_Checking_Mode := Mode_Before;
1776 Check_List (Statements (N));
1778 when N_Component_Association =>
1779 Check_Node (Expression (N));
1781 when N_Handled_Sequence_Of_Statements =>
1782 Check_List (Statements (N));
1784 when N_Parameter_Association =>
1785 Check_Node (Explicit_Actual_Parameter (N));
1787 when N_Range_Constraint =>
1788 Check_Node (Range_Expression (N));
1790 when N_Index_Or_Discriminant_Constraint =>
1791 Check_List (Constraints (N));
1793 -- Checking should not be called directly on these nodes
1795 when N_Abortable_Part
1796 | N_Accept_Alternative
1797 | N_Access_Definition
1798 | N_Access_Function_Definition
1799 | N_Access_Procedure_Definition
1800 | N_Access_To_Object_Definition
1801 | N_Aspect_Specification
1802 | N_Compilation_Unit
1803 | N_Compilation_Unit_Aux
1804 | N_Component_Clause
1805 | N_Component_Definition
1807 | N_Constrained_Array_Definition
1809 | N_Decimal_Fixed_Point_Definition
1810 | N_Defining_Character_Literal
1811 | N_Defining_Identifier
1812 | N_Defining_Operator_Symbol
1813 | N_Defining_Program_Unit_Name
1814 | N_Delay_Alternative
1815 | N_Derived_Type_Definition
1817 | N_Discriminant_Specification
1819 | N_Entry_Body_Formal_Part
1820 | N_Enumeration_Type_Definition
1821 | N_Entry_Call_Alternative
1822 | N_Entry_Index_Specification
1824 | N_Exception_Handler
1825 | N_Floating_Point_Definition
1826 | N_Formal_Decimal_Fixed_Point_Definition
1827 | N_Formal_Derived_Type_Definition
1828 | N_Formal_Discrete_Type_Definition
1829 | N_Formal_Floating_Point_Definition
1830 | N_Formal_Incomplete_Type_Definition
1831 | N_Formal_Modular_Type_Definition
1832 | N_Formal_Ordinary_Fixed_Point_Definition
1833 | N_Formal_Private_Type_Definition
1834 | N_Formal_Signed_Integer_Type_Definition
1835 | N_Generic_Association
1837 | N_Modular_Type_Definition
1838 | N_Ordinary_Fixed_Point_Definition
1839 | N_Package_Specification
1840 | N_Parameter_Specification
1841 | N_Pragma_Argument_Association
1842 | N_Protected_Definition
1843 | N_Push_Pop_xxx_Label
1844 | N_Real_Range_Specification
1845 | N_Record_Definition
1846 | N_SCIL_Dispatch_Table_Tag_Init
1847 | N_SCIL_Dispatching_Call
1848 | N_SCIL_Membership_Test
1849 | N_Signed_Integer_Type_Definition
1852 | N_Terminate_Alternative
1853 | N_Triggering_Alternative
1854 | N_Unconstrained_Array_Definition
1860 raise Program_Error;
1862 -- Unsupported constructs in SPARK
1864 when N_Iterated_Component_Association =>
1865 Error_Msg_N ("unsupported construct in SPARK", N);
1867 -- Ignored constructs for pointer checking
1869 when N_Abstract_Subprogram_Declaration
1871 | N_Attribute_Definition_Clause
1873 | N_Delta_Constraint
1874 | N_Digits_Constraint
1876 | N_Enumeration_Representation_Clause
1877 | N_Exception_Declaration
1878 | N_Exception_Renaming_Declaration
1879 | N_Formal_Package_Declaration
1880 | N_Formal_Subprogram_Declaration
1882 | N_Freeze_Generic_Entity
1883 | N_Function_Instantiation
1884 | N_Generic_Function_Renaming_Declaration
1885 | N_Generic_Package_Declaration
1886 | N_Generic_Package_Renaming_Declaration
1887 | N_Generic_Procedure_Renaming_Declaration
1888 | N_Generic_Subprogram_Declaration
1889 | N_Implicit_Label_Declaration
1892 | N_Number_Declaration
1893 | N_Object_Renaming_Declaration
1895 | N_Package_Instantiation
1896 | N_Package_Renaming_Declaration
1898 | N_Procedure_Instantiation
1899 | N_Record_Representation_Clause
1900 | N_Subprogram_Declaration
1901 | N_Subprogram_Renaming_Declaration
1902 | N_Task_Type_Declaration
1903 | N_Use_Package_Clause
1906 | N_Validate_Unchecked_Conversion
1907 | N_Variable_Reference_Marker
1908 | N_Discriminant_Association
1910 -- ??? check whether we should do sth special for
1911 -- N_Discriminant_Association, or maybe raise a program error.
1914 -- The following nodes are rewritten by semantic analysis
1916 when N_Single_Protected_Declaration
1917 | N_Single_Task_Declaration
1919 raise Program_Error;
1922 Current_Checking_Mode := Mode_Before;
1925 ------------------------
1926 -- Check_Package_Body --
1927 ------------------------
1929 procedure Check_Package_Body (Pack : Node_Id) is
1930 Saved_Env : Perm_Env;
1934 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then
1935 if Get_SPARK_Mode_From_Annotation
1936 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On
1944 CorSp := Parent (Corresponding_Spec (Pack));
1945 while Nkind (CorSp) /= N_Package_Specification loop
1946 CorSp := Parent (CorSp);
1949 Check_List (Visible_Declarations (CorSp));
1953 Copy_Env (Current_Perm_Env, Saved_Env);
1954 Check_List (Private_Declarations (CorSp));
1956 -- Set mode to Read, and then analyze declarations and statements
1958 Current_Checking_Mode := Read;
1959 Check_List (Declarations (Pack));
1960 Check_Node (Handled_Statement_Sequence (Pack));
1962 -- Check RW for every stateful variable (i.e. in declarations)
1964 Return_Declarations (Private_Declarations (CorSp));
1965 Return_Declarations (Visible_Declarations (CorSp));
1966 Return_Declarations (Declarations (Pack));
1968 -- Restore previous environment (i.e. delete every nonvisible
1969 -- declaration) from environment.
1971 Free_Env (Current_Perm_Env);
1972 Copy_Env (Saved_Env, Current_Perm_Env);
1973 end Check_Package_Body;
1975 --------------------
1976 -- Check_Param_In --
1977 --------------------
1979 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is
1980 Mode : constant Entity_Kind := Ekind (Formal);
1981 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
1983 case Formal_Kind'(Mode) is
1985 -- Formal IN parameter
1987 when E_In_Parameter =>
1989 -- Formal IN parameter, access type
1991 if Is_Access_Type (Etype (Formal)) then
1993 -- Formal IN parameter, access to variable type
1995 if not Is_Access_Constant (Etype (Formal)) then
1997 -- Formal IN parameter, named/anonymous access-to-variable
2000 -- In SPARK, IN access-to-variable is an observe operation
2001 -- for a function, and a borrow operation for a procedure.
2003 if Ekind (Scope (Formal)) = E_Function then
2004 Current_Checking_Mode := Observe;
2005 Check_Node (Actual);
2007 Current_Checking_Mode := Borrow;
2008 Check_Node (Actual);
2011 -- Formal IN parameter, access-to-constant type
2012 -- Formal IN parameter, access-to-named-constant type
2014 elsif not Is_Anonymous_Access_Type (Etype (Formal)) then
2015 Error_Msg_N ("assignment not allowed, Ownership Aspect"
2016 & " False (Named general access type)",
2019 -- Formal IN parameter, access to anonymous constant type
2022 Current_Checking_Mode := Observe;
2023 Check_Node (Actual);
2026 -- Formal IN parameter, composite type
2028 elsif Is_Deep (Etype (Formal)) then
2030 -- Composite formal types should be named
2031 -- Formal IN parameter, composite named type
2033 Current_Checking_Mode := Observe;
2034 Check_Node (Actual);
2037 when E_Out_Parameter
2038 | E_In_Out_Parameter
2043 Current_Checking_Mode := Mode_Before;
2046 ----------------------
2047 -- Check_Param_Out --
2048 ----------------------
2050 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id) is
2051 Mode : constant Entity_Kind := Ekind (Formal);
2052 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2055 case Formal_Kind'(Mode) is
2057 -- Formal OUT/IN OUT parameter
2059 when E_Out_Parameter
2060 | E_In_Out_Parameter
2063 -- Formal OUT/IN OUT parameter, access type
2065 if Is_Access_Type (Etype (Formal)) then
2067 -- Formal OUT/IN OUT parameter, access to variable type
2069 if not Is_Access_Constant (Etype (Formal)) then
2071 -- Cannot have anonymous out access parameter
2072 -- Formal out/in out parameter, access to named variable
2075 Current_Checking_Mode := Move;
2076 Check_Node (Actual);
2078 -- Formal out/in out parameter, access to constant type
2081 Error_Msg_N ("assignment not allowed, Ownership Aspect False"
2082 & " (Named general access type)", Formal);
2086 -- Formal out/in out parameter, composite type
2088 elsif Is_Deep (Etype (Formal)) then
2090 -- Composite formal types should be named
2091 -- Formal out/in out Parameter, Composite Named type.
2093 Current_Checking_Mode := Borrow;
2094 Check_Node (Actual);
2097 when E_In_Parameter =>
2101 Current_Checking_Mode := Mode_Before;
2102 end Check_Param_Out;
2104 -------------------------
2105 -- Check_Safe_Pointers --
2106 -------------------------
2108 procedure Check_Safe_Pointers (N : Node_Id) is
2110 -- Local subprograms
2112 procedure Check_List (L : List_Id);
2113 -- Call the main analysis procedure on each element of the list
2115 procedure Initialize;
2116 -- Initialize global variables before starting the analysis of a body
2122 procedure Check_List (L : List_Id) is
2126 while Present (N) loop
2127 Check_Safe_Pointers (N);
2136 procedure Initialize is
2138 Reset (Current_Loops_Envs);
2139 Reset (Current_Loops_Accumulators);
2140 Reset (Current_Perm_Env);
2141 Reset (Current_Initialization_Map);
2148 -- SPARK_Mode pragma in application
2150 -- Start of processing for Check_Safe_Pointers
2155 when N_Compilation_Unit =>
2156 Check_Safe_Pointers (Unit (N));
2159 | N_Package_Declaration
2162 Prag := SPARK_Pragma (Defining_Entity (N));
2163 if Present (Prag) then
2164 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then
2170 elsif Nkind (N) = N_Package_Body then
2171 Check_List (Declarations (N));
2173 elsif Nkind (N) = N_Package_Declaration then
2174 Check_List (Private_Declarations (Specification (N)));
2175 Check_List (Visible_Declarations (Specification (N)));
2181 end Check_Safe_Pointers;
2183 ---------------------
2184 -- Check_Statement --
2185 ---------------------
2187 procedure Check_Statement (Stmt : Node_Id) is
2188 Mode_Before : constant Checking_Mode := Current_Checking_Mode;
2189 State_N : Perm_Kind;
2190 Check : Boolean := True;
2192 Ty_St_Name : Node_Id;
2194 function Get_Root (Comp_Stmt : Node_Id) return Node_Id;
2195 -- Return the root of the name given as input
2197 function Get_Root (Comp_Stmt : Node_Id) return Node_Id is
2199 case Nkind (Comp_Stmt) is
2202 => return Comp_Stmt;
2204 when N_Type_Conversion
2205 | N_Unchecked_Type_Conversion
2206 | N_Qualified_Expression
2208 return Get_Root (Expression (Comp_Stmt));
2210 when N_Parameter_Specification =>
2211 return Get_Root (Defining_Identifier (Comp_Stmt));
2213 when N_Selected_Component
2214 | N_Indexed_Component
2216 | N_Explicit_Dereference
2218 return Get_Root (Prefix (Comp_Stmt));
2221 raise Program_Error;
2226 case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
2227 when N_Entry_Call_Statement =>
2228 Check_Call_Statement (Stmt);
2230 -- Move right-hand side first, and then assign left-hand side
2232 when N_Assignment_Statement =>
2234 St_Name := Name (Stmt);
2235 Ty_St_Name := Etype (Name (Stmt));
2237 -- Check that is not a *general* access type
2239 if Has_Ownership_Aspect_True (St_Name, "assigning to") then
2241 -- Assigning to access type
2243 if Is_Access_Type (Ty_St_Name) then
2245 -- Assigning to access to variable type
2247 if not Is_Access_Constant (Ty_St_Name) then
2249 -- Assigning to named access to variable type
2251 if not Is_Anonymous_Access_Type (Ty_St_Name) then
2252 Current_Checking_Mode := Move;
2254 -- Assigning to anonymous access to variable type
2257 -- Target /= source root
2259 if Nkind_In (Expression (Stmt), N_Allocator, N_Null)
2260 or else Entity (St_Name) /=
2261 Entity (Get_Root (Expression (Stmt)))
2263 Error_Msg_N ("assignment not allowed, anonymous "
2264 & "access Object with Different Root",
2268 -- Target = source root
2271 -- Here we do nothing on the source nor on the
2272 -- target. However, we check the the legality rule:
2273 -- "The source shall be an owning access object
2274 -- denoted by a name that is not in the observed
2277 State_N := Get_Perm (Expression (Stmt));
2278 if State_N = Observed then
2279 Error_Msg_N ("assignment not allowed, Anonymous "
2280 & "access object with the same root"
2281 & " but source Observed", Stmt);
2287 -- else access-to-constant
2289 -- Assigning to anonymous access-to-constant type
2291 elsif Is_Anonymous_Access_Type (Ty_St_Name) then
2293 -- ??? Check the follwing condition. We may have to
2294 -- add that the root is in the observed state too.
2296 State_N := Get_Perm (Expression (Stmt));
2297 if State_N /= Observed then
2298 Error_Msg_N ("assignment not allowed, anonymous "
2299 & "access-to-constant object not in "
2300 & "the observed state)", Stmt);
2304 Error_Msg_N ("?here check accessibility level cited in"
2305 & " the second legality rule of assign",
2310 -- Assigning to named access-to-constant type:
2311 -- This case should have been detected when checking
2312 -- Has_Onwership_Aspect_True (Name (Stmt), "msg").
2315 raise Program_Error;
2318 -- Assigning to composite (deep) type.
2320 elsif Is_Deep (Ty_St_Name) then
2321 if Ekind_In (Ty_St_Name,
2327 First_Component_Or_Discriminant (Ty_St_Name);
2330 while Present (Elmt) loop
2331 if Is_Anonymous_Access_Type (Etype (Elmt)) or
2332 Ekind (Elmt) = E_General_Access_Type
2334 Error_Msg_N ("assignment not allowed, Ownership "
2335 & "Aspect False (Components have "
2336 & "Ownership Aspect False)", Stmt);
2341 Next_Component_Or_Discriminant (Elmt);
2345 -- Record types are always named so this is a move
2348 Current_Checking_Mode := Move;
2351 elsif Ekind_In (Ty_St_Name,
2356 Current_Checking_Mode := Move;
2359 -- Now handle legality rules of using a borrowed, observed,
2360 -- or moved name as a prefix in an assignment.
2363 if Nkind_In (St_Name,
2364 N_Attribute_Reference,
2366 N_Explicit_Dereference,
2367 N_Indexed_Component,
2369 N_Selected_Component,
2373 if Is_Access_Type (Etype (Prefix (St_Name))) or
2374 Is_Deep (Etype (Prefix (St_Name)))
2377 -- We set the Check variable to True so that we can
2378 -- Check_Node of the expression and the name first
2379 -- under the assumption of Current_Checking_Mode =
2380 -- Read => nothing to be done for the RHS if the
2381 -- following check on the expression fails, and
2382 -- Current_Checking_Mode := Assign => the name should
2383 -- not be borrowed or observed so that we can use it
2384 -- as a prefix in the target of an assignement.
2386 -- Note that we do not need to check the OA here
2387 -- because we are allowed to read and write "through"
2388 -- an object of OAF (example: traversing a DS).
2394 if Nkind_In (Expression (Stmt),
2395 N_Attribute_Reference,
2397 N_Explicit_Dereference,
2398 N_Indexed_Component,
2400 N_Selected_Component,
2404 if Is_Access_Type (Etype (Prefix (Expression (Stmt))))
2405 or else Is_Deep (Etype (Prefix (Expression (Stmt))))
2407 Current_Checking_Mode := Observe;
2414 Check_Node (Expression (Stmt));
2415 Current_Checking_Mode := Assign;
2416 Check_Node (St_Name);
2420 when N_Block_Statement =>
2422 Saved_Env : Perm_Env;
2426 Copy_Env (Current_Perm_Env, Saved_Env);
2428 -- Analyze declarations and Handled_Statement_Sequences
2430 Current_Checking_Mode := Read;
2431 Check_List (Declarations (Stmt));
2432 Check_Node (Handled_Statement_Sequence (Stmt));
2434 -- Restore environment
2436 Free_Env (Current_Perm_Env);
2437 Copy_Env (Saved_Env, Current_Perm_Env);
2440 when N_Case_Statement =>
2442 Saved_Env : Perm_Env;
2444 -- Accumulator for the different branches
2447 Elmt : Node_Id := First (Alternatives (Stmt));
2450 Current_Checking_Mode := Read;
2451 Check_Node (Expression (Stmt));
2452 Current_Checking_Mode := Mode_Before;
2456 Copy_Env (Current_Perm_Env, Saved_Env);
2458 -- Here we have the original env in saved, current with a fresh
2459 -- copy, and new aliased.
2461 -- First alternative
2465 Copy_Env (Current_Perm_Env, New_Env);
2466 Free_Env (Current_Perm_Env);
2468 -- Other alternatives
2470 while Present (Elmt) loop
2472 -- Restore environment
2474 Copy_Env (Saved_Env, Current_Perm_Env);
2479 Copy_Env (Saved_Env, Current_Perm_Env);
2481 Free_Env (Saved_Env);
2484 when N_Delay_Relative_Statement =>
2485 Check_Node (Expression (Stmt));
2487 when N_Delay_Until_Statement =>
2488 Check_Node (Expression (Stmt));
2490 when N_Loop_Statement =>
2491 Check_Loop_Statement (Stmt);
2493 -- If deep type expression, then move, else read
2495 when N_Simple_Return_Statement =>
2496 case Nkind (Expression (Stmt)) is
2499 -- ??? This does not take into account the fact that
2500 -- a simple return inside an extended return statement
2501 -- applies to the extended return statement.
2502 Subp : constant Entity_Id :=
2503 Return_Applies_To (Return_Statement_Entity (Stmt));
2505 Return_Globals (Subp);
2509 if Is_Deep (Etype (Expression (Stmt))) then
2510 Current_Checking_Mode := Move;
2516 Check_Node (Expression (Stmt));
2520 when N_Extended_Return_Statement =>
2521 Check_List (Return_Object_Declarations (Stmt));
2522 Check_Node (Handled_Statement_Sequence (Stmt));
2523 Return_Declarations (Return_Object_Declarations (Stmt));
2525 -- ??? This does not take into account the fact that a simple
2526 -- return inside an extended return statement applies to the
2527 -- extended return statement.
2528 Subp : constant Entity_Id :=
2529 Return_Applies_To (Return_Statement_Entity (Stmt));
2532 Return_Globals (Subp);
2535 -- Nothing to do when exiting a loop. No merge needed
2537 when N_Exit_Statement =>
2540 -- Copy environment, run on each branch
2542 when N_If_Statement =>
2544 Saved_Env : Perm_Env;
2546 -- Accumulator for the different branches
2551 Check_Node (Condition (Stmt));
2555 Copy_Env (Current_Perm_Env, Saved_Env);
2557 -- Here we have the original env in saved, current with a fresh
2562 Check_List (Then_Statements (Stmt));
2563 Copy_Env (Current_Perm_Env, New_Env);
2564 Free_Env (Current_Perm_Env);
2566 -- Here the new_environment contains curr env after then block
2574 Elmt := First (Elsif_Parts (Stmt));
2575 while Present (Elmt) loop
2577 -- Transfer into accumulator, and restore from save
2579 Copy_Env (Saved_Env, Current_Perm_Env);
2580 Check_Node (Condition (Elmt));
2581 Check_List (Then_Statements (Stmt));
2588 -- Restore environment before if
2590 Copy_Env (Saved_Env, Current_Perm_Env);
2592 -- Here new environment contains the environment after then and
2593 -- current the fresh copy of old one.
2595 Check_List (Else_Statements (Stmt));
2599 Copy_Env (Saved_Env, Current_Perm_Env);
2602 Free_Env (Saved_Env);
2605 -- Unsupported constructs in SPARK
2607 when N_Abort_Statement
2608 | N_Accept_Statement
2609 | N_Asynchronous_Select
2611 | N_Conditional_Entry_Call
2613 | N_Requeue_Statement
2614 | N_Selective_Accept
2615 | N_Timed_Entry_Call
2617 Error_Msg_N ("unsupported construct in SPARK", Stmt);
2619 -- Ignored constructs for pointer checking
2621 when N_Null_Statement
2626 -- The following nodes are never generated in GNATprove mode
2628 when N_Compound_Statement
2631 raise Program_Error;
2633 end Check_Statement;
2639 function Get_Perm (N : Node_Id) return Perm_Kind is
2640 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
2643 case Tree_Or_Perm.R is
2645 return Tree_Or_Perm.Found_Permission;
2648 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
2649 return Permission (Tree_Or_Perm.Tree_Access);
2651 -- We encoutered a function call, hence the memory area is fresh,
2652 -- which means that the association permission is RW.
2654 when Function_Call =>
2655 return Unrestricted;
2659 ----------------------
2660 -- Get_Perm_Or_Tree --
2661 ----------------------
2663 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
2667 -- Base identifier. Normally those are the roots of the trees stored
2668 -- in the permission environment.
2670 when N_Defining_Identifier =>
2671 raise Program_Error;
2677 P : constant Entity_Id := Entity (N);
2678 C : constant Perm_Tree_Access :=
2679 Get (Current_Perm_Env, Unique_Entity (P));
2682 -- Setting the initialization map to True, so that this
2683 -- variable cannot be ignored anymore when looking at end
2684 -- of elaboration of package.
2686 Set (Current_Initialization_Map, Unique_Entity (P), True);
2688 -- No null possible here, there are no parents for the path.
2689 -- This means we are using a global variable without adding
2690 -- it in environment with a global aspect.
2692 Illegal_Global_Usage (N);
2695 return (R => Unfolded, Tree_Access => C);
2699 when N_Type_Conversion
2700 | N_Unchecked_Type_Conversion
2701 | N_Qualified_Expression
2703 return Get_Perm_Or_Tree (Expression (N));
2705 -- Happening when we try to get the permission of a variable that
2706 -- is a formal parameter. We get instead the defining identifier
2707 -- associated with the parameter (which is the one that has been
2708 -- stored for indexing).
2710 when N_Parameter_Specification =>
2711 return Get_Perm_Or_Tree (Defining_Identifier (N));
2713 -- We get the permission tree of its prefix, and then get either the
2714 -- subtree associated with that specific selection, or if we have a
2715 -- leaf that folds its children, we take the children's permission
2716 -- and return it using the discriminant Folded.
2718 when N_Selected_Component =>
2720 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
2730 pragma Assert (C.Tree_Access /= null);
2731 pragma Assert (Kind (C.Tree_Access) = Entire_Object
2733 Kind (C.Tree_Access) = Record_Component);
2735 if Kind (C.Tree_Access) = Record_Component then
2737 Selected_Component : constant Entity_Id :=
2738 Entity (Selector_Name (N));
2739 Selected_C : constant Perm_Tree_Access :=
2741 (Component (C.Tree_Access), Selected_Component);
2744 if Selected_C = null then
2745 return (R => Unfolded,
2747 Other_Components (C.Tree_Access));
2750 return (R => Unfolded,
2751 Tree_Access => Selected_C);
2755 elsif Kind (C.Tree_Access) = Entire_Object then
2756 return (R => Folded,
2758 Children_Permission (C.Tree_Access));
2761 raise Program_Error;
2765 -- We get the permission tree of its prefix, and then get either the
2766 -- subtree associated with that specific selection, or if we have a
2767 -- leaf that folds its children, we take the children's permission
2768 -- and return it using the discriminant Folded.
2770 when N_Indexed_Component
2774 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
2784 pragma Assert (C.Tree_Access /= null);
2785 pragma Assert (Kind (C.Tree_Access) = Entire_Object
2787 Kind (C.Tree_Access) = Array_Component);
2789 if Kind (C.Tree_Access) = Array_Component then
2790 pragma Assert (Get_Elem (C.Tree_Access) /= null);
2791 return (R => Unfolded,
2792 Tree_Access => Get_Elem (C.Tree_Access));
2794 elsif Kind (C.Tree_Access) = Entire_Object then
2795 return (R => Folded, Found_Permission =>
2796 Children_Permission (C.Tree_Access));
2799 raise Program_Error;
2803 -- We get the permission tree of its prefix, and then get either the
2804 -- subtree associated with that specific selection, or if we have a
2805 -- leaf that folds its children, we take the children's permission
2806 -- and return it using the discriminant Folded.
2808 when N_Explicit_Dereference =>
2810 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
2820 pragma Assert (C.Tree_Access /= null);
2821 pragma Assert (Kind (C.Tree_Access) = Entire_Object
2823 Kind (C.Tree_Access) = Reference);
2825 if Kind (C.Tree_Access) = Reference then
2826 if Get_All (C.Tree_Access) = null then
2830 raise Program_Error;
2835 Tree_Access => Get_All (C.Tree_Access));
2838 elsif Kind (C.Tree_Access) = Entire_Object then
2839 return (R => Folded, Found_Permission =>
2840 Children_Permission (C.Tree_Access));
2843 raise Program_Error;
2847 -- The name contains a function call, hence the given path is always
2848 -- new. We do not have to check for anything.
2850 when N_Function_Call =>
2851 return (R => Function_Call);
2854 raise Program_Error;
2856 end Get_Perm_Or_Tree;
2862 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
2866 -- Base identifier. Normally those are the roots of the trees stored
2867 -- in the permission environment.
2869 when N_Defining_Identifier =>
2870 raise Program_Error;
2876 P : constant Node_Id := Entity (N);
2877 C : constant Perm_Tree_Access :=
2878 Get (Current_Perm_Env, Unique_Entity (P));
2881 -- Setting the initialization map to True, so that this
2882 -- variable cannot be ignored anymore when looking at end
2883 -- of elaboration of package.
2885 Set (Current_Initialization_Map, Unique_Entity (P), True);
2887 -- No null possible here, there are no parents for the path.
2888 -- This means we are using a global variable without adding
2889 -- it in environment with a global aspect.
2891 Illegal_Global_Usage (N);
2898 when N_Type_Conversion
2899 | N_Unchecked_Type_Conversion
2900 | N_Qualified_Expression
2902 return Get_Perm_Tree (Expression (N));
2904 when N_Parameter_Specification =>
2905 return Get_Perm_Tree (Defining_Identifier (N));
2907 -- We get the permission tree of its prefix, and then get either the
2908 -- subtree associated with that specific selection, or if we have a
2909 -- leaf that folds its children, we unroll it in one step.
2911 when N_Selected_Component =>
2913 C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
2918 -- If null then it means we went through a function call
2923 pragma Assert (Kind (C) = Entire_Object
2924 or else Kind (C) = Record_Component);
2926 if Kind (C) = Record_Component then
2928 -- The tree is unfolded. We just return the subtree.
2931 Selected_Component : constant Entity_Id :=
2932 Entity (Selector_Name (N));
2933 Selected_C : constant Perm_Tree_Access :=
2935 (Component (C), Selected_Component);
2938 if Selected_C = null then
2939 return Other_Components (C);
2944 elsif Kind (C) = Entire_Object then
2946 -- Expand the tree. Replace the node with
2947 -- Record_Component.
2951 -- Create the unrolled nodes
2953 Son : Perm_Tree_Access;
2955 Child_Perm : constant Perm_Kind :=
2956 Children_Permission (C);
2959 -- We change the current node from Entire_Object to
2960 -- Record_Component with same permission and an empty
2961 -- hash table as component list.
2964 (Kind => Record_Component,
2965 Is_Node_Deep => Is_Node_Deep (C),
2966 Permission => Permission (C),
2967 Component => Perm_Tree_Maps.Nil,
2969 new Perm_Tree_Wrapper'
2971 (Kind => Entire_Object,
2972 -- Is_Node_Deep is true, to be conservative
2973 Is_Node_Deep => True,
2974 Permission => Child_Perm,
2975 Children_Permission => Child_Perm)
2979 -- We fill the hash table with all sons of the record,
2980 -- with basic Entire_Objects nodes.
2982 Elem := First_Component_Or_Discriminant
2983 (Etype (Prefix (N)));
2985 while Present (Elem) loop
2986 Son := new Perm_Tree_Wrapper'
2988 (Kind => Entire_Object,
2989 Is_Node_Deep => Is_Deep (Etype (Elem)),
2990 Permission => Child_Perm,
2991 Children_Permission => Child_Perm));
2994 (C.all.Tree.Component, Elem, Son);
2995 Next_Component_Or_Discriminant (Elem);
2997 -- we return the tree to the sons, so that the recursion
3001 Selected_Component : constant Entity_Id :=
3002 Entity (Selector_Name (N));
3004 Selected_C : constant Perm_Tree_Access :=
3006 (Component (C), Selected_Component);
3009 pragma Assert (Selected_C /= null);
3014 raise Program_Error;
3017 -- We set the permission tree of its prefix, and then we extract from
3018 -- the returned pointer the subtree. If folded, we unroll the tree at
3021 when N_Indexed_Component
3025 C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N));
3029 -- If null then we went through a function call
3033 pragma Assert (Kind (C) = Entire_Object
3034 or else Kind (C) = Array_Component);
3036 if Kind (C) = Array_Component then
3038 -- The tree is unfolded. We just return the elem subtree
3040 pragma Assert (Get_Elem (C) = null);
3041 return Get_Elem (C);
3043 elsif Kind (C) = Entire_Object then
3045 -- Expand the tree. Replace node with Array_Component.
3047 Son : Perm_Tree_Access;
3050 Son := new Perm_Tree_Wrapper'
3052 (Kind => Entire_Object,
3053 Is_Node_Deep => Is_Node_Deep (C),
3054 Permission => Children_Permission (C),
3055 Children_Permission => Children_Permission (C)));
3057 -- We change the current node from Entire_Object
3058 -- to Array_Component with same permission and the
3059 -- previously defined son.
3061 C.all.Tree := (Kind => Array_Component,
3062 Is_Node_Deep => Is_Node_Deep (C),
3063 Permission => Permission (C),
3065 return Get_Elem (C);
3068 raise Program_Error;
3071 -- We get the permission tree of its prefix, and then get either the
3072 -- subtree associated with that specific selection, or if we have a
3073 -- leaf that folds its children, we unroll the tree.
3075 when N_Explicit_Dereference =>
3077 C : Perm_Tree_Access;
3080 C := Get_Perm_Tree (Prefix (N));
3084 -- If null, we went through a function call
3089 pragma Assert (Kind (C) = Entire_Object
3090 or else Kind (C) = Reference);
3092 if Kind (C) = Reference then
3094 -- The tree is unfolded. We return the elem subtree
3096 if Get_All (C) = null then
3100 raise Program_Error;
3104 elsif Kind (C) = Entire_Object then
3106 -- Expand the tree. Replace the node with Reference.
3108 Son : Perm_Tree_Access;
3111 Son := new Perm_Tree_Wrapper'
3113 (Kind => Entire_Object,
3114 Is_Node_Deep => Is_Deep (Etype (N)),
3115 Permission => Children_Permission (C),
3116 Children_Permission => Children_Permission (C)));
3118 -- We change the current node from Entire_Object to
3119 -- Reference with same permission and the previous son.
3121 pragma Assert (Is_Node_Deep (C));
3122 C.all.Tree := (Kind => Reference,
3123 Is_Node_Deep => Is_Node_Deep (C),
3124 Permission => Permission (C),
3129 raise Program_Error;
3132 -- No permission tree for function calls
3134 when N_Function_Call =>
3138 raise Program_Error;
3146 procedure Hp (P : Perm_Env) is
3147 Elem : Perm_Tree_Maps.Key_Option;
3150 Elem := Get_First_Key (P);
3151 while Elem.Present loop
3152 Print_Node_Briefly (Elem.K);
3153 Elem := Get_Next_Key (P);
3157 --------------------------
3158 -- Illegal_Global_Usage --
3159 --------------------------
3161 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is
3163 Error_Msg_NE ("cannot use global variable & of deep type", N, N);
3164 Error_Msg_N ("\without prior declaration in a Global aspect", N);
3165 Errout.Finalize (Last_Call => True);
3166 Errout.Output_Messages;
3167 Exit_Program (E_Errors);
3168 end Illegal_Global_Usage;
3174 function Is_Deep (E : Entity_Id) return Boolean is
3175 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean;
3176 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is
3178 Pack_Decl : Node_Id;
3181 if Is_Itype (E) then
3182 Decl := Associated_Node_For_Itype (E);
3187 Pack_Decl := Parent (Parent (Decl));
3189 if Nkind (Pack_Decl) /= N_Package_Declaration then
3194 Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl)))
3195 and then Get_SPARK_Mode_From_Annotation
3196 (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off;
3197 end Is_Private_Entity_Mode_Off;
3200 pragma Assert (Is_Type (E));
3208 -- Just check the depth of its component type
3213 return Is_Deep (Component_Type (E));
3215 when E_String_Literal_Subtype =>
3218 -- Per RM 8.11 for class-wide types
3220 when E_Class_Wide_Subtype
3225 -- ??? What about hidden components
3234 Elmt := First_Component_Or_Discriminant (E);
3235 while Present (Elmt) loop
3236 if Is_Deep (Etype (Elmt)) then
3239 Next_Component_Or_Discriminant (Elmt);
3245 when Private_Kind =>
3246 if Is_Private_Entity_Mode_Off (E) then
3249 if Present (Full_View (E)) then
3250 return Is_Deep (Full_View (E));
3256 when E_Incomplete_Type
3257 | E_Incomplete_Subtype
3261 -- No problem with synchronized types
3263 when E_Protected_Type
3264 | E_Protected_Subtype
3270 when E_Exception_Type =>
3274 raise Program_Error;
3282 procedure Perm_Error
3285 Found_Perm : Perm_Kind)
3287 procedure Set_Root_Object
3289 Obj : out Entity_Id;
3290 Deref : out Boolean);
3291 -- Set the root object Obj, and whether the path contains a dereference,
3292 -- from a path Path.
3294 ---------------------
3295 -- Set_Root_Object --
3296 ---------------------
3298 procedure Set_Root_Object
3300 Obj : out Entity_Id;
3301 Deref : out Boolean)
3304 case Nkind (Path) is
3308 Obj := Entity (Path);
3311 when N_Type_Conversion
3312 | N_Unchecked_Type_Conversion
3313 | N_Qualified_Expression
3315 Set_Root_Object (Expression (Path), Obj, Deref);
3317 when N_Indexed_Component
3318 | N_Selected_Component
3321 Set_Root_Object (Prefix (Path), Obj, Deref);
3323 when N_Explicit_Dereference =>
3324 Set_Root_Object (Prefix (Path), Obj, Deref);
3328 raise Program_Error;
3330 end Set_Root_Object;
3336 -- Start of processing for Perm_Error
3339 Set_Root_Object (N, Root, Is_Deref);
3343 ("insufficient permission on dereference from &", N, Root);
3345 Error_Msg_NE ("insufficient permission for &", N, Root);
3348 Perm_Mismatch (Perm, Found_Perm, N);
3351 -------------------------------
3352 -- Perm_Error_Subprogram_End --
3353 -------------------------------
3355 procedure Perm_Error_Subprogram_End
3359 Found_Perm : Perm_Kind)
3362 Error_Msg_Node_2 := Subp;
3363 Error_Msg_NE ("insufficient permission for & when returning from &",
3365 Perm_Mismatch (Perm, Found_Perm, Subp);
3366 end Perm_Error_Subprogram_End;
3372 procedure Process_Path (N : Node_Id) is
3373 Root : constant Entity_Id := Get_Enclosing_Object (N);
3374 State_N : Perm_Kind;
3376 -- We ignore if yielding to synchronized
3379 and then Is_Synchronized_Object (Root)
3384 State_N := Get_Perm (N);
3386 case Current_Checking_Mode is
3388 -- Check permission R, do nothing
3392 -- This condition should be removed when removing the read
3399 -- The rhs object in an assignment statement (including copy in
3400 -- and copy back) should be in the Unrestricted or Moved state.
3401 -- Otherwise the move is not allowed.
3402 -- This applies to both stand-alone and composite objects.
3403 -- If the state of the source is Moved, then a warning message
3404 -- is prompt to make the user aware of reading a nullified
3407 if State_N /= Unrestricted and State_N /= Moved then
3408 Perm_Error (N, Unrestricted, State_N);
3412 -- In the AI, after moving a path nothing to do since the rhs
3413 -- object was in the Unrestricted state and it shall be
3414 -- refreshed to Unrestricted. The object should be nullified
3415 -- however. To avoid moving again a name that has already been
3416 -- moved, in this implementation we set the state of the moved
3417 -- object to "Moved". This shall be used to prompt a warning
3418 -- when manipulating a null pointer and also to implement
3419 -- the no aliasing parameter restriction.
3421 if State_N = Moved then
3422 Error_Msg_N ("?the source or one of its extensions has"
3423 & " already been moved", N);
3427 -- Set state to Moved to the path and any of its prefixes
3429 Tree : constant Perm_Tree_Access :=
3430 Set_Perm_Prefixes (N, Moved);
3435 -- We went through a function call, no permission to
3441 -- Set state to Moved on any strict extension of the path
3443 Set_Perm_Extensions (Tree, Moved);
3448 -- The lhs object in an assignment statement (including copy in
3449 -- and copy back) should be in the Unrestricted state.
3450 -- Otherwise the move is not allowed.
3451 -- This applies to both stand-alone and composite objects.
3453 if State_N /= Unrestricted and State_N /= Moved then
3454 Perm_Error (N, Unrestricted, State_N);
3458 -- After assigning to a path nothing to do since it was in the
3459 -- Unrestricted state and it would be refreshed to
3464 -- Borrowing is only allowed on Unrestricted objects.
3466 if State_N /= Unrestricted and State_N /= Moved then
3467 Perm_Error (N, Unrestricted, State_N);
3470 if State_N = Moved then
3471 Error_Msg_N ("?the source or one of its extensions has"
3472 & " already been moved", N);
3476 -- Set state to Borrowed to the path and any of its prefixes
3478 Tree : constant Perm_Tree_Access :=
3479 Set_Perm_Prefixes (N, Borrowed);
3484 -- We went through a function call, no permission to
3490 -- Set state to Borrowed on any strict extension of the path
3492 Set_Perm_Extensions (Tree, Borrowed);
3496 if State_N /= Unrestricted
3497 and then State_N /= Observed
3499 Perm_Error (N, Observed, State_N);
3503 -- Set permission to Observed on the path and any of its
3504 -- prefixes if it is of a deep type. Actually, some operation
3505 -- like reading from an object of access type is considered as
3506 -- observe while it should not affect the permissions of
3507 -- the considered tree.
3509 Tree : Perm_Tree_Access;
3512 if Is_Deep (Etype (N)) then
3513 Tree := Set_Perm_Prefixes (N, Observed);
3520 -- We went through a function call, no permission to
3526 -- Set permissions to No on any strict extension of the path
3528 Set_Perm_Extensions (Tree, Observed);
3533 -------------------------
3534 -- Return_Declarations --
3535 -------------------------
3537 procedure Return_Declarations (L : List_Id) is
3538 procedure Return_Declaration (Decl : Node_Id);
3539 -- Check correct permissions for every declared object
3541 ------------------------
3542 -- Return_Declaration --
3543 ------------------------
3545 procedure Return_Declaration (Decl : Node_Id) is
3547 if Nkind (Decl) = N_Object_Declaration then
3549 -- Check RW for object declared, unless the object has never been
3552 if Get (Current_Initialization_Map,
3553 Unique_Entity (Defining_Identifier (Decl))) = False
3559 Elem : constant Perm_Tree_Access :=
3560 Get (Current_Perm_Env,
3561 Unique_Entity (Defining_Identifier (Decl)));
3566 -- Here we are on a declaration. Hence it should have been
3567 -- added in the environment when analyzing this node with
3568 -- mode Read. Hence it is not possible to find a null
3573 raise Program_Error;
3576 if Permission (Elem) /= Unrestricted then
3577 Perm_Error (Decl, Unrestricted, Permission (Elem));
3581 end Return_Declaration;
3586 -- Start of processing for Return_Declarations
3590 while Present (N) loop
3591 Return_Declaration (N);
3594 end Return_Declarations;
3596 --------------------
3597 -- Return_Globals --
3598 --------------------
3600 procedure Return_Globals (Subp : Entity_Id) is
3601 procedure Return_Globals_From_List
3602 (First_Item : Node_Id;
3603 Kind : Formal_Kind);
3604 -- Return global items from the list starting at Item
3606 procedure Return_Globals_Of_Mode (Global_Mode : Name_Id);
3607 -- Return global items for the mode Global_Mode
3609 ------------------------------
3610 -- Return_Globals_From_List --
3611 ------------------------------
3613 procedure Return_Globals_From_List
3614 (First_Item : Node_Id;
3617 Item : Node_Id := First_Item;
3621 while Present (Item) loop
3624 -- Ignore abstract states, which play no role in pointer aliasing
3626 if Ekind (E) = E_Abstract_State then
3629 Return_The_Global (E, Kind, Subp);
3633 end Return_Globals_From_List;
3635 ----------------------------
3636 -- Return_Globals_Of_Mode --
3637 ----------------------------
3639 procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is
3647 Kind := E_In_Parameter;
3649 Kind := E_Out_Parameter;
3651 Kind := E_In_Out_Parameter;
3653 raise Program_Error;
3656 -- Return both global items from Global and Refined_Global pragmas
3658 Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
3659 Return_Globals_From_List
3660 (First_Global (Subp, Global_Mode, Refined => True), Kind);
3661 end Return_Globals_Of_Mode;
3663 -- Start of processing for Return_Globals
3666 Return_Globals_Of_Mode (Name_Proof_In);
3667 Return_Globals_Of_Mode (Name_Input);
3668 Return_Globals_Of_Mode (Name_Output);
3669 Return_Globals_Of_Mode (Name_In_Out);
3672 --------------------------------
3673 -- Return_Parameter_Or_Global --
3674 --------------------------------
3676 procedure Return_The_Global
3681 Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
3682 pragma Assert (Elem /= null);
3685 -- Observed IN parameters and globals need not return a permission to
3688 if Mode = E_In_Parameter
3690 -- Check this for read-only globals.
3693 if Permission (Elem) /= Unrestricted
3694 and then Permission (Elem) /= Observed
3696 Perm_Error_Subprogram_End
3700 Found_Perm => Permission (Elem));
3703 -- All globals of mode out or in/out should return with mode
3707 if Permission (Elem) /= Unrestricted then
3708 Perm_Error_Subprogram_End
3711 Perm => Unrestricted,
3712 Found_Perm => Permission (Elem));
3715 end Return_The_Global;
3717 -------------------------
3718 -- Set_Perm_Extensions --
3719 -------------------------
3721 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is
3722 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
3723 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
3726 when Entire_Object =>
3730 Free_Perm_Tree (T.all.Tree.Get_All);
3732 when Array_Component =>
3733 Free_Perm_Tree (T.all.Tree.Get_Elem);
3735 -- Free every Component subtree
3737 when Record_Component =>
3739 Comp : Perm_Tree_Access;
3742 Comp := Perm_Tree_Maps.Get_First (Component (T));
3743 while Comp /= null loop
3744 Free_Perm_Tree (Comp);
3745 Comp := Perm_Tree_Maps.Get_Next (Component (T));
3748 Free_Perm_Tree (T.all.Tree.Other_Components);
3751 end Free_Perm_Tree_Children;
3753 Son : constant Perm_Tree :=
3755 (Kind => Entire_Object,
3756 Is_Node_Deep => Is_Node_Deep (T),
3757 Permission => Permission (T),
3758 Children_Permission => P);
3761 Free_Perm_Tree_Children (T);
3763 end Set_Perm_Extensions;
3765 ------------------------------
3766 -- Set_Perm_Prefixes --
3767 ------------------------------
3769 function Set_Perm_Prefixes
3771 New_Perm : Perm_Kind)
3772 return Perm_Tree_Access
3780 | N_Defining_Identifier
3782 if Nkind (N) = N_Defining_Identifier
3783 and then New_Perm = Borrowed
3785 raise Program_Error;
3790 C : Perm_Tree_Access;
3793 if Nkind (N) = N_Defining_Identifier then
3799 C := Get (Current_Perm_Env, Unique_Entity (P));
3800 pragma Assert (C /= null);
3802 -- Setting the initialization map to True, so that this
3803 -- variable cannot be ignored anymore when looking at end
3804 -- of elaboration of package.
3806 Set (Current_Initialization_Map, Unique_Entity (P), True);
3807 if New_Perm = Observed
3811 -- No null possible here, there are no parents for the path.
3812 -- This means we are using a global variable without adding
3813 -- it in environment with a global aspect.
3815 Illegal_Global_Usage (N);
3818 C.all.Tree.Permission := New_Perm;
3822 when N_Type_Conversion
3823 | N_Unchecked_Type_Conversion
3824 | N_Qualified_Expression
3826 return Set_Perm_Prefixes (Expression (N), New_Perm);
3828 when N_Parameter_Specification =>
3829 raise Program_Error;
3831 -- We set the permission tree of its prefix, and then we extract
3832 -- our subtree from the returned pointer and assign an adequate
3833 -- permission to it, if unfolded. If folded, we unroll the tree
3836 when N_Selected_Component =>
3838 C : constant Perm_Tree_Access :=
3839 Set_Perm_Prefixes (Prefix (N), New_Perm);
3844 -- We went through a function call, do nothing
3849 pragma Assert (Kind (C) = Entire_Object
3850 or else Kind (C) = Record_Component);
3852 if Kind (C) = Record_Component then
3853 -- The tree is unfolded. We just modify the permission and
3854 -- return the record subtree.
3857 Selected_Component : constant Entity_Id :=
3858 Entity (Selector_Name (N));
3860 Selected_C : Perm_Tree_Access :=
3862 (Component (C), Selected_Component);
3865 if Selected_C = null then
3866 Selected_C := Other_Components (C);
3869 pragma Assert (Selected_C /= null);
3870 Selected_C.all.Tree.Permission := New_Perm;
3874 elsif Kind (C) = Entire_Object then
3876 -- Expand the tree. Replace the node with
3877 -- Record_Component.
3881 -- Create an empty hash table
3883 Hashtbl : Perm_Tree_Maps.Instance;
3885 -- We create the unrolled nodes, that will all have same
3886 -- permission than parent.
3888 Son : Perm_Tree_Access;
3889 Children_Perm : constant Perm_Kind :=
3890 Children_Permission (C);
3893 -- We change the current node from Entire_Object to
3894 -- Record_Component with same permission and an empty
3895 -- hash table as component list.
3898 (Kind => Record_Component,
3899 Is_Node_Deep => Is_Node_Deep (C),
3900 Permission => Permission (C),
3901 Component => Hashtbl,
3903 new Perm_Tree_Wrapper'
3905 (Kind => Entire_Object,
3906 Is_Node_Deep => True,
3907 Permission => Children_Perm,
3908 Children_Permission => Children_Perm)
3911 -- We fill the hash table with all sons of the record,
3912 -- with basic Entire_Objects nodes.
3914 Elem := First_Component_Or_Discriminant
3915 (Etype (Prefix (N)));
3917 while Present (Elem) loop
3918 Son := new Perm_Tree_Wrapper'
3920 (Kind => Entire_Object,
3921 Is_Node_Deep => Is_Deep (Etype (Elem)),
3922 Permission => Children_Perm,
3923 Children_Permission => Children_Perm));
3925 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
3926 Next_Component_Or_Discriminant (Elem);
3928 -- Now we set the right field to Borrowed, and then we
3929 -- return the tree to the sons, so that the recursion can
3933 Selected_Component : constant Entity_Id :=
3934 Entity (Selector_Name (N));
3935 Selected_C : Perm_Tree_Access :=
3937 (Component (C), Selected_Component);
3940 if Selected_C = null then
3941 Selected_C := Other_Components (C);
3944 pragma Assert (Selected_C /= null);
3945 Selected_C.all.Tree.Permission := New_Perm;
3950 raise Program_Error;
3954 -- We set the permission tree of its prefix, and then we extract
3955 -- from the returned pointer the subtree and assign an adequate
3956 -- permission to it, if unfolded. If folded, we unroll the tree in
3959 when N_Indexed_Component
3963 C : constant Perm_Tree_Access :=
3964 Set_Perm_Prefixes (Prefix (N), New_Perm);
3969 -- We went through a function call, do nothing
3974 pragma Assert (Kind (C) = Entire_Object
3975 or else Kind (C) = Array_Component);
3977 if Kind (C) = Array_Component then
3979 -- The tree is unfolded. We just modify the permission and
3980 -- return the elem subtree.
3982 pragma Assert (Get_Elem (C) /= null);
3983 C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm;
3984 return Get_Elem (C);
3986 elsif Kind (C) = Entire_Object then
3988 -- Expand the tree. Replace node with Array_Component.
3990 Son : Perm_Tree_Access;
3993 Son := new Perm_Tree_Wrapper'
3995 (Kind => Entire_Object,
3996 Is_Node_Deep => Is_Node_Deep (C),
3997 Permission => New_Perm,
3998 Children_Permission => Children_Permission (C)));
4000 -- Children_Permission => Children_Permission (C)
4001 -- this line should be checked maybe New_Perm
4002 -- instead of Children_Permission (C)
4004 -- We change the current node from Entire_Object
4005 -- to Array_Component with same permission and the
4006 -- previously defined son.
4008 C.all.Tree := (Kind => Array_Component,
4009 Is_Node_Deep => Is_Node_Deep (C),
4010 Permission => New_Perm,
4012 return Get_Elem (C);
4015 raise Program_Error;
4019 -- We set the permission tree of its prefix, and then we extract
4020 -- from the returned pointer the subtree and assign an adequate
4021 -- permission to it, if unfolded. If folded, we unroll the tree
4024 when N_Explicit_Dereference =>
4026 C : constant Perm_Tree_Access :=
4027 Set_Perm_Prefixes (Prefix (N), New_Perm);
4032 -- We went through a function call. Do nothing.
4037 pragma Assert (Kind (C) = Entire_Object
4038 or else Kind (C) = Reference);
4040 if Kind (C) = Reference then
4042 -- The tree is unfolded. We just modify the permission and
4043 -- return the elem subtree.
4045 pragma Assert (Get_All (C) /= null);
4046 C.all.Tree.Get_All.all.Tree.Permission := New_Perm;
4049 elsif Kind (C) = Entire_Object then
4051 -- Expand the tree. Replace the node with Reference.
4053 Son : Perm_Tree_Access;
4056 Son := new Perm_Tree_Wrapper'
4058 (Kind => Entire_Object,
4059 Is_Node_Deep => Is_Deep (Etype (N)),
4060 Permission => New_Perm,
4061 Children_Permission => Children_Permission (C)));
4063 -- We change the current node from Entire_Object to
4064 -- Reference with Borrowed and the previous son.
4066 pragma Assert (Is_Node_Deep (C));
4067 C.all.Tree := (Kind => Reference,
4068 Is_Node_Deep => Is_Node_Deep (C),
4069 Permission => New_Perm,
4075 raise Program_Error;
4079 when N_Function_Call =>
4083 raise Program_Error;
4085 end Set_Perm_Prefixes;
4087 ------------------------------
4088 -- Set_Perm_Prefixes_Borrow --
4089 ------------------------------
4091 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access
4094 pragma Assert (Current_Checking_Mode = Borrow);
4101 P : constant Node_Id := Entity (N);
4102 C : constant Perm_Tree_Access :=
4103 Get (Current_Perm_Env, Unique_Entity (P));
4104 pragma Assert (C /= null);
4107 -- Setting the initialization map to True, so that this
4108 -- variable cannot be ignored anymore when looking at end
4109 -- of elaboration of package.
4111 Set (Current_Initialization_Map, Unique_Entity (P), True);
4112 C.all.Tree.Permission := Borrowed;
4116 when N_Type_Conversion
4117 | N_Unchecked_Type_Conversion
4118 | N_Qualified_Expression
4120 return Set_Perm_Prefixes_Borrow (Expression (N));
4122 when N_Parameter_Specification
4123 | N_Defining_Identifier
4125 raise Program_Error;
4127 -- We set the permission tree of its prefix, and then we extract
4128 -- our subtree from the returned pointer and assign an adequate
4129 -- permission to it, if unfolded. If folded, we unroll the tree
4132 when N_Selected_Component =>
4134 C : constant Perm_Tree_Access :=
4135 Set_Perm_Prefixes_Borrow (Prefix (N));
4140 -- We went through a function call, do nothing
4145 -- The permission of the returned node should be No
4147 pragma Assert (Permission (C) = Borrowed);
4148 pragma Assert (Kind (C) = Entire_Object
4149 or else Kind (C) = Record_Component);
4151 if Kind (C) = Record_Component then
4153 -- The tree is unfolded. We just modify the permission and
4154 -- return the record subtree.
4157 Selected_Component : constant Entity_Id :=
4158 Entity (Selector_Name (N));
4159 Selected_C : Perm_Tree_Access :=
4161 (Component (C), Selected_Component);
4164 if Selected_C = null then
4165 Selected_C := Other_Components (C);
4168 pragma Assert (Selected_C /= null);
4169 Selected_C.all.Tree.Permission := Borrowed;
4173 elsif Kind (C) = Entire_Object then
4175 -- Expand the tree. Replace the node with
4176 -- Record_Component.
4180 -- Create an empty hash table
4182 Hashtbl : Perm_Tree_Maps.Instance;
4184 -- We create the unrolled nodes, that will all have same
4185 -- permission than parent.
4187 Son : Perm_Tree_Access;
4188 ChildrenPerm : constant Perm_Kind :=
4189 Children_Permission (C);
4192 -- We change the current node from Entire_Object to
4193 -- Record_Component with same permission and an empty
4194 -- hash table as component list.
4197 (Kind => Record_Component,
4198 Is_Node_Deep => Is_Node_Deep (C),
4199 Permission => Permission (C),
4200 Component => Hashtbl,
4202 new Perm_Tree_Wrapper'
4204 (Kind => Entire_Object,
4205 Is_Node_Deep => True,
4206 Permission => ChildrenPerm,
4207 Children_Permission => ChildrenPerm)
4210 -- We fill the hash table with all sons of the record,
4211 -- with basic Entire_Objects nodes.
4213 Elem := First_Component_Or_Discriminant
4214 (Etype (Prefix (N)));
4216 while Present (Elem) loop
4217 Son := new Perm_Tree_Wrapper'
4219 (Kind => Entire_Object,
4220 Is_Node_Deep => Is_Deep (Etype (Elem)),
4221 Permission => ChildrenPerm,
4222 Children_Permission => ChildrenPerm));
4223 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son);
4224 Next_Component_Or_Discriminant (Elem);
4227 -- Now we set the right field to Borrowed, and then we
4228 -- return the tree to the sons, so that the recursion can
4232 Selected_Component : constant Entity_Id :=
4233 Entity (Selector_Name (N));
4234 Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get
4235 (Component (C), Selected_Component);
4238 if Selected_C = null then
4239 Selected_C := Other_Components (C);
4242 pragma Assert (Selected_C /= null);
4243 Selected_C.all.Tree.Permission := Borrowed;
4249 raise Program_Error;
4253 -- We set the permission tree of its prefix, and then we extract
4254 -- from the returned pointer the subtree and assign an adequate
4255 -- permission to it, if unfolded. If folded, we unroll the tree in
4258 when N_Indexed_Component
4262 C : constant Perm_Tree_Access :=
4263 Set_Perm_Prefixes_Borrow (Prefix (N));
4268 -- We went through a function call, do nothing
4273 pragma Assert (Permission (C) = Borrowed);
4274 pragma Assert (Kind (C) = Entire_Object
4275 or else Kind (C) = Array_Component);
4277 if Kind (C) = Array_Component then
4279 -- The tree is unfolded. We just modify the permission and
4280 -- return the elem subtree.
4282 pragma Assert (Get_Elem (C) /= null);
4283 C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed;
4284 return Get_Elem (C);
4286 elsif Kind (C) = Entire_Object then
4288 -- Expand the tree. Replace node with Array_Component.
4290 Son : Perm_Tree_Access;
4293 Son := new Perm_Tree_Wrapper'
4295 (Kind => Entire_Object,
4296 Is_Node_Deep => Is_Node_Deep (C),
4297 Permission => Borrowed,
4298 Children_Permission => Children_Permission (C)));
4300 -- We change the current node from Entire_Object
4301 -- to Array_Component with same permission and the
4302 -- previously defined son.
4304 C.all.Tree := (Kind => Array_Component,
4305 Is_Node_Deep => Is_Node_Deep (C),
4306 Permission => Borrowed,
4308 return Get_Elem (C);
4312 raise Program_Error;
4316 -- We set the permission tree of its prefix, and then we extract
4317 -- from the returned pointer the subtree and assign an adequate
4318 -- permission to it, if unfolded. If folded, we unroll the tree
4321 when N_Explicit_Dereference =>
4323 C : constant Perm_Tree_Access :=
4324 Set_Perm_Prefixes_Borrow (Prefix (N));
4329 -- We went through a function call. Do nothing.
4334 -- The permission of the returned node should be No
4336 pragma Assert (Permission (C) = Borrowed);
4337 pragma Assert (Kind (C) = Entire_Object
4338 or else Kind (C) = Reference);
4340 if Kind (C) = Reference then
4342 -- The tree is unfolded. We just modify the permission and
4343 -- return the elem subtree.
4345 pragma Assert (Get_All (C) /= null);
4346 C.all.Tree.Get_All.all.Tree.Permission := Borrowed;
4349 elsif Kind (C) = Entire_Object then
4351 -- Expand the tree. Replace the node with Reference.
4353 Son : Perm_Tree_Access;
4356 Son := new Perm_Tree_Wrapper'
4358 (Kind => Entire_Object,
4359 Is_Node_Deep => Is_Deep (Etype (N)),
4360 Permission => Borrowed,
4361 Children_Permission => Children_Permission (C)));
4363 -- We change the current node from Entire_Object to
4364 -- Reference with Borrowed and the previous son.
4366 pragma Assert (Is_Node_Deep (C));
4367 C.all.Tree := (Kind => Reference,
4368 Is_Node_Deep => Is_Node_Deep (C),
4369 Permission => Borrowed,
4375 raise Program_Error;
4379 when N_Function_Call =>
4383 raise Program_Error;
4385 end Set_Perm_Prefixes_Borrow;
4391 procedure Setup_Globals (Subp : Entity_Id) is
4392 procedure Setup_Globals_From_List
4393 (First_Item : Node_Id;
4394 Kind : Formal_Kind);
4395 -- Set up global items from the list starting at Item
4397 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id);
4398 -- Set up global items for the mode Global_Mode
4400 -----------------------------
4401 -- Setup_Globals_From_List --
4402 -----------------------------
4404 procedure Setup_Globals_From_List
4405 (First_Item : Node_Id;
4408 Item : Node_Id := First_Item;
4412 while Present (Item) loop
4415 -- Ignore abstract states, which play no role in pointer aliasing
4417 if Ekind (E) = E_Abstract_State then
4420 Setup_Parameter_Or_Global (E, Kind, Global_Var => True);
4424 end Setup_Globals_From_List;
4426 ---------------------------
4427 -- Setup_Globals_Of_Mode --
4428 ---------------------------
4430 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is
4438 Kind := E_In_Parameter;
4441 Kind := E_Out_Parameter;
4444 Kind := E_In_Out_Parameter;
4447 raise Program_Error;
4450 -- Set up both global items from Global and Refined_Global pragmas
4452 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
4453 Setup_Globals_From_List
4454 (First_Global (Subp, Global_Mode, Refined => True), Kind);
4455 end Setup_Globals_Of_Mode;
4457 -- Start of processing for Setup_Globals
4460 Setup_Globals_Of_Mode (Name_Proof_In);
4461 Setup_Globals_Of_Mode (Name_Input);
4462 Setup_Globals_Of_Mode (Name_Output);
4463 Setup_Globals_Of_Mode (Name_In_Out);
4466 -------------------------------
4467 -- Setup_Parameter_Or_Global --
4468 -------------------------------
4470 procedure Setup_Parameter_Or_Global
4473 Global_Var : Boolean)
4475 Elem : Perm_Tree_Access;
4476 View_Typ : Entity_Id;
4479 if Present (Full_View (Etype (Id))) then
4480 View_Typ := Full_View (Etype (Id));
4482 View_Typ := Etype (Id);
4485 Elem := new Perm_Tree_Wrapper'
4487 (Kind => Entire_Object,
4488 Is_Node_Deep => Is_Deep (Etype (Id)),
4489 Permission => Unrestricted,
4490 Children_Permission => Unrestricted));
4494 -- All out and in out parameters are considered to be unrestricted.
4495 -- They are whether borrowed or moved. Ada Rules would restrict
4496 -- these permissions further. For example an in parameter cannot
4499 -- In the following we deal with in parameters that can be observed.
4500 -- We only consider the observing cases.
4502 when E_In_Parameter =>
4504 -- Handling global variables as IN parameters here.
4505 -- Remove the following condition once it's decided how globals
4506 -- should be considered. ???
4508 -- In SPARK, IN access-to-variable is an observe operation for
4509 -- a function, and a borrow operation for a procedure.
4511 if not Global_Var then
4512 if (Is_Access_Type (View_Typ)
4513 and then Is_Access_Constant (View_Typ)
4514 and then Is_Anonymous_Access_Type (View_Typ))
4516 (Is_Access_Type (View_Typ)
4517 and then Ekind (Scope (Id)) = E_Function)
4519 (not Is_Access_Type (View_Typ)
4520 and then Is_Deep (View_Typ)
4521 and then not Is_Anonymous_Access_Type (View_Typ))
4523 Elem.all.Tree.Permission := Observed;
4524 Elem.all.Tree.Children_Permission := Observed;
4527 Elem.all.Tree.Permission := Unrestricted;
4528 Elem.all.Tree.Children_Permission := Unrestricted;
4532 Elem.all.Tree.Permission := Observed;
4533 Elem.all.Tree.Children_Permission := Observed;
4536 -- When out or in/out formal or global parameters, we set them to
4537 -- the Unrestricted state. "We want to be able to assume that all
4538 -- relevant writable globals are unrestricted when a subprogram
4539 -- starts executing". Formal parameters of mode out or in/out
4540 -- are whether Borrowers or the targets of a move operation:
4541 -- they start theirs lives in the subprogram as Unrestricted.
4544 Elem.all.Tree.Permission := Unrestricted;
4545 Elem.all.Tree.Children_Permission := Unrestricted;
4548 Set (Current_Perm_Env, Id, Elem);
4549 end Setup_Parameter_Or_Global;
4551 ----------------------
4552 -- Setup_Parameters --
4553 ----------------------
4555 procedure Setup_Parameters (Subp : Entity_Id) is Formal : Entity_Id;
4557 Formal := First_Formal (Subp);
4558 while Present (Formal) loop
4559 Setup_Parameter_Or_Global
4560 (Formal, Ekind (Formal), Global_Var => False);
4561 Next_Formal (Formal);
4563 end Setup_Parameters;
4565 -------------------------------
4566 -- Has_Ownership_Aspect_True --
4567 -------------------------------
4569 function Has_Ownership_Aspect_True
4575 case Ekind (Etype (N)) is
4577 if Ekind (Etype (N)) = E_General_Access_Type then
4578 Error_Msg_NE (Msg & " & not allowed " &
4579 "(Named General Access type)", N, N);
4590 Com_Ty : constant Node_Id := Component_Type (Etype (N));
4591 Ret : Boolean := Has_Ownership_Aspect_True (Com_Ty, "");
4594 if Nkind (Parent (N)) = N_Full_Type_Declaration and
4595 Is_Anonymous_Access_Type (Com_Ty)
4601 Error_Msg_NE (Msg & " & not allowed "
4602 & "(Components of Named General Access type or"
4603 & " Anonymous type)", N, N);
4608 -- ??? What about hidden components
4615 Elmt_T_Perm : Boolean := True;
4616 Elmt_Perm, Elmt_Anonym : Boolean;
4619 Elmt := First_Component_Or_Discriminant (Etype (N));
4620 while Present (Elmt) loop
4621 Elmt_Perm := Has_Ownership_Aspect_True (Elmt,
4622 "type of component");
4623 Elmt_Anonym := Is_Anonymous_Access_Type (Etype (Elmt));
4626 ("type of component & not allowed"
4627 & " (Components of Anonymous type)", Elmt, Elmt);
4629 Elmt_T_Perm := Elmt_T_Perm and Elmt_Perm and not Elmt_Anonym;
4630 Next_Component_Or_Discriminant (Elmt);
4632 if not Elmt_T_Perm then
4634 (Msg & " & not allowed (One or "
4635 & "more components have Ownership Aspect False)",
4645 end Has_Ownership_Aspect_True;