From bc9b358c9fb20db5f500ff1092b56c753a3d7739 Mon Sep 17 00:00:00 2001 From: pyos Date: Tue, 8 Nov 2022 11:47:57 +0100 Subject: [PATCH] FIR DFA: bring into compliance with De Morgan's laws I don't even know if this affects any real code, but it did uncover some deeper issues, like the fact that `!is` did not add any statements when `true`. --- .../analysis/cfa/FirReturnsImpliesAnalyzer.kt | 25 +++-- .../fir/resolve/dfa/FirDataFlowAnalyzer.kt | 35 +++---- .../kotlin/fir/resolve/dfa/LogicSystem.kt | 92 ++++++++----------- .../fir/resolve/dfa/PersistentLogicSystem.kt | 36 ++------ .../jetbrains/kotlin/fir/resolve/dfa/model.kt | 29 +----- .../kotlin/fir/resolve/dfa/statements.kt | 8 +- .../jetbrains/kotlin/fir/resolve/dfa/util.kt | 5 +- 7 files changed, 86 insertions(+), 144 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 242f61358db..ebb664f1dda 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 @@ -139,21 +139,17 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { statement: OperationStatement, builtinTypes: BuiltinTypes ): MutableTypeStatements { - val newTypeStatements: MutableTypeStatements = mutableMapOf() - + val newTypeStatements = flow.approvedTypeStatements.asMutableStatements() approveStatementsTo(newTypeStatements, flow, statement, flow.logicStatements.flatMap { it.value }) - newTypeStatements.mergeTypeStatements(flow.approvedTypeStatements) val variable = statement.variable - if (variable.isReal()) { - if (statement.operation == Operation.NotEqNull) { - newTypeStatements.addStatement(variable, simpleTypeStatement(variable, true, builtinTypes.anyType.type)) - } else if (statement.operation == Operation.EqNull) { - newTypeStatements.addStatement(variable, simpleTypeStatement(variable, false, builtinTypes.anyType.type)) - } + if (!variable.isReal()) return newTypeStatements + val extraStatement = when (statement.operation) { + Operation.NotEqNull -> simpleTypeStatement(variable, true, builtinTypes.anyType.type) + Operation.EqNull -> simpleTypeStatement(variable, false, builtinTypes.anyType.type) + else -> return newTypeStatements } - - return newTypeStatements + return andForTypeStatements(newTypeStatements, mapOf(variable to extraStatement)) } private fun ConeBooleanExpression.buildTypeStatements( @@ -181,9 +177,10 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() { val left = left.buildTypeStatements(function, logicSystem, variableStorage, flow, context) val right = right.buildTypeStatements(function, logicSystem, variableStorage, flow, context) if (left != null && right != null) { - if (kind == LogicOperationKind.AND) { - left.apply { mergeTypeStatements(right) } - } else logicSystem.orForTypeStatements(left, right) + if (kind == LogicOperationKind.AND) + logicSystem.andForTypeStatements(left, right) + else + logicSystem.orForTypeStatements(left, right) } else (left ?: right) } is ConeIsInstancePredicate -> buildTypeStatements(arg, !isNegated, type) 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 f010c8c6d40..c0e5ca122cf 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 @@ -632,6 +632,7 @@ abstract class FirDataFlowAnalyzer( // left == right && right not null -> left != null // [processEqNull] adds both implications: operator call could be true or false. We definitely need the matched case only. + // TODO: this is incomprehensible - the comments below say what the equivalent expression is fun shouldAddImplicationForStatement(operationStatement: OperationStatement): Boolean { if (!checkAddImplicationForStatement) return true // Only if operation statement is == True, i.e., left == right @@ -639,17 +640,22 @@ abstract class FirDataFlowAnalyzer( return !isEq && operationStatementOp == Operation.EqTrue || isEq && operationStatementOp == Operation.EqFalse } - logicSystem.approveOperationStatement(flow, predicate).forEach { effect -> - if (shouldAddImplicationForStatement(expressionVariable eq true)) { + // !checkAddImplicationForStatement || !isEq + if (shouldAddImplicationForStatement(expressionVariable eq true)) { + logicSystem.approveOperationStatement(flow, predicate).forEach { effect -> flow.addImplication((expressionVariable eq true) implies effect) } - if (shouldAddImplicationForStatement(expressionVariable eq false)) { - flow.addImplication((expressionVariable eq false) implies effect.invert()) - } } - val expressionVariableIsEq = shouldAddImplicationForStatement(expressionVariable eq isEq) - val expressionVariableIsNotEq = shouldAddImplicationForStatement(expressionVariable notEq isEq) + // !checkAddImplicationForStatement || isEq + if (shouldAddImplicationForStatement(expressionVariable eq false)) { + logicSystem.approveOperationStatement(flow, predicate.invert()).forEach { effect -> + flow.addImplication((expressionVariable eq false) implies effect) + } + } + + val expressionVariableIsEq = shouldAddImplicationForStatement(expressionVariable eq isEq) // !checkAddImplicationForStatement + val expressionVariableIsNotEq = shouldAddImplicationForStatement(expressionVariable notEq isEq) // true if (expressionVariableIsEq) { flow.addImplication((expressionVariable eq isEq) implies (operandVariable eq null)) @@ -665,10 +671,11 @@ abstract class FirDataFlowAnalyzer( if (expressionVariableIsNotEq) { flow.addImplication((expressionVariable notEq isEq) implies (operandVariable typeEq any)) } - + // true if (shouldAddImplicationForStatement(expressionVariable eq !isEq)) { flow.addImplication((expressionVariable eq !isEq) implies (operandVariable typeNotEq nullableNothing)) } + // !checkAddImplicationForStatement if (shouldAddImplicationForStatement(expressionVariable notEq !isEq)) { flow.addImplication((expressionVariable notEq !isEq) implies (operandVariable typeEq nullableNothing)) } @@ -1374,11 +1381,8 @@ abstract class FirDataFlowAnalyzer( val approvedIfTrue: MutableTypeStatements = mutableMapOf() logicSystem.approveStatementsTo(approvedIfTrue, flowFromRight, leftVariable eq bothEvaluated, conditionalFromLeft) logicSystem.approveStatementsTo(approvedIfTrue, flowFromRight, rightVariable eq bothEvaluated, conditionalFromRight) - approvedFromRight.forEach { (variable, info) -> - approvedIfTrue.addStatement(variable, info) - } - approvedIfTrue.values.forEach { info -> - flow.addImplication((operatorVariable eq bothEvaluated) implies info) + logicSystem.andForTypeStatements(approvedIfTrue, approvedFromRight).values.forEach { + flow.addImplication((operatorVariable eq bothEvaluated) implies it) } // left && right == False @@ -1387,9 +1391,8 @@ abstract class FirDataFlowAnalyzer( val leftIsFalse = logicSystem.approveOperationStatement(flowFromLeft, leftVariable eq onlyLeftEvaluated, conditionalFromLeft) val rightIsFalse = logicSystem.approveOperationStatement(flowFromRight, rightVariable eq onlyLeftEvaluated, conditionalFromRight) - approvedIfFalse.mergeTypeStatements(logicSystem.orForTypeStatements(leftIsFalse, rightIsFalse)) - approvedIfFalse.values.forEach { info -> - flow.addImplication((operatorVariable eq onlyLeftEvaluated) implies info) + logicSystem.andForTypeStatements(approvedIfFalse, logicSystem.orForTypeStatements(leftIsFalse, rightIsFalse)).values.forEach { + flow.addImplication((operatorVariable eq onlyLeftEvaluated) implies it) } } 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 0f3f4c1f3d6..d3b096a60e5 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 @@ -5,10 +5,7 @@ package org.jetbrains.kotlin.fir.resolve.dfa -import org.jetbrains.kotlin.fir.types.ConeInferenceContext -import org.jetbrains.kotlin.fir.types.ConeKotlinType -import org.jetbrains.kotlin.fir.types.canBeNull -import org.jetbrains.kotlin.fir.types.commonSuperTypeOrNull +import org.jetbrains.kotlin.fir.types.* abstract class LogicSystem(protected val context: ConeInferenceContext) { // ------------------------------- Flow operations ------------------------------- @@ -85,11 +82,8 @@ abstract class LogicSystem(protected val context: ConeInferenceCont return approveOperationStatement(flow, approvedStatement, statements).values } - fun orForTypeStatements( - left: TypeStatements, - right: TypeStatements, - ): MutableTypeStatements { - if (left.isNullOrEmpty() || right.isNullOrEmpty()) return mutableMapOf() + fun orForTypeStatements(left: TypeStatements, right: TypeStatements): MutableTypeStatements { + if (left.isEmpty() || right.isEmpty()) return mutableMapOf() val map = mutableMapOf() for (variable in left.keys.intersect(right.keys)) { val leftStatement = left.getValue(variable) @@ -99,63 +93,55 @@ abstract class LogicSystem(protected val context: ConeInferenceCont return map } - // ------------------------------- Util functions ------------------------------- - - // TODO - protected fun Collection>.intersectSets(): Set { - if (isEmpty()) return emptySet() - val iterator = iterator() - val result = LinkedHashSet(iterator.next()) - while (iterator.hasNext()) { - result.retainAll(iterator.next()) + fun andForTypeStatements(left: TypeStatements, right: TypeStatements): MutableTypeStatements { + if (left.isEmpty() && right.isEmpty()) return mutableMapOf() + val map = left.asMutableStatements() + for ((variable, rightStatement) in right) { + map[variable] = and(listOfNotNull(map[variable], rightStatement)) } - return result + return map } - private inline fun manipulateTypeStatements( - statements: Collection, - op: (Collection>) -> MutableSet - ): MutableTypeStatement { + // ------------------------------- Util functions ------------------------------- + + private fun foldStatements(statements: Collection, all: Boolean): MutableTypeStatement { require(statements.isNotEmpty()) statements.singleOrNull()?.let { return it.asMutableStatement() } val variable = statements.first().variable assert(statements.all { it.variable == variable }) - val exactType = op.invoke(statements.map { it.exactType }) - val exactNotType = op.invoke(statements.map { it.exactNotType }) - return MutableTypeStatement(variable, exactType, exactNotType) + // TypeStatement(variable, exactType, exactNotType) = + // variable is intersect(exactType) && variable !is intersect(exactNotType) + // So `and` of two type statements computes `and` of exactType and `or` of `exactNotType`, + // while `or` is the opposite. + return if (all) { + val exactType = statements.flatMapTo(mutableSetOf()) { it.exactType } + // variable !is a && variable !is b =/=> variable !is commonSuperType(a, b) + // So in this case we can only take the union if either type is a subtype of the other. + val exactNotType = unifyTypes(statements.map { it.exactNotType }, onlyInputTypes = true) + MutableTypeStatement(variable, exactType, exactNotType?.let { mutableSetOf(it) } ?: mutableSetOf()) + } else { + val exactType = unifyTypes(statements.map { it.exactType }, onlyInputTypes = false) + val exactNotType = statements.flatMapTo(mutableSetOf()) { it.exactNotType } + MutableTypeStatement(variable, exactType?.let { mutableSetOf(it) } ?: mutableSetOf(), exactNotType) + } } - protected fun or(statements: Collection): MutableTypeStatement = - manipulateTypeStatements(statements, ::orForTypes) - - private fun orForTypes(types: Collection>): MutableSet { - if (types.any { it.isEmpty() }) return mutableSetOf() - val intersectedTypes = types.map { - if (it.size > 1) { - context.intersectTypes(it.toList()) - } else { - assert(it.size == 1) { "We've already checked each set of types is not empty." } - it.single() - } - } - val result = mutableSetOf() - context.commonSuperTypeOrNull(intersectedTypes)?.let { - if (it.isAcceptableForSmartcast()) { - result.add(it) - } else if (!it.canBeNull) { - result.add(context.anyType()) - } - Unit - } - return result + private fun unifyTypes(types: Collection>, onlyInputTypes: Boolean): ConeKotlinType? { + if (types.any { it.isEmpty() }) return null + val intersected = types.map { ConeTypeIntersector.intersectTypes(context, it.toList()) } + val unified = context.commonSuperTypeOrNull(intersected) ?: return null + return when { + unified.isAcceptableForSmartcast() -> unified + unified.canBeNull -> null + else -> context.anyType() + }.takeIf { !onlyInputTypes || it in intersected } } protected fun and(statements: Collection): MutableTypeStatement = - manipulateTypeStatements(statements, ::andForTypes) + foldStatements(statements, all = true) - private fun andForTypes(types: Collection>): MutableSet { - return types.flatMapTo(mutableSetOf()) { it } - } + protected fun or(statements: Collection): MutableTypeStatement = + foldStatements(statements, all = false) } fun LogicSystem.approveOperationStatement( 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 fc990d146a5..433057b2c8b 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 @@ -18,20 +18,8 @@ data class PersistentTypeStatement( override val exactType: PersistentSet, override val exactNotType: PersistentSet ) : TypeStatement() { - override operator fun plus(other: TypeStatement): PersistentTypeStatement { - return PersistentTypeStatement( - variable, - exactType + other.exactType, - exactNotType + other.exactNotType - ) - } - - override val isEmpty: Boolean - get() = exactType.isEmpty() && exactNotType.isEmpty() - - override fun invert(): PersistentTypeStatement { - return PersistentTypeStatement(variable, exactNotType, exactType) - } + override fun invert(): PersistentTypeStatement = + PersistentTypeStatement(variable, exactNotType, exactType) } typealias PersistentApprovedTypeStatements = PersistentMap @@ -242,6 +230,9 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste } } + private fun PersistentApprovedTypeStatements.addTypeStatement(info: TypeStatement): PersistentApprovedTypeStatements = + put(info.variable, { info.toPersistent() }, { and(listOf(it, info)).toPersistent() }) + override fun addImplication(flow: PersistentFlow, implication: Implication) { if ((implication.effect as? TypeStatement)?.isEmpty == true) return if (implication.condition == implication.effect) return @@ -288,14 +279,10 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste val updatedReceivers = mutableSetOf() approvedFacts.asMap().forEach { (variable, infos) -> - var resultInfo = PersistentTypeStatement(variable, persistentSetOf(), persistentSetOf()) - for (info in infos) { - resultInfo += info - } if (variable.isThisReference) { updatedReceivers += variable } - addTypeStatement(resultFlow, resultInfo) + addTypeStatement(resultFlow, and(infos)) } updatedReceivers.forEach { @@ -361,13 +348,7 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste val approveOperationStatements = approveOperationStatementsInternal(flow, approvedStatement, statements, shouldRemoveSynthetics = false) approveOperationStatements.asMap().forEach { (variable, infos) -> - for (info in infos) { - val mutableInfo = info.asMutableStatement() - destination.put(variable, mutableInfo) { - it += mutableInfo - it - } - } + destination.put(variable, { and(infos) }, { and(listOf(it) + infos) }) } } @@ -416,9 +397,6 @@ private fun lowestCommonFlow(left: PersistentFlow, right: PersistentFlow): Persi return left } -private fun PersistentApprovedTypeStatements.addTypeStatement(info: TypeStatement): PersistentApprovedTypeStatements = - put(info.variable, { info.toPersistent() }, { it + info }) - private fun TypeStatement.toPersistent(): PersistentTypeStatement = when (this) { is PersistentTypeStatement -> this else -> PersistentTypeStatement(variable, exactType.toPersistentSet(), exactNotType.toPersistentSet()) diff --git a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/model.kt b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/model.kt index 2dfb544ff93..6f3804aee06 100644 --- a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/model.kt +++ b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/model.kt @@ -12,22 +12,11 @@ import kotlin.contracts.contract // --------------------------------------- Facts --------------------------------------- -operator fun TypeStatement.plus(other: TypeStatement?): TypeStatement = other?.let { this + other } ?: this - class MutableTypeStatement( override val variable: RealVariable, override val exactType: MutableSet = linkedSetOf(), override val exactNotType: MutableSet = linkedSetOf() ) : TypeStatement() { - override fun plus(other: TypeStatement): MutableTypeStatement = MutableTypeStatement( - variable, - LinkedHashSet(exactType).apply { addAll(other.exactType) }, - LinkedHashSet(exactNotType).apply { addAll(other.exactNotType) } - ) - - override val isEmpty: Boolean - get() = exactType.isEmpty() && exactType.isEmpty() - override fun invert(): MutableTypeStatement { return MutableTypeStatement( variable, @@ -36,11 +25,6 @@ class MutableTypeStatement( ) } - operator fun plusAssign(info: TypeStatement) { - exactType += info.exactType - exactNotType += info.exactNotType - } - fun copy(): MutableTypeStatement = MutableTypeStatement(variable, LinkedHashSet(exactType), LinkedHashSet(exactNotType)) } @@ -51,17 +35,8 @@ fun Implication.invertCondition(): Implication = Implication(condition.invert(), typealias TypeStatements = Map typealias MutableTypeStatements = MutableMap -typealias MutableOperationStatements = MutableMap - -fun MutableTypeStatements.addStatement(variable: RealVariable, statement: TypeStatement) { - put(variable, statement.asMutableStatement()) { it.apply { this += statement } } -} - -fun MutableTypeStatements.mergeTypeStatements(other: TypeStatements) { - other.forEach { (variable, info) -> - addStatement(variable, info) - } -} +fun TypeStatements.asMutableStatements(): MutableTypeStatements = + mapValuesTo(mutableMapOf()) { it.value.asMutableStatement() } // --------------------------------------- DSL --------------------------------------- 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 67d45739722..2ffef45dcf8 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 @@ -34,9 +34,11 @@ abstract class TypeStatement : Statement() { abstract val exactType: Set abstract val exactNotType: Set - abstract operator fun plus(other: TypeStatement): TypeStatement - abstract val isEmpty: Boolean - val isNotEmpty: Boolean get() = !isEmpty + val isEmpty: Boolean + get() = exactType.isEmpty() && exactNotType.isEmpty() + + val isNotEmpty: Boolean + get() = !isEmpty override fun toString(): String { return "$variable: $exactType, $exactNotType" diff --git a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/util.kt b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/util.kt index b87272ba9fa..e8b3e743a2f 100644 --- a/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/util.kt +++ b/compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/util.kt @@ -26,13 +26,14 @@ import kotlin.contracts.InvocationKind import kotlin.contracts.contract @OptIn(ExperimentalContracts::class) -internal inline fun MutableMap.put(key: K, value: V, remappingFunction: (existing: V) -> V) { +internal inline fun MutableMap.put(key: K, valueProducer: () -> V, remappingFunction: (existing: V) -> V) { contract { callsInPlace(remappingFunction, InvocationKind.AT_MOST_ONCE) + callsInPlace(valueProducer, InvocationKind.AT_MOST_ONCE) } val existing = this[key] if (existing == null) { - put(key, value) + put(key, valueProducer()) } else { put(key, remappingFunction(existing)) }