1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- S E M _ S P A R K --
9 -- Copyright (C) 2017-2019, 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 with Paths --
47 ---------------------------------------------------
49 package Permissions is
50 Elaboration_Context_Max : constant := 1009;
53 type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
55 function Elaboration_Context_Hash
56 (Key : Entity_Id) return Elaboration_Context_Index;
59 -- Permission type associated with paths. These are related to but not
60 -- the same as the states associated with names used in SPARK RM 3.10:
61 -- Unrestricted, Observed, Borrowed, Moved. When ownership rules lead to
62 -- a state change for a name, this may correspond to multiple permission
63 -- changes for the paths corresponding to the name, its prefixes, and
64 -- its extensions. For example, when an object is assigned to, the
65 -- corresponding name gets into state Moved, while the path for the name
66 -- gets permission Write_Only as well as every prefix of the name, and
67 -- every suffix gets permission No_Access.
69 type Perm_Kind_Option is
71 -- Special value used when no permission is passed around
74 -- The path cannot be accessed for reading or writing. This is the
75 -- case for the path of a name in the Borrowed state.
78 -- The path can only be accessed for reading. This is the case for
79 -- the path of a name in the Observed state.
82 -- The path can be accessed for both reading and writing. This is the
83 -- case for the path of a name in the Unrestricted state.
86 -- The path can only be accessed for writing. This is the case for
87 -- the path of a name in the Moved state.
90 subtype Perm_Kind is Perm_Kind_Option range No_Access .. Write_Only;
91 subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write;
92 subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only;
94 type Perm_Tree_Wrapper;
96 type Perm_Tree_Access is access Perm_Tree_Wrapper;
97 -- A tree of permissions is defined, where the root is a whole object
98 -- and tree branches follow access paths in memory. As Perm_Tree is a
99 -- discriminated record, a wrapper type is used for the access type
100 -- designating a subtree, to make it unconstrained so that it can be
103 -- Nodes in the permission tree are of different kinds
106 (Entire_Object, -- Scalar object, or folded object of any type
107 Reference, -- Unfolded object of access type
108 Array_Component, -- Unfolded object of array type
109 Record_Component -- Unfolded object of record type
112 package Perm_Tree_Maps is new Simple_HTable
113 (Header_Num => Elaboration_Context_Index,
115 Element => Perm_Tree_Access,
117 Hash => Elaboration_Context_Hash,
119 -- The instantation of a hash table, with keys being entities and values
120 -- being pointers to permission trees. This is used to define global
121 -- environment permissions (entities in that case are stand-alone
122 -- objects or formal parameters), as well as the permissions for the
123 -- extensions of a Record_Component node (entities in that case are
124 -- record components).
126 -- The definition of permission trees. This is a tree, which has a
127 -- permission at each node, and depending on the type of the node, can
128 -- have zero, one, or more children reached through an access to tree.
130 type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
131 Permission : Perm_Kind;
132 -- Permission at this level in the path
134 Is_Node_Deep : Boolean;
135 -- Whether this node is of a "deep" type, i.e. an access type or a
136 -- composite type containing access type subcomponents. This
137 -- corresponds to both "observing" and "owning" types in SPARK RM
138 -- 3.10. To be used when moving the path.
140 Explanation : Node_Id;
141 -- Node that can be used in an explanation for a permission mismatch
144 -- An entire object is either a leaf (an object which cannot be
145 -- extended further in a path) or a subtree in folded form (which
146 -- could later be unfolded further in another kind of node). The
147 -- field Children_Permission specifies a permission for every
148 -- extension of that node if that permission is different from the
149 -- node's permission.
151 when Entire_Object =>
152 Children_Permission : Perm_Kind;
154 -- Unfolded path of access type. The permission of the object
155 -- pointed to is given in Get_All.
158 Get_All : Perm_Tree_Access;
160 -- Unfolded path of array type. The permission of elements is
161 -- given in Get_Elem.
163 when Array_Component =>
164 Get_Elem : Perm_Tree_Access;
166 -- Unfolded path of record type. The permission of the components
167 -- is given in Component.
169 when Record_Component =>
170 Component : Perm_Tree_Maps.Instance;
174 type Perm_Tree_Wrapper is record
177 -- We use this wrapper in order to have unconstrained discriminants
179 type Perm_Env is new Perm_Tree_Maps.Instance;
180 -- The definition of a permission environment for the analysis. This is
181 -- just a hash table from entities to permission trees.
183 type Perm_Env_Access is access Perm_Env;
184 -- Access to permission environments
186 package Env_Maps is new Simple_HTable
187 (Header_Num => Elaboration_Context_Index,
189 Element => Perm_Env_Access,
191 Hash => Elaboration_Context_Hash,
193 -- The instantiation of a hash table whose elements are permission
194 -- environments. This hash table is used to save the environments at
195 -- the entry of each loop, with the key being the loop label.
197 type Env_Backups is new Env_Maps.Instance;
198 -- The type defining the hash table saving the environments at the entry
201 package Variable_Maps is new Simple_HTable
202 (Header_Num => Elaboration_Context_Index,
206 Hash => Elaboration_Context_Hash,
209 type Variable_Mapping is new Variable_Maps.Instance;
210 -- Mapping from variables to nodes denoting paths that are observed or
211 -- borrowed by the variable.
217 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course,
218 -- that's only for the top access, as otherwise this reverses the order
219 -- in accesses visually.
221 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind;
222 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance;
223 function Explanation (T : Perm_Tree_Access) return Node_Id;
224 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access;
225 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access;
226 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean;
227 function Kind (T : Perm_Tree_Access) return Path_Kind;
228 function Permission (T : Perm_Tree_Access) return Perm_Kind;
230 -----------------------
231 -- Memory Management --
232 -----------------------
236 To : in out Perm_Env);
237 -- Procedure to copy a permission environment
239 procedure Move_Env (From, To : in out Perm_Env);
240 -- Procedure to move a permission environment. It frees To, moves From
241 -- in To and sets From to Nil.
243 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping);
244 -- Move a variable mapping, freeing memory as needed and resetting the
247 procedure Copy_Tree (From, To : Perm_Tree_Access);
248 -- Procedure to copy a permission tree
250 procedure Free_Env (PE : in out Perm_Env);
251 -- Procedure to free a permission environment
253 procedure Free_Tree (PT : in out Perm_Tree_Access);
254 -- Procedure to free a permission tree
260 procedure Perm_Mismatch
262 Exp_Perm : Perm_Kind;
263 Act_Perm : Perm_Kind;
265 Forbidden_Perm : Boolean := False);
266 -- Issues a continuation error message about a mismatch between a
267 -- desired permission Exp_Perm and a permission obtained Act_Perm. N
268 -- is the node on which the error is reported.
272 package body Permissions is
274 -------------------------
275 -- Children_Permission --
276 -------------------------
278 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
280 return T.all.Tree.Children_Permission;
281 end Children_Permission;
287 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance
290 return T.all.Tree.Component;
297 procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is
298 Comp_From : Perm_Tree_Access;
299 Key_From : Perm_Tree_Maps.Key_Option;
300 Son : Perm_Tree_Access;
304 Key_From := Get_First_Key (From);
305 while Key_From.Present loop
306 Comp_From := Get (From, Key_From.K);
307 pragma Assert (Comp_From /= null);
309 Son := new Perm_Tree_Wrapper;
310 Copy_Tree (Comp_From, Son);
312 Set (To, Key_From.K, Son);
313 Key_From := Get_Next_Key (From);
321 procedure Copy_Tree (From, To : Perm_Tree_Access) is
323 -- Copy the direct components of the tree
327 -- Now reallocate access components for a deep copy of the tree
330 when Entire_Object =>
334 To.all.Tree.Get_All := new Perm_Tree_Wrapper;
335 Copy_Tree (Get_All (From), Get_All (To));
337 when Array_Component =>
338 To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
339 Copy_Tree (Get_Elem (From), Get_Elem (To));
341 when Record_Component =>
343 Comp_From : Perm_Tree_Access;
344 Key_From : Perm_Tree_Maps.Key_Option;
345 Son : Perm_Tree_Access;
346 Hash_Table : Perm_Tree_Maps.Instance;
348 -- We put a new hash table, so that it gets dealiased from
349 -- the Component (From) hash table.
350 To.all.Tree.Component := Hash_Table;
351 Key_From := Perm_Tree_Maps.Get_First_Key
354 while Key_From.Present loop
355 Comp_From := Perm_Tree_Maps.Get
356 (Component (From), Key_From.K);
357 pragma Assert (Comp_From /= null);
358 Son := new Perm_Tree_Wrapper;
359 Copy_Tree (Comp_From, Son);
361 (To.all.Tree.Component, Key_From.K, Son);
362 Key_From := Perm_Tree_Maps.Get_Next_Key
369 ------------------------------
370 -- Elaboration_Context_Hash --
371 ------------------------------
373 function Elaboration_Context_Hash
374 (Key : Entity_Id) return Elaboration_Context_Index
377 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
378 end Elaboration_Context_Hash;
384 procedure Free_Env (PE : in out Perm_Env) is
385 CompO : Perm_Tree_Access;
387 CompO := Get_First (PE);
388 while CompO /= null loop
390 CompO := Get_Next (PE);
400 procedure Free_Tree (PT : in out Perm_Tree_Access) is
401 procedure Free_Perm_Tree_Dealloc is
402 new Ada.Unchecked_Deallocation
403 (Perm_Tree_Wrapper, Perm_Tree_Access);
404 -- The deallocator for permission_trees
408 when Entire_Object =>
412 Free_Tree (PT.all.Tree.Get_All);
414 when Array_Component =>
415 Free_Tree (PT.all.Tree.Get_Elem);
417 when Record_Component =>
419 Comp : Perm_Tree_Access;
422 Comp := Perm_Tree_Maps.Get_First (Component (PT));
423 while Comp /= null loop
425 -- Free every Component subtree
428 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
433 Free_Perm_Tree_Dealloc (PT);
440 function Explanation (T : Perm_Tree_Access) return Node_Id is
442 return T.all.Tree.Explanation;
449 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
451 return T.all.Tree.Get_All;
458 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
460 return T.all.Tree.Get_Elem;
467 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
469 return T.all.Tree.Is_Node_Deep;
476 function Kind (T : Perm_Tree_Access) return Path_Kind is
478 return T.all.Tree.Kind;
485 procedure Move_Env (From, To : in out Perm_Env) is
489 From := Perm_Env (Perm_Tree_Maps.Nil);
492 ---------------------------
493 -- Move_Variable_Mapping --
494 ---------------------------
496 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping) is
500 From := Variable_Mapping (Variable_Maps.Nil);
501 end Move_Variable_Mapping;
507 function Permission (T : Perm_Tree_Access) return Perm_Kind is
509 return T.all.Tree.Permission;
516 procedure Perm_Mismatch
518 Exp_Perm : Perm_Kind;
519 Act_Perm : Perm_Kind;
521 Forbidden_Perm : Boolean := False)
524 Error_Msg_Sloc := Sloc (Expl);
526 if Forbidden_Perm then
527 if Exp_Perm = No_Access then
528 Error_Msg_N ("\object was moved #", N);
535 if Act_Perm = Read_Only then
537 ("\object was declared as not writeable #", N);
539 Error_Msg_N ("\object was moved #", N);
543 Error_Msg_N ("\object was moved #", N);
555 --------------------------------------
556 -- Analysis modes for AST traversal --
557 --------------------------------------
559 -- The different modes for analysis. This allows checking whether a path
560 -- has the right permission, and also updating permissions when a path is
561 -- moved, borrowed, or observed.
563 type Extended_Checking_Mode is
566 -- Special value used for assignment, to check that subexpressions of
567 -- the assigned path are readable.
573 -- Move semantics. Checks that paths have Read_Write permission. After
574 -- moving a path, its permission and the permission of its prefixes are
575 -- set to Write_Only, while the permission of its extensions is set to
579 -- Used for the target of an assignment, or an actual parameter with
580 -- mode OUT. Checks that paths have Write_Perm permission. After
581 -- assigning to a path, its permission and the permission of its
582 -- extensions are set to Read_Write. The permission of its prefixes may
583 -- be normalized from Write_Only to Read_Write depending on other
584 -- permissions in the tree (a prefix gets permission Read_Write when all
585 -- its extensions become Read_Write).
588 -- Borrow semantics. Checks that paths have Read_Write permission. After
589 -- borrowing a path, its permission and the permission of its prefixes
590 -- and extensions are set to No_Access.
593 -- Observe semantics. Checks that paths have Read_Perm permission. After
594 -- observing a path, its permission and the permission of its prefixes
595 -- and extensions are set to Read_Only.
598 subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe;
600 type Result_Kind is (Folded, Unfolded);
601 -- The type declaration to discriminate in the Perm_Or_Tree type
603 -- The result type of the function Get_Perm_Or_Tree. This returns either a
604 -- tree when it found the appropriate tree, or a permission when the search
605 -- finds a leaf and the subtree we are looking for is folded. In the last
606 -- case, we return instead the Children_Permission field of the leaf.
608 type Perm_Or_Tree (R : Result_Kind) is record
611 Found_Permission : Perm_Kind;
612 Explanation : Node_Id;
614 Tree_Access : Perm_Tree_Access;
618 type Error_Status is (OK, Error);
620 -----------------------
621 -- Local subprograms --
622 -----------------------
624 function "<=" (P1, P2 : Perm_Kind) return Boolean;
625 function ">=" (P1, P2 : Perm_Kind) return Boolean;
626 function Glb (P1, P2 : Perm_Kind) return Perm_Kind;
627 function Lub (P1, P2 : Perm_Kind) return Perm_Kind;
629 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id);
630 -- Handle assignment as part of an assignment statement or an object
633 procedure Check_Call_Statement (Call : Node_Id);
635 procedure Check_Callable_Body (Body_N : Node_Id);
636 -- Entry point for the analysis of a subprogram or entry body
638 procedure Check_Declaration (Decl : Node_Id);
640 procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
641 pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
643 N_Subtype_Indication,
646 or else Nkind (Expr) in N_Subexpr);
648 procedure Check_Globals (Subp : Entity_Id);
649 -- This procedure takes a subprogram called and checks the permission of
652 -- Checking proceduress for safe pointer usage. These procedures traverse
653 -- the AST, check nodes for correct permissions according to SPARK RM 3.10,
654 -- and update permissions depending on the node kind. The main procedure
655 -- Check_Node is mutually recursive with the specialized procedures that
658 procedure Check_List (L : List_Id);
659 -- Calls Check_Node on each element of the list
661 procedure Check_Loop_Statement (Stmt : Node_Id);
663 procedure Check_Node (N : Node_Id);
664 -- Main traversal procedure to check safe pointer usage
666 procedure Check_Package_Body (Pack : Node_Id);
668 procedure Check_Package_Spec (Pack : Node_Id);
670 procedure Check_Parameter_Or_Global
675 Global_Var : Boolean);
676 -- Check the permission of every actual parameter or global
678 procedure Check_Pragma (Prag : Node_Id);
680 procedure Check_Source_Of_Borrow_Or_Observe
682 Status : out Error_Status);
684 procedure Check_Statement (Stmt : Node_Id);
686 procedure Check_Type (Typ : Entity_Id);
687 -- Check that type Typ is either not deep, or that it is an observing or
688 -- owning type according to SPARK RM 3.10
690 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id;
691 -- The function that takes a name as input and returns an explanation node
692 -- for the permission associated with it.
694 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
695 pragma Precondition (Is_Path_Expression (Expr));
696 -- Return the expression being borrowed/observed when borrowing or
697 -- observing Expr. If Expr is a call to a traversal function, this is
698 -- the first actual, otherwise it is Expr.
700 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
701 -- The function that takes a name as input and returns a permission
702 -- associated with it.
704 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
705 pragma Precondition (Is_Path_Expression (N));
706 -- This function gets a node and looks recursively to find the appropriate
707 -- subtree for that node. If the tree is folded on that node, then it
708 -- returns the permission given at the right level.
710 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
711 pragma Precondition (Is_Path_Expression (N));
712 -- This function gets a node and looks recursively to find the appropriate
713 -- subtree for that node. If the tree is folded, then it unrolls the tree
714 -- up to the appropriate level.
716 function Get_Root_Object
718 Through_Traversal : Boolean := True;
719 Is_Traversal : Boolean := False) return Entity_Id;
720 -- Return the root of the path expression Expr, or Empty for an allocator,
721 -- NULL, or a function call. Through_Traversal is True if it should follow
722 -- through calls to traversal functions. Is_Traversal is True if this
723 -- corresponds to a value returned from a traversal function, which should
724 -- allow if-expressions and case-expressions that refer to the same root,
725 -- even if the paths are not the same in all branches.
728 with procedure Handle_Parameter_Or_Global
730 Formal_Typ : Entity_Id;
731 Param_Mode : Formal_Kind;
733 Global_Var : Boolean);
734 procedure Handle_Globals (Subp : Entity_Id);
735 -- Handling of globals is factored in a generic instantiated below
737 function Has_Array_Component (Expr : Node_Id) return Boolean;
738 pragma Precondition (Is_Path_Expression (Expr));
739 -- This function gets a node and looks recursively to determine whether the
740 -- given path has any array component.
742 procedure Hp (P : Perm_Env);
743 -- A procedure that outputs the hash table. This function is used only in
744 -- the debugger to look into a hash table.
745 pragma Unreferenced (Hp);
747 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id);
748 pragma No_Return (Illegal_Global_Usage);
749 -- A procedure that is called when deep globals or aliased globals are used
750 -- without any global aspect.
752 function Is_Path_Expression
754 Is_Traversal : Boolean := False) return Boolean;
755 -- Return whether Expr corresponds to a path. Is_Traversal is True if this
756 -- corresponds to a value returned from a traversal function, which should
757 -- allow if-expressions and case-expressions.
759 function Is_Subpath_Expression
761 Is_Traversal : Boolean := False) return Boolean;
762 -- Return True if Expr can be part of a path expression. Is_Traversal is
763 -- True if this corresponds to a value returned from a traversal function,
764 -- which should allow if-expressions and case-expressions.
766 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
767 -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
768 -- a prefix, in the sense that they could still refer to overlapping memory
771 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean;
773 function Loop_Of_Exit (N : Node_Id) return Entity_Id;
774 -- A function that takes an exit statement node and returns the entity of
775 -- the loop that this statement is exiting from.
777 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env);
778 -- Merge Target and Source into Target, and then deallocate the Source
783 Found_Perm : Perm_Kind;
785 Forbidden_Perm : Boolean := False);
786 -- A procedure that is called when the permissions found contradict the
787 -- rules established by the RM. This function is called with the node and
788 -- the permission that was expected, and issues an error message with the
789 -- appropriate values.
791 procedure Perm_Error_Subprogram_End
795 Found_Perm : Perm_Kind;
797 -- A procedure that is called when the permissions found contradict the
798 -- rules established by the RM at the end of subprograms. This function is
799 -- called with the node, the node of the returning function, and the
800 -- permission that was expected, and adds an error message with the
801 -- appropriate values.
803 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode);
804 pragma Precondition (Is_Path_Expression (Expr));
805 -- Check correct permission for the path in the checking mode Mode, and
806 -- update permissions of the path and its prefixes/extensions.
808 procedure Return_Globals (Subp : Entity_Id);
809 -- Takes a subprogram as input, and checks that all borrowed global items
810 -- of the subprogram indeed have Read_Write permission at the end of the
811 -- subprogram execution.
813 procedure Return_Parameter_Or_Global
818 Global_Var : Boolean);
819 -- Auxiliary procedure to Return_Parameters and Return_Globals
821 procedure Return_Parameters (Subp : Entity_Id);
822 -- Takes a subprogram as input, and checks that all out parameters of the
823 -- subprogram indeed have Read_Write permission at the end of the
824 -- subprogram execution.
826 procedure Set_Perm_Extensions
827 (T : Perm_Tree_Access;
830 -- This procedure takes an access to a permission tree and modifies the
831 -- tree so that any strict extensions of the given tree become of the
832 -- access specified by parameter P.
834 procedure Set_Perm_Extensions_Move
835 (T : Perm_Tree_Access;
838 -- Set permissions to
839 -- No for any extension with more .all
840 -- W for any deep extension with same number of .all
841 -- RW for any shallow extension with same number of .all
843 function Set_Perm_Prefixes
845 Perm : Perm_Kind_Option;
846 Expl : Node_Id) return Perm_Tree_Access;
847 pragma Precondition (Is_Path_Expression (N));
848 -- This function modifies the permissions of a given node in the permission
849 -- environment as well as all the prefixes of the path, to the new
850 -- permission Perm. The general rule here is that everybody updates the
851 -- permission of the subtree they are returning.
853 procedure Set_Perm_Prefixes_Assign (N : Node_Id);
854 pragma Precondition (Is_Path_Expression (N));
855 -- This procedure takes a name as an input and sets in the permission
856 -- tree the given permission to the given name. The general rule here is
857 -- that everybody updates the permission of the subtree it is returning.
858 -- The permission of the assigned path has been set to RW by the caller.
860 -- Case where we have to normalize a tree after the correct permissions
861 -- have been assigned already. We look for the right subtree at the given
862 -- path, actualize its permissions, and then call the normalization on its
865 -- Example: We assign x.y and x.z, and then Set_Perm_Prefixes_Assign will
866 -- change the permission of x to RW because all of its components have
869 procedure Setup_Globals (Subp : Entity_Id);
870 -- Takes a subprogram as input, and sets up the environment by adding
871 -- global items with appropriate permissions.
873 procedure Setup_Parameter_Or_Global
878 Global_Var : Boolean;
880 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
882 procedure Setup_Parameters (Subp : Entity_Id);
883 -- Takes a subprogram as input, and sets up the environment by adding
884 -- formal parameters with appropriate permissions.
886 procedure Setup_Protected_Components (Subp : Entity_Id);
887 -- Takes a protected operation as input, and sets up the environment by
888 -- adding protected components with appropriate permissions.
890 ----------------------
891 -- Global Variables --
892 ----------------------
894 Current_Perm_Env : Perm_Env;
895 -- The permission environment that is used for the analysis. This
896 -- environment can be saved, modified, reinitialized, but should be the
897 -- only one valid from which to extract the permissions of the paths in
898 -- scope. The analysis ensures at each point that this variables contains
899 -- a valid permission environment with all bindings in scope.
901 Inside_Procedure_Call : Boolean := False;
902 -- Set while checking the actual parameters of a procedure or entry call
904 Inside_Elaboration : Boolean := False;
905 -- Set during package spec/body elaboration, during which move and local
906 -- observe/borrow are not allowed. As a result, no other checking is needed
907 -- during elaboration.
909 Current_Loops_Envs : Env_Backups;
910 -- This variable contains saves of permission environments at each loop the
911 -- analysis entered. Each saved environment can be reached with the label
914 Current_Loops_Accumulators : Env_Backups;
915 -- This variable contains the environments used as accumulators for loops,
916 -- that consist of the merge of all environments at each exit point of
917 -- the loop (which can also be the entry point of the loop in the case of
918 -- non-infinite loops), each of them reachable from the label of the loop.
919 -- We require that the environment stored in the accumulator be less
920 -- restrictive than the saved environment at the beginning of the loop, and
921 -- the permission environment after the loop is equal to the accumulator.
923 Current_Borrowers : Variable_Mapping;
924 -- Mapping from borrowers to the path borrowed
926 Current_Observers : Variable_Mapping;
927 -- Mapping from observers to the path observed
933 -- Generic procedure is defined first so that instantiations can be defined
934 -- anywhere afterwards.
936 procedure Handle_Globals (Subp : Entity_Id) is
940 procedure Handle_Globals_From_List
941 (First_Item : Node_Id;
943 -- Handle global items from the list starting at Item
945 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id);
946 -- Handle global items for the mode Global_Mode
948 ------------------------------
949 -- Handle_Globals_From_List --
950 ------------------------------
952 procedure Handle_Globals_From_List
953 (First_Item : Node_Id;
956 Item : Node_Id := First_Item;
960 while Present (Item) loop
963 -- Ignore abstract states, which play no role in pointer aliasing
965 if Ekind (E) = E_Abstract_State then
968 Handle_Parameter_Or_Global (Expr => Item,
969 Formal_Typ => Retysp (Etype (Item)),
977 end Handle_Globals_From_List;
979 ----------------------------
980 -- Handle_Globals_Of_Mode --
981 ----------------------------
983 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id) is
991 Kind := E_In_Parameter;
994 Kind := E_Out_Parameter;
997 Kind := E_In_Out_Parameter;
1000 raise Program_Error;
1003 -- Check both global items from Global and Refined_Global pragmas
1005 Handle_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
1006 Handle_Globals_From_List
1007 (First_Global (Subp, Global_Mode, Refined => True), Kind);
1008 end Handle_Globals_Of_Mode;
1010 -- Start of processing for Handle_Globals
1013 Handle_Globals_Of_Mode (Name_Proof_In);
1014 Handle_Globals_Of_Mode (Name_Input);
1015 Handle_Globals_Of_Mode (Name_Output);
1016 Handle_Globals_Of_Mode (Name_In_Out);
1023 function "<=" (P1, P2 : Perm_Kind) return Boolean is
1032 function ">=" (P1, P2 : Perm_Kind) return Boolean is
1035 when No_Access => return True;
1036 when Read_Only => return P1 in Read_Perm;
1037 when Write_Only => return P1 in Write_Perm;
1038 when Read_Write => return P1 = Read_Write;
1042 ----------------------
1043 -- Check_Assignment --
1044 ----------------------
1046 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is
1048 -- Local subprograms
1050 procedure Handle_Borrow
1054 -- Update map of current borrowers
1056 procedure Handle_Observe
1060 -- Update map of current observers
1066 procedure Handle_Borrow
1071 Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1074 -- SPARK RM 3.10(8): If the type of the target is an anonymous
1075 -- access-to-variable type (an owning access type), the source shall
1076 -- be an owning access object [..] whose root object is the target
1079 -- ??? In fact we could be slightly more permissive in allowing even
1080 -- a call to a traversal function of the right form.
1083 and then (Is_Traversal_Function_Call (Expr)
1084 or else Get_Root_Object (Borrowed) /= Var)
1086 if Emit_Messages then
1088 ("source of assignment must have & as root" &
1089 " (SPARK RM 3.10(8)))",
1095 Set (Current_Borrowers, Var, Borrowed);
1098 --------------------
1099 -- Handle_Observe --
1100 --------------------
1102 procedure Handle_Observe
1107 Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1110 -- ??? We are currently using the same restriction for observers
1111 -- as for borrowers. To be seen if the SPARK RM current rule really
1112 -- allows more uses.
1115 and then (Is_Traversal_Function_Call (Expr)
1116 or else Get_Root_Object (Observed) /= Var)
1118 if Emit_Messages then
1120 ("source of assignment must have & as root" &
1121 " (SPARK RM 3.10(8)))",
1127 Set (Current_Observers, Var, Observed);
1132 Target_Typ : constant Node_Id := Etype (Target);
1133 Is_Decl : constant Boolean := Nkind (Target) = N_Defining_Identifier;
1134 Target_Root : Entity_Id;
1135 Expr_Root : Entity_Id;
1137 Status : Error_Status;
1139 -- Start of processing for Check_Assignment
1142 Check_Type (Target_Typ);
1144 if Is_Anonymous_Access_Type (Target_Typ) then
1145 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
1147 if Status /= OK then
1152 Target_Root := Target;
1154 Target_Root := Get_Root_Object (Target);
1157 Expr_Root := Get_Root_Object (Expr);
1159 -- SPARK RM 3.10(8): For an assignment statement where
1160 -- the target is a stand-alone object of an anonymous
1161 -- access-to-object type
1163 pragma Assert (Present (Target_Root));
1165 -- If the type of the target is an anonymous
1166 -- access-to-constant type (an observing access type), the
1167 -- source shall be an owning access object denoted by a name
1168 -- that is not in the Moved state, and whose root object
1169 -- is not in the Moved state and is not declared at a
1170 -- statically deeper accessibility level than that of
1171 -- the target object.
1173 if Is_Access_Constant (Target_Typ) then
1174 Perm := Get_Perm (Expr);
1176 if Perm = No_Access then
1177 Perm_Error (Expr, No_Access, No_Access,
1178 Expl => Get_Expl (Expr),
1179 Forbidden_Perm => True);
1183 Perm := Get_Perm (Expr_Root);
1185 if Perm = No_Access then
1186 Perm_Error (Expr, No_Access, No_Access,
1187 Expl => Get_Expl (Expr_Root),
1188 Forbidden_Perm => True);
1192 -- ??? check accessibility level
1194 -- If the type of the target is an anonymous
1195 -- access-to-variable type (an owning access type), the
1196 -- source shall be an owning access object denoted by a
1197 -- name that is in the Unrestricted state, and whose root
1198 -- object is the target object itself.
1200 Check_Expression (Expr, Observe);
1201 Handle_Observe (Target_Root, Expr, Is_Decl);
1204 Perm := Get_Perm (Expr);
1206 if Perm /= Read_Write then
1207 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
1212 if not Is_Entity_Name (Target) then
1213 if Emit_Messages then
1215 ("target of borrow must be stand-alone variable",
1220 elsif Target_Root /= Expr_Root then
1221 if Emit_Messages then
1223 ("source of borrow must be variable &",
1230 Check_Expression (Expr, Borrow);
1231 Handle_Borrow (Target_Root, Expr, Is_Decl);
1234 elsif Is_Deep (Target_Typ) then
1236 if Is_Path_Expression (Expr) then
1237 Check_Expression (Expr, Move);
1240 if Emit_Messages then
1241 Error_Msg_N ("expression not allowed as source of move", Expr);
1247 Check_Expression (Expr, Read);
1249 end Check_Assignment;
1251 --------------------------
1252 -- Check_Call_Statement --
1253 --------------------------
1255 procedure Check_Call_Statement (Call : Node_Id) is
1257 Subp : constant Entity_Id := Get_Called_Entity (Call);
1259 -- Local subprograms
1261 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
1262 -- Check the permission of every actual parameter
1264 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id);
1265 -- Update the permission of OUT actual parameters
1271 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
1273 Check_Parameter_Or_Global
1275 Typ => Retysp (Etype (Formal)),
1276 Kind => Ekind (Formal),
1278 Global_Var => False);
1285 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is
1286 Mode : constant Entity_Kind := Ekind (Formal);
1289 case Formal_Kind'(Mode) is
1290 when E_Out_Parameter =>
1291 Check_Expression (Actual, Assign);
1298 procedure Check_Params is new
1299 Iterate_Call_Parameters (Check_Param);
1301 procedure Update_Params is new
1302 Iterate_Call_Parameters (Update_Param);
1304 -- Start of processing for Check_Call_Statement
1307 Inside_Procedure_Call := True;
1308 Check_Params (Call);
1309 if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then
1310 if Emit_Messages then
1312 ("call through access to subprogram is not allowed in SPARK",
1316 Check_Globals (Get_Called_Entity (Call));
1319 Inside_Procedure_Call := False;
1320 Update_Params (Call);
1321 end Check_Call_Statement;
1323 -------------------------
1324 -- Check_Callable_Body --
1325 -------------------------
1327 procedure Check_Callable_Body (Body_N : Node_Id) is
1328 Save_In_Elab : constant Boolean := Inside_Elaboration;
1329 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
1330 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
1331 Prag : constant Node_Id := SPARK_Pragma (Body_Id);
1333 Saved_Env : Perm_Env;
1334 Saved_Borrowers : Variable_Mapping;
1335 Saved_Observers : Variable_Mapping;
1338 -- Only SPARK bodies are analyzed
1341 or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On
1346 Inside_Elaboration := False;
1348 if Ekind (Spec_Id) = E_Function
1349 and then Is_Anonymous_Access_Type (Etype (Spec_Id))
1350 and then not Is_Traversal_Function (Spec_Id)
1352 if Emit_Messages then
1353 Error_Msg_N ("anonymous access type for result only allowed for "
1354 & "traversal functions", Spec_Id);
1359 -- Save environment and put a new one in place
1361 Move_Env (Current_Perm_Env, Saved_Env);
1362 Move_Variable_Mapping (Current_Borrowers, Saved_Borrowers);
1363 Move_Variable_Mapping (Current_Observers, Saved_Observers);
1365 -- Add formals and globals to the environment with adequate permissions
1367 if Is_Subprogram_Or_Entry (Spec_Id) then
1368 Setup_Parameters (Spec_Id);
1369 Setup_Globals (Spec_Id);
1372 -- For protected operations, add protected components to the environment
1373 -- with adequate permissions.
1375 if Is_Protected_Operation (Spec_Id) then
1376 Setup_Protected_Components (Spec_Id);
1379 -- Analyze the body of the subprogram
1381 Check_List (Declarations (Body_N));
1382 Check_Node (Handled_Statement_Sequence (Body_N));
1384 -- Check the read-write permissions of borrowed parameters/globals
1386 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
1387 and then not No_Return (Spec_Id)
1389 Return_Parameters (Spec_Id);
1390 Return_Globals (Spec_Id);
1393 -- Restore the saved environment and free the current one
1395 Move_Env (Saved_Env, Current_Perm_Env);
1396 Move_Variable_Mapping (Saved_Borrowers, Current_Borrowers);
1397 Move_Variable_Mapping (Saved_Observers, Current_Observers);
1399 Inside_Elaboration := Save_In_Elab;
1400 end Check_Callable_Body;
1402 -----------------------
1403 -- Check_Declaration --
1404 -----------------------
1406 procedure Check_Declaration (Decl : Node_Id) is
1407 Target : constant Entity_Id := Defining_Identifier (Decl);
1408 Target_Typ : constant Node_Id := Etype (Target);
1412 case N_Declaration'(Nkind (Decl)) is
1413 when N_Full_Type_Declaration =>
1414 Check_Type (Target);
1416 -- ??? What about component declarations with defaults.
1418 when N_Subtype_Declaration =>
1419 Check_Expression (Subtype_Indication (Decl), Read);
1421 when N_Object_Declaration =>
1422 Expr := Expression (Decl);
1424 Check_Type (Target_Typ);
1426 -- A declaration of a stand-alone object of an anonymous access
1427 -- type shall have an explicit initial value and shall occur
1428 -- immediately within a subprogram body, an entry body, or a
1429 -- block statement (SPARK RM 3.10(4)).
1431 if Is_Anonymous_Access_Type (Target_Typ) then
1433 Scop : constant Entity_Id := Scope (Target);
1435 if not Is_Local_Context (Scop) then
1436 if Emit_Messages then
1438 ("object of anonymous access type must be declared "
1439 & "immediately within a subprogram, entry or block "
1440 & "(SPARK RM 3.10(4))", Decl);
1446 if Emit_Messages then
1447 Error_Msg_N ("object of anonymous access type must be "
1448 & "initialized (SPARK RM 3.10(4))", Decl);
1453 if Present (Expr) then
1454 Check_Assignment (Target => Target,
1458 if Is_Deep (Target_Typ) then
1460 Tree : constant Perm_Tree_Access :=
1461 new Perm_Tree_Wrapper'
1463 (Kind => Entire_Object,
1464 Is_Node_Deep => True,
1465 Explanation => Decl,
1466 Permission => Read_Write,
1467 Children_Permission => Read_Write));
1469 Set (Current_Perm_Env, Target, Tree);
1473 when N_Iterator_Specification =>
1476 when N_Loop_Parameter_Specification =>
1479 -- Checking should not be called directly on these nodes
1481 when N_Function_Specification
1482 | N_Entry_Declaration
1483 | N_Procedure_Specification
1484 | N_Component_Declaration
1486 raise Program_Error;
1488 -- Ignored constructs for pointer checking
1490 when N_Formal_Object_Declaration
1491 | N_Formal_Type_Declaration
1492 | N_Incomplete_Type_Declaration
1493 | N_Private_Extension_Declaration
1494 | N_Private_Type_Declaration
1495 | N_Protected_Type_Declaration
1499 -- The following nodes are rewritten by semantic analysis
1501 when N_Expression_Function =>
1502 raise Program_Error;
1504 end Check_Declaration;
1506 ----------------------
1507 -- Check_Expression --
1508 ----------------------
1510 procedure Check_Expression
1512 Mode : Extended_Checking_Mode)
1514 -- Local subprograms
1516 function Is_Type_Name (Expr : Node_Id) return Boolean;
1517 -- Detect when a path expression is in fact a type name
1519 procedure Move_Expression (Expr : Node_Id);
1520 -- Some subexpressions are only analyzed in Move mode. This is a
1521 -- specialized version of Check_Expression for that case.
1523 procedure Move_Expression_List (L : List_Id);
1524 -- Call Move_Expression on every expression in the list L
1526 procedure Read_Expression (Expr : Node_Id);
1527 -- Most subexpressions are only analyzed in Read mode. This is a
1528 -- specialized version of Check_Expression for that case.
1530 procedure Read_Expression_List (L : List_Id);
1531 -- Call Read_Expression on every expression in the list L
1533 procedure Read_Indexes (Expr : Node_Id);
1534 -- When processing a path, the index expressions and function call
1535 -- arguments occurring on the path should be analyzed in Read mode.
1541 function Is_Type_Name (Expr : Node_Id) return Boolean is
1543 return Nkind_In (Expr, N_Expanded_Name, N_Identifier)
1544 and then Is_Type (Entity (Expr));
1547 ---------------------
1548 -- Move_Expression --
1549 ---------------------
1551 -- Distinguish the case where the argument is a path expression that
1552 -- needs explicit moving.
1554 procedure Move_Expression (Expr : Node_Id) is
1556 if Is_Path_Expression (Expr) then
1557 Check_Expression (Expr, Move);
1559 Read_Expression (Expr);
1561 end Move_Expression;
1563 --------------------------
1564 -- Move_Expression_List --
1565 --------------------------
1567 procedure Move_Expression_List (L : List_Id) is
1571 while Present (N) loop
1572 Move_Expression (N);
1575 end Move_Expression_List;
1577 ---------------------
1578 -- Read_Expression --
1579 ---------------------
1581 procedure Read_Expression (Expr : Node_Id) is
1583 Check_Expression (Expr, Read);
1584 end Read_Expression;
1586 --------------------------
1587 -- Read_Expression_List --
1588 --------------------------
1590 procedure Read_Expression_List (L : List_Id) is
1594 while Present (N) loop
1595 Read_Expression (N);
1598 end Read_Expression_List;
1604 procedure Read_Indexes (Expr : Node_Id) is
1606 -- Local subprograms
1608 function Is_Singleton_Choice (Choices : List_Id) return Boolean;
1609 -- Return whether Choices is a singleton choice
1611 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id);
1612 -- Call Read_Expression on the actual
1614 -------------------------
1615 -- Is_Singleton_Choice --
1616 -------------------------
1618 function Is_Singleton_Choice (Choices : List_Id) return Boolean is
1619 Choice : constant Node_Id := First (Choices);
1621 return List_Length (Choices) = 1
1622 and then Nkind (Choice) /= N_Others_Choice
1623 and then not Nkind_In (Choice, N_Subtype_Indication, N_Range)
1625 (Nkind_In (Choice, N_Identifier, N_Expanded_Name)
1626 and then Is_Type (Entity (Choice)));
1627 end Is_Singleton_Choice;
1633 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id) is
1634 pragma Unreferenced (Formal);
1636 Read_Expression (Actual);
1639 procedure Read_Params is new Iterate_Call_Parameters (Read_Param);
1641 -- Start of processing for Read_Indexes
1644 if not Is_Subpath_Expression (Expr) then
1645 if Emit_Messages then
1647 ("name expected here for move/borrow/observe", Expr);
1652 case N_Subexpr'(Nkind (Expr)) is
1659 when N_Explicit_Dereference
1660 | N_Selected_Component
1662 Read_Indexes (Prefix (Expr));
1664 when N_Indexed_Component =>
1665 Read_Indexes (Prefix (Expr));
1666 Read_Expression_List (Expressions (Expr));
1669 Read_Indexes (Prefix (Expr));
1670 Read_Expression (Discrete_Range (Expr));
1672 -- The argument of an allocator is moved as part of the implicit
1676 Move_Expression (Expression (Expr));
1678 when N_Function_Call =>
1680 if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then
1681 if Emit_Messages then
1683 ("call through access to subprogram is not allowed in "
1687 Check_Globals (Get_Called_Entity (Expr));
1691 Read_Expression (Left_Opnd (Expr));
1692 Read_Expression (Right_Opnd (Expr));
1694 when N_Qualified_Expression
1696 | N_Unchecked_Type_Conversion
1698 Read_Indexes (Expression (Expr));
1702 Assocs : constant List_Id := Component_Associations (Expr);
1704 Assoc : Node_Id := Nlists.First (Assocs);
1708 -- The subexpressions of an aggregate are moved as part
1709 -- of the implicit assignments. Handle the positional
1710 -- components first.
1712 Move_Expression_List (Expressions (Expr));
1714 -- Handle the named components next
1716 while Present (Assoc) loop
1717 CL := Choices (Assoc);
1719 -- For an array aggregate, we should also check that the
1720 -- expressions used in choices are readable.
1722 if Is_Array_Type (Etype (Expr)) then
1723 Choice := Nlists.First (CL);
1724 while Present (Choice) loop
1725 if Nkind (Choice) /= N_Others_Choice then
1726 Read_Expression (Choice);
1732 -- There can be only one element for a value of deep type
1733 -- in order to avoid aliasing.
1735 if not Box_Present (Assoc)
1736 and then Is_Deep (Etype (Expression (Assoc)))
1737 and then not Is_Singleton_Choice (CL)
1738 and then Emit_Messages
1741 ("singleton choice required to prevent aliasing",
1745 -- The subexpressions of an aggregate are moved as part
1746 -- of the implicit assignments.
1748 if not Box_Present (Assoc) then
1749 Move_Expression (Expression (Assoc));
1756 when N_Extension_Aggregate =>
1758 Exprs : constant List_Id := Expressions (Expr);
1759 Assocs : constant List_Id := Component_Associations (Expr);
1761 Assoc : Node_Id := Nlists.First (Assocs);
1764 Move_Expression (Ancestor_Part (Expr));
1766 -- No positional components allowed at this stage
1768 if Present (Exprs) then
1769 raise Program_Error;
1772 while Present (Assoc) loop
1773 CL := Choices (Assoc);
1775 -- Only singleton components allowed at this stage
1777 if not Is_Singleton_Choice (CL) then
1778 raise Program_Error;
1781 -- The subexpressions of an aggregate are moved as part
1782 -- of the implicit assignments.
1784 if not Box_Present (Assoc) then
1785 Move_Expression (Expression (Assoc));
1792 when N_If_Expression =>
1794 Cond : constant Node_Id := First (Expressions (Expr));
1795 Then_Part : constant Node_Id := Next (Cond);
1796 Else_Part : constant Node_Id := Next (Then_Part);
1798 Read_Expression (Cond);
1799 Read_Indexes (Then_Part);
1800 Read_Indexes (Else_Part);
1803 when N_Case_Expression =>
1805 Cases : constant List_Id := Alternatives (Expr);
1806 Cur_Case : Node_Id := First (Cases);
1809 Read_Expression (Expression (Expr));
1811 while Present (Cur_Case) loop
1812 Read_Indexes (Expression (Cur_Case));
1817 when N_Attribute_Reference =>
1819 (Get_Attribute_Id (Attribute_Name (Expr)) =
1820 Attribute_Loop_Entry
1822 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1824 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image);
1826 Read_Expression (Prefix (Expr));
1828 if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1829 or else (Get_Attribute_Id (Attribute_Name (Expr)) =
1831 and then Is_Type_Name (Prefix (Expr)))
1833 Read_Expression_List (Expressions (Expr));
1837 raise Program_Error;
1841 -- Start of processing for Check_Expression
1844 if Is_Type_Name (Expr) then
1847 elsif Is_Path_Expression (Expr) then
1848 if Mode /= Assign then
1849 Read_Indexes (Expr);
1852 if Mode /= Read_Subexpr then
1853 Process_Path (Expr, Mode);
1859 -- Expressions that are not path expressions should only be analyzed in
1862 if Mode /= Read then
1863 if Emit_Messages then
1864 Error_Msg_N ("name expected here for move/borrow/observe", Expr);
1869 -- Special handling for nodes that may contain evaluated expressions in
1870 -- the form of constraints.
1872 case Nkind (Expr) is
1873 when N_Index_Or_Discriminant_Constraint =>
1875 Assn : Node_Id := First (Constraints (Expr));
1877 while Present (Assn) loop
1878 case Nkind (Assn) is
1879 when N_Discriminant_Association =>
1880 Read_Expression (Expression (Assn));
1883 Read_Expression (Assn);
1891 when N_Range_Constraint =>
1892 Read_Expression (Range_Expression (Expr));
1895 when N_Subtype_Indication =>
1896 if Present (Constraint (Expr)) then
1897 Read_Expression (Constraint (Expr));
1901 when N_Digits_Constraint =>
1902 Read_Expression (Digits_Expression (Expr));
1903 if Present (Range_Constraint (Expr)) then
1904 Read_Expression (Range_Constraint (Expr));
1908 when N_Delta_Constraint =>
1909 Read_Expression (Delta_Expression (Expr));
1910 if Present (Range_Constraint (Expr)) then
1911 Read_Expression (Range_Constraint (Expr));
1919 -- At this point Expr can only be a subexpression
1921 case N_Subexpr'(Nkind (Expr)) is
1926 Read_Expression (Left_Opnd (Expr));
1927 Read_Expression (Right_Opnd (Expr));
1929 when N_Membership_Test =>
1930 Read_Expression (Left_Opnd (Expr));
1931 if Present (Right_Opnd (Expr)) then
1932 Read_Expression (Right_Opnd (Expr));
1935 Cases : constant List_Id := Alternatives (Expr);
1936 Cur_Case : Node_Id := First (Cases);
1939 while Present (Cur_Case) loop
1940 Read_Expression (Cur_Case);
1947 Read_Expression (Right_Opnd (Expr));
1949 when N_Attribute_Reference =>
1951 Aname : constant Name_Id := Attribute_Name (Expr);
1952 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
1953 Pref : constant Node_Id := Prefix (Expr);
1954 Args : constant List_Id := Expressions (Expr);
1959 -- The following attributes take either no arguments, or
1960 -- arguments that do not refer to evaluated expressions
1961 -- (like Length or Loop_Entry), hence only the prefix
1962 -- needs to be read.
1964 when Attribute_Address
1965 | Attribute_Alignment
1966 | Attribute_Callable
1967 | Attribute_Component_Size
1968 | Attribute_Constrained
1970 | Attribute_First_Bit
1972 | Attribute_Last_Bit
1974 | Attribute_Loop_Entry
1975 | Attribute_Object_Size
1976 | Attribute_Position
1978 | Attribute_Terminated
1980 | Attribute_Value_Size
1982 Read_Expression (Pref);
1984 -- The following attributes take a type name as prefix,
1985 -- hence only the arguments need to be read.
1987 when Attribute_Ceiling
1994 | Attribute_Remainder
1995 | Attribute_Rounding
1997 | Attribute_Truncation
2001 Read_Expression_List (Args);
2003 -- Attributes Image and Img either take a type name as
2004 -- prefix with an expression in argument, or the expression
2005 -- directly as prefix. Adapt to each case.
2007 when Attribute_Image
2011 Read_Expression (Pref);
2013 Read_Expression_List (Args);
2016 -- Attribute Update takes expressions as both prefix and
2017 -- arguments, so both need to be read.
2019 when Attribute_Update =>
2020 Read_Expression (Pref);
2021 Read_Expression_List (Args);
2023 -- Attribute Modulus does not reference the evaluated
2024 -- expression, so it can be ignored for this analysis.
2026 when Attribute_Modulus =>
2029 -- The following attributes apply to types; there are no
2030 -- expressions to read.
2032 when Attribute_Class
2033 | Attribute_Storage_Size
2037 -- Postconditions should not be analyzed
2042 raise Program_Error;
2050 Read_Expression (Low_Bound (Expr));
2051 Read_Expression (High_Bound (Expr));
2053 when N_If_Expression =>
2054 Read_Expression_List (Expressions (Expr));
2056 when N_Case_Expression =>
2058 Cases : constant List_Id := Alternatives (Expr);
2059 Cur_Case : Node_Id := First (Cases);
2062 while Present (Cur_Case) loop
2063 Read_Expression (Expression (Cur_Case));
2067 Read_Expression (Expression (Expr));
2070 when N_Qualified_Expression
2072 | N_Unchecked_Type_Conversion
2074 Read_Expression (Expression (Expr));
2076 when N_Quantified_Expression =>
2078 For_In_Spec : constant Node_Id :=
2079 Loop_Parameter_Specification (Expr);
2080 For_Of_Spec : constant Node_Id :=
2081 Iterator_Specification (Expr);
2082 For_Of_Spec_Typ : Node_Id;
2085 if Present (For_In_Spec) then
2086 Read_Expression (Discrete_Subtype_Definition (For_In_Spec));
2088 Read_Expression (Name (For_Of_Spec));
2089 For_Of_Spec_Typ := Subtype_Indication (For_Of_Spec);
2090 if Present (For_Of_Spec_Typ) then
2091 Read_Expression (For_Of_Spec_Typ);
2095 Read_Expression (Condition (Expr));
2098 when N_Character_Literal
2099 | N_Numeric_Or_String_Literal
2101 | N_Raise_Expression
2106 when N_Delta_Aggregate
2111 -- Procedure calls are handled in Check_Node
2113 when N_Procedure_Call_Statement =>
2114 raise Program_Error;
2116 -- Path expressions are handled before this point
2121 | N_Explicit_Dereference
2122 | N_Extension_Aggregate
2125 | N_Indexed_Component
2127 | N_Selected_Component
2130 raise Program_Error;
2132 -- The following nodes are never generated in GNATprove mode
2134 when N_Expression_With_Actions
2136 | N_Unchecked_Expression
2138 raise Program_Error;
2140 end Check_Expression;
2146 procedure Check_List (L : List_Id) is
2150 while Present (N) loop
2156 --------------------------
2157 -- Check_Loop_Statement --
2158 --------------------------
2160 procedure Check_Loop_Statement (Stmt : Node_Id) is
2162 -- Local Subprograms
2164 procedure Check_Is_Less_Restrictive_Env
2165 (Exiting_Env : Perm_Env;
2166 Entry_Env : Perm_Env);
2167 -- This procedure checks that the Exiting_Env environment is less
2168 -- restrictive than the Entry_Env environment.
2170 procedure Check_Is_Less_Restrictive_Tree
2171 (New_Tree : Perm_Tree_Access;
2172 Orig_Tree : Perm_Tree_Access;
2174 -- Auxiliary procedure to check that the tree New_Tree is less
2175 -- restrictive than the tree Orig_Tree for the entity E.
2177 procedure Perm_Error_Loop_Exit
2181 Found_Perm : Perm_Kind;
2183 -- A procedure that is called when the permissions found contradict
2184 -- the rules established by the RM at the exit of loops. This function
2185 -- is called with the entity, the node of the enclosing loop, the
2186 -- permission that was expected, and the permission found, and issues
2187 -- an appropriate error message.
2189 -----------------------------------
2190 -- Check_Is_Less_Restrictive_Env --
2191 -----------------------------------
2193 procedure Check_Is_Less_Restrictive_Env
2194 (Exiting_Env : Perm_Env;
2195 Entry_Env : Perm_Env)
2197 Comp_Entry : Perm_Tree_Maps.Key_Option;
2198 Iter_Entry, Iter_Exit : Perm_Tree_Access;
2201 Comp_Entry := Get_First_Key (Entry_Env);
2202 while Comp_Entry.Present loop
2203 Iter_Entry := Get (Entry_Env, Comp_Entry.K);
2204 pragma Assert (Iter_Entry /= null);
2205 Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
2206 pragma Assert (Iter_Exit /= null);
2207 Check_Is_Less_Restrictive_Tree
2208 (New_Tree => Iter_Exit,
2209 Orig_Tree => Iter_Entry,
2211 Comp_Entry := Get_Next_Key (Entry_Env);
2213 end Check_Is_Less_Restrictive_Env;
2215 ------------------------------------
2216 -- Check_Is_Less_Restrictive_Tree --
2217 ------------------------------------
2219 procedure Check_Is_Less_Restrictive_Tree
2220 (New_Tree : Perm_Tree_Access;
2221 Orig_Tree : Perm_Tree_Access;
2224 -- Local subprograms
2226 procedure Check_Is_Less_Restrictive_Tree_Than
2227 (Tree : Perm_Tree_Access;
2230 -- Auxiliary procedure to check that the tree N is less restrictive
2231 -- than the given permission P.
2233 procedure Check_Is_More_Restrictive_Tree_Than
2234 (Tree : Perm_Tree_Access;
2237 -- Auxiliary procedure to check that the tree N is more restrictive
2238 -- than the given permission P.
2240 -----------------------------------------
2241 -- Check_Is_Less_Restrictive_Tree_Than --
2242 -----------------------------------------
2244 procedure Check_Is_Less_Restrictive_Tree_Than
2245 (Tree : Perm_Tree_Access;
2250 if not (Permission (Tree) >= Perm) then
2251 Perm_Error_Loop_Exit
2252 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2256 when Entire_Object =>
2257 if not (Children_Permission (Tree) >= Perm) then
2258 Perm_Error_Loop_Exit
2259 (E, Stmt, Children_Permission (Tree), Perm,
2260 Explanation (Tree));
2265 Check_Is_Less_Restrictive_Tree_Than
2266 (Get_All (Tree), Perm, E);
2268 when Array_Component =>
2269 Check_Is_Less_Restrictive_Tree_Than
2270 (Get_Elem (Tree), Perm, E);
2272 when Record_Component =>
2274 Comp : Perm_Tree_Access;
2276 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2277 while Comp /= null loop
2278 Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
2280 Perm_Tree_Maps.Get_Next (Component (Tree));
2284 end Check_Is_Less_Restrictive_Tree_Than;
2286 -----------------------------------------
2287 -- Check_Is_More_Restrictive_Tree_Than --
2288 -----------------------------------------
2290 procedure Check_Is_More_Restrictive_Tree_Than
2291 (Tree : Perm_Tree_Access;
2296 if not (Perm >= Permission (Tree)) then
2297 Perm_Error_Loop_Exit
2298 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2302 when Entire_Object =>
2303 if not (Perm >= Children_Permission (Tree)) then
2304 Perm_Error_Loop_Exit
2305 (E, Stmt, Children_Permission (Tree), Perm,
2306 Explanation (Tree));
2310 Check_Is_More_Restrictive_Tree_Than
2311 (Get_All (Tree), Perm, E);
2313 when Array_Component =>
2314 Check_Is_More_Restrictive_Tree_Than
2315 (Get_Elem (Tree), Perm, E);
2317 when Record_Component =>
2319 Comp : Perm_Tree_Access;
2321 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2322 while Comp /= null loop
2323 Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
2325 Perm_Tree_Maps.Get_Next (Component (Tree));
2329 end Check_Is_More_Restrictive_Tree_Than;
2331 -- Start of processing for Check_Is_Less_Restrictive_Tree
2334 if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
2335 Perm_Error_Loop_Exit
2338 Perm => Permission (New_Tree),
2339 Found_Perm => Permission (Orig_Tree),
2340 Expl => Explanation (New_Tree));
2343 case Kind (New_Tree) is
2345 -- Potentially folded tree. We check the other tree Orig_Tree to
2346 -- check whether it is folded or not. If folded we just compare
2347 -- their Permission and Children_Permission, if not, then we
2348 -- look at the Children_Permission of the folded tree against
2349 -- the unfolded tree Orig_Tree.
2351 when Entire_Object =>
2352 case Kind (Orig_Tree) is
2353 when Entire_Object =>
2354 if not (Children_Permission (New_Tree) <=
2355 Children_Permission (Orig_Tree))
2357 Perm_Error_Loop_Exit
2359 Children_Permission (New_Tree),
2360 Children_Permission (Orig_Tree),
2361 Explanation (New_Tree));
2365 Check_Is_More_Restrictive_Tree_Than
2366 (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
2368 when Array_Component =>
2369 Check_Is_More_Restrictive_Tree_Than
2370 (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
2372 when Record_Component =>
2374 Comp : Perm_Tree_Access;
2376 Comp := Perm_Tree_Maps.Get_First
2377 (Component (Orig_Tree));
2378 while Comp /= null loop
2379 Check_Is_More_Restrictive_Tree_Than
2380 (Comp, Children_Permission (New_Tree), E);
2381 Comp := Perm_Tree_Maps.Get_Next
2382 (Component (Orig_Tree));
2388 case Kind (Orig_Tree) is
2389 when Entire_Object =>
2390 Check_Is_Less_Restrictive_Tree_Than
2391 (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
2394 Check_Is_Less_Restrictive_Tree
2395 (Get_All (New_Tree), Get_All (Orig_Tree), E);
2398 raise Program_Error;
2401 when Array_Component =>
2402 case Kind (Orig_Tree) is
2403 when Entire_Object =>
2404 Check_Is_Less_Restrictive_Tree_Than
2405 (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2407 when Array_Component =>
2408 Check_Is_Less_Restrictive_Tree
2409 (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2412 raise Program_Error;
2415 when Record_Component =>
2417 CompN : Perm_Tree_Access;
2420 Perm_Tree_Maps.Get_First (Component (New_Tree));
2421 case Kind (Orig_Tree) is
2422 when Entire_Object =>
2423 while CompN /= null loop
2424 Check_Is_Less_Restrictive_Tree_Than
2425 (CompN, Children_Permission (Orig_Tree), E);
2428 Perm_Tree_Maps.Get_Next (Component (New_Tree));
2431 when Record_Component =>
2434 KeyO : Perm_Tree_Maps.Key_Option;
2435 CompO : Perm_Tree_Access;
2437 KeyO := Perm_Tree_Maps.Get_First_Key
2438 (Component (Orig_Tree));
2439 while KeyO.Present loop
2440 CompN := Perm_Tree_Maps.Get
2441 (Component (New_Tree), KeyO.K);
2442 CompO := Perm_Tree_Maps.Get
2443 (Component (Orig_Tree), KeyO.K);
2444 pragma Assert (CompO /= null);
2446 Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2448 KeyO := Perm_Tree_Maps.Get_Next_Key
2449 (Component (Orig_Tree));
2454 raise Program_Error;
2458 end Check_Is_Less_Restrictive_Tree;
2460 --------------------------
2461 -- Perm_Error_Loop_Exit --
2462 --------------------------
2464 procedure Perm_Error_Loop_Exit
2468 Found_Perm : Perm_Kind;
2472 if Emit_Messages then
2473 Error_Msg_Node_2 := Loop_Id;
2475 ("insufficient permission for & when exiting loop &", E);
2476 Perm_Mismatch (Exp_Perm => Perm,
2477 Act_Perm => Found_Perm,
2481 end Perm_Error_Loop_Exit;
2485 Loop_Name : constant Entity_Id := Entity (Identifier (Stmt));
2486 Loop_Env : constant Perm_Env_Access := new Perm_Env;
2487 Scheme : constant Node_Id := Iteration_Scheme (Stmt);
2489 -- Start of processing for Check_Loop_Statement
2492 -- Save environment prior to the loop
2494 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2496 -- Add saved environment to loop environment
2498 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2500 -- If the loop is not a plain-loop, then it may either never be entered,
2501 -- or it may be exited after a number of iterations. Hence add the
2502 -- current permission environment as the initial loop exit environment.
2503 -- Otherwise, the loop exit environment remains empty until it is
2504 -- populated by analyzing exit statements.
2506 if Present (Iteration_Scheme (Stmt)) then
2508 Exit_Env : constant Perm_Env_Access := new Perm_Env;
2511 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2512 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2518 if Present (Scheme) then
2520 -- Case of a WHILE loop
2522 if Present (Condition (Scheme)) then
2523 Check_Expression (Condition (Scheme), Read);
2525 -- Case of a FOR loop
2529 Param_Spec : constant Node_Id :=
2530 Loop_Parameter_Specification (Scheme);
2531 Iter_Spec : constant Node_Id := Iterator_Specification (Scheme);
2533 if Present (Param_Spec) then
2535 (Discrete_Subtype_Definition (Param_Spec), Read);
2537 Check_Expression (Name (Iter_Spec), Read);
2538 if Present (Subtype_Indication (Iter_Spec)) then
2539 Check_Expression (Subtype_Indication (Iter_Spec), Read);
2546 Check_List (Statements (Stmt));
2548 -- Check that environment gets less restrictive at end of loop
2550 Check_Is_Less_Restrictive_Env
2551 (Exiting_Env => Current_Perm_Env,
2552 Entry_Env => Loop_Env.all);
2554 -- Set environment to the one for exiting the loop
2557 Exit_Env : constant Perm_Env_Access :=
2558 Get (Current_Loops_Accumulators, Loop_Name);
2560 Free_Env (Current_Perm_Env);
2562 -- In the normal case, Exit_Env is not null and we use it. In the
2563 -- degraded case of a plain-loop without exit statements, Exit_Env is
2564 -- null, and we use the initial permission environment at the start
2565 -- of the loop to continue analysis. Any environment would be fine
2566 -- here, since the code after the loop is dead code, but this way we
2567 -- avoid spurious errors by having at least variables in scope inside
2570 if Exit_Env /= null then
2571 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2572 Free_Env (Loop_Env.all);
2573 Free_Env (Exit_Env.all);
2575 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2576 Free_Env (Loop_Env.all);
2579 end Check_Loop_Statement;
2585 procedure Check_Node (N : Node_Id) is
2588 when N_Declaration =>
2589 Check_Declaration (N);
2592 Check_Node (Get_Body_From_Stub (N));
2594 when N_Statement_Other_Than_Procedure_Call =>
2595 Check_Statement (N);
2597 when N_Procedure_Call_Statement =>
2598 Check_Call_Statement (N);
2600 when N_Package_Body =>
2601 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2602 Check_Package_Body (N);
2605 when N_Subprogram_Body
2609 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2610 Check_Callable_Body (N);
2613 when N_Protected_Body =>
2614 Check_List (Declarations (N));
2616 when N_Package_Declaration =>
2617 Check_Package_Spec (N);
2619 when N_Handled_Sequence_Of_Statements =>
2620 Check_List (Statements (N));
2625 -- Ignored constructs for pointer checking
2627 when N_Abstract_Subprogram_Declaration
2629 | N_Attribute_Definition_Clause
2631 | N_Delta_Constraint
2632 | N_Digits_Constraint
2634 | N_Enumeration_Representation_Clause
2635 | N_Exception_Declaration
2636 | N_Exception_Renaming_Declaration
2637 | N_Formal_Package_Declaration
2638 | N_Formal_Subprogram_Declaration
2640 | N_Freeze_Generic_Entity
2641 | N_Function_Instantiation
2642 | N_Generic_Function_Renaming_Declaration
2643 | N_Generic_Package_Declaration
2644 | N_Generic_Package_Renaming_Declaration
2645 | N_Generic_Procedure_Renaming_Declaration
2646 | N_Generic_Subprogram_Declaration
2647 | N_Implicit_Label_Declaration
2650 | N_Number_Declaration
2651 | N_Object_Renaming_Declaration
2653 | N_Package_Instantiation
2654 | N_Package_Renaming_Declaration
2655 | N_Procedure_Instantiation
2657 | N_Record_Representation_Clause
2658 | N_Subprogram_Declaration
2659 | N_Subprogram_Renaming_Declaration
2660 | N_Task_Type_Declaration
2661 | N_Use_Package_Clause
2664 | N_Validate_Unchecked_Conversion
2665 | N_Variable_Reference_Marker
2666 | N_Discriminant_Association
2668 -- ??? check whether we should do something special for
2669 -- N_Discriminant_Association, or maybe raise Program_Error.
2673 -- Checking should not be called directly on these nodes
2676 raise Program_Error;
2680 ------------------------
2681 -- Check_Package_Body --
2682 ------------------------
2684 procedure Check_Package_Body (Pack : Node_Id) is
2685 Save_In_Elab : constant Boolean := Inside_Elaboration;
2686 Spec : constant Node_Id :=
2687 Package_Specification (Corresponding_Spec (Pack));
2688 Id : constant Entity_Id := Defining_Entity (Pack);
2689 Prag : constant Node_Id := SPARK_Pragma (Id);
2690 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2691 Saved_Env : Perm_Env;
2695 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2697 Inside_Elaboration := True;
2699 -- Save environment and put a new one in place
2701 Move_Env (Current_Perm_Env, Saved_Env);
2703 -- Reanalyze package spec to have its variables in the environment
2705 Check_List (Visible_Declarations (Spec));
2706 Check_List (Private_Declarations (Spec));
2708 -- Check declarations and statements in the special mode for
2711 Check_List (Declarations (Pack));
2713 if Present (Aux_Prag)
2714 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2716 Check_Node (Handled_Statement_Sequence (Pack));
2719 -- Restore the saved environment and free the current one
2721 Move_Env (Saved_Env, Current_Perm_Env);
2723 Inside_Elaboration := Save_In_Elab;
2725 end Check_Package_Body;
2727 ------------------------
2728 -- Check_Package_Spec --
2729 ------------------------
2731 procedure Check_Package_Spec (Pack : Node_Id) is
2732 Save_In_Elab : constant Boolean := Inside_Elaboration;
2733 Spec : constant Node_Id := Specification (Pack);
2734 Id : constant Entity_Id := Defining_Entity (Pack);
2735 Prag : constant Node_Id := SPARK_Pragma (Id);
2736 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2737 Saved_Env : Perm_Env;
2741 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2743 Inside_Elaboration := True;
2745 -- Save environment and put a new one in place
2747 Move_Env (Current_Perm_Env, Saved_Env);
2749 -- Check declarations in the special mode for elaboration
2751 Check_List (Visible_Declarations (Spec));
2753 if Present (Aux_Prag)
2754 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2756 Check_List (Private_Declarations (Spec));
2759 -- Restore the saved environment and free the current one. As part of
2760 -- the restoration, the environment of the package spec is merged in
2761 -- the enclosing environment, which may be an enclosing
2762 -- package/subprogram spec or body which has access to the variables
2763 -- of the package spec.
2765 Merge_Env (Saved_Env, Current_Perm_Env);
2767 Inside_Elaboration := Save_In_Elab;
2769 end Check_Package_Spec;
2771 -------------------------------
2772 -- Check_Parameter_Or_Global --
2773 -------------------------------
2775 procedure Check_Parameter_Or_Global
2780 Global_Var : Boolean)
2782 Mode : Checking_Mode;
2783 Status : Error_Status;
2787 and then Is_Anonymous_Access_Type (Typ)
2789 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
2791 if Status /= OK then
2797 when E_In_Parameter =>
2799 -- Inputs of functions have R permission only
2801 if Ekind (Subp) = E_Function then
2804 -- Input global variables have R permission only
2806 elsif Global_Var then
2809 -- Anonymous access to constant is an observe
2811 elsif Is_Anonymous_Access_Type (Typ)
2812 and then Is_Access_Constant (Typ)
2816 -- Other access types are a borrow
2818 elsif Is_Access_Type (Typ) then
2821 -- Deep types other than access types define an observe
2823 elsif Is_Deep (Typ) then
2826 -- Otherwise the variable is read
2832 when E_Out_Parameter =>
2835 when E_In_Out_Parameter =>
2839 if Mode = Assign then
2840 Check_Expression (Expr, Read_Subexpr);
2843 Check_Expression (Expr, Mode);
2844 end Check_Parameter_Or_Global;
2846 procedure Check_Globals_Inst is
2847 new Handle_Globals (Check_Parameter_Or_Global);
2849 procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst;
2855 procedure Check_Pragma (Prag : Node_Id) is
2856 Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag);
2857 Arg1 : constant Node_Id :=
2858 First (Pragma_Argument_Associations (Prag));
2859 Arg2 : Node_Id := Empty;
2862 if Present (Arg1) then
2863 Arg2 := Next (Arg1);
2867 when Pragma_Check =>
2869 Expr : constant Node_Id := Expression (Arg2);
2871 Check_Expression (Expr, Read);
2874 -- There is no need to check contracts, as these can only access
2875 -- inputs and outputs of the subprogram. Inputs are checked
2876 -- independently for R permission. Outputs are checked
2877 -- independently to have RW permission on exit.
2879 -- Postconditions are checked for correct use of 'Old, but starting
2880 -- from the corresponding declaration, in order to avoid dealing with
2881 -- with contracts on generic subprograms, which are not handled in
2884 when Pragma_Precondition
2885 | Pragma_Postcondition
2886 | Pragma_Contract_Cases
2887 | Pragma_Refined_Post
2891 -- The same holds for the initial condition after package
2892 -- elaboration, for the different reason that library-level
2893 -- variables can only be left in RW state after elaboration.
2895 when Pragma_Initial_Condition =>
2898 -- These pragmas should have been rewritten and/or removed in
2902 | Pragma_Assert_And_Cut
2904 | Pragma_Compile_Time_Error
2905 | Pragma_Compile_Time_Warning
2907 | Pragma_Loop_Invariant
2909 raise Program_Error;
2916 -------------------------
2917 -- Check_Safe_Pointers --
2918 -------------------------
2920 procedure Check_Safe_Pointers (N : Node_Id) is
2922 -- Local subprograms
2924 procedure Check_List (L : List_Id);
2925 -- Call the main analysis procedure on each element of the list
2927 procedure Initialize;
2928 -- Initialize global variables before starting the analysis of a body
2934 procedure Check_List (L : List_Id) is
2938 while Present (N) loop
2939 Check_Safe_Pointers (N);
2948 procedure Initialize is
2950 Reset (Current_Loops_Envs);
2951 Reset (Current_Loops_Accumulators);
2952 Reset (Current_Perm_Env);
2955 -- Start of processing for Check_Safe_Pointers
2961 when N_Compilation_Unit =>
2962 Check_Safe_Pointers (Unit (N));
2965 | N_Package_Declaration
2969 E : constant Entity_Id := Defining_Entity (N);
2970 Prag : constant Node_Id := SPARK_Pragma (E);
2971 -- SPARK_Mode pragma in application
2974 if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
2977 elsif Present (Prag) then
2978 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
2982 elsif Nkind (N) = N_Package_Body then
2983 Check_List (Declarations (N));
2985 elsif Nkind (N) = N_Package_Declaration then
2986 Check_List (Private_Declarations (Specification (N)));
2987 Check_List (Visible_Declarations (Specification (N)));
2994 end Check_Safe_Pointers;
2996 ---------------------------------------
2997 -- Check_Source_Of_Borrow_Or_Observe --
2998 ---------------------------------------
3000 procedure Check_Source_Of_Borrow_Or_Observe
3002 Status : out Error_Status)
3007 if Is_Path_Expression (Expr) then
3008 Root := Get_Root_Object (Expr);
3015 -- SPARK RM 3.10(3): If the target of an assignment operation is an
3016 -- object of an anonymous access-to-object type (including copy-in for
3017 -- a parameter), then the source shall be a name denoting a part of a
3018 -- stand-alone object, a part of a parameter, or a call to a traversal
3022 if Emit_Messages then
3023 if Nkind (Expr) = N_Function_Call then
3025 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3027 ("\function called must be a traversal function", Expr);
3030 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3032 ("\expression must be part of stand-alone object or " &
3040 end Check_Source_Of_Borrow_Or_Observe;
3042 ---------------------
3043 -- Check_Statement --
3044 ---------------------
3046 procedure Check_Statement (Stmt : Node_Id) is
3048 case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
3050 -- An entry call is handled like other calls
3052 when N_Entry_Call_Statement =>
3053 Check_Call_Statement (Stmt);
3055 -- An assignment may correspond to a move, a borrow, or an observe
3057 when N_Assignment_Statement =>
3059 Target : constant Node_Id := Name (Stmt);
3062 -- Start with checking that the subexpressions of the target
3063 -- path are readable, before possibly updating the permission
3064 -- of these subexpressions in Check_Assignment.
3066 Check_Expression (Target, Read_Subexpr);
3068 Check_Assignment (Target => Target,
3069 Expr => Expression (Stmt));
3071 -- ??? We need a rule that forbids targets of assignment for
3072 -- which the path is not known, for example when there is a
3073 -- function call involved (which includes calls to traversal
3074 -- functions). Otherwise there is no way to update the
3075 -- corresponding path permission.
3077 if No (Get_Root_Object
3078 (Target, Through_Traversal => False))
3080 if Emit_Messages then
3081 Error_Msg_N ("illegal target for assignment", Target);
3086 Check_Expression (Target, Assign);
3089 when N_Block_Statement =>
3090 Check_List (Declarations (Stmt));
3091 Check_Node (Handled_Statement_Sequence (Stmt));
3093 -- Remove local borrowers and observers
3096 Decl : Node_Id := First (Declarations (Stmt));
3099 while Present (Decl) loop
3100 if Nkind (Decl) = N_Object_Declaration then
3101 Var := Defining_Identifier (Decl);
3102 Remove (Current_Borrowers, Var);
3103 Remove (Current_Observers, Var);
3110 when N_Case_Statement =>
3113 Saved_Env : Perm_Env;
3114 -- Copy of environment for analysis of the different cases
3116 -- Accumulator for the different cases
3119 Check_Expression (Expression (Stmt), Read);
3123 Copy_Env (Current_Perm_Env, Saved_Env);
3125 -- First alternative
3127 Alt := First (Alternatives (Stmt));
3128 Check_List (Statements (Alt));
3133 Move_Env (Current_Perm_Env, New_Env);
3135 -- Other alternatives
3137 while Present (Alt) loop
3139 -- Restore environment
3141 Copy_Env (Saved_Env, Current_Perm_Env);
3145 Check_List (Statements (Alt));
3148 -- Merge Current_Perm_Env into New_Env
3150 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3153 Move_Env (New_Env, Current_Perm_Env);
3154 Free_Env (Saved_Env);
3157 when N_Delay_Relative_Statement
3158 | N_Delay_Until_Statement
3160 Check_Expression (Expression (Stmt), Read);
3162 when N_Loop_Statement =>
3163 Check_Loop_Statement (Stmt);
3165 when N_Simple_Return_Statement =>
3167 Subp : constant Entity_Id :=
3168 Return_Applies_To (Return_Statement_Entity (Stmt));
3169 Expr : constant Node_Id := Expression (Stmt);
3171 if Present (Expression (Stmt)) then
3173 Return_Typ : constant Entity_Id :=
3174 Etype (Expression (Stmt));
3177 -- SPARK RM 3.10(5): A return statement that applies
3178 -- to a traversal function that has an anonymous
3179 -- access-to-constant (respectively, access-to-variable)
3180 -- result type, shall return either the literal null
3181 -- or an access object denoted by a direct or indirect
3182 -- observer (respectively, borrower) of the traversed
3185 if Is_Anonymous_Access_Type (Return_Typ) then
3186 pragma Assert (Is_Traversal_Function (Subp));
3188 if Nkind (Expr) /= N_Null then
3190 Expr_Root : constant Entity_Id :=
3191 Get_Root_Object (Expr, Is_Traversal => True);
3192 Param : constant Entity_Id :=
3193 First_Formal (Subp);
3195 if Param /= Expr_Root and then Emit_Messages then
3197 ("returned value must be rooted in "
3198 & "traversed parameter & "
3199 & "(SPARK RM 3.10(5))",
3205 -- Move expression to caller
3207 elsif Is_Deep (Return_Typ) then
3209 if Is_Path_Expression (Expr) then
3210 Check_Expression (Expr, Move);
3213 if Emit_Messages then
3215 ("expression not allowed as source of move",
3222 Check_Expression (Expr, Read);
3225 if Ekind_In (Subp, E_Procedure, E_Entry)
3226 and then not No_Return (Subp)
3228 Return_Parameters (Subp);
3229 Return_Globals (Subp);
3235 when N_Extended_Return_Statement =>
3237 Subp : constant Entity_Id :=
3238 Return_Applies_To (Return_Statement_Entity (Stmt));
3239 Decls : constant List_Id := Return_Object_Declarations (Stmt);
3240 Decl : constant Node_Id := Last_Non_Pragma (Decls);
3241 Obj : constant Entity_Id := Defining_Identifier (Decl);
3245 -- SPARK RM 3.10(5): return statement of traversal function
3247 if Is_Traversal_Function (Subp) and then Emit_Messages then
3249 ("extended return cannot apply to a traversal function",
3253 Check_List (Return_Object_Declarations (Stmt));
3254 Check_Node (Handled_Statement_Sequence (Stmt));
3256 if Is_Deep (Etype (Obj)) then
3257 Perm := Get_Perm (Obj);
3259 if Perm /= Read_Write then
3260 Perm_Error (Decl, Read_Write, Perm,
3261 Expl => Get_Expl (Obj));
3265 if Ekind_In (Subp, E_Procedure, E_Entry)
3266 and then not No_Return (Subp)
3268 Return_Parameters (Subp);
3269 Return_Globals (Subp);
3273 -- On loop exit, merge the current permission environment with the
3274 -- accumulator for the given loop.
3276 when N_Exit_Statement =>
3278 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
3279 Saved_Accumulator : constant Perm_Env_Access :=
3280 Get (Current_Loops_Accumulators, Loop_Name);
3281 Environment_Copy : constant Perm_Env_Access :=
3284 Copy_Env (Current_Perm_Env, Environment_Copy.all);
3286 if Saved_Accumulator = null then
3287 Set (Current_Loops_Accumulators,
3288 Loop_Name, Environment_Copy);
3290 Merge_Env (Source => Environment_Copy.all,
3291 Target => Saved_Accumulator.all);
3292 -- ??? Either free Environment_Copy, or change the type
3293 -- of loop accumulators to directly store permission
3298 -- On branches, analyze each branch independently on a fresh copy of
3299 -- the permission environment, then merge the resulting permission
3302 when N_If_Statement =>
3304 Saved_Env : Perm_Env;
3306 -- Accumulator for the different branches
3309 Check_Expression (Condition (Stmt), Read);
3313 Copy_Env (Current_Perm_Env, Saved_Env);
3317 Check_List (Then_Statements (Stmt));
3318 Move_Env (Current_Perm_Env, New_Env);
3325 Branch := First (Elsif_Parts (Stmt));
3326 while Present (Branch) loop
3328 -- Restore current permission environment
3330 Copy_Env (Saved_Env, Current_Perm_Env);
3331 Check_Expression (Condition (Branch), Read);
3332 Check_List (Then_Statements (Branch));
3334 -- Merge current permission environment
3336 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3343 -- Restore current permission environment
3345 Copy_Env (Saved_Env, Current_Perm_Env);
3346 Check_List (Else_Statements (Stmt));
3348 -- Merge current permission environment
3350 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3354 Move_Env (New_Env, Current_Perm_Env);
3355 Free_Env (Saved_Env);
3358 -- We should ideally ignore the branch after raising an exception,
3359 -- so that it is not taken into account in merges. For now, just
3360 -- propagate the current environment.
3362 when N_Raise_Statement =>
3365 when N_Null_Statement =>
3368 -- Unsupported constructs in SPARK
3370 when N_Abort_Statement
3371 | N_Accept_Statement
3372 | N_Asynchronous_Select
3374 | N_Conditional_Entry_Call
3376 | N_Requeue_Statement
3377 | N_Selective_Accept
3378 | N_Timed_Entry_Call
3382 -- The following nodes are never generated in GNATprove mode
3384 when N_Compound_Statement
3387 raise Program_Error;
3389 end Check_Statement;
3395 procedure Check_Type (Typ : Entity_Id) is
3396 Check_Typ : constant Entity_Id := Retysp (Typ);
3399 case Type_Kind'(Ekind (Check_Typ)) is
3401 case Access_Kind'(Ekind (Check_Typ)) is
3403 | E_Anonymous_Access_Type
3406 when E_Access_Subtype =>
3407 Check_Type (Base_Type (Check_Typ));
3408 when E_Access_Attribute_Type =>
3409 if Emit_Messages then
3410 Error_Msg_N ("access attribute not allowed in SPARK",
3413 when E_Allocator_Type =>
3414 if Emit_Messages then
3415 Error_Msg_N ("missing type resolution", Check_Typ);
3417 when E_General_Access_Type =>
3418 if Emit_Messages then
3420 ("general access type & not allowed in SPARK",
3421 Check_Typ, Check_Typ);
3423 when Access_Subprogram_Kind =>
3424 if Emit_Messages then
3426 ("access to subprogram type & not allowed in SPARK",
3427 Check_Typ, Check_Typ);
3434 Check_Type (Component_Type (Check_Typ));
3437 if Is_Deep (Check_Typ)
3438 and then (Is_Tagged_Type (Check_Typ)
3439 or else Is_Class_Wide_Type (Check_Typ))
3441 if Emit_Messages then
3443 ("tagged type & cannot be owning in SPARK",
3444 Check_Typ, Check_Typ);
3451 Comp := First_Component_Or_Discriminant (Check_Typ);
3452 while Present (Comp) loop
3454 -- Ignore components which are not visible in SPARK
3456 if Component_Is_Visible_In_SPARK (Comp) then
3457 Check_Type (Etype (Comp));
3459 Next_Component_Or_Discriminant (Comp);
3465 | E_String_Literal_Subtype
3474 -- Do not check type whose full view is not SPARK
3478 | E_Limited_Private_Type
3479 | E_Limited_Private_Subtype
3489 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is
3491 -- Special case for the object declared in an extended return statement
3493 if Nkind (N) = N_Defining_Identifier then
3495 C : constant Perm_Tree_Access :=
3496 Get (Current_Perm_Env, Unique_Entity (N));
3498 pragma Assert (C /= null);
3499 return Explanation (C);
3502 -- The expression is a call to a traversal function
3504 elsif Is_Traversal_Function_Call (N) then
3507 -- The expression is directly rooted in an object
3509 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3511 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3513 case Tree_Or_Perm.R is
3515 return Tree_Or_Perm.Explanation;
3518 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3519 return Explanation (Tree_Or_Perm.Tree_Access);
3523 -- The expression is a function call, an allocation, or null
3530 -----------------------------------
3531 -- Get_Observed_Or_Borrowed_Expr --
3532 -----------------------------------
3534 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is
3536 if Is_Traversal_Function_Call (Expr) then
3537 return First_Actual (Expr);
3541 end Get_Observed_Or_Borrowed_Expr;
3547 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is
3549 -- Special case for the object declared in an extended return statement
3551 if Nkind (N) = N_Defining_Identifier then
3553 C : constant Perm_Tree_Access :=
3554 Get (Current_Perm_Env, Unique_Entity (N));
3556 pragma Assert (C /= null);
3557 return Permission (C);
3560 -- The expression is a call to a traversal function
3562 elsif Is_Traversal_Function_Call (N) then
3564 Callee : constant Entity_Id := Get_Called_Entity (N);
3566 if Is_Access_Constant (Etype (Callee)) then
3573 -- The expression is directly rooted in an object
3575 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3577 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3579 case Tree_Or_Perm.R is
3581 return Tree_Or_Perm.Found_Permission;
3584 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3585 return Permission (Tree_Or_Perm.Tree_Access);
3589 -- The expression is a function call, an allocation, or null
3596 ----------------------
3597 -- Get_Perm_Or_Tree --
3598 ----------------------
3600 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
3604 when N_Expanded_Name
3608 C : constant Perm_Tree_Access :=
3609 Get (Current_Perm_Env, Unique_Entity (Entity (N)));
3611 -- Except during elaboration, the root object should have been
3612 -- declared and entered into the current permission
3615 if not Inside_Elaboration
3618 Illegal_Global_Usage (N, N);
3621 return (R => Unfolded, Tree_Access => C);
3624 -- For a nonterminal path, we get the permission tree of its
3625 -- prefix, and then get the subtree associated with the extension,
3626 -- if unfolded. If folded, we return the permission associated with
3629 when N_Explicit_Dereference
3630 | N_Indexed_Component
3631 | N_Selected_Component
3635 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
3639 -- Some earlier prefix was already folded, return the
3640 -- permission found.
3646 case Kind (C.Tree_Access) is
3648 -- If the prefix tree is already folded, return the
3649 -- children permission.
3651 when Entire_Object =>
3652 return (R => Folded,
3654 Children_Permission (C.Tree_Access),
3656 Explanation (C.Tree_Access));
3659 pragma Assert (Nkind (N) = N_Explicit_Dereference);
3660 return (R => Unfolded,
3661 Tree_Access => Get_All (C.Tree_Access));
3663 when Record_Component =>
3664 pragma Assert (Nkind (N) = N_Selected_Component);
3666 Comp : constant Entity_Id :=
3667 Original_Record_Component
3668 (Entity (Selector_Name (N)));
3669 D : constant Perm_Tree_Access :=
3671 (Component (C.Tree_Access), Comp);
3673 pragma Assert (D /= null);
3674 return (R => Unfolded,
3678 when Array_Component =>
3679 pragma Assert (Nkind (N) = N_Indexed_Component
3681 Nkind (N) = N_Slice);
3682 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3683 return (R => Unfolded,
3684 Tree_Access => Get_Elem (C.Tree_Access));
3689 when N_Qualified_Expression
3691 | N_Unchecked_Type_Conversion
3693 return Get_Perm_Or_Tree (Expression (N));
3696 raise Program_Error;
3698 end Get_Perm_Or_Tree;
3704 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
3706 return Set_Perm_Prefixes (N, None, Empty);
3709 ---------------------
3710 -- Get_Root_Object --
3711 ---------------------
3713 function Get_Root_Object
3715 Through_Traversal : Boolean := True;
3716 Is_Traversal : Boolean := False) return Entity_Id
3718 function GRO (Expr : Node_Id) return Entity_Id;
3719 -- Local wrapper on the actual function, to propagate the values of
3720 -- optional parameters.
3726 function GRO (Expr : Node_Id) return Entity_Id is
3728 return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
3731 Get_Root_Object : Boolean;
3732 pragma Unmodified (Get_Root_Object);
3733 -- Local variable to mask the name of function Get_Root_Object, to
3734 -- prevent direct call. Instead GRO wrapper should be called.
3736 -- Start of processing for Get_Root_Object
3739 if not Is_Subpath_Expression (Expr, Is_Traversal) then
3740 if Emit_Messages then
3741 Error_Msg_N ("name expected here for path", Expr);
3746 case Nkind (Expr) is
3747 when N_Expanded_Name
3750 return Entity (Expr);
3752 when N_Explicit_Dereference
3753 | N_Indexed_Component
3754 | N_Selected_Component
3757 return GRO (Prefix (Expr));
3759 -- There is no root object for an (extension) aggregate, allocator,
3764 | N_Extension_Aggregate
3770 -- In the case of a call to a traversal function, the root object is
3771 -- the root of the traversed parameter. Otherwise there is no root
3774 when N_Function_Call =>
3775 if Through_Traversal
3776 and then Is_Traversal_Function_Call (Expr)
3778 return GRO (First_Actual (Expr));
3783 when N_Qualified_Expression
3785 | N_Unchecked_Type_Conversion
3787 return GRO (Expression (Expr));
3789 when N_Attribute_Reference =>
3791 (Get_Attribute_Id (Attribute_Name (Expr)) =
3792 Attribute_Loop_Entry
3794 Get_Attribute_Id (Attribute_Name (Expr)) =
3796 or else Get_Attribute_Id (Attribute_Name (Expr)) =
3800 when N_If_Expression =>
3801 if Is_Traversal then
3803 Cond : constant Node_Id := First (Expressions (Expr));
3804 Then_Part : constant Node_Id := Next (Cond);
3805 Else_Part : constant Node_Id := Next (Then_Part);
3806 Then_Root : constant Entity_Id := GRO (Then_Part);
3807 Else_Root : constant Entity_Id := GRO (Else_Part);
3809 if Nkind (Then_Part) = N_Null then
3811 elsif Nkind (Else_Part) = N_Null then
3813 elsif Then_Root = Else_Root then
3816 if Emit_Messages then
3818 ("same name expected here in each branch", Expr);
3824 if Emit_Messages then
3825 Error_Msg_N ("name expected here for path", Expr);
3830 when N_Case_Expression =>
3831 if Is_Traversal then
3833 Cases : constant List_Id := Alternatives (Expr);
3834 Cur_Case : Node_Id := First (Cases);
3835 Cur_Root : Entity_Id;
3836 Common_Root : Entity_Id := Empty;
3839 while Present (Cur_Case) loop
3840 Cur_Root := GRO (Expression (Cur_Case));
3842 if Common_Root = Empty then
3843 Common_Root := Cur_Root;
3844 elsif Common_Root /= Cur_Root then
3845 if Emit_Messages then
3847 ("same name expected here in each branch", Expr);
3857 if Emit_Messages then
3858 Error_Msg_N ("name expected here for path", Expr);
3864 raise Program_Error;
3866 end Get_Root_Object;
3872 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
3906 -------------------------
3907 -- Has_Array_Component --
3908 -------------------------
3910 function Has_Array_Component (Expr : Node_Id) return Boolean is
3912 case Nkind (Expr) is
3913 when N_Expanded_Name
3918 when N_Explicit_Dereference
3919 | N_Selected_Component
3921 return Has_Array_Component (Prefix (Expr));
3923 when N_Indexed_Component
3934 when N_Qualified_Expression
3936 | N_Unchecked_Type_Conversion
3938 return Has_Array_Component (Expression (Expr));
3941 raise Program_Error;
3943 end Has_Array_Component;
3949 procedure Hp (P : Perm_Env) is
3950 Elem : Perm_Tree_Maps.Key_Option;
3953 Elem := Get_First_Key (P);
3954 while Elem.Present loop
3955 Print_Node_Briefly (Elem.K);
3956 Elem := Get_Next_Key (P);
3960 --------------------------
3961 -- Illegal_Global_Usage --
3962 --------------------------
3964 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id)
3967 Error_Msg_NE ("cannot use global variable & of deep type", N, E);
3968 Error_Msg_N ("\without prior declaration in a Global aspect", N);
3969 Errout.Finalize (Last_Call => True);
3970 Errout.Output_Messages;
3971 Exit_Program (E_Errors);
3972 end Illegal_Global_Usage;
3978 function Is_Deep (Typ : Entity_Id) return Boolean is
3980 case Type_Kind'(Ekind (Retysp (Typ))) is
3987 return Is_Deep (Component_Type (Retysp (Typ)));
3993 Comp := First_Component_Or_Discriminant (Retysp (Typ));
3994 while Present (Comp) loop
3996 -- Ignore components not visible in SPARK
3998 if Component_Is_Visible_In_SPARK (Comp)
3999 and then Is_Deep (Etype (Comp))
4003 Next_Component_Or_Discriminant (Comp);
4009 | E_String_Literal_Subtype
4018 -- Ignore full view of types if it is not in SPARK
4022 | E_Limited_Private_Type
4023 | E_Limited_Private_Subtype
4029 ----------------------
4030 -- Is_Local_Context --
4031 ----------------------
4033 function Is_Local_Context (Scop : Entity_Id) return Boolean is
4035 return Is_Subprogram_Or_Entry (Scop)
4036 or else Ekind (Scop) = E_Block;
4037 end Is_Local_Context;
4039 ------------------------
4040 -- Is_Path_Expression --
4041 ------------------------
4043 function Is_Path_Expression
4045 Is_Traversal : Boolean := False) return Boolean
4047 function IPE (Expr : Node_Id) return Boolean;
4048 -- Local wrapper on the actual function, to propagate the values of
4049 -- optional parameter Is_Traversal.
4055 function IPE (Expr : Node_Id) return Boolean is
4057 return Is_Path_Expression (Expr, Is_Traversal);
4060 Is_Path_Expression : Boolean;
4061 pragma Unmodified (Is_Path_Expression);
4062 -- Local variable to mask the name of function Is_Path_Expression, to
4063 -- prevent direct call. Instead IPE wrapper should be called.
4065 -- Start of processing for Is_Path_Expression
4068 case Nkind (Expr) is
4069 when N_Expanded_Name
4070 | N_Explicit_Dereference
4072 | N_Indexed_Component
4073 | N_Selected_Component
4078 -- Special value NULL corresponds to an empty path
4083 -- Object returned by an (extension) aggregate, an allocator, or
4084 -- a function call corresponds to a path.
4088 | N_Extension_Aggregate
4093 when N_Qualified_Expression
4095 | N_Unchecked_Type_Conversion
4097 return IPE (Expression (Expr));
4099 -- When returning from a traversal function, consider an
4100 -- if-expression as a possible path expression.
4102 when N_If_Expression =>
4103 if Is_Traversal then
4105 Cond : constant Node_Id := First (Expressions (Expr));
4106 Then_Part : constant Node_Id := Next (Cond);
4107 Else_Part : constant Node_Id := Next (Then_Part);
4109 return IPE (Then_Part)
4110 and then IPE (Else_Part);
4116 -- When returning from a traversal function, consider
4117 -- a case-expression as a possible path expression.
4119 when N_Case_Expression =>
4120 if Is_Traversal then
4122 Cases : constant List_Id := Alternatives (Expr);
4123 Cur_Case : Node_Id := First (Cases);
4126 while Present (Cur_Case) loop
4127 if not IPE (Expression (Cur_Case)) then
4142 end Is_Path_Expression;
4144 -------------------------
4145 -- Is_Prefix_Or_Almost --
4146 -------------------------
4148 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is
4150 type Expr_Array is array (Positive range <>) of Node_Id;
4151 -- Sequence of expressions that make up a path
4153 function Get_Expr_Array (Expr : Node_Id) return Expr_Array;
4154 pragma Precondition (Is_Path_Expression (Expr));
4155 -- Return the sequence of expressions that make up a path
4157 --------------------
4158 -- Get_Expr_Array --
4159 --------------------
4161 function Get_Expr_Array (Expr : Node_Id) return Expr_Array is
4163 case Nkind (Expr) is
4164 when N_Expanded_Name
4167 return Expr_Array'(1 => Expr);
4169 when N_Explicit_Dereference
4170 | N_Indexed_Component
4171 | N_Selected_Component
4174 return Get_Expr_Array (Prefix (Expr)) & Expr;
4176 when N_Qualified_Expression
4178 | N_Unchecked_Type_Conversion
4180 return Get_Expr_Array (Expression (Expr));
4183 raise Program_Error;
4189 Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref);
4190 Expr_Path : constant Expr_Array := Get_Expr_Array (Expr);
4192 Prefix_Root : constant Node_Id := Prefix_Path (1);
4193 Expr_Root : constant Node_Id := Expr_Path (1);
4195 Common_Len : constant Positive :=
4196 Positive'Min (Prefix_Path'Length, Expr_Path'Length);
4198 -- Start of processing for Is_Prefix_Or_Almost
4201 if Entity (Prefix_Root) /= Entity (Expr_Root) then
4205 for J in 2 .. Common_Len loop
4207 Prefix_Elt : constant Node_Id := Prefix_Path (J);
4208 Expr_Elt : constant Node_Id := Expr_Path (J);
4210 case Nkind (Prefix_Elt) is
4211 when N_Explicit_Dereference =>
4212 if Nkind (Expr_Elt) /= N_Explicit_Dereference then
4216 when N_Selected_Component =>
4217 if Nkind (Expr_Elt) /= N_Selected_Component
4218 or else Original_Record_Component
4219 (Entity (Selector_Name (Prefix_Elt)))
4220 /= Original_Record_Component
4221 (Entity (Selector_Name (Expr_Elt)))
4226 when N_Indexed_Component
4229 if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then
4234 raise Program_Error;
4239 -- If the expression path is longer than the prefix one, then at this
4240 -- point the prefix property holds.
4242 if Expr_Path'Length > Prefix_Path'Length then
4245 -- Otherwise check if none of the remaining path elements in the
4246 -- candidate prefix involve a dereference.
4249 for J in Common_Len + 1 .. Prefix_Path'Length loop
4250 if Nkind (Prefix_Path (J)) = N_Explicit_Dereference then
4257 end Is_Prefix_Or_Almost;
4259 ---------------------------
4260 -- Is_Subpath_Expression --
4261 ---------------------------
4263 function Is_Subpath_Expression
4265 Is_Traversal : Boolean := False) return Boolean
4268 return Is_Path_Expression (Expr, Is_Traversal)
4270 or else (Nkind_In (Expr, N_Qualified_Expression,
4272 N_Unchecked_Type_Conversion)
4273 and then Is_Subpath_Expression (Expression (Expr)))
4275 or else (Nkind (Expr) = N_Attribute_Reference
4277 (Get_Attribute_Id (Attribute_Name (Expr)) =
4280 Get_Attribute_Id (Attribute_Name (Expr)) =
4281 Attribute_Loop_Entry
4283 Get_Attribute_Id (Attribute_Name (Expr)) =
4286 or else Nkind (Expr) = N_Op_Concat;
4287 end Is_Subpath_Expression;
4289 ---------------------------
4290 -- Is_Traversal_Function --
4291 ---------------------------
4293 function Is_Traversal_Function (E : Entity_Id) return Boolean is
4295 return Ekind (E) = E_Function
4297 -- A function is said to be a traversal function if the result type of
4298 -- the function is an anonymous access-to-object type,
4300 and then Is_Anonymous_Access_Type (Etype (E))
4302 -- the function has at least one formal parameter,
4304 and then Present (First_Formal (E))
4306 -- and the function's first parameter is of an access type.
4308 and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
4309 end Is_Traversal_Function;
4311 --------------------------------
4312 -- Is_Traversal_Function_Call --
4313 --------------------------------
4315 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is
4317 return Nkind (Expr) = N_Function_Call
4318 and then Present (Get_Called_Entity (Expr))
4319 and then Is_Traversal_Function (Get_Called_Entity (Expr));
4320 end Is_Traversal_Function_Call;
4326 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
4327 Nam : Node_Id := Name (N);
4328 Stmt : Node_Id := N;
4331 while Present (Stmt) loop
4332 Stmt := Parent (Stmt);
4333 if Nkind (Stmt) = N_Loop_Statement then
4334 Nam := Identifier (Stmt);
4339 return Entity (Nam);
4346 function Lub (P1, P2 : Perm_Kind) return Perm_Kind is
4383 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is
4385 -- Local subprograms
4387 procedure Apply_Glb_Tree
4388 (A : Perm_Tree_Access;
4391 procedure Merge_Trees
4392 (Target : Perm_Tree_Access;
4393 Source : Perm_Tree_Access);
4395 --------------------
4396 -- Apply_Glb_Tree --
4397 --------------------
4399 procedure Apply_Glb_Tree
4400 (A : Perm_Tree_Access;
4404 A.all.Tree.Permission := Glb (Permission (A), P);
4407 when Entire_Object =>
4408 A.all.Tree.Children_Permission :=
4409 Glb (Children_Permission (A), P);
4412 Apply_Glb_Tree (Get_All (A), P);
4414 when Array_Component =>
4415 Apply_Glb_Tree (Get_Elem (A), P);
4417 when Record_Component =>
4419 Comp : Perm_Tree_Access;
4421 Comp := Perm_Tree_Maps.Get_First (Component (A));
4422 while Comp /= null loop
4423 Apply_Glb_Tree (Comp, P);
4424 Comp := Perm_Tree_Maps.Get_Next (Component (A));
4434 procedure Merge_Trees
4435 (Target : Perm_Tree_Access;
4436 Source : Perm_Tree_Access)
4438 Perm : constant Perm_Kind :=
4439 Glb (Permission (Target), Permission (Source));
4442 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
4443 Target.all.Tree.Permission := Perm;
4445 case Kind (Target) is
4446 when Entire_Object =>
4448 Child_Perm : constant Perm_Kind :=
4449 Children_Permission (Target);
4452 case Kind (Source) is
4453 when Entire_Object =>
4454 Target.all.Tree.Children_Permission :=
4455 Glb (Child_Perm, Children_Permission (Source));
4458 Copy_Tree (Source, Target);
4459 Target.all.Tree.Permission := Perm;
4460 Apply_Glb_Tree (Get_All (Target), Child_Perm);
4462 when Array_Component =>
4463 Copy_Tree (Source, Target);
4464 Target.all.Tree.Permission := Perm;
4465 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
4467 when Record_Component =>
4468 Copy_Tree (Source, Target);
4469 Target.all.Tree.Permission := Perm;
4471 Comp : Perm_Tree_Access;
4475 Perm_Tree_Maps.Get_First (Component (Target));
4476 while Comp /= null loop
4477 -- Apply glb tree on every component subtree
4479 Apply_Glb_Tree (Comp, Child_Perm);
4480 Comp := Perm_Tree_Maps.Get_Next
4481 (Component (Target));
4488 case Kind (Source) is
4489 when Entire_Object =>
4490 Apply_Glb_Tree (Get_All (Target),
4491 Children_Permission (Source));
4494 Merge_Trees (Get_All (Target), Get_All (Source));
4497 raise Program_Error;
4501 when Array_Component =>
4502 case Kind (Source) is
4503 when Entire_Object =>
4504 Apply_Glb_Tree (Get_Elem (Target),
4505 Children_Permission (Source));
4507 when Array_Component =>
4508 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4511 raise Program_Error;
4515 when Record_Component =>
4516 case Kind (Source) is
4517 when Entire_Object =>
4519 Child_Perm : constant Perm_Kind :=
4520 Children_Permission (Source);
4522 Comp : Perm_Tree_Access;
4525 Comp := Perm_Tree_Maps.Get_First
4526 (Component (Target));
4527 while Comp /= null loop
4528 -- Apply glb tree on every component subtree
4530 Apply_Glb_Tree (Comp, Child_Perm);
4532 Perm_Tree_Maps.Get_Next (Component (Target));
4536 when Record_Component =>
4538 Key_Source : Perm_Tree_Maps.Key_Option;
4539 CompTarget : Perm_Tree_Access;
4540 CompSource : Perm_Tree_Access;
4543 Key_Source := Perm_Tree_Maps.Get_First_Key
4544 (Component (Source));
4546 while Key_Source.Present loop
4547 CompSource := Perm_Tree_Maps.Get
4548 (Component (Source), Key_Source.K);
4549 CompTarget := Perm_Tree_Maps.Get
4550 (Component (Target), Key_Source.K);
4552 pragma Assert (CompSource /= null);
4553 Merge_Trees (CompTarget, CompSource);
4555 Key_Source := Perm_Tree_Maps.Get_Next_Key
4556 (Component (Source));
4561 raise Program_Error;
4568 CompTarget : Perm_Tree_Access;
4569 CompSource : Perm_Tree_Access;
4570 KeyTarget : Perm_Tree_Maps.Key_Option;
4572 -- Start of processing for Merge_Env
4575 KeyTarget := Get_First_Key (Target);
4576 -- Iterate over every tree of the environment in the target, and merge
4577 -- it with the source if there is such a similar one that exists. If
4578 -- there is none, then skip.
4579 while KeyTarget.Present loop
4581 CompSource := Get (Source, KeyTarget.K);
4582 CompTarget := Get (Target, KeyTarget.K);
4584 pragma Assert (CompTarget /= null);
4586 if CompSource /= null then
4587 Merge_Trees (CompTarget, CompSource);
4588 Remove (Source, KeyTarget.K);
4591 KeyTarget := Get_Next_Key (Target);
4594 -- Iterate over every tree of the environment of the source. And merge
4595 -- again. If there is not any tree of the target then just copy the tree
4596 -- from source to target.
4598 KeySource : Perm_Tree_Maps.Key_Option;
4600 KeySource := Get_First_Key (Source);
4601 while KeySource.Present loop
4603 CompSource := Get (Source, KeySource.K);
4604 CompTarget := Get (Target, KeySource.K);
4606 if CompTarget = null then
4607 CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
4608 Copy_Tree (CompSource, CompTarget);
4609 Set (Target, KeySource.K, CompTarget);
4611 Merge_Trees (CompTarget, CompSource);
4614 KeySource := Get_Next_Key (Source);
4625 procedure Perm_Error
4628 Found_Perm : Perm_Kind;
4630 Forbidden_Perm : Boolean := False)
4632 procedure Set_Root_Object
4634 Obj : out Entity_Id;
4635 Deref : out Boolean);
4636 -- Set the root object Obj, and whether the path contains a dereference,
4637 -- from a path Path.
4639 ---------------------
4640 -- Set_Root_Object --
4641 ---------------------
4643 procedure Set_Root_Object
4645 Obj : out Entity_Id;
4646 Deref : out Boolean)
4649 case Nkind (Path) is
4653 Obj := Entity (Path);
4656 when N_Type_Conversion
4657 | N_Unchecked_Type_Conversion
4658 | N_Qualified_Expression
4660 Set_Root_Object (Expression (Path), Obj, Deref);
4662 when N_Indexed_Component
4663 | N_Selected_Component
4666 Set_Root_Object (Prefix (Path), Obj, Deref);
4668 when N_Explicit_Dereference =>
4669 Set_Root_Object (Prefix (Path), Obj, Deref);
4673 raise Program_Error;
4675 end Set_Root_Object;
4681 -- Start of processing for Perm_Error
4684 Set_Root_Object (N, Root, Is_Deref);
4686 if Emit_Messages then
4689 ("insufficient permission on dereference from &", N, Root);
4691 Error_Msg_NE ("insufficient permission for &", N, Root);
4694 Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
4698 -------------------------------
4699 -- Perm_Error_Subprogram_End --
4700 -------------------------------
4702 procedure Perm_Error_Subprogram_End
4706 Found_Perm : Perm_Kind;
4710 if Emit_Messages then
4711 Error_Msg_Node_2 := Subp;
4712 Error_Msg_NE ("insufficient permission for & when returning from &",
4714 Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
4716 end Perm_Error_Subprogram_End;
4722 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is
4724 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id);
4725 -- Check expression Expr originating in Root was not borrowed
4727 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id);
4728 -- Check expression Expr originating in Root was not observed
4730 ------------------------
4731 -- Check_Not_Borrowed --
4732 ------------------------
4734 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is
4736 -- An expression without root object cannot be borrowed
4742 -- Otherwise, try to match the expression with one of the borrowed
4746 Key : Variable_Maps.Key_Option :=
4747 Get_First_Key (Current_Borrowers);
4752 while Key.Present loop
4754 Borrowed := Get (Current_Borrowers, Var);
4756 if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
4757 and then Emit_Messages
4759 Error_Msg_Sloc := Sloc (Borrowed);
4760 Error_Msg_N ("object was borrowed #", Expr);
4763 Key := Get_Next_Key (Current_Borrowers);
4766 end Check_Not_Borrowed;
4768 ------------------------
4769 -- Check_Not_Observed --
4770 ------------------------
4772 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is
4774 -- An expression without root object cannot be observed
4780 -- Otherwise, try to match the expression with one of the observed
4784 Key : Variable_Maps.Key_Option :=
4785 Get_First_Key (Current_Observers);
4790 while Key.Present loop
4792 Observed := Get (Current_Observers, Var);
4794 if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr)
4795 and then Emit_Messages
4797 Error_Msg_Sloc := Sloc (Observed);
4798 Error_Msg_N ("object was observed #", Expr);
4801 Key := Get_Next_Key (Current_Observers);
4804 end Check_Not_Observed;
4808 Expr_Type : constant Entity_Id := Etype (Expr);
4809 Root : Entity_Id := Get_Root_Object (Expr);
4810 Perm : Perm_Kind_Option;
4812 -- Start of processing for Process_Path
4815 -- Nothing to do if the root type is not deep, or the path is not rooted
4818 if not Present (Root)
4819 or else not Is_Deep (Etype (Root))
4824 -- Identify the root type for the path
4826 Root := Unique_Entity (Root);
4828 -- Except during elaboration, the root object should have been declared
4829 -- and entered into the current permission environment.
4831 if not Inside_Elaboration
4832 and then Get (Current_Perm_Env, Root) = null
4834 Illegal_Global_Usage (Expr, Root);
4837 -- During elaboration, only the validity of operations is checked, no
4838 -- need to compute the permission of Expr.
4840 if Inside_Elaboration then
4843 Perm := Get_Perm (Expr);
4846 -- Check permissions
4852 -- No checking needed during elaboration
4854 if Inside_Elaboration then
4858 -- Check path is readable
4860 if Perm not in Read_Perm then
4861 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
4867 -- Forbidden on deep path during elaboration, otherwise no
4870 if Inside_Elaboration then
4871 if Is_Deep (Expr_Type)
4872 and then not Inside_Procedure_Call
4873 and then Present (Get_Root_Object (Expr))
4874 and then Emit_Messages
4876 Error_Msg_N ("illegal move during elaboration", Expr);
4882 -- For deep path, check RW permission, otherwise R permission
4884 if not Is_Deep (Expr_Type) then
4885 if Perm not in Read_Perm then
4886 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
4891 -- SPARK RM 3.10(1): At the point of a move operation the state of
4892 -- the source object (if any) shall be Unrestricted.
4894 if Perm /= Read_Write then
4895 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
4901 -- No checking needed during elaboration
4903 if Inside_Elaboration then
4907 -- For assignment, check W permission
4909 if Perm not in Write_Perm then
4910 Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr));
4916 -- Forbidden during elaboration, an error is already issued in
4917 -- Check_Declaration, just return.
4919 if Inside_Elaboration then
4923 -- For borrowing, check RW permission
4925 if Perm /= Read_Write then
4926 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
4932 -- Forbidden during elaboration, an error is already issued in
4933 -- Check_Declaration, just return.
4935 if Inside_Elaboration then
4939 -- For borrowing, check R permission
4941 if Perm not in Read_Perm then
4942 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
4947 -- Check path was not borrowed
4949 Check_Not_Borrowed (Expr, Root);
4951 -- For modes that require W permission, check path was not observed
4954 when Read | Observe =>
4956 when Assign | Move | Borrow =>
4957 Check_Not_Observed (Expr, Root);
4960 -- Do not update permission environment when handling calls
4962 if Inside_Procedure_Call then
4966 -- Update the permissions
4975 -- SPARK RM 3.10(1): After a move operation, the state of the
4976 -- source object (if any) becomes Moved.
4978 if Present (Get_Root_Object (Expr)) then
4980 Tree : constant Perm_Tree_Access :=
4981 Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr);
4983 pragma Assert (Tree /= null);
4984 Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr);
4990 -- If there is no root object, or the tree has an array component,
4991 -- then the permissions do not get modified by the assignment.
4993 if No (Get_Root_Object (Expr))
4994 or else Has_Array_Component (Expr)
4999 -- Set permission RW for the path and its extensions
5002 Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr);
5004 Tree.all.Tree.Permission := Read_Write;
5005 Set_Perm_Extensions (Tree, Read_Write, Expl => Expr);
5007 -- Normalize the permission tree
5009 Set_Perm_Prefixes_Assign (Expr);
5012 -- Borrowing and observing of paths is handled by the variables
5013 -- Current_Borrowers and Current_Observers.
5015 when Borrow | Observe =>
5020 --------------------
5021 -- Return_Globals --
5022 --------------------
5024 procedure Return_Globals (Subp : Entity_Id) is
5026 procedure Return_Global
5031 Global_Var : Boolean);
5032 -- Proxy procedure to return globals, to adjust for the type of first
5033 -- parameter expected by Return_Parameter_Or_Global.
5039 procedure Return_Global
5044 Global_Var : Boolean)
5047 Return_Parameter_Or_Global
5048 (Id => Entity (Expr),
5052 Global_Var => Global_Var);
5055 procedure Return_Globals_Inst is new Handle_Globals (Return_Global);
5057 -- Start of processing for Return_Globals
5060 Return_Globals_Inst (Subp);
5063 --------------------------------
5064 -- Return_Parameter_Or_Global --
5065 --------------------------------
5067 procedure Return_Parameter_Or_Global
5072 Global_Var : Boolean)
5075 -- Shallow parameters and globals need not be considered
5077 if not Is_Deep (Typ) then
5080 elsif Kind = E_In_Parameter then
5082 -- Input global variables are observed only
5087 -- Anonymous access to constant is an observe
5089 elsif Is_Anonymous_Access_Type (Typ)
5090 and then Is_Access_Constant (Typ)
5094 -- Deep types other than access types define an observe
5096 elsif not Is_Access_Type (Typ) then
5101 -- All other parameters and globals should return with mode RW to the
5105 Tree : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
5107 if Permission (Tree) /= Read_Write then
5108 Perm_Error_Subprogram_End
5112 Found_Perm => Permission (Tree),
5113 Expl => Explanation (Tree));
5116 end Return_Parameter_Or_Global;
5118 -----------------------
5119 -- Return_Parameters --
5120 -----------------------
5122 procedure Return_Parameters (Subp : Entity_Id) is
5125 Formal := First_Formal (Subp);
5126 while Present (Formal) loop
5127 Return_Parameter_Or_Global
5129 Typ => Retysp (Etype (Formal)),
5130 Kind => Ekind (Formal),
5132 Global_Var => False);
5133 Next_Formal (Formal);
5135 end Return_Parameters;
5137 -------------------------
5138 -- Set_Perm_Extensions --
5139 -------------------------
5141 procedure Set_Perm_Extensions
5142 (T : Perm_Tree_Access;
5146 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
5147 -- Free the permission tree of children if any, prio to replacing T
5149 -----------------------------
5150 -- Free_Perm_Tree_Children --
5151 -----------------------------
5153 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
5156 when Entire_Object =>
5160 Free_Tree (T.all.Tree.Get_All);
5162 when Array_Component =>
5163 Free_Tree (T.all.Tree.Get_Elem);
5165 when Record_Component =>
5167 Hashtbl : Perm_Tree_Maps.Instance := Component (T);
5168 Comp : Perm_Tree_Access;
5171 Comp := Perm_Tree_Maps.Get_First (Hashtbl);
5172 while Comp /= null loop
5174 Comp := Perm_Tree_Maps.Get_Next (Hashtbl);
5177 Perm_Tree_Maps.Reset (Hashtbl);
5180 end Free_Perm_Tree_Children;
5182 -- Start of processing for Set_Perm_Extensions
5185 Free_Perm_Tree_Children (T);
5186 T.all.Tree := Perm_Tree'(Kind => Entire_Object,
5187 Is_Node_Deep => Is_Node_Deep (T),
5188 Explanation => Expl,
5189 Permission => Permission (T),
5190 Children_Permission => P);
5191 end Set_Perm_Extensions;
5193 ------------------------------
5194 -- Set_Perm_Extensions_Move --
5195 ------------------------------
5197 procedure Set_Perm_Extensions_Move
5198 (T : Perm_Tree_Access;
5202 Check_Ty : constant Entity_Id := Retysp (E);
5204 -- Shallow extensions are set to RW
5206 if not Is_Node_Deep (T) then
5207 Set_Perm_Extensions (T, Read_Write, Expl => Expl);
5211 -- Deep extensions are set to W before .all and NO afterwards
5213 T.all.Tree.Permission := Write_Only;
5215 case T.all.Tree.Kind is
5217 -- For a folded tree of composite type, unfold the tree for better
5220 when Entire_Object =>
5221 case Ekind (Check_Ty) is
5226 C : constant Perm_Tree_Access :=
5227 new Perm_Tree_Wrapper'
5229 (Kind => Entire_Object,
5230 Is_Node_Deep => Is_Node_Deep (T),
5231 Explanation => Expl,
5232 Permission => Read_Write,
5233 Children_Permission => Read_Write));
5235 Set_Perm_Extensions_Move
5236 (C, Component_Type (Check_Ty), Expl);
5237 T.all.Tree := (Kind => Array_Component,
5238 Is_Node_Deep => Is_Node_Deep (T),
5239 Explanation => Expl,
5240 Permission => Write_Only,
5246 C : Perm_Tree_Access;
5248 Hashtbl : Perm_Tree_Maps.Instance;
5251 Comp := First_Component_Or_Discriminant (Check_Ty);
5252 while Present (Comp) loop
5254 -- Unfold components which are visible in SPARK
5256 if Component_Is_Visible_In_SPARK (Comp) then
5257 C := new Perm_Tree_Wrapper'
5259 (Kind => Entire_Object,
5260 Is_Node_Deep => Is_Deep (Etype (Comp)),
5261 Explanation => Expl,
5262 Permission => Read_Write,
5263 Children_Permission => Read_Write));
5264 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5266 -- Hidden components are never deep
5269 C := new Perm_Tree_Wrapper'
5271 (Kind => Entire_Object,
5272 Is_Node_Deep => False,
5273 Explanation => Expl,
5274 Permission => Read_Write,
5275 Children_Permission => Read_Write));
5276 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5280 (Hashtbl, Original_Record_Component (Comp), C);
5281 Next_Component_Or_Discriminant (Comp);
5285 (Kind => Record_Component,
5286 Is_Node_Deep => Is_Node_Deep (T),
5287 Explanation => Expl,
5288 Permission => Write_Only,
5289 Component => Hashtbl);
5292 -- Otherwise, extensions are set to NO
5295 Set_Perm_Extensions (T, No_Access, Expl);
5299 Set_Perm_Extensions (T, No_Access, Expl);
5301 when Array_Component =>
5302 Set_Perm_Extensions_Move
5303 (Get_Elem (T), Component_Type (Check_Ty), Expl);
5305 when Record_Component =>
5307 C : Perm_Tree_Access;
5311 Comp := First_Component_Or_Discriminant (Check_Ty);
5312 while Present (Comp) loop
5313 C := Perm_Tree_Maps.Get
5314 (Component (T), Original_Record_Component (Comp));
5315 pragma Assert (C /= null);
5317 -- Move visible components
5319 if Component_Is_Visible_In_SPARK (Comp) then
5320 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5322 -- Hidden components are never deep
5325 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5328 Next_Component_Or_Discriminant (Comp);
5332 end Set_Perm_Extensions_Move;
5334 -----------------------
5335 -- Set_Perm_Prefixes --
5336 -----------------------
5338 function Set_Perm_Prefixes
5340 Perm : Perm_Kind_Option;
5341 Expl : Node_Id) return Perm_Tree_Access
5345 when N_Expanded_Name
5349 E : constant Entity_Id := Unique_Entity (Entity (N));
5350 C : constant Perm_Tree_Access := Get (Current_Perm_Env, E);
5351 pragma Assert (C /= null);
5354 if Perm /= None then
5355 C.all.Tree.Permission := Glb (Perm, Permission (C));
5361 -- For a nonterminal path, we set the permission tree of its prefix,
5362 -- and then we extract from the returned pointer the subtree and
5363 -- assign an adequate permission to it, if unfolded. If folded,
5364 -- we unroll the tree one level.
5366 when N_Explicit_Dereference =>
5368 C : constant Perm_Tree_Access :=
5369 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5370 pragma Assert (C /= null);
5371 pragma Assert (Kind (C) = Entire_Object
5372 or else Kind (C) = Reference);
5374 -- The tree is already unfolded. Replace the permission of the
5377 if Kind (C) = Reference then
5379 D : constant Perm_Tree_Access := Get_All (C);
5380 pragma Assert (D /= null);
5383 if Perm /= None then
5384 D.all.Tree.Permission := Glb (Perm, Permission (D));
5390 -- The tree is folded. Expand it.
5394 pragma Assert (Kind (C) = Entire_Object);
5396 Child_P : constant Perm_Kind := Children_Permission (C);
5397 D : constant Perm_Tree_Access :=
5398 new Perm_Tree_Wrapper'
5400 (Kind => Entire_Object,
5401 Is_Node_Deep => Is_Deep (Etype (N)),
5402 Explanation => Expl,
5403 Permission => Child_P,
5404 Children_Permission => Child_P));
5406 if Perm /= None then
5407 D.all.Tree.Permission := Perm;
5410 C.all.Tree := (Kind => Reference,
5411 Is_Node_Deep => Is_Node_Deep (C),
5412 Explanation => Expl,
5413 Permission => Permission (C),
5420 when N_Selected_Component =>
5422 C : constant Perm_Tree_Access :=
5423 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5424 pragma Assert (C /= null);
5425 pragma Assert (Kind (C) = Entire_Object
5426 or else Kind (C) = Record_Component);
5428 -- The tree is already unfolded. Replace the permission of the
5431 if Kind (C) = Record_Component then
5433 Comp : constant Entity_Id :=
5434 Original_Record_Component
5435 (Entity (Selector_Name (N)));
5436 D : constant Perm_Tree_Access :=
5437 Perm_Tree_Maps.Get (Component (C), Comp);
5438 pragma Assert (D /= null);
5441 if Perm /= None then
5442 D.all.Tree.Permission := Glb (Perm, Permission (D));
5448 -- The tree is folded. Expand it.
5452 pragma Assert (Kind (C) = Entire_Object);
5454 D : Perm_Tree_Access;
5455 D_This : Perm_Tree_Access;
5458 Child_P : constant Perm_Kind := Children_Permission (C);
5459 Hashtbl : Perm_Tree_Maps.Instance;
5460 -- Create an empty hash table
5464 First_Component_Or_Discriminant
5465 (Retysp (Etype (Prefix (N))));
5467 while Present (Comp) loop
5469 and then Original_Record_Component (Comp) =
5470 Original_Record_Component
5471 (Entity (Selector_Name (N)))
5478 D := new Perm_Tree_Wrapper'
5480 (Kind => Entire_Object,
5482 -- Hidden components are never deep
5483 Component_Is_Visible_In_SPARK (Comp)
5484 and then Is_Deep (Etype (Comp)),
5485 Explanation => Expl,
5487 Children_Permission => Child_P));
5489 (Hashtbl, Original_Record_Component (Comp), D);
5491 -- Store the tree to return for this component
5493 if Original_Record_Component (Comp) =
5494 Original_Record_Component
5495 (Entity (Selector_Name (N)))
5500 Next_Component_Or_Discriminant (Comp);
5503 C.all.Tree := (Kind => Record_Component,
5504 Is_Node_Deep => Is_Node_Deep (C),
5505 Explanation => Expl,
5506 Permission => Permission (C),
5507 Component => Hashtbl);
5513 when N_Indexed_Component
5517 C : constant Perm_Tree_Access :=
5518 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5519 pragma Assert (C /= null);
5520 pragma Assert (Kind (C) = Entire_Object
5521 or else Kind (C) = Array_Component);
5523 -- The tree is already unfolded. Replace the permission of the
5526 if Kind (C) = Array_Component then
5528 D : constant Perm_Tree_Access := Get_Elem (C);
5529 pragma Assert (D /= null);
5532 if Perm /= None then
5533 D.all.Tree.Permission := Glb (Perm, Permission (D));
5539 -- The tree is folded. Expand it.
5543 pragma Assert (Kind (C) = Entire_Object);
5545 Child_P : constant Perm_Kind := Children_Permission (C);
5546 D : constant Perm_Tree_Access :=
5547 new Perm_Tree_Wrapper'
5549 (Kind => Entire_Object,
5550 Is_Node_Deep => Is_Node_Deep (C),
5551 Explanation => Expl,
5552 Permission => Child_P,
5553 Children_Permission => Child_P));
5555 if Perm /= None then
5556 D.all.Tree.Permission := Perm;
5559 C.all.Tree := (Kind => Array_Component,
5560 Is_Node_Deep => Is_Node_Deep (C),
5561 Explanation => Expl,
5562 Permission => Permission (C),
5569 when N_Qualified_Expression
5571 | N_Unchecked_Type_Conversion
5573 return Set_Perm_Prefixes (Expression (N), Perm, Expl);
5576 raise Program_Error;
5578 end Set_Perm_Prefixes;
5580 ------------------------------
5581 -- Set_Perm_Prefixes_Assign --
5582 ------------------------------
5584 procedure Set_Perm_Prefixes_Assign (N : Node_Id) is
5585 C : constant Perm_Tree_Access := Get_Perm_Tree (N);
5589 when Entire_Object =>
5590 pragma Assert (Children_Permission (C) = Read_Write);
5591 C.all.Tree.Permission := Read_Write;
5594 C.all.Tree.Permission :=
5595 Lub (Permission (C), Permission (Get_All (C)));
5597 when Array_Component =>
5600 when Record_Component =>
5602 Comp : Perm_Tree_Access;
5603 Perm : Perm_Kind := Read_Write;
5606 -- We take the Glb of all the descendants, and then update the
5607 -- permission of the node with it.
5609 Comp := Perm_Tree_Maps.Get_First (Component (C));
5610 while Comp /= null loop
5611 Perm := Glb (Perm, Permission (Comp));
5612 Comp := Perm_Tree_Maps.Get_Next (Component (C));
5615 C.all.Tree.Permission := Lub (Permission (C), Perm);
5621 -- Base identifier end recursion
5623 when N_Expanded_Name
5628 when N_Explicit_Dereference
5629 | N_Indexed_Component
5630 | N_Selected_Component
5633 Set_Perm_Prefixes_Assign (Prefix (N));
5635 when N_Qualified_Expression
5637 | N_Unchecked_Type_Conversion
5639 Set_Perm_Prefixes_Assign (Expression (N));
5642 raise Program_Error;
5644 end Set_Perm_Prefixes_Assign;
5650 procedure Setup_Globals (Subp : Entity_Id) is
5652 procedure Setup_Global
5657 Global_Var : Boolean);
5658 -- Proxy procedure to set up globals, to adjust for the type of first
5659 -- parameter expected by Setup_Parameter_Or_Global.
5665 procedure Setup_Global
5670 Global_Var : Boolean)
5673 Setup_Parameter_Or_Global
5674 (Id => Entity (Expr),
5678 Global_Var => Global_Var,
5682 procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global);
5684 -- Start of processing for Setup_Globals
5687 Setup_Globals_Inst (Subp);
5690 -------------------------------
5691 -- Setup_Parameter_Or_Global --
5692 -------------------------------
5694 procedure Setup_Parameter_Or_Global
5699 Global_Var : Boolean;
5702 Perm : Perm_Kind_Option;
5706 when E_In_Parameter =>
5708 -- Shallow parameters and globals need not be considered
5710 if not Is_Deep (Typ) then
5713 -- Inputs of functions have R permission only
5715 elsif Ekind (Subp) = E_Function then
5718 -- Input global variables have R permission only
5720 elsif Global_Var then
5723 -- Anonymous access to constant is an observe
5725 elsif Is_Anonymous_Access_Type (Typ)
5726 and then Is_Access_Constant (Typ)
5730 -- Other access types are a borrow
5732 elsif Is_Access_Type (Typ) then
5735 -- Deep types other than access types define an observe
5741 when E_Out_Parameter
5742 | E_In_Out_Parameter
5744 -- Shallow parameters and globals need not be considered
5746 if not Is_Deep (Typ) then
5749 -- Functions cannot have outputs in SPARK
5751 elsif Ekind (Subp) = E_Function then
5754 -- Deep types define a borrow or a move
5761 if Perm /= None then
5763 Tree : constant Perm_Tree_Access :=
5764 new Perm_Tree_Wrapper'
5766 (Kind => Entire_Object,
5767 Is_Node_Deep => Is_Deep (Etype (Id)),
5768 Explanation => Expl,
5770 Children_Permission => Perm));
5772 Set (Current_Perm_Env, Id, Tree);
5775 end Setup_Parameter_Or_Global;
5777 ----------------------
5778 -- Setup_Parameters --
5779 ----------------------
5781 procedure Setup_Parameters (Subp : Entity_Id) is
5784 Formal := First_Formal (Subp);
5785 while Present (Formal) loop
5786 Setup_Parameter_Or_Global
5788 Typ => Retysp (Etype (Formal)),
5789 Kind => Ekind (Formal),
5791 Global_Var => False,
5793 Next_Formal (Formal);
5795 end Setup_Parameters;
5797 --------------------------------
5798 -- Setup_Protected_Components --
5799 --------------------------------
5801 procedure Setup_Protected_Components (Subp : Entity_Id) is
5802 Typ : constant Entity_Id := Scope (Subp);
5807 Comp := First_Component_Or_Discriminant (Typ);
5809 -- The protected object is an implicit input of protected functions, and
5810 -- an implicit input-output of protected procedures and entries.
5812 if Ekind (Subp) = E_Function then
5813 Kind := E_In_Parameter;
5815 Kind := E_In_Out_Parameter;
5818 while Present (Comp) loop
5819 Setup_Parameter_Or_Global
5821 Typ => Retysp (Etype (Comp)),
5824 Global_Var => False,
5827 Next_Component_Or_Discriminant (Comp);
5829 end Setup_Protected_Components;