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-2019, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- 17-- for more details. You should have received a copy of the GNU General -- 18-- Public License distributed with GNAT; see file COPYING3. If not, go to -- 19-- http://www.gnu.org/licenses for a complete copy of the license. -- 20-- -- 21-- GNAT was originally developed by the GNAT team at New York University. -- 22-- Extensive contributions were provided by Ada Core Technologies Inc. -- 23-- -- 24------------------------------------------------------------------------------ 25 26with Atree; use Atree; 27with 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_Eval; use Sem_Eval; 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 -- Replace occurrences of System'To_Address by calls to 57 -- System.Storage_Elements.To_Address 58 59 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id); 60 -- Build the DIC procedure of a type when needed, if not already done 61 62 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id); 63 -- Perform loop statement-specific expansion 64 65 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); 66 -- Perform object-declaration-specific expansion 67 68 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id); 69 -- Perform name evaluation for a renamed object 70 71 procedure Expand_SPARK_N_Op_Ne (N : Node_Id); 72 -- Rewrite operator /= based on operator = when defined explicitly 73 74 procedure Expand_SPARK_N_Selected_Component (N : Node_Id); 75 -- Insert explicit dereference if required 76 77 procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id); 78 -- Insert explicit dereference if required 79 80 ------------------ 81 -- Expand_SPARK -- 82 ------------------ 83 84 procedure Expand_SPARK (N : Node_Id) is 85 begin 86 case Nkind (N) is 87 88 -- Qualification of entity names in formal verification mode 89 -- is limited to the addition of a suffix for homonyms (see 90 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names 91 -- as full expansion does, but this was removed as this prevents the 92 -- verification back-end from using a short name for debugging and 93 -- user interaction. The verification back-end already takes care 94 -- of qualifying names when needed. 95 96 when N_Block_Statement 97 | N_Entry_Declaration 98 | N_Package_Body 99 | N_Package_Declaration 100 | N_Protected_Type_Declaration 101 | N_Subprogram_Body 102 | N_Task_Type_Declaration 103 => 104 Qualify_Entity_Names (N); 105 106 -- Replace occurrences of System'To_Address by calls to 107 -- System.Storage_Elements.To_Address. 108 109 when N_Attribute_Reference => 110 Expand_SPARK_N_Attribute_Reference (N); 111 112 when N_Expanded_Name 113 | N_Identifier 114 => 115 Expand_SPARK_Potential_Renaming (N); 116 117 -- Loop iterations over arrays need to be expanded, to avoid getting 118 -- two names referring to the same object in memory (the array and 119 -- the iterator) in GNATprove, especially since both can be written 120 -- (thus possibly leading to interferences due to aliasing). No such 121 -- problem arises with quantified expressions over arrays, which are 122 -- dealt with specially in GNATprove. 123 124 when N_Loop_Statement => 125 Expand_SPARK_N_Loop_Statement (N); 126 127 when N_Object_Declaration => 128 Expand_SPARK_N_Object_Declaration (N); 129 130 when N_Object_Renaming_Declaration => 131 Expand_SPARK_N_Object_Renaming_Declaration (N); 132 133 when N_Op_Ne => 134 Expand_SPARK_N_Op_Ne (N); 135 136 when N_Freeze_Entity => 137 if Is_Type (Entity (N)) then 138 Expand_SPARK_N_Freeze_Type (Entity (N)); 139 end if; 140 141 when N_Indexed_Component 142 | N_Slice 143 => 144 Expand_SPARK_N_Slice_Or_Indexed_Component (N); 145 146 when N_Selected_Component => 147 Expand_SPARK_N_Selected_Component (N); 148 149 -- In SPARK mode, no other constructs require expansion 150 151 when others => 152 null; 153 end case; 154 end Expand_SPARK; 155 156 -------------------------------- 157 -- Expand_SPARK_N_Freeze_Type -- 158 -------------------------------- 159 160 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is 161 begin 162 -- When a DIC is inherited by a tagged type, it may need to be 163 -- specialized to the descendant type, hence build a separate DIC 164 -- procedure for it as done during regular expansion for compilation. 165 166 if Has_DIC (E) and then Is_Tagged_Type (E) then 167 Build_DIC_Procedure_Body (E, For_Freeze => True); 168 end if; 169 end Expand_SPARK_N_Freeze_Type; 170 171 ---------------------------------------- 172 -- Expand_SPARK_N_Attribute_Reference -- 173 ---------------------------------------- 174 175 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is 176 Aname : constant Name_Id := Attribute_Name (N); 177 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); 178 Loc : constant Source_Ptr := Sloc (N); 179 Pref : constant Node_Id := Prefix (N); 180 Typ : constant Entity_Id := Etype (N); 181 Expr : Node_Id; 182 183 begin 184 if Attr_Id = Attribute_To_Address then 185 186 -- Extract and convert argument to expected type for call 187 188 Expr := 189 Make_Type_Conversion (Loc, 190 Subtype_Mark => 191 New_Occurrence_Of (RTE (RE_Integer_Address), Loc), 192 Expression => Relocate_Node (First (Expressions (N)))); 193 194 -- Replace attribute reference with call 195 196 Rewrite (N, 197 Make_Function_Call (Loc, 198 Name => 199 New_Occurrence_Of (RTE (RE_To_Address), Loc), 200 Parameter_Associations => New_List (Expr))); 201 Analyze_And_Resolve (N, Typ); 202 203 -- Whenever possible, replace a prefix which is an enumeration literal 204 -- by the corresponding literal value. 205 206 elsif Attr_Id = Attribute_Enum_Rep then 207 declare 208 Exprs : constant List_Id := Expressions (N); 209 begin 210 if Is_Non_Empty_List (Exprs) then 211 Expr := First (Exprs); 212 else 213 Expr := Prefix (N); 214 end if; 215 216 -- If the argument is a literal, expand it 217 218 if Nkind (Expr) in N_Has_Entity 219 and then 220 (Ekind (Entity (Expr)) = E_Enumeration_Literal 221 or else 222 (Nkind (Expr) in N_Has_Entity 223 and then Ekind (Entity (Expr)) = E_Constant 224 and then Present (Renamed_Object (Entity (Expr))) 225 and then Is_Entity_Name (Renamed_Object (Entity (Expr))) 226 and then Ekind (Entity (Renamed_Object (Entity (Expr)))) = 227 E_Enumeration_Literal)) 228 then 229 Exp_Attr.Expand_N_Attribute_Reference (N); 230 end if; 231 end; 232 233 elsif Attr_Id = Attribute_Object_Size 234 or else Attr_Id = Attribute_Size 235 or else Attr_Id = Attribute_Value_Size 236 or else Attr_Id = Attribute_VADS_Size 237 then 238 Exp_Attr.Expand_Size_Attribute (N); 239 240 -- For attributes which return Universal_Integer, introduce a conversion 241 -- to the expected type with the appropriate check flags set. 242 243 elsif Attr_Id = Attribute_Alignment 244 or else Attr_Id = Attribute_Bit 245 or else Attr_Id = Attribute_Bit_Position 246 or else Attr_Id = Attribute_Descriptor_Size 247 or else Attr_Id = Attribute_First_Bit 248 or else Attr_Id = Attribute_Last_Bit 249 or else Attr_Id = Attribute_Length 250 or else Attr_Id = Attribute_Max_Size_In_Storage_Elements 251 or else Attr_Id = Attribute_Pos 252 or else Attr_Id = Attribute_Position 253 or else Attr_Id = Attribute_Range_Length 254 or else Attr_Id = Attribute_Aft 255 or else Attr_Id = Attribute_Max_Alignment_For_Allocation 256 then 257 -- If the expected type is Long_Long_Integer, there will be no check 258 -- flag as the compiler assumes attributes always fit in this type. 259 -- Since in SPARK_Mode we do not take Storage_Error into account, we 260 -- cannot make this assumption and need to produce a check. 261 -- ??? It should be enough to add this check for attributes 'Length 262 -- and 'Range_Length when the type is as big as Long_Long_Integer. 263 264 declare 265 Typ : Entity_Id := Empty; 266 begin 267 if Attr_Id = Attribute_Range_Length then 268 Typ := Etype (Prefix (N)); 269 270 elsif Attr_Id = Attribute_Length then 271 Typ := Etype (Prefix (N)); 272 273 declare 274 Indx : Node_Id; 275 J : Int; 276 277 begin 278 if Is_Access_Type (Typ) then 279 Typ := Designated_Type (Typ); 280 end if; 281 282 if No (Expressions (N)) then 283 J := 1; 284 else 285 J := UI_To_Int (Expr_Value (First (Expressions (N)))); 286 end if; 287 288 Indx := First_Index (Typ); 289 while J > 1 loop 290 Next_Index (Indx); 291 J := J - 1; 292 end loop; 293 294 Typ := Etype (Indx); 295 end; 296 end if; 297 298 Apply_Universal_Integer_Attribute_Checks (N); 299 300 if Present (Typ) 301 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer) 302 then 303 Set_Do_Overflow_Check (N); 304 end if; 305 end; 306 307 elsif Attr_Id = Attribute_Constrained then 308 309 -- If the prefix is an access to object, the attribute applies to 310 -- the designated object, so rewrite with an explicit dereference. 311 312 if Is_Access_Type (Etype (Pref)) 313 and then 314 (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref))) 315 then 316 Rewrite (Pref, 317 Make_Explicit_Dereference (Loc, Relocate_Node (Pref))); 318 Analyze_And_Resolve (N, Standard_Boolean); 319 end if; 320 end if; 321 end Expand_SPARK_N_Attribute_Reference; 322 323 ----------------------------------- 324 -- Expand_SPARK_N_Loop_Statement -- 325 ----------------------------------- 326 327 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is 328 Scheme : constant Node_Id := Iteration_Scheme (N); 329 330 begin 331 -- Loop iterations over arrays need to be expanded, to avoid getting 332 -- two names referring to the same object in memory (the array and the 333 -- iterator) in GNATprove, especially since both can be written (thus 334 -- possibly leading to interferences due to aliasing). No such problem 335 -- arises with quantified expressions over arrays, which are dealt with 336 -- specially in GNATprove. 337 338 if Present (Scheme) 339 and then Present (Iterator_Specification (Scheme)) 340 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme)) 341 then 342 Expand_Iterator_Loop_Over_Array (N); 343 end if; 344 end Expand_SPARK_N_Loop_Statement; 345 346 --------------------------------------- 347 -- Expand_SPARK_N_Object_Declaration -- 348 --------------------------------------- 349 350 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is 351 Loc : constant Source_Ptr := Sloc (N); 352 Obj_Id : constant Entity_Id := Defining_Identifier (N); 353 Typ : constant Entity_Id := Etype (Obj_Id); 354 355 Call : Node_Id; 356 357 begin 358 -- If the object declaration denotes a variable without initialization 359 -- whose type is subject to pragma Default_Initial_Condition, create 360 -- and analyze a dummy call to the DIC procedure of the type in order 361 -- to detect potential elaboration issues. 362 363 if Comes_From_Source (Obj_Id) 364 and then Ekind (Obj_Id) = E_Variable 365 and then Has_DIC (Typ) 366 and then Present (DIC_Procedure (Typ)) 367 and then not Has_Init_Expression (N) 368 then 369 Call := Build_DIC_Call (Loc, Obj_Id, Typ); 370 371 -- Partially insert the call into the tree by setting its parent 372 -- pointer. 373 374 Set_Parent (Call, N); 375 Analyze (Call); 376 end if; 377 end Expand_SPARK_N_Object_Declaration; 378 379 ------------------------------------------------ 380 -- Expand_SPARK_N_Object_Renaming_Declaration -- 381 ------------------------------------------------ 382 383 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is 384 CFS : constant Boolean := Comes_From_Source (N); 385 Loc : constant Source_Ptr := Sloc (N); 386 Obj_Id : constant Entity_Id := Defining_Entity (N); 387 Nam : constant Node_Id := Name (N); 388 Typ : constant Entity_Id := Etype (Obj_Id); 389 390 begin 391 -- Transform a renaming of the form 392 393 -- Obj_Id : <subtype mark> renames <function call>; 394 395 -- into 396 397 -- Obj_Id : constant <subtype mark> := <function call>; 398 399 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces 400 -- a temporary to capture the function result. Once potential renamings 401 -- are rewritten for SPARK, the temporary may be leaked out into source 402 -- constructs and lead to confusing error diagnostics. Using an object 403 -- declaration prevents this unwanted side effect. 404 405 if Nkind (Nam) = N_Function_Call then 406 Rewrite (N, 407 Make_Object_Declaration (Loc, 408 Defining_Identifier => Obj_Id, 409 Constant_Present => True, 410 Object_Definition => New_Occurrence_Of (Typ, Loc), 411 Expression => Nam)); 412 413 -- Inherit the original Comes_From_Source status of the renaming 414 415 Set_Comes_From_Source (N, CFS); 416 417 -- Sever the link to the renamed function result because the entity 418 -- will no longer alias anything. 419 420 Set_Renamed_Object (Obj_Id, Empty); 421 422 -- Remove the entity of the renaming declaration from visibility as 423 -- the analysis of the object declaration will reintroduce it again. 424 425 Remove_Entity_And_Homonym (Obj_Id); 426 Analyze (N); 427 428 -- Otherwise unconditionally remove all side effects from the name 429 430 else 431 Evaluate_Name (Nam); 432 end if; 433 end Expand_SPARK_N_Object_Renaming_Declaration; 434 435 -------------------------- 436 -- Expand_SPARK_N_Op_Ne -- 437 -------------------------- 438 439 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is 440 Typ : constant Entity_Id := Etype (Left_Opnd (N)); 441 442 begin 443 -- Case of elementary type with standard operator 444 445 if Is_Elementary_Type (Typ) 446 and then Sloc (Entity (N)) = Standard_Location 447 then 448 null; 449 450 else 451 Exp_Ch4.Expand_N_Op_Ne (N); 452 end if; 453 end Expand_SPARK_N_Op_Ne; 454 455 ------------------------------------- 456 -- Expand_SPARK_Potential_Renaming -- 457 ------------------------------------- 458 459 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is 460 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean; 461 -- Determine whether arbitrary node Nod appears within a significant 462 -- pragma for SPARK. 463 464 ----------------------------- 465 -- In_Insignificant_Pragma -- 466 ----------------------------- 467 468 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is 469 Par : Node_Id; 470 471 begin 472 -- Climb the parent chain looking for an enclosing pragma 473 474 Par := Nod; 475 while Present (Par) loop 476 if Nkind (Par) = N_Pragma then 477 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par)); 478 479 -- Prevent the search from going too far 480 481 elsif Is_Body_Or_Package_Declaration (Par) then 482 exit; 483 end if; 484 485 Par := Parent (Par); 486 end loop; 487 488 return False; 489 end In_Insignificant_Pragma; 490 491 -- Local variables 492 493 Loc : constant Source_Ptr := Sloc (N); 494 Obj_Id : constant Entity_Id := Entity (N); 495 Typ : constant Entity_Id := Etype (N); 496 Ren : Node_Id; 497 498 -- Start of processing for Expand_SPARK_Potential_Renaming 499 500 begin 501 -- Replace a reference to a renaming with the actual renamed object 502 503 if Ekind (Obj_Id) in Object_Kind then 504 Ren := Renamed_Object (Obj_Id); 505 506 if Present (Ren) then 507 508 -- Do not process a reference when it appears within a pragma of 509 -- no significance to SPARK. It is assumed that the replacement 510 -- will violate the semantics of the pragma and cause a spurious 511 -- error. 512 513 if In_Insignificant_Pragma (N) then 514 return; 515 516 -- Instantiations and inlining of subprograms employ "prologues" 517 -- which map actual to formal parameters by means of renamings. 518 -- Replace a reference to a formal by the corresponding actual 519 -- parameter. 520 521 elsif Nkind (Ren) in N_Entity then 522 Rewrite (N, New_Occurrence_Of (Ren, Loc)); 523 524 -- Otherwise the renamed object denotes a name 525 526 else 527 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc)); 528 Reset_Analyzed_Flags (N); 529 end if; 530 531 Analyze_And_Resolve (N, Typ); 532 end if; 533 end if; 534 end Expand_SPARK_Potential_Renaming; 535 536 --------------------------------------- 537 -- Expand_SPARK_N_Selected_Component -- 538 --------------------------------------- 539 540 procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is 541 Pref : constant Node_Id := Prefix (N); 542 Typ : constant Entity_Id := Underlying_Type (Etype (Pref)); 543 544 begin 545 if Present (Typ) and then Is_Access_Type (Typ) then 546 547 -- First set prefix type to proper access type, in case it currently 548 -- has a private (non-access) view of this type. 549 550 Set_Etype (Pref, Typ); 551 552 Insert_Explicit_Dereference (Pref); 553 Analyze_And_Resolve (Pref, Designated_Type (Typ)); 554 end if; 555 end Expand_SPARK_N_Selected_Component; 556 557 ----------------------------------------------- 558 -- Expand_SPARK_N_Slice_Or_Indexed_Component -- 559 ----------------------------------------------- 560 561 procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id) is 562 Pref : constant Node_Id := Prefix (N); 563 Typ : constant Entity_Id := Etype (Pref); 564 565 begin 566 if Is_Access_Type (Typ) then 567 Insert_Explicit_Dereference (Pref); 568 Analyze_And_Resolve (Pref, Designated_Type (Typ)); 569 end if; 570 end Expand_SPARK_N_Slice_Or_Indexed_Component; 571 572end Exp_SPARK; 573