path: root/gcc/ada/exp_spark.adb

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                            E X P _ S P A R K                             --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--          Copyright (C) 1992-2019, Free Software Foundation, Inc.         --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

with Atree;    use Atree;
with Checks;   use Checks;
with Einfo;    use Einfo;
with Exp_Ch4;
with Exp_Ch5;  use Exp_Ch5;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
with Namet;    use Namet;
with Nlists;   use Nlists;
with Nmake;    use Nmake;
with Rtsfind;  use Rtsfind;
with Sem;      use Sem;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
with Sem_Res;  use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo;    use Sinfo;
with Snames;   use Snames;
with Stand;    use Stand;
with Tbuild;   use Tbuild;
with Uintp;    use Uintp;

package body Exp_SPARK is

   -----------------------
   -- Local Subprograms --
   -----------------------

   procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
   --  Replace occurrences of System'To_Address by calls to
   --  System.Storage_Elements.To_Address

   procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
   --  Build the DIC procedure of a type when needed, if not already done

   procedure Expand_SPARK_N_Indexed_Component (N : Node_Id);
   --  Insert explicit dereference if required

   procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
   --  Perform loop statement-specific expansion

   procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
   --  Perform object-declaration-specific expansion

   procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
   --  Perform name evaluation for a renamed object

   procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
   --  Rewrite operator /= based on operator = when defined explicitly

   procedure Expand_SPARK_N_Selected_Component (N : Node_Id);
   --  Insert explicit dereference if required

   ------------------
   -- Expand_SPARK --
   ------------------

   procedure Expand_SPARK (N : Node_Id) is
   begin
      case Nkind (N) is

         --  Qualification of entity names in formal verification mode
         --  is limited to the addition of a suffix for homonyms (see
         --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
         --  as full expansion does, but this was removed as this prevents the
         --  verification back-end from using a short name for debugging and
         --  user interaction. The verification back-end already takes care
         --  of qualifying names when needed.

         when N_Block_Statement
            | N_Entry_Declaration
            | N_Package_Body
            | N_Package_Declaration
            | N_Protected_Type_Declaration
            | N_Subprogram_Body
            | N_Task_Type_Declaration
         =>
            Qualify_Entity_Names (N);

         --  Replace occurrences of System'To_Address by calls to
         --  System.Storage_Elements.To_Address.

         when N_Attribute_Reference =>
            Expand_SPARK_N_Attribute_Reference (N);

         when N_Expanded_Name
            | N_Identifier
         =>
            Expand_SPARK_Potential_Renaming (N);

         --  Loop iterations over arrays need to be expanded, to avoid getting
         --  two names referring to the same object in memory (the array and
         --  the iterator) in GNATprove, especially since both can be written
         --  (thus possibly leading to interferences due to aliasing). No such
         --  problem arises with quantified expressions over arrays, which are
         --  dealt with specially in GNATprove.

         when N_Loop_Statement =>
            Expand_SPARK_N_Loop_Statement (N);

         when N_Object_Declaration =>
            Expand_SPARK_N_Object_Declaration (N);

         when N_Object_Renaming_Declaration =>
            Expand_SPARK_N_Object_Renaming_Declaration (N);

         when N_Op_Ne =>
            Expand_SPARK_N_Op_Ne (N);

         when N_Freeze_Entity =>
            if Is_Type (Entity (N)) then
               Expand_SPARK_N_Freeze_Type (Entity (N));
            end if;

         when N_Indexed_Component =>
            Expand_SPARK_N_Indexed_Component (N);

         when N_Selected_Component =>
            Expand_SPARK_N_Selected_Component (N);

         --  In SPARK mode, no other constructs require expansion

         when others =>
            null;
      end case;
   end Expand_SPARK;

   --------------------------------
   -- Expand_SPARK_N_Freeze_Type --
   --------------------------------

   procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
   begin
      --  When a DIC is inherited by a tagged type, it may need to be
      --  specialized to the descendant type, hence build a separate DIC
      --  procedure for it as done during regular expansion for compilation.

      if Has_DIC (E) and then Is_Tagged_Type (E) then
         Build_DIC_Procedure_Body (E, For_Freeze => True);
      end if;
   end Expand_SPARK_N_Freeze_Type;

   ----------------------------------------
   -- Expand_SPARK_N_Attribute_Reference --
   ----------------------------------------

   procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
      Aname   : constant Name_Id      := Attribute_Name (N);
      Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
      Loc     : constant Source_Ptr   := Sloc (N);
      Typ     : constant Entity_Id    := Etype (N);
      Expr    : Node_Id;

   begin
      if Attr_Id = Attribute_To_Address then

         --  Extract and convert argument to expected type for call

         Expr :=
           Make_Type_Conversion (Loc,
             Subtype_Mark =>
               New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
             Expression   => Relocate_Node (First (Expressions (N))));

         --  Replace attribute reference with call

         Rewrite (N,
           Make_Function_Call (Loc,
             Name                   =>
               New_Occurrence_Of (RTE (RE_To_Address), Loc),
             Parameter_Associations => New_List (Expr)));
         Analyze_And_Resolve (N, Typ);

      --  For attributes which return Universal_Integer, introduce a conversion
      --  to the expected type with the appropriate check flags set.

      elsif Attr_Id = Attribute_Alignment
        or else Attr_Id = Attribute_Bit
        or else Attr_Id = Attribute_Bit_Position
        or else Attr_Id = Attribute_Descriptor_Size
        or else Attr_Id = Attribute_First_Bit
        or else Attr_Id = Attribute_Last_Bit
        or else Attr_Id = Attribute_Length
        or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
        or else Attr_Id = Attribute_Pos
        or else Attr_Id = Attribute_Position
        or else Attr_Id = Attribute_Range_Length
        or else Attr_Id = Attribute_Object_Size
        or else Attr_Id = Attribute_Size
        or else Attr_Id = Attribute_Value_Size
        or else Attr_Id = Attribute_VADS_Size
        or else Attr_Id = Attribute_Aft
        or else Attr_Id = Attribute_Max_Alignment_For_Allocation
      then
         --  If the expected type is Long_Long_Integer, there will be no check
         --  flag as the compiler assumes attributes always fit in this type.
         --  Since in SPARK_Mode we do not take Storage_Error into account, we
         --  cannot make this assumption and need to produce a check.
         --  ??? It should be enough to add this check for attributes 'Length
         --  and 'Range_Length when the type is as big as Long_Long_Integer.

         declare
            Typ : Entity_Id := Empty;
         begin
            if Attr_Id = Attribute_Range_Length then
               Typ := Etype (Prefix (N));

            elsif Attr_Id = Attribute_Length then
               Typ := Etype (Prefix (N));

               declare
                  Indx : Node_Id;
                  J    : Int;

               begin
                  if Is_Access_Type (Typ) then
                     Typ := Designated_Type (Typ);
                  end if;

                  if No (Expressions (N)) then
                     J := 1;
                  else
                     J := UI_To_Int (Expr_Value (First (Expressions (N))));
                  end if;

                  Indx := First_Index (Typ);
                  while J > 1 loop
                     Next_Index (Indx);
                     J := J - 1;
                  end loop;

                  Typ := Etype (Indx);
               end;
            end if;

            Apply_Universal_Integer_Attribute_Checks (N);

            if Present (Typ)
              and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
            then
               Set_Do_Overflow_Check (N);
            end if;
         end;
      end if;
   end Expand_SPARK_N_Attribute_Reference;

   -----------------------------------
   -- Expand_SPARK_N_Loop_Statement --
   -----------------------------------

   procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
      Scheme : constant Node_Id := Iteration_Scheme (N);

   begin
      --  Loop iterations over arrays need to be expanded, to avoid getting
      --  two names referring to the same object in memory (the array and the
      --  iterator) in GNATprove, especially since both can be written (thus
      --  possibly leading to interferences due to aliasing). No such problem
      --  arises with quantified expressions over arrays, which are dealt with
      --  specially in GNATprove.

      if Present (Scheme)
        and then Present (Iterator_Specification (Scheme))
        and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
      then
         Expand_Iterator_Loop_Over_Array (N);
      end if;
   end Expand_SPARK_N_Loop_Statement;

   --------------------------------------
   -- Expand_SPARK_N_Indexed_Component --
   --------------------------------------

   procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is
      Pref : constant Node_Id    := Prefix (N);
      Typ  : constant Entity_Id  := Etype (Pref);

   begin
      if Is_Access_Type (Typ) then
         Insert_Explicit_Dereference (Pref);
         Analyze_And_Resolve (Pref, Designated_Type (Typ));
      end if;
   end Expand_SPARK_N_Indexed_Component;

   ---------------------------------------
   -- Expand_SPARK_N_Object_Declaration --
   ---------------------------------------

   procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
      Loc    : constant Source_Ptr := Sloc (N);
      Obj_Id : constant Entity_Id  := Defining_Identifier (N);
      Typ    : constant Entity_Id  := Etype (Obj_Id);

      Call : Node_Id;

   begin
      --  If the object declaration denotes a variable without initialization
      --  whose type is subject to pragma Default_Initial_Condition, create
      --  and analyze a dummy call to the DIC procedure of the type in order
      --  to detect potential elaboration issues.

      if Comes_From_Source (Obj_Id)
        and then Ekind (Obj_Id) = E_Variable
        and then Has_DIC (Typ)
        and then Present (DIC_Procedure (Typ))
        and then not Has_Init_Expression (N)
      then
         Call := Build_DIC_Call (Loc, Obj_Id, Typ);

         --  Partially insert the call into the tree by setting its parent
         --  pointer.

         Set_Parent (Call, N);
         Analyze (Call);
      end if;
   end Expand_SPARK_N_Object_Declaration;

   ------------------------------------------------
   -- Expand_SPARK_N_Object_Renaming_Declaration --
   ------------------------------------------------

   procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
      CFS    : constant Boolean    := Comes_From_Source (N);
      Loc    : constant Source_Ptr := Sloc (N);
      Obj_Id : constant Entity_Id  := Defining_Entity (N);
      Nam    : constant Node_Id    := Name (N);
      Typ    : constant Entity_Id  := Etype (Obj_Id);

   begin
      --  Transform a renaming of the form

      --    Obj_Id : <subtype mark> renames <function call>;

      --  into

      --    Obj_Id : constant <subtype mark> := <function call>;

      --  Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
      --  a temporary to capture the function result. Once potential renamings
      --  are rewritten for SPARK, the temporary may be leaked out into source
      --  constructs and lead to confusing error diagnostics. Using an object
      --  declaration prevents this unwanted side effect.

      if Nkind (Nam) = N_Function_Call then
         Rewrite (N,
           Make_Object_Declaration (Loc,
             Defining_Identifier => Obj_Id,
             Constant_Present    => True,
             Object_Definition   => New_Occurrence_Of (Typ, Loc),
             Expression          => Nam));

         --  Inherit the original Comes_From_Source status of the renaming

         Set_Comes_From_Source (N, CFS);

         --  Sever the link to the renamed function result because the entity
         --  will no longer alias anything.

         Set_Renamed_Object (Obj_Id, Empty);

         --  Remove the entity of the renaming declaration from visibility as
         --  the analysis of the object declaration will reintroduce it again.

         Remove_Entity_And_Homonym (Obj_Id);
         Analyze (N);

      --  Otherwise unconditionally remove all side effects from the name

      else
         Evaluate_Name (Nam);
      end if;
   end Expand_SPARK_N_Object_Renaming_Declaration;

   --------------------------
   -- Expand_SPARK_N_Op_Ne --
   --------------------------

   procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
      Typ : constant Entity_Id := Etype (Left_Opnd (N));

   begin
      --  Case of elementary type with standard operator

      if Is_Elementary_Type (Typ)
        and then Sloc (Entity (N)) = Standard_Location
      then
         null;

      else
         Exp_Ch4.Expand_N_Op_Ne (N);
      end if;
   end Expand_SPARK_N_Op_Ne;

   -------------------------------------
   -- Expand_SPARK_Potential_Renaming --
   -------------------------------------

   procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
      function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
      --  Determine whether arbitrary node Nod appears within a significant
      --  pragma for SPARK.

      -----------------------------
      -- In_Insignificant_Pragma --
      -----------------------------

      function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
         Par : Node_Id;

      begin
         --  Climb the parent chain looking for an enclosing pragma

         Par := Nod;
         while Present (Par) loop
            if Nkind (Par) = N_Pragma then
               return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));

            --  Prevent the search from going too far

            elsif Is_Body_Or_Package_Declaration (Par) then
               exit;
            end if;

            Par := Parent (Par);
         end loop;

         return False;
      end In_Insignificant_Pragma;

      --  Local variables

      Loc    : constant Source_Ptr := Sloc (N);
      Obj_Id : constant Entity_Id  := Entity (N);
      Typ    : constant Entity_Id  := Etype (N);
      Ren    : Node_Id;

   --  Start of processing for Expand_SPARK_Potential_Renaming

   begin
      --  Replace a reference to a renaming with the actual renamed object

      if Ekind (Obj_Id) in Object_Kind then
         Ren := Renamed_Object (Obj_Id);

         if Present (Ren) then

            --  Do not process a reference when it appears within a pragma of
            --  no significance to SPARK. It is assumed that the replacement
            --  will violate the semantics of the pragma and cause a spurious
            --  error.

            if In_Insignificant_Pragma (N) then
               return;

            --  Instantiations and inlining of subprograms employ "prologues"
            --  which map actual to formal parameters by means of renamings.
            --  Replace a reference to a formal by the corresponding actual
            --  parameter.

            elsif Nkind (Ren) in N_Entity then
               Rewrite (N, New_Occurrence_Of (Ren, Loc));

            --  Otherwise the renamed object denotes a name

            else
               Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
               Reset_Analyzed_Flags (N);
            end if;

            Analyze_And_Resolve (N, Typ);
         end if;
      end if;
   end Expand_SPARK_Potential_Renaming;

   ---------------------------------------
   -- Expand_SPARK_N_Selected_Component --
   ---------------------------------------

   procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is
      Pref : constant Node_Id   := Prefix (N);
      Typ  : constant Entity_Id := Underlying_Type (Etype (Pref));

   begin
      if Present (Typ) and then Is_Access_Type (Typ) then

         --  First set prefix type to proper access type, in case it currently
         --  has a private (non-access) view of this type.

         Set_Etype (Pref, Typ);

         Insert_Explicit_Dereference (Pref);
         Analyze_And_Resolve (Pref, Designated_Type (Typ));

         if Ekind (Etype (Pref)) = E_Private_Subtype
           and then Is_For_Access_Subtype (Etype (Pref))
         then
            Set_Etype (Pref, Base_Type (Etype (Pref)));
         end if;
      end if;
   end Expand_SPARK_N_Selected_Component;

end Exp_SPARK;