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