From 8ac59592edfc1d93a9f7ee529b983722800a2759 Mon Sep 17 00:00:00 2001 From: Brian Norman Date: Thu, 15 Jun 2023 14:16:15 -0500 Subject: [PATCH] [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 --- .../resolve/smartcasts/longElvisChain.fir.txt | 19 ++++++++++++++ .../resolve/smartcasts/longElvisChain.kt | 19 ++++++++++++-- .../fir/resolve/dfa/FirDataFlowAnalyzer.kt | 26 ++++++++++++++++--- 3 files changed, 59 insertions(+), 5 deletions(-) diff --git a/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.fir.txt b/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.fir.txt index e9a4fafde4d..d119e0270d4 100644 --- a/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.fir.txt +++ b/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.fir.txt @@ -18,3 +18,22 @@ FILE: longElvisChain.kt ) } ?: ^test_2 Unit throw R|/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|/b|?.{ $subj$.R|kotlin/let|( = let@fun (it: R|kotlin/Unit|): R|kotlin/Nothing| { + ^test_3 R|/it| + } + ) } ?: R|/a| ?: ^test_3 Unit + R|/c|!! + throw R|/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|/b|?.{ $subj$.R|kotlin/let|( = let@fun (it: R|kotlin/Unit|): R|kotlin/Nothing| { + ^test_4 R|/it| + } + ) } ?: R|/a| ?: ^test_4 Unit + throw R|/a| + } diff --git a/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.kt b/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.kt index 05942b21566..4f3bde579ec 100644 --- a/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.kt +++ b/compiler/fir/analysis-tests/testData/resolve/smartcasts/longElvisChain.kt @@ -6,12 +6,27 @@ fun test_1() { val b: Unit? = null val c = a ?: b?.let { return it } ?: return c!! - throw a + throw a } fun test_2() { val a: Throwable? = null; val b: Unit? = null val c = a ?: b?.let { return it } ?: return - throw a + throw a +} + +fun test_3() { + val a: Throwable? = null; + val b: Unit? = null + val c = b?.let { return it } ?: a ?: return + c!! + throw a +} + +fun test_4() { + val a: Throwable? = null; + val b: Unit? = null + val c = b?.let { return it } ?: a ?: return + throw a } diff --git a/compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/FirDataFlowAnalyzer.kt b/compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/FirDataFlowAnalyzer.kt index 8f734501280..27cc5344b1b 100644 --- a/compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/FirDataFlowAnalyzer.kt +++ b/compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/FirDataFlowAnalyzer.kt @@ -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) + } } }