|
| 1 | +package dotty.tools.dotc.core |
| 2 | + |
| 3 | +import dotty.tools.dotc.ast.tpd._ |
| 4 | +import StdNames.nme |
| 5 | +import dotty.tools.dotc.ast.Trees.{Apply, Block, If, Select, TypeApply} |
| 6 | +import dotty.tools.dotc.ast.tpd |
| 7 | +import dotty.tools.dotc.core.Constants.Constant |
| 8 | +import dotty.tools.dotc.core.Contexts.Context |
| 9 | +import dotty.tools.dotc.core.Names.Name |
| 10 | +import dotty.tools.dotc.core.Types.{NonNullTermRef, TermRef, Type} |
| 11 | + |
| 12 | +import scala.annotation.internal.sharable |
| 13 | + |
| 14 | +/** Flow-sensitive typer */ |
| 15 | +object FlowTyper { |
| 16 | + |
| 17 | + /** A set of `TermRef`s known to be non-null at the current program point */ |
| 18 | + type FlowFacts = Set[TermRef] |
| 19 | + |
| 20 | + /** The initial state where no `TermRef`s are known to be non-null */ |
| 21 | + @sharable val emptyFlowFacts = Set.empty[TermRef] |
| 22 | + |
| 23 | + /** Tries to improve the precision of `tpe` using flow-sensitive type information. |
| 24 | + * For nullability, is `tpe` is a `TermRef` declared as nullable but known to be non-nullable because of the |
| 25 | + * contextual info, returns the non-nullable version of the type. |
| 26 | + * If the precision of the type can't be improved, then returns the type unchanged. |
| 27 | + */ |
| 28 | + def refineType(tpe: Type)(implicit ctx: Context): Type = { |
| 29 | + assert(ctx.settings.YexplicitNulls.value) |
| 30 | + tpe match { |
| 31 | + case tref: TermRef if ctx.flowFacts.contains(tref) => |
| 32 | + NonNullTermRef.fromTermRef(tref) |
| 33 | + case _ => tpe |
| 34 | + } |
| 35 | + } |
| 36 | + |
| 37 | + /** Nullability facts inferred from a condition. |
| 38 | + * @param ifTrue are the terms known to be non-null if the condition is true. |
| 39 | + * @param ifFalse are the terms known to be non-null if the condition is false. |
| 40 | + */ |
| 41 | + case class Inferred(ifTrue: FlowFacts, ifFalse: FlowFacts) { |
| 42 | + // Let `NN(e, true/false)` be the set of terms that are non-null if `e` evaluates to `true/false`. |
| 43 | + // We can use De Morgan's laws to underapproximate `NN` via `Inferred`. |
| 44 | + // e.g. say `e = e1 && e2`. Then if `e` is `false`, we know that either `!e1` or `!e2`. |
| 45 | + // Let `t` be a term that is in both `NN(e1, false)` and `NN(e2, false)`. |
| 46 | + // Then it follows that `t` must be in `NN(e, false)`. This means that if we set |
| 47 | + // `Inferred(e1 && e2, false) = Inferred(e1, false) ∩ Inferred(e2, false)`, we'll have |
| 48 | + // `Inferred(e1 && e2, false) ⊂ NN(e1 && e2, false)` (formally, we'd do a structural induction on `e`). |
| 49 | + // This means that when we infer something we do so soundly. The methods below use this approach. |
| 50 | + |
| 51 | + /** If `this` corresponds to a condition `e1` and `other` to `e2`, calculate the inferred facts for `e1 && e2`. */ |
| 52 | + def combineAnd(other: Inferred): Inferred = Inferred(ifTrue.union(other.ifTrue), ifFalse.intersect(other.ifFalse)) |
| 53 | + |
| 54 | + /** If `this` corresponds to a condition `e1` and `other` to `e2`, calculate the inferred facts for `e1 || e2`. */ |
| 55 | + def combineOr(other: Inferred): Inferred = Inferred(ifTrue.intersect(other.ifTrue), ifFalse.union(other.ifFalse)) |
| 56 | + |
| 57 | + /** The inferred facts for the negation of this condition. */ |
| 58 | + def negate: Inferred = Inferred(ifFalse, ifTrue) |
| 59 | + } |
| 60 | + |
| 61 | + object Inferred { |
| 62 | + /** Create a singleton inferred fact containing `tref`. */ |
| 63 | + def apply(tref: TermRef, ifTrue: Boolean): Inferred = { |
| 64 | + if (ifTrue) Inferred(Set(tref), emptyFlowFacts) |
| 65 | + else Inferred(emptyFlowFacts, Set(tref)) |
| 66 | + } |
| 67 | + } |
| 68 | + |
| 69 | + /** Analyze the tree for a condition `cond` to learn new flow facts. |
| 70 | + * Supports ands, ors, and unary negation. |
| 71 | + * |
| 72 | + * Example: |
| 73 | + * (1) |
| 74 | + * ``` |
| 75 | + * val x: String|Null = "foo" |
| 76 | + * if (x != null) { |
| 77 | + * // x: String in the "then" branch |
| 78 | + * } |
| 79 | + * ``` |
| 80 | + * Notice that `x` must be stable for the above to work. |
| 81 | + * |
| 82 | + * Let NN(cond, true/false) be the set of paths (`TermRef`s) that we can infer to be non-null |
| 83 | + * if `cond` is true/false, respectively. Then define NN by (basically De Morgan's laws): |
| 84 | + * |
| 85 | + * NN(p == null, true) = {} we also handle `eq` |
| 86 | + * NN(p == null, false) = {p} if p is stable |
| 87 | + * NN(p != null, true) = {p} if p is stable we also handle `ne` |
| 88 | + * NN(p != null, false) = {} |
| 89 | + * NN(p.isInstanceOf[Null], true) = {} |
| 90 | + * NN(p.isInstanceOf[Null], false) = {p} if p is stable |
| 91 | + * NN(A && B, true) = ∪(NN(A, true), NN(B, true)) |
| 92 | + * NN(A && B, false) = ∩(NN(A, false), NN(B, false)) |
| 93 | + * NN(A || B, true) = ∩(NN(A, true), NN(B, true)) |
| 94 | + * NN(A || B, false) = ∪(NN(A, false), NN(B, false)) |
| 95 | + * NN(!A, true) = NN(A, false) |
| 96 | + * NN(!A, false) = NN(A, true) |
| 97 | + * NN({S1; ...; Sn, cond}, true/false) = NN(cond, true/false) |
| 98 | + * NN(cond, _) = {} otherwise |
| 99 | + */ |
| 100 | + def inferFromCond(cond: Tree)(implicit ctx: Context): Inferred = { |
| 101 | + assert(ctx.settings.YexplicitNulls.value) |
| 102 | + /** Combine two sets of facts according to `op`. */ |
| 103 | + def combine(lhs: Inferred, op: Name, rhs: Inferred): Inferred = { |
| 104 | + op match { |
| 105 | + case _ if op == nme.ZAND => lhs.combineAnd(rhs) |
| 106 | + case _ if op == nme.ZOR => lhs.combineOr(rhs) |
| 107 | + } |
| 108 | + } |
| 109 | + |
| 110 | + val emptyFacts = Inferred(emptyFlowFacts, emptyFlowFacts) |
| 111 | + val nullLit = tpd.Literal(Constant(null)) |
| 112 | + |
| 113 | + /** Recurse over a conditional to extract flow facts. */ |
| 114 | + def recur(tree: Tree): Inferred = { |
| 115 | + tree match { |
| 116 | + case Apply(Select(lhs, op), List(rhs)) => |
| 117 | + if (op == nme.ZAND || op == nme.ZOR) combine(recur(lhs), op, recur(rhs)) |
| 118 | + else if (op == nme.EQ || op == nme.NE || op == nme.eq || op == nme.ne) newFact(lhs, isEq = (op == nme.EQ || op == nme.eq), rhs) |
| 119 | + else emptyFacts |
| 120 | + // TODO(abeln): handle type test with argument that's not a subtype of `Null`. |
| 121 | + // We could infer "non-null" in that case: e.g. `if (x.isInstanceOf[String]) { // x can't be null }` |
| 122 | + // case TypeApply(Select(lhs, op), List(tArg)) if op == nme.isInstanceOf_ && tArg.tpe.isNullType => |
| 123 | + // newFact(lhs, isEq = true, nullLit) |
| 124 | + case Select(lhs, op) if op == nme.UNARY_! => recur(lhs).negate |
| 125 | + case Block(_, expr) => recur(expr) |
| 126 | + case inline: Inlined => recur(inline.expansion) |
| 127 | + case typed: Typed => recur(typed.expr) // TODO(abeln): check that the type is `Boolean`? |
| 128 | + case _ => emptyFacts |
| 129 | + } |
| 130 | + } |
| 131 | + |
| 132 | + /** Extract new facts from an expression `lhs = rhs` or `lhs != rhs` |
| 133 | + * if either the lhs or rhs is the `null` literal. |
| 134 | + */ |
| 135 | + def newFact(lhs: Tree, isEq: Boolean, rhs: Tree): Inferred = { |
| 136 | + def isNullLit(tree: Tree): Boolean = tree match { |
| 137 | + case lit: Literal if lit.const.tag == Constants.NullTag => true |
| 138 | + case _ => false |
| 139 | + } |
| 140 | + |
| 141 | + def isStableTermRef(tree: Tree): Boolean = asStableTermRef(tree).isDefined |
| 142 | + |
| 143 | + def asStableTermRef(tree: Tree): Option[TermRef] = tree.tpe match { |
| 144 | + case tref: TermRef if tref.isStable => Some(tref) |
| 145 | + case _ => None |
| 146 | + } |
| 147 | + |
| 148 | + val trefOpt = |
| 149 | + if (isNullLit(lhs) && isStableTermRef(rhs)) asStableTermRef(rhs) |
| 150 | + else if (isStableTermRef(lhs) && isNullLit(rhs)) asStableTermRef(lhs) |
| 151 | + else None |
| 152 | + |
| 153 | + trefOpt match { |
| 154 | + case Some(tref) => |
| 155 | + // If `isEq`, then the condition is of the form `lhs == null`, |
| 156 | + // in which case we know `lhs` is non-null if the condition is false. |
| 157 | + Inferred(tref, ifTrue = !isEq) |
| 158 | + case _ => emptyFacts |
| 159 | + } |
| 160 | + } |
| 161 | + |
| 162 | + recur(cond) |
| 163 | + } |
| 164 | + |
| 165 | + /** Infer flow-sensitive type information inside a condition. |
| 166 | + * |
| 167 | + * Specifically, if `cond` is of the form `lhs &&` or `lhs ||`, where the lhs has already been typed |
| 168 | + * (and the rhs hasn't been typed yet), compute the non-null facts that must hold so that the rhs can |
| 169 | + * execute. These facts can then be soundly assumed when typing the rhs, because boolean operators are |
| 170 | + * short-circuiting. |
| 171 | + * |
| 172 | + * This is useful in e.g. |
| 173 | + * ``` |
| 174 | + * val x: String|Null = ??? |
| 175 | + * if (x != null && x.length > 0) ... |
| 176 | + * ``` |
| 177 | + */ |
| 178 | + def inferWithinCond(cond: Tree)(implicit ctx: Context): FlowFacts = { |
| 179 | + assert(ctx.settings.YexplicitNulls.value) |
| 180 | + cond match { |
| 181 | + case Select(lhs, op) if op == nme.ZAND || op == nme.ZOR => |
| 182 | + val Inferred(ifTrue, ifFalse) = inferFromCond(lhs) |
| 183 | + if (op == nme.ZAND) ifTrue |
| 184 | + else ifFalse |
| 185 | + case _ => emptyFlowFacts |
| 186 | + } |
| 187 | + } |
| 188 | + |
| 189 | + /** Infer flow-sensitive type information within a block. |
| 190 | + * |
| 191 | + * More precisely, if `s1; s2` are consecutive statements in a block, this returns |
| 192 | + * a context with nullability facts that hold once `s1` has executed. |
| 193 | + * The new facts can then be used to type `s2`. |
| 194 | + * |
| 195 | + * This is useful for e.g. |
| 196 | + * ``` |
| 197 | + * val x: String|Null = ??? |
| 198 | + * if (x == null) return "foo" |
| 199 | + * val y = x.length // x: String inferred |
| 200 | + * ``` |
| 201 | + * |
| 202 | + * How can we obtain additional facts just from the fact that `s1` executed? |
| 203 | + * This can happen if `s1` is of the form `If(cond, then, else)`, where `then` or |
| 204 | + * `else` have non-local control flow. |
| 205 | + * |
| 206 | + * The following qualify as non-local: |
| 207 | + * 1) a return |
| 208 | + * 2) an expression of type `Nothing` (in particular, usages of `throw`) |
| 209 | + * 3) a block where the last expression is non-local |
| 210 | + * 4) nothing else is non-local |
| 211 | + * |
| 212 | + * So, for example, if we know that `x` must be non-null if `cond` is true, and `else` is non-local, |
| 213 | + * then in order for `s2` to execute `cond` must be true. We can thus soundly add `x` to our |
| 214 | + * flow facts. |
| 215 | + */ |
| 216 | + def inferWithinBlock(stat: Tree)(implicit ctx: Context): FlowFacts = { |
| 217 | + def isNonLocal(s: Tree): Boolean = s match { |
| 218 | + case _: Return => true |
| 219 | + case Block(_, expr) => isNonLocal(expr) |
| 220 | + case _ => |
| 221 | + // If the type is bottom (like the result of a `throw`), then we assume the statement |
| 222 | + // won't finish executing. |
| 223 | + s.tpe.isBottomType |
| 224 | + } |
| 225 | + |
| 226 | + assert(ctx.settings.YexplicitNulls.value) |
| 227 | + stat match { |
| 228 | + case If(cond, thenExpr, elseExpr) => |
| 229 | + val Inferred(ifTrue, ifFalse) = inferFromCond(cond) |
| 230 | + if (isNonLocal(thenExpr) && isNonLocal(elseExpr)) ifTrue ++ ifFalse |
| 231 | + else if (isNonLocal(thenExpr)) ifFalse |
| 232 | + else if (isNonLocal(elseExpr)) ifTrue |
| 233 | + else emptyFlowFacts |
| 234 | + case _ => emptyFlowFacts |
| 235 | + } |
| 236 | + } |
| 237 | +} |
0 commit comments