gcc/ada/sem_spark.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                            S E M _ S P A R K                             --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --              Copyright (C) 2017-2019, 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 --  This package implements an ownership analysis for access types. The rules
  27 --  that are enforced are defined in section 3.10 of the SPARK Reference
  28 --  Manual.
  29 --
  30 --  Check_Safe_Pointers is called by Gnat1drv, when GNATprove mode is
  31 --  activated. It does an analysis of the source code, looking for code that is
  32 --  considered as SPARK and launches another function called Analyze_Node that
  33 --  will do the whole analysis.
  34 --
  35 --  A path is an abstraction of a name, of which all indices, slices (for
  36 --  indexed components) and function calls have been abstracted and all
  37 --  dereferences are made explicit. A path is the atomic element viewed by the
  38 --  analysis, with the notion of prefixes and extensions of different paths.
  39 --
  40 --  The analysis explores the AST, and looks for different constructs
  41 --  that may involve aliasing. These main constructs are assignments
  42 --  (N_Assignment_Statement, N_Object_Declaration, ...), or calls
  43 --  (N_Procedure_Call_Statement, N_Entry_Call_Statement, N_Function_Call).
  44 --  The analysis checks the permissions of each construct and updates them
  45 --  according to the SPARK RM. This can follow three main different types
  46 --  of operations: move, borrow, and observe.
  47
  48 ----------------------------
  49 -- Deep and shallow types --
  50 ----------------------------
  51
  52 --  The analysis focuses on objects that can cause problems in terms of pointer
  53 --  aliasing. These objects have types that are called deep. Deep types are
  54 --  defined as being either types with an access part or class-wide types
  55 --  (which may have an access part in a derived type). Non-deep types are
  56 --  called shallow. Some objects of shallow type may cause pointer aliasing
  57 --  problems when they are explicitely marked as aliased (and then the aliasing
  58 --  occurs when we take the Access to this object and store it in a pointer).
  59
  60 ----------
  61 -- Move --
  62 ----------
  63
  64 --  Moves can happen at several points in the program: during assignment (and
  65 --  any similar statement such as object declaration with initial value), or
  66 --  during return statements.
  67 --
  68 --  The underlying concept consists of transferring the ownership of any path
  69 --  on the right-hand side to the left-hand side. There are some details that
  70 --  should be taken into account so as not to transfer paths that appear only
  71 --  as intermediate results of a more complex expression.
  72
  73 --  More specifically, the SPARK RM defines moved expressions, and any moved
  74 --  expression that points directly to a path is then checked and sees its
  75 --  permissions updated accordingly.
  76
  77 ------------
  78 -- Borrow --
  79 ------------
  80
  81 --  Borrows can happen in subprogram calls. They consist of a temporary
  82 --  transfer of ownership from a caller to a callee. Expressions that can be
  83 --  borrowed can be found in either procedure or entry actual parameters, and
  84 --  consist of parameters of mode either "out" or "in out", or parameters of
  85 --  mode "in" that are of type nonconstant access-to-variable. We consider
  86 --  global variables as implicit parameters to subprograms, with their mode
  87 --  given by the Global contract associated to the subprogram. Note that the
  88 --  analysis looks for such a Global contract mentioning any global variable
  89 --  of deep type accessed directly in the subprogram, and it raises an error if
  90 --  there is no Global contract, or if the Global contract does not mention the
  91 --  variable.
  92 --
  93 --  A borrow of a parameter X is equivalent in terms of aliasing to moving
  94 --  X'Access to the callee, and then assigning back X at the end of the call.
  95 --
  96 --  Borrowed parameters should have read-write permission (or write-only for
  97 --  "out" parameters), and should all have read-write permission at the end
  98 --  of the call (this guarantee is ensured by the callee).
  99
 100 -------------
 101 -- Observe --
 102 -------------
 103
 104 --  Observed parameters are all the other parameters that are not borrowed and
 105 --  that may cause problems with aliasing. They are considered as being sent to
 106 --  the callee with Read-Only permission, so that they can be aliased safely.
 107 --  This is the only construct that allows aliasing that does not prevent
 108 --  accessing the old path that is being aliased. However, this comes with
 109 --  the restriction that those aliased path cannot be written in the callee.
 110
 111 --------------------
 112 -- Implementation --
 113 --------------------
 114
 115 --  The implementation is based on trees that represent the possible paths
 116 --  in the source code. Those trees can be unbounded in depth, hence they are
 117 --  represented using lazy data structures, whose laziness is handled manually.
 118 --  Each time an identifier is declared, its path is added to the permission
 119 --  environment as a tree with only one node, the declared identifier. Each
 120 --  time a path is checked or updated, we look in the tree at the adequate
 121 --  node, unfolding the tree whenever needed.
 122
 123 --  For this, each node has several variables that indicate whether it is
 124 --  deep (Is_Node_Deep), what permission it has (Permission), and what is
 125 --  the lowest permission of all its descendants (Children_Permission). After
 126 --  unfolding the tree, we update the permissions of each node, deleting the
 127 --  Children_Permission, and specifying new ones for the leaves of the unfolded
 128 --  tree.
 129
 130 --  After assigning a path, the descendants of the assigned path are dumped
 131 --  (and hence the tree is folded back), given that all descendants directly
 132 --  get read-write permission, which can be specified using the node's
 133 --  Children_Permission field.
 134
 135 --  The implementation is done as a generic, so that GNATprove can instantiate
 136 --  it with suitable formal arguments that depend on the SPARK_Mode boundary
 137 --  as well as the two-phase architecture of GNATprove (which runs the GNAT
 138 --  front end twice, once for global generation and once for analysis).
 139
 140 with Types; use Types;
 141
 142 generic
 143    with function Retysp (X : Entity_Id) return Entity_Id;
 144    --  Return the representative type in SPARK for a type.
 145
 146    with function Component_Is_Visible_In_SPARK (C : Entity_Id) return Boolean;
 147    --  Return whether a component is visible in SPARK. No aliasing check is
 148    --  performed for a component that is visible.
 149
 150    with function Emit_Messages return Boolean;
 151    --  Return True when error messages should be emitted.
 152
 153    with function Is_Pledge_Function (E : Entity_Id) return Boolean;
 154    --  Return True if E is annotated with a pledge annotation
 155
 156 package Sem_SPARK is
 157
 158    function Is_Legal (N : Node_Id) return Boolean;
 159    --  Test the legality of a node wrt ownership-checking rules. This does not
 160    --  check rules related to the validity of permissions associated with paths
 161    --  from objects, so that it can be called from GNATprove on code of library
 162    --  units analyzed in SPARK_Mode Auto.
 163
 164    procedure Check_Safe_Pointers (N : Node_Id);
 165    --  The entry point of this package. It analyzes a node and reports errors
 166    --  when there are violations of ownership rules.
 167
 168    function Is_Deep (Typ : Entity_Id) return Boolean;
 169    --  A function that can tell whether a type is deep. Returns True if the
 170    --  type passed as argument is deep.
 171
 172    function Is_Traversal_Function (E : Entity_Id) return Boolean;
 173
 174    function Is_Local_Context (Scop : Entity_Id) return Boolean;
 175    --  Return if a given scope defines a local context where it is legal to
 176    --  declare a variable of anonymous access type.
 177
 178 end Sem_SPARK;