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-2017, 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_Ch4;
  30 with Exp_Ch5;  use Exp_Ch5;
  31 with Exp_Dbug; use Exp_Dbug;
  32 with Exp_Util; use Exp_Util;
  33 with Namet;    use Namet;
  34 with Nlists;   use Nlists;
  35 with Nmake;    use Nmake;
  36 with Rtsfind;  use Rtsfind;
  37 with Sem;      use Sem;
  38 with Sem_Eval; use Sem_Eval;
  39 with Sem_Res;  use Sem_Res;
  40 with Sem_Util; use Sem_Util;
  41 with Sinfo;    use Sinfo;
  42 with Snames;   use Snames;
  43 with Stand;    use Stand;
  44 with Tbuild;   use Tbuild;
  45 with Uintp;    use Uintp;
  46
  47 package body Exp_SPARK is
  48
  49    -----------------------
  50    -- Local Subprograms --
  51    -----------------------
  52
  53    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
  54    --  Replace occurrences of System'To_Address by calls to
  55    --  System.Storage_Elements.To_Address
  56
  57    procedure Expand_SPARK_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_Object_Declaration (N : Node_Id);
  61    --  Perform object-declaration-specific expansion
  62
  63    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  64    --  Perform name evaluation for a renamed object
  65
  66    procedure Expand_SPARK_Op_Ne (N : Node_Id);
  67    --  Rewrite operator /= based on operator = when defined explicitly
  68
  69    ------------------
  70    -- Expand_SPARK --
  71    ------------------
  72
  73    procedure Expand_SPARK (N : Node_Id) is
  74    begin
  75       case Nkind (N) is
  76
  77          --  Qualification of entity names in formal verification mode
  78          --  is limited to the addition of a suffix for homonyms (see
  79          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  80          --  as full expansion does, but this was removed as this prevents the
  81          --  verification back-end from using a short name for debugging and
  82          --  user interaction. The verification back-end already takes care
  83          --  of qualifying names when needed.
  84
  85          when N_Block_Statement
  86             | N_Entry_Declaration
  87             | N_Package_Body
  88             | N_Package_Declaration
  89             | N_Protected_Type_Declaration
  90             | N_Subprogram_Body
  91             | N_Task_Type_Declaration
  92          =>
  93             Qualify_Entity_Names (N);
  94
  95          --  Replace occurrences of System'To_Address by calls to
  96          --  System.Storage_Elements.To_Address.
  97
  98          when N_Attribute_Reference =>
  99             Expand_SPARK_N_Attribute_Reference (N);
 100
 101          when N_Expanded_Name
 102             | N_Identifier
 103          =>
 104             Expand_SPARK_Potential_Renaming (N);
 105
 106          --  Loop iterations over arrays need to be expanded, to avoid getting
 107          --  two names referring to the same object in memory (the array and
 108          --  the iterator) in GNATprove, especially since both can be written
 109          --  (thus possibly leading to interferences due to aliasing). No such
 110          --  problem arises with quantified expressions over arrays, which are
 111          --  dealt with specially in GNATprove.
 112
 113          when N_Loop_Statement =>
 114             declare
 115                Scheme : constant Node_Id := Iteration_Scheme (N);
 116             begin
 117                if Present (Scheme)
 118                  and then Present (Iterator_Specification (Scheme))
 119                  and then
 120                    Is_Iterator_Over_Array (Iterator_Specification (Scheme))
 121                then
 122                   Expand_Iterator_Loop_Over_Array (N);
 123                end if;
 124             end;
 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_Op_Ne (N);
 134
 135          when N_Freeze_Entity =>
 136             if Is_Type (Entity (N)) then
 137                Expand_SPARK_Freeze_Type (Entity (N));
 138             end if;
 139
 140          --  In SPARK mode, no other constructs require expansion
 141
 142          when others =>
 143             null;
 144       end case;
 145    end Expand_SPARK;
 146
 147    ----------------------------------------
 148    -- Expand_SPARK_N_Attribute_Reference --
 149    ----------------------------------------
 150
 151    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
 152       Aname   : constant Name_Id      := Attribute_Name (N);
 153       Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
 154       Loc     : constant Source_Ptr   := Sloc (N);
 155       Typ     : constant Entity_Id    := Etype (N);
 156       Expr    : Node_Id;
 157
 158    begin
 159       if Attr_Id = Attribute_To_Address then
 160
 161          --  Extract and convert argument to expected type for call
 162
 163          Expr :=
 164            Make_Type_Conversion (Loc,
 165              Subtype_Mark =>
 166                New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
 167              Expression   => Relocate_Node (First (Expressions (N))));
 168
 169          --  Replace attribute reference with call
 170
 171          Rewrite (N,
 172            Make_Function_Call (Loc,
 173              Name                   =>
 174                New_Occurrence_Of (RTE (RE_To_Address), Loc),
 175              Parameter_Associations => New_List (Expr)));
 176          Analyze_And_Resolve (N, Typ);
 177
 178       --  For attributes which return Universal_Integer, introduce a conversion
 179       --  to the expected type with the appropriate check flags set.
 180
 181       elsif Attr_Id = Attribute_Alignment
 182         or else Attr_Id = Attribute_Bit
 183         or else Attr_Id = Attribute_Bit_Position
 184         or else Attr_Id = Attribute_Descriptor_Size
 185         or else Attr_Id = Attribute_First_Bit
 186         or else Attr_Id = Attribute_Last_Bit
 187         or else Attr_Id = Attribute_Length
 188         or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
 189         or else Attr_Id = Attribute_Pos
 190         or else Attr_Id = Attribute_Position
 191         or else Attr_Id = Attribute_Range_Length
 192         or else Attr_Id = Attribute_Object_Size
 193         or else Attr_Id = Attribute_Size
 194         or else Attr_Id = Attribute_Value_Size
 195         or else Attr_Id = Attribute_VADS_Size
 196         or else Attr_Id = Attribute_Aft
 197         or else Attr_Id = Attribute_Max_Alignment_For_Allocation
 198       then
 199          --  If the expected type is Long_Long_Integer, there will be no check
 200          --  flag as the compiler assumes attributes always fit in this type.
 201          --  Since in SPARK_Mode we do not take Storage_Error into account, we
 202          --  cannot make this assumption and need to produce a check.
 203          --  ??? It should be enough to add this check for attributes 'Length
 204          --  and 'Range_Length when the type is as big as Long_Long_Integer.
 205
 206          declare
 207             Typ : Entity_Id := Empty;
 208          begin
 209             if Attr_Id = Attribute_Range_Length then
 210                Typ := Etype (Prefix (N));
 211
 212             elsif Attr_Id = Attribute_Length then
 213                Typ := Etype (Prefix (N));
 214
 215                declare
 216                   Indx : Node_Id;
 217                   J    : Int;
 218
 219                begin
 220                   if Is_Access_Type (Typ) then
 221                      Typ := Designated_Type (Typ);
 222                   end if;
 223
 224                   if No (Expressions (N)) then
 225                      J := 1;
 226                   else
 227                      J := UI_To_Int (Expr_Value (First (Expressions (N))));
 228                   end if;
 229
 230                   Indx := First_Index (Typ);
 231                   while J > 1 loop
 232                      Next_Index (Indx);
 233                      J := J - 1;
 234                   end loop;
 235
 236                   Typ := Etype (Indx);
 237                end;
 238             end if;
 239
 240             Apply_Universal_Integer_Attribute_Checks (N);
 241
 242             if Present (Typ)
 243               and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
 244             then
 245                Set_Do_Overflow_Check (N);
 246             end if;
 247          end;
 248       end if;
 249    end Expand_SPARK_N_Attribute_Reference;
 250
 251    ------------------------------
 252    -- Expand_SPARK_Freeze_Type --
 253    ------------------------------
 254
 255    procedure Expand_SPARK_Freeze_Type (E : Entity_Id) is
 256    begin
 257       --  When a DIC is inherited by a tagged type, it may need to be
 258       --  specialized to the descendant type, hence build a separate DIC
 259       --  procedure for it as done during regular expansion for compilation.
 260
 261       if Has_DIC (E) and then Is_Tagged_Type (E) then
 262          Build_DIC_Procedure_Body (E, For_Freeze => True);
 263       end if;
 264    end Expand_SPARK_Freeze_Type;
 265
 266    ---------------------------------------
 267    -- Expand_SPARK_N_Object_Declaration --
 268    ---------------------------------------
 269
 270    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
 271       Def_Id : constant Entity_Id  := Defining_Identifier (N);
 272       Loc    : constant Source_Ptr := Sloc (N);
 273       Typ    : constant Entity_Id  := Etype (Def_Id);
 274
 275    begin
 276       --  If the object declaration denotes a variable without initialization
 277       --  whose type is subject to pragma Default_Initial_Condition, create
 278       --  and analyze a dummy call to the DIC procedure of the type in order
 279       --  to detect potential elaboration issues.
 280
 281       if Comes_From_Source (Def_Id)
 282         and then Has_DIC (Typ)
 283         and then Present (DIC_Procedure (Typ))
 284         and then not Has_Init_Expression (N)
 285       then
 286          Analyze (Build_DIC_Call (Loc, Def_Id, Typ));
 287       end if;
 288    end Expand_SPARK_N_Object_Declaration;
 289
 290    ------------------------------------------------
 291    -- Expand_SPARK_N_Object_Renaming_Declaration --
 292    ------------------------------------------------
 293
 294    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 295       CFS    : constant Boolean    := Comes_From_Source (N);
 296       Loc    : constant Source_Ptr := Sloc (N);
 297       Obj_Id : constant Entity_Id  := Defining_Entity (N);
 298       Nam    : constant Node_Id    := Name (N);
 299       Typ    : constant Entity_Id  := Etype (Subtype_Mark (N));
 300
 301    begin
 302       --  Transform a renaming of the form
 303
 304       --    Obj_Id : <subtype mark> renames <function call>;
 305
 306       --  into
 307
 308       --    Obj_Id : constant <subtype mark> := <function call>;
 309
 310       --  Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
 311       --  a temporary to capture the function result. Once potential renamings
 312       --  are rewritten for SPARK, the temporary may be leaked out into source
 313       --  constructs and lead to confusing error diagnostics. Using an object
 314       --  declaration prevents this unwanted side effect.
 315
 316       if Nkind (Nam) = N_Function_Call then
 317          Rewrite (N,
 318            Make_Object_Declaration (Loc,
 319              Defining_Identifier => Obj_Id,
 320              Constant_Present    => True,
 321              Object_Definition   => New_Occurrence_Of (Typ, Loc),
 322              Expression          => Nam));
 323
 324          --  Inherit the original Comes_From_Source status of the renaming
 325
 326          Set_Comes_From_Source (N, CFS);
 327
 328          --  Sever the link to the renamed function result because the entity
 329          --  will no longer alias anything.
 330
 331          Set_Renamed_Object (Obj_Id, Empty);
 332
 333          --  Remove the entity of the renaming declaration from visibility as
 334          --  the analysis of the object declaration will reintroduce it again.
 335
 336          Remove_Entity (Obj_Id);
 337          Analyze (N);
 338
 339       --  Otherwise unconditionally remove all side effects from the name
 340
 341       else
 342          Evaluate_Name (Nam);
 343       end if;
 344    end Expand_SPARK_N_Object_Renaming_Declaration;
 345
 346    ------------------------
 347    -- Expand_SPARK_Op_Ne --
 348    ------------------------
 349
 350    procedure Expand_SPARK_Op_Ne (N : Node_Id) is
 351       Typ : constant Entity_Id := Etype (Left_Opnd (N));
 352
 353    begin
 354       --  Case of elementary type with standard operator
 355
 356       if Is_Elementary_Type (Typ)
 357         and then Sloc (Entity (N)) = Standard_Location
 358       then
 359          null;
 360
 361       else
 362          Exp_Ch4.Expand_N_Op_Ne (N);
 363       end if;
 364    end Expand_SPARK_Op_Ne;
 365
 366    -------------------------------------
 367    -- Expand_SPARK_Potential_Renaming --
 368    -------------------------------------
 369
 370    procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
 371       Loc    : constant Source_Ptr := Sloc (N);
 372       Obj_Id : constant Entity_Id  := Entity (N);
 373       Typ    : constant Entity_Id  := Etype (N);
 374       Ren    : Node_Id;
 375
 376    begin
 377       --  Replace a reference to a renaming with the actual renamed object
 378
 379       if Ekind (Obj_Id) in Object_Kind then
 380          Ren := Renamed_Object (Obj_Id);
 381
 382          if Present (Ren) then
 383
 384             --  Instantiations and inlining of subprograms employ "prologues"
 385             --  which map actual to formal parameters by means of renamings.
 386             --  Replace a reference to a formal by the corresponding actual
 387             --  parameter.
 388
 389             if Nkind (Ren) in N_Entity then
 390                Rewrite (N, New_Occurrence_Of (Ren, Loc));
 391
 392             --  Otherwise the renamed object denotes a name
 393
 394             else
 395                Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
 396                Reset_Analyzed_Flags (N);
 397             end if;
 398
 399             Analyze_And_Resolve (N, Typ);
 400          end if;
 401       end if;
 402    end Expand_SPARK_Potential_Renaming;
 403
 404 end Exp_SPARK;