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