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-2016, 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_Res;  use Sem_Res;
  37 with Sem_Util; use Sem_Util;
  38 with Sinfo;    use Sinfo;
  39 with Snames;   use Snames;
  40 with Tbuild;   use Tbuild;
  41
  42 package body Exp_SPARK is
  43
  44    -----------------------
  45    -- Local Subprograms --
  46    -----------------------
  47
  48    procedure Expand_SPARK_Attribute_Reference (N : Node_Id);
  49    --  Replace occurrences of System'To_Address by calls to
  50    --  System.Storage_Elements.To_Address
  51
  52    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  53    --  Perform name evaluation for a renamed object
  54
  55    ------------------
  56    -- Expand_SPARK --
  57    ------------------
  58
  59    procedure Expand_SPARK (N : Node_Id) is
  60    begin
  61       case Nkind (N) is
  62
  63          --  Qualification of entity names in formal verification mode
  64          --  is limited to the addition of a suffix for homonyms (see
  65          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  66          --  as full expansion does, but this was removed as this prevents the
  67          --  verification back-end from using a short name for debugging and
  68          --  user interaction. The verification back-end already takes care
  69          --  of qualifying names when needed.
  70
  71          when N_Block_Statement
  72             | N_Entry_Declaration
  73             | N_Package_Body
  74             | N_Package_Declaration
  75             | N_Protected_Type_Declaration
  76             | N_Subprogram_Body
  77             | N_Task_Type_Declaration
  78          =>
  79             Qualify_Entity_Names (N);
  80
  81          when N_Expanded_Name
  82             | N_Identifier
  83          =>
  84             Expand_SPARK_Potential_Renaming (N);
  85
  86          when N_Object_Renaming_Declaration =>
  87             Expand_SPARK_N_Object_Renaming_Declaration (N);
  88
  89          --  Replace occurrences of System'To_Address by calls to
  90          --  System.Storage_Elements.To_Address
  91
  92          when N_Attribute_Reference =>
  93             Expand_SPARK_Attribute_Reference (N);
  94
  95          --  Loop iterations over arrays need to be expanded, to avoid getting
  96          --  two names referring to the same object in memory (the array and
  97          --  the iterator) in GNATprove, especially since both can be written
  98          --  (thus possibly leading to interferences due to aliasing). No such
  99          --  problem arises with quantified expressions over arrays, which are
 100          --  dealt with specially in GNATprove.
 101
 102          when N_Loop_Statement =>
 103             declare
 104                Scheme : constant Node_Id := Iteration_Scheme (N);
 105             begin
 106                if Present (Scheme)
 107                  and then Present (Iterator_Specification (Scheme))
 108                  and then
 109                    Is_Iterator_Over_Array (Iterator_Specification (Scheme))
 110                then
 111                   Expand_Iterator_Loop_Over_Array (N);
 112                end if;
 113             end;
 114
 115          --  In SPARK mode, no other constructs require expansion
 116
 117          when others =>
 118             null;
 119       end case;
 120    end Expand_SPARK;
 121
 122    --------------------------------------
 123    -- Expand_SPARK_Attribute_Reference --
 124    --------------------------------------
 125
 126    procedure Expand_SPARK_Attribute_Reference (N : Node_Id) is
 127       Aname   : constant Name_Id      := Attribute_Name (N);
 128       Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
 129       Loc     : constant Source_Ptr   := Sloc (N);
 130       Typ     : constant Entity_Id    := Etype (N);
 131       Expr    : Node_Id;
 132
 133    begin
 134       if Attr_Id = Attribute_To_Address then
 135
 136          --  Extract and convert argument to expected type for call
 137
 138          Expr :=
 139            Make_Type_Conversion (Loc,
 140              Subtype_Mark =>
 141                New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
 142              Expression   => Relocate_Node (First (Expressions (N))));
 143
 144          --  Replace attribute reference with call
 145
 146          Rewrite (N,
 147            Make_Function_Call (Loc,
 148              Name                   =>
 149                New_Occurrence_Of (RTE (RE_To_Address), Loc),
 150              Parameter_Associations => New_List (Expr)));
 151          Analyze_And_Resolve (N, Typ);
 152
 153       --  For attributes which return Universal_Integer, introduce a conversion
 154       --  to the expected type with the appropriate check flags set.
 155
 156       elsif Attr_Id = Attribute_Alignment
 157         or else Attr_Id = Attribute_Bit
 158         or else Attr_Id = Attribute_Bit_Position
 159         or else Attr_Id = Attribute_Descriptor_Size
 160         or else Attr_Id = Attribute_First_Bit
 161         or else Attr_Id = Attribute_Last_Bit
 162         or else Attr_Id = Attribute_Length
 163         or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
 164         or else Attr_Id = Attribute_Pos
 165         or else Attr_Id = Attribute_Position
 166         or else Attr_Id = Attribute_Range_Length
 167         or else Attr_Id = Attribute_Object_Size
 168         or else Attr_Id = Attribute_Size
 169         or else Attr_Id = Attribute_Value_Size
 170         or else Attr_Id = Attribute_VADS_Size
 171         or else Attr_Id = Attribute_Aft
 172         or else Attr_Id = Attribute_Max_Alignment_For_Allocation
 173       then
 174          Apply_Universal_Integer_Attribute_Checks (N);
 175       end if;
 176    end Expand_SPARK_Attribute_Reference;
 177
 178    ------------------------------------------------
 179    -- Expand_SPARK_N_Object_Renaming_Declaration --
 180    ------------------------------------------------
 181
 182    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 183    begin
 184       --  Unconditionally remove all side effects from the name
 185
 186       Evaluate_Name (Name (N));
 187    end Expand_SPARK_N_Object_Renaming_Declaration;
 188
 189    -------------------------------------
 190    -- Expand_SPARK_Potential_Renaming --
 191    -------------------------------------
 192
 193    procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
 194       Loc    : constant Source_Ptr := Sloc (N);
 195       Ren_Id : constant Entity_Id  := Entity (N);
 196       Typ    : constant Entity_Id  := Etype (N);
 197       Obj_Id : Node_Id;
 198
 199    begin
 200       --  Replace a reference to a renaming with the actual renamed object
 201
 202       if Ekind (Ren_Id) in Object_Kind then
 203          Obj_Id := Renamed_Object (Ren_Id);
 204
 205          if Present (Obj_Id) then
 206
 207             --  The renamed object is an entity when instantiating generics
 208             --  or inlining bodies. In this case the renaming is part of the
 209             --  mapping "prologue" which links actuals to formals.
 210
 211             if Nkind (Obj_Id) in N_Entity then
 212                Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
 213
 214             --  Otherwise the renamed object denotes a name
 215
 216             else
 217                Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc));
 218                Reset_Analyzed_Flags (N);
 219             end if;
 220
 221             Analyze_And_Resolve (N, Typ);
 222          end if;
 223       end if;
 224    end Expand_SPARK_Potential_Renaming;
 225
 226 end Exp_SPARK;