1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- L I B . X R E F . S P A R K _ S P E C I F I C -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2011-2013, 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 SPARK_Xrefs; use SPARK_Xrefs; 27with Einfo; use Einfo; 28with Nmake; use Nmake; 29with Put_SPARK_Xrefs; 30 31with GNAT.HTable; 32 33separate (Lib.Xref) 34package body SPARK_Specific is 35 36 --------------------- 37 -- Local Constants -- 38 --------------------- 39 40 -- Table of SPARK_Entities, True for each entity kind used in SPARK 41 42 SPARK_Entities : constant array (Entity_Kind) of Boolean := 43 (E_Constant => True, 44 E_Function => True, 45 E_In_Out_Parameter => True, 46 E_In_Parameter => True, 47 E_Loop_Parameter => True, 48 E_Operator => True, 49 E_Out_Parameter => True, 50 E_Procedure => True, 51 E_Variable => True, 52 others => False); 53 54 -- True for each reference type used in SPARK 55 56 SPARK_References : constant array (Character) of Boolean := 57 ('m' => True, 58 'r' => True, 59 's' => True, 60 others => False); 61 62 type Entity_Hashed_Range is range 0 .. 255; 63 -- Size of hash table headers 64 65 --------------------- 66 -- Local Variables -- 67 --------------------- 68 69 Heap : Entity_Id := Empty; 70 -- A special entity which denotes the heap object 71 72 package Drefs is new Table.Table ( 73 Table_Component_Type => Xref_Entry, 74 Table_Index_Type => Xref_Entry_Number, 75 Table_Low_Bound => 1, 76 Table_Initial => Alloc.Drefs_Initial, 77 Table_Increment => Alloc.Drefs_Increment, 78 Table_Name => "Drefs"); 79 -- Table of cross-references for reads and writes through explicit 80 -- dereferences, that are output as reads/writes to the special variable 81 -- "Heap". These references are added to the regular references when 82 -- computing SPARK cross-references. 83 84 ----------------------- 85 -- Local Subprograms -- 86 ----------------------- 87 88 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat); 89 -- Add file and corresponding scopes for unit to the tables 90 -- SPARK_File_Table and SPARK_Scope_Table. When two units are present for 91 -- the same compilation unit, as it happens for library-level 92 -- instantiations of generics, then Ubody /= Uspec, and all scopes are 93 -- added to the same SPARK file. Otherwise Ubody = Uspec. 94 95 procedure Add_SPARK_Scope (N : Node_Id); 96 -- Add scope N to the table SPARK_Scope_Table 97 98 procedure Add_SPARK_Xrefs; 99 -- Filter table Xrefs to add all references used in SPARK to the table 100 -- SPARK_Xref_Table. 101 102 procedure Detect_And_Add_SPARK_Scope (N : Node_Id); 103 -- Call Add_SPARK_Scope on scopes 104 105 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; 106 -- Hash function for hash table 107 108 procedure Traverse_Declarations_Or_Statements 109 (L : List_Id; 110 Process : Node_Processing; 111 Inside_Stubs : Boolean); 112 procedure Traverse_Handled_Statement_Sequence 113 (N : Node_Id; 114 Process : Node_Processing; 115 Inside_Stubs : Boolean); 116 procedure Traverse_Package_Body 117 (N : Node_Id; 118 Process : Node_Processing; 119 Inside_Stubs : Boolean); 120 procedure Traverse_Package_Declaration 121 (N : Node_Id; 122 Process : Node_Processing; 123 Inside_Stubs : Boolean); 124 procedure Traverse_Subprogram_Body 125 (N : Node_Id; 126 Process : Node_Processing; 127 Inside_Stubs : Boolean); 128 -- Traverse corresponding construct, calling Process on all declarations 129 130 -------------------- 131 -- Add_SPARK_File -- 132 -------------------- 133 134 procedure Add_SPARK_File (Ubody, Uspec : Unit_Number_Type; Dspec : Nat) is 135 File : constant Source_File_Index := Source_Index (Uspec); 136 From : Scope_Index; 137 138 File_Name : String_Ptr; 139 Unit_File_Name : String_Ptr; 140 141 begin 142 -- Source file could be inexistant as a result of an error, if option 143 -- gnatQ is used. 144 145 if File = No_Source_File then 146 return; 147 end if; 148 149 From := SPARK_Scope_Table.Last + 1; 150 151 -- Unit might not have an associated compilation unit, as seen in code 152 -- filling Sdep_Table in Write_ALI. 153 154 if Present (Cunit (Ubody)) then 155 Traverse_Compilation_Unit 156 (CU => Cunit (Ubody), 157 Process => Detect_And_Add_SPARK_Scope'Access, 158 Inside_Stubs => False); 159 end if; 160 161 -- When two units are present for the same compilation unit, as it 162 -- happens for library-level instantiations of generics, then add all 163 -- scopes to the same SPARK file. 164 165 if Ubody /= Uspec then 166 if Present (Cunit (Uspec)) then 167 Traverse_Compilation_Unit 168 (CU => Cunit (Uspec), 169 Process => Detect_And_Add_SPARK_Scope'Access, 170 Inside_Stubs => False); 171 end if; 172 end if; 173 174 -- Update scope numbers 175 176 declare 177 Scope_Id : Int; 178 begin 179 Scope_Id := 1; 180 for Index in From .. SPARK_Scope_Table.Last loop 181 declare 182 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 183 begin 184 S.Scope_Num := Scope_Id; 185 S.File_Num := Dspec; 186 Scope_Id := Scope_Id + 1; 187 end; 188 end loop; 189 end; 190 191 -- Remove those scopes previously marked for removal 192 193 declare 194 Scope_Id : Scope_Index; 195 196 begin 197 Scope_Id := From; 198 for Index in From .. SPARK_Scope_Table.Last loop 199 declare 200 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 201 begin 202 if S.Scope_Num /= 0 then 203 SPARK_Scope_Table.Table (Scope_Id) := S; 204 Scope_Id := Scope_Id + 1; 205 end if; 206 end; 207 end loop; 208 209 SPARK_Scope_Table.Set_Last (Scope_Id - 1); 210 end; 211 212 -- Make entry for new file in file table 213 214 Get_Name_String (Reference_Name (File)); 215 File_Name := new String'(Name_Buffer (1 .. Name_Len)); 216 217 -- For subunits, also retrieve the file name of the unit. Only do so if 218 -- unit has an associated compilation unit. 219 220 if Present (Cunit (Uspec)) 221 and then Present (Cunit (Unit (File))) 222 and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit 223 then 224 Get_Name_String (Reference_Name (Main_Source_File)); 225 Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len)); 226 end if; 227 228 SPARK_File_Table.Append ( 229 (File_Name => File_Name, 230 Unit_File_Name => Unit_File_Name, 231 File_Num => Dspec, 232 From_Scope => From, 233 To_Scope => SPARK_Scope_Table.Last)); 234 end Add_SPARK_File; 235 236 --------------------- 237 -- Add_SPARK_Scope -- 238 --------------------- 239 240 procedure Add_SPARK_Scope (N : Node_Id) is 241 E : constant Entity_Id := Defining_Entity (N); 242 Loc : constant Source_Ptr := Sloc (E); 243 Typ : Character; 244 245 begin 246 -- Ignore scopes without a proper location 247 248 if Sloc (N) = No_Location then 249 return; 250 end if; 251 252 case Ekind (E) is 253 when E_Function | E_Generic_Function => 254 Typ := 'V'; 255 256 when E_Procedure | E_Generic_Procedure => 257 Typ := 'U'; 258 259 when E_Subprogram_Body => 260 declare 261 Spec : Node_Id; 262 263 begin 264 Spec := Parent (E); 265 266 if Nkind (Spec) = N_Defining_Program_Unit_Name then 267 Spec := Parent (Spec); 268 end if; 269 270 if Nkind (Spec) = N_Function_Specification then 271 Typ := 'V'; 272 else 273 pragma Assert 274 (Nkind (Spec) = N_Procedure_Specification); 275 Typ := 'U'; 276 end if; 277 end; 278 279 when E_Package | E_Package_Body | E_Generic_Package => 280 Typ := 'K'; 281 282 when E_Void => 283 -- Compilation of prj-attr.adb with -gnatn creates a node with 284 -- entity E_Void for the package defined at a-charac.ads16:13 285 286 -- ??? TBD 287 288 return; 289 290 when others => 291 raise Program_Error; 292 end case; 293 294 -- File_Num and Scope_Num are filled later. From_Xref and To_Xref are 295 -- filled even later, but are initialized to represent an empty range. 296 297 SPARK_Scope_Table.Append ( 298 (Scope_Name => new String'(Unique_Name (E)), 299 File_Num => 0, 300 Scope_Num => 0, 301 Spec_File_Num => 0, 302 Spec_Scope_Num => 0, 303 Line => Nat (Get_Logical_Line_Number (Loc)), 304 Stype => Typ, 305 Col => Nat (Get_Column_Number (Loc)), 306 From_Xref => 1, 307 To_Xref => 0, 308 Scope_Entity => E)); 309 end Add_SPARK_Scope; 310 311 --------------------- 312 -- Add_SPARK_Xrefs -- 313 --------------------- 314 315 procedure Add_SPARK_Xrefs is 316 function Entity_Of_Scope (S : Scope_Index) return Entity_Id; 317 -- Return the entity which maps to the input scope index 318 319 function Get_Entity_Type (E : Entity_Id) return Character; 320 -- Return a character representing the type of entity 321 322 function Is_SPARK_Reference 323 (E : Entity_Id; 324 Typ : Character) return Boolean; 325 -- Return whether entity reference E meets SPARK requirements. Typ is 326 -- the reference type. 327 328 function Is_SPARK_Scope (E : Entity_Id) return Boolean; 329 -- Return whether the entity or reference scope meets requirements for 330 -- being an SPARK scope. 331 332 function Is_Future_Scope_Entity 333 (E : Entity_Id; 334 S : Scope_Index) return Boolean; 335 -- Check whether entity E is in SPARK_Scope_Table at index S or higher 336 337 function Lt (Op1 : Natural; Op2 : Natural) return Boolean; 338 -- Comparison function for Sort call 339 340 procedure Move (From : Natural; To : Natural); 341 -- Move procedure for Sort call 342 343 procedure Update_Scope_Range 344 (S : Scope_Index; 345 From : Xref_Index; 346 To : Xref_Index); 347 -- Update the scope which maps to S with the new range From .. To 348 349 package Sorting is new GNAT.Heap_Sort_G (Move, Lt); 350 351 function Get_Scope_Num (N : Entity_Id) return Nat; 352 -- Return the scope number associated to entity N 353 354 procedure Set_Scope_Num (N : Entity_Id; Num : Nat); 355 -- Associate entity N to scope number Num 356 357 No_Scope : constant Nat := 0; 358 -- Initial scope counter 359 360 type Scope_Rec is record 361 Num : Nat; 362 Entity : Entity_Id; 363 end record; 364 -- Type used to relate an entity and a scope number 365 366 package Scopes is new GNAT.HTable.Simple_HTable 367 (Header_Num => Entity_Hashed_Range, 368 Element => Scope_Rec, 369 No_Element => (Num => No_Scope, Entity => Empty), 370 Key => Entity_Id, 371 Hash => Entity_Hash, 372 Equal => "="); 373 -- Package used to build a correspondance between entities and scope 374 -- numbers used in SPARK cross references. 375 376 Nrefs : Nat := Xrefs.Last; 377 -- Number of references in table. This value may get reset (reduced) 378 -- when we eliminate duplicate reference entries as well as references 379 -- not suitable for local cross-references. 380 381 Nrefs_Add : constant Nat := Drefs.Last; 382 -- Number of additional references which correspond to dereferences in 383 -- the source code. 384 385 Rnums : array (0 .. Nrefs + Nrefs_Add) of Nat; 386 -- This array contains numbers of references in the Xrefs table. This 387 -- list is sorted in output order. The extra 0'th entry is convenient 388 -- for the call to sort. When we sort the table, we move the entries in 389 -- Rnums around, but we do not move the original table entries. 390 391 --------------------- 392 -- Entity_Of_Scope -- 393 --------------------- 394 395 function Entity_Of_Scope (S : Scope_Index) return Entity_Id is 396 begin 397 return SPARK_Scope_Table.Table (S).Scope_Entity; 398 end Entity_Of_Scope; 399 400 --------------------- 401 -- Get_Entity_Type -- 402 --------------------- 403 404 function Get_Entity_Type (E : Entity_Id) return Character is 405 begin 406 case Ekind (E) is 407 when E_Out_Parameter => return '<'; 408 when E_In_Out_Parameter => return '='; 409 when E_In_Parameter => return '>'; 410 when others => return '*'; 411 end case; 412 end Get_Entity_Type; 413 414 ------------------- 415 -- Get_Scope_Num -- 416 ------------------- 417 418 function Get_Scope_Num (N : Entity_Id) return Nat is 419 begin 420 return Scopes.Get (N).Num; 421 end Get_Scope_Num; 422 423 ------------------------ 424 -- Is_SPARK_Reference -- 425 ------------------------ 426 427 function Is_SPARK_Reference 428 (E : Entity_Id; 429 Typ : Character) return Boolean 430 is 431 begin 432 -- The only references of interest on callable entities are calls. On 433 -- non-callable entities, the only references of interest are reads 434 -- and writes. 435 436 if Ekind (E) in Overloadable_Kind then 437 return Typ = 's'; 438 439 -- Objects of Task type or protected type are not SPARK references 440 441 elsif Present (Etype (E)) 442 and then Ekind (Etype (E)) in Concurrent_Kind 443 then 444 return False; 445 446 -- In all other cases, result is true for reference/modify cases, 447 -- and false for all other cases. 448 449 else 450 return Typ = 'r' or else Typ = 'm'; 451 end if; 452 end Is_SPARK_Reference; 453 454 -------------------- 455 -- Is_SPARK_Scope -- 456 -------------------- 457 458 function Is_SPARK_Scope (E : Entity_Id) return Boolean is 459 begin 460 return Present (E) 461 and then not Is_Generic_Unit (E) 462 and then Renamed_Entity (E) = Empty 463 and then Get_Scope_Num (E) /= No_Scope; 464 end Is_SPARK_Scope; 465 466 ---------------------------- 467 -- Is_Future_Scope_Entity -- 468 ---------------------------- 469 470 function Is_Future_Scope_Entity 471 (E : Entity_Id; 472 S : Scope_Index) return Boolean 473 is 474 function Is_Past_Scope_Entity return Boolean; 475 -- Check whether entity E is in SPARK_Scope_Table at index strictly 476 -- lower than S. 477 478 -------------------------- 479 -- Is_Past_Scope_Entity -- 480 -------------------------- 481 482 function Is_Past_Scope_Entity return Boolean is 483 begin 484 for Index in SPARK_Scope_Table.First .. S - 1 loop 485 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then 486 declare 487 Dummy : constant SPARK_Scope_Record := 488 SPARK_Scope_Table.Table (Index); 489 pragma Unreferenced (Dummy); 490 begin 491 return True; 492 end; 493 end if; 494 end loop; 495 496 return False; 497 end Is_Past_Scope_Entity; 498 499 -- Start of processing for Is_Future_Scope_Entity 500 501 begin 502 for Index in S .. SPARK_Scope_Table.Last loop 503 if SPARK_Scope_Table.Table (Index).Scope_Entity = E then 504 return True; 505 end if; 506 end loop; 507 508 -- If this assertion fails, this means that the scope which we are 509 -- looking for has been treated already, which reveals a problem in 510 -- the order of cross-references. 511 512 pragma Assert (not Is_Past_Scope_Entity); 513 514 return False; 515 end Is_Future_Scope_Entity; 516 517 -------- 518 -- Lt -- 519 -------- 520 521 function Lt (Op1, Op2 : Natural) return Boolean is 522 T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1))); 523 T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2))); 524 525 begin 526 -- First test: if entity is in different unit, sort by unit. Note: 527 -- that we use Ent_Scope_File rather than Eun, as Eun may refer to 528 -- the file where the generic scope is defined, which may differ from 529 -- the file where the enclosing scope is defined. It is the latter 530 -- which matters for a correct order here. 531 532 if T1.Ent_Scope_File /= T2.Ent_Scope_File then 533 return Dependency_Num (T1.Ent_Scope_File) < 534 Dependency_Num (T2.Ent_Scope_File); 535 536 -- Second test: within same unit, sort by location of the scope of 537 -- the entity definition. 538 539 elsif Get_Scope_Num (T1.Key.Ent_Scope) /= 540 Get_Scope_Num (T2.Key.Ent_Scope) 541 then 542 return Get_Scope_Num (T1.Key.Ent_Scope) < 543 Get_Scope_Num (T2.Key.Ent_Scope); 544 545 -- Third test: within same unit and scope, sort by location of 546 -- entity definition. 547 548 elsif T1.Def /= T2.Def then 549 return T1.Def < T2.Def; 550 551 else 552 -- Both entities must be equal at this point 553 554 pragma Assert (T1.Key.Ent = T2.Key.Ent); 555 556 -- Fourth test: if reference is in same unit as entity definition, 557 -- sort first. 558 559 if T1.Key.Lun /= T2.Key.Lun 560 and then T1.Ent_Scope_File = T1.Key.Lun 561 then 562 return True; 563 564 elsif T1.Key.Lun /= T2.Key.Lun 565 and then T2.Ent_Scope_File = T2.Key.Lun 566 then 567 return False; 568 569 -- Fifth test: if reference is in same unit and same scope as 570 -- entity definition, sort first. 571 572 elsif T1.Ent_Scope_File = T1.Key.Lun 573 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope 574 and then T1.Key.Ent_Scope = T1.Key.Ref_Scope 575 then 576 return True; 577 578 elsif T2.Ent_Scope_File = T2.Key.Lun 579 and then T1.Key.Ref_Scope /= T2.Key.Ref_Scope 580 and then T2.Key.Ent_Scope = T2.Key.Ref_Scope 581 then 582 return False; 583 584 -- Sixth test: for same entity, sort by reference location unit 585 586 elsif T1.Key.Lun /= T2.Key.Lun then 587 return Dependency_Num (T1.Key.Lun) < 588 Dependency_Num (T2.Key.Lun); 589 590 -- Seventh test: for same entity, sort by reference location scope 591 592 elsif Get_Scope_Num (T1.Key.Ref_Scope) /= 593 Get_Scope_Num (T2.Key.Ref_Scope) 594 then 595 return Get_Scope_Num (T1.Key.Ref_Scope) < 596 Get_Scope_Num (T2.Key.Ref_Scope); 597 598 -- Eighth test: order of location within referencing unit 599 600 elsif T1.Key.Loc /= T2.Key.Loc then 601 return T1.Key.Loc < T2.Key.Loc; 602 603 -- Finally, for two locations at the same address prefer the one 604 -- that does NOT have the type 'r', so that a modification or 605 -- extension takes preference, when there are more than one 606 -- reference at the same location. As a result, in the case of 607 -- entities that are in-out actuals, the read reference follows 608 -- the modify reference. 609 610 else 611 return T2.Key.Typ = 'r'; 612 end if; 613 end if; 614 end Lt; 615 616 ---------- 617 -- Move -- 618 ---------- 619 620 procedure Move (From : Natural; To : Natural) is 621 begin 622 Rnums (Nat (To)) := Rnums (Nat (From)); 623 end Move; 624 625 ------------------- 626 -- Set_Scope_Num -- 627 ------------------- 628 629 procedure Set_Scope_Num (N : Entity_Id; Num : Nat) is 630 begin 631 Scopes.Set (K => N, E => Scope_Rec'(Num => Num, Entity => N)); 632 end Set_Scope_Num; 633 634 ------------------------ 635 -- Update_Scope_Range -- 636 ------------------------ 637 638 procedure Update_Scope_Range 639 (S : Scope_Index; 640 From : Xref_Index; 641 To : Xref_Index) 642 is 643 begin 644 SPARK_Scope_Table.Table (S).From_Xref := From; 645 SPARK_Scope_Table.Table (S).To_Xref := To; 646 end Update_Scope_Range; 647 648 -- Local variables 649 650 Col : Nat; 651 From_Index : Xref_Index; 652 Line : Nat; 653 Loc : Source_Ptr; 654 Prev_Typ : Character; 655 Ref_Count : Nat; 656 Ref_Id : Entity_Id; 657 Ref_Name : String_Ptr; 658 Scope_Id : Scope_Index; 659 660 -- Start of processing for Add_SPARK_Xrefs 661 662 begin 663 for Index in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 664 declare 665 S : SPARK_Scope_Record renames SPARK_Scope_Table.Table (Index); 666 begin 667 Set_Scope_Num (S.Scope_Entity, S.Scope_Num); 668 end; 669 end loop; 670 671 -- Set up the pointer vector for the sort 672 673 for Index in 1 .. Nrefs loop 674 Rnums (Index) := Index; 675 end loop; 676 677 for Index in Drefs.First .. Drefs.Last loop 678 Xrefs.Append (Drefs.Table (Index)); 679 680 Nrefs := Nrefs + 1; 681 Rnums (Nrefs) := Xrefs.Last; 682 end loop; 683 684 -- Capture the definition Sloc values. As in the case of normal cross 685 -- references, we have to wait until now to get the correct value. 686 687 for Index in 1 .. Nrefs loop 688 Xrefs.Table (Index).Def := Sloc (Xrefs.Table (Index).Key.Ent); 689 end loop; 690 691 -- Eliminate entries not appropriate for SPARK. Done prior to sorting 692 -- cross-references, as it discards useless references which do not have 693 -- a proper format for the comparison function (like no location). 694 695 Ref_Count := Nrefs; 696 Nrefs := 0; 697 698 for Index in 1 .. Ref_Count loop 699 declare 700 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; 701 702 begin 703 if SPARK_Entities (Ekind (Ref.Ent)) 704 and then SPARK_References (Ref.Typ) 705 and then Is_SPARK_Scope (Ref.Ent_Scope) 706 and then Is_SPARK_Scope (Ref.Ref_Scope) 707 and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) 708 709 -- Discard references from unknown scopes, e.g. generic scopes 710 711 and then Get_Scope_Num (Ref.Ent_Scope) /= No_Scope 712 and then Get_Scope_Num (Ref.Ref_Scope) /= No_Scope 713 then 714 Nrefs := Nrefs + 1; 715 Rnums (Nrefs) := Rnums (Index); 716 end if; 717 end; 718 end loop; 719 720 -- Sort the references 721 722 Sorting.Sort (Integer (Nrefs)); 723 724 -- Eliminate duplicate entries 725 726 -- We need this test for Ref_Count because if we force ALI file 727 -- generation in case of errors detected, it may be the case that 728 -- Nrefs is 0, so we should not reset it here. 729 730 if Nrefs >= 2 then 731 Ref_Count := Nrefs; 732 Nrefs := 1; 733 734 for Index in 2 .. Ref_Count loop 735 if Xrefs.Table (Rnums (Index)) /= 736 Xrefs.Table (Rnums (Nrefs)) 737 then 738 Nrefs := Nrefs + 1; 739 Rnums (Nrefs) := Rnums (Index); 740 end if; 741 end loop; 742 end if; 743 744 -- Eliminate the reference if it is at the same location as the previous 745 -- one, unless it is a read-reference indicating that the entity is an 746 -- in-out actual in a call. 747 748 Ref_Count := Nrefs; 749 Nrefs := 0; 750 Loc := No_Location; 751 Prev_Typ := 'm'; 752 753 for Index in 1 .. Ref_Count loop 754 declare 755 Ref : Xref_Key renames Xrefs.Table (Rnums (Index)).Key; 756 757 begin 758 if Ref.Loc /= Loc 759 or else (Prev_Typ = 'm' and then Ref.Typ = 'r') 760 then 761 Loc := Ref.Loc; 762 Prev_Typ := Ref.Typ; 763 Nrefs := Nrefs + 1; 764 Rnums (Nrefs) := Rnums (Index); 765 end if; 766 end; 767 end loop; 768 769 -- The two steps have eliminated all references, nothing to do 770 771 if SPARK_Scope_Table.Last = 0 then 772 return; 773 end if; 774 775 Ref_Id := Empty; 776 Scope_Id := 1; 777 From_Index := 1; 778 779 -- Loop to output references 780 781 for Refno in 1 .. Nrefs loop 782 declare 783 Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); 784 Ref : Xref_Key renames Ref_Entry.Key; 785 Typ : Character; 786 787 begin 788 -- If this assertion fails, the scope which we are looking for is 789 -- not in SPARK scope table, which reveals either a problem in the 790 -- construction of the scope table, or an erroneous scope for the 791 -- current cross-reference. 792 793 pragma Assert (Is_Future_Scope_Entity (Ref.Ent_Scope, Scope_Id)); 794 795 -- Update the range of cross references to which the current scope 796 -- refers to. This may be the empty range only for the first scope 797 -- considered. 798 799 if Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) then 800 Update_Scope_Range 801 (S => Scope_Id, 802 From => From_Index, 803 To => SPARK_Xref_Table.Last); 804 805 From_Index := SPARK_Xref_Table.Last + 1; 806 end if; 807 808 while Ref.Ent_Scope /= Entity_Of_Scope (Scope_Id) loop 809 Scope_Id := Scope_Id + 1; 810 pragma Assert (Scope_Id <= SPARK_Scope_Table.Last); 811 end loop; 812 813 if Ref.Ent /= Ref_Id then 814 Ref_Name := new String'(Unique_Name (Ref.Ent)); 815 end if; 816 817 if Ref.Ent = Heap then 818 Line := 0; 819 Col := 0; 820 else 821 Line := Int (Get_Logical_Line_Number (Ref_Entry.Def)); 822 Col := Int (Get_Column_Number (Ref_Entry.Def)); 823 end if; 824 825 -- References to constant objects are considered specially in 826 -- SPARK section, because these will be translated as constants in 827 -- the intermediate language for formal verification, and should 828 -- therefore never appear in frame conditions. 829 830 if Is_Constant_Object (Ref.Ent) then 831 Typ := 'c'; 832 else 833 Typ := Ref.Typ; 834 end if; 835 836 SPARK_Xref_Table.Append ( 837 (Entity_Name => Ref_Name, 838 Entity_Line => Line, 839 Etype => Get_Entity_Type (Ref.Ent), 840 Entity_Col => Col, 841 File_Num => Dependency_Num (Ref.Lun), 842 Scope_Num => Get_Scope_Num (Ref.Ref_Scope), 843 Line => Int (Get_Logical_Line_Number (Ref.Loc)), 844 Rtype => Typ, 845 Col => Int (Get_Column_Number (Ref.Loc)))); 846 end; 847 end loop; 848 849 -- Update the range of cross references to which the scope refers to 850 851 Update_Scope_Range 852 (S => Scope_Id, 853 From => From_Index, 854 To => SPARK_Xref_Table.Last); 855 end Add_SPARK_Xrefs; 856 857 ------------------------- 858 -- Collect_SPARK_Xrefs -- 859 ------------------------- 860 861 procedure Collect_SPARK_Xrefs 862 (Sdep_Table : Unit_Ref_Table; 863 Num_Sdep : Nat) 864 is 865 D1 : Nat; 866 D2 : Nat; 867 868 begin 869 -- Cross-references should have been computed first 870 871 pragma Assert (Xrefs.Last /= 0); 872 873 Initialize_SPARK_Tables; 874 875 -- Generate file and scope SPARK cross-reference information 876 877 D1 := 1; 878 while D1 <= Num_Sdep loop 879 880 -- In rare cases, when treating the library-level instantiation of a 881 -- generic, two consecutive units refer to the same compilation unit 882 -- node and entity. In that case, treat them as a single unit for the 883 -- sake of SPARK cross references by passing to Add_SPARK_File. 884 885 if D1 < Num_Sdep 886 and then Cunit_Entity (Sdep_Table (D1)) = 887 Cunit_Entity (Sdep_Table (D1 + 1)) 888 then 889 D2 := D1 + 1; 890 else 891 D2 := D1; 892 end if; 893 894 Add_SPARK_File 895 (Ubody => Sdep_Table (D1), 896 Uspec => Sdep_Table (D2), 897 Dspec => D2); 898 D1 := D2 + 1; 899 end loop; 900 901 -- Fill in the spec information when relevant 902 903 declare 904 package Entity_Hash_Table is new 905 GNAT.HTable.Simple_HTable 906 (Header_Num => Entity_Hashed_Range, 907 Element => Scope_Index, 908 No_Element => 0, 909 Key => Entity_Id, 910 Hash => Entity_Hash, 911 Equal => "="); 912 913 begin 914 -- Fill in the hash-table 915 916 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 917 declare 918 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); 919 begin 920 Entity_Hash_Table.Set (Srec.Scope_Entity, S); 921 end; 922 end loop; 923 924 -- Use the hash-table to locate spec entities 925 926 for S in SPARK_Scope_Table.First .. SPARK_Scope_Table.Last loop 927 declare 928 Srec : SPARK_Scope_Record renames SPARK_Scope_Table.Table (S); 929 930 Spec_Entity : constant Entity_Id := 931 Unique_Entity (Srec.Scope_Entity); 932 Spec_Scope : constant Scope_Index := 933 Entity_Hash_Table.Get (Spec_Entity); 934 935 begin 936 -- Generic spec may be missing in which case Spec_Scope is zero 937 938 if Spec_Entity /= Srec.Scope_Entity 939 and then Spec_Scope /= 0 940 then 941 Srec.Spec_File_Num := 942 SPARK_Scope_Table.Table (Spec_Scope).File_Num; 943 Srec.Spec_Scope_Num := 944 SPARK_Scope_Table.Table (Spec_Scope).Scope_Num; 945 end if; 946 end; 947 end loop; 948 end; 949 950 -- Generate SPARK cross-reference information 951 952 Add_SPARK_Xrefs; 953 end Collect_SPARK_Xrefs; 954 955 -------------------------------- 956 -- Detect_And_Add_SPARK_Scope -- 957 -------------------------------- 958 959 procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is 960 begin 961 if Nkind_In (N, N_Subprogram_Declaration, 962 N_Subprogram_Body, 963 N_Subprogram_Body_Stub, 964 N_Package_Declaration, 965 N_Package_Body) 966 then 967 Add_SPARK_Scope (N); 968 end if; 969 end Detect_And_Add_SPARK_Scope; 970 971 ------------------------------------- 972 -- Enclosing_Subprogram_Or_Package -- 973 ------------------------------------- 974 975 function Enclosing_Subprogram_Or_Package (N : Node_Id) return Entity_Id is 976 Result : Entity_Id; 977 978 begin 979 -- If N is the defining identifier for a subprogram, then return the 980 -- enclosing subprogram or package, not this subprogram. 981 982 if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) 983 and then Nkind (Parent (N)) in N_Subprogram_Specification 984 then 985 Result := Parent (Parent (Parent (N))); 986 else 987 Result := N; 988 end if; 989 990 while Present (Result) loop 991 case Nkind (Result) is 992 when N_Package_Specification => 993 Result := Defining_Unit_Name (Result); 994 exit; 995 996 when N_Package_Body => 997 Result := Defining_Unit_Name (Result); 998 exit; 999 1000 when N_Subprogram_Specification => 1001 Result := Defining_Unit_Name (Result); 1002 exit; 1003 1004 when N_Subprogram_Declaration => 1005 Result := Defining_Unit_Name (Specification (Result)); 1006 exit; 1007 1008 when N_Subprogram_Body => 1009 Result := Defining_Unit_Name (Specification (Result)); 1010 exit; 1011 1012 when N_Pragma => 1013 1014 -- The enclosing subprogram for a precondition, postcondition, 1015 -- or contract case should be the declaration preceding the 1016 -- pragma (skipping any other pragmas between this pragma and 1017 -- this declaration. 1018 1019 while Nkind (Result) = N_Pragma 1020 and then Is_List_Member (Result) 1021 and then Present (Prev (Result)) 1022 loop 1023 Result := Prev (Result); 1024 end loop; 1025 1026 if Nkind (Result) = N_Pragma then 1027 Result := Parent (Result); 1028 end if; 1029 1030 when others => 1031 Result := Parent (Result); 1032 end case; 1033 end loop; 1034 1035 if Nkind (Result) = N_Defining_Program_Unit_Name then 1036 Result := Defining_Identifier (Result); 1037 end if; 1038 1039 -- Do not return a scope without a proper location 1040 1041 if Present (Result) 1042 and then Sloc (Result) = No_Location 1043 then 1044 return Empty; 1045 end if; 1046 1047 return Result; 1048 end Enclosing_Subprogram_Or_Package; 1049 1050 ----------------- 1051 -- Entity_Hash -- 1052 ----------------- 1053 1054 function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range is 1055 begin 1056 return 1057 Entity_Hashed_Range (E mod (Entity_Id (Entity_Hashed_Range'Last) + 1)); 1058 end Entity_Hash; 1059 1060 -------------------------- 1061 -- Generate_Dereference -- 1062 -------------------------- 1063 1064 procedure Generate_Dereference 1065 (N : Node_Id; 1066 Typ : Character := 'r') 1067 is 1068 procedure Create_Heap; 1069 -- Create and decorate the special entity which denotes the heap 1070 1071 ----------------- 1072 -- Create_Heap -- 1073 ----------------- 1074 1075 procedure Create_Heap is 1076 begin 1077 Name_Len := Name_Of_Heap_Variable'Length; 1078 Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable; 1079 1080 Heap := Make_Defining_Identifier (Standard_Location, Name_Enter); 1081 1082 Set_Ekind (Heap, E_Variable); 1083 Set_Is_Internal (Heap, True); 1084 Set_Has_Fully_Qualified_Name (Heap); 1085 end Create_Heap; 1086 1087 -- Local variables 1088 1089 Loc : constant Source_Ptr := Sloc (N); 1090 Index : Nat; 1091 Ref_Scope : Entity_Id; 1092 1093 -- Start of processing for Generate_Dereference 1094 1095 begin 1096 1097 if Loc > No_Location then 1098 Drefs.Increment_Last; 1099 Index := Drefs.Last; 1100 1101 declare 1102 Deref_Entry : Xref_Entry renames Drefs.Table (Index); 1103 Deref : Xref_Key renames Deref_Entry.Key; 1104 1105 begin 1106 if No (Heap) then 1107 Create_Heap; 1108 end if; 1109 1110 Ref_Scope := Enclosing_Subprogram_Or_Package (N); 1111 1112 Deref.Ent := Heap; 1113 Deref.Loc := Loc; 1114 Deref.Typ := Typ; 1115 1116 -- It is as if the special "Heap" was defined in every scope where 1117 -- it is referenced. 1118 1119 Deref.Eun := Get_Code_Unit (Loc); 1120 Deref.Lun := Get_Code_Unit (Loc); 1121 1122 Deref.Ref_Scope := Ref_Scope; 1123 Deref.Ent_Scope := Ref_Scope; 1124 1125 Deref_Entry.Def := No_Location; 1126 1127 Deref_Entry.Ent_Scope_File := Get_Code_Unit (N); 1128 end; 1129 end if; 1130 end Generate_Dereference; 1131 1132 ------------------------------------ 1133 -- Traverse_All_Compilation_Units -- 1134 ------------------------------------ 1135 1136 procedure Traverse_All_Compilation_Units (Process : Node_Processing) is 1137 begin 1138 for U in Units.First .. Last_Unit loop 1139 Traverse_Compilation_Unit (Cunit (U), Process, Inside_Stubs => False); 1140 end loop; 1141 end Traverse_All_Compilation_Units; 1142 1143 ------------------------------- 1144 -- Traverse_Compilation_Unit -- 1145 ------------------------------- 1146 1147 procedure Traverse_Compilation_Unit 1148 (CU : Node_Id; 1149 Process : Node_Processing; 1150 Inside_Stubs : Boolean) 1151 is 1152 Lu : Node_Id; 1153 1154 begin 1155 -- Get Unit (checking case of subunit) 1156 1157 Lu := Unit (CU); 1158 1159 if Nkind (Lu) = N_Subunit then 1160 Lu := Proper_Body (Lu); 1161 end if; 1162 1163 -- Do not add scopes for generic units 1164 1165 if Nkind (Lu) = N_Package_Body 1166 and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind 1167 then 1168 return; 1169 end if; 1170 1171 -- Call Process on all declarations 1172 1173 if Nkind (Lu) in N_Declaration 1174 or else Nkind (Lu) in N_Later_Decl_Item 1175 then 1176 Process (Lu); 1177 end if; 1178 1179 -- Traverse the unit 1180 1181 if Nkind (Lu) = N_Subprogram_Body then 1182 Traverse_Subprogram_Body (Lu, Process, Inside_Stubs); 1183 1184 elsif Nkind (Lu) = N_Subprogram_Declaration then 1185 null; 1186 1187 elsif Nkind (Lu) = N_Package_Declaration then 1188 Traverse_Package_Declaration (Lu, Process, Inside_Stubs); 1189 1190 elsif Nkind (Lu) = N_Package_Body then 1191 Traverse_Package_Body (Lu, Process, Inside_Stubs); 1192 1193 -- All other cases of compilation units (e.g. renamings), are not 1194 -- declarations, or else generic declarations which are ignored. 1195 1196 else 1197 null; 1198 end if; 1199 end Traverse_Compilation_Unit; 1200 1201 ----------------------------------------- 1202 -- Traverse_Declarations_Or_Statements -- 1203 ----------------------------------------- 1204 1205 procedure Traverse_Declarations_Or_Statements 1206 (L : List_Id; 1207 Process : Node_Processing; 1208 Inside_Stubs : Boolean) 1209 is 1210 N : Node_Id; 1211 1212 begin 1213 -- Loop through statements or declarations 1214 1215 N := First (L); 1216 while Present (N) loop 1217 -- Call Process on all declarations 1218 1219 if Nkind (N) in N_Declaration 1220 or else 1221 Nkind (N) in N_Later_Decl_Item 1222 then 1223 Process (N); 1224 end if; 1225 1226 case Nkind (N) is 1227 1228 -- Package declaration 1229 1230 when N_Package_Declaration => 1231 Traverse_Package_Declaration (N, Process, Inside_Stubs); 1232 1233 -- Package body 1234 1235 when N_Package_Body => 1236 if Ekind (Defining_Entity (N)) /= E_Generic_Package then 1237 Traverse_Package_Body (N, Process, Inside_Stubs); 1238 end if; 1239 1240 when N_Package_Body_Stub => 1241 if Present (Library_Unit (N)) then 1242 declare 1243 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1244 begin 1245 if Inside_Stubs 1246 and then 1247 Ekind (Defining_Entity (Body_N)) /= E_Generic_Package 1248 then 1249 Traverse_Package_Body (Body_N, Process, Inside_Stubs); 1250 end if; 1251 end; 1252 end if; 1253 1254 -- Subprogram declaration 1255 1256 when N_Subprogram_Declaration => 1257 null; 1258 1259 -- Subprogram body 1260 1261 when N_Subprogram_Body => 1262 if not Is_Generic_Subprogram (Defining_Entity (N)) then 1263 Traverse_Subprogram_Body (N, Process, Inside_Stubs); 1264 end if; 1265 1266 when N_Subprogram_Body_Stub => 1267 if Present (Library_Unit (N)) then 1268 declare 1269 Body_N : constant Node_Id := Get_Body_From_Stub (N); 1270 begin 1271 if Inside_Stubs 1272 and then 1273 not Is_Generic_Subprogram (Defining_Entity (Body_N)) 1274 then 1275 Traverse_Subprogram_Body 1276 (Body_N, Process, Inside_Stubs); 1277 end if; 1278 end; 1279 end if; 1280 1281 -- Block statement 1282 1283 when N_Block_Statement => 1284 Traverse_Declarations_Or_Statements 1285 (Declarations (N), Process, Inside_Stubs); 1286 Traverse_Handled_Statement_Sequence 1287 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1288 1289 when N_If_Statement => 1290 1291 -- Traverse the statements in the THEN part 1292 1293 Traverse_Declarations_Or_Statements 1294 (Then_Statements (N), Process, Inside_Stubs); 1295 1296 -- Loop through ELSIF parts if present 1297 1298 if Present (Elsif_Parts (N)) then 1299 declare 1300 Elif : Node_Id := First (Elsif_Parts (N)); 1301 1302 begin 1303 while Present (Elif) loop 1304 Traverse_Declarations_Or_Statements 1305 (Then_Statements (Elif), Process, Inside_Stubs); 1306 Next (Elif); 1307 end loop; 1308 end; 1309 end if; 1310 1311 -- Finally traverse the ELSE statements if present 1312 1313 Traverse_Declarations_Or_Statements 1314 (Else_Statements (N), Process, Inside_Stubs); 1315 1316 -- Case statement 1317 1318 when N_Case_Statement => 1319 1320 -- Process case branches 1321 1322 declare 1323 Alt : Node_Id; 1324 begin 1325 Alt := First (Alternatives (N)); 1326 while Present (Alt) loop 1327 Traverse_Declarations_Or_Statements 1328 (Statements (Alt), Process, Inside_Stubs); 1329 Next (Alt); 1330 end loop; 1331 end; 1332 1333 -- Extended return statement 1334 1335 when N_Extended_Return_Statement => 1336 Traverse_Handled_Statement_Sequence 1337 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1338 1339 -- Loop 1340 1341 when N_Loop_Statement => 1342 Traverse_Declarations_Or_Statements 1343 (Statements (N), Process, Inside_Stubs); 1344 1345 -- Generic declarations are ignored 1346 1347 when others => 1348 null; 1349 end case; 1350 1351 Next (N); 1352 end loop; 1353 end Traverse_Declarations_Or_Statements; 1354 1355 ----------------------------------------- 1356 -- Traverse_Handled_Statement_Sequence -- 1357 ----------------------------------------- 1358 1359 procedure Traverse_Handled_Statement_Sequence 1360 (N : Node_Id; 1361 Process : Node_Processing; 1362 Inside_Stubs : Boolean) 1363 is 1364 Handler : Node_Id; 1365 1366 begin 1367 if Present (N) then 1368 Traverse_Declarations_Or_Statements 1369 (Statements (N), Process, Inside_Stubs); 1370 1371 if Present (Exception_Handlers (N)) then 1372 Handler := First (Exception_Handlers (N)); 1373 while Present (Handler) loop 1374 Traverse_Declarations_Or_Statements 1375 (Statements (Handler), Process, Inside_Stubs); 1376 Next (Handler); 1377 end loop; 1378 end if; 1379 end if; 1380 end Traverse_Handled_Statement_Sequence; 1381 1382 --------------------------- 1383 -- Traverse_Package_Body -- 1384 --------------------------- 1385 1386 procedure Traverse_Package_Body 1387 (N : Node_Id; 1388 Process : Node_Processing; 1389 Inside_Stubs : Boolean) is 1390 begin 1391 Traverse_Declarations_Or_Statements 1392 (Declarations (N), Process, Inside_Stubs); 1393 Traverse_Handled_Statement_Sequence 1394 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1395 end Traverse_Package_Body; 1396 1397 ---------------------------------- 1398 -- Traverse_Package_Declaration -- 1399 ---------------------------------- 1400 1401 procedure Traverse_Package_Declaration 1402 (N : Node_Id; 1403 Process : Node_Processing; 1404 Inside_Stubs : Boolean) 1405 is 1406 Spec : constant Node_Id := Specification (N); 1407 begin 1408 Traverse_Declarations_Or_Statements 1409 (Visible_Declarations (Spec), Process, Inside_Stubs); 1410 Traverse_Declarations_Or_Statements 1411 (Private_Declarations (Spec), Process, Inside_Stubs); 1412 end Traverse_Package_Declaration; 1413 1414 ------------------------------ 1415 -- Traverse_Subprogram_Body -- 1416 ------------------------------ 1417 1418 procedure Traverse_Subprogram_Body 1419 (N : Node_Id; 1420 Process : Node_Processing; 1421 Inside_Stubs : Boolean) 1422 is 1423 begin 1424 Traverse_Declarations_Or_Statements 1425 (Declarations (N), Process, Inside_Stubs); 1426 Traverse_Handled_Statement_Sequence 1427 (Handled_Statement_Sequence (N), Process, Inside_Stubs); 1428 end Traverse_Subprogram_Body; 1429 1430end SPARK_Specific; 1431