[multiple changes]

2017-09-12  Bob Duff  <duff@adacore.com>

	* sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to
	Empty.

2017-09-12  Georges-Axel Jaloyan  <jaloyan@adacore.com>

	* debug.adb: Reserving flag -gnatdF for safe pointer checking.
	* gnat1drv.adb (gnat1drv): Adding the call to the analysis on
	dF flag.
	* sem_spark.adb, sem_spark.ads: Implementation of the analysis,
	in preparation for the evolution of the SPARK language that
	includes a pointer analysis for checking non-aliasing of access
	types. The Check_Safe_Pointers function is the entry point, and
	will traverse the AST and raise compile-time errors everytime
	it detects non-begign aliasing.  Detailed comments are present
	in the sem_spark.ads file.
	* sem_util.adb, sem_util.ads (First_Global, Next_Global): New
	functions to iterate over the list of globals of a subprogram.
	* libgnat/system.ads: Add restriction No_Finalization.
	* gcc-interface/Make-lang.in: Add new file sem_spark.adb and
	dependency on g-dynhta.adb.

From-SVN: r252000

gcc/ada/ChangeLog

 2017-09-12  Bob Duff  <duff@adacore.com>
 
+	* sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to
+	Empty.
+
+2017-09-12  Georges-Axel Jaloyan  <jaloyan@adacore.com>
+
+	* debug.adb: Reserving flag -gnatdF for safe pointer checking.
+	* gnat1drv.adb (gnat1drv): Adding the call to the analysis on
+	dF flag.
+	* sem_spark.adb, sem_spark.ads: Implementation of the analysis,
+	in preparation for the evolution of the SPARK language that
+	includes a pointer analysis for checking non-aliasing of access
+	types. The Check_Safe_Pointers function is the entry point, and
+	will traverse the AST and raise compile-time errors everytime
+	it detects non-begign aliasing.  Detailed comments are present
+	in the sem_spark.ads file.
+	* sem_util.adb, sem_util.ads (First_Global, Next_Global): New
+	functions to iterate over the list of globals of a subprogram.
+	* libgnat/system.ads: Add restriction No_Finalization.
+	* gcc-interface/Make-lang.in: Add new file sem_spark.adb and
+	dependency on g-dynhta.adb.
+
+2017-09-12  Bob Duff  <duff@adacore.com>
+
 	* sem_ch6.adb (Analyze_Expression_Function): Call
 	Check_Dynamically_Tagged_Expression.
 	* sem_util.adb (Check_Dynamically_Tagged_Expression): Remove

gcc/ada/debug.adb

@@ -69,7 +69,7 @@ package body Debug is
    --  dC   Output debugging information on check suppression
    --  dD   Delete elaboration checks in inner level routines
    --  dE   Apply elaboration checks to predefined units
-   --  dF
+   --  dF   Perform the new SPARK checking rules for pointer aliasing
    --  dG   Generate all warnings including those normally suppressed
    --  dH   Hold (kill) call to gigi
    --  dI   Inhibit internal name numbering in gnatG listing
@@ -383,6 +383,11 @@ package body Debug is
    --  dE   Apply compile time elaboration checking for with relations between
    --       predefined units. Normally no checks are made.
 
+   --  dF   Perform the new SPARK checking rules for pointer aliasing. This is
+   --       only activated in GNATprove mode and on SPARK code. These rules are
+   --       not yet part of the official SPARK language, but are expected to be
+   --       included in a future version of SPARK.
+
    --  dG   Generate all warnings. Normally Errout suppresses warnings on
    --       units that are not part of the main extended source, and also
    --       suppresses warnings on instantiations in the main extended

gcc/ada/gcc-interface/Make-lang.in

@@ -312,6 +312,7 @@ GNAT_ADA_OBJS =	\
  ada/freeze.o	\
  ada/frontend.o	\
  ada/libgnat/g-byorma.o	\
+ ada/libgnat/g-dynhta.o	\
  ada/libgnat/g-hesora.o	\
  ada/libgnat/g-htable.o	\
  ada/libgnat/g-spchge.o	\
@@ -443,6 +444,7 @@ GNAT_ADA_OBJS =	\
  ada/sem_res.o	\
  ada/sem_scil.o	\
  ada/sem_smem.o	\
+ ada/sem_spark.o	\
  ada/sem_type.o	\
  ada/sem_util.o	\
  ada/sem_warn.o	\

gcc/ada/gnat1drv.adb

@@ -61,6 +61,7 @@ with Sem_Ch12;
 with Sem_Ch13;
 with Sem_Elim;
 with Sem_Eval;
+with Sem_SPARK; use Sem_SPARK;
 with Sem_Type;
 with Set_Targ;
 with Sinfo;    use Sinfo;
@@ -1449,12 +1450,19 @@ begin
 
       Prepcomp.Add_Dependencies;
 
-      --  In gnatprove mode we're writing the ALI much earlier than usual
-      --  as flow analysis needs the file present in order to append its
-      --  own globals to it.
-
       if GNATprove_Mode then
 
+         --  Perform the new SPARK checking rules for pointer aliasing. This is
+         --  only activated in GNATprove mode and on SPARK code.
+
+         if Debug_Flag_FF then
+            Check_Safe_Pointers (Main_Unit_Node);
+         end if;
+
+         --  In GNATprove mode we're writing the ALI much earlier than usual
+         --  as flow analysis needs the file present in order to append its
+         --  own globals to it.
+
          --  Note: In GNATprove mode, an "object" file is always generated as
          --  the result of calling gnat1 or gnat2why, although this is not the
          --  same as the object file produced for compilation.

gcc/ada/libgnat/system.ads

@@ -44,6 +44,12 @@ pragma Restrictions (No_Implicit_Dynamic_Code);
 --  which prevent execution of code on the stack, e.g. in windows environments
 --  with DEP (Data Execution Protection) enabled.
 
+pragma Restrictions (No_Finalization);
+--  Use restriction No_Finalization to avoid pulling finalization (not allowed
+--  in GNAT) inside sem_spark.adb, when defining type Perm_Tree_Access as an
+--  access type on incomplete type Perm_Tree_Wrapper (which is required for
+--  defining a recursive type).
+
 package System is
    pragma Pure;
    --  Note that we take advantage of the implementation permission to make

gcc/ada/sem_ch6.adb

@@ -466,7 +466,7 @@ package body Sem_Ch6 is
       Orig_N   : Node_Id;
       Ret      : Node_Id;
 
-      Def_Id   : Entity_Id;
+      Def_Id   : Entity_Id := Empty;
       Prev     : Entity_Id;
       --  If the expression is a completion, Prev is the entity whose
       --  declaration is completed. Def_Id is needed to analyze the spec.

gcc/ada/sem_spark.ads

+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                            S E M _ S P A R K                             --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--              Copyright (C) 2017, 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.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package implements an anti-aliasing analysis for access types. The
+--  rules that are enforced are defined in the anti-aliasing section of the
+--  SPARK RM 6.4.2
+--
+--  Analyze_SPARK is called by Gnat1drv, when GNATprove mode is activated. It
+--  does an analysis of the source code, looking for code that is considered
+--  as SPARK and launches another function called Analyze_Node that will do
+--  the whole analysis.
+--
+--  A path is an abstraction of a name, of which all indices, slices (for
+--  indexed components) and function calls have been abstracted and all
+--  dereferences are made explicit. A path is the atomic element viewed by the
+--  analysis, with the notion of prefixes and extensions of different paths.
+--
+--  The analysis explores the AST, and looks for different constructs
+--  that may involve aliasing. These main constructs are assignments
+--  (N_Assignment_Statement, N_Object_Declaration, ...), or calls
+--  (N_Procedure_Call_Statement, N_Entry_Call_Statement, N_Function_Call).
+--  The analysis checks the permissions of each construct and updates them
+--  according to the SPARK RM. This can follow three main different types
+--  of operations: move, borrow, and observe.
+
+----------------------------
+-- Deep and shallow types --
+----------------------------
+
+--  The analysis focuses on objects that can cause problems in terms of pointer
+--  aliasing. These objects have types that are called deep. Deep types are
+--  defined as being either types with an access part or class-wide types
+--  (which may have an access part in a derived type). Non-deep types are
+--  called shallow. Some objects of shallow type may cause pointer aliasing
+--  problems when they are explicitely marked as aliased (and then the aliasing
+--  occurs when we take the Access to this object and store it in a pointer).
+
+----------
+-- Move --
+----------
+
+--  Moves can happen at several points in the program: during assignment (and
+--  any similar statement such as object declaration with initial value), or
+--  during return statements.
+--
+--  The underlying concept consists of transferring the ownership of any path
+--  on the right-hand side to the left-hand side. There are some details that
+--  should be taken into account so as not to transfer paths that appear only
+--  as intermediate results of a more complex expression.
+
+--  More specifically, the SPARK RM defines moved expressions, and any moved
+--  expression that points directly to a path is then checked and sees its
+--  permissions updated accordingly.
+
+------------
+-- Borrow --
+------------
+
+--  Borrows can happen in subprogram calls. They consist of a temporary
+--  transfer of ownership from a caller to a callee. Expressions that can be
+--  borrowed can be found in either procedure or entry actual parameters, and
+--  consist of parameters of mode either "out" or "in out", or parameters of
+--  mode "in" that are of type nonconstant access-to-variable. We consider
+--  global variables as implicit parameters to subprograms, with their mode
+--  given by the Global contract associated to the subprogram. Note that the
+--  analysis looks for such a Global contract mentioning any global variable
+--  of deep type accessed directly in the subprogram, and it raises an error if
+--  there is no Global contract, or if the Global contract does not mention the
+--  variable.
+--
+--  A borrow of a parameter X is equivalent in terms of aliasing to moving
+--  X'Access to the callee, and then assigning back X at the end of the call.
+--
+--  Borrowed parameters should have read-write permission (or write-only for
+--  "out" parameters), and should all have read-write permission at the end
+--  of the call (this guarantee is ensured by the callee).
+
+-------------
+-- Observe --
+-------------
+
+--  Observed parameters are all the other parameters that are not borrowed and
+--  that may cause problems with aliasing. They are considered as being sent to
+--  the callee with Read-Only permission, so that they can be aliased safely.
+--  This is the only construct that allows aliasing that does not prevent
+--  accessing the old path that is being aliased. However, this comes with
+--  the restriction that those aliased path cannot be written in the callee.
+
+--------------------
+-- Implementation --
+--------------------
+
+--  The implementation is based on trees that represent the possible paths
+--  in the source code. Those trees can be unbounded in depth, hence they are
+--  represented using lazy data structures, whose laziness is handled manually.
+--  Each time an identifier is declared, its path is added to the permission
+--  environment as a tree with only one node, the declared identifier. Each
+--  time a path is checked or updated, we look in the tree at the adequate
+--  node, unfolding the tree whenever needed.
+
+--  For this, each node has several variables that indicate whether it is
+--  deep (Is_Node_Deep), what permission it has (Permission), and what is
+--  the lowest permission of all its descendants (Children_Permission). After
+--  unfolding the tree, we update the permissions of each node, deleting the
+--  Children_Permission, and specifying new ones for the leaves of the unfolded
+--  tree.
+
+--  After assigning a path, the descendants of the assigned path are dumped
+--  (and hence the tree is folded back), given that all descendants directly
+--  get read-write permission, which can be specified using the node's
+--  Children_Permission field.
+
+with Types; use Types;
+
+package Sem_SPARK is
+
+   procedure Check_Safe_Pointers (N : Node_Id);
+   --  The entry point of this package. It analyzes a node and reports errors
+   --  when there are violations of aliasing rules.
+
+end Sem_SPARK;

gcc/ada/sem_util.adb

@@ -8093,6 +8093,124 @@ package body Sem_Util is
       end if;
    end First_Actual;
 
+   ------------------
+   -- First_Global --
+   ------------------
+
+   function First_Global
+     (Subp        : Entity_Id;
+      Global_Mode : Name_Id;
+      Refined     : Boolean := False) return Node_Id
+   is
+      function First_From_Global_List
+        (List        : Node_Id;
+         Global_Mode : Name_Id := Name_Input) return Entity_Id;
+      --  Get the first item with suitable mode from List
+
+      ----------------------------
+      -- First_From_Global_List --
+      ----------------------------
+
+      function First_From_Global_List
+        (List        : Node_Id;
+         Global_Mode : Name_Id := Name_Input) return Entity_Id
+      is
+         Assoc : Node_Id;
+
+      begin
+         --  Empty list (no global items)
+
+         if Nkind (List) = N_Null then
+            return Empty;
+
+         --  Single global item declaration (only input items)
+
+         elsif Nkind_In (List, N_Expanded_Name,
+                               N_Identifier,
+                               N_Selected_Component)
+         then
+            if Global_Mode = Name_Input then
+               return List;
+            else
+               return Empty;
+            end if;
+
+         --  Simple global list (only input items) or moded global list
+         --  declaration.
+
+         elsif Nkind (List) = N_Aggregate then
+            if Present (Expressions (List)) then
+               if Global_Mode = Name_Input then
+                  return First (Expressions (List));
+               else
+                  return Empty;
+               end if;
+
+            else
+               Assoc := First (Component_Associations (List));
+               while Present (Assoc) loop
+
+                  --  When we find the desired mode in an association, call
+                  --  recursively First_From_Global_List as if the mode was
+                  --  Name_Input, in order to reuse the existing machinery
+                  --  for the other cases.
+
+                  if Chars (First (Choices (Assoc))) = Global_Mode then
+                     return First_From_Global_List (Expression (Assoc));
+                  end if;
+
+                  Next (Assoc);
+               end loop;
+
+               return Empty;
+            end if;
+
+            --  To accommodate partial decoration of disabled SPARK features,
+            --  this routine may be called with illegal input. If this is the
+            --  case, do not raise Program_Error.
+
+         else
+            return Empty;
+         end if;
+      end First_From_Global_List;
+
+      --  Local variables
+
+      Global  : Node_Id := Empty;
+      Body_Id : Entity_Id;
+
+   begin
+      pragma Assert (Global_Mode = Name_Input
+                      or else Global_Mode = Name_Output
+                      or else Global_Mode = Name_In_Out
+                      or else Global_Mode = Name_Proof_In);
+
+      --  Retrieve the suitable pragma Global or Refined_Global. In the second
+      --  case, it can only be located on the body entity.
+
+      if Refined then
+         Body_Id := Subprogram_Body_Entity (Subp);
+         if Present (Body_Id) then
+            Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
+         end if;
+      else
+         Global := Get_Pragma (Subp, Pragma_Global);
+      end if;
+
+      --  No corresponding global if pragma is not present
+
+      if No (Global) then
+         return Empty;
+
+      --  Otherwise retrieve the corresponding list of items depending on the
+      --  Global_Mode.
+
+      else
+         return First_From_Global_List
+           (Expression (Get_Argument (Global, Subp)), Global_Mode);
+      end if;
+   end First_Global;
+
    -------------
    -- Fix_Msg --
    -------------
@@ -18980,6 +19098,27 @@ package body Sem_Util is
       Actual_Id := Next_Actual (Actual_Id);
    end Next_Actual;
 
+   -----------------
+   -- Next_Global --
+   -----------------
+
+   function Next_Global (Node : Node_Id) return Node_Id is
+   begin
+      --  The global item may either be in a list, or by itself, in which case
+      --  there is no next global item with the same mode.
+
+      if Is_List_Member (Node) then
+         return Next (Node);
+      else
+         return Empty;
+      end if;
+   end Next_Global;
+
+   procedure Next_Global (Node : in out Node_Id) is
+   begin
+      Node := Next_Global (Node);
+   end Next_Global;
+
    ----------------------------------
    -- New_Requires_Transient_Scope --
    ----------------------------------

gcc/ada/sem_util.ads

@@ -885,6 +885,17 @@ package Sem_Util is
    --  Note that the value returned is always the expression (not the
    --  N_Parameter_Association nodes, even if named association is used).
 
+   function First_Global
+     (Subp        : Entity_Id;
+      Global_Mode : Name_Id;
+      Refined     : Boolean := False) return Node_Id;
+   --  Returns the first global item of mode Global_Mode (which can be
+   --  Name_Input, Name_Output, Name_In_Out or Name_Proof_In) associated to
+   --  subprogram Subp, or Empty otherwise. If Refined is True, the global item
+   --  is retrieved from the Refined_Global aspect/pragma associated to the
+   --  body of Subp if present. Next_Global can be used to get the next global
+   --  item with the same mode.
+
    function Fix_Msg (Id : Entity_Id; Msg : String) return String;
    --  Replace all occurrences of a particular word in string Msg depending on
    --  the Ekind of Id as follows:
@@ -2177,6 +2188,16 @@ package Sem_Util is
    --  Note that the result produced is always an expression, not a parameter
    --  association node, even if named notation was used.
 
+   procedure Next_Global (Node : in out Node_Id);
+   pragma Inline (Next_Actual);
+   --  Next_Global (N) is equivalent to N := Next_Global (N). Note that we
+   --  inline this procedural form, but not the functional form that follows.
+
+   function Next_Global (Node : Node_Id) return Node_Id;
+   --  Node is a global item from a list, obtained through calling First_Global
+   --  and possibly Next_Global a number of times. Returns the next global item
+   --  with the same mode.
+
    function No_Heap_Finalization (Typ : Entity_Id) return Boolean;
    --  Determine whether type Typ is subject to pragma No_Heap_Finalization