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-2013, 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_Attr; use Exp_Attr;
  29 with Exp_Ch4;  use Exp_Ch4;
  30 with Exp_Ch6;  use Exp_Ch6;
  31 with Exp_Dbug; use Exp_Dbug;
  32 with Exp_Util; use Exp_Util;
  33 with Nlists;   use Nlists;
  34 with Rtsfind;  use Rtsfind;
  35 with Sem_Aux;  use Sem_Aux;
  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 Stand;    use Stand;
  41 with Tbuild;   use Tbuild;
  42
  43 package body Exp_SPARK is
  44
  45    -----------------------
  46    -- Local Subprograms --
  47    -----------------------
  48
  49    procedure Expand_SPARK_Call (N : Node_Id);
  50    --  This procedure contains common processing for function and procedure
  51    --  calls:
  52    --    * expansion of actuals to introduce necessary temporaries
  53    --    * replacement of renaming by subprogram renamed
  54
  55    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
  56    --  Expand attributes 'Old and 'Result only
  57
  58    procedure Expand_SPARK_N_In (N : Node_Id);
  59    --  Expand set membership into individual ones
  60
  61    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  62    --  Perform name evaluation for a renamed object
  63
  64    procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id);
  65    --  Insert conversion on function return if necessary
  66
  67    procedure Expand_SPARK_Simple_Function_Return (N : Node_Id);
  68    --  Expand simple return from function
  69
  70    procedure Expand_Potential_Renaming (N : Node_Id);
  71    --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
  72    --  replace N with the renamed object.
  73
  74    ------------------
  75    -- Expand_SPARK --
  76    ------------------
  77
  78    procedure Expand_SPARK (N : Node_Id) is
  79    begin
  80       case Nkind (N) is
  81          when N_Attribute_Reference =>
  82             Expand_SPARK_N_Attribute_Reference (N);
  83
  84          --  Qualification of entity names in formal verification mode
  85          --  is limited to the addition of a suffix for homonyms (see
  86          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  87          --  as full expansion does, but this was removed as this prevents the
  88          --  verification back-end from using a short name for debugging and
  89          --  user interaction. The verification back-end already takes care
  90          --  of qualifying names when needed.
  91
  92          when N_Block_Statement     |
  93               N_Package_Body        |
  94               N_Package_Declaration |
  95               N_Subprogram_Body     =>
  96             Qualify_Entity_Names (N);
  97
  98          when N_Subprogram_Call     =>
  99             Expand_SPARK_Call (N);
 100
 101          when N_Expanded_Name |
 102               N_Identifier    =>
 103             Expand_Potential_Renaming (N);
 104
 105          when N_In =>
 106             Expand_SPARK_N_In (N);
 107
 108          --  A NOT IN B gets transformed to NOT (A IN B). This is the same
 109          --  expansion used in the normal case, so shared the code.
 110
 111          when N_Not_In =>
 112             Expand_N_Not_In (N);
 113
 114          when N_Object_Renaming_Declaration =>
 115             Expand_SPARK_N_Object_Renaming_Declaration (N);
 116
 117          when N_Simple_Return_Statement =>
 118             Expand_SPARK_N_Simple_Return_Statement (N);
 119
 120          --  In SPARK mode, no other constructs require expansion
 121
 122          when others =>
 123             null;
 124       end case;
 125    end Expand_SPARK;
 126
 127    -----------------------
 128    -- Expand_SPARK_Call --
 129    -----------------------
 130
 131    procedure Expand_SPARK_Call (N : Node_Id) is
 132       Call_Node   : constant Node_Id := N;
 133       Parent_Subp : Entity_Id;
 134       Subp        : Entity_Id;
 135
 136    begin
 137       --  Ignore if previous error
 138
 139       if Nkind (Call_Node) in N_Has_Etype
 140         and then Etype (Call_Node) = Any_Type
 141       then
 142          return;
 143       end if;
 144
 145       --  Call using access to subprogram with explicit dereference
 146
 147       if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
 148          Subp        := Etype (Name (Call_Node));
 149          Parent_Subp := Empty;
 150
 151       --  Case of call to simple entry, where the Name is a selected component
 152       --  whose prefix is the task, and whose selector name is the entry name
 153
 154       elsif Nkind (Name (Call_Node)) = N_Selected_Component then
 155          Subp        := Entity (Selector_Name (Name (Call_Node)));
 156          Parent_Subp := Empty;
 157
 158       --  Case of call to member of entry family, where Name is an indexed
 159       --  component, with the prefix being a selected component giving the
 160       --  task and entry family name, and the index being the entry index.
 161
 162       elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
 163          Subp        := Entity (Selector_Name (Prefix (Name (Call_Node))));
 164          Parent_Subp := Empty;
 165
 166       --  Normal case
 167
 168       else
 169          Subp        := Entity (Name (Call_Node));
 170          Parent_Subp := Alias (Subp);
 171       end if;
 172
 173       --  Various expansion activities for actuals are carried out
 174
 175       Expand_Actuals (N, Subp);
 176
 177       --  If the subprogram is a renaming, replace it in the call with the name
 178       --  of the actual subprogram being called.
 179
 180       if Present (Parent_Subp) then
 181          Parent_Subp := Ultimate_Alias (Parent_Subp);
 182
 183          --  The below setting of Entity is suspect, see F109-018 discussion???
 184
 185          Set_Entity (Name (Call_Node), Parent_Subp);
 186       end if;
 187    end Expand_SPARK_Call;
 188
 189    ----------------------------------------
 190    -- Expand_SPARK_N_Attribute_Reference --
 191    ----------------------------------------
 192
 193    procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
 194       Id : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
 195
 196    begin
 197       case Id is
 198          when Attribute_Old    |
 199               Attribute_Result =>
 200             Expand_N_Attribute_Reference (N);
 201
 202          when others =>
 203             null;
 204       end case;
 205    end Expand_SPARK_N_Attribute_Reference;
 206
 207    -----------------------
 208    -- Expand_SPARK_N_In --
 209    -----------------------
 210
 211    procedure Expand_SPARK_N_In (N : Node_Id) is
 212    begin
 213       if Present (Alternatives (N)) then
 214          Expand_Set_Membership (N);
 215       end if;
 216    end Expand_SPARK_N_In;
 217
 218    ------------------------------------------------
 219    -- Expand_SPARK_N_Object_Renaming_Declaration --
 220    ------------------------------------------------
 221
 222    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 223    begin
 224       --  Unconditionally remove all side effects from the name
 225
 226       Evaluate_Name (Name (N));
 227    end Expand_SPARK_N_Object_Renaming_Declaration;
 228
 229    --------------------------------------------
 230    -- Expand_SPARK_N_Simple_Return_Statement --
 231    --------------------------------------------
 232
 233    procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id) is
 234    begin
 235       --  Defend against previous errors (i.e. the return statement calls a
 236       --  function that is not available in configurable runtime).
 237
 238       if Present (Expression (N))
 239         and then Nkind (Expression (N)) = N_Empty
 240       then
 241          return;
 242       end if;
 243
 244       --  Distinguish the function and non-function cases:
 245
 246       case Ekind (Return_Applies_To (Return_Statement_Entity (N))) is
 247
 248          when E_Function          |
 249               E_Generic_Function  =>
 250             Expand_SPARK_Simple_Function_Return (N);
 251
 252          when E_Procedure         |
 253               E_Generic_Procedure |
 254               E_Entry             |
 255               E_Entry_Family      |
 256               E_Return_Statement =>
 257             null;
 258
 259          when others =>
 260             raise Program_Error;
 261       end case;
 262
 263    exception
 264       when RE_Not_Available =>
 265          return;
 266    end Expand_SPARK_N_Simple_Return_Statement;
 267
 268    -----------------------------------------
 269    -- Expand_SPARK_Simple_Function_Return --
 270    -----------------------------------------
 271
 272    procedure Expand_SPARK_Simple_Function_Return (N : Node_Id) is
 273       Scope_Id : constant Entity_Id :=
 274                    Return_Applies_To (Return_Statement_Entity (N));
 275       --  The function we are returning from
 276
 277       R_Type : constant Entity_Id := Etype (Scope_Id);
 278       --  The result type of the function
 279
 280       Exp : constant Node_Id := Expression (N);
 281       pragma Assert (Present (Exp));
 282
 283       Exptyp : constant Entity_Id := Etype (Exp);
 284       --  The type of the expression (not necessarily the same as R_Type)
 285
 286    begin
 287       --  Check the result expression of a scalar function against the subtype
 288       --  of the function by inserting a conversion. This conversion must
 289       --  eventually be performed for other classes of types, but for now it's
 290       --  only done for scalars.
 291       --  ???
 292
 293       if Is_Scalar_Type (Exptyp) then
 294          Rewrite (Exp, Convert_To (R_Type, Exp));
 295
 296          --  The expression is resolved to ensure that the conversion gets
 297          --  expanded to generate a possible constraint check.
 298
 299          Analyze_And_Resolve (Exp, R_Type);
 300       end if;
 301    end Expand_SPARK_Simple_Function_Return;
 302
 303    -------------------------------
 304    -- Expand_Potential_Renaming --
 305    -------------------------------
 306
 307    procedure Expand_Potential_Renaming (N : Node_Id) is
 308       E : constant Entity_Id := Entity (N);
 309       T : constant Entity_Id := Etype (N);
 310
 311    begin
 312       --  Replace a reference to a renaming with the actual renamed object
 313
 314       if Ekind (E) in Object_Kind and then Present (Renamed_Object (E)) then
 315          Rewrite (N, New_Copy_Tree (Renamed_Object (E)));
 316          Reset_Analyzed_Flags (N);
 317          Analyze_And_Resolve (N, T);
 318       end if;
 319    end Expand_Potential_Renaming;
 320
 321 end Exp_SPARK;