1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- S E M _ S P A R K -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2017-2019, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- 17-- for more details. You should have received a copy of the GNU General -- 18-- Public License distributed with GNAT; see file COPYING3. If not, go to -- 19-- http://www.gnu.org/licenses for a complete copy of the license. -- 20-- -- 21-- GNAT was originally developed by the GNAT team at New York University. -- 22-- Extensive contributions were provided by Ada Core Technologies Inc. -- 23-- -- 24------------------------------------------------------------------------------ 25 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 (Key : Entity_Id) 56 return Elaboration_Context_Index; 57 -- Function to hash any node of the AST 58 59 type Perm_Kind is (Borrowed, Observed, Unrestricted, Moved); 60 -- Permission type associated with paths. The Moved permission is 61 -- equivalent to the Unrestricted one (same permissions). The Moved is 62 -- however used to mark the RHS after a move (which still unrestricted). 63 -- This way, we may generate warnings when manipulating the RHS 64 -- afterwads since it is set to Null after the assignment. 65 66 type Perm_Tree_Wrapper; 67 68 type Perm_Tree_Access is access Perm_Tree_Wrapper; 69 -- A tree of permissions is defined, where the root is a whole object 70 -- and tree branches follow access paths in memory. As Perm_Tree is a 71 -- discriminated record, a wrapper type is used for the access type 72 -- designating a subtree, to make it unconstrained so that it can be 73 -- updated. 74 75 -- Nodes in the permission tree are of different kinds 76 77 type Path_Kind is 78 (Entire_Object, -- Scalar object, or folded object of any type 79 Reference, -- Unfolded object of access type 80 Array_Component, -- Unfolded object of array type 81 Record_Component -- Unfolded object of record type 82 ); 83 84 package Perm_Tree_Maps is new Simple_HTable 85 (Header_Num => Elaboration_Context_Index, 86 Key => Node_Id, 87 Element => Perm_Tree_Access, 88 No_Element => null, 89 Hash => Elaboration_Context_Hash, 90 Equal => "="); 91 -- The instantation of a hash table, with keys being nodes and values 92 -- being pointers to trees. This is used to reference easily all 93 -- extensions of a Record_Component node (that can have name x, y, ...). 94 95 -- The definition of permission trees. This is a tree, which has a 96 -- permission at each node, and depending on the type of the node, 97 -- can have zero, one, or more children pointed to by an access to tree. 98 99 type Perm_Tree (Kind : Path_Kind := Entire_Object) is record 100 Permission : Perm_Kind; 101 -- Permission at this level in the path 102 103 Is_Node_Deep : Boolean; 104 -- Whether this node is of a deep type, to be used when moving the 105 -- path. 106 107 case Kind is 108 -- An entire object is either a leaf (an object which cannot be 109 -- extended further in a path) or a subtree in folded form (which 110 -- could later be unfolded further in another kind of node). The 111 -- field Children_Permission specifies a permission for every 112 -- extension of that node if that permission is different from 113 -- the node's permission. 114 115 when Entire_Object => 116 Children_Permission : Perm_Kind; 117 118 -- Unfolded path of access type. The permission of the object 119 -- pointed to is given in Get_All. 120 121 when Reference => 122 Get_All : Perm_Tree_Access; 123 124 -- Unfolded path of array type. The permission of the elements is 125 -- given in Get_Elem. 126 127 when Array_Component => 128 Get_Elem : Perm_Tree_Access; 129 130 -- Unfolded path of record type. The permission of the regular 131 -- components is given in Component. The permission of unknown 132 -- components (for objects of tagged type) is given in 133 -- Other_Components. 134 135 when Record_Component => 136 Component : Perm_Tree_Maps.Instance; 137 Other_Components : Perm_Tree_Access; 138 end case; 139 end record; 140 141 type Perm_Tree_Wrapper is record 142 Tree : Perm_Tree; 143 end record; 144 -- We use this wrapper in order to have unconstrained discriminants 145 146 type Perm_Env is new Perm_Tree_Maps.Instance; 147 -- The definition of a permission environment for the analysis. This 148 -- is just a hash table of permission trees, each of them rooted with 149 -- an Identifier/Expanded_Name. 150 151 type Perm_Env_Access is access Perm_Env; 152 -- Access to permission environments 153 154 package Env_Maps is new Simple_HTable 155 (Header_Num => Elaboration_Context_Index, 156 Key => Entity_Id, 157 Element => Perm_Env_Access, 158 No_Element => null, 159 Hash => Elaboration_Context_Hash, 160 Equal => "="); 161 -- The instantiation of a hash table whose elements are permission 162 -- environments. This hash table is used to save the environments at 163 -- the entry of each loop, with the key being the loop label. 164 165 type Env_Backups is new Env_Maps.Instance; 166 -- The type defining the hash table saving the environments at the entry 167 -- of each loop. 168 169 package Boolean_Variables_Maps is new Simple_HTable 170 (Header_Num => Elaboration_Context_Index, 171 Key => Entity_Id, 172 Element => Boolean, 173 No_Element => False, 174 Hash => Elaboration_Context_Hash, 175 Equal => "="); 176 -- These maps allow tracking the variables that have been declared but 177 -- never used anywhere in the source code. Especially, we do not raise 178 -- an error if the variable stays write-only and is declared at package 179 -- level, because there is no risk that the variable has been moved, 180 -- because it has never been used. 181 182 type Initialization_Map is new Boolean_Variables_Maps.Instance; 183 184 -------------------- 185 -- Simple Getters -- 186 -------------------- 187 188 -- Simple getters to avoid having .all.Tree.Field everywhere. Of course, 189 -- that's only for the top access, as otherwise this reverses the order 190 -- in accesses visually. 191 192 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind; 193 function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance; 194 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access; 195 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access; 196 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean; 197 function Kind (T : Perm_Tree_Access) return Path_Kind; 198 function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access; 199 function Permission (T : Perm_Tree_Access) return Perm_Kind; 200 201 ----------------------- 202 -- Memory Management -- 203 ----------------------- 204 205 procedure Copy_Env 206 (From : Perm_Env; 207 To : in out Perm_Env); 208 -- Procedure to copy a permission environment 209 210 procedure Copy_Init_Map 211 (From : Initialization_Map; 212 To : in out Initialization_Map); 213 -- Procedure to copy an initialization map 214 215 procedure Copy_Tree 216 (From : Perm_Tree_Access; 217 To : Perm_Tree_Access); 218 -- Procedure to copy a permission tree 219 220 procedure Free_Env 221 (PE : in out Perm_Env); 222 -- Procedure to free a permission environment 223 224 procedure Free_Perm_Tree 225 (PT : in out Perm_Tree_Access); 226 -- Procedure to free a permission tree 227 228 -------------------- 229 -- Error Messages -- 230 -------------------- 231 232 procedure Perm_Mismatch 233 (Exp_Perm, Act_Perm : Perm_Kind; 234 N : Node_Id); 235 -- Issues a continuation error message about a mismatch between a 236 -- desired permission Exp_Perm and a permission obtained Act_Perm. N 237 -- is the node on which the error is reported. 238 239 end Permissions; 240 241 package body Permissions is 242 243 ------------------------- 244 -- Children_Permission -- 245 ------------------------- 246 247 function Children_Permission (T : Perm_Tree_Access) return Perm_Kind is 248 begin 249 return T.all.Tree.Children_Permission; 250 end Children_Permission; 251 252 --------------- 253 -- Component -- 254 --------------- 255 256 function Component 257 (T : Perm_Tree_Access) 258 return Perm_Tree_Maps.Instance 259 is 260 begin 261 return T.all.Tree.Component; 262 end Component; 263 264 -------------- 265 -- Copy_Env -- 266 -------------- 267 268 procedure Copy_Env (From : Perm_Env; To : in out Perm_Env) is 269 Comp_From : Perm_Tree_Access; 270 Key_From : Perm_Tree_Maps.Key_Option; 271 Son : Perm_Tree_Access; 272 273 begin 274 Reset (To); 275 Key_From := Get_First_Key (From); 276 while Key_From.Present loop 277 Comp_From := Get (From, Key_From.K); 278 pragma Assert (Comp_From /= null); 279 280 Son := new Perm_Tree_Wrapper; 281 Copy_Tree (Comp_From, Son); 282 283 Set (To, Key_From.K, Son); 284 Key_From := Get_Next_Key (From); 285 end loop; 286 end Copy_Env; 287 288 ------------------- 289 -- Copy_Init_Map -- 290 ------------------- 291 292 procedure Copy_Init_Map 293 (From : Initialization_Map; 294 To : in out Initialization_Map) 295 is 296 Comp_From : Boolean; 297 Key_From : Boolean_Variables_Maps.Key_Option; 298 299 begin 300 Reset (To); 301 Key_From := Get_First_Key (From); 302 while Key_From.Present loop 303 Comp_From := Get (From, Key_From.K); 304 Set (To, Key_From.K, Comp_From); 305 Key_From := Get_Next_Key (From); 306 end loop; 307 end Copy_Init_Map; 308 309 --------------- 310 -- Copy_Tree -- 311 --------------- 312 313 procedure Copy_Tree (From : Perm_Tree_Access; To : Perm_Tree_Access) is 314 begin 315 To.all := From.all; 316 case Kind (From) is 317 when Entire_Object => 318 null; 319 320 when Reference => 321 To.all.Tree.Get_All := new Perm_Tree_Wrapper; 322 Copy_Tree (Get_All (From), Get_All (To)); 323 324 when Array_Component => 325 To.all.Tree.Get_Elem := new Perm_Tree_Wrapper; 326 Copy_Tree (Get_Elem (From), Get_Elem (To)); 327 328 when Record_Component => 329 declare 330 Comp_From : Perm_Tree_Access; 331 Key_From : Perm_Tree_Maps.Key_Option; 332 Son : Perm_Tree_Access; 333 Hash_Table : Perm_Tree_Maps.Instance; 334 begin 335 -- We put a new hash table, so that it gets dealiased from the 336 -- Component (From) hash table. 337 To.all.Tree.Component := Hash_Table; 338 To.all.Tree.Other_Components := 339 new Perm_Tree_Wrapper'(Other_Components (From).all); 340 Copy_Tree (Other_Components (From), Other_Components (To)); 341 Key_From := Perm_Tree_Maps.Get_First_Key 342 (Component (From)); 343 344 while Key_From.Present loop 345 Comp_From := Perm_Tree_Maps.Get 346 (Component (From), Key_From.K); 347 pragma Assert (Comp_From /= null); 348 Son := new Perm_Tree_Wrapper; 349 Copy_Tree (Comp_From, Son); 350 Perm_Tree_Maps.Set 351 (To.all.Tree.Component, Key_From.K, Son); 352 Key_From := Perm_Tree_Maps.Get_Next_Key 353 (Component (From)); 354 end loop; 355 end; 356 end case; 357 358 end Copy_Tree; 359 360 ------------------------------ 361 -- Elaboration_Context_Hash -- 362 ------------------------------ 363 364 function Elaboration_Context_Hash 365 (Key : Entity_Id) return Elaboration_Context_Index 366 is 367 begin 368 return Elaboration_Context_Index (Key mod Elaboration_Context_Max); 369 end Elaboration_Context_Hash; 370 371 -------------- 372 -- Free_Env -- 373 -------------- 374 375 procedure Free_Env (PE : in out Perm_Env) is 376 CompO : Perm_Tree_Access; 377 begin 378 CompO := Get_First (PE); 379 while CompO /= null loop 380 Free_Perm_Tree (CompO); 381 CompO := Get_Next (PE); 382 end loop; 383 end Free_Env; 384 385 -------------------- 386 -- Free_Perm_Tree -- 387 -------------------- 388 389 procedure Free_Perm_Tree (PT : in out Perm_Tree_Access) is 390 procedure Free_Perm_Tree_Dealloc is 391 new Ada.Unchecked_Deallocation 392 (Perm_Tree_Wrapper, Perm_Tree_Access); 393 -- The deallocator for permission_trees 394 395 begin 396 case Kind (PT) is 397 when Entire_Object => 398 Free_Perm_Tree_Dealloc (PT); 399 400 when Reference => 401 Free_Perm_Tree (PT.all.Tree.Get_All); 402 Free_Perm_Tree_Dealloc (PT); 403 404 when Array_Component => 405 Free_Perm_Tree (PT.all.Tree.Get_Elem); 406 407 when Record_Component => 408 declare 409 Comp : Perm_Tree_Access; 410 411 begin 412 Free_Perm_Tree (PT.all.Tree.Other_Components); 413 Comp := Perm_Tree_Maps.Get_First (Component (PT)); 414 while Comp /= null loop 415 416 -- Free every Component subtree 417 418 Free_Perm_Tree (Comp); 419 Comp := Perm_Tree_Maps.Get_Next (Component (PT)); 420 end loop; 421 end; 422 Free_Perm_Tree_Dealloc (PT); 423 end case; 424 end Free_Perm_Tree; 425 426 ------------- 427 -- Get_All -- 428 ------------- 429 430 function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access is 431 begin 432 return T.all.Tree.Get_All; 433 end Get_All; 434 435 -------------- 436 -- Get_Elem -- 437 -------------- 438 439 function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access is 440 begin 441 return T.all.Tree.Get_Elem; 442 end Get_Elem; 443 444 ------------------ 445 -- Is_Node_Deep -- 446 ------------------ 447 448 function Is_Node_Deep (T : Perm_Tree_Access) return Boolean is 449 begin 450 return T.all.Tree.Is_Node_Deep; 451 end Is_Node_Deep; 452 453 ---------- 454 -- Kind -- 455 ---------- 456 457 function Kind (T : Perm_Tree_Access) return Path_Kind is 458 begin 459 return T.all.Tree.Kind; 460 end Kind; 461 462 ---------------------- 463 -- Other_Components -- 464 ---------------------- 465 466 function Other_Components 467 (T : Perm_Tree_Access) 468 return Perm_Tree_Access 469 is 470 begin 471 return T.all.Tree.Other_Components; 472 end Other_Components; 473 474 ---------------- 475 -- Permission -- 476 ---------------- 477 478 function Permission (T : Perm_Tree_Access) return Perm_Kind is 479 begin 480 return T.all.Tree.Permission; 481 end Permission; 482 483 ------------------- 484 -- Perm_Mismatch -- 485 ------------------- 486 487 procedure Perm_Mismatch (Exp_Perm, Act_Perm : Perm_Kind; N : Node_Id) is 488 begin 489 Error_Msg_N ("\expected state `" 490 & Perm_Kind'Image (Exp_Perm) & "` at least, got `" 491 & Perm_Kind'Image (Act_Perm) & "`", N); 492 end Perm_Mismatch; 493 494 end Permissions; 495 496 use Permissions; 497 498 -------------------------------------- 499 -- Analysis modes for AST traversal -- 500 -------------------------------------- 501 502 -- The different modes for analysis. This allows to checking whether a path 503 -- found in the code should be moved, borrowed, or observed. 504 505 type Checking_Mode is 506 507 (Read, 508 -- Default mode 509 510 Move, 511 -- Regular moving semantics. Checks that paths have Unrestricted 512 -- permission. After moving a path, the permission of both it and 513 -- its extensions are set to Unrestricted. 514 515 Assign, 516 -- Used for the target of an assignment, or an actual parameter with 517 -- mode OUT. Checks that paths have Unrestricted permission. After 518 -- assigning to a path, its permission is set to Unrestricted. 519 520 Borrow, 521 -- Used for the source of an assignement when initializes a stand alone 522 -- object of anonymous type, constant, or IN parameter and also OUT 523 -- or IN OUT composite object. 524 -- In the borrowed state, the access object is completely "dead". 525 526 Observe 527 -- Used for actual IN parameters of a scalar type. Checks that paths 528 -- have Read_Perm permission. After checking a path, its permission 529 -- is set to Observed. 530 -- 531 -- Also used for formal IN parameters 532 533 ); 534 535 type Result_Kind is (Folded, Unfolded, Function_Call); 536 -- The type declaration to discriminate in the Perm_Or_Tree type 537 538 -- The result type of the function Get_Perm_Or_Tree. This returns either a 539 -- tree when it found the appropriate tree, or a permission when the search 540 -- finds a leaf and the subtree we are looking for is folded. In the last 541 -- case, we return instead the Children_Permission field of the leaf. 542 543 type Perm_Or_Tree (R : Result_Kind) is record 544 case R is 545 when Folded => Found_Permission : Perm_Kind; 546 when Unfolded => Tree_Access : Perm_Tree_Access; 547 when Function_Call => null; 548 end case; 549 end record; 550 551 ----------------------- 552 -- Local subprograms -- 553 ----------------------- 554 555 -- Checking proceduress for safe pointer usage. These procedures traverse 556 -- the AST, check nodes for correct permissions according to SPARK RM 557 -- 6.4.2, and update permissions depending on the node kind. 558 559 procedure Check_Call_Statement (Call : Node_Id); 560 561 procedure Check_Callable_Body (Body_N : Node_Id); 562 -- We are not in End_Of_Callee mode, hence we will save the environment 563 -- and start from a new one. We will add in the environment all formal 564 -- parameters as well as global used during the subprogram, with the 565 -- appropriate permissions (unrestricted for borrowed and moved, observed 566 -- for observed names). 567 568 procedure Check_Declaration (Decl : Node_Id); 569 570 procedure Check_Expression (Expr : Node_Id); 571 572 procedure Check_Globals (N : Node_Id); 573 -- This procedure takes a global pragma and checks it 574 575 procedure Check_List (L : List_Id); 576 -- Calls Check_Node on each element of the list 577 578 procedure Check_Loop_Statement (Loop_N : Node_Id); 579 580 procedure Check_Node (N : Node_Id); 581 -- Main traversal procedure to check safe pointer usage. This procedure is 582 -- mutually recursive with the specialized procedures that follow. 583 584 procedure Check_Package_Body (Pack : Node_Id); 585 586 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id); 587 -- This procedure takes a formal and an actual parameter and checks the 588 -- permission of every in-mode parameter. This includes Observing and 589 -- Borrowing. 590 591 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id); 592 -- This procedure takes a formal and an actual parameter and checks the 593 -- state of every out-mode and in out-mode parameter. This includes 594 -- Moving and Borrowing. 595 596 procedure Check_Statement (Stmt : Node_Id); 597 598 function Get_Perm (N : Node_Id) return Perm_Kind; 599 -- The function that takes a name as input and returns a permission 600 -- associated to it. 601 602 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree; 603 -- This function gets a Node_Id and looks recursively to find the 604 -- appropriate subtree for that Node_Id. If the tree is folded on 605 -- that node, then it returns the permission given at the right level. 606 607 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access; 608 -- This function gets a Node_Id and looks recursively to find the 609 -- appropriate subtree for that Node_Id. If the tree is folded, then 610 -- it unrolls the tree up to the appropriate level. 611 612 procedure Hp (P : Perm_Env); 613 -- A procedure that outputs the hash table. This function is used only in 614 -- the debugger to look into a hash table. 615 pragma Unreferenced (Hp); 616 617 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id); 618 pragma No_Return (Illegal_Global_Usage); 619 -- A procedure that is called when deep globals or aliased globals are used 620 -- without any global aspect. 621 622 function Is_Deep (E : Entity_Id) return Boolean; 623 -- A function that can tell if a type is deep or not. Returns true if the 624 -- type passed as argument is deep. 625 626 procedure Perm_Error 627 (N : Node_Id; 628 Perm : Perm_Kind; 629 Found_Perm : Perm_Kind); 630 -- A procedure that is called when the permissions found contradict the 631 -- rules established by the RM. This function is called with the node, its 632 -- entity and the permission that was expected, and adds an error message 633 -- with the appropriate values. 634 635 procedure Perm_Error_Subprogram_End 636 (E : Entity_Id; 637 Subp : Entity_Id; 638 Perm : Perm_Kind; 639 Found_Perm : Perm_Kind); 640 -- A procedure that is called when the permissions found contradict the 641 -- rules established by the RM at the end of subprograms. This function 642 -- is called with the node, its entity, the node of the returning function 643 -- and the permission that was expected, and adds an error message with the 644 -- appropriate values. 645 646 procedure Process_Path (N : Node_Id); 647 648 procedure Return_Declarations (L : List_Id); 649 -- Check correct permissions on every declared object at the end of a 650 -- callee. Used at the end of the body of a callable entity. Checks that 651 -- paths of all borrowed formal parameters and global have Unrestricted 652 -- permission. 653 654 procedure Return_Globals (Subp : Entity_Id); 655 -- Takes a subprogram as input, and checks that all borrowed global items 656 -- of the subprogram indeed have RW permission at the end of the subprogram 657 -- execution. 658 659 procedure Return_The_Global 660 (Id : Entity_Id; 661 Mode : Formal_Kind; 662 Subp : Entity_Id); 663 -- Auxiliary procedure to Return_Globals 664 -- There is no need to return parameters because they will be reassigned 665 -- their state once the subprogram returns. Local variables that have 666 -- borrowed, observed, or moved an actual parameter go out of the scope. 667 668 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind); 669 -- This procedure takes an access to a permission tree and modifies the 670 -- tree so that any strict extensions of the given tree become of the 671 -- access specified by parameter P. 672 673 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access; 674 -- This function modifies the permissions of a given node_id in the 675 -- permission environment as well as in all the prefixes of the path, 676 -- given that the path is borrowed with mode out. 677 678 function Set_Perm_Prefixes 679 (N : Node_Id; 680 New_Perm : Perm_Kind) 681 return Perm_Tree_Access; 682 -- This function sets the permissions of a given node_id in the 683 -- permission environment as well as in all the prefixes of the path 684 -- to the one given in parameter (P). 685 686 procedure Setup_Globals (Subp : Entity_Id); 687 -- Takes a subprogram as input, and sets up the environment by adding 688 -- global items with appropriate permissions. 689 690 procedure Setup_Parameter_Or_Global 691 (Id : Entity_Id; 692 Mode : Formal_Kind; 693 Global_Var : Boolean); 694 -- Auxiliary procedure to Setup_Parameters and Setup_Globals 695 696 procedure Setup_Parameters (Subp : Entity_Id); 697 -- Takes a subprogram as input, and sets up the environment by adding 698 -- formal parameters with appropriate permissions. 699 700 function Has_Ownership_Aspect_True 701 (N : Node_Id; 702 Msg : String) 703 return Boolean; 704 -- Takes a node as an input, and finds out whether it has ownership aspect 705 -- True or False. This function is recursive whenever the node has a 706 -- composite type. Access-to-objects have ownership aspect False if they 707 -- have a general access type. 708 709 ---------------------- 710 -- Global Variables -- 711 ---------------------- 712 713 Current_Perm_Env : Perm_Env; 714 -- The permission environment that is used for the analysis. This 715 -- environment can be saved, modified, reinitialized, but should be the 716 -- only one valid from which to extract the permissions of the paths in 717 -- scope. The analysis ensures at each point that this variables contains 718 -- a valid permission environment with all bindings in scope. 719 720 Current_Checking_Mode : Checking_Mode := Read; 721 -- The current analysis mode. This global variable indicates at each point 722 -- of the analysis whether the node being analyzed is moved, borrowed, 723 -- assigned, read, ... The full list of possible values can be found in 724 -- the declaration of type Checking_Mode. 725 726 Current_Loops_Envs : Env_Backups; 727 -- This variable contains saves of permission environments at each loop the 728 -- analysis entered. Each saved environment can be reached with the label 729 -- of the loop. 730 731 Current_Loops_Accumulators : Env_Backups; 732 -- This variable contains the environments used as accumulators for loops, 733 -- that consist of the merge of all environments at each exit point of 734 -- the loop (which can also be the entry point of the loop in the case of 735 -- non-infinite loops), each of them reachable from the label of the loop. 736 -- We require that the environment stored in the accumulator be less 737 -- restrictive than the saved environment at the beginning of the loop, and 738 -- the permission environment after the loop is equal to the accumulator. 739 740 Current_Initialization_Map : Initialization_Map; 741 -- This variable contains a map that binds each variable of the analyzed 742 -- source code to a boolean that becomes true whenever the variable is used 743 -- after declaration. Hence we can exclude from analysis variables that 744 -- are just declared and never accessed, typically at package declaration. 745 746 -------------------------- 747 -- Check_Call_Statement -- 748 -------------------------- 749 750 procedure Check_Call_Statement (Call : Node_Id) is 751 Saved_Env : Perm_Env; 752 753 procedure Iterate_Call_In is new 754 Iterate_Call_Parameters (Check_Param_In); 755 procedure Iterate_Call_Out is new 756 Iterate_Call_Parameters (Check_Param_Out); 757 758 begin 759 -- Save environment, so that the modifications done by analyzing the 760 -- parameters are not kept at the end of the call. 761 762 Copy_Env (Current_Perm_Env, Saved_Env); 763 764 -- We first check the globals then parameters to handle the 765 -- No_Parameter_Aliasing Restriction. An out or in-out global is 766 -- considered as borrowing while a parameter with the same mode is 767 -- a move. This order disallow passing a part of a variable to a 768 -- subprogram if it is referenced as a global by the callable (when 769 -- writable). 770 -- For paremeters, we fisrt check in parameters and then the out ones. 771 -- This is to avoid Observing or Borrowing objects that are already 772 -- moved. This order is not mandatory but allows to catch runtime 773 -- errors like null pointer dereferencement at the analysis time. 774 775 Current_Checking_Mode := Read; 776 Check_Globals (Get_Pragma (Get_Called_Entity (Call), Pragma_Global)); 777 Iterate_Call_In (Call); 778 Iterate_Call_Out (Call); 779 780 -- Restore environment, because after borrowing/observing actual 781 -- parameters, they get their permission reverted to the ones before 782 -- the call. 783 784 Free_Env (Current_Perm_Env); 785 Copy_Env (Saved_Env, Current_Perm_Env); 786 Free_Env (Saved_Env); 787 end Check_Call_Statement; 788 789 ------------------------- 790 -- Check_Callable_Body -- 791 ------------------------- 792 793 procedure Check_Callable_Body (Body_N : Node_Id) is 794 795 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 796 Saved_Env : Perm_Env; 797 Saved_Init_Map : Initialization_Map; 798 New_Env : Perm_Env; 799 Body_Id : constant Entity_Id := Defining_Entity (Body_N); 800 Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); 801 802 begin 803 -- Check if SPARK pragma is not set to Off 804 805 if Present (SPARK_Pragma (Defining_Entity (Body_N))) then 806 if Get_SPARK_Mode_From_Annotation 807 (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On 808 then 809 return; 810 end if; 811 else 812 return; 813 end if; 814 815 -- Save environment and put a new one in place 816 817 Copy_Env (Current_Perm_Env, Saved_Env); 818 819 -- Save initialization map 820 821 Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map); 822 Current_Checking_Mode := Read; 823 Current_Perm_Env := New_Env; 824 825 -- Add formals and globals to the environment with adequate permissions 826 827 if Is_Subprogram_Or_Entry (Spec_Id) then 828 Setup_Parameters (Spec_Id); 829 Setup_Globals (Spec_Id); 830 end if; 831 832 -- Analyze the body of the function 833 834 Check_List (Declarations (Body_N)); 835 Check_Node (Handled_Statement_Sequence (Body_N)); 836 837 -- Check the read-write permissions of borrowed parameters/globals 838 839 if Ekind_In (Spec_Id, E_Procedure, E_Entry) 840 and then not No_Return (Spec_Id) 841 then 842 Return_Globals (Spec_Id); 843 end if; 844 845 -- Free the environments 846 847 Free_Env (Current_Perm_Env); 848 Copy_Env (Saved_Env, Current_Perm_Env); 849 Free_Env (Saved_Env); 850 851 -- Restore initialization map 852 853 Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map); 854 Reset (Saved_Init_Map); 855 856 -- The assignment of all out parameters will be done by caller 857 858 Current_Checking_Mode := Mode_Before; 859 end Check_Callable_Body; 860 861 ----------------------- 862 -- Check_Declaration -- 863 ----------------------- 864 865 procedure Check_Declaration (Decl : Node_Id) is 866 Target_Ent : constant Entity_Id := Defining_Identifier (Decl); 867 Target_Typ : Node_Id renames Etype (Target_Ent); 868 869 Target_View_Typ : Entity_Id; 870 871 Check : Boolean := True; 872 begin 873 if Present (Full_View (Target_Typ)) then 874 Target_View_Typ := Full_View (Target_Typ); 875 else 876 Target_View_Typ := Target_Typ; 877 end if; 878 879 case N_Declaration'(Nkind (Decl)) is 880 when N_Full_Type_Declaration => 881 if not Has_Ownership_Aspect_True (Target_Ent, "type declaration") 882 then 883 Check := False; 884 end if; 885 886 -- ??? What about component declarations with defaults. 887 888 when N_Object_Declaration => 889 if (Is_Access_Type (Target_View_Typ) 890 or else Is_Deep (Target_Typ)) 891 and then not Has_Ownership_Aspect_True 892 (Target_Ent, "Object declaration ") 893 then 894 Check := False; 895 end if; 896 897 if Is_Anonymous_Access_Type (Target_View_Typ) 898 and then not Present (Expression (Decl)) 899 then 900 901 -- ??? Check the case of default value (AI) 902 -- ??? How an anonymous access type can be with default exp? 903 904 Error_Msg_NE ("? object declaration & has OAF (Anonymous " 905 & "access-to-object with no initialization)", 906 Decl, Target_Ent); 907 908 -- If it it an initialization 909 910 elsif Present (Expression (Decl)) and Check then 911 912 -- Find out the operation to be done on the right-hand side 913 914 -- Initializing object, access type 915 916 if Is_Access_Type (Target_View_Typ) then 917 918 -- Initializing object, constant access type 919 920 if Is_Constant_Object (Target_Ent) then 921 922 -- Initializing object, constant access to variable type 923 924 if not Is_Access_Constant (Target_View_Typ) then 925 Current_Checking_Mode := Borrow; 926 927 -- Initializing object, constant access to constant type 928 929 -- Initializing object, 930 -- constant access to constant anonymous type. 931 932 elsif Is_Anonymous_Access_Type (Target_View_Typ) then 933 934 -- This is an object declaration so the target 935 -- of the assignement is a stand-alone object. 936 937 Current_Checking_Mode := Observe; 938 939 -- Initializing object, constant access to constant 940 -- named type. 941 942 else 943 -- If named then it is a general access type 944 -- Hence, Has_Ownership_Aspec_True is False. 945 946 raise Program_Error; 947 end if; 948 949 -- Initializing object, variable access type 950 951 else 952 -- Initializing object, variable access to variable type 953 954 if not Is_Access_Constant (Target_View_Typ) then 955 956 -- Initializing object, variable named access to 957 -- variable type. 958 959 if not Is_Anonymous_Access_Type (Target_View_Typ) then 960 Current_Checking_Mode := Move; 961 962 -- Initializing object, variable anonymous access to 963 -- variable type. 964 965 else 966 -- This is an object declaration so the target 967 -- object of the assignement is a stand-alone 968 -- object. 969 970 Current_Checking_Mode := Borrow; 971 end if; 972 973 -- Initializing object, variable access to constant type 974 975 else 976 -- Initializing object, 977 -- variable named access to constant type. 978 979 if not Is_Anonymous_Access_Type (Target_View_Typ) then 980 Error_Msg_N ("assignment not allowed, Ownership " 981 & "Aspect False (Anonymous Access " 982 & "Object)", Decl); 983 Check := False; 984 985 -- Initializing object, 986 -- variable anonymous access to constant type. 987 988 else 989 -- This is an object declaration so the target 990 -- of the assignement is a stand-alone object. 991 992 Current_Checking_Mode := Observe; 993 end if; 994 end if; 995 end if; 996 997 -- Initializing object, composite (deep) type 998 999 elsif Is_Deep (Target_Typ) then 1000 1001 -- Initializing object, constant composite type 1002 1003 if Is_Constant_Object (Target_Ent) then 1004 Current_Checking_Mode := Observe; 1005 1006 -- Initializing object, variable composite type 1007 1008 else 1009 1010 -- Initializing object, variable anonymous composite type 1011 1012 if Nkind (Object_Definition (Decl)) = 1013 N_Constrained_Array_Definition 1014 1015 -- An N_Constrained_Array_Definition is an anonymous 1016 -- array (to be checked). Record types are always 1017 -- named and are considered in the else part. 1018 1019 then 1020 declare 1021 Com_Ty : constant Node_Id := 1022 Component_Type (Etype (Target_Typ)); 1023 begin 1024 1025 if Is_Access_Type (Com_Ty) then 1026 1027 -- If components are of anonymous type 1028 1029 if Is_Anonymous_Access_Type (Com_Ty) then 1030 if Is_Access_Constant (Com_Ty) then 1031 Current_Checking_Mode := Observe; 1032 1033 else 1034 Current_Checking_Mode := Borrow; 1035 end if; 1036 1037 else 1038 Current_Checking_Mode := Move; 1039 end if; 1040 1041 elsif Is_Deep (Com_Ty) then 1042 1043 -- This is certainly named so it is a move 1044 1045 Current_Checking_Mode := Move; 1046 end if; 1047 end; 1048 1049 else 1050 Current_Checking_Mode := Move; 1051 end if; 1052 end if; 1053 1054 end if; 1055 end if; 1056 1057 if Check then 1058 Check_Node (Expression (Decl)); 1059 end if; 1060 1061 -- If lhs is not a pointer, we still give it the unrestricted 1062 -- state which is useless but not harmful. 1063 1064 declare 1065 Elem : Perm_Tree_Access; 1066 Deep : constant Boolean := Is_Deep (Target_Typ); 1067 1068 begin 1069 -- Note that all declared variables are set to the unrestricted 1070 -- state. 1071 -- 1072 -- If variables are not initialized: 1073 -- unrestricted to every declared object. 1074 -- Exp: 1075 -- R : Rec 1076 -- S : Rec := (...) 1077 -- R := S 1078 -- The assignement R := S is not allowed in the new rules 1079 -- if R is not unrestricted. 1080 -- 1081 -- If variables are initialized: 1082 -- If it is a move, then the target is unrestricted 1083 -- If it is a borrow, then the target is unrestricted 1084 -- If it is an observe, then the target should be observed 1085 1086 if Current_Checking_Mode = Observe then 1087 Elem := new Perm_Tree_Wrapper' 1088 (Tree => 1089 (Kind => Entire_Object, 1090 Is_Node_Deep => Deep, 1091 Permission => Observed, 1092 Children_Permission => Observed)); 1093 else 1094 Elem := new Perm_Tree_Wrapper' 1095 (Tree => 1096 (Kind => Entire_Object, 1097 Is_Node_Deep => Deep, 1098 Permission => Unrestricted, 1099 Children_Permission => Unrestricted)); 1100 end if; 1101 1102 -- Create new tree for defining identifier 1103 1104 Set (Current_Perm_Env, 1105 Unique_Entity (Defining_Identifier (Decl)), 1106 Elem); 1107 pragma Assert (Get_First (Current_Perm_Env) /= null); 1108 end; 1109 1110 when N_Subtype_Declaration => 1111 Check_Node (Subtype_Indication (Decl)); 1112 1113 when N_Iterator_Specification => 1114 null; 1115 1116 when N_Loop_Parameter_Specification => 1117 null; 1118 1119 -- Checking should not be called directly on these nodes 1120 1121 when N_Function_Specification 1122 | N_Entry_Declaration 1123 | N_Procedure_Specification 1124 | N_Component_Declaration 1125 => 1126 raise Program_Error; 1127 1128 -- Ignored constructs for pointer checking 1129 1130 when N_Formal_Object_Declaration 1131 | N_Formal_Type_Declaration 1132 | N_Incomplete_Type_Declaration 1133 | N_Private_Extension_Declaration 1134 | N_Private_Type_Declaration 1135 | N_Protected_Type_Declaration 1136 => 1137 null; 1138 1139 -- The following nodes are rewritten by semantic analysis 1140 1141 when N_Expression_Function => 1142 raise Program_Error; 1143 end case; 1144 end Check_Declaration; 1145 1146 ---------------------- 1147 -- Check_Expression -- 1148 ---------------------- 1149 1150 procedure Check_Expression (Expr : Node_Id) is 1151 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 1152 begin 1153 case N_Subexpr'(Nkind (Expr)) is 1154 when N_Procedure_Call_Statement 1155 | N_Function_Call 1156 => 1157 Check_Call_Statement (Expr); 1158 1159 when N_Identifier 1160 | N_Expanded_Name 1161 => 1162 -- Check if identifier is pointing to nothing (On/Off/...) 1163 1164 if not Present (Entity (Expr)) then 1165 return; 1166 end if; 1167 1168 -- Do not analyze things that are not of object Kind 1169 1170 if Ekind (Entity (Expr)) not in Object_Kind then 1171 return; 1172 end if; 1173 1174 -- Consider as ident 1175 1176 Process_Path (Expr); 1177 1178 -- Switch to read mode and then check the readability of each operand 1179 1180 when N_Binary_Op => 1181 Current_Checking_Mode := Read; 1182 Check_Node (Left_Opnd (Expr)); 1183 Check_Node (Right_Opnd (Expr)); 1184 1185 -- Switch to read mode and then check the readability of each operand 1186 1187 when N_Op_Abs 1188 | N_Op_Minus 1189 | N_Op_Not 1190 | N_Op_Plus 1191 => 1192 Current_Checking_Mode := Read; 1193 Check_Node (Right_Opnd (Expr)); 1194 1195 -- Forbid all deep expressions for Attribute ??? 1196 -- What about generics? (formal parameters). 1197 1198 when N_Attribute_Reference => 1199 case Attribute_Name (Expr) is 1200 when Name_Access => 1201 Error_Msg_N ("access attribute not allowed", Expr); 1202 1203 when Name_Last 1204 | Name_First 1205 => 1206 Current_Checking_Mode := Read; 1207 Check_Node (Prefix (Expr)); 1208 1209 when Name_Min => 1210 Current_Checking_Mode := Read; 1211 Check_Node (Prefix (Expr)); 1212 1213 when Name_Image => 1214 Check_List (Expressions (Expr)); 1215 1216 when Name_Img => 1217 Check_Node (Prefix (Expr)); 1218 1219 when Name_SPARK_Mode => 1220 null; 1221 1222 when Name_Value => 1223 Current_Checking_Mode := Read; 1224 Check_Node (Prefix (Expr)); 1225 1226 when Name_Update => 1227 Check_List (Expressions (Expr)); 1228 Check_Node (Prefix (Expr)); 1229 1230 when Name_Pred 1231 | Name_Succ 1232 => 1233 Check_List (Expressions (Expr)); 1234 Check_Node (Prefix (Expr)); 1235 1236 when Name_Length => 1237 Current_Checking_Mode := Read; 1238 Check_Node (Prefix (Expr)); 1239 1240 -- Any Attribute referring to the underlying memory is ignored 1241 -- in the analysis. This means that taking the address of a 1242 -- variable makes a silent alias that is not rejected by the 1243 -- analysis. 1244 1245 when Name_Address 1246 | Name_Alignment 1247 | Name_Component_Size 1248 | Name_First_Bit 1249 | Name_Last_Bit 1250 | Name_Size 1251 | Name_Position 1252 => 1253 null; 1254 1255 -- Attributes referring to types (get values from types), hence 1256 -- no need to check either for borrows or any loans. 1257 1258 when Name_Base 1259 | Name_Val 1260 => 1261 null; 1262 -- Other attributes that fall out of the scope of the analysis 1263 1264 when others => 1265 null; 1266 end case; 1267 1268 when N_In => 1269 Current_Checking_Mode := Read; 1270 Check_Node (Left_Opnd (Expr)); 1271 Check_Node (Right_Opnd (Expr)); 1272 1273 when N_Not_In => 1274 Current_Checking_Mode := Read; 1275 Check_Node (Left_Opnd (Expr)); 1276 Check_Node (Right_Opnd (Expr)); 1277 1278 -- Switch to read mode and then check the readability of each operand 1279 1280 when N_And_Then 1281 | N_Or_Else 1282 => 1283 Current_Checking_Mode := Read; 1284 Check_Node (Left_Opnd (Expr)); 1285 Check_Node (Right_Opnd (Expr)); 1286 1287 -- Check the arguments of the call 1288 1289 when N_Explicit_Dereference => 1290 Process_Path (Expr); 1291 1292 -- Copy environment, run on each branch, and then merge 1293 1294 when N_If_Expression => 1295 declare 1296 Saved_Env : Perm_Env; 1297 1298 -- Accumulator for the different branches 1299 1300 New_Env : Perm_Env; 1301 Elmt : Node_Id := First (Expressions (Expr)); 1302 1303 begin 1304 Current_Checking_Mode := Read; 1305 Check_Node (Elmt); 1306 Current_Checking_Mode := Mode_Before; 1307 1308 -- Save environment 1309 1310 Copy_Env (Current_Perm_Env, Saved_Env); 1311 1312 -- Here we have the original env in saved, current with a fresh 1313 -- copy, and new aliased. 1314 1315 -- THEN PART 1316 1317 Next (Elmt); 1318 Check_Node (Elmt); 1319 1320 -- Here the new_environment contains curr env after then block 1321 1322 -- ELSE part 1323 -- Restore environment before if 1324 Copy_Env (Current_Perm_Env, New_Env); 1325 Free_Env (Current_Perm_Env); 1326 Copy_Env (Saved_Env, Current_Perm_Env); 1327 1328 -- Here new environment contains the environment after then and 1329 -- current the fresh copy of old one. 1330 1331 Next (Elmt); 1332 Check_Node (Elmt); 1333 1334 -- CLEANUP 1335 1336 Copy_Env (New_Env, Current_Perm_Env); 1337 Free_Env (New_Env); 1338 Free_Env (Saved_Env); 1339 end; 1340 1341 when N_Indexed_Component => 1342 Process_Path (Expr); 1343 1344 -- Analyze the expression that is getting qualified 1345 1346 when N_Qualified_Expression => 1347 Check_Node (Expression (Expr)); 1348 1349 when N_Quantified_Expression => 1350 declare 1351 Saved_Env : Perm_Env; 1352 1353 begin 1354 Copy_Env (Current_Perm_Env, Saved_Env); 1355 Current_Checking_Mode := Read; 1356 Check_Node (Iterator_Specification (Expr)); 1357 Check_Node (Loop_Parameter_Specification (Expr)); 1358 1359 Check_Node (Condition (Expr)); 1360 Free_Env (Current_Perm_Env); 1361 Copy_Env (Saved_Env, Current_Perm_Env); 1362 Free_Env (Saved_Env); 1363 end; 1364 -- Analyze the list of associations in the aggregate 1365 1366 when N_Aggregate => 1367 Check_List (Expressions (Expr)); 1368 Check_List (Component_Associations (Expr)); 1369 1370 when N_Allocator => 1371 Check_Node (Expression (Expr)); 1372 1373 when N_Case_Expression => 1374 declare 1375 Saved_Env : Perm_Env; 1376 1377 -- Accumulator for the different branches 1378 1379 New_Env : Perm_Env; 1380 Elmt : Node_Id := First (Alternatives (Expr)); 1381 1382 begin 1383 Current_Checking_Mode := Read; 1384 Check_Node (Expression (Expr)); 1385 Current_Checking_Mode := Mode_Before; 1386 1387 -- Save environment 1388 1389 Copy_Env (Current_Perm_Env, Saved_Env); 1390 1391 -- Here we have the original env in saved, current with a fresh 1392 -- copy, and new aliased. 1393 1394 -- First alternative 1395 1396 Check_Node (Elmt); 1397 Next (Elmt); 1398 Copy_Env (Current_Perm_Env, New_Env); 1399 Free_Env (Current_Perm_Env); 1400 1401 -- Other alternatives 1402 1403 while Present (Elmt) loop 1404 1405 -- Restore environment 1406 1407 Copy_Env (Saved_Env, Current_Perm_Env); 1408 Check_Node (Elmt); 1409 Next (Elmt); 1410 end loop; 1411 -- CLEANUP 1412 1413 Copy_Env (Saved_Env, Current_Perm_Env); 1414 Free_Env (New_Env); 1415 Free_Env (Saved_Env); 1416 end; 1417 -- Analyze the list of associates in the aggregate as well as the 1418 -- ancestor part. 1419 1420 when N_Extension_Aggregate => 1421 Check_Node (Ancestor_Part (Expr)); 1422 Check_List (Expressions (Expr)); 1423 1424 when N_Range => 1425 Check_Node (Low_Bound (Expr)); 1426 Check_Node (High_Bound (Expr)); 1427 1428 -- We arrived at a path. Process it. 1429 1430 when N_Selected_Component => 1431 Process_Path (Expr); 1432 1433 when N_Slice => 1434 Process_Path (Expr); 1435 1436 when N_Type_Conversion => 1437 Check_Node (Expression (Expr)); 1438 1439 when N_Unchecked_Type_Conversion => 1440 Check_Node (Expression (Expr)); 1441 1442 -- Checking should not be called directly on these nodes 1443 1444 when N_Target_Name => 1445 raise Program_Error; 1446 1447 -- Unsupported constructs in SPARK 1448 1449 when N_Delta_Aggregate => 1450 Error_Msg_N ("unsupported construct in SPARK", Expr); 1451 1452 -- Ignored constructs for pointer checking 1453 1454 when N_Character_Literal 1455 | N_Null 1456 | N_Numeric_Or_String_Literal 1457 | N_Operator_Symbol 1458 | N_Raise_Expression 1459 | N_Raise_xxx_Error 1460 => 1461 null; 1462 -- The following nodes are never generated in GNATprove mode 1463 1464 when N_Expression_With_Actions 1465 | N_Reference 1466 | N_Unchecked_Expression 1467 => 1468 raise Program_Error; 1469 end case; 1470 end Check_Expression; 1471 1472 ------------------- 1473 -- Check_Globals -- 1474 ------------------- 1475 1476 procedure Check_Globals (N : Node_Id) is 1477 begin 1478 if Nkind (N) = N_Empty then 1479 return; 1480 end if; 1481 1482 declare 1483 pragma Assert (List_Length (Pragma_Argument_Associations (N)) = 1); 1484 PAA : constant Node_Id := First (Pragma_Argument_Associations (N)); 1485 pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association); 1486 Row : Node_Id; 1487 The_Mode : Name_Id; 1488 RHS : Node_Id; 1489 1490 procedure Process (Mode : Name_Id; The_Global : Entity_Id); 1491 procedure Process (Mode : Name_Id; The_Global : Node_Id) is 1492 Ident_Elt : constant Entity_Id := 1493 Unique_Entity (Entity (The_Global)); 1494 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 1495 1496 begin 1497 if Ekind (Ident_Elt) = E_Abstract_State then 1498 return; 1499 end if; 1500 case Mode is 1501 when Name_Input 1502 | Name_Proof_In 1503 => 1504 Current_Checking_Mode := Observe; 1505 Check_Node (The_Global); 1506 1507 when Name_Output 1508 | Name_In_Out 1509 => 1510 -- ??? Borrow not Move? 1511 Current_Checking_Mode := Borrow; 1512 Check_Node (The_Global); 1513 1514 when others => 1515 raise Program_Error; 1516 end case; 1517 Current_Checking_Mode := Mode_Before; 1518 end Process; 1519 1520 begin 1521 if Nkind (Expression (PAA)) = N_Null then 1522 1523 -- global => null 1524 -- No globals, nothing to do 1525 1526 return; 1527 1528 elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then 1529 1530 -- global => foo 1531 -- A single input 1532 1533 Process (Name_Input, Expression (PAA)); 1534 1535 elsif Nkind (Expression (PAA)) = N_Aggregate 1536 and then Expressions (Expression (PAA)) /= No_List 1537 then 1538 -- global => (foo, bar) 1539 -- Inputs 1540 1541 RHS := First (Expressions (Expression (PAA))); 1542 while Present (RHS) loop 1543 case Nkind (RHS) is 1544 when N_Identifier 1545 | N_Expanded_Name 1546 => 1547 Process (Name_Input, RHS); 1548 1549 when N_Numeric_Or_String_Literal => 1550 Process (Name_Input, Original_Node (RHS)); 1551 1552 when others => 1553 raise Program_Error; 1554 end case; 1555 RHS := Next (RHS); 1556 end loop; 1557 1558 elsif Nkind (Expression (PAA)) = N_Aggregate 1559 and then Component_Associations (Expression (PAA)) /= No_List 1560 then 1561 -- global => (mode => foo, 1562 -- mode => (bar, baz)) 1563 -- A mixture of things 1564 1565 declare 1566 CA : constant List_Id := 1567 Component_Associations (Expression (PAA)); 1568 begin 1569 Row := First (CA); 1570 while Present (Row) loop 1571 pragma Assert (List_Length (Choices (Row)) = 1); 1572 The_Mode := Chars (First (Choices (Row))); 1573 RHS := Expression (Row); 1574 1575 case Nkind (RHS) is 1576 when N_Aggregate => 1577 RHS := First (Expressions (RHS)); 1578 while Present (RHS) loop 1579 case Nkind (RHS) is 1580 when N_Numeric_Or_String_Literal => 1581 Process (The_Mode, Original_Node (RHS)); 1582 1583 when others => 1584 Process (The_Mode, RHS); 1585 end case; 1586 RHS := Next (RHS); 1587 end loop; 1588 1589 when N_Identifier 1590 | N_Expanded_Name 1591 => 1592 Process (The_Mode, RHS); 1593 1594 when N_Null => 1595 null; 1596 1597 when N_Numeric_Or_String_Literal => 1598 Process (The_Mode, Original_Node (RHS)); 1599 1600 when others => 1601 raise Program_Error; 1602 end case; 1603 Row := Next (Row); 1604 end loop; 1605 end; 1606 1607 else 1608 raise Program_Error; 1609 end if; 1610 end; 1611 end Check_Globals; 1612 1613 ---------------- 1614 -- Check_List -- 1615 ---------------- 1616 1617 procedure Check_List (L : List_Id) is 1618 N : Node_Id; 1619 begin 1620 N := First (L); 1621 while Present (N) loop 1622 Check_Node (N); 1623 Next (N); 1624 end loop; 1625 end Check_List; 1626 1627 -------------------------- 1628 -- Check_Loop_Statement -- 1629 -------------------------- 1630 1631 procedure Check_Loop_Statement (Loop_N : Node_Id) is 1632 1633 -- Local variables 1634 1635 Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N)); 1636 Loop_Env : constant Perm_Env_Access := new Perm_Env; 1637 1638 begin 1639 -- Save environment prior to the loop 1640 1641 Copy_Env (From => Current_Perm_Env, To => Loop_Env.all); 1642 1643 -- Add saved environment to loop environment 1644 1645 Set (Current_Loops_Envs, Loop_Name, Loop_Env); 1646 1647 -- If the loop is not a plain-loop, then it may either never be entered, 1648 -- or it may be exited after a number of iterations. Hence add the 1649 -- current permission environment as the initial loop exit environment. 1650 -- Otherwise, the loop exit environment remains empty until it is 1651 -- populated by analyzing exit statements. 1652 1653 if Present (Iteration_Scheme (Loop_N)) then 1654 declare 1655 Exit_Env : constant Perm_Env_Access := new Perm_Env; 1656 1657 begin 1658 Copy_Env (From => Current_Perm_Env, To => Exit_Env.all); 1659 Set (Current_Loops_Accumulators, Loop_Name, Exit_Env); 1660 end; 1661 end if; 1662 1663 -- Analyze loop 1664 1665 Check_Node (Iteration_Scheme (Loop_N)); 1666 Check_List (Statements (Loop_N)); 1667 1668 -- Set environment to the one for exiting the loop 1669 1670 declare 1671 Exit_Env : constant Perm_Env_Access := 1672 Get (Current_Loops_Accumulators, Loop_Name); 1673 begin 1674 Free_Env (Current_Perm_Env); 1675 1676 -- In the normal case, Exit_Env is not null and we use it. In the 1677 -- degraded case of a plain-loop without exit statements, Exit_Env is 1678 -- null, and we use the initial permission environment at the start 1679 -- of the loop to continue analysis. Any environment would be fine 1680 -- here, since the code after the loop is dead code, but this way we 1681 -- avoid spurious errors by having at least variables in scope inside 1682 -- the environment. 1683 1684 if Exit_Env /= null then 1685 Copy_Env (From => Exit_Env.all, To => Current_Perm_Env); 1686 Free_Env (Loop_Env.all); 1687 Free_Env (Exit_Env.all); 1688 else 1689 Copy_Env (From => Loop_Env.all, To => Current_Perm_Env); 1690 Free_Env (Loop_Env.all); 1691 end if; 1692 end; 1693 end Check_Loop_Statement; 1694 1695 ---------------- 1696 -- Check_Node -- 1697 ---------------- 1698 1699 procedure Check_Node (N : Node_Id) is 1700 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 1701 begin 1702 case Nkind (N) is 1703 when N_Declaration => 1704 Check_Declaration (N); 1705 1706 when N_Subexpr => 1707 Check_Expression (N); 1708 1709 when N_Subtype_Indication => 1710 Check_Node (Constraint (N)); 1711 1712 when N_Body_Stub => 1713 Check_Node (Get_Body_From_Stub (N)); 1714 1715 when N_Statement_Other_Than_Procedure_Call => 1716 Check_Statement (N); 1717 1718 when N_Package_Body => 1719 Check_Package_Body (N); 1720 1721 when N_Subprogram_Body 1722 | N_Entry_Body 1723 | N_Task_Body 1724 => 1725 Check_Callable_Body (N); 1726 1727 when N_Protected_Body => 1728 Check_List (Declarations (N)); 1729 1730 when N_Package_Declaration => 1731 declare 1732 Spec : constant Node_Id := Specification (N); 1733 1734 begin 1735 Current_Checking_Mode := Read; 1736 Check_List (Visible_Declarations (Spec)); 1737 Check_List (Private_Declarations (Spec)); 1738 1739 Return_Declarations (Visible_Declarations (Spec)); 1740 Return_Declarations (Private_Declarations (Spec)); 1741 end; 1742 1743 when N_Iteration_Scheme => 1744 Current_Checking_Mode := Read; 1745 Check_Node (Condition (N)); 1746 Check_Node (Iterator_Specification (N)); 1747 Check_Node (Loop_Parameter_Specification (N)); 1748 1749 when N_Case_Expression_Alternative => 1750 Current_Checking_Mode := Read; 1751 Check_List (Discrete_Choices (N)); 1752 Current_Checking_Mode := Mode_Before; 1753 Check_Node (Expression (N)); 1754 1755 when N_Case_Statement_Alternative => 1756 Current_Checking_Mode := Read; 1757 Check_List (Discrete_Choices (N)); 1758 Current_Checking_Mode := Mode_Before; 1759 Check_List (Statements (N)); 1760 1761 when N_Component_Association => 1762 Check_Node (Expression (N)); 1763 1764 when N_Handled_Sequence_Of_Statements => 1765 Check_List (Statements (N)); 1766 1767 when N_Parameter_Association => 1768 Check_Node (Explicit_Actual_Parameter (N)); 1769 1770 when N_Range_Constraint => 1771 Check_Node (Range_Expression (N)); 1772 1773 when N_Index_Or_Discriminant_Constraint => 1774 Check_List (Constraints (N)); 1775 1776 -- Checking should not be called directly on these nodes 1777 1778 when N_Abortable_Part 1779 | N_Accept_Alternative 1780 | N_Access_Definition 1781 | N_Access_Function_Definition 1782 | N_Access_Procedure_Definition 1783 | N_Access_To_Object_Definition 1784 | N_Aspect_Specification 1785 | N_Compilation_Unit 1786 | N_Compilation_Unit_Aux 1787 | N_Component_Clause 1788 | N_Component_Definition 1789 | N_Component_List 1790 | N_Constrained_Array_Definition 1791 | N_Contract 1792 | N_Decimal_Fixed_Point_Definition 1793 | N_Defining_Character_Literal 1794 | N_Defining_Identifier 1795 | N_Defining_Operator_Symbol 1796 | N_Defining_Program_Unit_Name 1797 | N_Delay_Alternative 1798 | N_Derived_Type_Definition 1799 | N_Designator 1800 | N_Discriminant_Specification 1801 | N_Elsif_Part 1802 | N_Entry_Body_Formal_Part 1803 | N_Enumeration_Type_Definition 1804 | N_Entry_Call_Alternative 1805 | N_Entry_Index_Specification 1806 | N_Error 1807 | N_Exception_Handler 1808 | N_Floating_Point_Definition 1809 | N_Formal_Decimal_Fixed_Point_Definition 1810 | N_Formal_Derived_Type_Definition 1811 | N_Formal_Discrete_Type_Definition 1812 | N_Formal_Floating_Point_Definition 1813 | N_Formal_Incomplete_Type_Definition 1814 | N_Formal_Modular_Type_Definition 1815 | N_Formal_Ordinary_Fixed_Point_Definition 1816 | N_Formal_Private_Type_Definition 1817 | N_Formal_Signed_Integer_Type_Definition 1818 | N_Generic_Association 1819 | N_Mod_Clause 1820 | N_Modular_Type_Definition 1821 | N_Ordinary_Fixed_Point_Definition 1822 | N_Package_Specification 1823 | N_Parameter_Specification 1824 | N_Pragma_Argument_Association 1825 | N_Protected_Definition 1826 | N_Push_Pop_xxx_Label 1827 | N_Real_Range_Specification 1828 | N_Record_Definition 1829 | N_SCIL_Dispatch_Table_Tag_Init 1830 | N_SCIL_Dispatching_Call 1831 | N_SCIL_Membership_Test 1832 | N_Signed_Integer_Type_Definition 1833 | N_Subunit 1834 | N_Task_Definition 1835 | N_Terminate_Alternative 1836 | N_Triggering_Alternative 1837 | N_Unconstrained_Array_Definition 1838 | N_Unused_At_Start 1839 | N_Unused_At_End 1840 | N_Variant 1841 | N_Variant_Part 1842 => 1843 raise Program_Error; 1844 1845 -- Unsupported constructs in SPARK 1846 1847 when N_Iterated_Component_Association => 1848 Error_Msg_N ("unsupported construct in SPARK", N); 1849 1850 -- Ignored constructs for pointer checking 1851 1852 when N_Abstract_Subprogram_Declaration 1853 | N_At_Clause 1854 | N_Attribute_Definition_Clause 1855 | N_Call_Marker 1856 | N_Delta_Constraint 1857 | N_Digits_Constraint 1858 | N_Empty 1859 | N_Enumeration_Representation_Clause 1860 | N_Exception_Declaration 1861 | N_Exception_Renaming_Declaration 1862 | N_Formal_Package_Declaration 1863 | N_Formal_Subprogram_Declaration 1864 | N_Freeze_Entity 1865 | N_Freeze_Generic_Entity 1866 | N_Function_Instantiation 1867 | N_Generic_Function_Renaming_Declaration 1868 | N_Generic_Package_Declaration 1869 | N_Generic_Package_Renaming_Declaration 1870 | N_Generic_Procedure_Renaming_Declaration 1871 | N_Generic_Subprogram_Declaration 1872 | N_Implicit_Label_Declaration 1873 | N_Itype_Reference 1874 | N_Label 1875 | N_Number_Declaration 1876 | N_Object_Renaming_Declaration 1877 | N_Others_Choice 1878 | N_Package_Instantiation 1879 | N_Package_Renaming_Declaration 1880 | N_Pragma 1881 | N_Procedure_Instantiation 1882 | N_Record_Representation_Clause 1883 | N_Subprogram_Declaration 1884 | N_Subprogram_Renaming_Declaration 1885 | N_Task_Type_Declaration 1886 | N_Use_Package_Clause 1887 | N_With_Clause 1888 | N_Use_Type_Clause 1889 | N_Validate_Unchecked_Conversion 1890 | N_Variable_Reference_Marker 1891 | N_Discriminant_Association 1892 1893 -- ??? check whether we should do sth special for 1894 -- N_Discriminant_Association, or maybe raise a program error. 1895 => 1896 null; 1897 -- The following nodes are rewritten by semantic analysis 1898 1899 when N_Single_Protected_Declaration 1900 | N_Single_Task_Declaration 1901 => 1902 raise Program_Error; 1903 end case; 1904 1905 Current_Checking_Mode := Mode_Before; 1906 end Check_Node; 1907 1908 ------------------------ 1909 -- Check_Package_Body -- 1910 ------------------------ 1911 1912 procedure Check_Package_Body (Pack : Node_Id) is 1913 Saved_Env : Perm_Env; 1914 CorSp : Node_Id; 1915 1916 begin 1917 if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then 1918 if Get_SPARK_Mode_From_Annotation 1919 (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On 1920 then 1921 return; 1922 end if; 1923 else 1924 return; 1925 end if; 1926 1927 CorSp := Parent (Corresponding_Spec (Pack)); 1928 while Nkind (CorSp) /= N_Package_Specification loop 1929 CorSp := Parent (CorSp); 1930 end loop; 1931 1932 Check_List (Visible_Declarations (CorSp)); 1933 1934 -- Save environment 1935 1936 Copy_Env (Current_Perm_Env, Saved_Env); 1937 Check_List (Private_Declarations (CorSp)); 1938 1939 -- Set mode to Read, and then analyze declarations and statements 1940 1941 Current_Checking_Mode := Read; 1942 Check_List (Declarations (Pack)); 1943 Check_Node (Handled_Statement_Sequence (Pack)); 1944 1945 -- Check RW for every stateful variable (i.e. in declarations) 1946 1947 Return_Declarations (Private_Declarations (CorSp)); 1948 Return_Declarations (Visible_Declarations (CorSp)); 1949 Return_Declarations (Declarations (Pack)); 1950 1951 -- Restore previous environment (i.e. delete every nonvisible 1952 -- declaration) from environment. 1953 1954 Free_Env (Current_Perm_Env); 1955 Copy_Env (Saved_Env, Current_Perm_Env); 1956 end Check_Package_Body; 1957 1958 -------------------- 1959 -- Check_Param_In -- 1960 -------------------- 1961 1962 procedure Check_Param_In (Formal : Entity_Id; Actual : Node_Id) is 1963 Mode : constant Entity_Kind := Ekind (Formal); 1964 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 1965 begin 1966 case Formal_Kind'(Mode) is 1967 1968 -- Formal IN parameter 1969 1970 when E_In_Parameter => 1971 1972 -- Formal IN parameter, access type 1973 1974 if Is_Access_Type (Etype (Formal)) then 1975 1976 -- Formal IN parameter, access to variable type 1977 1978 if not Is_Access_Constant (Etype (Formal)) then 1979 1980 -- Formal IN parameter, named/anonymous access-to-variable 1981 -- type. 1982 -- 1983 -- In SPARK, IN access-to-variable is an observe operation 1984 -- for a function, and a borrow operation for a procedure. 1985 1986 if Ekind (Scope (Formal)) = E_Function then 1987 Current_Checking_Mode := Observe; 1988 Check_Node (Actual); 1989 else 1990 Current_Checking_Mode := Borrow; 1991 Check_Node (Actual); 1992 end if; 1993 1994 -- Formal IN parameter, access-to-constant type 1995 -- Formal IN parameter, access-to-named-constant type 1996 1997 elsif not Is_Anonymous_Access_Type (Etype (Formal)) then 1998 Error_Msg_N ("assignment not allowed, Ownership Aspect" 1999 & " False (Named general access type)", 2000 Formal); 2001 2002 -- Formal IN parameter, access to anonymous constant type 2003 2004 else 2005 Current_Checking_Mode := Observe; 2006 Check_Node (Actual); 2007 end if; 2008 2009 -- Formal IN parameter, composite type 2010 2011 elsif Is_Deep (Etype (Formal)) then 2012 2013 -- Composite formal types should be named 2014 -- Formal IN parameter, composite named type 2015 2016 Current_Checking_Mode := Observe; 2017 Check_Node (Actual); 2018 end if; 2019 2020 when E_Out_Parameter 2021 | E_In_Out_Parameter 2022 => 2023 null; 2024 end case; 2025 2026 Current_Checking_Mode := Mode_Before; 2027 end Check_Param_In; 2028 2029 ---------------------- 2030 -- Check_Param_Out -- 2031 ---------------------- 2032 2033 procedure Check_Param_Out (Formal : Entity_Id; Actual : Node_Id) is 2034 Mode : constant Entity_Kind := Ekind (Formal); 2035 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 2036 2037 begin 2038 case Formal_Kind'(Mode) is 2039 2040 -- Formal OUT/IN OUT parameter 2041 2042 when E_Out_Parameter 2043 | E_In_Out_Parameter 2044 => 2045 2046 -- Formal OUT/IN OUT parameter, access type 2047 2048 if Is_Access_Type (Etype (Formal)) then 2049 2050 -- Formal OUT/IN OUT parameter, access to variable type 2051 2052 if not Is_Access_Constant (Etype (Formal)) then 2053 2054 -- Cannot have anonymous out access parameter 2055 -- Formal out/in out parameter, access to named variable 2056 -- type. 2057 2058 Current_Checking_Mode := Move; 2059 Check_Node (Actual); 2060 2061 -- Formal out/in out parameter, access to constant type 2062 2063 else 2064 Error_Msg_N ("assignment not allowed, Ownership Aspect False" 2065 & " (Named general access type)", Formal); 2066 2067 end if; 2068 2069 -- Formal out/in out parameter, composite type 2070 2071 elsif Is_Deep (Etype (Formal)) then 2072 2073 -- Composite formal types should be named 2074 -- Formal out/in out Parameter, Composite Named type. 2075 2076 Current_Checking_Mode := Borrow; 2077 Check_Node (Actual); 2078 end if; 2079 2080 when E_In_Parameter => 2081 null; 2082 end case; 2083 2084 Current_Checking_Mode := Mode_Before; 2085 end Check_Param_Out; 2086 2087 ------------------------- 2088 -- Check_Safe_Pointers -- 2089 ------------------------- 2090 2091 procedure Check_Safe_Pointers (N : Node_Id) is 2092 2093 -- Local subprograms 2094 2095 procedure Check_List (L : List_Id); 2096 -- Call the main analysis procedure on each element of the list 2097 2098 procedure Initialize; 2099 -- Initialize global variables before starting the analysis of a body 2100 2101 ---------------- 2102 -- Check_List -- 2103 ---------------- 2104 2105 procedure Check_List (L : List_Id) is 2106 N : Node_Id; 2107 begin 2108 N := First (L); 2109 while Present (N) loop 2110 Check_Safe_Pointers (N); 2111 Next (N); 2112 end loop; 2113 end Check_List; 2114 2115 ---------------- 2116 -- Initialize -- 2117 ---------------- 2118 2119 procedure Initialize is 2120 begin 2121 Reset (Current_Loops_Envs); 2122 Reset (Current_Loops_Accumulators); 2123 Reset (Current_Perm_Env); 2124 Reset (Current_Initialization_Map); 2125 end Initialize; 2126 2127 -- Local variables 2128 2129 Prag : Node_Id; 2130 2131 -- SPARK_Mode pragma in application 2132 2133 -- Start of processing for Check_Safe_Pointers 2134 2135 begin 2136 Initialize; 2137 case Nkind (N) is 2138 when N_Compilation_Unit => 2139 Check_Safe_Pointers (Unit (N)); 2140 2141 when N_Package_Body 2142 | N_Package_Declaration 2143 | N_Subprogram_Body 2144 => 2145 Prag := SPARK_Pragma (Defining_Entity (N)); 2146 if Present (Prag) then 2147 if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then 2148 return; 2149 else 2150 Check_Node (N); 2151 end if; 2152 2153 elsif Nkind (N) = N_Package_Body then 2154 Check_List (Declarations (N)); 2155 2156 elsif Nkind (N) = N_Package_Declaration then 2157 Check_List (Private_Declarations (Specification (N))); 2158 Check_List (Visible_Declarations (Specification (N))); 2159 end if; 2160 2161 when others => 2162 null; 2163 end case; 2164 end Check_Safe_Pointers; 2165 2166 --------------------- 2167 -- Check_Statement -- 2168 --------------------- 2169 2170 procedure Check_Statement (Stmt : Node_Id) is 2171 Mode_Before : constant Checking_Mode := Current_Checking_Mode; 2172 State_N : Perm_Kind; 2173 Check : Boolean := True; 2174 St_Name : Node_Id; 2175 Ty_St_Name : Node_Id; 2176 2177 function Get_Root (Comp_Stmt : Node_Id) return Node_Id; 2178 -- Return the root of the name given as input 2179 2180 function Get_Root (Comp_Stmt : Node_Id) return Node_Id is 2181 begin 2182 case Nkind (Comp_Stmt) is 2183 when N_Identifier 2184 | N_Expanded_Name 2185 => return Comp_Stmt; 2186 2187 when N_Type_Conversion 2188 | N_Unchecked_Type_Conversion 2189 | N_Qualified_Expression 2190 => 2191 return Get_Root (Expression (Comp_Stmt)); 2192 2193 when N_Parameter_Specification => 2194 return Get_Root (Defining_Identifier (Comp_Stmt)); 2195 2196 when N_Selected_Component 2197 | N_Indexed_Component 2198 | N_Slice 2199 | N_Explicit_Dereference 2200 => 2201 return Get_Root (Prefix (Comp_Stmt)); 2202 2203 when others => 2204 raise Program_Error; 2205 end case; 2206 end Get_Root; 2207 2208 begin 2209 case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is 2210 when N_Entry_Call_Statement => 2211 Check_Call_Statement (Stmt); 2212 2213 -- Move right-hand side first, and then assign left-hand side 2214 2215 when N_Assignment_Statement => 2216 2217 St_Name := Name (Stmt); 2218 Ty_St_Name := Etype (Name (Stmt)); 2219 2220 -- Check that is not a *general* access type 2221 2222 if Has_Ownership_Aspect_True (St_Name, "assigning to") then 2223 2224 -- Assigning to access type 2225 2226 if Is_Access_Type (Ty_St_Name) then 2227 2228 -- Assigning to access to variable type 2229 2230 if not Is_Access_Constant (Ty_St_Name) then 2231 2232 -- Assigning to named access to variable type 2233 2234 if not Is_Anonymous_Access_Type (Ty_St_Name) then 2235 Current_Checking_Mode := Move; 2236 2237 -- Assigning to anonymous access to variable type 2238 2239 else 2240 -- Target /= source root 2241 2242 if Nkind_In (Expression (Stmt), N_Allocator, N_Null) 2243 or else Entity (St_Name) /= 2244 Entity (Get_Root (Expression (Stmt))) 2245 then 2246 Error_Msg_N ("assignment not allowed, anonymous " 2247 & "access Object with Different Root", 2248 Stmt); 2249 Check := False; 2250 2251 -- Target = source root 2252 2253 else 2254 -- Here we do nothing on the source nor on the 2255 -- target. However, we check the the legality rule: 2256 -- "The source shall be an owning access object 2257 -- denoted by a name that is not in the observed 2258 -- state". 2259 2260 State_N := Get_Perm (Expression (Stmt)); 2261 if State_N = Observed then 2262 Error_Msg_N ("assignment not allowed, Anonymous " 2263 & "access object with the same root" 2264 & " but source Observed", Stmt); 2265 Check := False; 2266 end if; 2267 end if; 2268 end if; 2269 2270 -- else access-to-constant 2271 2272 -- Assigning to anonymous access-to-constant type 2273 2274 elsif Is_Anonymous_Access_Type (Ty_St_Name) then 2275 2276 -- ??? Check the follwing condition. We may have to 2277 -- add that the root is in the observed state too. 2278 2279 State_N := Get_Perm (Expression (Stmt)); 2280 if State_N /= Observed then 2281 Error_Msg_N ("assignment not allowed, anonymous " 2282 & "access-to-constant object not in " 2283 & "the observed state)", Stmt); 2284 Check := False; 2285 2286 else 2287 Error_Msg_N ("?here check accessibility level cited in" 2288 & " the second legality rule of assign", 2289 Stmt); 2290 Check := False; 2291 end if; 2292 2293 -- Assigning to named access-to-constant type: 2294 -- This case should have been detected when checking 2295 -- Has_Onwership_Aspect_True (Name (Stmt), "msg"). 2296 2297 else 2298 raise Program_Error; 2299 end if; 2300 2301 -- Assigning to composite (deep) type. 2302 2303 elsif Is_Deep (Ty_St_Name) then 2304 if Ekind_In (Ty_St_Name, 2305 E_Record_Type, 2306 E_Record_Subtype) 2307 then 2308 declare 2309 Elmt : Entity_Id := 2310 First_Component_Or_Discriminant (Ty_St_Name); 2311 2312 begin 2313 while Present (Elmt) loop 2314 if Is_Anonymous_Access_Type (Etype (Elmt)) or 2315 Ekind (Elmt) = E_General_Access_Type 2316 then 2317 Error_Msg_N ("assignment not allowed, Ownership " 2318 & "Aspect False (Components have " 2319 & "Ownership Aspect False)", Stmt); 2320 Check := False; 2321 exit; 2322 end if; 2323 2324 Next_Component_Or_Discriminant (Elmt); 2325 end loop; 2326 end; 2327 2328 -- Record types are always named so this is a move 2329 2330 if Check then 2331 Current_Checking_Mode := Move; 2332 end if; 2333 2334 elsif Ekind_In (Ty_St_Name, 2335 E_Array_Type, 2336 E_Array_Subtype) 2337 and then Check 2338 then 2339 Current_Checking_Mode := Move; 2340 end if; 2341 2342 -- Now handle legality rules of using a borrowed, observed, 2343 -- or moved name as a prefix in an assignment. 2344 2345 else 2346 if Nkind_In (St_Name, 2347 N_Attribute_Reference, 2348 N_Expanded_Name, 2349 N_Explicit_Dereference, 2350 N_Indexed_Component, 2351 N_Reference, 2352 N_Selected_Component, 2353 N_Slice) 2354 then 2355 2356 if Is_Access_Type (Etype (Prefix (St_Name))) or 2357 Is_Deep (Etype (Prefix (St_Name))) 2358 then 2359 2360 -- We set the Check variable to True so that we can 2361 -- Check_Node of the expression and the name first 2362 -- under the assumption of Current_Checking_Mode = 2363 -- Read => nothing to be done for the RHS if the 2364 -- following check on the expression fails, and 2365 -- Current_Checking_Mode := Assign => the name should 2366 -- not be borrowed or observed so that we can use it 2367 -- as a prefix in the target of an assignement. 2368 -- 2369 -- Note that we do not need to check the OA here 2370 -- because we are allowed to read and write "through" 2371 -- an object of OAF (example: traversing a DS). 2372 2373 Check := True; 2374 end if; 2375 end if; 2376 2377 if Nkind_In (Expression (Stmt), 2378 N_Attribute_Reference, 2379 N_Expanded_Name, 2380 N_Explicit_Dereference, 2381 N_Indexed_Component, 2382 N_Reference, 2383 N_Selected_Component, 2384 N_Slice) 2385 then 2386 2387 if Is_Access_Type (Etype (Prefix (Expression (Stmt)))) 2388 or else Is_Deep (Etype (Prefix (Expression (Stmt)))) 2389 then 2390 Current_Checking_Mode := Observe; 2391 Check := True; 2392 end if; 2393 end if; 2394 end if; 2395 2396 if Check then 2397 Check_Node (Expression (Stmt)); 2398 Current_Checking_Mode := Assign; 2399 Check_Node (St_Name); 2400 end if; 2401 end if; 2402 2403 when N_Block_Statement => 2404 declare 2405 Saved_Env : Perm_Env; 2406 begin 2407 -- Save environment 2408 2409 Copy_Env (Current_Perm_Env, Saved_Env); 2410 2411 -- Analyze declarations and Handled_Statement_Sequences 2412 2413 Current_Checking_Mode := Read; 2414 Check_List (Declarations (Stmt)); 2415 Check_Node (Handled_Statement_Sequence (Stmt)); 2416 2417 -- Restore environment 2418 2419 Free_Env (Current_Perm_Env); 2420 Copy_Env (Saved_Env, Current_Perm_Env); 2421 end; 2422 2423 when N_Case_Statement => 2424 declare 2425 Saved_Env : Perm_Env; 2426 2427 -- Accumulator for the different branches 2428 2429 New_Env : Perm_Env; 2430 Elmt : Node_Id := First (Alternatives (Stmt)); 2431 2432 begin 2433 Current_Checking_Mode := Read; 2434 Check_Node (Expression (Stmt)); 2435 Current_Checking_Mode := Mode_Before; 2436 2437 -- Save environment 2438 2439 Copy_Env (Current_Perm_Env, Saved_Env); 2440 2441 -- Here we have the original env in saved, current with a fresh 2442 -- copy, and new aliased. 2443 2444 -- First alternative 2445 2446 Check_Node (Elmt); 2447 Next (Elmt); 2448 Copy_Env (Current_Perm_Env, New_Env); 2449 Free_Env (Current_Perm_Env); 2450 2451 -- Other alternatives 2452 2453 while Present (Elmt) loop 2454 2455 -- Restore environment 2456 2457 Copy_Env (Saved_Env, Current_Perm_Env); 2458 Check_Node (Elmt); 2459 Next (Elmt); 2460 end loop; 2461 2462 Copy_Env (Saved_Env, Current_Perm_Env); 2463 Free_Env (New_Env); 2464 Free_Env (Saved_Env); 2465 end; 2466 2467 when N_Delay_Relative_Statement => 2468 Check_Node (Expression (Stmt)); 2469 2470 when N_Delay_Until_Statement => 2471 Check_Node (Expression (Stmt)); 2472 2473 when N_Loop_Statement => 2474 Check_Loop_Statement (Stmt); 2475 2476 -- If deep type expression, then move, else read 2477 2478 when N_Simple_Return_Statement => 2479 case Nkind (Expression (Stmt)) is 2480 when N_Empty => 2481 declare 2482 -- ??? This does not take into account the fact that 2483 -- a simple return inside an extended return statement 2484 -- applies to the extended return statement. 2485 Subp : constant Entity_Id := 2486 Return_Applies_To (Return_Statement_Entity (Stmt)); 2487 begin 2488 Return_Globals (Subp); 2489 end; 2490 2491 when others => 2492 if Is_Deep (Etype (Expression (Stmt))) then 2493 Current_Checking_Mode := Move; 2494 else 2495 Check := False; 2496 end if; 2497 2498 if Check then 2499 Check_Node (Expression (Stmt)); 2500 end if; 2501 end case; 2502 2503 when N_Extended_Return_Statement => 2504 Check_List (Return_Object_Declarations (Stmt)); 2505 Check_Node (Handled_Statement_Sequence (Stmt)); 2506 Return_Declarations (Return_Object_Declarations (Stmt)); 2507 declare 2508 -- ??? This does not take into account the fact that a simple 2509 -- return inside an extended return statement applies to the 2510 -- extended return statement. 2511 Subp : constant Entity_Id := 2512 Return_Applies_To (Return_Statement_Entity (Stmt)); 2513 2514 begin 2515 Return_Globals (Subp); 2516 end; 2517 2518 -- Nothing to do when exiting a loop. No merge needed 2519 2520 when N_Exit_Statement => 2521 null; 2522 2523 -- Copy environment, run on each branch 2524 2525 when N_If_Statement => 2526 declare 2527 Saved_Env : Perm_Env; 2528 2529 -- Accumulator for the different branches 2530 2531 New_Env : Perm_Env; 2532 2533 begin 2534 Check_Node (Condition (Stmt)); 2535 2536 -- Save environment 2537 2538 Copy_Env (Current_Perm_Env, Saved_Env); 2539 2540 -- Here we have the original env in saved, current with a fresh 2541 -- copy. 2542 2543 -- THEN PART 2544 2545 Check_List (Then_Statements (Stmt)); 2546 Copy_Env (Current_Perm_Env, New_Env); 2547 Free_Env (Current_Perm_Env); 2548 2549 -- Here the new_environment contains curr env after then block 2550 2551 -- ELSIF part 2552 2553 declare 2554 Elmt : Node_Id; 2555 2556 begin 2557 Elmt := First (Elsif_Parts (Stmt)); 2558 while Present (Elmt) loop 2559 2560 -- Transfer into accumulator, and restore from save 2561 2562 Copy_Env (Saved_Env, Current_Perm_Env); 2563 Check_Node (Condition (Elmt)); 2564 Check_List (Then_Statements (Stmt)); 2565 Next (Elmt); 2566 end loop; 2567 end; 2568 2569 -- ELSE part 2570 2571 -- Restore environment before if 2572 2573 Copy_Env (Saved_Env, Current_Perm_Env); 2574 2575 -- Here new environment contains the environment after then and 2576 -- current the fresh copy of old one. 2577 2578 Check_List (Else_Statements (Stmt)); 2579 2580 -- CLEANUP 2581 2582 Copy_Env (Saved_Env, Current_Perm_Env); 2583 2584 Free_Env (New_Env); 2585 Free_Env (Saved_Env); 2586 end; 2587 2588 -- Unsupported constructs in SPARK 2589 2590 when N_Abort_Statement 2591 | N_Accept_Statement 2592 | N_Asynchronous_Select 2593 | N_Code_Statement 2594 | N_Conditional_Entry_Call 2595 | N_Goto_Statement 2596 | N_Requeue_Statement 2597 | N_Selective_Accept 2598 | N_Timed_Entry_Call 2599 => 2600 Error_Msg_N ("unsupported construct in SPARK", Stmt); 2601 2602 -- Ignored constructs for pointer checking 2603 2604 when N_Null_Statement 2605 | N_Raise_Statement 2606 => 2607 null; 2608 2609 -- The following nodes are never generated in GNATprove mode 2610 2611 when N_Compound_Statement 2612 | N_Free_Statement 2613 => 2614 raise Program_Error; 2615 end case; 2616 end Check_Statement; 2617 2618 -------------- 2619 -- Get_Perm -- 2620 -------------- 2621 2622 function Get_Perm (N : Node_Id) return Perm_Kind is 2623 Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N); 2624 2625 begin 2626 case Tree_Or_Perm.R is 2627 when Folded => 2628 return Tree_Or_Perm.Found_Permission; 2629 2630 when Unfolded => 2631 pragma Assert (Tree_Or_Perm.Tree_Access /= null); 2632 return Permission (Tree_Or_Perm.Tree_Access); 2633 2634 -- We encoutered a function call, hence the memory area is fresh, 2635 -- which means that the association permission is RW. 2636 2637 when Function_Call => 2638 return Unrestricted; 2639 end case; 2640 end Get_Perm; 2641 2642 ---------------------- 2643 -- Get_Perm_Or_Tree -- 2644 ---------------------- 2645 2646 function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is 2647 begin 2648 case Nkind (N) is 2649 2650 -- Base identifier. Normally those are the roots of the trees stored 2651 -- in the permission environment. 2652 2653 when N_Defining_Identifier => 2654 raise Program_Error; 2655 2656 when N_Identifier 2657 | N_Expanded_Name 2658 => 2659 declare 2660 P : constant Entity_Id := Entity (N); 2661 C : constant Perm_Tree_Access := 2662 Get (Current_Perm_Env, Unique_Entity (P)); 2663 2664 begin 2665 -- Setting the initialization map to True, so that this 2666 -- variable cannot be ignored anymore when looking at end 2667 -- of elaboration of package. 2668 2669 Set (Current_Initialization_Map, Unique_Entity (P), True); 2670 if C = null then 2671 -- No null possible here, there are no parents for the path. 2672 -- This means we are using a global variable without adding 2673 -- it in environment with a global aspect. 2674 2675 Illegal_Global_Usage (N); 2676 2677 else 2678 return (R => Unfolded, Tree_Access => C); 2679 end if; 2680 end; 2681 2682 when N_Type_Conversion 2683 | N_Unchecked_Type_Conversion 2684 | N_Qualified_Expression 2685 => 2686 return Get_Perm_Or_Tree (Expression (N)); 2687 2688 -- Happening when we try to get the permission of a variable that 2689 -- is a formal parameter. We get instead the defining identifier 2690 -- associated with the parameter (which is the one that has been 2691 -- stored for indexing). 2692 2693 when N_Parameter_Specification => 2694 return Get_Perm_Or_Tree (Defining_Identifier (N)); 2695 2696 -- We get the permission tree of its prefix, and then get either the 2697 -- subtree associated with that specific selection, or if we have a 2698 -- leaf that folds its children, we take the children's permission 2699 -- and return it using the discriminant Folded. 2700 2701 when N_Selected_Component => 2702 declare 2703 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); 2704 2705 begin 2706 case C.R is 2707 when Folded 2708 | Function_Call 2709 => 2710 return C; 2711 2712 when Unfolded => 2713 pragma Assert (C.Tree_Access /= null); 2714 pragma Assert (Kind (C.Tree_Access) = Entire_Object 2715 or else 2716 Kind (C.Tree_Access) = Record_Component); 2717 2718 if Kind (C.Tree_Access) = Record_Component then 2719 declare 2720 Selected_Component : constant Entity_Id := 2721 Entity (Selector_Name (N)); 2722 Selected_C : constant Perm_Tree_Access := 2723 Perm_Tree_Maps.Get 2724 (Component (C.Tree_Access), Selected_Component); 2725 2726 begin 2727 if Selected_C = null then 2728 return (R => Unfolded, 2729 Tree_Access => 2730 Other_Components (C.Tree_Access)); 2731 2732 else 2733 return (R => Unfolded, 2734 Tree_Access => Selected_C); 2735 end if; 2736 end; 2737 2738 elsif Kind (C.Tree_Access) = Entire_Object then 2739 return (R => Folded, 2740 Found_Permission => 2741 Children_Permission (C.Tree_Access)); 2742 2743 else 2744 raise Program_Error; 2745 end if; 2746 end case; 2747 end; 2748 -- We get the permission tree of its prefix, and then get either the 2749 -- subtree associated with that specific selection, or if we have a 2750 -- leaf that folds its children, we take the children's permission 2751 -- and return it using the discriminant Folded. 2752 2753 when N_Indexed_Component 2754 | N_Slice 2755 => 2756 declare 2757 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); 2758 2759 begin 2760 case C.R is 2761 when Folded 2762 | Function_Call 2763 => 2764 return C; 2765 2766 when Unfolded => 2767 pragma Assert (C.Tree_Access /= null); 2768 pragma Assert (Kind (C.Tree_Access) = Entire_Object 2769 or else 2770 Kind (C.Tree_Access) = Array_Component); 2771 2772 if Kind (C.Tree_Access) = Array_Component then 2773 pragma Assert (Get_Elem (C.Tree_Access) /= null); 2774 return (R => Unfolded, 2775 Tree_Access => Get_Elem (C.Tree_Access)); 2776 2777 elsif Kind (C.Tree_Access) = Entire_Object then 2778 return (R => Folded, Found_Permission => 2779 Children_Permission (C.Tree_Access)); 2780 2781 else 2782 raise Program_Error; 2783 end if; 2784 end case; 2785 end; 2786 -- We get the permission tree of its prefix, and then get either the 2787 -- subtree associated with that specific selection, or if we have a 2788 -- leaf that folds its children, we take the children's permission 2789 -- and return it using the discriminant Folded. 2790 2791 when N_Explicit_Dereference => 2792 declare 2793 C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); 2794 2795 begin 2796 case C.R is 2797 when Folded 2798 | Function_Call 2799 => 2800 return C; 2801 2802 when Unfolded => 2803 pragma Assert (C.Tree_Access /= null); 2804 pragma Assert (Kind (C.Tree_Access) = Entire_Object 2805 or else 2806 Kind (C.Tree_Access) = Reference); 2807 2808 if Kind (C.Tree_Access) = Reference then 2809 if Get_All (C.Tree_Access) = null then 2810 2811 -- Hash_Table_Error 2812 2813 raise Program_Error; 2814 2815 else 2816 return 2817 (R => Unfolded, 2818 Tree_Access => Get_All (C.Tree_Access)); 2819 end if; 2820 2821 elsif Kind (C.Tree_Access) = Entire_Object then 2822 return (R => Folded, Found_Permission => 2823 Children_Permission (C.Tree_Access)); 2824 2825 else 2826 raise Program_Error; 2827 end if; 2828 end case; 2829 end; 2830 -- The name contains a function call, hence the given path is always 2831 -- new. We do not have to check for anything. 2832 2833 when N_Function_Call => 2834 return (R => Function_Call); 2835 2836 when others => 2837 raise Program_Error; 2838 end case; 2839 end Get_Perm_Or_Tree; 2840 2841 ------------------- 2842 -- Get_Perm_Tree -- 2843 ------------------- 2844 2845 function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access is 2846 begin 2847 case Nkind (N) is 2848 2849 -- Base identifier. Normally those are the roots of the trees stored 2850 -- in the permission environment. 2851 2852 when N_Defining_Identifier => 2853 raise Program_Error; 2854 2855 when N_Identifier 2856 | N_Expanded_Name 2857 => 2858 declare 2859 P : constant Node_Id := Entity (N); 2860 C : constant Perm_Tree_Access := 2861 Get (Current_Perm_Env, Unique_Entity (P)); 2862 2863 begin 2864 -- Setting the initialization map to True, so that this 2865 -- variable cannot be ignored anymore when looking at end 2866 -- of elaboration of package. 2867 2868 Set (Current_Initialization_Map, Unique_Entity (P), True); 2869 if C = null then 2870 -- No null possible here, there are no parents for the path. 2871 -- This means we are using a global variable without adding 2872 -- it in environment with a global aspect. 2873 2874 Illegal_Global_Usage (N); 2875 2876 else 2877 return C; 2878 end if; 2879 end; 2880 2881 when N_Type_Conversion 2882 | N_Unchecked_Type_Conversion 2883 | N_Qualified_Expression 2884 => 2885 return Get_Perm_Tree (Expression (N)); 2886 2887 when N_Parameter_Specification => 2888 return Get_Perm_Tree (Defining_Identifier (N)); 2889 2890 -- We get the permission tree of its prefix, and then get either the 2891 -- subtree associated with that specific selection, or if we have a 2892 -- leaf that folds its children, we unroll it in one step. 2893 2894 when N_Selected_Component => 2895 declare 2896 C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N)); 2897 2898 begin 2899 if C = null then 2900 2901 -- If null then it means we went through a function call 2902 2903 return null; 2904 end if; 2905 2906 pragma Assert (Kind (C) = Entire_Object 2907 or else Kind (C) = Record_Component); 2908 2909 if Kind (C) = Record_Component then 2910 2911 -- The tree is unfolded. We just return the subtree. 2912 2913 declare 2914 Selected_Component : constant Entity_Id := 2915 Entity (Selector_Name (N)); 2916 Selected_C : constant Perm_Tree_Access := 2917 Perm_Tree_Maps.Get 2918 (Component (C), Selected_Component); 2919 2920 begin 2921 if Selected_C = null then 2922 return Other_Components (C); 2923 end if; 2924 return Selected_C; 2925 end; 2926 2927 elsif Kind (C) = Entire_Object then 2928 declare 2929 -- Expand the tree. Replace the node with 2930 -- Record_Component. 2931 2932 Elem : Node_Id; 2933 2934 -- Create the unrolled nodes 2935 2936 Son : Perm_Tree_Access; 2937 2938 Child_Perm : constant Perm_Kind := 2939 Children_Permission (C); 2940 2941 begin 2942 -- We change the current node from Entire_Object to 2943 -- Record_Component with same permission and an empty 2944 -- hash table as component list. 2945 2946 C.all.Tree := 2947 (Kind => Record_Component, 2948 Is_Node_Deep => Is_Node_Deep (C), 2949 Permission => Permission (C), 2950 Component => Perm_Tree_Maps.Nil, 2951 Other_Components => 2952 new Perm_Tree_Wrapper' 2953 (Tree => 2954 (Kind => Entire_Object, 2955 -- Is_Node_Deep is true, to be conservative 2956 Is_Node_Deep => True, 2957 Permission => Child_Perm, 2958 Children_Permission => Child_Perm) 2959 ) 2960 ); 2961 2962 -- We fill the hash table with all sons of the record, 2963 -- with basic Entire_Objects nodes. 2964 2965 Elem := First_Component_Or_Discriminant 2966 (Etype (Prefix (N))); 2967 2968 while Present (Elem) loop 2969 Son := new Perm_Tree_Wrapper' 2970 (Tree => 2971 (Kind => Entire_Object, 2972 Is_Node_Deep => Is_Deep (Etype (Elem)), 2973 Permission => Child_Perm, 2974 Children_Permission => Child_Perm)); 2975 2976 Perm_Tree_Maps.Set 2977 (C.all.Tree.Component, Elem, Son); 2978 Next_Component_Or_Discriminant (Elem); 2979 end loop; 2980 -- we return the tree to the sons, so that the recursion 2981 -- can continue. 2982 2983 declare 2984 Selected_Component : constant Entity_Id := 2985 Entity (Selector_Name (N)); 2986 2987 Selected_C : constant Perm_Tree_Access := 2988 Perm_Tree_Maps.Get 2989 (Component (C), Selected_Component); 2990 2991 begin 2992 pragma Assert (Selected_C /= null); 2993 return Selected_C; 2994 end; 2995 end; 2996 else 2997 raise Program_Error; 2998 end if; 2999 end; 3000 -- We set the permission tree of its prefix, and then we extract from 3001 -- the returned pointer the subtree. If folded, we unroll the tree at 3002 -- one step. 3003 3004 when N_Indexed_Component 3005 | N_Slice 3006 => 3007 declare 3008 C : constant Perm_Tree_Access := Get_Perm_Tree (Prefix (N)); 3009 3010 begin 3011 if C = null then 3012 -- If null then we went through a function call 3013 3014 return null; 3015 end if; 3016 pragma Assert (Kind (C) = Entire_Object 3017 or else Kind (C) = Array_Component); 3018 3019 if Kind (C) = Array_Component then 3020 3021 -- The tree is unfolded. We just return the elem subtree 3022 3023 pragma Assert (Get_Elem (C) = null); 3024 return Get_Elem (C); 3025 3026 elsif Kind (C) = Entire_Object then 3027 declare 3028 -- Expand the tree. Replace node with Array_Component. 3029 3030 Son : Perm_Tree_Access; 3031 3032 begin 3033 Son := new Perm_Tree_Wrapper' 3034 (Tree => 3035 (Kind => Entire_Object, 3036 Is_Node_Deep => Is_Node_Deep (C), 3037 Permission => Children_Permission (C), 3038 Children_Permission => Children_Permission (C))); 3039 3040 -- We change the current node from Entire_Object 3041 -- to Array_Component with same permission and the 3042 -- previously defined son. 3043 3044 C.all.Tree := (Kind => Array_Component, 3045 Is_Node_Deep => Is_Node_Deep (C), 3046 Permission => Permission (C), 3047 Get_Elem => Son); 3048 return Get_Elem (C); 3049 end; 3050 else 3051 raise Program_Error; 3052 end if; 3053 end; 3054 -- We get the permission tree of its prefix, and then get either the 3055 -- subtree associated with that specific selection, or if we have a 3056 -- leaf that folds its children, we unroll the tree. 3057 3058 when N_Explicit_Dereference => 3059 declare 3060 C : Perm_Tree_Access; 3061 3062 begin 3063 C := Get_Perm_Tree (Prefix (N)); 3064 3065 if C = null then 3066 3067 -- If null, we went through a function call 3068 3069 return null; 3070 end if; 3071 3072 pragma Assert (Kind (C) = Entire_Object 3073 or else Kind (C) = Reference); 3074 3075 if Kind (C) = Reference then 3076 3077 -- The tree is unfolded. We return the elem subtree 3078 3079 if Get_All (C) = null then 3080 3081 -- Hash_Table_Error 3082 3083 raise Program_Error; 3084 end if; 3085 return Get_All (C); 3086 3087 elsif Kind (C) = Entire_Object then 3088 declare 3089 -- Expand the tree. Replace the node with Reference. 3090 3091 Son : Perm_Tree_Access; 3092 3093 begin 3094 Son := new Perm_Tree_Wrapper' 3095 (Tree => 3096 (Kind => Entire_Object, 3097 Is_Node_Deep => Is_Deep (Etype (N)), 3098 Permission => Children_Permission (C), 3099 Children_Permission => Children_Permission (C))); 3100 3101 -- We change the current node from Entire_Object to 3102 -- Reference with same permission and the previous son. 3103 3104 pragma Assert (Is_Node_Deep (C)); 3105 C.all.Tree := (Kind => Reference, 3106 Is_Node_Deep => Is_Node_Deep (C), 3107 Permission => Permission (C), 3108 Get_All => Son); 3109 return Get_All (C); 3110 end; 3111 else 3112 raise Program_Error; 3113 end if; 3114 end; 3115 -- No permission tree for function calls 3116 3117 when N_Function_Call => 3118 return null; 3119 3120 when others => 3121 raise Program_Error; 3122 end case; 3123 end Get_Perm_Tree; 3124 3125 -------- 3126 -- Hp -- 3127 -------- 3128 3129 procedure Hp (P : Perm_Env) is 3130 Elem : Perm_Tree_Maps.Key_Option; 3131 3132 begin 3133 Elem := Get_First_Key (P); 3134 while Elem.Present loop 3135 Print_Node_Briefly (Elem.K); 3136 Elem := Get_Next_Key (P); 3137 end loop; 3138 end Hp; 3139 3140 -------------------------- 3141 -- Illegal_Global_Usage -- 3142 -------------------------- 3143 3144 procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is 3145 begin 3146 Error_Msg_NE ("cannot use global variable & of deep type", N, N); 3147 Error_Msg_N ("\without prior declaration in a Global aspect", N); 3148 Errout.Finalize (Last_Call => True); 3149 Errout.Output_Messages; 3150 Exit_Program (E_Errors); 3151 end Illegal_Global_Usage; 3152 3153 ------------- 3154 -- Is_Deep -- 3155 ------------- 3156 3157 function Is_Deep (E : Entity_Id) return Boolean is 3158 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean; 3159 function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is 3160 Decl : Node_Id; 3161 Pack_Decl : Node_Id; 3162 3163 begin 3164 if Is_Itype (E) then 3165 Decl := Associated_Node_For_Itype (E); 3166 else 3167 Decl := Parent (E); 3168 end if; 3169 3170 Pack_Decl := Parent (Parent (Decl)); 3171 3172 if Nkind (Pack_Decl) /= N_Package_Declaration then 3173 return False; 3174 end if; 3175 3176 return 3177 Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) 3178 and then Get_SPARK_Mode_From_Annotation 3179 (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off; 3180 end Is_Private_Entity_Mode_Off; 3181 3182 begin 3183 pragma Assert (Is_Type (E)); 3184 case Ekind (E) is 3185 when Scalar_Kind => 3186 return False; 3187 3188 when Access_Kind => 3189 return True; 3190 3191 -- Just check the depth of its component type 3192 3193 when E_Array_Type 3194 | E_Array_Subtype 3195 => 3196 return Is_Deep (Component_Type (E)); 3197 3198 when E_String_Literal_Subtype => 3199 return False; 3200 3201 -- Per RM 8.11 for class-wide types 3202 3203 when E_Class_Wide_Subtype 3204 | E_Class_Wide_Type 3205 => 3206 return True; 3207 3208 -- ??? What about hidden components 3209 3210 when E_Record_Type 3211 | E_Record_Subtype 3212 => 3213 declare 3214 Elmt : Entity_Id; 3215 3216 begin 3217 Elmt := First_Component_Or_Discriminant (E); 3218 while Present (Elmt) loop 3219 if Is_Deep (Etype (Elmt)) then 3220 return True; 3221 else 3222 Next_Component_Or_Discriminant (Elmt); 3223 end if; 3224 end loop; 3225 return False; 3226 end; 3227 3228 when Private_Kind => 3229 if Is_Private_Entity_Mode_Off (E) then 3230 return False; 3231 else 3232 if Present (Full_View (E)) then 3233 return Is_Deep (Full_View (E)); 3234 else 3235 return True; 3236 end if; 3237 end if; 3238 3239 when E_Incomplete_Type 3240 | E_Incomplete_Subtype 3241 => 3242 return True; 3243 3244 -- No problem with synchronized types 3245 3246 when E_Protected_Type 3247 | E_Protected_Subtype 3248 | E_Task_Subtype 3249 | E_Task_Type 3250 => 3251 return False; 3252 3253 when E_Exception_Type => 3254 return False; 3255 3256 when others => 3257 raise Program_Error; 3258 end case; 3259 end Is_Deep; 3260 3261 ---------------- 3262 -- Perm_Error -- 3263 ---------------- 3264 3265 procedure Perm_Error 3266 (N : Node_Id; 3267 Perm : Perm_Kind; 3268 Found_Perm : Perm_Kind) 3269 is 3270 procedure Set_Root_Object 3271 (Path : Node_Id; 3272 Obj : out Entity_Id; 3273 Deref : out Boolean); 3274 -- Set the root object Obj, and whether the path contains a dereference, 3275 -- from a path Path. 3276 3277 --------------------- 3278 -- Set_Root_Object -- 3279 --------------------- 3280 3281 procedure Set_Root_Object 3282 (Path : Node_Id; 3283 Obj : out Entity_Id; 3284 Deref : out Boolean) 3285 is 3286 begin 3287 case Nkind (Path) is 3288 when N_Identifier 3289 | N_Expanded_Name 3290 => 3291 Obj := Entity (Path); 3292 Deref := False; 3293 3294 when N_Type_Conversion 3295 | N_Unchecked_Type_Conversion 3296 | N_Qualified_Expression 3297 => 3298 Set_Root_Object (Expression (Path), Obj, Deref); 3299 3300 when N_Indexed_Component 3301 | N_Selected_Component 3302 | N_Slice 3303 => 3304 Set_Root_Object (Prefix (Path), Obj, Deref); 3305 3306 when N_Explicit_Dereference => 3307 Set_Root_Object (Prefix (Path), Obj, Deref); 3308 Deref := True; 3309 3310 when others => 3311 raise Program_Error; 3312 end case; 3313 end Set_Root_Object; 3314 -- Local variables 3315 3316 Root : Entity_Id; 3317 Is_Deref : Boolean; 3318 3319 -- Start of processing for Perm_Error 3320 3321 begin 3322 Set_Root_Object (N, Root, Is_Deref); 3323 3324 if Is_Deref then 3325 Error_Msg_NE 3326 ("insufficient permission on dereference from &", N, Root); 3327 else 3328 Error_Msg_NE ("insufficient permission for &", N, Root); 3329 end if; 3330 3331 Perm_Mismatch (Perm, Found_Perm, N); 3332 end Perm_Error; 3333 3334 ------------------------------- 3335 -- Perm_Error_Subprogram_End -- 3336 ------------------------------- 3337 3338 procedure Perm_Error_Subprogram_End 3339 (E : Entity_Id; 3340 Subp : Entity_Id; 3341 Perm : Perm_Kind; 3342 Found_Perm : Perm_Kind) 3343 is 3344 begin 3345 Error_Msg_Node_2 := Subp; 3346 Error_Msg_NE ("insufficient permission for & when returning from &", 3347 Subp, E); 3348 Perm_Mismatch (Perm, Found_Perm, Subp); 3349 end Perm_Error_Subprogram_End; 3350 3351 ------------------ 3352 -- Process_Path -- 3353 ------------------ 3354 3355 procedure Process_Path (N : Node_Id) is 3356 Root : constant Entity_Id := Get_Enclosing_Object (N); 3357 State_N : Perm_Kind; 3358 begin 3359 -- We ignore if yielding to synchronized 3360 3361 if Present (Root) 3362 and then Is_Synchronized_Object (Root) 3363 then 3364 return; 3365 end if; 3366 3367 State_N := Get_Perm (N); 3368 3369 case Current_Checking_Mode is 3370 3371 -- Check permission R, do nothing 3372 3373 when Read => 3374 3375 -- This condition should be removed when removing the read 3376 -- checking mode. 3377 3378 return; 3379 3380 when Move => 3381 3382 -- The rhs object in an assignment statement (including copy in 3383 -- and copy back) should be in the Unrestricted or Moved state. 3384 -- Otherwise the move is not allowed. 3385 -- This applies to both stand-alone and composite objects. 3386 -- If the state of the source is Moved, then a warning message 3387 -- is prompt to make the user aware of reading a nullified 3388 -- object. 3389 3390 if State_N /= Unrestricted and State_N /= Moved then 3391 Perm_Error (N, Unrestricted, State_N); 3392 return; 3393 end if; 3394 3395 -- In the AI, after moving a path nothing to do since the rhs 3396 -- object was in the Unrestricted state and it shall be 3397 -- refreshed to Unrestricted. The object should be nullified 3398 -- however. To avoid moving again a name that has already been 3399 -- moved, in this implementation we set the state of the moved 3400 -- object to "Moved". This shall be used to prompt a warning 3401 -- when manipulating a null pointer and also to implement 3402 -- the no aliasing parameter restriction. 3403 3404 if State_N = Moved then 3405 Error_Msg_N ("?the source or one of its extensions has" 3406 & " already been moved", N); 3407 end if; 3408 3409 declare 3410 -- Set state to Moved to the path and any of its prefixes 3411 3412 Tree : constant Perm_Tree_Access := 3413 Set_Perm_Prefixes (N, Moved); 3414 3415 begin 3416 if Tree = null then 3417 3418 -- We went through a function call, no permission to 3419 -- modify. 3420 3421 return; 3422 end if; 3423 3424 -- Set state to Moved on any strict extension of the path 3425 3426 Set_Perm_Extensions (Tree, Moved); 3427 end; 3428 3429 when Assign => 3430 3431 -- The lhs object in an assignment statement (including copy in 3432 -- and copy back) should be in the Unrestricted state. 3433 -- Otherwise the move is not allowed. 3434 -- This applies to both stand-alone and composite objects. 3435 3436 if State_N /= Unrestricted and State_N /= Moved then 3437 Perm_Error (N, Unrestricted, State_N); 3438 return; 3439 end if; 3440 3441 -- After assigning to a path nothing to do since it was in the 3442 -- Unrestricted state and it would be refreshed to 3443 -- Unrestricted. 3444 3445 when Borrow => 3446 3447 -- Borrowing is only allowed on Unrestricted objects. 3448 3449 if State_N /= Unrestricted and State_N /= Moved then 3450 Perm_Error (N, Unrestricted, State_N); 3451 end if; 3452 3453 if State_N = Moved then 3454 Error_Msg_N ("?the source or one of its extensions has" 3455 & " already been moved", N); 3456 end if; 3457 3458 declare 3459 -- Set state to Borrowed to the path and any of its prefixes 3460 3461 Tree : constant Perm_Tree_Access := 3462 Set_Perm_Prefixes (N, Borrowed); 3463 3464 begin 3465 if Tree = null then 3466 3467 -- We went through a function call, no permission to 3468 -- modify. 3469 3470 return; 3471 end if; 3472 3473 -- Set state to Borrowed on any strict extension of the path 3474 3475 Set_Perm_Extensions (Tree, Borrowed); 3476 end; 3477 3478 when Observe => 3479 if State_N /= Unrestricted 3480 and then State_N /= Observed 3481 then 3482 Perm_Error (N, Observed, State_N); 3483 end if; 3484 3485 declare 3486 -- Set permission to Observed on the path and any of its 3487 -- prefixes if it is of a deep type. Actually, some operation 3488 -- like reading from an object of access type is considered as 3489 -- observe while it should not affect the permissions of 3490 -- the considered tree. 3491 3492 Tree : Perm_Tree_Access; 3493 3494 begin 3495 if Is_Deep (Etype (N)) then 3496 Tree := Set_Perm_Prefixes (N, Observed); 3497 else 3498 Tree := null; 3499 end if; 3500 3501 if Tree = null then 3502 3503 -- We went through a function call, no permission to 3504 -- modify. 3505 3506 return; 3507 end if; 3508 3509 -- Set permissions to No on any strict extension of the path 3510 3511 Set_Perm_Extensions (Tree, Observed); 3512 end; 3513 end case; 3514 end Process_Path; 3515 3516 ------------------------- 3517 -- Return_Declarations -- 3518 ------------------------- 3519 3520 procedure Return_Declarations (L : List_Id) is 3521 procedure Return_Declaration (Decl : Node_Id); 3522 -- Check correct permissions for every declared object 3523 3524 ------------------------ 3525 -- Return_Declaration -- 3526 ------------------------ 3527 3528 procedure Return_Declaration (Decl : Node_Id) is 3529 begin 3530 if Nkind (Decl) = N_Object_Declaration then 3531 3532 -- Check RW for object declared, unless the object has never been 3533 -- initialized. 3534 3535 if Get (Current_Initialization_Map, 3536 Unique_Entity (Defining_Identifier (Decl))) = False 3537 then 3538 return; 3539 end if; 3540 3541 declare 3542 Elem : constant Perm_Tree_Access := 3543 Get (Current_Perm_Env, 3544 Unique_Entity (Defining_Identifier (Decl))); 3545 3546 begin 3547 if Elem = null then 3548 3549 -- Here we are on a declaration. Hence it should have been 3550 -- added in the environment when analyzing this node with 3551 -- mode Read. Hence it is not possible to find a null 3552 -- pointer here. 3553 3554 -- Hash_Table_Error 3555 3556 raise Program_Error; 3557 end if; 3558 3559 if Permission (Elem) /= Unrestricted then 3560 Perm_Error (Decl, Unrestricted, Permission (Elem)); 3561 end if; 3562 end; 3563 end if; 3564 end Return_Declaration; 3565 -- Local Variables 3566 3567 N : Node_Id; 3568 3569 -- Start of processing for Return_Declarations 3570 3571 begin 3572 N := First (L); 3573 while Present (N) loop 3574 Return_Declaration (N); 3575 Next (N); 3576 end loop; 3577 end Return_Declarations; 3578 3579 -------------------- 3580 -- Return_Globals -- 3581 -------------------- 3582 3583 procedure Return_Globals (Subp : Entity_Id) is 3584 procedure Return_Globals_From_List 3585 (First_Item : Node_Id; 3586 Kind : Formal_Kind); 3587 -- Return global items from the list starting at Item 3588 3589 procedure Return_Globals_Of_Mode (Global_Mode : Name_Id); 3590 -- Return global items for the mode Global_Mode 3591 3592 ------------------------------ 3593 -- Return_Globals_From_List -- 3594 ------------------------------ 3595 3596 procedure Return_Globals_From_List 3597 (First_Item : Node_Id; 3598 Kind : Formal_Kind) 3599 is 3600 Item : Node_Id := First_Item; 3601 E : Entity_Id; 3602 3603 begin 3604 while Present (Item) loop 3605 E := Entity (Item); 3606 3607 -- Ignore abstract states, which play no role in pointer aliasing 3608 3609 if Ekind (E) = E_Abstract_State then 3610 null; 3611 else 3612 Return_The_Global (E, Kind, Subp); 3613 end if; 3614 Next_Global (Item); 3615 end loop; 3616 end Return_Globals_From_List; 3617 3618 ---------------------------- 3619 -- Return_Globals_Of_Mode -- 3620 ---------------------------- 3621 3622 procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is 3623 Kind : Formal_Kind; 3624 3625 begin 3626 case Global_Mode is 3627 when Name_Input 3628 | Name_Proof_In 3629 => 3630 Kind := E_In_Parameter; 3631 when Name_Output => 3632 Kind := E_Out_Parameter; 3633 when Name_In_Out => 3634 Kind := E_In_Out_Parameter; 3635 when others => 3636 raise Program_Error; 3637 end case; 3638 3639 -- Return both global items from Global and Refined_Global pragmas 3640 3641 Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind); 3642 Return_Globals_From_List 3643 (First_Global (Subp, Global_Mode, Refined => True), Kind); 3644 end Return_Globals_Of_Mode; 3645 3646 -- Start of processing for Return_Globals 3647 3648 begin 3649 Return_Globals_Of_Mode (Name_Proof_In); 3650 Return_Globals_Of_Mode (Name_Input); 3651 Return_Globals_Of_Mode (Name_Output); 3652 Return_Globals_Of_Mode (Name_In_Out); 3653 end Return_Globals; 3654 3655 -------------------------------- 3656 -- Return_Parameter_Or_Global -- 3657 -------------------------------- 3658 3659 procedure Return_The_Global 3660 (Id : Entity_Id; 3661 Mode : Formal_Kind; 3662 Subp : Entity_Id) 3663 is 3664 Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); 3665 pragma Assert (Elem /= null); 3666 3667 begin 3668 -- Observed IN parameters and globals need not return a permission to 3669 -- the caller. 3670 3671 if Mode = E_In_Parameter 3672 3673 -- Check this for read-only globals. 3674 3675 then 3676 if Permission (Elem) /= Unrestricted 3677 and then Permission (Elem) /= Observed 3678 then 3679 Perm_Error_Subprogram_End 3680 (E => Id, 3681 Subp => Subp, 3682 Perm => Observed, 3683 Found_Perm => Permission (Elem)); 3684 end if; 3685 3686 -- All globals of mode out or in/out should return with mode 3687 -- Unrestricted. 3688 3689 else 3690 if Permission (Elem) /= Unrestricted then 3691 Perm_Error_Subprogram_End 3692 (E => Id, 3693 Subp => Subp, 3694 Perm => Unrestricted, 3695 Found_Perm => Permission (Elem)); 3696 end if; 3697 end if; 3698 end Return_The_Global; 3699 3700 ------------------------- 3701 -- Set_Perm_Extensions -- 3702 ------------------------- 3703 3704 procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind) is 3705 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); 3706 procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is 3707 begin 3708 case Kind (T) is 3709 when Entire_Object => 3710 null; 3711 3712 when Reference => 3713 Free_Perm_Tree (T.all.Tree.Get_All); 3714 3715 when Array_Component => 3716 Free_Perm_Tree (T.all.Tree.Get_Elem); 3717 3718 -- Free every Component subtree 3719 3720 when Record_Component => 3721 declare 3722 Comp : Perm_Tree_Access; 3723 3724 begin 3725 Comp := Perm_Tree_Maps.Get_First (Component (T)); 3726 while Comp /= null loop 3727 Free_Perm_Tree (Comp); 3728 Comp := Perm_Tree_Maps.Get_Next (Component (T)); 3729 end loop; 3730 3731 Free_Perm_Tree (T.all.Tree.Other_Components); 3732 end; 3733 end case; 3734 end Free_Perm_Tree_Children; 3735 3736 Son : constant Perm_Tree := 3737 Perm_Tree' 3738 (Kind => Entire_Object, 3739 Is_Node_Deep => Is_Node_Deep (T), 3740 Permission => Permission (T), 3741 Children_Permission => P); 3742 3743 begin 3744 Free_Perm_Tree_Children (T); 3745 T.all.Tree := Son; 3746 end Set_Perm_Extensions; 3747 3748 ------------------------------ 3749 -- Set_Perm_Prefixes -- 3750 ------------------------------ 3751 3752 function Set_Perm_Prefixes 3753 (N : Node_Id; 3754 New_Perm : Perm_Kind) 3755 return Perm_Tree_Access 3756 is 3757 begin 3758 3759 case Nkind (N) is 3760 3761 when N_Identifier 3762 | N_Expanded_Name 3763 | N_Defining_Identifier 3764 => 3765 if Nkind (N) = N_Defining_Identifier 3766 and then New_Perm = Borrowed 3767 then 3768 raise Program_Error; 3769 end if; 3770 3771 declare 3772 P : Node_Id; 3773 C : Perm_Tree_Access; 3774 3775 begin 3776 if Nkind (N) = N_Defining_Identifier then 3777 P := N; 3778 else 3779 P := Entity (N); 3780 end if; 3781 3782 C := Get (Current_Perm_Env, Unique_Entity (P)); 3783 pragma Assert (C /= null); 3784 3785 -- Setting the initialization map to True, so that this 3786 -- variable cannot be ignored anymore when looking at end 3787 -- of elaboration of package. 3788 3789 Set (Current_Initialization_Map, Unique_Entity (P), True); 3790 if New_Perm = Observed 3791 and then C = null 3792 then 3793 3794 -- No null possible here, there are no parents for the path. 3795 -- This means we are using a global variable without adding 3796 -- it in environment with a global aspect. 3797 3798 Illegal_Global_Usage (N); 3799 end if; 3800 3801 C.all.Tree.Permission := New_Perm; 3802 return C; 3803 end; 3804 3805 when N_Type_Conversion 3806 | N_Unchecked_Type_Conversion 3807 | N_Qualified_Expression 3808 => 3809 return Set_Perm_Prefixes (Expression (N), New_Perm); 3810 3811 when N_Parameter_Specification => 3812 raise Program_Error; 3813 3814 -- We set the permission tree of its prefix, and then we extract 3815 -- our subtree from the returned pointer and assign an adequate 3816 -- permission to it, if unfolded. If folded, we unroll the tree 3817 -- in one step. 3818 3819 when N_Selected_Component => 3820 declare 3821 C : constant Perm_Tree_Access := 3822 Set_Perm_Prefixes (Prefix (N), New_Perm); 3823 3824 begin 3825 if C = null then 3826 3827 -- We went through a function call, do nothing 3828 3829 return null; 3830 end if; 3831 3832 pragma Assert (Kind (C) = Entire_Object 3833 or else Kind (C) = Record_Component); 3834 3835 if Kind (C) = Record_Component then 3836 -- The tree is unfolded. We just modify the permission and 3837 -- return the record subtree. 3838 3839 declare 3840 Selected_Component : constant Entity_Id := 3841 Entity (Selector_Name (N)); 3842 3843 Selected_C : Perm_Tree_Access := 3844 Perm_Tree_Maps.Get 3845 (Component (C), Selected_Component); 3846 3847 begin 3848 if Selected_C = null then 3849 Selected_C := Other_Components (C); 3850 end if; 3851 3852 pragma Assert (Selected_C /= null); 3853 Selected_C.all.Tree.Permission := New_Perm; 3854 return Selected_C; 3855 end; 3856 3857 elsif Kind (C) = Entire_Object then 3858 declare 3859 -- Expand the tree. Replace the node with 3860 -- Record_Component. 3861 3862 Elem : Node_Id; 3863 3864 -- Create an empty hash table 3865 3866 Hashtbl : Perm_Tree_Maps.Instance; 3867 3868 -- We create the unrolled nodes, that will all have same 3869 -- permission than parent. 3870 3871 Son : Perm_Tree_Access; 3872 Children_Perm : constant Perm_Kind := 3873 Children_Permission (C); 3874 3875 begin 3876 -- We change the current node from Entire_Object to 3877 -- Record_Component with same permission and an empty 3878 -- hash table as component list. 3879 3880 C.all.Tree := 3881 (Kind => Record_Component, 3882 Is_Node_Deep => Is_Node_Deep (C), 3883 Permission => Permission (C), 3884 Component => Hashtbl, 3885 Other_Components => 3886 new Perm_Tree_Wrapper' 3887 (Tree => 3888 (Kind => Entire_Object, 3889 Is_Node_Deep => True, 3890 Permission => Children_Perm, 3891 Children_Permission => Children_Perm) 3892 )); 3893 3894 -- We fill the hash table with all sons of the record, 3895 -- with basic Entire_Objects nodes. 3896 3897 Elem := First_Component_Or_Discriminant 3898 (Etype (Prefix (N))); 3899 3900 while Present (Elem) loop 3901 Son := new Perm_Tree_Wrapper' 3902 (Tree => 3903 (Kind => Entire_Object, 3904 Is_Node_Deep => Is_Deep (Etype (Elem)), 3905 Permission => Children_Perm, 3906 Children_Permission => Children_Perm)); 3907 3908 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son); 3909 Next_Component_Or_Discriminant (Elem); 3910 end loop; 3911 -- Now we set the right field to Borrowed, and then we 3912 -- return the tree to the sons, so that the recursion can 3913 -- continue. 3914 3915 declare 3916 Selected_Component : constant Entity_Id := 3917 Entity (Selector_Name (N)); 3918 Selected_C : Perm_Tree_Access := 3919 Perm_Tree_Maps.Get 3920 (Component (C), Selected_Component); 3921 3922 begin 3923 if Selected_C = null then 3924 Selected_C := Other_Components (C); 3925 end if; 3926 3927 pragma Assert (Selected_C /= null); 3928 Selected_C.all.Tree.Permission := New_Perm; 3929 return Selected_C; 3930 end; 3931 end; 3932 else 3933 raise Program_Error; 3934 end if; 3935 end; 3936 3937 -- We set the permission tree of its prefix, and then we extract 3938 -- from the returned pointer the subtree and assign an adequate 3939 -- permission to it, if unfolded. If folded, we unroll the tree in 3940 -- one step. 3941 3942 when N_Indexed_Component 3943 | N_Slice 3944 => 3945 declare 3946 C : constant Perm_Tree_Access := 3947 Set_Perm_Prefixes (Prefix (N), New_Perm); 3948 3949 begin 3950 if C = null then 3951 3952 -- We went through a function call, do nothing 3953 3954 return null; 3955 end if; 3956 3957 pragma Assert (Kind (C) = Entire_Object 3958 or else Kind (C) = Array_Component); 3959 3960 if Kind (C) = Array_Component then 3961 3962 -- The tree is unfolded. We just modify the permission and 3963 -- return the elem subtree. 3964 3965 pragma Assert (Get_Elem (C) /= null); 3966 C.all.Tree.Get_Elem.all.Tree.Permission := New_Perm; 3967 return Get_Elem (C); 3968 3969 elsif Kind (C) = Entire_Object then 3970 declare 3971 -- Expand the tree. Replace node with Array_Component. 3972 3973 Son : Perm_Tree_Access; 3974 3975 begin 3976 Son := new Perm_Tree_Wrapper' 3977 (Tree => 3978 (Kind => Entire_Object, 3979 Is_Node_Deep => Is_Node_Deep (C), 3980 Permission => New_Perm, 3981 Children_Permission => Children_Permission (C))); 3982 3983 -- Children_Permission => Children_Permission (C) 3984 -- this line should be checked maybe New_Perm 3985 -- instead of Children_Permission (C) 3986 3987 -- We change the current node from Entire_Object 3988 -- to Array_Component with same permission and the 3989 -- previously defined son. 3990 3991 C.all.Tree := (Kind => Array_Component, 3992 Is_Node_Deep => Is_Node_Deep (C), 3993 Permission => New_Perm, 3994 Get_Elem => Son); 3995 return Get_Elem (C); 3996 end; 3997 else 3998 raise Program_Error; 3999 end if; 4000 end; 4001 4002 -- We set the permission tree of its prefix, and then we extract 4003 -- from the returned pointer the subtree and assign an adequate 4004 -- permission to it, if unfolded. If folded, we unroll the tree 4005 -- at one step. 4006 4007 when N_Explicit_Dereference => 4008 declare 4009 C : constant Perm_Tree_Access := 4010 Set_Perm_Prefixes (Prefix (N), New_Perm); 4011 4012 begin 4013 if C = null then 4014 4015 -- We went through a function call. Do nothing. 4016 4017 return null; 4018 end if; 4019 4020 pragma Assert (Kind (C) = Entire_Object 4021 or else Kind (C) = Reference); 4022 4023 if Kind (C) = Reference then 4024 4025 -- The tree is unfolded. We just modify the permission and 4026 -- return the elem subtree. 4027 4028 pragma Assert (Get_All (C) /= null); 4029 C.all.Tree.Get_All.all.Tree.Permission := New_Perm; 4030 return Get_All (C); 4031 4032 elsif Kind (C) = Entire_Object then 4033 declare 4034 -- Expand the tree. Replace the node with Reference. 4035 4036 Son : Perm_Tree_Access; 4037 4038 begin 4039 Son := new Perm_Tree_Wrapper' 4040 (Tree => 4041 (Kind => Entire_Object, 4042 Is_Node_Deep => Is_Deep (Etype (N)), 4043 Permission => New_Perm, 4044 Children_Permission => Children_Permission (C))); 4045 4046 -- We change the current node from Entire_Object to 4047 -- Reference with Borrowed and the previous son. 4048 4049 pragma Assert (Is_Node_Deep (C)); 4050 C.all.Tree := (Kind => Reference, 4051 Is_Node_Deep => Is_Node_Deep (C), 4052 Permission => New_Perm, 4053 Get_All => Son); 4054 return Get_All (C); 4055 end; 4056 4057 else 4058 raise Program_Error; 4059 end if; 4060 end; 4061 4062 when N_Function_Call => 4063 return null; 4064 4065 when others => 4066 raise Program_Error; 4067 end case; 4068 end Set_Perm_Prefixes; 4069 4070 ------------------------------ 4071 -- Set_Perm_Prefixes_Borrow -- 4072 ------------------------------ 4073 4074 function Set_Perm_Prefixes_Borrow (N : Node_Id) return Perm_Tree_Access 4075 is 4076 begin 4077 pragma Assert (Current_Checking_Mode = Borrow); 4078 case Nkind (N) is 4079 4080 when N_Identifier 4081 | N_Expanded_Name 4082 => 4083 declare 4084 P : constant Node_Id := Entity (N); 4085 C : constant Perm_Tree_Access := 4086 Get (Current_Perm_Env, Unique_Entity (P)); 4087 pragma Assert (C /= null); 4088 4089 begin 4090 -- Setting the initialization map to True, so that this 4091 -- variable cannot be ignored anymore when looking at end 4092 -- of elaboration of package. 4093 4094 Set (Current_Initialization_Map, Unique_Entity (P), True); 4095 C.all.Tree.Permission := Borrowed; 4096 return C; 4097 end; 4098 4099 when N_Type_Conversion 4100 | N_Unchecked_Type_Conversion 4101 | N_Qualified_Expression 4102 => 4103 return Set_Perm_Prefixes_Borrow (Expression (N)); 4104 4105 when N_Parameter_Specification 4106 | N_Defining_Identifier 4107 => 4108 raise Program_Error; 4109 4110 -- We set the permission tree of its prefix, and then we extract 4111 -- our subtree from the returned pointer and assign an adequate 4112 -- permission to it, if unfolded. If folded, we unroll the tree 4113 -- in one step. 4114 4115 when N_Selected_Component => 4116 declare 4117 C : constant Perm_Tree_Access := 4118 Set_Perm_Prefixes_Borrow (Prefix (N)); 4119 4120 begin 4121 if C = null then 4122 4123 -- We went through a function call, do nothing 4124 4125 return null; 4126 end if; 4127 4128 -- The permission of the returned node should be No 4129 4130 pragma Assert (Permission (C) = Borrowed); 4131 pragma Assert (Kind (C) = Entire_Object 4132 or else Kind (C) = Record_Component); 4133 4134 if Kind (C) = Record_Component then 4135 4136 -- The tree is unfolded. We just modify the permission and 4137 -- return the record subtree. 4138 4139 declare 4140 Selected_Component : constant Entity_Id := 4141 Entity (Selector_Name (N)); 4142 Selected_C : Perm_Tree_Access := 4143 Perm_Tree_Maps.Get 4144 (Component (C), Selected_Component); 4145 4146 begin 4147 if Selected_C = null then 4148 Selected_C := Other_Components (C); 4149 end if; 4150 4151 pragma Assert (Selected_C /= null); 4152 Selected_C.all.Tree.Permission := Borrowed; 4153 return Selected_C; 4154 end; 4155 4156 elsif Kind (C) = Entire_Object then 4157 declare 4158 -- Expand the tree. Replace the node with 4159 -- Record_Component. 4160 4161 Elem : Node_Id; 4162 4163 -- Create an empty hash table 4164 4165 Hashtbl : Perm_Tree_Maps.Instance; 4166 4167 -- We create the unrolled nodes, that will all have same 4168 -- permission than parent. 4169 4170 Son : Perm_Tree_Access; 4171 ChildrenPerm : constant Perm_Kind := 4172 Children_Permission (C); 4173 4174 begin 4175 -- We change the current node from Entire_Object to 4176 -- Record_Component with same permission and an empty 4177 -- hash table as component list. 4178 4179 C.all.Tree := 4180 (Kind => Record_Component, 4181 Is_Node_Deep => Is_Node_Deep (C), 4182 Permission => Permission (C), 4183 Component => Hashtbl, 4184 Other_Components => 4185 new Perm_Tree_Wrapper' 4186 (Tree => 4187 (Kind => Entire_Object, 4188 Is_Node_Deep => True, 4189 Permission => ChildrenPerm, 4190 Children_Permission => ChildrenPerm) 4191 )); 4192 4193 -- We fill the hash table with all sons of the record, 4194 -- with basic Entire_Objects nodes. 4195 4196 Elem := First_Component_Or_Discriminant 4197 (Etype (Prefix (N))); 4198 4199 while Present (Elem) loop 4200 Son := new Perm_Tree_Wrapper' 4201 (Tree => 4202 (Kind => Entire_Object, 4203 Is_Node_Deep => Is_Deep (Etype (Elem)), 4204 Permission => ChildrenPerm, 4205 Children_Permission => ChildrenPerm)); 4206 Perm_Tree_Maps.Set (C.all.Tree.Component, Elem, Son); 4207 Next_Component_Or_Discriminant (Elem); 4208 end loop; 4209 4210 -- Now we set the right field to Borrowed, and then we 4211 -- return the tree to the sons, so that the recursion can 4212 -- continue. 4213 4214 declare 4215 Selected_Component : constant Entity_Id := 4216 Entity (Selector_Name (N)); 4217 Selected_C : Perm_Tree_Access := Perm_Tree_Maps.Get 4218 (Component (C), Selected_Component); 4219 4220 begin 4221 if Selected_C = null then 4222 Selected_C := Other_Components (C); 4223 end if; 4224 4225 pragma Assert (Selected_C /= null); 4226 Selected_C.all.Tree.Permission := Borrowed; 4227 return Selected_C; 4228 end; 4229 end; 4230 4231 else 4232 raise Program_Error; 4233 end if; 4234 end; 4235 4236 -- We set the permission tree of its prefix, and then we extract 4237 -- from the returned pointer the subtree and assign an adequate 4238 -- permission to it, if unfolded. If folded, we unroll the tree in 4239 -- one step. 4240 4241 when N_Indexed_Component 4242 | N_Slice 4243 => 4244 declare 4245 C : constant Perm_Tree_Access := 4246 Set_Perm_Prefixes_Borrow (Prefix (N)); 4247 4248 begin 4249 if C = null then 4250 4251 -- We went through a function call, do nothing 4252 4253 return null; 4254 end if; 4255 4256 pragma Assert (Permission (C) = Borrowed); 4257 pragma Assert (Kind (C) = Entire_Object 4258 or else Kind (C) = Array_Component); 4259 4260 if Kind (C) = Array_Component then 4261 4262 -- The tree is unfolded. We just modify the permission and 4263 -- return the elem subtree. 4264 4265 pragma Assert (Get_Elem (C) /= null); 4266 C.all.Tree.Get_Elem.all.Tree.Permission := Borrowed; 4267 return Get_Elem (C); 4268 4269 elsif Kind (C) = Entire_Object then 4270 declare 4271 -- Expand the tree. Replace node with Array_Component. 4272 4273 Son : Perm_Tree_Access; 4274 4275 begin 4276 Son := new Perm_Tree_Wrapper' 4277 (Tree => 4278 (Kind => Entire_Object, 4279 Is_Node_Deep => Is_Node_Deep (C), 4280 Permission => Borrowed, 4281 Children_Permission => Children_Permission (C))); 4282 4283 -- We change the current node from Entire_Object 4284 -- to Array_Component with same permission and the 4285 -- previously defined son. 4286 4287 C.all.Tree := (Kind => Array_Component, 4288 Is_Node_Deep => Is_Node_Deep (C), 4289 Permission => Borrowed, 4290 Get_Elem => Son); 4291 return Get_Elem (C); 4292 end; 4293 4294 else 4295 raise Program_Error; 4296 end if; 4297 end; 4298 4299 -- We set the permission tree of its prefix, and then we extract 4300 -- from the returned pointer the subtree and assign an adequate 4301 -- permission to it, if unfolded. If folded, we unroll the tree 4302 -- at one step. 4303 4304 when N_Explicit_Dereference => 4305 declare 4306 C : constant Perm_Tree_Access := 4307 Set_Perm_Prefixes_Borrow (Prefix (N)); 4308 4309 begin 4310 if C = null then 4311 4312 -- We went through a function call. Do nothing. 4313 4314 return null; 4315 end if; 4316 4317 -- The permission of the returned node should be No 4318 4319 pragma Assert (Permission (C) = Borrowed); 4320 pragma Assert (Kind (C) = Entire_Object 4321 or else Kind (C) = Reference); 4322 4323 if Kind (C) = Reference then 4324 4325 -- The tree is unfolded. We just modify the permission and 4326 -- return the elem subtree. 4327 4328 pragma Assert (Get_All (C) /= null); 4329 C.all.Tree.Get_All.all.Tree.Permission := Borrowed; 4330 return Get_All (C); 4331 4332 elsif Kind (C) = Entire_Object then 4333 declare 4334 -- Expand the tree. Replace the node with Reference. 4335 4336 Son : Perm_Tree_Access; 4337 4338 begin 4339 Son := new Perm_Tree_Wrapper' 4340 (Tree => 4341 (Kind => Entire_Object, 4342 Is_Node_Deep => Is_Deep (Etype (N)), 4343 Permission => Borrowed, 4344 Children_Permission => Children_Permission (C))); 4345 4346 -- We change the current node from Entire_Object to 4347 -- Reference with Borrowed and the previous son. 4348 4349 pragma Assert (Is_Node_Deep (C)); 4350 C.all.Tree := (Kind => Reference, 4351 Is_Node_Deep => Is_Node_Deep (C), 4352 Permission => Borrowed, 4353 Get_All => Son); 4354 return Get_All (C); 4355 end; 4356 4357 else 4358 raise Program_Error; 4359 end if; 4360 end; 4361 4362 when N_Function_Call => 4363 return null; 4364 4365 when others => 4366 raise Program_Error; 4367 end case; 4368 end Set_Perm_Prefixes_Borrow; 4369 4370 ------------------- 4371 -- Setup_Globals -- 4372 ------------------- 4373 4374 procedure Setup_Globals (Subp : Entity_Id) is 4375 procedure Setup_Globals_From_List 4376 (First_Item : Node_Id; 4377 Kind : Formal_Kind); 4378 -- Set up global items from the list starting at Item 4379 4380 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id); 4381 -- Set up global items for the mode Global_Mode 4382 4383 ----------------------------- 4384 -- Setup_Globals_From_List -- 4385 ----------------------------- 4386 4387 procedure Setup_Globals_From_List 4388 (First_Item : Node_Id; 4389 Kind : Formal_Kind) 4390 is 4391 Item : Node_Id := First_Item; 4392 E : Entity_Id; 4393 4394 begin 4395 while Present (Item) loop 4396 E := Entity (Item); 4397 4398 -- Ignore abstract states, which play no role in pointer aliasing 4399 4400 if Ekind (E) = E_Abstract_State then 4401 null; 4402 else 4403 Setup_Parameter_Or_Global (E, Kind, Global_Var => True); 4404 end if; 4405 Next_Global (Item); 4406 end loop; 4407 end Setup_Globals_From_List; 4408 4409 --------------------------- 4410 -- Setup_Globals_Of_Mode -- 4411 --------------------------- 4412 4413 procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is 4414 Kind : Formal_Kind; 4415 4416 begin 4417 case Global_Mode is 4418 when Name_Input 4419 | Name_Proof_In 4420 => 4421 Kind := E_In_Parameter; 4422 4423 when Name_Output => 4424 Kind := E_Out_Parameter; 4425 4426 when Name_In_Out => 4427 Kind := E_In_Out_Parameter; 4428 4429 when others => 4430 raise Program_Error; 4431 end case; 4432 4433 -- Set up both global items from Global and Refined_Global pragmas 4434 4435 Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind); 4436 Setup_Globals_From_List 4437 (First_Global (Subp, Global_Mode, Refined => True), Kind); 4438 end Setup_Globals_Of_Mode; 4439 4440 -- Start of processing for Setup_Globals 4441 4442 begin 4443 Setup_Globals_Of_Mode (Name_Proof_In); 4444 Setup_Globals_Of_Mode (Name_Input); 4445 Setup_Globals_Of_Mode (Name_Output); 4446 Setup_Globals_Of_Mode (Name_In_Out); 4447 end Setup_Globals; 4448 4449 ------------------------------- 4450 -- Setup_Parameter_Or_Global -- 4451 ------------------------------- 4452 4453 procedure Setup_Parameter_Or_Global 4454 (Id : Entity_Id; 4455 Mode : Formal_Kind; 4456 Global_Var : Boolean) 4457 is 4458 Elem : Perm_Tree_Access; 4459 View_Typ : Entity_Id; 4460 4461 begin 4462 if Present (Full_View (Etype (Id))) then 4463 View_Typ := Full_View (Etype (Id)); 4464 else 4465 View_Typ := Etype (Id); 4466 end if; 4467 4468 Elem := new Perm_Tree_Wrapper' 4469 (Tree => 4470 (Kind => Entire_Object, 4471 Is_Node_Deep => Is_Deep (Etype (Id)), 4472 Permission => Unrestricted, 4473 Children_Permission => Unrestricted)); 4474 4475 case Mode is 4476 4477 -- All out and in out parameters are considered to be unrestricted. 4478 -- They are whether borrowed or moved. Ada Rules would restrict 4479 -- these permissions further. For example an in parameter cannot 4480 -- be written. 4481 4482 -- In the following we deal with in parameters that can be observed. 4483 -- We only consider the observing cases. 4484 4485 when E_In_Parameter => 4486 4487 -- Handling global variables as IN parameters here. 4488 -- Remove the following condition once it's decided how globals 4489 -- should be considered. ??? 4490 -- 4491 -- In SPARK, IN access-to-variable is an observe operation for 4492 -- a function, and a borrow operation for a procedure. 4493 4494 if not Global_Var then 4495 if (Is_Access_Type (View_Typ) 4496 and then Is_Access_Constant (View_Typ) 4497 and then Is_Anonymous_Access_Type (View_Typ)) 4498 or else 4499 (Is_Access_Type (View_Typ) 4500 and then Ekind (Scope (Id)) = E_Function) 4501 or else 4502 (not Is_Access_Type (View_Typ) 4503 and then Is_Deep (View_Typ) 4504 and then not Is_Anonymous_Access_Type (View_Typ)) 4505 then 4506 Elem.all.Tree.Permission := Observed; 4507 Elem.all.Tree.Children_Permission := Observed; 4508 4509 else 4510 Elem.all.Tree.Permission := Unrestricted; 4511 Elem.all.Tree.Children_Permission := Unrestricted; 4512 end if; 4513 4514 else 4515 Elem.all.Tree.Permission := Observed; 4516 Elem.all.Tree.Children_Permission := Observed; 4517 end if; 4518 4519 -- When out or in/out formal or global parameters, we set them to 4520 -- the Unrestricted state. "We want to be able to assume that all 4521 -- relevant writable globals are unrestricted when a subprogram 4522 -- starts executing". Formal parameters of mode out or in/out 4523 -- are whether Borrowers or the targets of a move operation: 4524 -- they start theirs lives in the subprogram as Unrestricted. 4525 4526 when others => 4527 Elem.all.Tree.Permission := Unrestricted; 4528 Elem.all.Tree.Children_Permission := Unrestricted; 4529 end case; 4530 4531 Set (Current_Perm_Env, Id, Elem); 4532 end Setup_Parameter_Or_Global; 4533 4534 ---------------------- 4535 -- Setup_Parameters -- 4536 ---------------------- 4537 4538 procedure Setup_Parameters (Subp : Entity_Id) is Formal : Entity_Id; 4539 begin 4540 Formal := First_Formal (Subp); 4541 while Present (Formal) loop 4542 Setup_Parameter_Or_Global 4543 (Formal, Ekind (Formal), Global_Var => False); 4544 Next_Formal (Formal); 4545 end loop; 4546 end Setup_Parameters; 4547 4548 ------------------------------- 4549 -- Has_Ownership_Aspect_True -- 4550 ------------------------------- 4551 4552 function Has_Ownership_Aspect_True 4553 (N : Entity_Id; 4554 Msg : String) 4555 return Boolean 4556 is 4557 begin 4558 case Ekind (Etype (N)) is 4559 when Access_Kind => 4560 if Ekind (Etype (N)) = E_General_Access_Type then 4561 Error_Msg_NE (Msg & " & not allowed " & 4562 "(Named General Access type)", N, N); 4563 return False; 4564 4565 else 4566 return True; 4567 end if; 4568 4569 when E_Array_Type 4570 | E_Array_Subtype 4571 => 4572 declare 4573 Com_Ty : constant Node_Id := Component_Type (Etype (N)); 4574 Ret : Boolean := Has_Ownership_Aspect_True (Com_Ty, ""); 4575 4576 begin 4577 if Nkind (Parent (N)) = N_Full_Type_Declaration and 4578 Is_Anonymous_Access_Type (Com_Ty) 4579 then 4580 Ret := False; 4581 end if; 4582 4583 if not Ret then 4584 Error_Msg_NE (Msg & " & not allowed " 4585 & "(Components of Named General Access type or" 4586 & " Anonymous type)", N, N); 4587 end if; 4588 return Ret; 4589 end; 4590 4591 -- ??? What about hidden components 4592 4593 when E_Record_Type 4594 | E_Record_Subtype 4595 => 4596 declare 4597 Elmt : Entity_Id; 4598 Elmt_T_Perm : Boolean := True; 4599 Elmt_Perm, Elmt_Anonym : Boolean; 4600 4601 begin 4602 Elmt := First_Component_Or_Discriminant (Etype (N)); 4603 while Present (Elmt) loop 4604 Elmt_Perm := Has_Ownership_Aspect_True (Elmt, 4605 "type of component"); 4606 Elmt_Anonym := Is_Anonymous_Access_Type (Etype (Elmt)); 4607 if Elmt_Anonym then 4608 Error_Msg_NE 4609 ("type of component & not allowed" 4610 & " (Components of Anonymous type)", Elmt, Elmt); 4611 end if; 4612 Elmt_T_Perm := Elmt_T_Perm and Elmt_Perm and not Elmt_Anonym; 4613 Next_Component_Or_Discriminant (Elmt); 4614 end loop; 4615 if not Elmt_T_Perm then 4616 Error_Msg_NE 4617 (Msg & " & not allowed (One or " 4618 & "more components have Ownership Aspect False)", 4619 N, N); 4620 end if; 4621 return Elmt_T_Perm; 4622 end; 4623 4624 when others => 4625 return True; 4626 end case; 4627 4628 end Has_Ownership_Aspect_True; 4629end Sem_SPARK; 4630