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