From 67a6785f63ad14e3ae5f8f1b0f41ddb9477ee19a Mon Sep 17 00:00:00 2001 From: pyos Date: Sat, 12 Nov 2022 16:19:22 +0100 Subject: [PATCH] FIR DFA: move `eq/notEq null`-to-type translation to LogicSystem This makes the `returns() implies` checker slightly cleaner, and also fixes the case that I've missed where in RHS of `x ?:` type of `x` was not set to `Nothing?`. --- .../analysis/cfa/FirReturnsImpliesAnalyzer.kt | 24 ++----- .../fir/resolve/dfa/FirDataFlowAnalyzer.kt | 72 +++++++++---------- .../kotlin/fir/resolve/dfa/LogicSystem.kt | 5 ++ .../fir/resolve/dfa/PersistentLogicSystem.kt | 24 +++++-- .../kotlin/fir/resolve/dfa/statements.kt | 2 +- .../unboxInlineClassAfterElvis.kt | 4 +- .../diagnostics/notLinked/dfa/neg/14.fir.kt | 2 +- .../diagnostics/notLinked/dfa/neg/39.fir.kt | 40 +++++------ .../diagnostics/notLinked/dfa/neg/7.fir.kt | 2 +- .../diagnostics/notLinked/dfa/pos/35.fir.kt | 2 +- 10 files changed, 87 insertions(+), 90 deletions(-) diff --git a/compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/cfa/FirReturnsImpliesAnalyzer.kt b/compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/cfa/FirReturnsImpliesAnalyzer.kt index d4d5577b9cf..03a0d168bc9 100644 --- a/compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/cfa/FirReturnsImpliesAnalyzer.kt +++ b/compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/cfa/FirReturnsImpliesAnalyzer.kt @@ -76,7 +76,6 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { val effect = effectDeclaration.effect as ConeReturnsEffectDeclaration val builtinTypes = context.session.builtinTypes val typeContext = context.session.typeContext - val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow val isReturn = node is JumpNode && node.fir is FirReturnExpression val resultExpression = if (isReturn) (node.fir as FirReturnExpression).result else node.fir @@ -92,7 +91,7 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { // TODO: create separate variable storage and don't modify existing one val variableStorage = dataFlowInfo.variableStorage as VariableStorageImpl - + val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow var typeStatements: TypeStatements = flow.approvedTypeStatements if (effect.value != ConeConstantReference.WILDCARD) { @@ -103,7 +102,10 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { if (!resultExpression.isApplicableWith(operation)) return false } else { val resultVar = variableStorage.getOrCreate(flow, resultExpression) - typeStatements = logicSystem.approveOperationStatement(flow, OperationStatement(resultVar, operation), builtinTypes) + typeStatements = logicSystem.andForTypeStatements( + typeStatements, + logicSystem.approveOperationStatement(flow, OperationStatement(resultVar, operation)) + ) } } @@ -121,22 +123,6 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { return false } - private fun LogicSystem.approveOperationStatement( - flow: PersistentFlow, - statement: OperationStatement, - builtinTypes: BuiltinTypes - ): TypeStatements { - val newTypeStatements = andForTypeStatements(flow.approvedTypeStatements, approveOperationStatement(flow, statement)) - val variable = statement.variable - if (!variable.isReal()) return newTypeStatements - val extraStatement = when (statement.operation) { - Operation.NotEqNull -> variable.nullabilityStatement(builtinTypes, isNull = false) - Operation.EqNull -> variable.nullabilityStatement(builtinTypes, isNull = true) - else -> return newTypeStatements - } - return andForTypeStatements(newTypeStatements, mapOf(variable to extraStatement)) - } - private fun ConeBooleanExpression.buildTypeStatements( function: FirFunction, logicSystem: LogicSystem<*>, 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 e029f1c051d..86e875c45b5 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 @@ -45,7 +45,6 @@ class DataFlowAnalyzerContext( val graphBuilder: ControlFlowGraphBuilder, variableStorage: VariableStorageImpl, flowOnNodes: MutableMap, FLOW>, - val variablesForWhenConditions: MutableMap, val preliminaryLoopVisitor: PreliminaryLoopVisitor ) { var flowOnNodes = flowOnNodes @@ -63,7 +62,6 @@ class DataFlowAnalyzerContext( fun reset() { graphBuilder.reset() - variablesForWhenConditions.clear() variableStorage = variableStorage.clear() flowOnNodes = mutableMapOf() @@ -76,7 +74,7 @@ class DataFlowAnalyzerContext( fun empty(session: FirSession): DataFlowAnalyzerContext = DataFlowAnalyzerContext( ControlFlowGraphBuilder(), VariableStorageImpl(session), - mutableMapOf(), mutableMapOf(), PreliminaryLoopVisitor() + mutableMapOf(), PreliminaryLoopVisitor() ) } } @@ -410,6 +408,7 @@ abstract class FirDataFlowAnalyzer( } else { val expressionVariable = variableStorage.createSynthetic(typeOperatorCall) flow.addImplication((expressionVariable notEq null) implies (operandVariable notEq null)) + // TODO? flow.addImplication((expressionVariable eq null) implies (operandVariable eq null)) } } @@ -477,14 +476,15 @@ abstract class FirDataFlowAnalyzer( val flow = node.flow val operandVariable = variableStorage.getOrCreateIfReal(flow, operand) ?: return val expressionVariable = variableStorage.createSynthetic(node.fir) - // expression == non-null const -> expression != null - flow.addImplication((expressionVariable eq isEq) implies (operandVariable notEq null)) - if (const.kind == ConstantValueKind.Boolean) { + if (const.kind == ConstantValueKind.Boolean && operand.coneType.isBooleanOrNullableBoolean) { val expected = (const.value as Boolean) flow.addImplication((expressionVariable eq isEq) implies (operandVariable eq expected)) if (operand.coneType.isBoolean) { flow.addImplication((expressionVariable eq !isEq) implies (operandVariable eq !expected)) } + } else { + // expression == non-null const -> expression != null + flow.addImplication((expressionVariable eq isEq) implies (operandVariable notEq null)) } } @@ -620,8 +620,11 @@ abstract class FirDataFlowAnalyzer( val previousConditionExitNode = previousNodes.singleOrNull() if (previousConditionExitNode is WhenBranchConditionExitNode) { val flow = mergeIncomingFlow() - val previousConditionVariable = context.variablesForWhenConditions.remove(previousConditionExitNode) ?: return - flow.commitOperationStatement(previousConditionVariable eq false) + val previousCondition = previousConditionExitNode.fir.condition + if (previousCondition.coneType.isBoolean) { + val previousConditionVariable = variableStorage.get(flow, previousCondition) ?: return + flow.commitOperationStatement(previousConditionVariable eq false) + } } else { // first branch mergeIncomingFlow() } @@ -631,9 +634,11 @@ abstract class FirDataFlowAnalyzer( val (conditionExitNode, resultEnterNode) = graphBuilder.exitWhenBranchCondition(whenBranch) val conditionExitFlow = conditionExitNode.mergeIncomingFlow() val resultEnterFlow = resultEnterNode.mergeIncomingFlow() - val conditionVariable = variableStorage.get(conditionExitFlow, whenBranch.condition) ?: return - context.variablesForWhenConditions[conditionExitNode] = conditionVariable - resultEnterFlow.commitOperationStatement(conditionVariable eq true) + // If the condition is invalid, don't generate smart casts to Any or Boolean. + if (whenBranch.condition.coneType.isBoolean) { + val conditionVariable = variableStorage.get(conditionExitFlow, whenBranch.condition) ?: return + resultEnterFlow.commitOperationStatement(conditionVariable eq true) + } } fun exitWhenBranchResult(whenBranch: FirWhenBranch) { @@ -664,8 +669,10 @@ abstract class FirDataFlowAnalyzer( val (loopConditionExitNode, loopBlockEnterNode) = graphBuilder.exitWhileLoopCondition(loop) val conditionExitFlow = loopConditionExitNode.mergeIncomingFlow() val blockEnterFlow = loopBlockEnterNode.mergeIncomingFlow() - val conditionVariable = variableStorage.get(conditionExitFlow, loop.condition) ?: return - blockEnterFlow.commitOperationStatement(conditionVariable eq true) + if (loop.condition.coneType.isBoolean) { + val conditionVariable = variableStorage.get(conditionExitFlow, loop.condition) ?: return + blockEnterFlow.commitOperationStatement(conditionVariable eq true) + } } fun exitWhileLoop(loop: FirLoop) { @@ -679,8 +686,10 @@ abstract class FirDataFlowAnalyzer( val flow = mergeIncomingFlow() // Might be > 1 node or other type if there are `break`s: val singlePreviousNode = previousNodes.singleOrNull { !it.isDead } as? LoopConditionExitNode ?: return - val variable = variableStorage.get(flow, singlePreviousNode.fir) ?: return - flow.commitOperationStatement(variable eq false) + if (singlePreviousNode.fir.coneType.isBoolean) { + val variable = variableStorage.get(flow, singlePreviousNode.fir) ?: return + flow.commitOperationStatement(variable eq false) + } } private fun enterCapturingStatement(flow: FLOW, statement: FirStatement) { @@ -1044,14 +1053,16 @@ abstract class FirDataFlowAnalyzer( val flow = node.mergeIncomingFlow() val leftVariable = variableStorage.get(flowFromLeft, binaryLogicExpression.leftOperand) + val leftIsBoolean = leftVariable != null && binaryLogicExpression.leftOperand.coneType.isBoolean if (!node.leftOperandNode.isDead && node.rightOperandNode.isDead) { // If the right operand does not terminate, then we know that the value of the entire expression // has to be saturating (true for or, false for and), and it has to be produced by the left operand. - if (leftVariable != null) { - flow.commitOperationStatement(leftVariable eq !isAnd) + if (leftIsBoolean) { + flow.commitOperationStatement(leftVariable!! eq !isAnd) } } else { val rightVariable = variableStorage.get(flowFromRight, binaryLogicExpression.rightOperand) + val rightIsBoolean = rightVariable != null && binaryLogicExpression.rightOperand.coneType.isBoolean val operatorVariable = variableStorage.createSynthetic(binaryLogicExpression) // If `left && right` is true, then both are evaluated to true. If `left || right` is false, then both are false. // Approved type statements for RHS already contain everything implied by the corresponding value of LHS. @@ -1059,19 +1070,19 @@ abstract class FirDataFlowAnalyzer( // TODO? `bothEvaluated` also implies all implications from RHS. This requires a second level // of implications, which the logic system currently doesn't support. See also safe calls. flow.addAllConditionally(bothEvaluated, flowFromRight.approvedTypeStatements) - if (rightVariable != null) { - flow.addAllConditionally(bothEvaluated, logicSystem.approveOperationStatement(flowFromRight, rightVariable eq isAnd)) + if (rightIsBoolean) { + flow.addAllConditionally(bothEvaluated, logicSystem.approveOperationStatement(flowFromRight, rightVariable!! eq isAnd)) } // If `left && right` is false, then either `left` is false, or both were evaluated and `right` is false. // If `left || right` is true, then either `left` is true, or both were evaluated and `right` is true. - if (leftVariable != null && rightVariable != null) { + if (leftIsBoolean && rightIsBoolean) { flow.addAllConditionally( operatorVariable eq !isAnd, logicSystem.orForTypeStatements( - logicSystem.approveOperationStatement(flowFromLeft, leftVariable eq !isAnd), + logicSystem.approveOperationStatement(flowFromLeft, leftVariable!! eq !isAnd), // TODO: and(approved from right, ...)? FE1.0 doesn't seem to handle that correctly either. // if (x is A || whatever(x as B)) { /* x is (A | B) */ } - logicSystem.approveOperationStatement(flowFromRight, rightVariable eq !isAnd), + logicSystem.approveOperationStatement(flowFromRight, rightVariable!! eq !isAnd), ) ) } @@ -1248,17 +1259,6 @@ abstract class FirDataFlowAnalyzer( } private fun FLOW.addImplication(statement: Implication) { - val effect = statement.effect - if (effect is OperationStatement) { - val variable = effect.variable - if (variable.isReal()) { - when (effect.operation) { - Operation.EqNull -> variable typeEq nullableNothing - Operation.NotEqNull -> variable typeEq any - else -> null - }?.let { logicSystem.addImplication(this, statement.condition implies it) } - } - } logicSystem.addImplication(this, statement) } @@ -1277,12 +1277,6 @@ abstract class FirDataFlowAnalyzer( logicSystem.approveOperationStatement(this, statement, removeApprovedOrImpossible = true).values.forEach { addTypeStatement(it) } - if (statement.operation == Operation.NotEqNull) { - val variable = statement.variable - if (variable is RealVariable) { - addTypeStatement(variable typeEq any) - } - } } private val CFGNode<*>.previousFlow: FLOW diff --git a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/LogicSystem.kt b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/LogicSystem.kt index 0eeafd12311..38746192031 100644 --- a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/LogicSystem.kt +++ b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/LogicSystem.kt @@ -79,12 +79,17 @@ abstract class LogicSystem(protected val context: ConeInferenceCont val intersected = types.map { ConeTypeIntersector.intersectTypes(context, it.toList()) } val unified = context.commonSuperTypeOrNull(intersected) ?: return null return when { + unified.isNullableAny -> null unified.isAcceptableForSmartcast() -> unified unified.canBeNull -> null else -> context.anyType() } } + protected operator fun MutableTypeStatement.plusAssign(other: TypeStatement) { + exactType += other.exactType + } + protected fun and(statements: Collection): TypeStatement? = statements.singleOrNew { statements.flatMapTo(mutableSetOf()) { it.exactType } } diff --git a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/PersistentLogicSystem.kt b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/PersistentLogicSystem.kt index 768be3a382d..8c70c515677 100644 --- a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/PersistentLogicSystem.kt +++ b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/PersistentLogicSystem.kt @@ -5,7 +5,6 @@ package org.jetbrains.kotlin.fir.resolve.dfa -import com.google.common.collect.ArrayListMultimap import kotlinx.collections.immutable.* import org.jetbrains.kotlin.fir.types.ConeInferenceContext import org.jetbrains.kotlin.fir.types.ConeKotlinType @@ -254,26 +253,37 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste } } + private val nullableNothingType = context.session.builtinTypes.nullableNothingType.type + private val anyType = context.session.builtinTypes.anyType.type + override fun approveOperationStatement( flow: PersistentFlow, approvedStatement: OperationStatement, removeApprovedOrImpossible: Boolean, ): TypeStatements { - val approvedTypeStatements: ArrayListMultimap = ArrayListMultimap.create() + val result = mutableMapOf() val queue = LinkedList().apply { this += approvedStatement } val approved = mutableSetOf() while (queue.isNotEmpty()) { - val next: OperationStatement = queue.removeFirst() + val next = queue.removeFirst() // Defense from cycles in facts - if (!approved.add(next)) continue + if (!removeApprovedOrImpossible && !approved.add(next)) continue + + val operation = next.operation val variable = next.variable + if (variable.isReal()) { + val impliedType = if (operation == Operation.EqNull) nullableNothingType else anyType + result.getOrPut(variable) { MutableTypeStatement(variable) }.exactType.add(impliedType) + } + val statements = flow.logicStatements[variable] ?: continue val stillUnknown = statements.removeAll { - val knownValue = it.condition.operation.valueIfKnown(next.operation) + val knownValue = it.condition.operation.valueIfKnown(operation) if (knownValue == true) { when (val effect = it.effect) { is OperationStatement -> queue += effect - is TypeStatement -> approvedTypeStatements.put(effect.variable, effect) + is TypeStatement -> + result.getOrPut(effect.variable) { MutableTypeStatement(effect.variable) } += effect } } removeApprovedOrImpossible && knownValue != null @@ -284,7 +294,7 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste flow.logicStatements = flow.logicStatements.put(variable, stillUnknown) } } - return approvedTypeStatements.asMap().mapValues { and(it.value)!! } + return result } override fun recordNewAssignment(flow: PersistentFlow, variable: RealVariable, index: Int) { diff --git a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/statements.kt b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/statements.kt index a52d063fd07..8f799235861 100644 --- a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/statements.kt +++ b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/statements.kt @@ -54,7 +54,7 @@ enum class Operation { fun valueIfKnown(given: Operation): Boolean? = when (this) { EqTrue, EqFalse -> if (given == NotEqNull) null else given == this EqNull -> given == EqNull - NotEqNull -> given == NotEqNull + NotEqNull -> given != EqNull } override fun toString(): String = when (this) { diff --git a/compiler/testData/codegen/bytecodeText/inlineClasses/unboxInlineClassAfterElvis.kt b/compiler/testData/codegen/bytecodeText/inlineClasses/unboxInlineClassAfterElvis.kt index fe15ea8d553..318f41a9b78 100644 --- a/compiler/testData/codegen/bytecodeText/inlineClasses/unboxInlineClassAfterElvis.kt +++ b/compiler/testData/codegen/bytecodeText/inlineClasses/unboxInlineClassAfterElvis.kt @@ -1,4 +1,6 @@ // !LANGUAGE: +InlineClasses +// IGNORE_BACKEND_K2: JVM_IR +// FIR_STATUS: `x ?: x!!` assumed to throw if x is null, so only 2 unboxings // FILE: utils.kt @@ -16,4 +18,4 @@ fun test(x: UInt?, y: UInt) { // 3 INVOKEVIRTUAL UInt.unbox // 0 valueOf -// 0 intValue \ No newline at end of file +// 0 intValue diff --git a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/14.fir.kt b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/14.fir.kt index e56242be81c..8c4334f1522 100644 --- a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/14.fir.kt +++ b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/14.fir.kt @@ -19,7 +19,7 @@ fun case_2(x: Int?) { // TESTCASE NUMBER: 3 fun case_3(x: Boolean?) { - if (x ?: (x != null)) { + if (x ?: (x != null)) { x x.not() } diff --git a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/39.fir.kt b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/39.fir.kt index ef24f598852..39dcef1676f 100644 --- a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/39.fir.kt +++ b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/39.fir.kt @@ -11,8 +11,8 @@ fun case_1() { while (true) { println(x ?: break) } - x - x.length + x + x.length } /* @@ -25,8 +25,8 @@ fun case_2(y: MutableList) { while (true) { y[x ?: break] = 10 } - x - x.inv() + x + x.inv() } /* @@ -39,8 +39,8 @@ fun case_3(y: MutableList) { while (true) { y[0] = x ?: break } - x - x.inv() + x + x.inv() } // TESTCASE NUMBER: 4 @@ -49,8 +49,8 @@ fun case_4() { while (true) { x ?: break } - x - x.inv() + x + x.inv() } // TESTCASE NUMBER: 5 @@ -59,8 +59,8 @@ fun case_5(y: Boolean) { while (true) { y && (x ?: break) } - x - x.not() + x + x.not() } // TESTCASE NUMBER: 6 @@ -69,8 +69,8 @@ fun case_6(y: Boolean) { while (true) { y || (x ?: break) } - x - x.not() + x + x.not() } // TESTCASE NUMBER: 7 @@ -94,8 +94,8 @@ fun case_8() { while (true) { y += x ?: break } - x - x.inv() + x + x.inv() } /* @@ -109,8 +109,8 @@ fun case_9() { while (true) { y -= x ?: break } - x - x.inv() + x + x.inv() } /* @@ -124,8 +124,8 @@ fun case_10() { while (true) { val z = y - (x ?: break) } - x - x.inv() + x + x.inv() } /* @@ -139,8 +139,8 @@ fun case_11() { while (true) { val z = y * (x ?: break) } - x - x.inv() + x + x.inv() } // TESTCASE NUMBER: 12 diff --git a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/7.fir.kt b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/7.fir.kt index e56242be81c..8c4334f1522 100644 --- a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/7.fir.kt +++ b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/neg/7.fir.kt @@ -19,7 +19,7 @@ fun case_2(x: Int?) { // TESTCASE NUMBER: 3 fun case_3(x: Boolean?) { - if (x ?: (x != null)) { + if (x ?: (x != null)) { x x.not() } diff --git a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/pos/35.fir.kt b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/pos/35.fir.kt index 9e08a568f14..914d629a7b6 100644 --- a/compiler/tests-spec/testData/diagnostics/notLinked/dfa/pos/35.fir.kt +++ b/compiler/tests-spec/testData/diagnostics/notLinked/dfa/pos/35.fir.kt @@ -48,7 +48,7 @@ fun case_4(x: Any?) { x.equals(10) } - x + x } // TESTCASE NUMBER: 5