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