1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- E X P _ S P A R K -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 1992-2020, 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 Checks; use Checks; 28with Einfo; use Einfo; 29with Exp_Attr; 30with Exp_Ch4; 31with Exp_Ch5; use Exp_Ch5; 32with Exp_Dbug; use Exp_Dbug; 33with Exp_Util; use Exp_Util; 34with Namet; use Namet; 35with Nlists; use Nlists; 36with Nmake; use Nmake; 37with Rtsfind; use Rtsfind; 38with Sem; use Sem; 39with Sem_Ch8; use Sem_Ch8; 40with Sem_Prag; use Sem_Prag; 41with Sem_Res; use Sem_Res; 42with Sem_Util; use Sem_Util; 43with Sinfo; use Sinfo; 44with Snames; use Snames; 45with Stand; use Stand; 46with Tbuild; use Tbuild; 47with Uintp; use Uintp; 48 49package body Exp_SPARK is 50 51 ----------------------- 52 -- Local Subprograms -- 53 ----------------------- 54 55 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id); 56 -- Perform attribute-reference-specific expansion 57 58 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id); 59 -- Perform delta-aggregate-specific expansion 60 61 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id); 62 -- Build the DIC procedure of a type when needed, if not already done 63 64 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id); 65 -- Perform loop-statement-specific expansion 66 67 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); 68 -- Perform object-declaration-specific expansion 69 70 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id); 71 -- Perform name evaluation for a renamed object 72 73 procedure Expand_SPARK_N_Op_Ne (N : Node_Id); 74 -- Rewrite operator /= based on operator = when defined explicitly 75 76 procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id); 77 -- Common expansion for attribute Update and delta aggregates 78 79 ------------------ 80 -- Expand_SPARK -- 81 ------------------ 82 83 procedure Expand_SPARK (N : Node_Id) is 84 begin 85 case Nkind (N) is 86 87 -- Qualification of entity names in formal verification mode 88 -- is limited to the addition of a suffix for homonyms (see 89 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names 90 -- as full expansion does, but this was removed as this prevents the 91 -- verification back-end from using a short name for debugging and 92 -- user interaction. The verification back-end already takes care 93 -- of qualifying names when needed. 94 95 when N_Block_Statement 96 | N_Entry_Declaration 97 | N_Package_Body 98 | N_Package_Declaration 99 | N_Protected_Type_Declaration 100 | N_Subprogram_Body 101 | N_Task_Type_Declaration 102 => 103 Qualify_Entity_Names (N); 104 105 -- Replace occurrences of System'To_Address by calls to 106 -- System.Storage_Elements.To_Address. 107 108 when N_Attribute_Reference => 109 Expand_SPARK_N_Attribute_Reference (N); 110 111 when N_Delta_Aggregate => 112 Expand_SPARK_N_Delta_Aggregate (N); 113 114 when N_Expanded_Name 115 | N_Identifier 116 => 117 Expand_SPARK_Potential_Renaming (N); 118 119 -- Loop iterations over arrays need to be expanded, to avoid getting 120 -- two names referring to the same object in memory (the array and 121 -- the iterator) in GNATprove, especially since both can be written 122 -- (thus possibly leading to interferences due to aliasing). No such 123 -- problem arises with quantified expressions over arrays, which are 124 -- dealt with specially in GNATprove. 125 126 when N_Loop_Statement => 127 Expand_SPARK_N_Loop_Statement (N); 128 129 when N_Object_Declaration => 130 Expand_SPARK_N_Object_Declaration (N); 131 132 when N_Object_Renaming_Declaration => 133 Expand_SPARK_N_Object_Renaming_Declaration (N); 134 135 when N_Op_Ne => 136 Expand_SPARK_N_Op_Ne (N); 137 138 when N_Freeze_Entity => 139 if Is_Type (Entity (N)) then 140 Expand_SPARK_N_Freeze_Type (Entity (N)); 141 end if; 142 143 -- In SPARK mode, no other constructs require expansion 144 145 when others => 146 null; 147 end case; 148 end Expand_SPARK; 149 150 ---------------------------------- 151 -- Expand_SPARK_Delta_Or_Update -- 152 ---------------------------------- 153 154 procedure Expand_SPARK_Delta_Or_Update 155 (Typ : Entity_Id; 156 Aggr : Node_Id) 157 is 158 Assoc : Node_Id; 159 Comp : Node_Id; 160 Comp_Id : Entity_Id; 161 Comp_Type : Entity_Id; 162 Expr : Node_Id; 163 Index : Node_Id; 164 Index_Typ : Entity_Id; 165 New_Assoc : Node_Id; 166 167 begin 168 -- Apply scalar range checks on the updated components, if needed 169 170 if Is_Array_Type (Typ) then 171 172 -- Multidimensional arrays 173 174 if Present (Next_Index (First_Index (Typ))) then 175 Assoc := First (Component_Associations (Aggr)); 176 177 while Present (Assoc) loop 178 Expr := Expression (Assoc); 179 Comp_Type := Component_Type (Typ); 180 181 if Is_Scalar_Type (Comp_Type) then 182 Apply_Scalar_Range_Check (Expr, Comp_Type); 183 end if; 184 185 -- The current association contains a sequence of indexes 186 -- denoting an element of a multidimensional array: 187 -- 188 -- (Index_1, ..., Index_N) 189 190 Expr := First (Choices (Assoc)); 191 192 pragma Assert (Nkind (Aggr) = N_Aggregate); 193 194 while Present (Expr) loop 195 Index := First (Expressions (Expr)); 196 Index_Typ := First_Index (Typ); 197 198 while Present (Index_Typ) loop 199 Apply_Scalar_Range_Check (Index, Etype (Index_Typ)); 200 Next (Index); 201 Next_Index (Index_Typ); 202 end loop; 203 204 Next (Expr); 205 end loop; 206 207 Next (Assoc); 208 end loop; 209 210 -- One-dimensional arrays 211 212 else 213 Assoc := First (Component_Associations (Aggr)); 214 215 while Present (Assoc) loop 216 Expr := Expression (Assoc); 217 Comp_Type := Component_Type (Typ); 218 219 -- Analyze expression of the iterated_component_association 220 -- with its index parameter in scope. 221 222 if Nkind (Assoc) = N_Iterated_Component_Association then 223 Push_Scope (Scope (Defining_Identifier (Assoc))); 224 Enter_Name (Defining_Identifier (Assoc)); 225 Analyze_And_Resolve (Expr, Comp_Type); 226 end if; 227 228 if Is_Scalar_Type (Comp_Type) then 229 Apply_Scalar_Range_Check (Expr, Comp_Type); 230 end if; 231 232 -- Restore scope of the iterated_component_association 233 234 if Nkind (Assoc) = N_Iterated_Component_Association then 235 End_Scope; 236 end if; 237 238 Index := First (Choice_List (Assoc)); 239 Index_Typ := First_Index (Typ); 240 241 while Present (Index) loop 242 -- If the index denotes a range of elements or a constrained 243 -- subtype indication, then their low and high bounds 244 -- already have range checks applied. 245 246 if Nkind (Index) in N_Range | N_Subtype_Indication then 247 null; 248 249 -- Otherwise the index denotes a single expression where 250 -- range checks need to be applied or a subtype name 251 -- (without range constraints) where applying checks is 252 -- harmless. 253 -- 254 -- In delta_aggregate and Update attribute on array the 255 -- others_choice is not allowed. 256 257 else pragma Assert (Nkind (Index) in N_Subexpr); 258 Apply_Scalar_Range_Check (Index, Etype (Index_Typ)); 259 end if; 260 261 Next (Index); 262 end loop; 263 264 Next (Assoc); 265 end loop; 266 end if; 267 268 else pragma Assert (Is_Record_Type (Typ)); 269 270 -- If the aggregate has multiple component choices, e.g.: 271 -- 272 -- X'Update (A | B | C => 123) 273 -- 274 -- then each component might be of a different type and might or 275 -- might not require a range check. We first rewrite associations 276 -- into single-component choices, e.g.: 277 -- 278 -- X'Update (A => 123, B => 123, C => 123) 279 -- 280 -- and then apply range checks to individual copies of the 281 -- expressions. We do the same for delta aggregates, accordingly. 282 283 -- Iterate over associations of the original aggregate 284 285 Assoc := First (Component_Associations (Aggr)); 286 287 -- Rewrite into a new aggregate and decorate 288 289 case Nkind (Aggr) is 290 when N_Aggregate => 291 Rewrite 292 (Aggr, 293 Make_Aggregate 294 (Sloc => Sloc (Aggr), 295 Component_Associations => New_List)); 296 297 when N_Delta_Aggregate => 298 Rewrite 299 (Aggr, 300 Make_Delta_Aggregate 301 (Sloc => Sloc (Aggr), 302 Expression => Expression (Aggr), 303 Component_Associations => New_List)); 304 305 when others => 306 raise Program_Error; 307 end case; 308 309 Set_Etype (Aggr, Typ); 310 311 -- Populate the new aggregate with component associations 312 313 while Present (Assoc) loop 314 Expr := Expression (Assoc); 315 Comp := First (Choices (Assoc)); 316 317 while Present (Comp) loop 318 Comp_Id := Entity (Comp); 319 Comp_Type := Etype (Comp_Id); 320 321 New_Assoc := 322 Make_Component_Association 323 (Sloc => Sloc (Assoc), 324 Choices => 325 New_List 326 (New_Occurrence_Of (Comp_Id, Sloc (Comp))), 327 Expression => New_Copy_Tree (Expr)); 328 329 -- New association must be attached to the aggregate before we 330 -- analyze it. 331 332 Append (New_Assoc, Component_Associations (Aggr)); 333 334 Analyze_And_Resolve (Expression (New_Assoc), Comp_Type); 335 336 if Is_Scalar_Type (Comp_Type) then 337 Apply_Scalar_Range_Check 338 (Expression (New_Assoc), Comp_Type); 339 end if; 340 341 Next (Comp); 342 end loop; 343 344 Next (Assoc); 345 end loop; 346 end if; 347 end Expand_SPARK_Delta_Or_Update; 348 349 -------------------------------- 350 -- Expand_SPARK_N_Freeze_Type -- 351 -------------------------------- 352 353 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is 354 begin 355 -- When a DIC is inherited by a tagged type, it may need to be 356 -- specialized to the descendant type, hence build a separate DIC 357 -- procedure for it as done during regular expansion for compilation. 358 359 if Has_DIC (E) and then Is_Tagged_Type (E) then 360 -- Why is this needed for DIC, but not for other aspects (such as 361 -- Type_Invariant)??? 362 363 Build_DIC_Procedure_Body (E); 364 end if; 365 end Expand_SPARK_N_Freeze_Type; 366 367 ---------------------------------------- 368 -- Expand_SPARK_N_Attribute_Reference -- 369 ---------------------------------------- 370 371 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is 372 Aname : constant Name_Id := Attribute_Name (N); 373 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); 374 Loc : constant Source_Ptr := Sloc (N); 375 Pref : constant Node_Id := Prefix (N); 376 Typ : constant Entity_Id := Etype (N); 377 Expr : Node_Id; 378 379 begin 380 case Attr_Id is 381 when Attribute_To_Address => 382 383 -- Extract and convert argument to expected type for call 384 385 Expr := 386 Make_Type_Conversion (Loc, 387 Subtype_Mark => 388 New_Occurrence_Of (RTE (RE_Integer_Address), Loc), 389 Expression => Relocate_Node (First (Expressions (N)))); 390 391 -- Replace attribute reference with call 392 393 Rewrite 394 (N, 395 Make_Function_Call (Loc, 396 Name => 397 New_Occurrence_Of (RTE (RE_To_Address), Loc), 398 Parameter_Associations => New_List (Expr))); 399 Analyze_And_Resolve (N, Typ); 400 401 when Attribute_Object_Size 402 | Attribute_Size 403 | Attribute_Value_Size 404 | Attribute_VADS_Size 405 => 406 Exp_Attr.Expand_Size_Attribute (N); 407 408 -- For attributes which return Universal_Integer, introduce a 409 -- conversion to the expected type with the appropriate check flags 410 -- set. 411 412 when Attribute_Aft 413 | Attribute_Alignment 414 | Attribute_Bit 415 | Attribute_Bit_Position 416 | Attribute_Descriptor_Size 417 | Attribute_First_Bit 418 | Attribute_Last_Bit 419 | Attribute_Length 420 | Attribute_Max_Alignment_For_Allocation 421 | Attribute_Max_Size_In_Storage_Elements 422 | Attribute_Pos 423 | Attribute_Position 424 | Attribute_Range_Length 425 => 426 -- If the expected type is Long_Long_Integer, there will be no 427 -- check flag as the compiler assumes attributes always fit in 428 -- this type. Since in SPARK_Mode we do not take Storage_Error 429 -- into account, we cannot make this assumption and need to 430 -- produce a check. ??? It should be enough to add this check for 431 -- attributes 'Length, 'Range_Length and 'Pos when the type is as 432 -- big as Long_Long_Integer. 433 434 declare 435 Typ : Entity_Id; 436 begin 437 if Attr_Id in Attribute_Pos | Attribute_Range_Length then 438 Typ := Etype (Prefix (N)); 439 440 elsif Attr_Id = Attribute_Length then 441 Typ := Get_Index_Subtype (N); 442 443 else 444 Typ := Empty; 445 end if; 446 447 Apply_Universal_Integer_Attribute_Checks (N); 448 449 if Present (Typ) 450 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer) 451 then 452 -- ??? This should rather be a range check, but this would 453 -- crash GNATprove which somehow recovers the proper kind 454 -- of check anyway. 455 Set_Do_Overflow_Check (N); 456 end if; 457 end; 458 459 when Attribute_Constrained => 460 461 -- If the prefix is an access to object, the attribute applies to 462 -- the designated object, so rewrite with an explicit dereference. 463 464 if Is_Access_Type (Etype (Pref)) 465 and then 466 (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref))) 467 then 468 Rewrite (Pref, 469 Make_Explicit_Dereference (Loc, Relocate_Node (Pref))); 470 Analyze_And_Resolve (N, Standard_Boolean); 471 end if; 472 473 when Attribute_Update => 474 Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N))); 475 476 when others => 477 null; 478 end case; 479 end Expand_SPARK_N_Attribute_Reference; 480 481 ------------------------------------ 482 -- Expand_SPARK_N_Delta_Aggregate -- 483 ------------------------------------ 484 485 procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is 486 begin 487 Expand_SPARK_Delta_Or_Update (Etype (N), N); 488 end Expand_SPARK_N_Delta_Aggregate; 489 490 ----------------------------------- 491 -- Expand_SPARK_N_Loop_Statement -- 492 ----------------------------------- 493 494 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is 495 Scheme : constant Node_Id := Iteration_Scheme (N); 496 497 begin 498 -- Loop iterations over arrays need to be expanded, to avoid getting 499 -- two names referring to the same object in memory (the array and the 500 -- iterator) in GNATprove, especially since both can be written (thus 501 -- possibly leading to interferences due to aliasing). No such problem 502 -- arises with quantified expressions over arrays, which are dealt with 503 -- specially in GNATprove. 504 505 if Present (Scheme) 506 and then Present (Iterator_Specification (Scheme)) 507 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme)) 508 then 509 Expand_Iterator_Loop_Over_Array (N); 510 end if; 511 end Expand_SPARK_N_Loop_Statement; 512 513 --------------------------------------- 514 -- Expand_SPARK_N_Object_Declaration -- 515 --------------------------------------- 516 517 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is 518 Loc : constant Source_Ptr := Sloc (N); 519 Obj_Id : constant Entity_Id := Defining_Identifier (N); 520 Typ : constant Entity_Id := Etype (Obj_Id); 521 522 Call : Node_Id; 523 524 begin 525 -- If the object declaration denotes a variable without initialization 526 -- whose type is subject to pragma Default_Initial_Condition, create 527 -- and analyze a dummy call to the DIC procedure of the type in order 528 -- to detect potential elaboration issues. 529 530 if Comes_From_Source (Obj_Id) 531 and then Ekind (Obj_Id) = E_Variable 532 and then Has_DIC (Typ) 533 and then Present (DIC_Procedure (Typ)) 534 and then not Has_Init_Expression (N) 535 then 536 Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ); 537 538 -- Partially insert the call into the tree by setting its parent 539 -- pointer. 540 541 Set_Parent (Call, N); 542 Analyze (Call); 543 end if; 544 end Expand_SPARK_N_Object_Declaration; 545 546 ------------------------------------------------ 547 -- Expand_SPARK_N_Object_Renaming_Declaration -- 548 ------------------------------------------------ 549 550 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is 551 CFS : constant Boolean := Comes_From_Source (N); 552 Loc : constant Source_Ptr := Sloc (N); 553 Obj_Id : constant Entity_Id := Defining_Entity (N); 554 Nam : constant Node_Id := Name (N); 555 Typ : constant Entity_Id := Etype (Obj_Id); 556 557 begin 558 -- Transform a renaming of the form 559 560 -- Obj_Id : <subtype mark> renames <function call>; 561 562 -- into 563 564 -- Obj_Id : constant <subtype mark> := <function call>; 565 566 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces 567 -- a temporary to capture the function result. Once potential renamings 568 -- are rewritten for SPARK, the temporary may be leaked out into source 569 -- constructs and lead to confusing error diagnostics. Using an object 570 -- declaration prevents this unwanted side effect. 571 572 if Nkind (Nam) = N_Function_Call then 573 Rewrite (N, 574 Make_Object_Declaration (Loc, 575 Defining_Identifier => Obj_Id, 576 Constant_Present => True, 577 Object_Definition => New_Occurrence_Of (Typ, Loc), 578 Expression => Nam)); 579 580 -- Inherit the original Comes_From_Source status of the renaming 581 582 Set_Comes_From_Source (N, CFS); 583 584 -- Sever the link to the renamed function result because the entity 585 -- will no longer alias anything. 586 587 Set_Renamed_Object (Obj_Id, Empty); 588 589 -- Remove the entity of the renaming declaration from visibility as 590 -- the analysis of the object declaration will reintroduce it again. 591 592 Remove_Entity_And_Homonym (Obj_Id); 593 Analyze (N); 594 595 -- Otherwise unconditionally remove all side effects from the name 596 597 else 598 Evaluate_Name (Nam); 599 end if; 600 end Expand_SPARK_N_Object_Renaming_Declaration; 601 602 -------------------------- 603 -- Expand_SPARK_N_Op_Ne -- 604 -------------------------- 605 606 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is 607 Typ : constant Entity_Id := Etype (Left_Opnd (N)); 608 609 begin 610 -- Case of elementary type with standard operator 611 612 if Is_Elementary_Type (Typ) 613 and then Sloc (Entity (N)) = Standard_Location 614 then 615 null; 616 617 else 618 Exp_Ch4.Expand_N_Op_Ne (N); 619 end if; 620 end Expand_SPARK_N_Op_Ne; 621 622 ------------------------------------- 623 -- Expand_SPARK_Potential_Renaming -- 624 ------------------------------------- 625 626 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is 627 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean; 628 -- Determine whether arbitrary node Nod appears within a significant 629 -- pragma for SPARK. 630 631 ----------------------------- 632 -- In_Insignificant_Pragma -- 633 ----------------------------- 634 635 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is 636 Par : Node_Id; 637 638 begin 639 -- Climb the parent chain looking for an enclosing pragma 640 641 Par := Nod; 642 while Present (Par) loop 643 if Nkind (Par) = N_Pragma then 644 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par)); 645 646 -- Prevent the search from going too far 647 648 elsif Is_Body_Or_Package_Declaration (Par) then 649 exit; 650 end if; 651 652 Par := Parent (Par); 653 end loop; 654 655 return False; 656 end In_Insignificant_Pragma; 657 658 -- Local variables 659 660 Loc : constant Source_Ptr := Sloc (N); 661 Obj_Id : constant Entity_Id := Entity (N); 662 Typ : constant Entity_Id := Etype (N); 663 Ren : Node_Id; 664 665 -- Start of processing for Expand_SPARK_Potential_Renaming 666 667 begin 668 -- Replace a reference to a renaming with the actual renamed object 669 670 if Is_Object (Obj_Id) then 671 Ren := Renamed_Object (Obj_Id); 672 673 if Present (Ren) then 674 675 -- Do not process a reference when it appears within a pragma of 676 -- no significance to SPARK. It is assumed that the replacement 677 -- will violate the semantics of the pragma and cause a spurious 678 -- error. 679 680 if In_Insignificant_Pragma (N) then 681 return; 682 683 -- Instantiations and inlining of subprograms employ "prologues" 684 -- which map actual to formal parameters by means of renamings. 685 -- Replace a reference to a formal by the corresponding actual 686 -- parameter. 687 688 elsif Nkind (Ren) in N_Entity then 689 Rewrite (N, New_Occurrence_Of (Ren, Loc)); 690 691 -- Otherwise the renamed object denotes a name 692 693 else 694 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc)); 695 Reset_Analyzed_Flags (N); 696 end if; 697 698 Analyze_And_Resolve (N, Typ); 699 end if; 700 end if; 701 end Expand_SPARK_Potential_Renaming; 702 703end Exp_SPARK; 704