@@ -17,7 +17,7 @@ object Nullables with
1717 import ast .tpd ._
1818
1919 /** 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
2121 */
2222 case class NotNullInfo (asserted : Set [TermRef ], retracted : Set [TermRef ])
2323 assert((asserted & retracted).isEmpty)
@@ -34,7 +34,9 @@ object Nullables with
3434 this .asserted.union(that.asserted).diff(that.retracted),
3535 this .retracted.union(that.retracted).diff(that.asserted))
3636
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+ */
3840 def alt (that : NotNullInfo ): NotNullInfo =
3941 NotNullInfo (this .asserted.intersect(that.asserted), this .retracted.union(that.retracted))
4042
@@ -99,9 +101,9 @@ object Nullables with
99101 end TrackedRef
100102
101103 /** 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) .
105107 */
106108 def isTracked (ref : TermRef )(given Context ) =
107109 ref.isStable
@@ -114,10 +116,17 @@ object Nullables with
114116 && curCtx.compilationUnit.assignmentSpans.contains(sym.span.start)
115117 }
116118
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+ */
117122 def afterPatternContext (sel : Tree , pat : Tree )(given ctx : Context ) = (sel, pat) match
118123 case (TrackedRef (ref), Literal (Constant (null ))) => ctx.addNotNullRefs(Set (ref))
119124 case _ => ctx
120125
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+ */
121130 def caseContext (sel : Tree , pat : Tree )(given ctx : Context ): Context = sel match
122131 case TrackedRef (ref) if matchesNotNull(pat) => ctx.addNotNullRefs(Set (ref))
123132 case _ => ctx
@@ -129,19 +138,26 @@ object Nullables with
129138 case _ => false
130139
131140 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
134147 case info :: infos1 =>
135148 if info.asserted.contains(ref) then true
136149 else if info.retracted.contains(ref) then false
137- else containsRef (infos1)(ref)
150+ else impliesNotNull (infos1)(ref)
138151 case _ =>
139152 false
140153
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+ */
141157 def extendWith (info : NotNullInfo ) =
142158 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 (_))
145161 then infos
146162 else info :: infos
147163
@@ -245,13 +261,16 @@ object Nullables with
245261
246262 /** A map from (name-) offsets of all local variables in this compilation unit
247263 * 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
249265 * An assignment is reachable if the path of tree nodes between the block enclosing
250266 * the variable declaration to the assignment consists only of if-expressions,
251267 * while-expressions, block-expressions and type-ascriptions.
252268 * Only reachable assignments are handled correctly in the nullability analysis.
253269 * Therefore, variables with unreachable assignments can be assumed to be not-null
254270 * 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.
255274 */
256275 def assignmentSpans (given Context ): Map [Int , List [Span ]] =
257276 import ast .untpd ._
@@ -305,7 +324,7 @@ object Nullables with
305324
306325 /** The initial context to be used for a while expression with given span.
307326 * 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.
309328 * While necessary for soundness, this scheme loses precision: Even if
310329 * the initial state of the variable is not null and all assignments to the variable
311330 * in the while expression are also known to be not null, the variable is still
@@ -323,8 +342,8 @@ object Nullables with
323342 *
324343 * class Links(val elem: T, val next: Links | Null)
325344 *
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
328347 * while xs != null
329348 * ys = Links(xs.elem, ys.next) // error in unrefined: ys is potentially null here
330349 * xs = xs.next
@@ -334,7 +353,7 @@ object Nullables with
334353 val sym = ref.symbol
335354 sym.span.exists
336355 && assignmentSpans.getOrElse(sym.span.start, Nil ).exists(whileSpan.contains(_))
337- && curCtx.notNullInfos.containsRef (ref)
356+ && curCtx.notNullInfos.impliesNotNull (ref)
338357 val retractedVars = curCtx.notNullInfos.flatMap(_.asserted.filter(isRetracted)).toSet
339358 curCtx.addNotNullInfo(NotNullInfo (Set (), retractedVars))
340359
0 commit comments