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