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_Ch5;  use Exp_Ch5;
  30 with Exp_Dbug; use Exp_Dbug;
  31 with Exp_Util; use Exp_Util;
  32 with Namet;    use Namet;
  33 with Nlists;   use Nlists;
  34 with Nmake;    use Nmake;
  35 with Rtsfind;  use Rtsfind;
  36 with Sem;      use Sem;
  37 with Sem_Eval; use Sem_Eval;
  38 with Sem_Res;  use Sem_Res;
  39 with Sem_Util; use Sem_Util;
  40 with Sinfo;    use Sinfo;
  41 with Snames;   use Snames;
  42 with Stand;    use Stand;
  43 with Tbuild;   use Tbuild;
  44 with Uintp;    use Uintp;
  45
  46 package body Exp_SPARK is
  47
  48    -----------------------
  49    -- Local Subprograms --
  50    -----------------------
  51
  52    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
  53    --  Replace occurrences of System'To_Address by calls to
  54    --  System.Storage_Elements.To_Address
  55
  56    procedure Expand_SPARK_Freeze_Type (E : Entity_Id);
  57    --  Build the DIC procedure of a type when needed, if not already done
  58
  59    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
  60    --  Perform object-declaration-specific expansion
  61
  62    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  63    --  Perform name evaluation for a renamed object
  64
  65    ------------------
  66    -- Expand_SPARK --
  67    ------------------
  68
  69    procedure Expand_SPARK (N : Node_Id) is
  70    begin
  71       case Nkind (N) is
  72
  73          --  Qualification of entity names in formal verification mode
  74          --  is limited to the addition of a suffix for homonyms (see
  75          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  76          --  as full expansion does, but this was removed as this prevents the
  77          --  verification back-end from using a short name for debugging and
  78          --  user interaction. The verification back-end already takes care
  79          --  of qualifying names when needed.
  80
  81          when N_Block_Statement
  82             | N_Entry_Declaration
  83             | N_Package_Body
  84             | N_Package_Declaration
  85             | N_Protected_Type_Declaration
  86             | N_Subprogram_Body
  87             | N_Task_Type_Declaration
  88          =>
  89             Qualify_Entity_Names (N);
  90
  91          --  Replace occurrences of System'To_Address by calls to
  92          --  System.Storage_Elements.To_Address.
  93
  94          when N_Attribute_Reference =>
  95             Expand_SPARK_N_Attribute_Reference (N);
  96
  97          when N_Expanded_Name
  98             | N_Identifier
  99          =>
 100             Expand_SPARK_Potential_Renaming (N);
 101
 102          --  Loop iterations over arrays need to be expanded, to avoid getting
 103          --  two names referring to the same object in memory (the array and
 104          --  the iterator) in GNATprove, especially since both can be written
 105          --  (thus possibly leading to interferences due to aliasing). No such
 106          --  problem arises with quantified expressions over arrays, which are
 107          --  dealt with specially in GNATprove.
 108
 109          when N_Loop_Statement =>
 110             declare
 111                Scheme : constant Node_Id := Iteration_Scheme (N);
 112             begin
 113                if Present (Scheme)
 114                  and then Present (Iterator_Specification (Scheme))
 115                  and then
 116                    Is_Iterator_Over_Array (Iterator_Specification (Scheme))
 117                then
 118                   Expand_Iterator_Loop_Over_Array (N);
 119                end if;
 120             end;
 121
 122          when N_Object_Declaration =>
 123             Expand_SPARK_N_Object_Declaration (N);
 124
 125          when N_Object_Renaming_Declaration =>
 126             Expand_SPARK_N_Object_Renaming_Declaration (N);
 127
 128          when N_Freeze_Entity =>
 129             if Is_Type (Entity (N)) then
 130                Expand_SPARK_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_Attribute_Reference --
 142    ----------------------------------------
 143
 144    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
 145       Aname   : constant Name_Id      := Attribute_Name (N);
 146       Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
 147       Loc     : constant Source_Ptr   := Sloc (N);
 148       Typ     : constant Entity_Id    := Etype (N);
 149       Expr    : Node_Id;
 150
 151    begin
 152       if Attr_Id = Attribute_To_Address then
 153
 154          --  Extract and convert argument to expected type for call
 155
 156          Expr :=
 157            Make_Type_Conversion (Loc,
 158              Subtype_Mark =>
 159                New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
 160              Expression   => Relocate_Node (First (Expressions (N))));
 161
 162          --  Replace attribute reference with call
 163
 164          Rewrite (N,
 165            Make_Function_Call (Loc,
 166              Name                   =>
 167                New_Occurrence_Of (RTE (RE_To_Address), Loc),
 168              Parameter_Associations => New_List (Expr)));
 169          Analyze_And_Resolve (N, Typ);
 170
 171       --  For attributes which return Universal_Integer, introduce a conversion
 172       --  to the expected type with the appropriate check flags set.
 173
 174       elsif Attr_Id = Attribute_Alignment
 175         or else Attr_Id = Attribute_Bit
 176         or else Attr_Id = Attribute_Bit_Position
 177         or else Attr_Id = Attribute_Descriptor_Size
 178         or else Attr_Id = Attribute_First_Bit
 179         or else Attr_Id = Attribute_Last_Bit
 180         or else Attr_Id = Attribute_Length
 181         or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
 182         or else Attr_Id = Attribute_Pos
 183         or else Attr_Id = Attribute_Position
 184         or else Attr_Id = Attribute_Range_Length
 185         or else Attr_Id = Attribute_Object_Size
 186         or else Attr_Id = Attribute_Size
 187         or else Attr_Id = Attribute_Value_Size
 188         or else Attr_Id = Attribute_VADS_Size
 189         or else Attr_Id = Attribute_Aft
 190         or else Attr_Id = Attribute_Max_Alignment_For_Allocation
 191       then
 192          --  If the expected type is Long_Long_Integer, there will be no check
 193          --  flag as the compiler assumes attributes always fit in this type.
 194          --  Since in SPARK_Mode we do not take Storage_Error into account, we
 195          --  cannot make this assumption and need to produce a check.
 196          --  ??? It should be enough to add this check for attributes 'Length
 197          --  and 'Range_Length when the type is as big as Long_Long_Integer.
 198
 199          declare
 200             Typ : Entity_Id := Empty;
 201          begin
 202             if Attr_Id = Attribute_Range_Length then
 203                Typ := Etype (Prefix (N));
 204
 205             elsif Attr_Id = Attribute_Length then
 206                Typ := Etype (Prefix (N));
 207
 208                declare
 209                   Indx : Node_Id;
 210                   J    : Int;
 211
 212                begin
 213                   if Is_Access_Type (Typ) then
 214                      Typ := Designated_Type (Typ);
 215                   end if;
 216
 217                   if No (Expressions (N)) then
 218                      J := 1;
 219                   else
 220                      J := UI_To_Int (Expr_Value (First (Expressions (N))));
 221                   end if;
 222
 223                   Indx := First_Index (Typ);
 224                   while J > 1 loop
 225                      Next_Index (Indx);
 226                      J := J - 1;
 227                   end loop;
 228
 229                   Typ := Etype (Indx);
 230                end;
 231             end if;
 232
 233             Apply_Universal_Integer_Attribute_Checks (N);
 234
 235             if Present (Typ)
 236               and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
 237             then
 238                Set_Do_Overflow_Check (N);
 239             end if;
 240          end;
 241       end if;
 242    end Expand_SPARK_N_Attribute_Reference;
 243
 244    ------------------------------
 245    -- Expand_SPARK_Freeze_Type --
 246    ------------------------------
 247
 248    procedure Expand_SPARK_Freeze_Type (E : Entity_Id) is
 249    begin
 250       --  When a DIC is inherited by a tagged type, it may need to be
 251       --  specialized to the descendant type, hence build a separate DIC
 252       --  procedure for it as done during regular expansion for compilation.
 253
 254       if Has_DIC (E)
 255         and then Is_Tagged_Type (E)
 256       then
 257          Build_DIC_Procedure_Body (E, For_Freeze => True);
 258       end if;
 259    end Expand_SPARK_Freeze_Type;
 260
 261    ---------------------------------------
 262    -- Expand_SPARK_N_Object_Declaration --
 263    ---------------------------------------
 264
 265    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
 266       Def_Id : constant Entity_Id  := Defining_Identifier (N);
 267       Loc    : constant Source_Ptr := Sloc (N);
 268       Typ    : constant Entity_Id  := Etype (Def_Id);
 269
 270    begin
 271       --  If the object declaration denotes a variable without initialization
 272       --  whose type is subject to pragma Default_Initial_Condition, create
 273       --  and analyze a dummy call to the DIC procedure of the type in order
 274       --  to detect potential elaboration issues.
 275
 276       if Comes_From_Source (Def_Id)
 277         and then Has_DIC (Typ)
 278         and then Present (DIC_Procedure (Typ))
 279         and then not Has_Init_Expression (N)
 280       then
 281          Analyze (Build_DIC_Call (Loc, Def_Id, Typ));
 282       end if;
 283    end Expand_SPARK_N_Object_Declaration;
 284
 285    ------------------------------------------------
 286    -- Expand_SPARK_N_Object_Renaming_Declaration --
 287    ------------------------------------------------
 288
 289    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 290    begin
 291       --  Unconditionally remove all side effects from the name
 292
 293       Evaluate_Name (Name (N));
 294    end Expand_SPARK_N_Object_Renaming_Declaration;
 295
 296    -------------------------------------
 297    -- Expand_SPARK_Potential_Renaming --
 298    -------------------------------------
 299
 300    procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
 301       Loc    : constant Source_Ptr := Sloc (N);
 302       Ren_Id : constant Entity_Id  := Entity (N);
 303       Typ    : constant Entity_Id  := Etype (N);
 304       Obj_Id : Node_Id;
 305
 306    begin
 307       --  Replace a reference to a renaming with the actual renamed object
 308
 309       if Ekind (Ren_Id) in Object_Kind then
 310          Obj_Id := Renamed_Object (Ren_Id);
 311
 312          if Present (Obj_Id) then
 313
 314             --  The renamed object is an entity when instantiating generics
 315             --  or inlining bodies. In this case the renaming is part of the
 316             --  mapping "prologue" which links actuals to formals.
 317
 318             if Nkind (Obj_Id) in N_Entity then
 319                Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
 320
 321             --  Otherwise the renamed object denotes a name
 322
 323             else
 324                Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc));
 325                Reset_Analyzed_Flags (N);
 326             end if;
 327
 328             Analyze_And_Resolve (N, Typ);
 329          end if;
 330       end if;
 331    end Expand_SPARK_Potential_Renaming;
 332
 333 end Exp_SPARK;