]>
Commit | Line | Data |
---|---|---|
faee1e18 | 1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
5 | -- S E M _ S P A R K -- | |
6 | -- -- | |
7 | -- S p e c -- | |
8 | -- -- | |
e9c75a1a | 9 | -- Copyright (C) 2017-2019, Free Software Foundation, Inc. -- |
faee1e18 | 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 | ||
d087b9ca | 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. | |
faee1e18 | 29 | -- |
5bb74b99 | 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. | |
faee1e18 | 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 | ||
1e5359c0 | 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 | ||
faee1e18 | 140 | with Types; use Types; |
141 | ||
1e5359c0 | 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 | ||
a6f3144f | 153 | with function Is_Pledge_Function (E : Entity_Id) return Boolean; |
154 | -- Return True if E is annotated with a pledge annotation | |
155 | ||
faee1e18 | 156 | package Sem_SPARK is |
157 | ||
7bd7174a | 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 | ||
faee1e18 | 164 | procedure Check_Safe_Pointers (N : Node_Id); |
165 | -- The entry point of this package. It analyzes a node and reports errors | |
d087b9ca | 166 | -- when there are violations of ownership rules. |
faee1e18 | 167 | |
1e5359c0 | 168 | function Is_Deep (Typ : Entity_Id) return Boolean; |
7a5b8c31 | 169 | -- Returns True if the type passed as argument is deep |
1e5359c0 | 170 | |
171 | function Is_Traversal_Function (E : Entity_Id) return Boolean; | |
172 | ||
583f62e9 | 173 | function Is_Local_Context (Scop : Entity_Id) return Boolean; |
174 | -- Return if a given scope defines a local context where it is legal to | |
175 | -- declare a variable of anonymous access type. | |
176 | ||
faee1e18 | 177 | end Sem_SPARK; |