@@ -17,7 +17,7 @@ object Nullables with
17
17
import ast .tpd ._
18
18
19
19
/** A set of val or var references that are known to be not null, plus a set of
20
- * variable references that are not known (anymore) to be null
20
+ * variable references that are not known (anymore) to be not null
21
21
*/
22
22
case class NotNullInfo (asserted : Set [TermRef ], retracted : Set [TermRef ])
23
23
assert((asserted & retracted).isEmpty)
@@ -34,7 +34,9 @@ object Nullables with
34
34
this .asserted.union(that.asserted).diff(that.retracted),
35
35
this .retracted.union(that.retracted).diff(that.asserted))
36
36
37
- /** The alternative path combination with another not-null info */
37
+ /** The alternative path combination with another not-null info. Used to merge
38
+ * the nullability info of the two branches of an if.
39
+ */
38
40
def alt (that : NotNullInfo ): NotNullInfo =
39
41
NotNullInfo (this .asserted.intersect(that.asserted), this .retracted.union(that.retracted))
40
42
@@ -99,9 +101,9 @@ object Nullables with
99
101
end TrackedRef
100
102
101
103
/** Is given reference tracked for nullability?
102
- * This is the case if the reference is a path to an immutable val,
103
- * or if it refers to a local mutable variable where all assignments
104
- * to the variable are reachable .
104
+ * This is the case if the reference is a path to an immutable val, or if it refers
105
+ * to a local mutable variable where all assignments to the variable are _reachable_
106
+ * (in the sense of how it is defined in assignmentSpans) .
105
107
*/
106
108
def isTracked (ref : TermRef )(given Context ) =
107
109
ref.isStable
@@ -114,10 +116,17 @@ object Nullables with
114
116
&& curCtx.compilationUnit.assignmentSpans.contains(sym.span.start)
115
117
}
116
118
119
+ /** The nullability context to be used after a case that matches pattern `pat`.
120
+ * If `pat` is `null`, this will assert that the selector `sel` is not null afterwards.
121
+ */
117
122
def afterPatternContext (sel : Tree , pat : Tree )(given ctx : Context ) = (sel, pat) match
118
123
case (TrackedRef (ref), Literal (Constant (null ))) => ctx.addNotNullRefs(Set (ref))
119
124
case _ => ctx
120
125
126
+ /** The nullability context to be used for the guard and rhs of a case with
127
+ * given pattern `pat`. If the pattern can only match non-null values, this
128
+ * will assert that the selector `sel` is not null in these regions.
129
+ */
121
130
def caseContext (sel : Tree , pat : Tree )(given ctx : Context ): Context = sel match
122
131
case TrackedRef (ref) if matchesNotNull(pat) => ctx.addNotNullRefs(Set (ref))
123
132
case _ => ctx
@@ -129,19 +138,26 @@ object Nullables with
129
138
case _ => false
130
139
131
140
given (infos : List [NotNullInfo ])
132
- @ tailRec
133
- def containsRef (ref : TermRef ): Boolean = infos match
141
+
142
+ /** Do the current not-null infos imply that `ref` is not null?
143
+ * Not-null infos are as a history where earlier assertions and retractions replace
144
+ * later ones (i.e. it records the assignment history in reverse, with most recent first)
145
+ */
146
+ @ tailrec def impliesNotNull (ref : TermRef ): Boolean = infos match
134
147
case info :: infos1 =>
135
148
if info.asserted.contains(ref) then true
136
149
else if info.retracted.contains(ref) then false
137
- else containsRef (infos1)(ref)
150
+ else impliesNotNull (infos1)(ref)
138
151
case _ =>
139
152
false
140
153
154
+ /** Add `info` as the most recent entry to the list of null infos. Assertions
155
+ * or retractions in `info` supersede infos in existing entries of `infos`.
156
+ */
141
157
def extendWith (info : NotNullInfo ) =
142
158
if info.isEmpty
143
- || info.asserted.forall(infos.containsRef (_))
144
- && ! info.retracted.exists(infos.containsRef (_))
159
+ || info.asserted.forall(infos.impliesNotNull (_))
160
+ && ! info.retracted.exists(infos.impliesNotNull (_))
145
161
then infos
146
162
else info :: infos
147
163
@@ -245,13 +261,16 @@ object Nullables with
245
261
246
262
/** A map from (name-) offsets of all local variables in this compilation unit
247
263
* that can be tracked for being not null to the list of spans of assignments
248
- * to these variables. A variable can be tracked if it has only reachable assignments.
264
+ * to these variables. A variable can be tracked if it has only reachable assignments
249
265
* An assignment is reachable if the path of tree nodes between the block enclosing
250
266
* the variable declaration to the assignment consists only of if-expressions,
251
267
* while-expressions, block-expressions and type-ascriptions.
252
268
* Only reachable assignments are handled correctly in the nullability analysis.
253
269
* Therefore, variables with unreachable assignments can be assumed to be not-null
254
270
* only if their type asserts it.
271
+ *
272
+ * Note: we the local variables through their offset and not through their name
273
+ * because of shadowing.
255
274
*/
256
275
def assignmentSpans (given Context ): Map [Int , List [Span ]] =
257
276
import ast .untpd ._
@@ -305,7 +324,7 @@ object Nullables with
305
324
306
325
/** The initial context to be used for a while expression with given span.
307
326
* In this context, all variables that are assigned within the while expression
308
- * have their nullability status retracted, i.e. are not known to be null.
327
+ * have their nullability status retracted, i.e. are not known to be not null.
309
328
* While necessary for soundness, this scheme loses precision: Even if
310
329
* the initial state of the variable is not null and all assignments to the variable
311
330
* in the while expression are also known to be not null, the variable is still
@@ -323,8 +342,8 @@ object Nullables with
323
342
*
324
343
* class Links(val elem: T, val next: Links | Null)
325
344
*
326
- * var ys : Links | Null = Links(1, null)
327
- * var xs : Links | Null = xs
345
+ * var xs : Links | Null = Links(1, null)
346
+ * var ys : Links | Null = xs
328
347
* while xs != null
329
348
* ys = Links(xs.elem, ys.next) // error in unrefined: ys is potentially null here
330
349
* xs = xs.next
@@ -334,7 +353,7 @@ object Nullables with
334
353
val sym = ref.symbol
335
354
sym.span.exists
336
355
&& assignmentSpans.getOrElse(sym.span.start, Nil ).exists(whileSpan.contains(_))
337
- && curCtx.notNullInfos.containsRef (ref)
356
+ && curCtx.notNullInfos.impliesNotNull (ref)
338
357
val retractedVars = curCtx.notNullInfos.flatMap(_.asserted.filter(isRetracted)).toSet
339
358
curCtx.addNotNullInfo(NotNullInfo (Set (), retractedVars))
340
359
0 commit comments