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-2018, 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 anti-aliasing analysis for access types. The
27--  rules that are enforced are defined in the anti-aliasing section of the
28--  SPARK RM 6.4.2
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
135with Types; use Types;
136
137package Sem_SPARK is
138
139   procedure Check_Safe_Pointers (N : Node_Id);
140   --  The entry point of this package. It analyzes a node and reports errors
141   --  when there are violations of aliasing rules.
142
143end Sem_SPARK;
144