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_Ch4; 30with Exp_Ch5; use Exp_Ch5; 31with Exp_Dbug; use Exp_Dbug; 32with Exp_Util; use Exp_Util; 33with Namet; use Namet; 34with Nlists; use Nlists; 35with Nmake; use Nmake; 36with Rtsfind; use Rtsfind; 37with Sem; use Sem; 38with Sem_Eval; use Sem_Eval; 39with Sem_Prag; use Sem_Prag; 40with Sem_Res; use Sem_Res; 41with Sem_Util; use Sem_Util; 42with Sinfo; use Sinfo; 43with Snames; use Snames; 44with Stand; use Stand; 45with Tbuild; use Tbuild; 46with Uintp; use Uintp; 47 48package body Exp_SPARK is 49 50 ----------------------- 51 -- Local Subprograms -- 52 ----------------------- 53 54 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id); 55 -- Replace occurrences of System'To_Address by calls to 56 -- System.Storage_Elements.To_Address 57 58 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id); 59 -- Build the DIC procedure of a type when needed, if not already done 60 61 procedure Expand_SPARK_N_Indexed_Component (N : Node_Id); 62 -- Insert explicit dereference if required 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_N_Selected_Component (N : Node_Id); 77 -- Insert explicit dereference if required 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_Expanded_Name 112 | N_Identifier 113 => 114 Expand_SPARK_Potential_Renaming (N); 115 116 -- Loop iterations over arrays need to be expanded, to avoid getting 117 -- two names referring to the same object in memory (the array and 118 -- the iterator) in GNATprove, especially since both can be written 119 -- (thus possibly leading to interferences due to aliasing). No such 120 -- problem arises with quantified expressions over arrays, which are 121 -- dealt with specially in GNATprove. 122 123 when N_Loop_Statement => 124 Expand_SPARK_N_Loop_Statement (N); 125 126 when N_Object_Declaration => 127 Expand_SPARK_N_Object_Declaration (N); 128 129 when N_Object_Renaming_Declaration => 130 Expand_SPARK_N_Object_Renaming_Declaration (N); 131 132 when N_Op_Ne => 133 Expand_SPARK_N_Op_Ne (N); 134 135 when N_Freeze_Entity => 136 if Is_Type (Entity (N)) then 137 Expand_SPARK_N_Freeze_Type (Entity (N)); 138 end if; 139 140 when N_Indexed_Component => 141 Expand_SPARK_N_Indexed_Component (N); 142 143 when N_Selected_Component => 144 Expand_SPARK_N_Selected_Component (N); 145 146 -- In SPARK mode, no other constructs require expansion 147 148 when others => 149 null; 150 end case; 151 end Expand_SPARK; 152 153 -------------------------------- 154 -- Expand_SPARK_N_Freeze_Type -- 155 -------------------------------- 156 157 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is 158 begin 159 -- When a DIC is inherited by a tagged type, it may need to be 160 -- specialized to the descendant type, hence build a separate DIC 161 -- procedure for it as done during regular expansion for compilation. 162 163 if Has_DIC (E) and then Is_Tagged_Type (E) then 164 Build_DIC_Procedure_Body (E, For_Freeze => True); 165 end if; 166 end Expand_SPARK_N_Freeze_Type; 167 168 ---------------------------------------- 169 -- Expand_SPARK_N_Attribute_Reference -- 170 ---------------------------------------- 171 172 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is 173 Aname : constant Name_Id := Attribute_Name (N); 174 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); 175 Loc : constant Source_Ptr := Sloc (N); 176 Typ : constant Entity_Id := Etype (N); 177 Expr : Node_Id; 178 179 begin 180 if Attr_Id = Attribute_To_Address then 181 182 -- Extract and convert argument to expected type for call 183 184 Expr := 185 Make_Type_Conversion (Loc, 186 Subtype_Mark => 187 New_Occurrence_Of (RTE (RE_Integer_Address), Loc), 188 Expression => Relocate_Node (First (Expressions (N)))); 189 190 -- Replace attribute reference with call 191 192 Rewrite (N, 193 Make_Function_Call (Loc, 194 Name => 195 New_Occurrence_Of (RTE (RE_To_Address), Loc), 196 Parameter_Associations => New_List (Expr))); 197 Analyze_And_Resolve (N, Typ); 198 199 -- For attributes which return Universal_Integer, introduce a conversion 200 -- to the expected type with the appropriate check flags set. 201 202 elsif Attr_Id = Attribute_Alignment 203 or else Attr_Id = Attribute_Bit 204 or else Attr_Id = Attribute_Bit_Position 205 or else Attr_Id = Attribute_Descriptor_Size 206 or else Attr_Id = Attribute_First_Bit 207 or else Attr_Id = Attribute_Last_Bit 208 or else Attr_Id = Attribute_Length 209 or else Attr_Id = Attribute_Max_Size_In_Storage_Elements 210 or else Attr_Id = Attribute_Pos 211 or else Attr_Id = Attribute_Position 212 or else Attr_Id = Attribute_Range_Length 213 or else Attr_Id = Attribute_Object_Size 214 or else Attr_Id = Attribute_Size 215 or else Attr_Id = Attribute_Value_Size 216 or else Attr_Id = Attribute_VADS_Size 217 or else Attr_Id = Attribute_Aft 218 or else Attr_Id = Attribute_Max_Alignment_For_Allocation 219 then 220 -- If the expected type is Long_Long_Integer, there will be no check 221 -- flag as the compiler assumes attributes always fit in this type. 222 -- Since in SPARK_Mode we do not take Storage_Error into account, we 223 -- cannot make this assumption and need to produce a check. 224 -- ??? It should be enough to add this check for attributes 'Length 225 -- and 'Range_Length when the type is as big as Long_Long_Integer. 226 227 declare 228 Typ : Entity_Id := Empty; 229 begin 230 if Attr_Id = Attribute_Range_Length then 231 Typ := Etype (Prefix (N)); 232 233 elsif Attr_Id = Attribute_Length then 234 Typ := Etype (Prefix (N)); 235 236 declare 237 Indx : Node_Id; 238 J : Int; 239 240 begin 241 if Is_Access_Type (Typ) then 242 Typ := Designated_Type (Typ); 243 end if; 244 245 if No (Expressions (N)) then 246 J := 1; 247 else 248 J := UI_To_Int (Expr_Value (First (Expressions (N)))); 249 end if; 250 251 Indx := First_Index (Typ); 252 while J > 1 loop 253 Next_Index (Indx); 254 J := J - 1; 255 end loop; 256 257 Typ := Etype (Indx); 258 end; 259 end if; 260 261 Apply_Universal_Integer_Attribute_Checks (N); 262 263 if Present (Typ) 264 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer) 265 then 266 Set_Do_Overflow_Check (N); 267 end if; 268 end; 269 end if; 270 end Expand_SPARK_N_Attribute_Reference; 271 272 ----------------------------------- 273 -- Expand_SPARK_N_Loop_Statement -- 274 ----------------------------------- 275 276 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is 277 Scheme : constant Node_Id := Iteration_Scheme (N); 278 279 begin 280 -- Loop iterations over arrays need to be expanded, to avoid getting 281 -- two names referring to the same object in memory (the array and the 282 -- iterator) in GNATprove, especially since both can be written (thus 283 -- possibly leading to interferences due to aliasing). No such problem 284 -- arises with quantified expressions over arrays, which are dealt with 285 -- specially in GNATprove. 286 287 if Present (Scheme) 288 and then Present (Iterator_Specification (Scheme)) 289 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme)) 290 then 291 Expand_Iterator_Loop_Over_Array (N); 292 end if; 293 end Expand_SPARK_N_Loop_Statement; 294 295 -------------------------------------- 296 -- Expand_SPARK_N_Indexed_Component -- 297 -------------------------------------- 298 299 procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is 300 Pref : constant Node_Id := Prefix (N); 301 Typ : constant Entity_Id := Etype (Pref); 302 303 begin 304 if Is_Access_Type (Typ) then 305 Insert_Explicit_Dereference (Pref); 306 Analyze_And_Resolve (Pref, Designated_Type (Typ)); 307 end if; 308 end Expand_SPARK_N_Indexed_Component; 309 310 --------------------------------------- 311 -- Expand_SPARK_N_Object_Declaration -- 312 --------------------------------------- 313 314 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is 315 Loc : constant Source_Ptr := Sloc (N); 316 Obj_Id : constant Entity_Id := Defining_Identifier (N); 317 Typ : constant Entity_Id := Etype (Obj_Id); 318 319 Call : Node_Id; 320 321 begin 322 -- If the object declaration denotes a variable without initialization 323 -- whose type is subject to pragma Default_Initial_Condition, create 324 -- and analyze a dummy call to the DIC procedure of the type in order 325 -- to detect potential elaboration issues. 326 327 if Comes_From_Source (Obj_Id) 328 and then Ekind (Obj_Id) = E_Variable 329 and then Has_DIC (Typ) 330 and then Present (DIC_Procedure (Typ)) 331 and then not Has_Init_Expression (N) 332 then 333 Call := Build_DIC_Call (Loc, Obj_Id, Typ); 334 335 -- Partially insert the call into the tree by setting its parent 336 -- pointer. 337 338 Set_Parent (Call, N); 339 Analyze (Call); 340 end if; 341 end Expand_SPARK_N_Object_Declaration; 342 343 ------------------------------------------------ 344 -- Expand_SPARK_N_Object_Renaming_Declaration -- 345 ------------------------------------------------ 346 347 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is 348 CFS : constant Boolean := Comes_From_Source (N); 349 Loc : constant Source_Ptr := Sloc (N); 350 Obj_Id : constant Entity_Id := Defining_Entity (N); 351 Nam : constant Node_Id := Name (N); 352 Typ : constant Entity_Id := Etype (Obj_Id); 353 354 begin 355 -- Transform a renaming of the form 356 357 -- Obj_Id : <subtype mark> renames <function call>; 358 359 -- into 360 361 -- Obj_Id : constant <subtype mark> := <function call>; 362 363 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces 364 -- a temporary to capture the function result. Once potential renamings 365 -- are rewritten for SPARK, the temporary may be leaked out into source 366 -- constructs and lead to confusing error diagnostics. Using an object 367 -- declaration prevents this unwanted side effect. 368 369 if Nkind (Nam) = N_Function_Call then 370 Rewrite (N, 371 Make_Object_Declaration (Loc, 372 Defining_Identifier => Obj_Id, 373 Constant_Present => True, 374 Object_Definition => New_Occurrence_Of (Typ, Loc), 375 Expression => Nam)); 376 377 -- Inherit the original Comes_From_Source status of the renaming 378 379 Set_Comes_From_Source (N, CFS); 380 381 -- Sever the link to the renamed function result because the entity 382 -- will no longer alias anything. 383 384 Set_Renamed_Object (Obj_Id, Empty); 385 386 -- Remove the entity of the renaming declaration from visibility as 387 -- the analysis of the object declaration will reintroduce it again. 388 389 Remove_Entity_And_Homonym (Obj_Id); 390 Analyze (N); 391 392 -- Otherwise unconditionally remove all side effects from the name 393 394 else 395 Evaluate_Name (Nam); 396 end if; 397 end Expand_SPARK_N_Object_Renaming_Declaration; 398 399 -------------------------- 400 -- Expand_SPARK_N_Op_Ne -- 401 -------------------------- 402 403 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is 404 Typ : constant Entity_Id := Etype (Left_Opnd (N)); 405 406 begin 407 -- Case of elementary type with standard operator 408 409 if Is_Elementary_Type (Typ) 410 and then Sloc (Entity (N)) = Standard_Location 411 then 412 null; 413 414 else 415 Exp_Ch4.Expand_N_Op_Ne (N); 416 end if; 417 end Expand_SPARK_N_Op_Ne; 418 419 ------------------------------------- 420 -- Expand_SPARK_Potential_Renaming -- 421 ------------------------------------- 422 423 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is 424 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean; 425 -- Determine whether arbitrary node Nod appears within a significant 426 -- pragma for SPARK. 427 428 ----------------------------- 429 -- In_Insignificant_Pragma -- 430 ----------------------------- 431 432 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is 433 Par : Node_Id; 434 435 begin 436 -- Climb the parent chain looking for an enclosing pragma 437 438 Par := Nod; 439 while Present (Par) loop 440 if Nkind (Par) = N_Pragma then 441 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par)); 442 443 -- Prevent the search from going too far 444 445 elsif Is_Body_Or_Package_Declaration (Par) then 446 exit; 447 end if; 448 449 Par := Parent (Par); 450 end loop; 451 452 return False; 453 end In_Insignificant_Pragma; 454 455 -- Local variables 456 457 Loc : constant Source_Ptr := Sloc (N); 458 Obj_Id : constant Entity_Id := Entity (N); 459 Typ : constant Entity_Id := Etype (N); 460 Ren : Node_Id; 461 462 -- Start of processing for Expand_SPARK_Potential_Renaming 463 464 begin 465 -- Replace a reference to a renaming with the actual renamed object 466 467 if Ekind (Obj_Id) in Object_Kind then 468 Ren := Renamed_Object (Obj_Id); 469 470 if Present (Ren) then 471 472 -- Do not process a reference when it appears within a pragma of 473 -- no significance to SPARK. It is assumed that the replacement 474 -- will violate the semantics of the pragma and cause a spurious 475 -- error. 476 477 if In_Insignificant_Pragma (N) then 478 return; 479 480 -- Instantiations and inlining of subprograms employ "prologues" 481 -- which map actual to formal parameters by means of renamings. 482 -- Replace a reference to a formal by the corresponding actual 483 -- parameter. 484 485 elsif Nkind (Ren) in N_Entity then 486 Rewrite (N, New_Occurrence_Of (Ren, Loc)); 487 488 -- Otherwise the renamed object denotes a name 489 490 else 491 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc)); 492 Reset_Analyzed_Flags (N); 493 end if; 494 495 Analyze_And_Resolve (N, Typ); 496 end if; 497 end if; 498 end Expand_SPARK_Potential_Renaming; 499 500 --------------------------------------- 501 -- Expand_SPARK_N_Selected_Component -- 502 --------------------------------------- 503 504 procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is 505 Pref : constant Node_Id := Prefix (N); 506 Typ : constant Entity_Id := Underlying_Type (Etype (Pref)); 507 508 begin 509 if Present (Typ) and then Is_Access_Type (Typ) then 510 511 -- First set prefix type to proper access type, in case it currently 512 -- has a private (non-access) view of this type. 513 514 Set_Etype (Pref, Typ); 515 516 Insert_Explicit_Dereference (Pref); 517 Analyze_And_Resolve (Pref, Designated_Type (Typ)); 518 519 if Ekind (Etype (Pref)) = E_Private_Subtype 520 and then Is_For_Access_Subtype (Etype (Pref)) 521 then 522 Set_Etype (Pref, Base_Type (Etype (Pref))); 523 end if; 524 end if; 525 end Expand_SPARK_N_Selected_Component; 526 527end Exp_SPARK; 528