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