|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- S E M _ S P A R K --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
131
|
9 -- Copyright (C) 2017-2018, Free Software Foundation, Inc. --
|
|
111
|
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 --
|
|
131
|
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.
|
|
111
|
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 with Types; use Types;
|
|
|
136
|
|
|
137 package 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
|
|
|
143 end Sem_SPARK;
|
