]> git.ipfire.org Git - thirdparty/gcc.git/blob - gcc/ada/sem_spark.adb
[Ada] Minor reformattings
[thirdparty/gcc.git] / gcc / ada / sem_spark.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- S E M _ S P A R K --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2017-2019, Free Software Foundation, Inc. --
10 -- --
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. --
20 -- --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
23 -- --
24 ------------------------------------------------------------------------------
25
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;
31 with Opt; use Opt;
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;
39
40 with Ada.Unchecked_Deallocation;
41 with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables;
42
43 package body Sem_SPARK is
44
45 ---------------------------------------------------
46 -- Handling of Permissions Associated with Paths --
47 ---------------------------------------------------
48
49 package Permissions is
50 Elaboration_Context_Max : constant := 1009;
51 -- The hash range
52
53 type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1;
54
55 function Elaboration_Context_Hash
56 (Key : Entity_Id) return Elaboration_Context_Index;
57 -- The hash function
58
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.
68
69 type Perm_Kind_Option is
70 (None,
71 -- Special value used when no permission is passed around
72
73 No_Access,
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.
76
77 Read_Only,
78 -- The path can only be accessed for reading. This is the case for
79 -- the path of a name in the Observed state.
80
81 Read_Write,
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.
84
85 Write_Only
86 -- The path can only be accessed for writing. This is the case for
87 -- the path of a name in the Moved state.
88 );
89
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;
93
94 type Perm_Tree_Wrapper;
95
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
101 -- updated.
102
103 -- Nodes in the permission tree are of different kinds
104
105 type Path_Kind is
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
110 );
111
112 package Perm_Tree_Maps is new Simple_HTable
113 (Header_Num => Elaboration_Context_Index,
114 Key => Entity_Id,
115 Element => Perm_Tree_Access,
116 No_Element => null,
117 Hash => Elaboration_Context_Hash,
118 Equal => "=");
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).
125
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.
129
130 type Perm_Tree (Kind : Path_Kind := Entire_Object) is record
131 Permission : Perm_Kind;
132 -- Permission at this level in the path
133
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.
139
140 Explanation : Node_Id;
141 -- Node that can be used in an explanation for a permission mismatch
142
143 case Kind is
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.
150
151 when Entire_Object =>
152 Children_Permission : Perm_Kind;
153
154 -- Unfolded path of access type. The permission of the object
155 -- pointed to is given in Get_All.
156
157 when Reference =>
158 Get_All : Perm_Tree_Access;
159
160 -- Unfolded path of array type. The permission of elements is
161 -- given in Get_Elem.
162
163 when Array_Component =>
164 Get_Elem : Perm_Tree_Access;
165
166 -- Unfolded path of record type. The permission of the components
167 -- is given in Component.
168
169 when Record_Component =>
170 Component : Perm_Tree_Maps.Instance;
171 end case;
172 end record;
173
174 type Perm_Tree_Wrapper is record
175 Tree : Perm_Tree;
176 end record;
177 -- We use this wrapper in order to have unconstrained discriminants
178
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.
182
183 type Perm_Env_Access is access Perm_Env;
184 -- Access to permission environments
185
186 package Env_Maps is new Simple_HTable
187 (Header_Num => Elaboration_Context_Index,
188 Key => Entity_Id,
189 Element => Perm_Env_Access,
190 No_Element => null,
191 Hash => Elaboration_Context_Hash,
192 Equal => "=");
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.
196
197 type Env_Backups is new Env_Maps.Instance;
198 -- The type defining the hash table saving the environments at the entry
199 -- of each loop.
200
201 package Variable_Maps is new Simple_HTable
202 (Header_Num => Elaboration_Context_Index,
203 Key => Entity_Id,
204 Element => Node_Id,
205 No_Element => Empty,
206 Hash => Elaboration_Context_Hash,
207 Equal => "=");
208
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.
212
213 --------------------
214 -- Simple Getters --
215 --------------------
216
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.
220
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;
229
230 -----------------------
231 -- Memory Management --
232 -----------------------
233
234 procedure Copy_Env
235 (From : Perm_Env;
236 To : in out Perm_Env);
237 -- Procedure to copy a permission environment
238
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.
242
243 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping);
244 -- Move a variable mapping, freeing memory as needed and resetting the
245 -- source mapping.
246
247 procedure Copy_Tree (From, To : Perm_Tree_Access);
248 -- Procedure to copy a permission tree
249
250 procedure Free_Env (PE : in out Perm_Env);
251 -- Procedure to free a permission environment
252
253 procedure Free_Tree (PT : in out Perm_Tree_Access);
254 -- Procedure to free a permission tree
255
256 --------------------
257 -- Error Messages --
258 --------------------
259
260 procedure Perm_Mismatch
261 (N : Node_Id;
262 Exp_Perm : Perm_Kind;
263 Act_Perm : Perm_Kind;
264 Expl : Node_Id;
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.
269
270 end Permissions;
271
272 package body Permissions is
273
274 -------------------------
275 -- Children_Permission --
276 -------------------------
277
278 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is
279 begin
280 return T.all.Tree.Children_Permission;
281 end Children_Permission;
282
283 ---------------
284 -- Component --
285 ---------------
286
287 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance
288 is
289 begin
290 return T.all.Tree.Component;
291 end Component;
292
293 --------------
294 -- Copy_Env --
295 --------------
296
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;
301
302 begin
303 Free_Env (To);
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);
308
309 Son := new Perm_Tree_Wrapper;
310 Copy_Tree (Comp_From, Son);
311
312 Set (To, Key_From.K, Son);
313 Key_From := Get_Next_Key (From);
314 end loop;
315 end Copy_Env;
316
317 ---------------
318 -- Copy_Tree --
319 ---------------
320
321 procedure Copy_Tree (From, To : Perm_Tree_Access) is
322 begin
323 -- Copy the direct components of the tree
324
325 To.all := From.all;
326
327 -- Now reallocate access components for a deep copy of the tree
328
329 case Kind (From) is
330 when Entire_Object =>
331 null;
332
333 when Reference =>
334 To.all.Tree.Get_All := new Perm_Tree_Wrapper;
335 Copy_Tree (Get_All (From), Get_All (To));
336
337 when Array_Component =>
338 To.all.Tree.Get_Elem := new Perm_Tree_Wrapper;
339 Copy_Tree (Get_Elem (From), Get_Elem (To));
340
341 when Record_Component =>
342 declare
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;
347 begin
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
352 (Component (From));
353
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);
360 Perm_Tree_Maps.Set
361 (To.all.Tree.Component, Key_From.K, Son);
362 Key_From := Perm_Tree_Maps.Get_Next_Key
363 (Component (From));
364 end loop;
365 end;
366 end case;
367 end Copy_Tree;
368
369 ------------------------------
370 -- Elaboration_Context_Hash --
371 ------------------------------
372
373 function Elaboration_Context_Hash
374 (Key : Entity_Id) return Elaboration_Context_Index
375 is
376 begin
377 return Elaboration_Context_Index (Key mod Elaboration_Context_Max);
378 end Elaboration_Context_Hash;
379
380 --------------
381 -- Free_Env --
382 --------------
383
384 procedure Free_Env (PE : in out Perm_Env) is
385 CompO : Perm_Tree_Access;
386 begin
387 CompO := Get_First (PE);
388 while CompO /= null loop
389 Free_Tree (CompO);
390 CompO := Get_Next (PE);
391 end loop;
392
393 Reset (PE);
394 end Free_Env;
395
396 ---------------
397 -- Free_Tree --
398 ---------------
399
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
405
406 begin
407 case Kind (PT) is
408 when Entire_Object =>
409 null;
410
411 when Reference =>
412 Free_Tree (PT.all.Tree.Get_All);
413
414 when Array_Component =>
415 Free_Tree (PT.all.Tree.Get_Elem);
416
417 when Record_Component =>
418 declare
419 Comp : Perm_Tree_Access;
420
421 begin
422 Comp := Perm_Tree_Maps.Get_First (Component (PT));
423 while Comp /= null loop
424
425 -- Free every Component subtree
426
427 Free_Tree (Comp);
428 Comp := Perm_Tree_Maps.Get_Next (Component (PT));
429 end loop;
430 end;
431 end case;
432
433 Free_Perm_Tree_Dealloc (PT);
434 end Free_Tree;
435
436 -----------------
437 -- Explanation --
438 -----------------
439
440 function Explanation (T : Perm_Tree_Access) return Node_Id is
441 begin
442 return T.all.Tree.Explanation;
443 end Explanation;
444
445 -------------
446 -- Get_All --
447 -------------
448
449 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is
450 begin
451 return T.all.Tree.Get_All;
452 end Get_All;
453
454 --------------
455 -- Get_Elem --
456 --------------
457
458 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is
459 begin
460 return T.all.Tree.Get_Elem;
461 end Get_Elem;
462
463 ------------------
464 -- Is_Node_Deep --
465 ------------------
466
467 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is
468 begin
469 return T.all.Tree.Is_Node_Deep;
470 end Is_Node_Deep;
471
472 ----------
473 -- Kind --
474 ----------
475
476 function Kind (T : Perm_Tree_Access) return Path_Kind is
477 begin
478 return T.all.Tree.Kind;
479 end Kind;
480
481 --------------
482 -- Move_Env --
483 --------------
484
485 procedure Move_Env (From, To : in out Perm_Env) is
486 begin
487 Free_Env (To);
488 To := From;
489 From := Perm_Env (Perm_Tree_Maps.Nil);
490 end Move_Env;
491
492 ---------------------------
493 -- Move_Variable_Mapping --
494 ---------------------------
495
496 procedure Move_Variable_Mapping (From, To : in out Variable_Mapping) is
497 begin
498 Reset (To);
499 To := From;
500 From := Variable_Mapping (Variable_Maps.Nil);
501 end Move_Variable_Mapping;
502
503 ----------------
504 -- Permission --
505 ----------------
506
507 function Permission (T : Perm_Tree_Access) return Perm_Kind is
508 begin
509 return T.all.Tree.Permission;
510 end Permission;
511
512 -------------------
513 -- Perm_Mismatch --
514 -------------------
515
516 procedure Perm_Mismatch
517 (N : Node_Id;
518 Exp_Perm : Perm_Kind;
519 Act_Perm : Perm_Kind;
520 Expl : Node_Id;
521 Forbidden_Perm : Boolean := False)
522 is
523 begin
524 Error_Msg_Sloc := Sloc (Expl);
525
526 if Forbidden_Perm then
527 if Exp_Perm = No_Access then
528 Error_Msg_N ("\object was moved #", N);
529 else
530 raise Program_Error;
531 end if;
532 else
533 case Exp_Perm is
534 when Write_Perm =>
535 if Act_Perm = Read_Only then
536 Error_Msg_N
537 ("\object was declared as not writeable #", N);
538 else
539 Error_Msg_N ("\object was moved #", N);
540 end if;
541
542 when Read_Only =>
543 Error_Msg_N ("\object was moved #", N);
544
545 when No_Access =>
546 raise Program_Error;
547 end case;
548 end if;
549 end Perm_Mismatch;
550
551 end Permissions;
552
553 use Permissions;
554
555 --------------------------------------
556 -- Analysis modes for AST traversal --
557 --------------------------------------
558
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.
562
563 type Extended_Checking_Mode is
564
565 (Read_Subexpr,
566 -- Special value used for assignment, to check that subexpressions of
567 -- the assigned path are readable.
568
569 Read,
570 -- Default mode
571
572 Move,
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
576 -- No_Access.
577
578 Assign,
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).
586
587 Borrow,
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.
591
592 Observe
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.
596 );
597
598 subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe;
599
600 type Result_Kind is (Folded, Unfolded);
601 -- The type declaration to discriminate in the Perm_Or_Tree type
602
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.
607
608 type Perm_Or_Tree (R : Result_Kind) is record
609 case R is
610 when Folded =>
611 Found_Permission : Perm_Kind;
612 Explanation : Node_Id;
613 when Unfolded =>
614 Tree_Access : Perm_Tree_Access;
615 end case;
616 end record;
617
618 type Error_Status is (OK, Error);
619
620 -----------------------
621 -- Local subprograms --
622 -----------------------
623
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;
628
629 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id);
630 -- Handle assignment as part of an assignment statement or an object
631 -- declaration.
632
633 procedure Check_Call_Statement (Call : Node_Id);
634
635 procedure Check_Callable_Body (Body_N : Node_Id);
636 -- Entry point for the analysis of a subprogram or entry body
637
638 procedure Check_Declaration (Decl : Node_Id);
639
640 procedure Check_Declaration_Legality
641 (Decl : Node_Id;
642 Force : Boolean;
643 Legal : in out Boolean);
644 -- Check the legality of declaration Decl regarding rules not related to
645 -- permissions. Update Legal to False if a rule is violated. Issue an
646 -- error message if Force is True and Emit_Messages returns True.
647
648 procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
649 pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
650 N_Range_Constraint,
651 N_Subtype_Indication,
652 N_Digits_Constraint,
653 N_Delta_Constraint)
654 or else Nkind (Expr) in N_Subexpr);
655
656 procedure Check_Globals (Subp : Entity_Id);
657 -- This procedure takes a subprogram called and checks the permission of
658 -- globals.
659
660 -- Checking proceduress for safe pointer usage. These procedures traverse
661 -- the AST, check nodes for correct permissions according to SPARK RM 3.10,
662 -- and update permissions depending on the node kind. The main procedure
663 -- Check_Node is mutually recursive with the specialized procedures that
664 -- follow.
665
666 procedure Check_List (L : List_Id);
667 -- Calls Check_Node on each element of the list
668
669 procedure Check_Loop_Statement (Stmt : Node_Id);
670
671 procedure Check_Node (N : Node_Id);
672 -- Main traversal procedure to check safe pointer usage
673
674 procedure Check_Old_Loop_Entry (N : Node_Id);
675 -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
676
677 procedure Check_Package_Body (Pack : Node_Id);
678
679 procedure Check_Package_Spec (Pack : Node_Id);
680
681 procedure Check_Parameter_Or_Global
682 (Expr : Node_Id;
683 Typ : Entity_Id;
684 Kind : Formal_Kind;
685 Subp : Entity_Id;
686 Global_Var : Boolean);
687 -- Check the permission of every actual parameter or global
688
689 procedure Check_Pragma (Prag : Node_Id);
690
691 procedure Check_Source_Of_Borrow_Or_Observe
692 (Expr : Node_Id;
693 Status : out Error_Status);
694
695 procedure Check_Statement (Stmt : Node_Id);
696
697 procedure Check_Type_Legality
698 (Typ : Entity_Id;
699 Force : Boolean;
700 Legal : in out Boolean);
701 -- Check that type Typ is either not deep, or that it is an observing or
702 -- owning type according to SPARK RM 3.10
703
704 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id;
705 -- The function that takes a name as input and returns an explanation node
706 -- for the permission associated with it.
707
708 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id;
709 pragma Precondition (Is_Path_Expression (Expr));
710 -- Return the expression being borrowed/observed when borrowing or
711 -- observing Expr. If Expr is a call to a traversal function, this is
712 -- the first actual, otherwise it is Expr.
713
714 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind;
715 -- The function that takes a name as input and returns a permission
716 -- associated with it.
717
718 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree;
719 pragma Precondition (Is_Path_Expression (N));
720 -- This function gets a node and looks recursively to find the appropriate
721 -- subtree for that node. If the tree is folded on that node, then it
722 -- returns the permission given at the right level.
723
724 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access;
725 pragma Precondition (Is_Path_Expression (N));
726 -- This function gets a node and looks recursively to find the appropriate
727 -- subtree for that node. If the tree is folded, then it unrolls the tree
728 -- up to the appropriate level.
729
730 function Get_Root_Object
731 (Expr : Node_Id;
732 Through_Traversal : Boolean := True;
733 Is_Traversal : Boolean := False) return Entity_Id;
734 -- Return the root of the path expression Expr, or Empty for an allocator,
735 -- NULL, or a function call. Through_Traversal is True if it should follow
736 -- through calls to traversal functions. Is_Traversal is True if this
737 -- corresponds to a value returned from a traversal function, which should
738 -- allow if-expressions and case-expressions that refer to the same root,
739 -- even if the paths are not the same in all branches.
740
741 generic
742 with procedure Handle_Parameter_Or_Global
743 (Expr : Node_Id;
744 Formal_Typ : Entity_Id;
745 Param_Mode : Formal_Kind;
746 Subp : Entity_Id;
747 Global_Var : Boolean);
748 procedure Handle_Globals (Subp : Entity_Id);
749 -- Handling of globals is factored in a generic instantiated below
750
751 function Has_Array_Component (Expr : Node_Id) return Boolean;
752 pragma Precondition (Is_Path_Expression (Expr));
753 -- This function gets a node and looks recursively to determine whether the
754 -- given path has any array component.
755
756 procedure Hp (P : Perm_Env);
757 -- A procedure that outputs the hash table. This function is used only in
758 -- the debugger to look into a hash table.
759 pragma Unreferenced (Hp);
760
761 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id);
762 pragma No_Return (Illegal_Global_Usage);
763 -- A procedure that is called when deep globals or aliased globals are used
764 -- without any global aspect.
765
766 function Is_Path_Expression
767 (Expr : Node_Id;
768 Is_Traversal : Boolean := False) return Boolean;
769 -- Return whether Expr corresponds to a path. Is_Traversal is True if this
770 -- corresponds to a value returned from a traversal function, which should
771 -- allow if-expressions and case-expressions.
772
773 function Is_Subpath_Expression
774 (Expr : Node_Id;
775 Is_Traversal : Boolean := False) return Boolean;
776 -- Return True if Expr can be part of a path expression. Is_Traversal is
777 -- True if this corresponds to a value returned from a traversal function,
778 -- which should allow if-expressions and case-expressions.
779
780 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean;
781 -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost
782 -- a prefix, in the sense that they could still refer to overlapping memory
783 -- locations.
784
785 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean;
786
787 function Loop_Of_Exit (N : Node_Id) return Entity_Id;
788 -- A function that takes an exit statement node and returns the entity of
789 -- the loop that this statement is exiting from.
790
791 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env);
792 -- Merge Target and Source into Target, and then deallocate the Source
793
794 procedure Perm_Error
795 (N : Node_Id;
796 Perm : Perm_Kind;
797 Found_Perm : Perm_Kind;
798 Expl : Node_Id;
799 Forbidden_Perm : Boolean := False);
800 -- A procedure that is called when the permissions found contradict the
801 -- rules established by the RM. This function is called with the node and
802 -- the permission that was expected, and issues an error message with the
803 -- appropriate values.
804
805 procedure Perm_Error_Subprogram_End
806 (E : Entity_Id;
807 Subp : Entity_Id;
808 Perm : Perm_Kind;
809 Found_Perm : Perm_Kind;
810 Expl : Node_Id);
811 -- A procedure that is called when the permissions found contradict the
812 -- rules established by the RM at the end of subprograms. This function is
813 -- called with the node, the node of the returning function, and the
814 -- permission that was expected, and adds an error message with the
815 -- appropriate values.
816
817 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode);
818 pragma Precondition (Is_Path_Expression (Expr));
819 -- Check correct permission for the path in the checking mode Mode, and
820 -- update permissions of the path and its prefixes/extensions.
821
822 procedure Return_Globals (Subp : Entity_Id);
823 -- Takes a subprogram as input, and checks that all borrowed global items
824 -- of the subprogram indeed have Read_Write permission at the end of the
825 -- subprogram execution.
826
827 procedure Return_Parameter_Or_Global
828 (Id : Entity_Id;
829 Typ : Entity_Id;
830 Kind : Formal_Kind;
831 Subp : Entity_Id;
832 Global_Var : Boolean);
833 -- Auxiliary procedure to Return_Parameters and Return_Globals
834
835 procedure Return_Parameters (Subp : Entity_Id);
836 -- Takes a subprogram as input, and checks that all out parameters of the
837 -- subprogram indeed have Read_Write permission at the end of the
838 -- subprogram execution.
839
840 procedure Set_Perm_Extensions
841 (T : Perm_Tree_Access;
842 P : Perm_Kind;
843 Expl : Node_Id);
844 -- This procedure takes an access to a permission tree and modifies the
845 -- tree so that any strict extensions of the given tree become of the
846 -- access specified by parameter P.
847
848 procedure Set_Perm_Extensions_Move
849 (T : Perm_Tree_Access;
850 E : Entity_Id;
851 Expl : Node_Id);
852 -- Set permissions to
853 -- No for any extension with more .all
854 -- W for any deep extension with same number of .all
855 -- RW for any shallow extension with same number of .all
856
857 function Set_Perm_Prefixes
858 (N : Node_Id;
859 Perm : Perm_Kind_Option;
860 Expl : Node_Id) return Perm_Tree_Access;
861 pragma Precondition (Is_Path_Expression (N));
862 -- This function modifies the permissions of a given node in the permission
863 -- environment as well as all the prefixes of the path, to the new
864 -- permission Perm. The general rule here is that everybody updates the
865 -- permission of the subtree they are returning.
866
867 procedure Set_Perm_Prefixes_Assign (N : Node_Id);
868 pragma Precondition (Is_Path_Expression (N));
869 -- This procedure takes a name as an input and sets in the permission
870 -- tree the given permission to the given name. The general rule here is
871 -- that everybody updates the permission of the subtree it is returning.
872 -- The permission of the assigned path has been set to RW by the caller.
873 --
874 -- Case where we have to normalize a tree after the correct permissions
875 -- have been assigned already. We look for the right subtree at the given
876 -- path, actualize its permissions, and then call the normalization on its
877 -- parent.
878 --
879 -- Example: We assign x.y and x.z, and then Set_Perm_Prefixes_Assign will
880 -- change the permission of x to RW because all of its components have
881 -- permission RW.
882
883 procedure Setup_Globals (Subp : Entity_Id);
884 -- Takes a subprogram as input, and sets up the environment by adding
885 -- global items with appropriate permissions.
886
887 procedure Setup_Parameter_Or_Global
888 (Id : Entity_Id;
889 Typ : Entity_Id;
890 Kind : Formal_Kind;
891 Subp : Entity_Id;
892 Global_Var : Boolean;
893 Expl : Node_Id);
894 -- Auxiliary procedure to Setup_Parameters and Setup_Globals
895
896 procedure Setup_Parameters (Subp : Entity_Id);
897 -- Takes a subprogram as input, and sets up the environment by adding
898 -- formal parameters with appropriate permissions.
899
900 procedure Setup_Protected_Components (Subp : Entity_Id);
901 -- Takes a protected operation as input, and sets up the environment by
902 -- adding protected components with appropriate permissions.
903
904 ----------------------
905 -- Global Variables --
906 ----------------------
907
908 Current_Perm_Env : Perm_Env;
909 -- The permission environment that is used for the analysis. This
910 -- environment can be saved, modified, reinitialized, but should be the
911 -- only one valid from which to extract the permissions of the paths in
912 -- scope. The analysis ensures at each point that this variables contains
913 -- a valid permission environment with all bindings in scope.
914
915 Inside_Procedure_Call : Boolean := False;
916 -- Set while checking the actual parameters of a procedure or entry call
917
918 Inside_Elaboration : Boolean := False;
919 -- Set during package spec/body elaboration, during which move and local
920 -- observe/borrow are not allowed. As a result, no other checking is needed
921 -- during elaboration.
922
923 Current_Loops_Envs : Env_Backups;
924 -- This variable contains saves of permission environments at each loop the
925 -- analysis entered. Each saved environment can be reached with the label
926 -- of the loop.
927
928 Current_Loops_Accumulators : Env_Backups;
929 -- This variable contains the environments used as accumulators for loops,
930 -- that consist of the merge of all environments at each exit point of
931 -- the loop (which can also be the entry point of the loop in the case of
932 -- non-infinite loops), each of them reachable from the label of the loop.
933 -- We require that the environment stored in the accumulator be less
934 -- restrictive than the saved environment at the beginning of the loop, and
935 -- the permission environment after the loop is equal to the accumulator.
936
937 Current_Borrowers : Variable_Mapping;
938 -- Mapping from borrowers to the path borrowed
939
940 Current_Observers : Variable_Mapping;
941 -- Mapping from observers to the path observed
942
943 --------------------
944 -- Handle_Globals --
945 --------------------
946
947 -- Generic procedure is defined first so that instantiations can be defined
948 -- anywhere afterwards.
949
950 procedure Handle_Globals (Subp : Entity_Id) is
951
952 -- Local subprograms
953
954 procedure Handle_Globals_From_List
955 (First_Item : Node_Id;
956 Kind : Formal_Kind);
957 -- Handle global items from the list starting at Item
958
959 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id);
960 -- Handle global items for the mode Global_Mode
961
962 ------------------------------
963 -- Handle_Globals_From_List --
964 ------------------------------
965
966 procedure Handle_Globals_From_List
967 (First_Item : Node_Id;
968 Kind : Formal_Kind)
969 is
970 Item : Node_Id := First_Item;
971 E : Entity_Id;
972
973 begin
974 while Present (Item) loop
975 E := Entity (Item);
976
977 -- Ignore abstract states, which play no role in pointer aliasing
978
979 if Ekind (E) = E_Abstract_State then
980 null;
981 else
982 Handle_Parameter_Or_Global (Expr => Item,
983 Formal_Typ => Retysp (Etype (Item)),
984 Param_Mode => Kind,
985 Subp => Subp,
986 Global_Var => True);
987 end if;
988
989 Next_Global (Item);
990 end loop;
991 end Handle_Globals_From_List;
992
993 ----------------------------
994 -- Handle_Globals_Of_Mode --
995 ----------------------------
996
997 procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id) is
998 Kind : Formal_Kind;
999
1000 begin
1001 case Global_Mode is
1002 when Name_Input
1003 | Name_Proof_In
1004 =>
1005 Kind := E_In_Parameter;
1006
1007 when Name_Output =>
1008 Kind := E_Out_Parameter;
1009
1010 when Name_In_Out =>
1011 Kind := E_In_Out_Parameter;
1012
1013 when others =>
1014 raise Program_Error;
1015 end case;
1016
1017 -- Check both global items from Global and Refined_Global pragmas
1018
1019 Handle_Globals_From_List (First_Global (Subp, Global_Mode), Kind);
1020 Handle_Globals_From_List
1021 (First_Global (Subp, Global_Mode, Refined => True), Kind);
1022 end Handle_Globals_Of_Mode;
1023
1024 -- Start of processing for Handle_Globals
1025
1026 begin
1027 Handle_Globals_Of_Mode (Name_Proof_In);
1028 Handle_Globals_Of_Mode (Name_Input);
1029 Handle_Globals_Of_Mode (Name_Output);
1030 Handle_Globals_Of_Mode (Name_In_Out);
1031 end Handle_Globals;
1032
1033 ----------
1034 -- "<=" --
1035 ----------
1036
1037 function "<=" (P1, P2 : Perm_Kind) return Boolean is
1038 begin
1039 return P2 >= P1;
1040 end "<=";
1041
1042 ----------
1043 -- ">=" --
1044 ----------
1045
1046 function ">=" (P1, P2 : Perm_Kind) return Boolean is
1047 begin
1048 case P2 is
1049 when No_Access => return True;
1050 when Read_Only => return P1 in Read_Perm;
1051 when Write_Only => return P1 in Write_Perm;
1052 when Read_Write => return P1 = Read_Write;
1053 end case;
1054 end ">=";
1055
1056 ----------------------
1057 -- Check_Assignment --
1058 ----------------------
1059
1060 procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is
1061
1062 -- Local subprograms
1063
1064 procedure Handle_Borrow
1065 (Var : Entity_Id;
1066 Expr : Node_Id;
1067 Is_Decl : Boolean);
1068 -- Update map of current borrowers
1069
1070 procedure Handle_Observe
1071 (Var : Entity_Id;
1072 Expr : Node_Id;
1073 Is_Decl : Boolean);
1074 -- Update map of current observers
1075
1076 -------------------
1077 -- Handle_Borrow --
1078 -------------------
1079
1080 procedure Handle_Borrow
1081 (Var : Entity_Id;
1082 Expr : Node_Id;
1083 Is_Decl : Boolean)
1084 is
1085 Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1086
1087 begin
1088 -- SPARK RM 3.10(8): If the type of the target is an anonymous
1089 -- access-to-variable type (an owning access type), the source shall
1090 -- be an owning access object [..] whose root object is the target
1091 -- object itself.
1092
1093 -- ??? In fact we could be slightly more permissive in allowing even
1094 -- a call to a traversal function of the right form.
1095
1096 if not Is_Decl
1097 and then (Is_Traversal_Function_Call (Expr)
1098 or else Get_Root_Object (Borrowed) /= Var)
1099 then
1100 if Emit_Messages then
1101 Error_Msg_NE
1102 ("source of assignment must have & as root" &
1103 " (SPARK RM 3.10(8)))",
1104 Expr, Var);
1105 end if;
1106 return;
1107 end if;
1108
1109 Set (Current_Borrowers, Var, Borrowed);
1110 end Handle_Borrow;
1111
1112 --------------------
1113 -- Handle_Observe --
1114 --------------------
1115
1116 procedure Handle_Observe
1117 (Var : Entity_Id;
1118 Expr : Node_Id;
1119 Is_Decl : Boolean)
1120 is
1121 Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr);
1122
1123 begin
1124 -- ??? We are currently using the same restriction for observers
1125 -- as for borrowers. To be seen if the SPARK RM current rule really
1126 -- allows more uses.
1127
1128 if not Is_Decl
1129 and then (Is_Traversal_Function_Call (Expr)
1130 or else Get_Root_Object (Observed) /= Var)
1131 then
1132 if Emit_Messages then
1133 Error_Msg_NE
1134 ("source of assignment must have & as root" &
1135 " (SPARK RM 3.10(8)))",
1136 Expr, Var);
1137 end if;
1138 return;
1139 end if;
1140
1141 Set (Current_Observers, Var, Observed);
1142 end Handle_Observe;
1143
1144 -- Local variables
1145
1146 Target_Typ : constant Node_Id := Etype (Target);
1147 Is_Decl : constant Boolean := Nkind (Target) = N_Defining_Identifier;
1148 Target_Root : Entity_Id;
1149 Expr_Root : Entity_Id;
1150 Perm : Perm_Kind;
1151 Status : Error_Status;
1152 Dummy : Boolean := True;
1153
1154 -- Start of processing for Check_Assignment
1155
1156 begin
1157 Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
1158
1159 if Is_Anonymous_Access_Type (Target_Typ) then
1160 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
1161
1162 if Status /= OK then
1163 return;
1164 end if;
1165
1166 if Is_Decl then
1167 Target_Root := Target;
1168 else
1169 Target_Root := Get_Root_Object (Target);
1170 end if;
1171
1172 Expr_Root := Get_Root_Object (Expr);
1173
1174 -- SPARK RM 3.10(7): For an assignment statement where the target is
1175 -- a stand-alone object of an anonymous access-to-object type.
1176
1177 pragma Assert (Present (Target_Root));
1178
1179 -- If the type of the target is an anonymous access-to-constant type
1180 -- (an observing access type), the source shall be an owning access
1181 -- object denoted by a name that is not in the Moved state, and whose
1182 -- root object is not in the Moved state and is not declared at a
1183 -- statically deeper accessibility level than that of the target
1184 -- object.
1185
1186 if Is_Access_Constant (Target_Typ) then
1187 Perm := Get_Perm (Expr);
1188
1189 if Perm = No_Access then
1190 Perm_Error (Expr, No_Access, No_Access,
1191 Expl => Get_Expl (Expr),
1192 Forbidden_Perm => True);
1193 return;
1194 end if;
1195
1196 Perm := Get_Perm (Expr_Root);
1197
1198 if Perm = No_Access then
1199 Perm_Error (Expr, No_Access, No_Access,
1200 Expl => Get_Expl (Expr_Root),
1201 Forbidden_Perm => True);
1202 return;
1203 end if;
1204
1205 -- ??? check accessibility level
1206
1207 -- If the type of the target is an anonymous access-to-variable
1208 -- type (an owning access type), the source shall be an owning
1209 -- access object denoted by a name that is in the Unrestricted
1210 -- state, and whose root object is the target object itself.
1211
1212 Check_Expression (Expr, Observe);
1213 Handle_Observe (Target_Root, Expr, Is_Decl);
1214
1215 else
1216 Perm := Get_Perm (Expr);
1217
1218 if Perm /= Read_Write then
1219 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
1220 return;
1221 end if;
1222
1223 if not Is_Decl then
1224 if not Is_Entity_Name (Target) then
1225 if Emit_Messages then
1226 Error_Msg_N
1227 ("target of borrow must be stand-alone variable",
1228 Target);
1229 end if;
1230 return;
1231
1232 elsif Target_Root /= Expr_Root then
1233 if Emit_Messages then
1234 Error_Msg_NE
1235 ("source of borrow must be variable &",
1236 Expr, Target);
1237 end if;
1238 return;
1239 end if;
1240 end if;
1241
1242 Check_Expression (Expr, Borrow);
1243 Handle_Borrow (Target_Root, Expr, Is_Decl);
1244 end if;
1245
1246 elsif Is_Deep (Target_Typ) then
1247
1248 if Is_Path_Expression (Expr) then
1249 Check_Expression (Expr, Move);
1250
1251 else
1252 if Emit_Messages then
1253 Error_Msg_N ("expression not allowed as source of move", Expr);
1254 end if;
1255 return;
1256 end if;
1257
1258 else
1259 Check_Expression (Expr, Read);
1260 end if;
1261 end Check_Assignment;
1262
1263 --------------------------
1264 -- Check_Call_Statement --
1265 --------------------------
1266
1267 procedure Check_Call_Statement (Call : Node_Id) is
1268
1269 Subp : constant Entity_Id := Get_Called_Entity (Call);
1270
1271 -- Local subprograms
1272
1273 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id);
1274 -- Check the permission of every actual parameter
1275
1276 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id);
1277 -- Update the permission of OUT actual parameters
1278
1279 -----------------
1280 -- Check_Param --
1281 -----------------
1282
1283 procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is
1284 begin
1285 Check_Parameter_Or_Global
1286 (Expr => Actual,
1287 Typ => Retysp (Etype (Formal)),
1288 Kind => Ekind (Formal),
1289 Subp => Subp,
1290 Global_Var => False);
1291 end Check_Param;
1292
1293 ------------------
1294 -- Update_Param --
1295 ------------------
1296
1297 procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is
1298 Mode : constant Entity_Kind := Ekind (Formal);
1299
1300 begin
1301 case Formal_Kind'(Mode) is
1302 when E_Out_Parameter =>
1303 Check_Expression (Actual, Assign);
1304
1305 when others =>
1306 null;
1307 end case;
1308 end Update_Param;
1309
1310 procedure Check_Params is new
1311 Iterate_Call_Parameters (Check_Param);
1312
1313 procedure Update_Params is new
1314 Iterate_Call_Parameters (Update_Param);
1315
1316 -- Start of processing for Check_Call_Statement
1317
1318 begin
1319 Inside_Procedure_Call := True;
1320 Check_Params (Call);
1321 if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then
1322 if Emit_Messages then
1323 Error_Msg_N
1324 ("call through access to subprogram is not allowed in SPARK",
1325 Call);
1326 end if;
1327 else
1328 Check_Globals (Get_Called_Entity (Call));
1329 end if;
1330
1331 Inside_Procedure_Call := False;
1332 Update_Params (Call);
1333 end Check_Call_Statement;
1334
1335 -------------------------
1336 -- Check_Callable_Body --
1337 -------------------------
1338
1339 procedure Check_Callable_Body (Body_N : Node_Id) is
1340 Save_In_Elab : constant Boolean := Inside_Elaboration;
1341 Body_Id : constant Entity_Id := Defining_Entity (Body_N);
1342 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id);
1343 Prag : constant Node_Id := SPARK_Pragma (Body_Id);
1344
1345 Saved_Env : Perm_Env;
1346 Saved_Borrowers : Variable_Mapping;
1347 Saved_Observers : Variable_Mapping;
1348
1349 begin
1350 -- Only SPARK bodies are analyzed
1351
1352 if No (Prag)
1353 or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On
1354 then
1355 return;
1356 end if;
1357
1358 Inside_Elaboration := False;
1359
1360 if Ekind (Spec_Id) = E_Function
1361 and then Is_Anonymous_Access_Type (Etype (Spec_Id))
1362 and then not Is_Traversal_Function (Spec_Id)
1363 then
1364 if Emit_Messages then
1365 Error_Msg_N ("anonymous access type for result only allowed for "
1366 & "traversal functions", Spec_Id);
1367 end if;
1368 return;
1369 end if;
1370
1371 -- Save environment and put a new one in place
1372
1373 Move_Env (Current_Perm_Env, Saved_Env);
1374 Move_Variable_Mapping (Current_Borrowers, Saved_Borrowers);
1375 Move_Variable_Mapping (Current_Observers, Saved_Observers);
1376
1377 -- Add formals and globals to the environment with adequate permissions
1378
1379 if Is_Subprogram_Or_Entry (Spec_Id) then
1380 Setup_Parameters (Spec_Id);
1381 Setup_Globals (Spec_Id);
1382 end if;
1383
1384 -- For protected operations, add protected components to the environment
1385 -- with adequate permissions.
1386
1387 if Is_Protected_Operation (Spec_Id) then
1388 Setup_Protected_Components (Spec_Id);
1389 end if;
1390
1391 -- Analyze the body of the subprogram
1392
1393 Check_List (Declarations (Body_N));
1394 Check_Node (Handled_Statement_Sequence (Body_N));
1395
1396 -- Check the read-write permissions of borrowed parameters/globals
1397
1398 if Ekind_In (Spec_Id, E_Procedure, E_Entry)
1399 and then not No_Return (Spec_Id)
1400 then
1401 Return_Parameters (Spec_Id);
1402 Return_Globals (Spec_Id);
1403 end if;
1404
1405 -- Restore the saved environment and free the current one
1406
1407 Move_Env (Saved_Env, Current_Perm_Env);
1408 Move_Variable_Mapping (Saved_Borrowers, Current_Borrowers);
1409 Move_Variable_Mapping (Saved_Observers, Current_Observers);
1410
1411 Inside_Elaboration := Save_In_Elab;
1412 end Check_Callable_Body;
1413
1414 -----------------------
1415 -- Check_Declaration --
1416 -----------------------
1417
1418 procedure Check_Declaration (Decl : Node_Id) is
1419 Target : constant Entity_Id := Defining_Identifier (Decl);
1420 Target_Typ : constant Node_Id := Etype (Target);
1421 Expr : Node_Id;
1422 Dummy : Boolean := True;
1423
1424 begin
1425 -- Start with legality rules not related to permissions
1426
1427 Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
1428
1429 -- Now check permission-related legality rules
1430
1431 case N_Declaration'(Nkind (Decl)) is
1432 when N_Full_Type_Declaration =>
1433 null;
1434
1435 -- ??? What about component declarations with defaults.
1436
1437 when N_Subtype_Declaration =>
1438 Check_Expression (Subtype_Indication (Decl), Read);
1439
1440 when N_Object_Declaration =>
1441 Expr := Expression (Decl);
1442
1443 if Present (Expr) then
1444 Check_Assignment (Target => Target,
1445 Expr => Expr);
1446 end if;
1447
1448 if Is_Deep (Target_Typ) then
1449 declare
1450 Tree : constant Perm_Tree_Access :=
1451 new Perm_Tree_Wrapper'
1452 (Tree =>
1453 (Kind => Entire_Object,
1454 Is_Node_Deep => True,
1455 Explanation => Decl,
1456 Permission => Read_Write,
1457 Children_Permission => Read_Write));
1458 begin
1459 Set (Current_Perm_Env, Target, Tree);
1460 end;
1461 end if;
1462
1463 when N_Iterator_Specification =>
1464 null;
1465
1466 when N_Loop_Parameter_Specification =>
1467 null;
1468
1469 -- Checking should not be called directly on these nodes
1470
1471 when N_Function_Specification
1472 | N_Entry_Declaration
1473 | N_Procedure_Specification
1474 | N_Component_Declaration
1475 =>
1476 raise Program_Error;
1477
1478 -- Ignored constructs for pointer checking
1479
1480 when N_Formal_Object_Declaration
1481 | N_Formal_Type_Declaration
1482 | N_Incomplete_Type_Declaration
1483 | N_Private_Extension_Declaration
1484 | N_Private_Type_Declaration
1485 | N_Protected_Type_Declaration
1486 =>
1487 null;
1488
1489 -- The following nodes are rewritten by semantic analysis
1490
1491 when N_Expression_Function =>
1492 raise Program_Error;
1493 end case;
1494 end Check_Declaration;
1495
1496 --------------------------------
1497 -- Check_Declaration_Legality --
1498 --------------------------------
1499
1500 procedure Check_Declaration_Legality
1501 (Decl : Node_Id;
1502 Force : Boolean;
1503 Legal : in out Boolean)
1504 is
1505 function Original_Emit_Messages return Boolean renames Emit_Messages;
1506
1507 function Emit_Messages return Boolean;
1508 -- Local wrapper around generic formal parameter Emit_Messages, to
1509 -- check the value of parameter Force before calling the original
1510 -- Emit_Messages, and setting Legal to False.
1511
1512 -------------------
1513 -- Emit_Messages --
1514 -------------------
1515
1516 function Emit_Messages return Boolean is
1517 begin
1518 Legal := False;
1519 return Force and then Original_Emit_Messages;
1520 end Emit_Messages;
1521
1522 -- Local variables
1523
1524 Target : constant Entity_Id := Defining_Identifier (Decl);
1525 Target_Typ : constant Node_Id := Etype (Target);
1526 Expr : Node_Id;
1527
1528 -- Start of processing for Check_Declaration_Legality
1529
1530 begin
1531 case N_Declaration'(Nkind (Decl)) is
1532 when N_Full_Type_Declaration =>
1533 Check_Type_Legality (Target, Force, Legal);
1534
1535 when N_Subtype_Declaration =>
1536 null;
1537
1538 when N_Object_Declaration =>
1539 Expr := Expression (Decl);
1540
1541 Check_Type_Legality (Target_Typ, Force, Legal);
1542
1543 -- A declaration of a stand-alone object of an anonymous access
1544 -- type shall have an explicit initial value and shall occur
1545 -- immediately within a subprogram body, an entry body, or a
1546 -- block statement (SPARK RM 3.10(4)).
1547
1548 if Is_Anonymous_Access_Type (Target_Typ) then
1549 declare
1550 Scop : constant Entity_Id := Scope (Target);
1551 begin
1552 if not Is_Local_Context (Scop) then
1553 if Emit_Messages then
1554 Error_Msg_N
1555 ("object of anonymous access type must be declared "
1556 & "immediately within a subprogram, entry or block "
1557 & "(SPARK RM 3.10(4))", Decl);
1558 end if;
1559 end if;
1560 end;
1561
1562 if No (Expr) then
1563 if Emit_Messages then
1564 Error_Msg_N ("object of anonymous access type must be "
1565 & "initialized (SPARK RM 3.10(4))", Decl);
1566 end if;
1567 end if;
1568 end if;
1569
1570 when N_Iterator_Specification =>
1571 null;
1572
1573 when N_Loop_Parameter_Specification =>
1574 null;
1575
1576 -- Checking should not be called directly on these nodes
1577
1578 when N_Function_Specification
1579 | N_Entry_Declaration
1580 | N_Procedure_Specification
1581 | N_Component_Declaration
1582 =>
1583 raise Program_Error;
1584
1585 -- Ignored constructs for pointer checking
1586
1587 when N_Formal_Object_Declaration
1588 | N_Formal_Type_Declaration
1589 | N_Incomplete_Type_Declaration
1590 | N_Private_Extension_Declaration
1591 | N_Private_Type_Declaration
1592 | N_Protected_Type_Declaration
1593 =>
1594 null;
1595
1596 -- The following nodes are rewritten by semantic analysis
1597
1598 when N_Expression_Function =>
1599 raise Program_Error;
1600 end case;
1601 end Check_Declaration_Legality;
1602
1603 ----------------------
1604 -- Check_Expression --
1605 ----------------------
1606
1607 procedure Check_Expression
1608 (Expr : Node_Id;
1609 Mode : Extended_Checking_Mode)
1610 is
1611 -- Local subprograms
1612
1613 function Is_Type_Name (Expr : Node_Id) return Boolean;
1614 -- Detect when a path expression is in fact a type name
1615
1616 procedure Move_Expression (Expr : Node_Id);
1617 -- Some subexpressions are only analyzed in Move mode. This is a
1618 -- specialized version of Check_Expression for that case.
1619
1620 procedure Move_Expression_List (L : List_Id);
1621 -- Call Move_Expression on every expression in the list L
1622
1623 procedure Read_Expression (Expr : Node_Id);
1624 -- Most subexpressions are only analyzed in Read mode. This is a
1625 -- specialized version of Check_Expression for that case.
1626
1627 procedure Read_Expression_List (L : List_Id);
1628 -- Call Read_Expression on every expression in the list L
1629
1630 procedure Read_Indexes (Expr : Node_Id);
1631 -- When processing a path, the index expressions and function call
1632 -- arguments occurring on the path should be analyzed in Read mode.
1633
1634 ------------------
1635 -- Is_Type_Name --
1636 ------------------
1637
1638 function Is_Type_Name (Expr : Node_Id) return Boolean is
1639 begin
1640 return Nkind_In (Expr, N_Expanded_Name, N_Identifier)
1641 and then Is_Type (Entity (Expr));
1642 end Is_Type_Name;
1643
1644 ---------------------
1645 -- Move_Expression --
1646 ---------------------
1647
1648 -- Distinguish the case where the argument is a path expression that
1649 -- needs explicit moving.
1650
1651 procedure Move_Expression (Expr : Node_Id) is
1652 begin
1653 if Is_Path_Expression (Expr) then
1654 Check_Expression (Expr, Move);
1655 else
1656 Read_Expression (Expr);
1657 end if;
1658 end Move_Expression;
1659
1660 --------------------------
1661 -- Move_Expression_List --
1662 --------------------------
1663
1664 procedure Move_Expression_List (L : List_Id) is
1665 N : Node_Id;
1666 begin
1667 N := First (L);
1668 while Present (N) loop
1669 Move_Expression (N);
1670 Next (N);
1671 end loop;
1672 end Move_Expression_List;
1673
1674 ---------------------
1675 -- Read_Expression --
1676 ---------------------
1677
1678 procedure Read_Expression (Expr : Node_Id) is
1679 begin
1680 Check_Expression (Expr, Read);
1681 end Read_Expression;
1682
1683 --------------------------
1684 -- Read_Expression_List --
1685 --------------------------
1686
1687 procedure Read_Expression_List (L : List_Id) is
1688 N : Node_Id;
1689 begin
1690 N := First (L);
1691 while Present (N) loop
1692 Read_Expression (N);
1693 Next (N);
1694 end loop;
1695 end Read_Expression_List;
1696
1697 ------------------
1698 -- Read_Indexes --
1699 ------------------
1700
1701 procedure Read_Indexes (Expr : Node_Id) is
1702
1703 -- Local subprograms
1704
1705 function Is_Singleton_Choice (Choices : List_Id) return Boolean;
1706 -- Return whether Choices is a singleton choice
1707
1708 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id);
1709 -- Call Read_Expression on the actual
1710
1711 -------------------------
1712 -- Is_Singleton_Choice --
1713 -------------------------
1714
1715 function Is_Singleton_Choice (Choices : List_Id) return Boolean is
1716 Choice : constant Node_Id := First (Choices);
1717 begin
1718 return List_Length (Choices) = 1
1719 and then Nkind (Choice) /= N_Others_Choice
1720 and then not Nkind_In (Choice, N_Subtype_Indication, N_Range)
1721 and then not
1722 (Nkind_In (Choice, N_Identifier, N_Expanded_Name)
1723 and then Is_Type (Entity (Choice)));
1724 end Is_Singleton_Choice;
1725
1726 ----------------
1727 -- Read_Param --
1728 ----------------
1729
1730 procedure Read_Param (Formal : Entity_Id; Actual : Node_Id) is
1731 pragma Unreferenced (Formal);
1732 begin
1733 Read_Expression (Actual);
1734 end Read_Param;
1735
1736 procedure Read_Params is new Iterate_Call_Parameters (Read_Param);
1737
1738 -- Start of processing for Read_Indexes
1739
1740 begin
1741 if not Is_Subpath_Expression (Expr) then
1742 if Emit_Messages then
1743 Error_Msg_N
1744 ("name expected here for move/borrow/observe", Expr);
1745 end if;
1746 return;
1747 end if;
1748
1749 case N_Subexpr'(Nkind (Expr)) is
1750 when N_Identifier
1751 | N_Expanded_Name
1752 | N_Null
1753 =>
1754 null;
1755
1756 when N_Explicit_Dereference
1757 | N_Selected_Component
1758 =>
1759 Read_Indexes (Prefix (Expr));
1760
1761 when N_Indexed_Component =>
1762 Read_Indexes (Prefix (Expr));
1763 Read_Expression_List (Expressions (Expr));
1764
1765 when N_Slice =>
1766 Read_Indexes (Prefix (Expr));
1767 Read_Expression (Discrete_Range (Expr));
1768
1769 -- The argument of an allocator is moved as part of the implicit
1770 -- assignment.
1771
1772 when N_Allocator =>
1773 Move_Expression (Expression (Expr));
1774
1775 when N_Function_Call =>
1776 Read_Params (Expr);
1777 if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then
1778 if Emit_Messages then
1779 Error_Msg_N
1780 ("call through access to subprogram is not allowed in "
1781 & "SPARK", Expr);
1782 end if;
1783 else
1784 Check_Globals (Get_Called_Entity (Expr));
1785 end if;
1786
1787 when N_Op_Concat =>
1788 Read_Expression (Left_Opnd (Expr));
1789 Read_Expression (Right_Opnd (Expr));
1790
1791 when N_Qualified_Expression
1792 | N_Type_Conversion
1793 | N_Unchecked_Type_Conversion
1794 =>
1795 Read_Indexes (Expression (Expr));
1796
1797 when N_Aggregate =>
1798 declare
1799 Assocs : constant List_Id := Component_Associations (Expr);
1800 CL : List_Id;
1801 Assoc : Node_Id := Nlists.First (Assocs);
1802 Choice : Node_Id;
1803
1804 begin
1805 -- The subexpressions of an aggregate are moved as part
1806 -- of the implicit assignments. Handle the positional
1807 -- components first.
1808
1809 Move_Expression_List (Expressions (Expr));
1810
1811 -- Handle the named components next
1812
1813 while Present (Assoc) loop
1814 CL := Choices (Assoc);
1815
1816 -- For an array aggregate, we should also check that the
1817 -- expressions used in choices are readable.
1818
1819 if Is_Array_Type (Etype (Expr)) then
1820 Choice := Nlists.First (CL);
1821 while Present (Choice) loop
1822 if Nkind (Choice) /= N_Others_Choice then
1823 Read_Expression (Choice);
1824 end if;
1825 Next (Choice);
1826 end loop;
1827 end if;
1828
1829 -- There can be only one element for a value of deep type
1830 -- in order to avoid aliasing.
1831
1832 if not Box_Present (Assoc)
1833 and then Is_Deep (Etype (Expression (Assoc)))
1834 and then not Is_Singleton_Choice (CL)
1835 and then Emit_Messages
1836 then
1837 Error_Msg_F
1838 ("singleton choice required to prevent aliasing",
1839 First (CL));
1840 end if;
1841
1842 -- The subexpressions of an aggregate are moved as part
1843 -- of the implicit assignments.
1844
1845 if not Box_Present (Assoc) then
1846 Move_Expression (Expression (Assoc));
1847 end if;
1848
1849 Next (Assoc);
1850 end loop;
1851 end;
1852
1853 when N_Extension_Aggregate =>
1854 declare
1855 Exprs : constant List_Id := Expressions (Expr);
1856 Assocs : constant List_Id := Component_Associations (Expr);
1857 CL : List_Id;
1858 Assoc : Node_Id := Nlists.First (Assocs);
1859
1860 begin
1861 Move_Expression (Ancestor_Part (Expr));
1862
1863 -- No positional components allowed at this stage
1864
1865 if Present (Exprs) then
1866 raise Program_Error;
1867 end if;
1868
1869 while Present (Assoc) loop
1870 CL := Choices (Assoc);
1871
1872 -- Only singleton components allowed at this stage
1873
1874 if not Is_Singleton_Choice (CL) then
1875 raise Program_Error;
1876 end if;
1877
1878 -- The subexpressions of an aggregate are moved as part
1879 -- of the implicit assignments.
1880
1881 if not Box_Present (Assoc) then
1882 Move_Expression (Expression (Assoc));
1883 end if;
1884
1885 Next (Assoc);
1886 end loop;
1887 end;
1888
1889 when N_If_Expression =>
1890 declare
1891 Cond : constant Node_Id := First (Expressions (Expr));
1892 Then_Part : constant Node_Id := Next (Cond);
1893 Else_Part : constant Node_Id := Next (Then_Part);
1894 begin
1895 Read_Expression (Cond);
1896 Read_Indexes (Then_Part);
1897 Read_Indexes (Else_Part);
1898 end;
1899
1900 when N_Case_Expression =>
1901 declare
1902 Cases : constant List_Id := Alternatives (Expr);
1903 Cur_Case : Node_Id := First (Cases);
1904
1905 begin
1906 Read_Expression (Expression (Expr));
1907
1908 while Present (Cur_Case) loop
1909 Read_Indexes (Expression (Cur_Case));
1910 Next (Cur_Case);
1911 end loop;
1912 end;
1913
1914 when N_Attribute_Reference =>
1915 pragma Assert
1916 (Get_Attribute_Id (Attribute_Name (Expr)) =
1917 Attribute_Loop_Entry
1918 or else
1919 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1920 or else
1921 Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image);
1922
1923 Read_Expression (Prefix (Expr));
1924
1925 if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
1926 or else (Get_Attribute_Id (Attribute_Name (Expr)) =
1927 Attribute_Image
1928 and then Is_Type_Name (Prefix (Expr)))
1929 then
1930 Read_Expression_List (Expressions (Expr));
1931 end if;
1932
1933 when others =>
1934 raise Program_Error;
1935 end case;
1936 end Read_Indexes;
1937
1938 -- Start of processing for Check_Expression
1939
1940 begin
1941 if Is_Type_Name (Expr) then
1942 return;
1943
1944 elsif Is_Path_Expression (Expr) then
1945 if Mode /= Assign then
1946 Read_Indexes (Expr);
1947 end if;
1948
1949 if Mode /= Read_Subexpr then
1950 Process_Path (Expr, Mode);
1951 end if;
1952
1953 return;
1954 end if;
1955
1956 -- Expressions that are not path expressions should only be analyzed in
1957 -- Read mode.
1958
1959 if Mode /= Read then
1960 if Emit_Messages then
1961 Error_Msg_N ("name expected here for move/borrow/observe", Expr);
1962 end if;
1963 return;
1964 end if;
1965
1966 -- Special handling for nodes that may contain evaluated expressions in
1967 -- the form of constraints.
1968
1969 case Nkind (Expr) is
1970 when N_Index_Or_Discriminant_Constraint =>
1971 declare
1972 Assn : Node_Id := First (Constraints (Expr));
1973 begin
1974 while Present (Assn) loop
1975 case Nkind (Assn) is
1976 when N_Discriminant_Association =>
1977 Read_Expression (Expression (Assn));
1978
1979 when others =>
1980 Read_Expression (Assn);
1981 end case;
1982
1983 Next (Assn);
1984 end loop;
1985 end;
1986 return;
1987
1988 when N_Range_Constraint =>
1989 Read_Expression (Range_Expression (Expr));
1990 return;
1991
1992 when N_Subtype_Indication =>
1993 if Present (Constraint (Expr)) then
1994 Read_Expression (Constraint (Expr));
1995 end if;
1996 return;
1997
1998 when N_Digits_Constraint =>
1999 Read_Expression (Digits_Expression (Expr));
2000 if Present (Range_Constraint (Expr)) then
2001 Read_Expression (Range_Constraint (Expr));
2002 end if;
2003 return;
2004
2005 when N_Delta_Constraint =>
2006 Read_Expression (Delta_Expression (Expr));
2007 if Present (Range_Constraint (Expr)) then
2008 Read_Expression (Range_Constraint (Expr));
2009 end if;
2010 return;
2011
2012 when others =>
2013 null;
2014 end case;
2015
2016 -- At this point Expr can only be a subexpression
2017
2018 case N_Subexpr'(Nkind (Expr)) is
2019
2020 when N_Binary_Op
2021 | N_Short_Circuit
2022 =>
2023 Read_Expression (Left_Opnd (Expr));
2024 Read_Expression (Right_Opnd (Expr));
2025
2026 when N_Membership_Test =>
2027 Read_Expression (Left_Opnd (Expr));
2028 if Present (Right_Opnd (Expr)) then
2029 Read_Expression (Right_Opnd (Expr));
2030 else
2031 declare
2032 Cases : constant List_Id := Alternatives (Expr);
2033 Cur_Case : Node_Id := First (Cases);
2034
2035 begin
2036 while Present (Cur_Case) loop
2037 Read_Expression (Cur_Case);
2038 Next (Cur_Case);
2039 end loop;
2040 end;
2041 end if;
2042
2043 when N_Unary_Op =>
2044 Read_Expression (Right_Opnd (Expr));
2045
2046 when N_Attribute_Reference =>
2047 declare
2048 Aname : constant Name_Id := Attribute_Name (Expr);
2049 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
2050 Pref : constant Node_Id := Prefix (Expr);
2051 Args : constant List_Id := Expressions (Expr);
2052
2053 begin
2054 case Attr_Id is
2055
2056 -- The following attributes take either no arguments, or
2057 -- arguments that do not refer to evaluated expressions
2058 -- (like Length or Loop_Entry), hence only the prefix
2059 -- needs to be read.
2060
2061 when Attribute_Address
2062 | Attribute_Alignment
2063 | Attribute_Callable
2064 | Attribute_Component_Size
2065 | Attribute_Constrained
2066 | Attribute_First
2067 | Attribute_First_Bit
2068 | Attribute_Last
2069 | Attribute_Last_Bit
2070 | Attribute_Length
2071 | Attribute_Loop_Entry
2072 | Attribute_Object_Size
2073 | Attribute_Position
2074 | Attribute_Size
2075 | Attribute_Terminated
2076 | Attribute_Valid
2077 | Attribute_Value_Size
2078 =>
2079 Read_Expression (Pref);
2080
2081 -- The following attributes take a type name as prefix,
2082 -- hence only the arguments need to be read.
2083
2084 when Attribute_Ceiling
2085 | Attribute_Floor
2086 | Attribute_Max
2087 | Attribute_Min
2088 | Attribute_Mod
2089 | Attribute_Pos
2090 | Attribute_Pred
2091 | Attribute_Remainder
2092 | Attribute_Rounding
2093 | Attribute_Succ
2094 | Attribute_Truncation
2095 | Attribute_Val
2096 | Attribute_Value
2097 =>
2098 Read_Expression_List (Args);
2099
2100 -- Attributes Image and Img either take a type name as
2101 -- prefix with an expression in argument, or the expression
2102 -- directly as prefix. Adapt to each case.
2103
2104 when Attribute_Image
2105 | Attribute_Img
2106 =>
2107 if No (Args) then
2108 Read_Expression (Pref);
2109 else
2110 Read_Expression_List (Args);
2111 end if;
2112
2113 -- Attribute Update takes expressions as both prefix and
2114 -- arguments, so both need to be read.
2115
2116 when Attribute_Update =>
2117 Read_Expression (Pref);
2118 Read_Expression_List (Args);
2119
2120 -- Attribute Modulus does not reference the evaluated
2121 -- expression, so it can be ignored for this analysis.
2122
2123 when Attribute_Modulus =>
2124 null;
2125
2126 -- The following attributes apply to types; there are no
2127 -- expressions to read.
2128
2129 when Attribute_Class
2130 | Attribute_Storage_Size
2131 =>
2132 null;
2133
2134 -- Postconditions should not be analyzed
2135
2136 when Attribute_Old
2137 | Attribute_Result
2138 =>
2139 raise Program_Error;
2140
2141 when others =>
2142 null;
2143 end case;
2144 end;
2145
2146 when N_Range =>
2147 Read_Expression (Low_Bound (Expr));
2148 Read_Expression (High_Bound (Expr));
2149
2150 when N_If_Expression =>
2151 Read_Expression_List (Expressions (Expr));
2152
2153 when N_Case_Expression =>
2154 declare
2155 Cases : constant List_Id := Alternatives (Expr);
2156 Cur_Case : Node_Id := First (Cases);
2157
2158 begin
2159 while Present (Cur_Case) loop
2160 Read_Expression (Expression (Cur_Case));
2161 Next (Cur_Case);
2162 end loop;
2163
2164 Read_Expression (Expression (Expr));
2165 end;
2166
2167 when N_Qualified_Expression
2168 | N_Type_Conversion
2169 | N_Unchecked_Type_Conversion
2170 =>
2171 Read_Expression (Expression (Expr));
2172
2173 when N_Quantified_Expression =>
2174 declare
2175 For_In_Spec : constant Node_Id :=
2176 Loop_Parameter_Specification (Expr);
2177 For_Of_Spec : constant Node_Id :=
2178 Iterator_Specification (Expr);
2179 For_Of_Spec_Typ : Node_Id;
2180
2181 begin
2182 if Present (For_In_Spec) then
2183 Read_Expression (Discrete_Subtype_Definition (For_In_Spec));
2184 else
2185 Read_Expression (Name (For_Of_Spec));
2186 For_Of_Spec_Typ := Subtype_Indication (For_Of_Spec);
2187 if Present (For_Of_Spec_Typ) then
2188 Read_Expression (For_Of_Spec_Typ);
2189 end if;
2190 end if;
2191
2192 Read_Expression (Condition (Expr));
2193 end;
2194
2195 when N_Character_Literal
2196 | N_Numeric_Or_String_Literal
2197 | N_Operator_Symbol
2198 | N_Raise_Expression
2199 | N_Raise_xxx_Error
2200 =>
2201 null;
2202
2203 when N_Delta_Aggregate
2204 | N_Target_Name
2205 =>
2206 null;
2207
2208 -- Procedure calls are handled in Check_Node
2209
2210 when N_Procedure_Call_Statement =>
2211 raise Program_Error;
2212
2213 -- Path expressions are handled before this point
2214
2215 when N_Aggregate
2216 | N_Allocator
2217 | N_Expanded_Name
2218 | N_Explicit_Dereference
2219 | N_Extension_Aggregate
2220 | N_Function_Call
2221 | N_Identifier
2222 | N_Indexed_Component
2223 | N_Null
2224 | N_Selected_Component
2225 | N_Slice
2226 =>
2227 raise Program_Error;
2228
2229 -- The following nodes are never generated in GNATprove mode
2230
2231 when N_Expression_With_Actions
2232 | N_Reference
2233 | N_Unchecked_Expression
2234 =>
2235 raise Program_Error;
2236 end case;
2237 end Check_Expression;
2238
2239 ----------------
2240 -- Check_List --
2241 ----------------
2242
2243 procedure Check_List (L : List_Id) is
2244 N : Node_Id;
2245 begin
2246 N := First (L);
2247 while Present (N) loop
2248 Check_Node (N);
2249 Next (N);
2250 end loop;
2251 end Check_List;
2252
2253 --------------------------
2254 -- Check_Loop_Statement --
2255 --------------------------
2256
2257 procedure Check_Loop_Statement (Stmt : Node_Id) is
2258
2259 -- Local Subprograms
2260
2261 procedure Check_Is_Less_Restrictive_Env
2262 (Exiting_Env : Perm_Env;
2263 Entry_Env : Perm_Env);
2264 -- This procedure checks that the Exiting_Env environment is less
2265 -- restrictive than the Entry_Env environment.
2266
2267 procedure Check_Is_Less_Restrictive_Tree
2268 (New_Tree : Perm_Tree_Access;
2269 Orig_Tree : Perm_Tree_Access;
2270 E : Entity_Id);
2271 -- Auxiliary procedure to check that the tree New_Tree is less
2272 -- restrictive than the tree Orig_Tree for the entity E.
2273
2274 procedure Perm_Error_Loop_Exit
2275 (E : Entity_Id;
2276 Loop_Id : Node_Id;
2277 Perm : Perm_Kind;
2278 Found_Perm : Perm_Kind;
2279 Expl : Node_Id);
2280 -- A procedure that is called when the permissions found contradict
2281 -- the rules established by the RM at the exit of loops. This function
2282 -- is called with the entity, the node of the enclosing loop, the
2283 -- permission that was expected, and the permission found, and issues
2284 -- an appropriate error message.
2285
2286 -----------------------------------
2287 -- Check_Is_Less_Restrictive_Env --
2288 -----------------------------------
2289
2290 procedure Check_Is_Less_Restrictive_Env
2291 (Exiting_Env : Perm_Env;
2292 Entry_Env : Perm_Env)
2293 is
2294 Comp_Entry : Perm_Tree_Maps.Key_Option;
2295 Iter_Entry, Iter_Exit : Perm_Tree_Access;
2296
2297 begin
2298 Comp_Entry := Get_First_Key (Entry_Env);
2299 while Comp_Entry.Present loop
2300 Iter_Entry := Get (Entry_Env, Comp_Entry.K);
2301 pragma Assert (Iter_Entry /= null);
2302 Iter_Exit := Get (Exiting_Env, Comp_Entry.K);
2303 pragma Assert (Iter_Exit /= null);
2304 Check_Is_Less_Restrictive_Tree
2305 (New_Tree => Iter_Exit,
2306 Orig_Tree => Iter_Entry,
2307 E => Comp_Entry.K);
2308 Comp_Entry := Get_Next_Key (Entry_Env);
2309 end loop;
2310 end Check_Is_Less_Restrictive_Env;
2311
2312 ------------------------------------
2313 -- Check_Is_Less_Restrictive_Tree --
2314 ------------------------------------
2315
2316 procedure Check_Is_Less_Restrictive_Tree
2317 (New_Tree : Perm_Tree_Access;
2318 Orig_Tree : Perm_Tree_Access;
2319 E : Entity_Id)
2320 is
2321 -- Local subprograms
2322
2323 procedure Check_Is_Less_Restrictive_Tree_Than
2324 (Tree : Perm_Tree_Access;
2325 Perm : Perm_Kind;
2326 E : Entity_Id);
2327 -- Auxiliary procedure to check that the tree N is less restrictive
2328 -- than the given permission P.
2329
2330 procedure Check_Is_More_Restrictive_Tree_Than
2331 (Tree : Perm_Tree_Access;
2332 Perm : Perm_Kind;
2333 E : Entity_Id);
2334 -- Auxiliary procedure to check that the tree N is more restrictive
2335 -- than the given permission P.
2336
2337 -----------------------------------------
2338 -- Check_Is_Less_Restrictive_Tree_Than --
2339 -----------------------------------------
2340
2341 procedure Check_Is_Less_Restrictive_Tree_Than
2342 (Tree : Perm_Tree_Access;
2343 Perm : Perm_Kind;
2344 E : Entity_Id)
2345 is
2346 begin
2347 if not (Permission (Tree) >= Perm) then
2348 Perm_Error_Loop_Exit
2349 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2350 end if;
2351
2352 case Kind (Tree) is
2353 when Entire_Object =>
2354 if not (Children_Permission (Tree) >= Perm) then
2355 Perm_Error_Loop_Exit
2356 (E, Stmt, Children_Permission (Tree), Perm,
2357 Explanation (Tree));
2358
2359 end if;
2360
2361 when Reference =>
2362 Check_Is_Less_Restrictive_Tree_Than
2363 (Get_All (Tree), Perm, E);
2364
2365 when Array_Component =>
2366 Check_Is_Less_Restrictive_Tree_Than
2367 (Get_Elem (Tree), Perm, E);
2368
2369 when Record_Component =>
2370 declare
2371 Comp : Perm_Tree_Access;
2372 begin
2373 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2374 while Comp /= null loop
2375 Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E);
2376 Comp :=
2377 Perm_Tree_Maps.Get_Next (Component (Tree));
2378 end loop;
2379 end;
2380 end case;
2381 end Check_Is_Less_Restrictive_Tree_Than;
2382
2383 -----------------------------------------
2384 -- Check_Is_More_Restrictive_Tree_Than --
2385 -----------------------------------------
2386
2387 procedure Check_Is_More_Restrictive_Tree_Than
2388 (Tree : Perm_Tree_Access;
2389 Perm : Perm_Kind;
2390 E : Entity_Id)
2391 is
2392 begin
2393 if not (Perm >= Permission (Tree)) then
2394 Perm_Error_Loop_Exit
2395 (E, Stmt, Permission (Tree), Perm, Explanation (Tree));
2396 end if;
2397
2398 case Kind (Tree) is
2399 when Entire_Object =>
2400 if not (Perm >= Children_Permission (Tree)) then
2401 Perm_Error_Loop_Exit
2402 (E, Stmt, Children_Permission (Tree), Perm,
2403 Explanation (Tree));
2404 end if;
2405
2406 when Reference =>
2407 Check_Is_More_Restrictive_Tree_Than
2408 (Get_All (Tree), Perm, E);
2409
2410 when Array_Component =>
2411 Check_Is_More_Restrictive_Tree_Than
2412 (Get_Elem (Tree), Perm, E);
2413
2414 when Record_Component =>
2415 declare
2416 Comp : Perm_Tree_Access;
2417 begin
2418 Comp := Perm_Tree_Maps.Get_First (Component (Tree));
2419 while Comp /= null loop
2420 Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E);
2421 Comp :=
2422 Perm_Tree_Maps.Get_Next (Component (Tree));
2423 end loop;
2424 end;
2425 end case;
2426 end Check_Is_More_Restrictive_Tree_Than;
2427
2428 -- Start of processing for Check_Is_Less_Restrictive_Tree
2429
2430 begin
2431 if not (Permission (New_Tree) <= Permission (Orig_Tree)) then
2432 Perm_Error_Loop_Exit
2433 (E => E,
2434 Loop_Id => Stmt,
2435 Perm => Permission (New_Tree),
2436 Found_Perm => Permission (Orig_Tree),
2437 Expl => Explanation (New_Tree));
2438 end if;
2439
2440 case Kind (New_Tree) is
2441
2442 -- Potentially folded tree. We check the other tree Orig_Tree to
2443 -- check whether it is folded or not. If folded we just compare
2444 -- their Permission and Children_Permission, if not, then we
2445 -- look at the Children_Permission of the folded tree against
2446 -- the unfolded tree Orig_Tree.
2447
2448 when Entire_Object =>
2449 case Kind (Orig_Tree) is
2450 when Entire_Object =>
2451 if not (Children_Permission (New_Tree) <=
2452 Children_Permission (Orig_Tree))
2453 then
2454 Perm_Error_Loop_Exit
2455 (E, Stmt,
2456 Children_Permission (New_Tree),
2457 Children_Permission (Orig_Tree),
2458 Explanation (New_Tree));
2459 end if;
2460
2461 when Reference =>
2462 Check_Is_More_Restrictive_Tree_Than
2463 (Get_All (Orig_Tree), Children_Permission (New_Tree), E);
2464
2465 when Array_Component =>
2466 Check_Is_More_Restrictive_Tree_Than
2467 (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E);
2468
2469 when Record_Component =>
2470 declare
2471 Comp : Perm_Tree_Access;
2472 begin
2473 Comp := Perm_Tree_Maps.Get_First
2474 (Component (Orig_Tree));
2475 while Comp /= null loop
2476 Check_Is_More_Restrictive_Tree_Than
2477 (Comp, Children_Permission (New_Tree), E);
2478 Comp := Perm_Tree_Maps.Get_Next
2479 (Component (Orig_Tree));
2480 end loop;
2481 end;
2482 end case;
2483
2484 when Reference =>
2485 case Kind (Orig_Tree) is
2486 when Entire_Object =>
2487 Check_Is_Less_Restrictive_Tree_Than
2488 (Get_All (New_Tree), Children_Permission (Orig_Tree), E);
2489
2490 when Reference =>
2491 Check_Is_Less_Restrictive_Tree
2492 (Get_All (New_Tree), Get_All (Orig_Tree), E);
2493
2494 when others =>
2495 raise Program_Error;
2496 end case;
2497
2498 when Array_Component =>
2499 case Kind (Orig_Tree) is
2500 when Entire_Object =>
2501 Check_Is_Less_Restrictive_Tree_Than
2502 (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E);
2503
2504 when Array_Component =>
2505 Check_Is_Less_Restrictive_Tree
2506 (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E);
2507
2508 when others =>
2509 raise Program_Error;
2510 end case;
2511
2512 when Record_Component =>
2513 declare
2514 CompN : Perm_Tree_Access;
2515 begin
2516 CompN :=
2517 Perm_Tree_Maps.Get_First (Component (New_Tree));
2518 case Kind (Orig_Tree) is
2519 when Entire_Object =>
2520 while CompN /= null loop
2521 Check_Is_Less_Restrictive_Tree_Than
2522 (CompN, Children_Permission (Orig_Tree), E);
2523
2524 CompN :=
2525 Perm_Tree_Maps.Get_Next (Component (New_Tree));
2526 end loop;
2527
2528 when Record_Component =>
2529 declare
2530
2531 KeyO : Perm_Tree_Maps.Key_Option;
2532 CompO : Perm_Tree_Access;
2533 begin
2534 KeyO := Perm_Tree_Maps.Get_First_Key
2535 (Component (Orig_Tree));
2536 while KeyO.Present loop
2537 CompN := Perm_Tree_Maps.Get
2538 (Component (New_Tree), KeyO.K);
2539 CompO := Perm_Tree_Maps.Get
2540 (Component (Orig_Tree), KeyO.K);
2541 pragma Assert (CompO /= null);
2542
2543 Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
2544
2545 KeyO := Perm_Tree_Maps.Get_Next_Key
2546 (Component (Orig_Tree));
2547 end loop;
2548 end;
2549
2550 when others =>
2551 raise Program_Error;
2552 end case;
2553 end;
2554 end case;
2555 end Check_Is_Less_Restrictive_Tree;
2556
2557 --------------------------
2558 -- Perm_Error_Loop_Exit --
2559 --------------------------
2560
2561 procedure Perm_Error_Loop_Exit
2562 (E : Entity_Id;
2563 Loop_Id : Node_Id;
2564 Perm : Perm_Kind;
2565 Found_Perm : Perm_Kind;
2566 Expl : Node_Id)
2567 is
2568 begin
2569 if Emit_Messages then
2570 Error_Msg_Node_2 := Loop_Id;
2571 Error_Msg_N
2572 ("insufficient permission for & when exiting loop &", E);
2573 Perm_Mismatch (Exp_Perm => Perm,
2574 Act_Perm => Found_Perm,
2575 N => Loop_Id,
2576 Expl => Expl);
2577 end if;
2578 end Perm_Error_Loop_Exit;
2579
2580 -- Local variables
2581
2582 Loop_Name : constant Entity_Id := Entity (Identifier (Stmt));
2583 Loop_Env : constant Perm_Env_Access := new Perm_Env;
2584 Scheme : constant Node_Id := Iteration_Scheme (Stmt);
2585
2586 -- Start of processing for Check_Loop_Statement
2587
2588 begin
2589 -- Save environment prior to the loop
2590
2591 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all);
2592
2593 -- Add saved environment to loop environment
2594
2595 Set (Current_Loops_Envs, Loop_Name, Loop_Env);
2596
2597 -- If the loop is not a plain-loop, then it may either never be entered,
2598 -- or it may be exited after a number of iterations. Hence add the
2599 -- current permission environment as the initial loop exit environment.
2600 -- Otherwise, the loop exit environment remains empty until it is
2601 -- populated by analyzing exit statements.
2602
2603 if Present (Iteration_Scheme (Stmt)) then
2604 declare
2605 Exit_Env : constant Perm_Env_Access := new Perm_Env;
2606
2607 begin
2608 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all);
2609 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env);
2610 end;
2611 end if;
2612
2613 -- Analyze loop
2614
2615 if Present (Scheme) then
2616
2617 -- Case of a WHILE loop
2618
2619 if Present (Condition (Scheme)) then
2620 Check_Expression (Condition (Scheme), Read);
2621
2622 -- Case of a FOR loop
2623
2624 else
2625 declare
2626 Param_Spec : constant Node_Id :=
2627 Loop_Parameter_Specification (Scheme);
2628 Iter_Spec : constant Node_Id := Iterator_Specification (Scheme);
2629 begin
2630 if Present (Param_Spec) then
2631 Check_Expression
2632 (Discrete_Subtype_Definition (Param_Spec), Read);
2633 else
2634 Check_Expression (Name (Iter_Spec), Read);
2635 if Present (Subtype_Indication (Iter_Spec)) then
2636 Check_Expression (Subtype_Indication (Iter_Spec), Read);
2637 end if;
2638 end if;
2639 end;
2640 end if;
2641 end if;
2642
2643 Check_List (Statements (Stmt));
2644
2645 -- Check that environment gets less restrictive at end of loop
2646
2647 Check_Is_Less_Restrictive_Env
2648 (Exiting_Env => Current_Perm_Env,
2649 Entry_Env => Loop_Env.all);
2650
2651 -- Set environment to the one for exiting the loop
2652
2653 declare
2654 Exit_Env : constant Perm_Env_Access :=
2655 Get (Current_Loops_Accumulators, Loop_Name);
2656 begin
2657 Free_Env (Current_Perm_Env);
2658
2659 -- In the normal case, Exit_Env is not null and we use it. In the
2660 -- degraded case of a plain-loop without exit statements, Exit_Env is
2661 -- null, and we use the initial permission environment at the start
2662 -- of the loop to continue analysis. Any environment would be fine
2663 -- here, since the code after the loop is dead code, but this way we
2664 -- avoid spurious errors by having at least variables in scope inside
2665 -- the environment.
2666
2667 if Exit_Env /= null then
2668 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env);
2669 Free_Env (Loop_Env.all);
2670 Free_Env (Exit_Env.all);
2671 else
2672 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env);
2673 Free_Env (Loop_Env.all);
2674 end if;
2675 end;
2676 end Check_Loop_Statement;
2677
2678 ----------------
2679 -- Check_Node --
2680 ----------------
2681
2682 procedure Check_Node (N : Node_Id) is
2683
2684 procedure Check_Subprogram_Contract (N : Node_Id);
2685 -- Check the postcondition-like contracts for use of 'Old
2686
2687 -------------------------------
2688 -- Check_Subprogram_Contract --
2689 -------------------------------
2690
2691 procedure Check_Subprogram_Contract (N : Node_Id) is
2692 begin
2693 if Nkind (N) = N_Subprogram_Declaration
2694 or else Acts_As_Spec (N)
2695 then
2696 declare
2697 E : constant Entity_Id := Unique_Defining_Entity (N);
2698 Post : constant Node_Id :=
2699 Get_Pragma (E, Pragma_Postcondition);
2700 Cases : constant Node_Id :=
2701 Get_Pragma (E, Pragma_Contract_Cases);
2702 begin
2703 Check_Old_Loop_Entry (Post);
2704 Check_Old_Loop_Entry (Cases);
2705 end;
2706
2707 elsif Nkind (N) = N_Subprogram_Body then
2708 declare
2709 E : constant Entity_Id := Defining_Entity (N);
2710 Ref_Post : constant Node_Id :=
2711 Get_Pragma (E, Pragma_Refined_Post);
2712 begin
2713 Check_Old_Loop_Entry (Ref_Post);
2714 end;
2715 end if;
2716 end Check_Subprogram_Contract;
2717
2718 -- Start of processing for Check_Node
2719
2720 begin
2721 case Nkind (N) is
2722 when N_Declaration =>
2723 Check_Declaration (N);
2724
2725 when N_Body_Stub =>
2726 Check_Node (Get_Body_From_Stub (N));
2727
2728 when N_Statement_Other_Than_Procedure_Call =>
2729 Check_Statement (N);
2730
2731 when N_Procedure_Call_Statement =>
2732 Check_Call_Statement (N);
2733
2734 when N_Package_Body =>
2735 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2736 Check_Package_Body (N);
2737 end if;
2738
2739 when N_Subprogram_Body =>
2740 if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
2741 Check_Subprogram_Contract (N);
2742 Check_Callable_Body (N);
2743 end if;
2744
2745 when N_Entry_Body
2746 | N_Task_Body
2747 =>
2748 Check_Callable_Body (N);
2749
2750 when N_Protected_Body =>
2751 Check_List (Declarations (N));
2752
2753 when N_Package_Declaration =>
2754 Check_Package_Spec (N);
2755
2756 when N_Handled_Sequence_Of_Statements =>
2757 Check_List (Statements (N));
2758
2759 when N_Pragma =>
2760 Check_Pragma (N);
2761
2762 when N_Subprogram_Declaration =>
2763 Check_Subprogram_Contract (N);
2764
2765 -- Attribute references in statement position are not supported in
2766 -- SPARK and will be rejected by GNATprove.
2767
2768 when N_Attribute_Reference =>
2769 null;
2770
2771 -- Ignored constructs for pointer checking
2772
2773 when N_Abstract_Subprogram_Declaration
2774 | N_At_Clause
2775 | N_Attribute_Definition_Clause
2776 | N_Call_Marker
2777 | N_Delta_Constraint
2778 | N_Digits_Constraint
2779 | N_Empty
2780 | N_Enumeration_Representation_Clause
2781 | N_Exception_Declaration
2782 | N_Exception_Renaming_Declaration
2783 | N_Formal_Package_Declaration
2784 | N_Formal_Subprogram_Declaration
2785 | N_Freeze_Entity
2786 | N_Freeze_Generic_Entity
2787 | N_Function_Instantiation
2788 | N_Generic_Function_Renaming_Declaration
2789 | N_Generic_Package_Declaration
2790 | N_Generic_Package_Renaming_Declaration
2791 | N_Generic_Procedure_Renaming_Declaration
2792 | N_Generic_Subprogram_Declaration
2793 | N_Implicit_Label_Declaration
2794 | N_Itype_Reference
2795 | N_Label
2796 | N_Number_Declaration
2797 | N_Object_Renaming_Declaration
2798 | N_Others_Choice
2799 | N_Package_Instantiation
2800 | N_Package_Renaming_Declaration
2801 | N_Procedure_Instantiation
2802 | N_Raise_xxx_Error
2803 | N_Record_Representation_Clause
2804 | N_Subprogram_Renaming_Declaration
2805 | N_Task_Type_Declaration
2806 | N_Use_Package_Clause
2807 | N_With_Clause
2808 | N_Use_Type_Clause
2809 | N_Validate_Unchecked_Conversion
2810 | N_Variable_Reference_Marker
2811 | N_Discriminant_Association
2812
2813 -- ??? check whether we should do something special for
2814 -- N_Discriminant_Association, or maybe raise Program_Error.
2815 =>
2816 null;
2817
2818 -- Checking should not be called directly on these nodes
2819
2820 when others =>
2821 raise Program_Error;
2822 end case;
2823 end Check_Node;
2824
2825 --------------------------
2826 -- Check_Old_Loop_Entry --
2827 --------------------------
2828
2829 procedure Check_Old_Loop_Entry (N : Node_Id) is
2830
2831 function Check_Attribute (N : Node_Id) return Traverse_Result;
2832
2833 ---------------------
2834 -- Check_Attribute --
2835 ---------------------
2836
2837 function Check_Attribute (N : Node_Id) return Traverse_Result is
2838 Attr_Id : Attribute_Id;
2839 Aname : Name_Id;
2840 Pref : Node_Id;
2841
2842 begin
2843 if Nkind (N) = N_Attribute_Reference then
2844 Attr_Id := Get_Attribute_Id (Attribute_Name (N));
2845 Aname := Attribute_Name (N);
2846
2847 if Attr_Id = Attribute_Old
2848 or else Attr_Id = Attribute_Loop_Entry
2849 then
2850 Pref := Prefix (N);
2851
2852 if Is_Deep (Etype (Pref)) then
2853 if Nkind (Pref) /= N_Function_Call then
2854 if Emit_Messages then
2855 Error_Msg_Name_1 := Aname;
2856 Error_Msg_N
2857 ("prefix of % attribute must be a function call "
2858 & "(SPARK RM 3.10(14))", Pref);
2859 end if;
2860
2861 elsif Is_Traversal_Function_Call (Pref) then
2862 if Emit_Messages then
2863 Error_Msg_Name_1 := Aname;
2864 Error_Msg_N
2865 ("prefix of % attribute should not call a traversal "
2866 & "function (SPARK RM 3.10(14))", Pref);
2867 end if;
2868 end if;
2869 end if;
2870 end if;
2871 end if;
2872
2873 return OK;
2874 end Check_Attribute;
2875
2876 procedure Check_All is new Traverse_Proc (Check_Attribute);
2877
2878 -- Start of processing for Check_Old_Loop_Entry
2879
2880 begin
2881 Check_All (N);
2882 end Check_Old_Loop_Entry;
2883
2884 ------------------------
2885 -- Check_Package_Body --
2886 ------------------------
2887
2888 procedure Check_Package_Body (Pack : Node_Id) is
2889 Save_In_Elab : constant Boolean := Inside_Elaboration;
2890 Spec : constant Node_Id :=
2891 Package_Specification (Corresponding_Spec (Pack));
2892 Id : constant Entity_Id := Defining_Entity (Pack);
2893 Prag : constant Node_Id := SPARK_Pragma (Id);
2894 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2895 Saved_Env : Perm_Env;
2896
2897 begin
2898 if Present (Prag)
2899 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2900 then
2901 Inside_Elaboration := True;
2902
2903 -- Save environment and put a new one in place
2904
2905 Move_Env (Current_Perm_Env, Saved_Env);
2906
2907 -- Reanalyze package spec to have its variables in the environment
2908
2909 Check_List (Visible_Declarations (Spec));
2910 Check_List (Private_Declarations (Spec));
2911
2912 -- Check declarations and statements in the special mode for
2913 -- elaboration.
2914
2915 Check_List (Declarations (Pack));
2916
2917 if Present (Aux_Prag)
2918 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2919 then
2920 Check_Node (Handled_Statement_Sequence (Pack));
2921 end if;
2922
2923 -- Restore the saved environment and free the current one
2924
2925 Move_Env (Saved_Env, Current_Perm_Env);
2926
2927 Inside_Elaboration := Save_In_Elab;
2928 end if;
2929 end Check_Package_Body;
2930
2931 ------------------------
2932 -- Check_Package_Spec --
2933 ------------------------
2934
2935 procedure Check_Package_Spec (Pack : Node_Id) is
2936 Save_In_Elab : constant Boolean := Inside_Elaboration;
2937 Spec : constant Node_Id := Specification (Pack);
2938 Id : constant Entity_Id := Defining_Entity (Pack);
2939 Prag : constant Node_Id := SPARK_Pragma (Id);
2940 Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id);
2941 Saved_Env : Perm_Env;
2942
2943 begin
2944 if Present (Prag)
2945 and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On
2946 then
2947 Inside_Elaboration := True;
2948
2949 -- Save environment and put a new one in place
2950
2951 Move_Env (Current_Perm_Env, Saved_Env);
2952
2953 -- Check declarations in the special mode for elaboration
2954
2955 Check_List (Visible_Declarations (Spec));
2956
2957 if Present (Aux_Prag)
2958 and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On
2959 then
2960 Check_List (Private_Declarations (Spec));
2961 end if;
2962
2963 -- Restore the saved environment and free the current one. As part of
2964 -- the restoration, the environment of the package spec is merged in
2965 -- the enclosing environment, which may be an enclosing
2966 -- package/subprogram spec or body which has access to the variables
2967 -- of the package spec.
2968
2969 Merge_Env (Saved_Env, Current_Perm_Env);
2970
2971 Inside_Elaboration := Save_In_Elab;
2972 end if;
2973 end Check_Package_Spec;
2974
2975 -------------------------------
2976 -- Check_Parameter_Or_Global --
2977 -------------------------------
2978
2979 procedure Check_Parameter_Or_Global
2980 (Expr : Node_Id;
2981 Typ : Entity_Id;
2982 Kind : Formal_Kind;
2983 Subp : Entity_Id;
2984 Global_Var : Boolean)
2985 is
2986 Mode : Checking_Mode;
2987 Status : Error_Status;
2988
2989 begin
2990 if not Global_Var
2991 and then Is_Anonymous_Access_Type (Typ)
2992 then
2993 Check_Source_Of_Borrow_Or_Observe (Expr, Status);
2994
2995 if Status /= OK then
2996 return;
2997 end if;
2998 end if;
2999
3000 case Kind is
3001 when E_In_Parameter =>
3002
3003 -- Inputs of functions have R permission only
3004
3005 if Ekind (Subp) = E_Function then
3006 Mode := Read;
3007
3008 -- Input global variables have R permission only
3009
3010 elsif Global_Var then
3011 Mode := Read;
3012
3013 -- Anonymous access to constant is an observe
3014
3015 elsif Is_Anonymous_Access_Type (Typ)
3016 and then Is_Access_Constant (Typ)
3017 then
3018 Mode := Observe;
3019
3020 -- Other access types are a borrow
3021
3022 elsif Is_Access_Type (Typ) then
3023 Mode := Borrow;
3024
3025 -- Deep types other than access types define an observe
3026
3027 elsif Is_Deep (Typ) then
3028 Mode := Observe;
3029
3030 -- Otherwise the variable is read
3031
3032 else
3033 Mode := Read;
3034 end if;
3035
3036 when E_Out_Parameter =>
3037 Mode := Assign;
3038
3039 when E_In_Out_Parameter =>
3040 Mode := Move;
3041 end case;
3042
3043 if Mode = Assign then
3044 Check_Expression (Expr, Read_Subexpr);
3045 end if;
3046
3047 Check_Expression (Expr, Mode);
3048 end Check_Parameter_Or_Global;
3049
3050 procedure Check_Globals_Inst is
3051 new Handle_Globals (Check_Parameter_Or_Global);
3052
3053 procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst;
3054
3055 ------------------
3056 -- Check_Pragma --
3057 ------------------
3058
3059 procedure Check_Pragma (Prag : Node_Id) is
3060 Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag);
3061 Arg1 : constant Node_Id :=
3062 First (Pragma_Argument_Associations (Prag));
3063 Arg2 : Node_Id := Empty;
3064
3065 begin
3066 if Present (Arg1) then
3067 Arg2 := Next (Arg1);
3068 end if;
3069
3070 case Prag_Id is
3071 when Pragma_Check =>
3072 declare
3073 Expr : constant Node_Id := Expression (Arg2);
3074 begin
3075 Check_Expression (Expr, Read);
3076
3077 -- Prefix of Loop_Entry should be checked inside any assertion
3078 -- where it may appear.
3079
3080 Check_Old_Loop_Entry (Expr);
3081 end;
3082
3083 -- Prefix of Loop_Entry should be checked inside a Loop_Variant
3084
3085 when Pragma_Loop_Variant =>
3086 Check_Old_Loop_Entry (Prag);
3087
3088 -- There is no need to check contracts, as these can only access
3089 -- inputs and outputs of the subprogram. Inputs are checked
3090 -- independently for R permission. Outputs are checked
3091 -- independently to have RW permission on exit.
3092
3093 -- Postconditions are checked for correct use of 'Old, but starting
3094 -- from the corresponding declaration, in order to avoid dealing with
3095 -- with contracts on generic subprograms, which are not handled in
3096 -- GNATprove.
3097
3098 when Pragma_Precondition
3099 | Pragma_Postcondition
3100 | Pragma_Contract_Cases
3101 | Pragma_Refined_Post
3102 =>
3103 null;
3104
3105 -- The same holds for the initial condition after package
3106 -- elaboration, for the different reason that library-level
3107 -- variables can only be left in RW state after elaboration.
3108
3109 when Pragma_Initial_Condition =>
3110 null;
3111
3112 -- These pragmas should have been rewritten and/or removed in
3113 -- GNATprove mode.
3114
3115 when Pragma_Assert
3116 | Pragma_Assert_And_Cut
3117 | Pragma_Assume
3118 | Pragma_Compile_Time_Error
3119 | Pragma_Compile_Time_Warning
3120 | Pragma_Debug
3121 | Pragma_Loop_Invariant
3122 =>
3123 raise Program_Error;
3124
3125 when others =>
3126 null;
3127 end case;
3128 end Check_Pragma;
3129
3130 -------------------------
3131 -- Check_Safe_Pointers --
3132 -------------------------
3133
3134 procedure Check_Safe_Pointers (N : Node_Id) is
3135
3136 -- Local subprograms
3137
3138 procedure Check_List (L : List_Id);
3139 -- Call the main analysis procedure on each element of the list
3140
3141 procedure Initialize;
3142 -- Initialize global variables before starting the analysis of a body
3143
3144 ----------------
3145 -- Check_List --
3146 ----------------
3147
3148 procedure Check_List (L : List_Id) is
3149 N : Node_Id;
3150 begin
3151 N := First (L);
3152 while Present (N) loop
3153 Check_Safe_Pointers (N);
3154 Next (N);
3155 end loop;
3156 end Check_List;
3157
3158 ----------------
3159 -- Initialize --
3160 ----------------
3161
3162 procedure Initialize is
3163 begin
3164 Reset (Current_Loops_Envs);
3165 Reset (Current_Loops_Accumulators);
3166 Reset (Current_Perm_Env);
3167 end Initialize;
3168
3169 -- Start of processing for Check_Safe_Pointers
3170
3171 begin
3172 Initialize;
3173
3174 case Nkind (N) is
3175 when N_Compilation_Unit =>
3176 Check_Safe_Pointers (Unit (N));
3177
3178 when N_Package_Body
3179 | N_Package_Declaration
3180 | N_Subprogram_Declaration
3181 | N_Subprogram_Body
3182 =>
3183 declare
3184 E : constant Entity_Id := Defining_Entity (N);
3185 Prag : constant Node_Id := SPARK_Pragma (E);
3186 -- SPARK_Mode pragma in application
3187
3188 begin
3189 if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then
3190 null;
3191
3192 elsif Present (Prag) then
3193 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then
3194 Check_Node (N);
3195 end if;
3196
3197 elsif Nkind (N) = N_Package_Body then
3198 Check_List (Declarations (N));
3199
3200 elsif Nkind (N) = N_Package_Declaration then
3201 Check_List (Private_Declarations (Specification (N)));
3202 Check_List (Visible_Declarations (Specification (N)));
3203 end if;
3204 end;
3205
3206 when others =>
3207 null;
3208 end case;
3209 end Check_Safe_Pointers;
3210
3211 ---------------------------------------
3212 -- Check_Source_Of_Borrow_Or_Observe --
3213 ---------------------------------------
3214
3215 procedure Check_Source_Of_Borrow_Or_Observe
3216 (Expr : Node_Id;
3217 Status : out Error_Status)
3218 is
3219 Root : Entity_Id;
3220
3221 begin
3222 if Is_Path_Expression (Expr) then
3223 Root := Get_Root_Object (Expr);
3224 else
3225 Root := Empty;
3226 end if;
3227
3228 Status := OK;
3229
3230 -- SPARK RM 3.10(3): If the target of an assignment operation is an
3231 -- object of an anonymous access-to-object type (including copy-in for
3232 -- a parameter), then the source shall be a name denoting a part of a
3233 -- stand-alone object, a part of a parameter, or a call to a traversal
3234 -- function.
3235
3236 if No (Root) then
3237 if Emit_Messages then
3238 if Nkind (Expr) = N_Function_Call then
3239 Error_Msg_N
3240 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3241 Error_Msg_N
3242 ("\function called must be a traversal function", Expr);
3243 else
3244 Error_Msg_N
3245 ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
3246 Error_Msg_N
3247 ("\expression must be part of stand-alone object or " &
3248 "parameter",
3249 Expr);
3250 end if;
3251 end if;
3252
3253 Status := Error;
3254 end if;
3255 end Check_Source_Of_Borrow_Or_Observe;
3256
3257 ---------------------
3258 -- Check_Statement --
3259 ---------------------
3260
3261 procedure Check_Statement (Stmt : Node_Id) is
3262 begin
3263 case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is
3264
3265 -- An entry call is handled like other calls
3266
3267 when N_Entry_Call_Statement =>
3268 Check_Call_Statement (Stmt);
3269
3270 -- An assignment may correspond to a move, a borrow, or an observe
3271
3272 when N_Assignment_Statement =>
3273 declare
3274 Target : constant Node_Id := Name (Stmt);
3275
3276 begin
3277 -- Start with checking that the subexpressions of the target
3278 -- path are readable, before possibly updating the permission
3279 -- of these subexpressions in Check_Assignment.
3280
3281 Check_Expression (Target, Read_Subexpr);
3282
3283 Check_Assignment (Target => Target,
3284 Expr => Expression (Stmt));
3285
3286 -- ??? We need a rule that forbids targets of assignment for
3287 -- which the path is not known, for example when there is a
3288 -- function call involved (which includes calls to traversal
3289 -- functions). Otherwise there is no way to update the
3290 -- corresponding path permission.
3291
3292 if No (Get_Root_Object
3293 (Target, Through_Traversal => False))
3294 then
3295 if Emit_Messages then
3296 Error_Msg_N ("illegal target for assignment", Target);
3297 end if;
3298 return;
3299 end if;
3300
3301 Check_Expression (Target, Assign);
3302 end;
3303
3304 when N_Block_Statement =>
3305 Check_List (Declarations (Stmt));
3306 Check_Node (Handled_Statement_Sequence (Stmt));
3307
3308 -- Remove local borrowers and observers
3309
3310 declare
3311 Decl : Node_Id := First (Declarations (Stmt));
3312 Var : Entity_Id;
3313 begin
3314 while Present (Decl) loop
3315 if Nkind (Decl) = N_Object_Declaration then
3316 Var := Defining_Identifier (Decl);
3317 Remove (Current_Borrowers, Var);
3318 Remove (Current_Observers, Var);
3319 end if;
3320
3321 Next (Decl);
3322 end loop;
3323 end;
3324
3325 when N_Case_Statement =>
3326 declare
3327 Alt : Node_Id;
3328 Saved_Env : Perm_Env;
3329 -- Copy of environment for analysis of the different cases
3330 New_Env : Perm_Env;
3331 -- Accumulator for the different cases
3332
3333 begin
3334 Check_Expression (Expression (Stmt), Read);
3335
3336 -- Save environment
3337
3338 Copy_Env (Current_Perm_Env, Saved_Env);
3339
3340 -- First alternative
3341
3342 Alt := First (Alternatives (Stmt));
3343 Check_List (Statements (Alt));
3344 Next (Alt);
3345
3346 -- Cleanup
3347
3348 Move_Env (Current_Perm_Env, New_Env);
3349
3350 -- Other alternatives
3351
3352 while Present (Alt) loop
3353
3354 -- Restore environment
3355
3356 Copy_Env (Saved_Env, Current_Perm_Env);
3357
3358 -- Next alternative
3359
3360 Check_List (Statements (Alt));
3361 Next (Alt);
3362
3363 -- Merge Current_Perm_Env into New_Env
3364
3365 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3366 end loop;
3367
3368 Move_Env (New_Env, Current_Perm_Env);
3369 Free_Env (Saved_Env);
3370 end;
3371
3372 when N_Delay_Relative_Statement
3373 | N_Delay_Until_Statement
3374 =>
3375 Check_Expression (Expression (Stmt), Read);
3376
3377 when N_Loop_Statement =>
3378 Check_Loop_Statement (Stmt);
3379
3380 when N_Simple_Return_Statement =>
3381 declare
3382 Subp : constant Entity_Id :=
3383 Return_Applies_To (Return_Statement_Entity (Stmt));
3384 Expr : constant Node_Id := Expression (Stmt);
3385 begin
3386 if Present (Expression (Stmt)) then
3387 declare
3388 Return_Typ : constant Entity_Id :=
3389 Etype (Expression (Stmt));
3390
3391 begin
3392 -- SPARK RM 3.10(5): A return statement that applies
3393 -- to a traversal function that has an anonymous
3394 -- access-to-constant (respectively, access-to-variable)
3395 -- result type, shall return either the literal null
3396 -- or an access object denoted by a direct or indirect
3397 -- observer (respectively, borrower) of the traversed
3398 -- parameter.
3399
3400 if Is_Anonymous_Access_Type (Return_Typ) then
3401 pragma Assert (Is_Traversal_Function (Subp));
3402
3403 if Nkind (Expr) /= N_Null then
3404 declare
3405 Expr_Root : constant Entity_Id :=
3406 Get_Root_Object (Expr, Is_Traversal => True);
3407 Param : constant Entity_Id :=
3408 First_Formal (Subp);
3409 begin
3410 if Param /= Expr_Root and then Emit_Messages then
3411 Error_Msg_NE
3412 ("returned value must be rooted in "
3413 & "traversed parameter & "
3414 & "(SPARK RM 3.10(5))",
3415 Stmt, Param);
3416 end if;
3417 end;
3418 end if;
3419
3420 -- Move expression to caller
3421
3422 elsif Is_Deep (Return_Typ) then
3423
3424 if Is_Path_Expression (Expr) then
3425 Check_Expression (Expr, Move);
3426
3427 else
3428 if Emit_Messages then
3429 Error_Msg_N
3430 ("expression not allowed as source of move",
3431 Expr);
3432 end if;
3433 return;
3434 end if;
3435
3436 else
3437 Check_Expression (Expr, Read);
3438 end if;
3439
3440 if Ekind_In (Subp, E_Procedure, E_Entry)
3441 and then not No_Return (Subp)
3442 then
3443 Return_Parameters (Subp);
3444 Return_Globals (Subp);
3445 end if;
3446 end;
3447 end if;
3448 end;
3449
3450 when N_Extended_Return_Statement =>
3451 declare
3452 Subp : constant Entity_Id :=
3453 Return_Applies_To (Return_Statement_Entity (Stmt));
3454 Decls : constant List_Id := Return_Object_Declarations (Stmt);
3455 Decl : constant Node_Id := Last_Non_Pragma (Decls);
3456 Obj : constant Entity_Id := Defining_Identifier (Decl);
3457 Perm : Perm_Kind;
3458
3459 begin
3460 -- SPARK RM 3.10(5): return statement of traversal function
3461
3462 if Is_Traversal_Function (Subp) and then Emit_Messages then
3463 Error_Msg_N
3464 ("extended return cannot apply to a traversal function",
3465 Stmt);
3466 end if;
3467
3468 Check_List (Return_Object_Declarations (Stmt));
3469 Check_Node (Handled_Statement_Sequence (Stmt));
3470
3471 if Is_Deep (Etype (Obj)) then
3472 Perm := Get_Perm (Obj);
3473
3474 if Perm /= Read_Write then
3475 Perm_Error (Decl, Read_Write, Perm,
3476 Expl => Get_Expl (Obj));
3477 end if;
3478 end if;
3479
3480 if Ekind_In (Subp, E_Procedure, E_Entry)
3481 and then not No_Return (Subp)
3482 then
3483 Return_Parameters (Subp);
3484 Return_Globals (Subp);
3485 end if;
3486 end;
3487
3488 -- On loop exit, merge the current permission environment with the
3489 -- accumulator for the given loop.
3490
3491 when N_Exit_Statement =>
3492 declare
3493 Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt);
3494 Saved_Accumulator : constant Perm_Env_Access :=
3495 Get (Current_Loops_Accumulators, Loop_Name);
3496 Environment_Copy : constant Perm_Env_Access :=
3497 new Perm_Env;
3498 begin
3499 Copy_Env (Current_Perm_Env, Environment_Copy.all);
3500
3501 if Saved_Accumulator = null then
3502 Set (Current_Loops_Accumulators,
3503 Loop_Name, Environment_Copy);
3504 else
3505 Merge_Env (Source => Environment_Copy.all,
3506 Target => Saved_Accumulator.all);
3507 -- ??? Either free Environment_Copy, or change the type
3508 -- of loop accumulators to directly store permission
3509 -- environments.
3510 end if;
3511 end;
3512
3513 -- On branches, analyze each branch independently on a fresh copy of
3514 -- the permission environment, then merge the resulting permission
3515 -- environments.
3516
3517 when N_If_Statement =>
3518 declare
3519 Saved_Env : Perm_Env;
3520 New_Env : Perm_Env;
3521 -- Accumulator for the different branches
3522
3523 begin
3524 Check_Expression (Condition (Stmt), Read);
3525
3526 -- Save environment
3527
3528 Copy_Env (Current_Perm_Env, Saved_Env);
3529
3530 -- THEN branch
3531
3532 Check_List (Then_Statements (Stmt));
3533 Move_Env (Current_Perm_Env, New_Env);
3534
3535 -- ELSIF branches
3536
3537 declare
3538 Branch : Node_Id;
3539 begin
3540 Branch := First (Elsif_Parts (Stmt));
3541 while Present (Branch) loop
3542
3543 -- Restore current permission environment
3544
3545 Copy_Env (Saved_Env, Current_Perm_Env);
3546 Check_Expression (Condition (Branch), Read);
3547 Check_List (Then_Statements (Branch));
3548
3549 -- Merge current permission environment
3550
3551 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3552 Next (Branch);
3553 end loop;
3554 end;
3555
3556 -- ELSE branch
3557
3558 -- Restore current permission environment
3559
3560 Copy_Env (Saved_Env, Current_Perm_Env);
3561 Check_List (Else_Statements (Stmt));
3562
3563 -- Merge current permission environment
3564
3565 Merge_Env (Source => Current_Perm_Env, Target => New_Env);
3566
3567 -- Cleanup
3568
3569 Move_Env (New_Env, Current_Perm_Env);
3570 Free_Env (Saved_Env);
3571 end;
3572
3573 -- We should ideally ignore the branch after raising an exception,
3574 -- so that it is not taken into account in merges. For now, just
3575 -- propagate the current environment.
3576
3577 when N_Raise_Statement =>
3578 null;
3579
3580 when N_Null_Statement =>
3581 null;
3582
3583 -- Unsupported constructs in SPARK
3584
3585 when N_Abort_Statement
3586 | N_Accept_Statement
3587 | N_Asynchronous_Select
3588 | N_Code_Statement
3589 | N_Conditional_Entry_Call
3590 | N_Goto_Statement
3591 | N_Requeue_Statement
3592 | N_Selective_Accept
3593 | N_Timed_Entry_Call
3594 =>
3595 null;
3596
3597 -- The following nodes are never generated in GNATprove mode
3598
3599 when N_Compound_Statement
3600 | N_Free_Statement
3601 =>
3602 raise Program_Error;
3603 end case;
3604 end Check_Statement;
3605
3606 -------------------------
3607 -- Check_Type_Legality --
3608 -------------------------
3609
3610 procedure Check_Type_Legality
3611 (Typ : Entity_Id;
3612 Force : Boolean;
3613 Legal : in out Boolean)
3614 is
3615 function Original_Emit_Messages return Boolean renames Emit_Messages;
3616
3617 function Emit_Messages return Boolean;
3618 -- Local wrapper around generic formal parameter Emit_Messages, to
3619 -- check the value of parameter Force before calling the original
3620 -- Emit_Messages, and setting Legal to False.
3621
3622 -------------------
3623 -- Emit_Messages --
3624 -------------------
3625
3626 function Emit_Messages return Boolean is
3627 begin
3628 Legal := False;
3629 return Force and then Original_Emit_Messages;
3630 end Emit_Messages;
3631
3632 -- Local variables
3633
3634 Check_Typ : constant Entity_Id := Retysp (Typ);
3635
3636 -- Start of processing for Check_Type_Legality
3637
3638 begin
3639 case Type_Kind'(Ekind (Check_Typ)) is
3640 when Access_Kind =>
3641 case Access_Kind'(Ekind (Check_Typ)) is
3642 when E_Access_Type
3643 | E_Anonymous_Access_Type
3644 =>
3645 null;
3646 when E_Access_Subtype =>
3647 Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
3648 when E_Access_Attribute_Type =>
3649 if Emit_Messages then
3650 Error_Msg_N ("access attribute not allowed in SPARK",
3651 Check_Typ);
3652 end if;
3653 when E_Allocator_Type =>
3654 if Emit_Messages then
3655 Error_Msg_N ("missing type resolution", Check_Typ);
3656 end if;
3657 when E_General_Access_Type =>
3658 if Emit_Messages then
3659 Error_Msg_NE
3660 ("general access type & not allowed in SPARK",
3661 Check_Typ, Check_Typ);
3662 end if;
3663 when Access_Subprogram_Kind =>
3664 if Emit_Messages then
3665 Error_Msg_NE
3666 ("access to subprogram type & not allowed in SPARK",
3667 Check_Typ, Check_Typ);
3668 end if;
3669 end case;
3670
3671 when E_Array_Type
3672 | E_Array_Subtype
3673 =>
3674 Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
3675
3676 when Record_Kind =>
3677 if Is_Deep (Check_Typ)
3678 and then (Is_Tagged_Type (Check_Typ)
3679 or else Is_Class_Wide_Type (Check_Typ))
3680 then
3681 if Emit_Messages then
3682 Error_Msg_NE
3683 ("tagged type & cannot be owning in SPARK",
3684 Check_Typ, Check_Typ);
3685 end if;
3686
3687 else
3688 declare
3689 Comp : Entity_Id;
3690 begin
3691 Comp := First_Component_Or_Discriminant (Check_Typ);
3692 while Present (Comp) loop
3693
3694 -- Ignore components which are not visible in SPARK
3695
3696 if Component_Is_Visible_In_SPARK (Comp) then
3697 Check_Type_Legality (Etype (Comp), Force, Legal);
3698 end if;
3699 Next_Component_Or_Discriminant (Comp);
3700 end loop;
3701 end;
3702 end if;
3703
3704 when Scalar_Kind
3705 | E_String_Literal_Subtype
3706 | Protected_Kind
3707 | Task_Kind
3708 | Incomplete_Kind
3709 | E_Exception_Type
3710 | E_Subprogram_Type
3711 =>
3712 null;
3713
3714 -- Do not check type whose full view is not SPARK
3715
3716 when E_Private_Type
3717 | E_Private_Subtype
3718 | E_Limited_Private_Type
3719 | E_Limited_Private_Subtype
3720 =>
3721 null;
3722 end case;
3723 end Check_Type_Legality;
3724
3725 --------------
3726 -- Get_Expl --
3727 --------------
3728
3729 function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is
3730 begin
3731 -- Special case for the object declared in an extended return statement
3732
3733 if Nkind (N) = N_Defining_Identifier then
3734 declare
3735 C : constant Perm_Tree_Access :=
3736 Get (Current_Perm_Env, Unique_Entity (N));
3737 begin
3738 pragma Assert (C /= null);
3739 return Explanation (C);
3740 end;
3741
3742 -- The expression is a call to a traversal function
3743
3744 elsif Is_Traversal_Function_Call (N) then
3745 return N;
3746
3747 -- The expression is directly rooted in an object
3748
3749 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3750 declare
3751 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3752 begin
3753 case Tree_Or_Perm.R is
3754 when Folded =>
3755 return Tree_Or_Perm.Explanation;
3756
3757 when Unfolded =>
3758 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3759 return Explanation (Tree_Or_Perm.Tree_Access);
3760 end case;
3761 end;
3762
3763 -- The expression is a function call, an allocation, or null
3764
3765 else
3766 return N;
3767 end if;
3768 end Get_Expl;
3769
3770 -----------------------------------
3771 -- Get_Observed_Or_Borrowed_Expr --
3772 -----------------------------------
3773
3774 function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is
3775 begin
3776 if Is_Traversal_Function_Call (Expr) then
3777 return First_Actual (Expr);
3778 else
3779 return Expr;
3780 end if;
3781 end Get_Observed_Or_Borrowed_Expr;
3782
3783 --------------
3784 -- Get_Perm --
3785 --------------
3786
3787 function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is
3788 begin
3789 -- Special case for the object declared in an extended return statement
3790
3791 if Nkind (N) = N_Defining_Identifier then
3792 declare
3793 C : constant Perm_Tree_Access :=
3794 Get (Current_Perm_Env, Unique_Entity (N));
3795 begin
3796 pragma Assert (C /= null);
3797 return Permission (C);
3798 end;
3799
3800 -- The expression is a call to a traversal function
3801
3802 elsif Is_Traversal_Function_Call (N) then
3803 declare
3804 Callee : constant Entity_Id := Get_Called_Entity (N);
3805 begin
3806 if Is_Access_Constant (Etype (Callee)) then
3807 return Read_Only;
3808 else
3809 return Read_Write;
3810 end if;
3811 end;
3812
3813 -- The expression is directly rooted in an object
3814
3815 elsif Present (Get_Root_Object (N, Through_Traversal => False)) then
3816 declare
3817 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N);
3818 begin
3819 case Tree_Or_Perm.R is
3820 when Folded =>
3821 return Tree_Or_Perm.Found_Permission;
3822
3823 when Unfolded =>
3824 pragma Assert (Tree_Or_Perm.Tree_Access /= null);
3825 return Permission (Tree_Or_Perm.Tree_Access);
3826 end case;
3827 end;
3828
3829 -- The expression is a function call, an allocation, or null
3830
3831 else
3832 return Read_Write;
3833 end if;
3834 end Get_Perm;
3835
3836 ----------------------
3837 -- Get_Perm_Or_Tree --
3838 ----------------------
3839
3840 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is
3841 begin
3842 case Nkind (N) is
3843
3844 when N_Expanded_Name
3845 | N_Identifier
3846 =>
3847 declare
3848 C : constant Perm_Tree_Access :=
3849 Get (Current_Perm_Env, Unique_Entity (Entity (N)));
3850 begin
3851 -- Except during elaboration, the root object should have been
3852 -- declared and entered into the current permission
3853 -- environment.
3854
3855 if not Inside_Elaboration
3856 and then C = null
3857 then
3858 Illegal_Global_Usage (N, N);
3859 end if;
3860
3861 return (R => Unfolded, Tree_Access => C);
3862 end;
3863
3864 -- For a nonterminal path, we get the permission tree of its
3865 -- prefix, and then get the subtree associated with the extension,
3866 -- if unfolded. If folded, we return the permission associated with
3867 -- children.
3868
3869 when N_Explicit_Dereference
3870 | N_Indexed_Component
3871 | N_Selected_Component
3872 | N_Slice
3873 =>
3874 declare
3875 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N));
3876 begin
3877 case C.R is
3878
3879 -- Some earlier prefix was already folded, return the
3880 -- permission found.
3881
3882 when Folded =>
3883 return C;
3884
3885 when Unfolded =>
3886 case Kind (C.Tree_Access) is
3887
3888 -- If the prefix tree is already folded, return the
3889 -- children permission.
3890
3891 when Entire_Object =>
3892 return (R => Folded,
3893 Found_Permission =>
3894 Children_Permission (C.Tree_Access),
3895 Explanation =>
3896 Explanation (C.Tree_Access));
3897
3898 when Reference =>
3899 pragma Assert (Nkind (N) = N_Explicit_Dereference);
3900 return (R => Unfolded,
3901 Tree_Access => Get_All (C.Tree_Access));
3902
3903 when Record_Component =>
3904 pragma Assert (Nkind (N) = N_Selected_Component);
3905 declare
3906 Comp : constant Entity_Id :=
3907 Original_Record_Component
3908 (Entity (Selector_Name (N)));
3909 D : constant Perm_Tree_Access :=
3910 Perm_Tree_Maps.Get
3911 (Component (C.Tree_Access), Comp);
3912 begin
3913 pragma Assert (D /= null);
3914 return (R => Unfolded,
3915 Tree_Access => D);
3916 end;
3917
3918 when Array_Component =>
3919 pragma Assert (Nkind (N) = N_Indexed_Component
3920 or else
3921 Nkind (N) = N_Slice);
3922 pragma Assert (Get_Elem (C.Tree_Access) /= null);
3923 return (R => Unfolded,
3924 Tree_Access => Get_Elem (C.Tree_Access));
3925 end case;
3926 end case;
3927 end;
3928
3929 when N_Qualified_Expression
3930 | N_Type_Conversion
3931 | N_Unchecked_Type_Conversion
3932 =>
3933 return Get_Perm_Or_Tree (Expression (N));
3934
3935 when others =>
3936 raise Program_Error;
3937 end case;
3938 end Get_Perm_Or_Tree;
3939
3940 -------------------
3941 -- Get_Perm_Tree --
3942 -------------------
3943
3944 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is
3945 begin
3946 return Set_Perm_Prefixes (N, None, Empty);
3947 end Get_Perm_Tree;
3948
3949 ---------------------
3950 -- Get_Root_Object --
3951 ---------------------
3952
3953 function Get_Root_Object
3954 (Expr : Node_Id;
3955 Through_Traversal : Boolean := True;
3956 Is_Traversal : Boolean := False) return Entity_Id
3957 is
3958 function GRO (Expr : Node_Id) return Entity_Id;
3959 -- Local wrapper on the actual function, to propagate the values of
3960 -- optional parameters.
3961
3962 ---------
3963 -- GRO --
3964 ---------
3965
3966 function GRO (Expr : Node_Id) return Entity_Id is
3967 begin
3968 return Get_Root_Object (Expr, Through_Traversal, Is_Traversal);
3969 end GRO;
3970
3971 Get_Root_Object : Boolean;
3972 pragma Unmodified (Get_Root_Object);
3973 -- Local variable to mask the name of function Get_Root_Object, to
3974 -- prevent direct call. Instead GRO wrapper should be called.
3975
3976 -- Start of processing for Get_Root_Object
3977
3978 begin
3979 if not Is_Subpath_Expression (Expr, Is_Traversal) then
3980 if Emit_Messages then
3981 Error_Msg_N ("name expected here for path", Expr);
3982 end if;
3983 return Empty;
3984 end if;
3985
3986 case Nkind (Expr) is
3987 when N_Expanded_Name
3988 | N_Identifier
3989 =>
3990 return Entity (Expr);
3991
3992 when N_Explicit_Dereference
3993 | N_Indexed_Component
3994 | N_Selected_Component
3995 | N_Slice
3996 =>
3997 return GRO (Prefix (Expr));
3998
3999 -- There is no root object for an (extension) aggregate, allocator,
4000 -- concat, or NULL.
4001
4002 when N_Aggregate
4003 | N_Allocator
4004 | N_Extension_Aggregate
4005 | N_Null
4006 | N_Op_Concat
4007 =>
4008 return Empty;
4009
4010 -- In the case of a call to a traversal function, the root object is
4011 -- the root of the traversed parameter. Otherwise there is no root
4012 -- object.
4013
4014 when N_Function_Call =>
4015 if Through_Traversal
4016 and then Is_Traversal_Function_Call (Expr)
4017 then
4018 return GRO (First_Actual (Expr));
4019 else
4020 return Empty;
4021 end if;
4022
4023 when N_Qualified_Expression
4024 | N_Type_Conversion
4025 | N_Unchecked_Type_Conversion
4026 =>
4027 return GRO (Expression (Expr));
4028
4029 when N_Attribute_Reference =>
4030 pragma Assert
4031 (Get_Attribute_Id (Attribute_Name (Expr)) =
4032 Attribute_Loop_Entry
4033 or else
4034 Get_Attribute_Id (Attribute_Name (Expr)) =
4035 Attribute_Update
4036 or else Get_Attribute_Id (Attribute_Name (Expr)) =
4037 Attribute_Image);
4038 return Empty;
4039
4040 when N_If_Expression =>
4041 if Is_Traversal then
4042 declare
4043 Cond : constant Node_Id := First (Expressions (Expr));
4044 Then_Part : constant Node_Id := Next (Cond);
4045 Else_Part : constant Node_Id := Next (Then_Part);
4046 Then_Root : constant Entity_Id := GRO (Then_Part);
4047 Else_Root : constant Entity_Id := GRO (Else_Part);
4048 begin
4049 if Nkind (Then_Part) = N_Null then
4050 return Else_Root;
4051 elsif Nkind (Else_Part) = N_Null then
4052 return Then_Part;
4053 elsif Then_Root = Else_Root then
4054 return Then_Root;
4055 else
4056 if Emit_Messages then
4057 Error_Msg_N
4058 ("same name expected here in each branch", Expr);
4059 end if;
4060 return Empty;
4061 end if;
4062 end;
4063 else
4064 if Emit_Messages then
4065 Error_Msg_N ("name expected here for path", Expr);
4066 end if;
4067 return Empty;
4068 end if;
4069
4070 when N_Case_Expression =>
4071 if Is_Traversal then
4072 declare
4073 Cases : constant List_Id := Alternatives (Expr);
4074 Cur_Case : Node_Id := First (Cases);
4075 Cur_Root : Entity_Id;
4076 Common_Root : Entity_Id := Empty;
4077
4078 begin
4079 while Present (Cur_Case) loop
4080 Cur_Root := GRO (Expression (Cur_Case));
4081
4082 if Common_Root = Empty then
4083 Common_Root := Cur_Root;
4084 elsif Common_Root /= Cur_Root then
4085 if Emit_Messages then
4086 Error_Msg_N
4087 ("same name expected here in each branch", Expr);
4088 end if;
4089 return Empty;
4090 end if;
4091 Next (Cur_Case);
4092 end loop;
4093
4094 return Common_Root;
4095 end;
4096 else
4097 if Emit_Messages then
4098 Error_Msg_N ("name expected here for path", Expr);
4099 end if;
4100 return Empty;
4101 end if;
4102
4103 when others =>
4104 raise Program_Error;
4105 end case;
4106 end Get_Root_Object;
4107
4108 ---------
4109 -- Glb --
4110 ---------
4111
4112 function Glb (P1, P2 : Perm_Kind) return Perm_Kind
4113 is
4114 begin
4115 case P1 is
4116 when No_Access =>
4117 return No_Access;
4118
4119 when Read_Only =>
4120 case P2 is
4121 when No_Access
4122 | Write_Only
4123 =>
4124 return No_Access;
4125
4126 when Read_Perm =>
4127 return Read_Only;
4128 end case;
4129
4130 when Write_Only =>
4131 case P2 is
4132 when No_Access
4133 | Read_Only
4134 =>
4135 return No_Access;
4136
4137 when Write_Perm =>
4138 return Write_Only;
4139 end case;
4140
4141 when Read_Write =>
4142 return P2;
4143 end case;
4144 end Glb;
4145
4146 -------------------------
4147 -- Has_Array_Component --
4148 -------------------------
4149
4150 function Has_Array_Component (Expr : Node_Id) return Boolean is
4151 begin
4152 case Nkind (Expr) is
4153 when N_Expanded_Name
4154 | N_Identifier
4155 =>
4156 return False;
4157
4158 when N_Explicit_Dereference
4159 | N_Selected_Component
4160 =>
4161 return Has_Array_Component (Prefix (Expr));
4162
4163 when N_Indexed_Component
4164 | N_Slice
4165 =>
4166 return True;
4167
4168 when N_Allocator
4169 | N_Null
4170 | N_Function_Call
4171 =>
4172 return False;
4173
4174 when N_Qualified_Expression
4175 | N_Type_Conversion
4176 | N_Unchecked_Type_Conversion
4177 =>
4178 return Has_Array_Component (Expression (Expr));
4179
4180 when others =>
4181 raise Program_Error;
4182 end case;
4183 end Has_Array_Component;
4184
4185 --------
4186 -- Hp --
4187 --------
4188
4189 procedure Hp (P : Perm_Env) is
4190 Elem : Perm_Tree_Maps.Key_Option;
4191
4192 begin
4193 Elem := Get_First_Key (P);
4194 while Elem.Present loop
4195 Print_Node_Briefly (Elem.K);
4196 Elem := Get_Next_Key (P);
4197 end loop;
4198 end Hp;
4199
4200 --------------------------
4201 -- Illegal_Global_Usage --
4202 --------------------------
4203
4204 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id; E : Entity_Id)
4205 is
4206 begin
4207 Error_Msg_NE ("cannot use global variable & of deep type", N, E);
4208 Error_Msg_N ("\without prior declaration in a Global aspect", N);
4209 Errout.Finalize (Last_Call => True);
4210 Errout.Output_Messages;
4211 Exit_Program (E_Errors);
4212 end Illegal_Global_Usage;
4213
4214 -------------
4215 -- Is_Deep --
4216 -------------
4217
4218 function Is_Deep (Typ : Entity_Id) return Boolean is
4219 begin
4220 case Type_Kind'(Ekind (Retysp (Typ))) is
4221 when Access_Kind =>
4222 return True;
4223
4224 when E_Array_Type
4225 | E_Array_Subtype
4226 =>
4227 return Is_Deep (Component_Type (Retysp (Typ)));
4228
4229 when Record_Kind =>
4230 declare
4231 Comp : Entity_Id;
4232 begin
4233 Comp := First_Component_Or_Discriminant (Retysp (Typ));
4234 while Present (Comp) loop
4235
4236 -- Ignore components not visible in SPARK
4237
4238 if Component_Is_Visible_In_SPARK (Comp)
4239 and then Is_Deep (Etype (Comp))
4240 then
4241 return True;
4242 end if;
4243 Next_Component_Or_Discriminant (Comp);
4244 end loop;
4245 end;
4246 return False;
4247
4248 when Scalar_Kind
4249 | E_String_Literal_Subtype
4250 | Protected_Kind
4251 | Task_Kind
4252 | Incomplete_Kind
4253 | E_Exception_Type
4254 | E_Subprogram_Type
4255 =>
4256 return False;
4257
4258 -- Ignore full view of types if it is not in SPARK
4259
4260 when E_Private_Type
4261 | E_Private_Subtype
4262 | E_Limited_Private_Type
4263 | E_Limited_Private_Subtype
4264 =>
4265 return False;
4266 end case;
4267 end Is_Deep;
4268
4269 --------------
4270 -- Is_Legal --
4271 --------------
4272
4273 function Is_Legal (N : Node_Id) return Boolean is
4274 Legal : Boolean := True;
4275
4276 begin
4277 case Nkind (N) is
4278 when N_Declaration =>
4279 Check_Declaration_Legality (N, Force => False, Legal => Legal);
4280 when others =>
4281 null;
4282 end case;
4283
4284 return Legal;
4285 end Is_Legal;
4286
4287 ----------------------
4288 -- Is_Local_Context --
4289 ----------------------
4290
4291 function Is_Local_Context (Scop : Entity_Id) return Boolean is
4292 begin
4293 return Is_Subprogram_Or_Entry (Scop)
4294 or else Ekind (Scop) = E_Block;
4295 end Is_Local_Context;
4296
4297 ------------------------
4298 -- Is_Path_Expression --
4299 ------------------------
4300
4301 function Is_Path_Expression
4302 (Expr : Node_Id;
4303 Is_Traversal : Boolean := False) return Boolean
4304 is
4305 function IPE (Expr : Node_Id) return Boolean;
4306 -- Local wrapper on the actual function, to propagate the values of
4307 -- optional parameter Is_Traversal.
4308
4309 ---------
4310 -- IPE --
4311 ---------
4312
4313 function IPE (Expr : Node_Id) return Boolean is
4314 begin
4315 return Is_Path_Expression (Expr, Is_Traversal);
4316 end IPE;
4317
4318 Is_Path_Expression : Boolean;
4319 pragma Unmodified (Is_Path_Expression);
4320 -- Local variable to mask the name of function Is_Path_Expression, to
4321 -- prevent direct call. Instead IPE wrapper should be called.
4322
4323 -- Start of processing for Is_Path_Expression
4324
4325 begin
4326 case Nkind (Expr) is
4327 when N_Expanded_Name
4328 | N_Explicit_Dereference
4329 | N_Identifier
4330 | N_Indexed_Component
4331 | N_Selected_Component
4332 | N_Slice
4333 =>
4334 return True;
4335
4336 -- Special value NULL corresponds to an empty path
4337
4338 when N_Null =>
4339 return True;
4340
4341 -- Object returned by an (extension) aggregate, an allocator, or
4342 -- a function call corresponds to a path.
4343
4344 when N_Aggregate
4345 | N_Allocator
4346 | N_Extension_Aggregate
4347 | N_Function_Call
4348 =>
4349 return True;
4350
4351 when N_Qualified_Expression
4352 | N_Type_Conversion
4353 | N_Unchecked_Type_Conversion
4354 =>
4355 return IPE (Expression (Expr));
4356
4357 -- When returning from a traversal function, consider an
4358 -- if-expression as a possible path expression.
4359
4360 when N_If_Expression =>
4361 if Is_Traversal then
4362 declare
4363 Cond : constant Node_Id := First (Expressions (Expr));
4364 Then_Part : constant Node_Id := Next (Cond);
4365 Else_Part : constant Node_Id := Next (Then_Part);
4366 begin
4367 return IPE (Then_Part)
4368 and then IPE (Else_Part);
4369 end;
4370 else
4371 return False;
4372 end if;
4373
4374 -- When returning from a traversal function, consider
4375 -- a case-expression as a possible path expression.
4376
4377 when N_Case_Expression =>
4378 if Is_Traversal then
4379 declare
4380 Cases : constant List_Id := Alternatives (Expr);
4381 Cur_Case : Node_Id := First (Cases);
4382
4383 begin
4384 while Present (Cur_Case) loop
4385 if not IPE (Expression (Cur_Case)) then
4386 return False;
4387 end if;
4388 Next (Cur_Case);
4389 end loop;
4390
4391 return True;
4392 end;
4393 else
4394 return False;
4395 end if;
4396
4397 when others =>
4398 return False;
4399 end case;
4400 end Is_Path_Expression;
4401
4402 -------------------------
4403 -- Is_Prefix_Or_Almost --
4404 -------------------------
4405
4406 function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is
4407
4408 type Expr_Array is array (Positive range <>) of Node_Id;
4409 -- Sequence of expressions that make up a path
4410
4411 function Get_Expr_Array (Expr : Node_Id) return Expr_Array;
4412 pragma Precondition (Is_Path_Expression (Expr));
4413 -- Return the sequence of expressions that make up a path
4414
4415 --------------------
4416 -- Get_Expr_Array --
4417 --------------------
4418
4419 function Get_Expr_Array (Expr : Node_Id) return Expr_Array is
4420 begin
4421 case Nkind (Expr) is
4422 when N_Expanded_Name
4423 | N_Identifier
4424 =>
4425 return Expr_Array'(1 => Expr);
4426
4427 when N_Explicit_Dereference
4428 | N_Indexed_Component
4429 | N_Selected_Component
4430 | N_Slice
4431 =>
4432 return Get_Expr_Array (Prefix (Expr)) & Expr;
4433
4434 when N_Qualified_Expression
4435 | N_Type_Conversion
4436 | N_Unchecked_Type_Conversion
4437 =>
4438 return Get_Expr_Array (Expression (Expr));
4439
4440 when others =>
4441 raise Program_Error;
4442 end case;
4443 end Get_Expr_Array;
4444
4445 -- Local variables
4446
4447 Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref);
4448 Expr_Path : constant Expr_Array := Get_Expr_Array (Expr);
4449
4450 Prefix_Root : constant Node_Id := Prefix_Path (1);
4451 Expr_Root : constant Node_Id := Expr_Path (1);
4452
4453 Common_Len : constant Positive :=
4454 Positive'Min (Prefix_Path'Length, Expr_Path'Length);
4455
4456 -- Start of processing for Is_Prefix_Or_Almost
4457
4458 begin
4459 if Entity (Prefix_Root) /= Entity (Expr_Root) then
4460 return False;
4461 end if;
4462
4463 for J in 2 .. Common_Len loop
4464 declare
4465 Prefix_Elt : constant Node_Id := Prefix_Path (J);
4466 Expr_Elt : constant Node_Id := Expr_Path (J);
4467 begin
4468 case Nkind (Prefix_Elt) is
4469 when N_Explicit_Dereference =>
4470 if Nkind (Expr_Elt) /= N_Explicit_Dereference then
4471 return False;
4472 end if;
4473
4474 when N_Selected_Component =>
4475 if Nkind (Expr_Elt) /= N_Selected_Component
4476 or else Original_Record_Component
4477 (Entity (Selector_Name (Prefix_Elt)))
4478 /= Original_Record_Component
4479 (Entity (Selector_Name (Expr_Elt)))
4480 then
4481 return False;
4482 end if;
4483
4484 when N_Indexed_Component
4485 | N_Slice
4486 =>
4487 if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then
4488 return False;
4489 end if;
4490
4491 when others =>
4492 raise Program_Error;
4493 end case;
4494 end;
4495 end loop;
4496
4497 -- If the expression path is longer than the prefix one, then at this
4498 -- point the prefix property holds.
4499
4500 if Expr_Path'Length > Prefix_Path'Length then
4501 return True;
4502
4503 -- Otherwise check if none of the remaining path elements in the
4504 -- candidate prefix involve a dereference.
4505
4506 else
4507 for J in Common_Len + 1 .. Prefix_Path'Length loop
4508 if Nkind (Prefix_Path (J)) = N_Explicit_Dereference then
4509 return False;
4510 end if;
4511 end loop;
4512
4513 return True;
4514 end if;
4515 end Is_Prefix_Or_Almost;
4516
4517 ---------------------------
4518 -- Is_Subpath_Expression --
4519 ---------------------------
4520
4521 function Is_Subpath_Expression
4522 (Expr : Node_Id;
4523 Is_Traversal : Boolean := False) return Boolean
4524 is
4525 begin
4526 return Is_Path_Expression (Expr, Is_Traversal)
4527
4528 or else (Nkind_In (Expr, N_Qualified_Expression,
4529 N_Type_Conversion,
4530 N_Unchecked_Type_Conversion)
4531 and then Is_Subpath_Expression (Expression (Expr)))
4532
4533 or else (Nkind (Expr) = N_Attribute_Reference
4534 and then
4535 (Get_Attribute_Id (Attribute_Name (Expr)) =
4536 Attribute_Update
4537 or else
4538 Get_Attribute_Id (Attribute_Name (Expr)) =
4539 Attribute_Loop_Entry
4540 or else
4541 Get_Attribute_Id (Attribute_Name (Expr)) =
4542 Attribute_Image))
4543
4544 or else Nkind (Expr) = N_Op_Concat;
4545 end Is_Subpath_Expression;
4546
4547 ---------------------------
4548 -- Is_Traversal_Function --
4549 ---------------------------
4550
4551 function Is_Traversal_Function (E : Entity_Id) return Boolean is
4552 begin
4553 return Ekind (E) = E_Function
4554
4555 -- A function is said to be a traversal function if the result type of
4556 -- the function is an anonymous access-to-object type,
4557
4558 and then Is_Anonymous_Access_Type (Etype (E))
4559
4560 -- the function has at least one formal parameter,
4561
4562 and then Present (First_Formal (E))
4563
4564 -- and the function's first parameter is of an access type.
4565
4566 and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
4567 end Is_Traversal_Function;
4568
4569 --------------------------------
4570 -- Is_Traversal_Function_Call --
4571 --------------------------------
4572
4573 function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is
4574 begin
4575 return Nkind (Expr) = N_Function_Call
4576 and then Present (Get_Called_Entity (Expr))
4577 and then Is_Traversal_Function (Get_Called_Entity (Expr));
4578 end Is_Traversal_Function_Call;
4579
4580 ------------------
4581 -- Loop_Of_Exit --
4582 ------------------
4583
4584 function Loop_Of_Exit (N : Node_Id) return Entity_Id is
4585 Nam : Node_Id := Name (N);
4586 Stmt : Node_Id := N;
4587 begin
4588 if No (Nam) then
4589 while Present (Stmt) loop
4590 Stmt := Parent (Stmt);
4591 if Nkind (Stmt) = N_Loop_Statement then
4592 Nam := Identifier (Stmt);
4593 exit;
4594 end if;
4595 end loop;
4596 end if;
4597 return Entity (Nam);
4598 end Loop_Of_Exit;
4599
4600 ---------
4601 -- Lub --
4602 ---------
4603
4604 function Lub (P1, P2 : Perm_Kind) return Perm_Kind is
4605 begin
4606 case P1 is
4607 when No_Access =>
4608 return P2;
4609
4610 when Read_Only =>
4611 case P2 is
4612 when No_Access
4613 | Read_Only
4614 =>
4615 return Read_Only;
4616
4617 when Write_Perm =>
4618 return Read_Write;
4619 end case;
4620
4621 when Write_Only =>
4622 case P2 is
4623 when No_Access
4624 | Write_Only
4625 =>
4626 return Write_Only;
4627
4628 when Read_Perm =>
4629 return Read_Write;
4630 end case;
4631
4632 when Read_Write =>
4633 return Read_Write;
4634 end case;
4635 end Lub;
4636
4637 ---------------
4638 -- Merge_Env --
4639 ---------------
4640
4641 procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is
4642
4643 -- Local subprograms
4644
4645 procedure Apply_Glb_Tree
4646 (A : Perm_Tree_Access;
4647 P : Perm_Kind);
4648
4649 procedure Merge_Trees
4650 (Target : Perm_Tree_Access;
4651 Source : Perm_Tree_Access);
4652
4653 --------------------
4654 -- Apply_Glb_Tree --
4655 --------------------
4656
4657 procedure Apply_Glb_Tree
4658 (A : Perm_Tree_Access;
4659 P : Perm_Kind)
4660 is
4661 begin
4662 A.all.Tree.Permission := Glb (Permission (A), P);
4663
4664 case Kind (A) is
4665 when Entire_Object =>
4666 A.all.Tree.Children_Permission :=
4667 Glb (Children_Permission (A), P);
4668
4669 when Reference =>
4670 Apply_Glb_Tree (Get_All (A), P);
4671
4672 when Array_Component =>
4673 Apply_Glb_Tree (Get_Elem (A), P);
4674
4675 when Record_Component =>
4676 declare
4677 Comp : Perm_Tree_Access;
4678 begin
4679 Comp := Perm_Tree_Maps.Get_First (Component (A));
4680 while Comp /= null loop
4681 Apply_Glb_Tree (Comp, P);
4682 Comp := Perm_Tree_Maps.Get_Next (Component (A));
4683 end loop;
4684 end;
4685 end case;
4686 end Apply_Glb_Tree;
4687
4688 -----------------
4689 -- Merge_Trees --
4690 -----------------
4691
4692 procedure Merge_Trees
4693 (Target : Perm_Tree_Access;
4694 Source : Perm_Tree_Access)
4695 is
4696 Perm : constant Perm_Kind :=
4697 Glb (Permission (Target), Permission (Source));
4698
4699 begin
4700 pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source));
4701 Target.all.Tree.Permission := Perm;
4702
4703 case Kind (Target) is
4704 when Entire_Object =>
4705 declare
4706 Child_Perm : constant Perm_Kind :=
4707 Children_Permission (Target);
4708
4709 begin
4710 case Kind (Source) is
4711 when Entire_Object =>
4712 Target.all.Tree.Children_Permission :=
4713 Glb (Child_Perm, Children_Permission (Source));
4714
4715 when Reference =>
4716 Copy_Tree (Source, Target);
4717 Target.all.Tree.Permission := Perm;
4718 Apply_Glb_Tree (Get_All (Target), Child_Perm);
4719
4720 when Array_Component =>
4721 Copy_Tree (Source, Target);
4722 Target.all.Tree.Permission := Perm;
4723 Apply_Glb_Tree (Get_Elem (Target), Child_Perm);
4724
4725 when Record_Component =>
4726 Copy_Tree (Source, Target);
4727 Target.all.Tree.Permission := Perm;
4728 declare
4729 Comp : Perm_Tree_Access;
4730
4731 begin
4732 Comp :=
4733 Perm_Tree_Maps.Get_First (Component (Target));
4734 while Comp /= null loop
4735 -- Apply glb tree on every component subtree
4736
4737 Apply_Glb_Tree (Comp, Child_Perm);
4738 Comp := Perm_Tree_Maps.Get_Next
4739 (Component (Target));
4740 end loop;
4741 end;
4742 end case;
4743 end;
4744
4745 when Reference =>
4746 case Kind (Source) is
4747 when Entire_Object =>
4748 Apply_Glb_Tree (Get_All (Target),
4749 Children_Permission (Source));
4750
4751 when Reference =>
4752 Merge_Trees (Get_All (Target), Get_All (Source));
4753
4754 when others =>
4755 raise Program_Error;
4756
4757 end case;
4758
4759 when Array_Component =>
4760 case Kind (Source) is
4761 when Entire_Object =>
4762 Apply_Glb_Tree (Get_Elem (Target),
4763 Children_Permission (Source));
4764
4765 when Array_Component =>
4766 Merge_Trees (Get_Elem (Target), Get_Elem (Source));
4767
4768 when others =>
4769 raise Program_Error;
4770
4771 end case;
4772
4773 when Record_Component =>
4774 case Kind (Source) is
4775 when Entire_Object =>
4776 declare
4777 Child_Perm : constant Perm_Kind :=
4778 Children_Permission (Source);
4779
4780 Comp : Perm_Tree_Access;
4781
4782 begin
4783 Comp := Perm_Tree_Maps.Get_First
4784 (Component (Target));
4785 while Comp /= null loop
4786 -- Apply glb tree on every component subtree
4787
4788 Apply_Glb_Tree (Comp, Child_Perm);
4789 Comp :=
4790 Perm_Tree_Maps.Get_Next (Component (Target));
4791 end loop;
4792 end;
4793
4794 when Record_Component =>
4795 declare
4796 Key_Source : Perm_Tree_Maps.Key_Option;
4797 CompTarget : Perm_Tree_Access;
4798 CompSource : Perm_Tree_Access;
4799
4800 begin
4801 Key_Source := Perm_Tree_Maps.Get_First_Key
4802 (Component (Source));
4803
4804 while Key_Source.Present loop
4805 CompSource := Perm_Tree_Maps.Get
4806 (Component (Source), Key_Source.K);
4807 CompTarget := Perm_Tree_Maps.Get
4808 (Component (Target), Key_Source.K);
4809
4810 pragma Assert (CompSource /= null);
4811 Merge_Trees (CompTarget, CompSource);
4812
4813 Key_Source := Perm_Tree_Maps.Get_Next_Key
4814 (Component (Source));
4815 end loop;
4816 end;
4817
4818 when others =>
4819 raise Program_Error;
4820 end case;
4821 end case;
4822 end Merge_Trees;
4823
4824 -- Local variables
4825
4826 CompTarget : Perm_Tree_Access;
4827 CompSource : Perm_Tree_Access;
4828 KeyTarget : Perm_Tree_Maps.Key_Option;
4829
4830 -- Start of processing for Merge_Env
4831
4832 begin
4833 KeyTarget := Get_First_Key (Target);
4834 -- Iterate over every tree of the environment in the target, and merge
4835 -- it with the source if there is such a similar one that exists. If
4836 -- there is none, then skip.
4837 while KeyTarget.Present loop
4838
4839 CompSource := Get (Source, KeyTarget.K);
4840 CompTarget := Get (Target, KeyTarget.K);
4841
4842 pragma Assert (CompTarget /= null);
4843
4844 if CompSource /= null then
4845 Merge_Trees (CompTarget, CompSource);
4846 Remove (Source, KeyTarget.K);
4847 end if;
4848
4849 KeyTarget := Get_Next_Key (Target);
4850 end loop;
4851
4852 -- Iterate over every tree of the environment of the source. And merge
4853 -- again. If there is not any tree of the target then just copy the tree
4854 -- from source to target.
4855 declare
4856 KeySource : Perm_Tree_Maps.Key_Option;
4857 begin
4858 KeySource := Get_First_Key (Source);
4859 while KeySource.Present loop
4860
4861 CompSource := Get (Source, KeySource.K);
4862 CompTarget := Get (Target, KeySource.K);
4863
4864 if CompTarget = null then
4865 CompTarget := new Perm_Tree_Wrapper'(CompSource.all);
4866 Copy_Tree (CompSource, CompTarget);
4867 Set (Target, KeySource.K, CompTarget);
4868 else
4869 Merge_Trees (CompTarget, CompSource);
4870 end if;
4871
4872 KeySource := Get_Next_Key (Source);
4873 end loop;
4874 end;
4875
4876 Free_Env (Source);
4877 end Merge_Env;
4878
4879 ----------------
4880 -- Perm_Error --
4881 ----------------
4882
4883 procedure Perm_Error
4884 (N : Node_Id;
4885 Perm : Perm_Kind;
4886 Found_Perm : Perm_Kind;
4887 Expl : Node_Id;
4888 Forbidden_Perm : Boolean := False)
4889 is
4890 procedure Set_Root_Object
4891 (Path : Node_Id;
4892 Obj : out Entity_Id;
4893 Deref : out Boolean);
4894 -- Set the root object Obj, and whether the path contains a dereference,
4895 -- from a path Path.
4896
4897 ---------------------
4898 -- Set_Root_Object --
4899 ---------------------
4900
4901 procedure Set_Root_Object
4902 (Path : Node_Id;
4903 Obj : out Entity_Id;
4904 Deref : out Boolean)
4905 is
4906 begin
4907 case Nkind (Path) is
4908 when N_Identifier
4909 | N_Expanded_Name
4910 =>
4911 Obj := Entity (Path);
4912 Deref := False;
4913
4914 when N_Type_Conversion
4915 | N_Unchecked_Type_Conversion
4916 | N_Qualified_Expression
4917 =>
4918 Set_Root_Object (Expression (Path), Obj, Deref);
4919
4920 when N_Indexed_Component
4921 | N_Selected_Component
4922 | N_Slice
4923 =>
4924 Set_Root_Object (Prefix (Path), Obj, Deref);
4925
4926 when N_Explicit_Dereference =>
4927 Set_Root_Object (Prefix (Path), Obj, Deref);
4928 Deref := True;
4929
4930 when others =>
4931 raise Program_Error;
4932 end case;
4933 end Set_Root_Object;
4934 -- Local variables
4935
4936 Root : Entity_Id;
4937 Is_Deref : Boolean;
4938
4939 -- Start of processing for Perm_Error
4940
4941 begin
4942 Set_Root_Object (N, Root, Is_Deref);
4943
4944 if Emit_Messages then
4945 if Is_Deref then
4946 Error_Msg_NE
4947 ("insufficient permission on dereference from &", N, Root);
4948 else
4949 Error_Msg_NE ("insufficient permission for &", N, Root);
4950 end if;
4951
4952 Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
4953 end if;
4954 end Perm_Error;
4955
4956 -------------------------------
4957 -- Perm_Error_Subprogram_End --
4958 -------------------------------
4959
4960 procedure Perm_Error_Subprogram_End
4961 (E : Entity_Id;
4962 Subp : Entity_Id;
4963 Perm : Perm_Kind;
4964 Found_Perm : Perm_Kind;
4965 Expl : Node_Id)
4966 is
4967 begin
4968 if Emit_Messages then
4969 Error_Msg_Node_2 := Subp;
4970 Error_Msg_NE ("insufficient permission for & when returning from &",
4971 Subp, E);
4972 Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
4973 end if;
4974 end Perm_Error_Subprogram_End;
4975
4976 ------------------
4977 -- Process_Path --
4978 ------------------
4979
4980 procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is
4981
4982 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id);
4983 -- Check expression Expr originating in Root was not borrowed
4984
4985 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id);
4986 -- Check expression Expr originating in Root was not observed
4987
4988 ------------------------
4989 -- Check_Not_Borrowed --
4990 ------------------------
4991
4992 procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is
4993 begin
4994 -- An expression without root object cannot be borrowed
4995
4996 if No (Root) then
4997 return;
4998 end if;
4999
5000 -- Otherwise, try to match the expression with one of the borrowed
5001 -- expressions.
5002
5003 declare
5004 Key : Variable_Maps.Key_Option :=
5005 Get_First_Key (Current_Borrowers);
5006 Var : Entity_Id;
5007 Borrowed : Node_Id;
5008 B_Pledge : Entity_Id := Empty;
5009
5010 begin
5011 -- Search for a call to a pledge function or a global pragma in
5012 -- the parents of Expr.
5013
5014 declare
5015 Call : Node_Id := Expr;
5016 begin
5017 while Present (Call)
5018 and then
5019 (Nkind (Call) /= N_Function_Call
5020 or else not Is_Pledge_Function (Get_Called_Entity (Call)))
5021 loop
5022 -- Do not check for borrowed objects in global contracts
5023 -- ??? However we should keep these objects in the borrowed
5024 -- state when verifying the subprogram so that we can make
5025 -- sure that they are only read inside pledges.
5026 -- ??? There is probably a better way to disable checking of
5027 -- borrows inside global contracts.
5028
5029 if Nkind (Call) = N_Pragma
5030 and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global
5031 then
5032 return;
5033 end if;
5034
5035 Call := Parent (Call);
5036 end loop;
5037
5038 if Present (Call)
5039 and then Nkind (First_Actual (Call)) in N_Has_Entity
5040 then
5041 B_Pledge := Entity (First_Actual (Call));
5042 end if;
5043 end;
5044
5045 while Key.Present loop
5046 Var := Key.K;
5047 Borrowed := Get (Current_Borrowers, Var);
5048
5049 if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
5050 and then Var /= B_Pledge
5051 and then Emit_Messages
5052 then
5053 Error_Msg_Sloc := Sloc (Borrowed);
5054 Error_Msg_N ("object was borrowed #", Expr);
5055 end if;
5056
5057 Key := Get_Next_Key (Current_Borrowers);
5058 end loop;
5059 end;
5060 end Check_Not_Borrowed;
5061
5062 ------------------------
5063 -- Check_Not_Observed --
5064 ------------------------
5065
5066 procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is
5067 begin
5068 -- An expression without root object cannot be observed
5069
5070 if No (Root) then
5071 return;
5072 end if;
5073
5074 -- Otherwise, try to match the expression with one of the observed
5075 -- expressions.
5076
5077 declare
5078 Key : Variable_Maps.Key_Option :=
5079 Get_First_Key (Current_Observers);
5080 Var : Entity_Id;
5081 Observed : Node_Id;
5082
5083 begin
5084 while Key.Present loop
5085 Var := Key.K;
5086 Observed := Get (Current_Observers, Var);
5087
5088 if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr)
5089 and then Emit_Messages
5090 then
5091 Error_Msg_Sloc := Sloc (Observed);
5092 Error_Msg_N ("object was observed #", Expr);
5093 end if;
5094
5095 Key := Get_Next_Key (Current_Observers);
5096 end loop;
5097 end;
5098 end Check_Not_Observed;
5099
5100 -- Local variables
5101
5102 Expr_Type : constant Entity_Id := Etype (Expr);
5103 Root : Entity_Id := Get_Root_Object (Expr);
5104 Perm : Perm_Kind_Option;
5105
5106 -- Start of processing for Process_Path
5107
5108 begin
5109 -- Nothing to do if the root type is not deep, or the path is not rooted
5110 -- in an object.
5111
5112 if not Present (Root)
5113 or else not Is_Deep (Etype (Root))
5114 then
5115 return;
5116 end if;
5117
5118 -- Identify the root type for the path
5119
5120 Root := Unique_Entity (Root);
5121
5122 -- Except during elaboration, the root object should have been declared
5123 -- and entered into the current permission environment.
5124
5125 if not Inside_Elaboration
5126 and then Get (Current_Perm_Env, Root) = null
5127 then
5128 Illegal_Global_Usage (Expr, Root);
5129 end if;
5130
5131 -- During elaboration, only the validity of operations is checked, no
5132 -- need to compute the permission of Expr.
5133
5134 if Inside_Elaboration then
5135 Perm := None;
5136 else
5137 Perm := Get_Perm (Expr);
5138 end if;
5139
5140 -- Check permissions
5141
5142 case Mode is
5143
5144 when Read =>
5145
5146 -- No checking needed during elaboration
5147
5148 if Inside_Elaboration then
5149 return;
5150 end if;
5151
5152 -- Check path is readable
5153
5154 if Perm not in Read_Perm then
5155 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5156 return;
5157 end if;
5158
5159 when Move =>
5160
5161 -- Forbidden on deep path during elaboration, otherwise no
5162 -- checking needed.
5163
5164 if Inside_Elaboration then
5165 if Is_Deep (Expr_Type)
5166 and then not Inside_Procedure_Call
5167 and then Present (Get_Root_Object (Expr))
5168 and then Emit_Messages
5169 then
5170 Error_Msg_N ("illegal move during elaboration", Expr);
5171 end if;
5172
5173 return;
5174 end if;
5175
5176 -- For deep path, check RW permission, otherwise R permission
5177
5178 if not Is_Deep (Expr_Type) then
5179 if Perm not in Read_Perm then
5180 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5181 end if;
5182 return;
5183 end if;
5184
5185 -- SPARK RM 3.10(1): At the point of a move operation the state of
5186 -- the source object (if any) shall be Unrestricted.
5187
5188 if Perm /= Read_Write then
5189 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
5190 return;
5191 end if;
5192
5193 when Assign =>
5194
5195 -- No checking needed during elaboration
5196
5197 if Inside_Elaboration then
5198 return;
5199 end if;
5200
5201 -- For assignment, check W permission
5202
5203 if Perm not in Write_Perm then
5204 Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr));
5205 return;
5206 end if;
5207
5208 when Borrow =>
5209
5210 -- Forbidden during elaboration, an error is already issued in
5211 -- Check_Declaration, just return.
5212
5213 if Inside_Elaboration then
5214 return;
5215 end if;
5216
5217 -- For borrowing, check RW permission
5218
5219 if Perm /= Read_Write then
5220 Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr));
5221 return;
5222 end if;
5223
5224 when Observe =>
5225
5226 -- Forbidden during elaboration, an error is already issued in
5227 -- Check_Declaration, just return.
5228
5229 if Inside_Elaboration then
5230 return;
5231 end if;
5232
5233 -- For borrowing, check R permission
5234
5235 if Perm not in Read_Perm then
5236 Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr));
5237 return;
5238 end if;
5239 end case;
5240
5241 -- Check path was not borrowed
5242
5243 Check_Not_Borrowed (Expr, Root);
5244
5245 -- For modes that require W permission, check path was not observed
5246
5247 case Mode is
5248 when Read | Observe =>
5249 null;
5250 when Assign | Move | Borrow =>
5251 Check_Not_Observed (Expr, Root);
5252 end case;
5253
5254 -- Do not update permission environment when handling calls
5255
5256 if Inside_Procedure_Call then
5257 return;
5258 end if;
5259
5260 -- Update the permissions
5261
5262 case Mode is
5263
5264 when Read =>
5265 null;
5266
5267 when Move =>
5268
5269 -- SPARK RM 3.10(1): After a move operation, the state of the
5270 -- source object (if any) becomes Moved.
5271
5272 if Present (Get_Root_Object (Expr)) then
5273 declare
5274 Tree : constant Perm_Tree_Access :=
5275 Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr);
5276 begin
5277 pragma Assert (Tree /= null);
5278 Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr);
5279 end;
5280 end if;
5281
5282 when Assign =>
5283
5284 -- If there is no root object, or the tree has an array component,
5285 -- then the permissions do not get modified by the assignment.
5286
5287 if No (Get_Root_Object (Expr))
5288 or else Has_Array_Component (Expr)
5289 then
5290 return;
5291 end if;
5292
5293 -- Set permission RW for the path and its extensions
5294
5295 declare
5296 Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr);
5297 begin
5298 Tree.all.Tree.Permission := Read_Write;
5299 Set_Perm_Extensions (Tree, Read_Write, Expl => Expr);
5300
5301 -- Normalize the permission tree
5302
5303 Set_Perm_Prefixes_Assign (Expr);
5304 end;
5305
5306 -- Borrowing and observing of paths is handled by the variables
5307 -- Current_Borrowers and Current_Observers.
5308
5309 when Borrow | Observe =>
5310 null;
5311 end case;
5312 end Process_Path;
5313
5314 --------------------
5315 -- Return_Globals --
5316 --------------------
5317
5318 procedure Return_Globals (Subp : Entity_Id) is
5319
5320 procedure Return_Global
5321 (Expr : Node_Id;
5322 Typ : Entity_Id;
5323 Kind : Formal_Kind;
5324 Subp : Entity_Id;
5325 Global_Var : Boolean);
5326 -- Proxy procedure to return globals, to adjust for the type of first
5327 -- parameter expected by Return_Parameter_Or_Global.
5328
5329 -------------------
5330 -- Return_Global --
5331 -------------------
5332
5333 procedure Return_Global
5334 (Expr : Node_Id;
5335 Typ : Entity_Id;
5336 Kind : Formal_Kind;
5337 Subp : Entity_Id;
5338 Global_Var : Boolean)
5339 is
5340 begin
5341 Return_Parameter_Or_Global
5342 (Id => Entity (Expr),
5343 Typ => Typ,
5344 Kind => Kind,
5345 Subp => Subp,
5346 Global_Var => Global_Var);
5347 end Return_Global;
5348
5349 procedure Return_Globals_Inst is new Handle_Globals (Return_Global);
5350
5351 -- Start of processing for Return_Globals
5352
5353 begin
5354 Return_Globals_Inst (Subp);
5355 end Return_Globals;
5356
5357 --------------------------------
5358 -- Return_Parameter_Or_Global --
5359 --------------------------------
5360
5361 procedure Return_Parameter_Or_Global
5362 (Id : Entity_Id;
5363 Typ : Entity_Id;
5364 Kind : Formal_Kind;
5365 Subp : Entity_Id;
5366 Global_Var : Boolean)
5367 is
5368 begin
5369 -- Shallow parameters and globals need not be considered
5370
5371 if not Is_Deep (Typ) then
5372 return;
5373
5374 elsif Kind = E_In_Parameter then
5375
5376 -- Input global variables are observed only
5377
5378 if Global_Var then
5379 return;
5380
5381 -- Anonymous access to constant is an observe
5382
5383 elsif Is_Anonymous_Access_Type (Typ)
5384 and then Is_Access_Constant (Typ)
5385 then
5386 return;
5387
5388 -- Deep types other than access types define an observe
5389
5390 elsif not Is_Access_Type (Typ) then
5391 return;
5392 end if;
5393 end if;
5394
5395 -- All other parameters and globals should return with mode RW to the
5396 -- caller.
5397
5398 declare
5399 Tree : constant Perm_Tree_Access := Get (Current_Perm_Env, Id);
5400 begin
5401 if Permission (Tree) /= Read_Write then
5402 Perm_Error_Subprogram_End
5403 (E => Id,
5404 Subp => Subp,
5405 Perm => Read_Write,
5406 Found_Perm => Permission (Tree),
5407 Expl => Explanation (Tree));
5408 end if;
5409 end;
5410 end Return_Parameter_Or_Global;
5411
5412 -----------------------
5413 -- Return_Parameters --
5414 -----------------------
5415
5416 procedure Return_Parameters (Subp : Entity_Id) is
5417 Formal : Entity_Id;
5418 begin
5419 Formal := First_Formal (Subp);
5420 while Present (Formal) loop
5421 Return_Parameter_Or_Global
5422 (Id => Formal,
5423 Typ => Retysp (Etype (Formal)),
5424 Kind => Ekind (Formal),
5425 Subp => Subp,
5426 Global_Var => False);
5427 Next_Formal (Formal);
5428 end loop;
5429 end Return_Parameters;
5430
5431 -------------------------
5432 -- Set_Perm_Extensions --
5433 -------------------------
5434
5435 procedure Set_Perm_Extensions
5436 (T : Perm_Tree_Access;
5437 P : Perm_Kind;
5438 Expl : Node_Id) is
5439
5440 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access);
5441 -- Free the permission tree of children if any, prio to replacing T
5442
5443 -----------------------------
5444 -- Free_Perm_Tree_Children --
5445 -----------------------------
5446
5447 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is
5448 begin
5449 case Kind (T) is
5450 when Entire_Object =>
5451 null;
5452
5453 when Reference =>
5454 Free_Tree (T.all.Tree.Get_All);
5455
5456 when Array_Component =>
5457 Free_Tree (T.all.Tree.Get_Elem);
5458
5459 when Record_Component =>
5460 declare
5461 Hashtbl : Perm_Tree_Maps.Instance := Component (T);
5462 Comp : Perm_Tree_Access;
5463
5464 begin
5465 Comp := Perm_Tree_Maps.Get_First (Hashtbl);
5466 while Comp /= null loop
5467 Free_Tree (Comp);
5468 Comp := Perm_Tree_Maps.Get_Next (Hashtbl);
5469 end loop;
5470
5471 Perm_Tree_Maps.Reset (Hashtbl);
5472 end;
5473 end case;
5474 end Free_Perm_Tree_Children;
5475
5476 -- Start of processing for Set_Perm_Extensions
5477
5478 begin
5479 Free_Perm_Tree_Children (T);
5480 T.all.Tree := Perm_Tree'(Kind => Entire_Object,
5481 Is_Node_Deep => Is_Node_Deep (T),
5482 Explanation => Expl,
5483 Permission => Permission (T),
5484 Children_Permission => P);
5485 end Set_Perm_Extensions;
5486
5487 ------------------------------
5488 -- Set_Perm_Extensions_Move --
5489 ------------------------------
5490
5491 procedure Set_Perm_Extensions_Move
5492 (T : Perm_Tree_Access;
5493 E : Entity_Id;
5494 Expl : Node_Id)
5495 is
5496 Check_Ty : constant Entity_Id := Retysp (E);
5497 begin
5498 -- Shallow extensions are set to RW
5499
5500 if not Is_Node_Deep (T) then
5501 Set_Perm_Extensions (T, Read_Write, Expl => Expl);
5502 return;
5503 end if;
5504
5505 -- Deep extensions are set to W before .all and NO afterwards
5506
5507 T.all.Tree.Permission := Write_Only;
5508
5509 case T.all.Tree.Kind is
5510
5511 -- For a folded tree of composite type, unfold the tree for better
5512 -- precision.
5513
5514 when Entire_Object =>
5515 case Ekind (Check_Ty) is
5516 when E_Array_Type
5517 | E_Array_Subtype
5518 =>
5519 declare
5520 C : constant Perm_Tree_Access :=
5521 new Perm_Tree_Wrapper'
5522 (Tree =>
5523 (Kind => Entire_Object,
5524 Is_Node_Deep => Is_Node_Deep (T),
5525 Explanation => Expl,
5526 Permission => Read_Write,
5527 Children_Permission => Read_Write));
5528 begin
5529 Set_Perm_Extensions_Move
5530 (C, Component_Type (Check_Ty), Expl);
5531 T.all.Tree := (Kind => Array_Component,
5532 Is_Node_Deep => Is_Node_Deep (T),
5533 Explanation => Expl,
5534 Permission => Write_Only,
5535 Get_Elem => C);
5536 end;
5537
5538 when Record_Kind =>
5539 declare
5540 C : Perm_Tree_Access;
5541 Comp : Entity_Id;
5542 Hashtbl : Perm_Tree_Maps.Instance;
5543
5544 begin
5545 Comp := First_Component_Or_Discriminant (Check_Ty);
5546 while Present (Comp) loop
5547
5548 -- Unfold components which are visible in SPARK
5549
5550 if Component_Is_Visible_In_SPARK (Comp) then
5551 C := new Perm_Tree_Wrapper'
5552 (Tree =>
5553 (Kind => Entire_Object,
5554 Is_Node_Deep => Is_Deep (Etype (Comp)),
5555 Explanation => Expl,
5556 Permission => Read_Write,
5557 Children_Permission => Read_Write));
5558 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5559
5560 -- Hidden components are never deep
5561
5562 else
5563 C := new Perm_Tree_Wrapper'
5564 (Tree =>
5565 (Kind => Entire_Object,
5566 Is_Node_Deep => False,
5567 Explanation => Expl,
5568 Permission => Read_Write,
5569 Children_Permission => Read_Write));
5570 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5571 end if;
5572
5573 Perm_Tree_Maps.Set
5574 (Hashtbl, Original_Record_Component (Comp), C);
5575 Next_Component_Or_Discriminant (Comp);
5576 end loop;
5577
5578 T.all.Tree :=
5579 (Kind => Record_Component,
5580 Is_Node_Deep => Is_Node_Deep (T),
5581 Explanation => Expl,
5582 Permission => Write_Only,
5583 Component => Hashtbl);
5584 end;
5585
5586 -- Otherwise, extensions are set to NO
5587
5588 when others =>
5589 Set_Perm_Extensions (T, No_Access, Expl);
5590 end case;
5591
5592 when Reference =>
5593 Set_Perm_Extensions (T, No_Access, Expl);
5594
5595 when Array_Component =>
5596 Set_Perm_Extensions_Move
5597 (Get_Elem (T), Component_Type (Check_Ty), Expl);
5598
5599 when Record_Component =>
5600 declare
5601 C : Perm_Tree_Access;
5602 Comp : Entity_Id;
5603
5604 begin
5605 Comp := First_Component_Or_Discriminant (Check_Ty);
5606 while Present (Comp) loop
5607 C := Perm_Tree_Maps.Get
5608 (Component (T), Original_Record_Component (Comp));
5609 pragma Assert (C /= null);
5610
5611 -- Move visible components
5612
5613 if Component_Is_Visible_In_SPARK (Comp) then
5614 Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
5615
5616 -- Hidden components are never deep
5617
5618 else
5619 Set_Perm_Extensions (C, Read_Write, Expl => Expl);
5620 end if;
5621
5622 Next_Component_Or_Discriminant (Comp);
5623 end loop;
5624 end;
5625 end case;
5626 end Set_Perm_Extensions_Move;
5627
5628 -----------------------
5629 -- Set_Perm_Prefixes --
5630 -----------------------
5631
5632 function Set_Perm_Prefixes
5633 (N : Node_Id;
5634 Perm : Perm_Kind_Option;
5635 Expl : Node_Id) return Perm_Tree_Access
5636 is
5637 begin
5638 case Nkind (N) is
5639 when N_Expanded_Name
5640 | N_Identifier
5641 =>
5642 declare
5643 E : constant Entity_Id := Unique_Entity (Entity (N));
5644 C : constant Perm_Tree_Access := Get (Current_Perm_Env, E);
5645 pragma Assert (C /= null);
5646
5647 begin
5648 if Perm /= None then
5649 C.all.Tree.Permission := Glb (Perm, Permission (C));
5650 end if;
5651
5652 return C;
5653 end;
5654
5655 -- For a nonterminal path, we set the permission tree of its prefix,
5656 -- and then we extract from the returned pointer the subtree and
5657 -- assign an adequate permission to it, if unfolded. If folded,
5658 -- we unroll the tree one level.
5659
5660 when N_Explicit_Dereference =>
5661 declare
5662 C : constant Perm_Tree_Access :=
5663 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5664 pragma Assert (C /= null);
5665 pragma Assert (Kind (C) = Entire_Object
5666 or else Kind (C) = Reference);
5667 begin
5668 -- The tree is already unfolded. Replace the permission of the
5669 -- dereference.
5670
5671 if Kind (C) = Reference then
5672 declare
5673 D : constant Perm_Tree_Access := Get_All (C);
5674 pragma Assert (D /= null);
5675
5676 begin
5677 if Perm /= None then
5678 D.all.Tree.Permission := Glb (Perm, Permission (D));
5679 end if;
5680
5681 return D;
5682 end;
5683
5684 -- The tree is folded. Expand it.
5685
5686 else
5687 declare
5688 pragma Assert (Kind (C) = Entire_Object);
5689
5690 Child_P : constant Perm_Kind := Children_Permission (C);
5691 D : constant Perm_Tree_Access :=
5692 new Perm_Tree_Wrapper'
5693 (Tree =>
5694 (Kind => Entire_Object,
5695 Is_Node_Deep => Is_Deep (Etype (N)),
5696 Explanation => Expl,
5697 Permission => Child_P,
5698 Children_Permission => Child_P));
5699 begin
5700 if Perm /= None then
5701 D.all.Tree.Permission := Perm;
5702 end if;
5703
5704 C.all.Tree := (Kind => Reference,
5705 Is_Node_Deep => Is_Node_Deep (C),
5706 Explanation => Expl,
5707 Permission => Permission (C),
5708 Get_All => D);
5709 return D;
5710 end;
5711 end if;
5712 end;
5713
5714 when N_Selected_Component =>
5715 declare
5716 C : constant Perm_Tree_Access :=
5717 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5718 pragma Assert (C /= null);
5719 pragma Assert (Kind (C) = Entire_Object
5720 or else Kind (C) = Record_Component);
5721 begin
5722 -- The tree is already unfolded. Replace the permission of the
5723 -- component.
5724
5725 if Kind (C) = Record_Component then
5726 declare
5727 Comp : constant Entity_Id :=
5728 Original_Record_Component
5729 (Entity (Selector_Name (N)));
5730 D : constant Perm_Tree_Access :=
5731 Perm_Tree_Maps.Get (Component (C), Comp);
5732 pragma Assert (D /= null);
5733
5734 begin
5735 if Perm /= None then
5736 D.all.Tree.Permission := Glb (Perm, Permission (D));
5737 end if;
5738
5739 return D;
5740 end;
5741
5742 -- The tree is folded. Expand it.
5743
5744 else
5745 declare
5746 pragma Assert (Kind (C) = Entire_Object);
5747
5748 D : Perm_Tree_Access;
5749 D_This : Perm_Tree_Access;
5750 Comp : Node_Id;
5751 P : Perm_Kind;
5752 Child_P : constant Perm_Kind := Children_Permission (C);
5753 Hashtbl : Perm_Tree_Maps.Instance;
5754 -- Create an empty hash table
5755
5756 begin
5757 Comp :=
5758 First_Component_Or_Discriminant
5759 (Retysp (Etype (Prefix (N))));
5760
5761 while Present (Comp) loop
5762 if Perm /= None
5763 and then Original_Record_Component (Comp) =
5764 Original_Record_Component
5765 (Entity (Selector_Name (N)))
5766 then
5767 P := Perm;
5768 else
5769 P := Child_P;
5770 end if;
5771
5772 D := new Perm_Tree_Wrapper'
5773 (Tree =>
5774 (Kind => Entire_Object,
5775 Is_Node_Deep =>
5776 -- Hidden components are never deep
5777 Component_Is_Visible_In_SPARK (Comp)
5778 and then Is_Deep (Etype (Comp)),
5779 Explanation => Expl,
5780 Permission => P,
5781 Children_Permission => Child_P));
5782 Perm_Tree_Maps.Set
5783 (Hashtbl, Original_Record_Component (Comp), D);
5784
5785 -- Store the tree to return for this component
5786
5787 if Original_Record_Component (Comp) =
5788 Original_Record_Component
5789 (Entity (Selector_Name (N)))
5790 then
5791 D_This := D;
5792 end if;
5793
5794 Next_Component_Or_Discriminant (Comp);
5795 end loop;
5796
5797 C.all.Tree := (Kind => Record_Component,
5798 Is_Node_Deep => Is_Node_Deep (C),
5799 Explanation => Expl,
5800 Permission => Permission (C),
5801 Component => Hashtbl);
5802 return D_This;
5803 end;
5804 end if;
5805 end;
5806
5807 when N_Indexed_Component
5808 | N_Slice
5809 =>
5810 declare
5811 C : constant Perm_Tree_Access :=
5812 Set_Perm_Prefixes (Prefix (N), Perm, Expl);
5813 pragma Assert (C /= null);
5814 pragma Assert (Kind (C) = Entire_Object
5815 or else Kind (C) = Array_Component);
5816 begin
5817 -- The tree is already unfolded. Replace the permission of the
5818 -- component.
5819
5820 if Kind (C) = Array_Component then
5821 declare
5822 D : constant Perm_Tree_Access := Get_Elem (C);
5823 pragma Assert (D /= null);
5824
5825 begin
5826 if Perm /= None then
5827 D.all.Tree.Permission := Glb (Perm, Permission (D));
5828 end if;
5829
5830 return D;
5831 end;
5832
5833 -- The tree is folded. Expand it.
5834
5835 else
5836 declare
5837 pragma Assert (Kind (C) = Entire_Object);
5838
5839 Child_P : constant Perm_Kind := Children_Permission (C);
5840 D : constant Perm_Tree_Access :=
5841 new Perm_Tree_Wrapper'
5842 (Tree =>
5843 (Kind => Entire_Object,
5844 Is_Node_Deep => Is_Node_Deep (C),
5845 Explanation => Expl,
5846 Permission => Child_P,
5847 Children_Permission => Child_P));
5848 begin
5849 if Perm /= None then
5850 D.all.Tree.Permission := Perm;
5851 end if;
5852
5853 C.all.Tree := (Kind => Array_Component,
5854 Is_Node_Deep => Is_Node_Deep (C),
5855 Explanation => Expl,
5856 Permission => Permission (C),
5857 Get_Elem => D);
5858 return D;
5859 end;
5860 end if;
5861 end;
5862
5863 when N_Qualified_Expression
5864 | N_Type_Conversion
5865 | N_Unchecked_Type_Conversion
5866 =>
5867 return Set_Perm_Prefixes (Expression (N), Perm, Expl);
5868
5869 when others =>
5870 raise Program_Error;
5871 end case;
5872 end Set_Perm_Prefixes;
5873
5874 ------------------------------
5875 -- Set_Perm_Prefixes_Assign --
5876 ------------------------------
5877
5878 procedure Set_Perm_Prefixes_Assign (N : Node_Id) is
5879 C : constant Perm_Tree_Access := Get_Perm_Tree (N);
5880
5881 begin
5882 case Kind (C) is
5883 when Entire_Object =>
5884 pragma Assert (Children_Permission (C) = Read_Write);
5885 C.all.Tree.Permission := Read_Write;
5886
5887 when Reference =>
5888 C.all.Tree.Permission :=
5889 Lub (Permission (C), Permission (Get_All (C)));
5890
5891 when Array_Component =>
5892 null;
5893
5894 when Record_Component =>
5895 declare
5896 Comp : Perm_Tree_Access;
5897 Perm : Perm_Kind := Read_Write;
5898
5899 begin
5900 -- We take the Glb of all the descendants, and then update the
5901 -- permission of the node with it.
5902
5903 Comp := Perm_Tree_Maps.Get_First (Component (C));
5904 while Comp /= null loop
5905 Perm := Glb (Perm, Permission (Comp));
5906 Comp := Perm_Tree_Maps.Get_Next (Component (C));
5907 end loop;
5908
5909 C.all.Tree.Permission := Lub (Permission (C), Perm);
5910 end;
5911 end case;
5912
5913 case Nkind (N) is
5914
5915 -- Base identifier end recursion
5916
5917 when N_Expanded_Name
5918 | N_Identifier
5919 =>
5920 null;
5921
5922 when N_Explicit_Dereference
5923 | N_Indexed_Component
5924 | N_Selected_Component
5925 | N_Slice
5926 =>
5927 Set_Perm_Prefixes_Assign (Prefix (N));
5928
5929 when N_Qualified_Expression
5930 | N_Type_Conversion
5931 | N_Unchecked_Type_Conversion
5932 =>
5933 Set_Perm_Prefixes_Assign (Expression (N));
5934
5935 when others =>
5936 raise Program_Error;
5937 end case;
5938 end Set_Perm_Prefixes_Assign;
5939
5940 -------------------
5941 -- Setup_Globals --
5942 -------------------
5943
5944 procedure Setup_Globals (Subp : Entity_Id) is
5945
5946 procedure Setup_Global
5947 (Expr : Node_Id;
5948 Typ : Entity_Id;
5949 Kind : Formal_Kind;
5950 Subp : Entity_Id;
5951 Global_Var : Boolean);
5952 -- Proxy procedure to set up globals, to adjust for the type of first
5953 -- parameter expected by Setup_Parameter_Or_Global.
5954
5955 ------------------
5956 -- Setup_Global --
5957 ------------------
5958
5959 procedure Setup_Global
5960 (Expr : Node_Id;
5961 Typ : Entity_Id;
5962 Kind : Formal_Kind;
5963 Subp : Entity_Id;
5964 Global_Var : Boolean)
5965 is
5966 begin
5967 Setup_Parameter_Or_Global
5968 (Id => Entity (Expr),
5969 Typ => Typ,
5970 Kind => Kind,
5971 Subp => Subp,
5972 Global_Var => Global_Var,
5973 Expl => Expr);
5974 end Setup_Global;
5975
5976 procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global);
5977
5978 -- Start of processing for Setup_Globals
5979
5980 begin
5981 Setup_Globals_Inst (Subp);
5982 end Setup_Globals;
5983
5984 -------------------------------
5985 -- Setup_Parameter_Or_Global --
5986 -------------------------------
5987
5988 procedure Setup_Parameter_Or_Global
5989 (Id : Entity_Id;
5990 Typ : Entity_Id;
5991 Kind : Formal_Kind;
5992 Subp : Entity_Id;
5993 Global_Var : Boolean;
5994 Expl : Node_Id)
5995 is
5996 Perm : Perm_Kind_Option;
5997
5998 begin
5999 case Kind is
6000 when E_In_Parameter =>
6001
6002 -- Shallow parameters and globals need not be considered
6003
6004 if not Is_Deep (Typ) then
6005 Perm := None;
6006
6007 -- Inputs of functions have R permission only
6008
6009 elsif Ekind (Subp) = E_Function then
6010 Perm := Read_Only;
6011
6012 -- Input global variables have R permission only
6013
6014 elsif Global_Var then
6015 Perm := Read_Only;
6016
6017 -- Anonymous access to constant is an observe
6018
6019 elsif Is_Anonymous_Access_Type (Typ)
6020 and then Is_Access_Constant (Typ)
6021 then
6022 Perm := Read_Only;
6023
6024 -- Other access types are a borrow
6025
6026 elsif Is_Access_Type (Typ) then
6027 Perm := Read_Write;
6028
6029 -- Deep types other than access types define an observe
6030
6031 else
6032 Perm := Read_Only;
6033 end if;
6034
6035 when E_Out_Parameter
6036 | E_In_Out_Parameter
6037 =>
6038 -- Shallow parameters and globals need not be considered
6039
6040 if not Is_Deep (Typ) then
6041 Perm := None;
6042
6043 -- Functions cannot have outputs in SPARK
6044
6045 elsif Ekind (Subp) = E_Function then
6046 return;
6047
6048 -- Deep types define a borrow or a move
6049
6050 else
6051 Perm := Read_Write;
6052 end if;
6053 end case;
6054
6055 if Perm /= None then
6056 declare
6057 Tree : constant Perm_Tree_Access :=
6058 new Perm_Tree_Wrapper'
6059 (Tree =>
6060 (Kind => Entire_Object,
6061 Is_Node_Deep => Is_Deep (Etype (Id)),
6062 Explanation => Expl,
6063 Permission => Perm,
6064 Children_Permission => Perm));
6065 begin
6066 Set (Current_Perm_Env, Id, Tree);
6067 end;
6068 end if;
6069 end Setup_Parameter_Or_Global;
6070
6071 ----------------------
6072 -- Setup_Parameters --
6073 ----------------------
6074
6075 procedure Setup_Parameters (Subp : Entity_Id) is
6076 Formal : Entity_Id;
6077 begin
6078 Formal := First_Formal (Subp);
6079 while Present (Formal) loop
6080 Setup_Parameter_Or_Global
6081 (Id => Formal,
6082 Typ => Retysp (Etype (Formal)),
6083 Kind => Ekind (Formal),
6084 Subp => Subp,
6085 Global_Var => False,
6086 Expl => Formal);
6087 Next_Formal (Formal);
6088 end loop;
6089 end Setup_Parameters;
6090
6091 --------------------------------
6092 -- Setup_Protected_Components --
6093 --------------------------------
6094
6095 procedure Setup_Protected_Components (Subp : Entity_Id) is
6096 Typ : constant Entity_Id := Scope (Subp);
6097 Comp : Entity_Id;
6098 Kind : Formal_Kind;
6099
6100 begin
6101 Comp := First_Component_Or_Discriminant (Typ);
6102
6103 -- The protected object is an implicit input of protected functions, and
6104 -- an implicit input-output of protected procedures and entries.
6105
6106 if Ekind (Subp) = E_Function then
6107 Kind := E_In_Parameter;
6108 else
6109 Kind := E_In_Out_Parameter;
6110 end if;
6111
6112 while Present (Comp) loop
6113 Setup_Parameter_Or_Global
6114 (Id => Comp,
6115 Typ => Retysp (Etype (Comp)),
6116 Kind => Kind,
6117 Subp => Subp,
6118 Global_Var => False,
6119 Expl => Comp);
6120
6121 Next_Component_Or_Discriminant (Comp);
6122 end loop;
6123 end Setup_Protected_Components;
6124
6125 end Sem_SPARK;