gcc/ada/exp_spark.adb

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