[FIR] Add DFA implications when one side of an Elvis operator is null
When one side of an Elvis operator can only be `null`, and the entire Elvis operator expression cannot be `null`, this implies that the opposite side of the Elvis operator cannot be `null`. Add such implications to the Elvis exit node of the DFA. This helps smart-casting of variables used within long Elvis operator chains. #KT-49249 Fixed
This commit is contained in:
+19
@@ -18,3 +18,22 @@ FILE: longElvisChain.kt
|
||||
) } ?: ^test_2 Unit
|
||||
throw R|<local>/a|
|
||||
}
|
||||
public final fun test_3(): R|kotlin/Unit| {
|
||||
lval a: R|kotlin/Throwable?| = Null(null)
|
||||
lval b: R|kotlin/Unit?| = Null(null)
|
||||
lval c: R|kotlin/Throwable| = R|<local>/b|?.{ $subj$.R|kotlin/let|<R|kotlin/Unit|, R|kotlin/Nothing|>(<L> = let@fun <anonymous>(it: R|kotlin/Unit|): R|kotlin/Nothing| <inline=Inline, kind=EXACTLY_ONCE> {
|
||||
^test_3 R|<local>/it|
|
||||
}
|
||||
) } ?: R|<local>/a| ?: ^test_3 Unit
|
||||
R|<local>/c|!!
|
||||
throw R|<local>/a|
|
||||
}
|
||||
public final fun test_4(): R|kotlin/Unit| {
|
||||
lval a: R|kotlin/Throwable?| = Null(null)
|
||||
lval b: R|kotlin/Unit?| = Null(null)
|
||||
lval c: R|kotlin/Throwable| = R|<local>/b|?.{ $subj$.R|kotlin/let|<R|kotlin/Unit|, R|kotlin/Nothing|>(<L> = let@fun <anonymous>(it: R|kotlin/Unit|): R|kotlin/Nothing| <inline=Inline, kind=EXACTLY_ONCE> {
|
||||
^test_4 R|<local>/it|
|
||||
}
|
||||
) } ?: R|<local>/a| ?: ^test_4 Unit
|
||||
throw R|<local>/a|
|
||||
}
|
||||
|
||||
@@ -6,12 +6,27 @@ fun test_1() {
|
||||
val b: Unit? = null
|
||||
val c = a ?: b?.let { return it } ?: return
|
||||
c<!UNNECESSARY_NOT_NULL_ASSERTION!>!!<!>
|
||||
throw <!TYPE_MISMATCH!>a<!>
|
||||
throw a
|
||||
}
|
||||
|
||||
fun test_2() {
|
||||
val a: Throwable? = null;
|
||||
val b: Unit? = null
|
||||
val c = a ?: b?.let { return it } ?: return
|
||||
throw <!TYPE_MISMATCH!>a<!>
|
||||
throw a
|
||||
}
|
||||
|
||||
fun test_3() {
|
||||
val a: Throwable? = null;
|
||||
val b: Unit? = null
|
||||
val c = b?.let { return it } ?: a ?: return
|
||||
c<!UNNECESSARY_NOT_NULL_ASSERTION!>!!<!>
|
||||
throw a
|
||||
}
|
||||
|
||||
fun test_4() {
|
||||
val a: Throwable? = null;
|
||||
val b: Unit? = null
|
||||
val c = b?.let { return it } ?: a ?: return
|
||||
throw a
|
||||
}
|
||||
|
||||
+23
-3
@@ -1097,11 +1097,31 @@ abstract class FirDataFlowAnalyzer(
|
||||
// If LHS is never null, then the edge from RHS is dead and this node's flow already contains
|
||||
// all statements from LHS unconditionally.
|
||||
if (isLhsNotNull) return@mergeIncomingFlow
|
||||
|
||||
val elvisVariable by lazy { variableStorage.createSynthetic(elvisExpression) }
|
||||
|
||||
// If (x ?: null) != null then x != null
|
||||
if (elvisExpression.rhs.resultType.isNullableNothing) {
|
||||
val lhsVariable = variableStorage.getOrCreateIfReal(flow, elvisExpression.lhs)
|
||||
if (lhsVariable != null) {
|
||||
flow.addImplication((elvisVariable notEq null) implies (lhsVariable notEq null))
|
||||
}
|
||||
}
|
||||
|
||||
// If (null ?: x) != null then x != null
|
||||
if (elvisExpression.lhs.resultType.isNullableNothing) {
|
||||
val rhsVariable = variableStorage.getOrCreateIfReal(flow, elvisExpression.rhs)
|
||||
if (rhsVariable != null) {
|
||||
flow.addImplication((elvisVariable notEq null) implies (rhsVariable notEq null))
|
||||
}
|
||||
}
|
||||
|
||||
// For any predicate P(x), if P(v) != P(u ?: v) then u != null. In general this requires two levels of
|
||||
// implications, but for constant v the logic system can handle some basic cases of P(x).
|
||||
val rhs = (elvisExpression.rhs as? FirConstExpression<*>)?.value as? Boolean ?: return@mergeIncomingFlow
|
||||
val elvisVariable = variableStorage.createSynthetic(elvisExpression)
|
||||
flow.addAllConditionally(elvisVariable eq !rhs, node.firstPreviousNode.flow)
|
||||
val rhs = (elvisExpression.rhs as? FirConstExpression<*>)?.value as? Boolean
|
||||
if (rhs != null) {
|
||||
flow.addAllConditionally(elvisVariable eq !rhs, node.firstPreviousNode.flow)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user