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?`.
This commit is contained in:
+5
-19
@@ -76,7 +76,6 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
|
|||||||
val effect = effectDeclaration.effect as ConeReturnsEffectDeclaration
|
val effect = effectDeclaration.effect as ConeReturnsEffectDeclaration
|
||||||
val builtinTypes = context.session.builtinTypes
|
val builtinTypes = context.session.builtinTypes
|
||||||
val typeContext = context.session.typeContext
|
val typeContext = context.session.typeContext
|
||||||
val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow
|
|
||||||
|
|
||||||
val isReturn = node is JumpNode && node.fir is FirReturnExpression
|
val isReturn = node is JumpNode && node.fir is FirReturnExpression
|
||||||
val resultExpression = if (isReturn) (node.fir as FirReturnExpression).result else node.fir
|
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
|
// TODO: create separate variable storage and don't modify existing one
|
||||||
val variableStorage = dataFlowInfo.variableStorage as VariableStorageImpl
|
val variableStorage = dataFlowInfo.variableStorage as VariableStorageImpl
|
||||||
|
val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow
|
||||||
var typeStatements: TypeStatements = flow.approvedTypeStatements
|
var typeStatements: TypeStatements = flow.approvedTypeStatements
|
||||||
|
|
||||||
if (effect.value != ConeConstantReference.WILDCARD) {
|
if (effect.value != ConeConstantReference.WILDCARD) {
|
||||||
@@ -103,7 +102,10 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
|
|||||||
if (!resultExpression.isApplicableWith(operation)) return false
|
if (!resultExpression.isApplicableWith(operation)) return false
|
||||||
} else {
|
} else {
|
||||||
val resultVar = variableStorage.getOrCreate(flow, resultExpression)
|
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
|
return false
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun LogicSystem<PersistentFlow>.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(
|
private fun ConeBooleanExpression.buildTypeStatements(
|
||||||
function: FirFunction,
|
function: FirFunction,
|
||||||
logicSystem: LogicSystem<*>,
|
logicSystem: LogicSystem<*>,
|
||||||
|
|||||||
+33
-39
@@ -45,7 +45,6 @@ class DataFlowAnalyzerContext<FLOW : Flow>(
|
|||||||
val graphBuilder: ControlFlowGraphBuilder,
|
val graphBuilder: ControlFlowGraphBuilder,
|
||||||
variableStorage: VariableStorageImpl,
|
variableStorage: VariableStorageImpl,
|
||||||
flowOnNodes: MutableMap<CFGNode<*>, FLOW>,
|
flowOnNodes: MutableMap<CFGNode<*>, FLOW>,
|
||||||
val variablesForWhenConditions: MutableMap<WhenBranchConditionExitNode, DataFlowVariable>,
|
|
||||||
val preliminaryLoopVisitor: PreliminaryLoopVisitor
|
val preliminaryLoopVisitor: PreliminaryLoopVisitor
|
||||||
) {
|
) {
|
||||||
var flowOnNodes = flowOnNodes
|
var flowOnNodes = flowOnNodes
|
||||||
@@ -63,7 +62,6 @@ class DataFlowAnalyzerContext<FLOW : Flow>(
|
|||||||
|
|
||||||
fun reset() {
|
fun reset() {
|
||||||
graphBuilder.reset()
|
graphBuilder.reset()
|
||||||
variablesForWhenConditions.clear()
|
|
||||||
|
|
||||||
variableStorage = variableStorage.clear()
|
variableStorage = variableStorage.clear()
|
||||||
flowOnNodes = mutableMapOf()
|
flowOnNodes = mutableMapOf()
|
||||||
@@ -76,7 +74,7 @@ class DataFlowAnalyzerContext<FLOW : Flow>(
|
|||||||
fun <FLOW : Flow> empty(session: FirSession): DataFlowAnalyzerContext<FLOW> =
|
fun <FLOW : Flow> empty(session: FirSession): DataFlowAnalyzerContext<FLOW> =
|
||||||
DataFlowAnalyzerContext(
|
DataFlowAnalyzerContext(
|
||||||
ControlFlowGraphBuilder(), VariableStorageImpl(session),
|
ControlFlowGraphBuilder(), VariableStorageImpl(session),
|
||||||
mutableMapOf(), mutableMapOf(), PreliminaryLoopVisitor()
|
mutableMapOf(), PreliminaryLoopVisitor()
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -410,6 +408,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
} else {
|
} else {
|
||||||
val expressionVariable = variableStorage.createSynthetic(typeOperatorCall)
|
val expressionVariable = variableStorage.createSynthetic(typeOperatorCall)
|
||||||
flow.addImplication((expressionVariable notEq null) implies (operandVariable notEq null))
|
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<FLOW : Flow>(
|
|||||||
val flow = node.flow
|
val flow = node.flow
|
||||||
val operandVariable = variableStorage.getOrCreateIfReal(flow, operand) ?: return
|
val operandVariable = variableStorage.getOrCreateIfReal(flow, operand) ?: return
|
||||||
val expressionVariable = variableStorage.createSynthetic(node.fir)
|
val expressionVariable = variableStorage.createSynthetic(node.fir)
|
||||||
// expression == non-null const -> expression != null
|
if (const.kind == ConstantValueKind.Boolean && operand.coneType.isBooleanOrNullableBoolean) {
|
||||||
flow.addImplication((expressionVariable eq isEq) implies (operandVariable notEq null))
|
|
||||||
if (const.kind == ConstantValueKind.Boolean) {
|
|
||||||
val expected = (const.value as Boolean)
|
val expected = (const.value as Boolean)
|
||||||
flow.addImplication((expressionVariable eq isEq) implies (operandVariable eq expected))
|
flow.addImplication((expressionVariable eq isEq) implies (operandVariable eq expected))
|
||||||
if (operand.coneType.isBoolean) {
|
if (operand.coneType.isBoolean) {
|
||||||
flow.addImplication((expressionVariable eq !isEq) implies (operandVariable eq !expected))
|
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<FLOW : Flow>(
|
|||||||
val previousConditionExitNode = previousNodes.singleOrNull()
|
val previousConditionExitNode = previousNodes.singleOrNull()
|
||||||
if (previousConditionExitNode is WhenBranchConditionExitNode) {
|
if (previousConditionExitNode is WhenBranchConditionExitNode) {
|
||||||
val flow = mergeIncomingFlow()
|
val flow = mergeIncomingFlow()
|
||||||
val previousConditionVariable = context.variablesForWhenConditions.remove(previousConditionExitNode) ?: return
|
val previousCondition = previousConditionExitNode.fir.condition
|
||||||
flow.commitOperationStatement(previousConditionVariable eq false)
|
if (previousCondition.coneType.isBoolean) {
|
||||||
|
val previousConditionVariable = variableStorage.get(flow, previousCondition) ?: return
|
||||||
|
flow.commitOperationStatement(previousConditionVariable eq false)
|
||||||
|
}
|
||||||
} else { // first branch
|
} else { // first branch
|
||||||
mergeIncomingFlow()
|
mergeIncomingFlow()
|
||||||
}
|
}
|
||||||
@@ -631,9 +634,11 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
val (conditionExitNode, resultEnterNode) = graphBuilder.exitWhenBranchCondition(whenBranch)
|
val (conditionExitNode, resultEnterNode) = graphBuilder.exitWhenBranchCondition(whenBranch)
|
||||||
val conditionExitFlow = conditionExitNode.mergeIncomingFlow()
|
val conditionExitFlow = conditionExitNode.mergeIncomingFlow()
|
||||||
val resultEnterFlow = resultEnterNode.mergeIncomingFlow()
|
val resultEnterFlow = resultEnterNode.mergeIncomingFlow()
|
||||||
val conditionVariable = variableStorage.get(conditionExitFlow, whenBranch.condition) ?: return
|
// If the condition is invalid, don't generate smart casts to Any or Boolean.
|
||||||
context.variablesForWhenConditions[conditionExitNode] = conditionVariable
|
if (whenBranch.condition.coneType.isBoolean) {
|
||||||
resultEnterFlow.commitOperationStatement(conditionVariable eq true)
|
val conditionVariable = variableStorage.get(conditionExitFlow, whenBranch.condition) ?: return
|
||||||
|
resultEnterFlow.commitOperationStatement(conditionVariable eq true)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fun exitWhenBranchResult(whenBranch: FirWhenBranch) {
|
fun exitWhenBranchResult(whenBranch: FirWhenBranch) {
|
||||||
@@ -664,8 +669,10 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
val (loopConditionExitNode, loopBlockEnterNode) = graphBuilder.exitWhileLoopCondition(loop)
|
val (loopConditionExitNode, loopBlockEnterNode) = graphBuilder.exitWhileLoopCondition(loop)
|
||||||
val conditionExitFlow = loopConditionExitNode.mergeIncomingFlow()
|
val conditionExitFlow = loopConditionExitNode.mergeIncomingFlow()
|
||||||
val blockEnterFlow = loopBlockEnterNode.mergeIncomingFlow()
|
val blockEnterFlow = loopBlockEnterNode.mergeIncomingFlow()
|
||||||
val conditionVariable = variableStorage.get(conditionExitFlow, loop.condition) ?: return
|
if (loop.condition.coneType.isBoolean) {
|
||||||
blockEnterFlow.commitOperationStatement(conditionVariable eq true)
|
val conditionVariable = variableStorage.get(conditionExitFlow, loop.condition) ?: return
|
||||||
|
blockEnterFlow.commitOperationStatement(conditionVariable eq true)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fun exitWhileLoop(loop: FirLoop) {
|
fun exitWhileLoop(loop: FirLoop) {
|
||||||
@@ -679,8 +686,10 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
val flow = mergeIncomingFlow()
|
val flow = mergeIncomingFlow()
|
||||||
// Might be > 1 node or other type if there are `break`s:
|
// Might be > 1 node or other type if there are `break`s:
|
||||||
val singlePreviousNode = previousNodes.singleOrNull { !it.isDead } as? LoopConditionExitNode ?: return
|
val singlePreviousNode = previousNodes.singleOrNull { !it.isDead } as? LoopConditionExitNode ?: return
|
||||||
val variable = variableStorage.get(flow, singlePreviousNode.fir) ?: return
|
if (singlePreviousNode.fir.coneType.isBoolean) {
|
||||||
flow.commitOperationStatement(variable eq false)
|
val variable = variableStorage.get(flow, singlePreviousNode.fir) ?: return
|
||||||
|
flow.commitOperationStatement(variable eq false)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun enterCapturingStatement(flow: FLOW, statement: FirStatement) {
|
private fun enterCapturingStatement(flow: FLOW, statement: FirStatement) {
|
||||||
@@ -1044,14 +1053,16 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
val flow = node.mergeIncomingFlow()
|
val flow = node.mergeIncomingFlow()
|
||||||
|
|
||||||
val leftVariable = variableStorage.get(flowFromLeft, binaryLogicExpression.leftOperand)
|
val leftVariable = variableStorage.get(flowFromLeft, binaryLogicExpression.leftOperand)
|
||||||
|
val leftIsBoolean = leftVariable != null && binaryLogicExpression.leftOperand.coneType.isBoolean
|
||||||
if (!node.leftOperandNode.isDead && node.rightOperandNode.isDead) {
|
if (!node.leftOperandNode.isDead && node.rightOperandNode.isDead) {
|
||||||
// If the right operand does not terminate, then we know that the value of the entire expression
|
// 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.
|
// has to be saturating (true for or, false for and), and it has to be produced by the left operand.
|
||||||
if (leftVariable != null) {
|
if (leftIsBoolean) {
|
||||||
flow.commitOperationStatement(leftVariable eq !isAnd)
|
flow.commitOperationStatement(leftVariable!! eq !isAnd)
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
val rightVariable = variableStorage.get(flowFromRight, binaryLogicExpression.rightOperand)
|
val rightVariable = variableStorage.get(flowFromRight, binaryLogicExpression.rightOperand)
|
||||||
|
val rightIsBoolean = rightVariable != null && binaryLogicExpression.rightOperand.coneType.isBoolean
|
||||||
val operatorVariable = variableStorage.createSynthetic(binaryLogicExpression)
|
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.
|
// 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.
|
// Approved type statements for RHS already contain everything implied by the corresponding value of LHS.
|
||||||
@@ -1059,19 +1070,19 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
// TODO? `bothEvaluated` also implies all implications from RHS. This requires a second level
|
// 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.
|
// of implications, which the logic system currently doesn't support. See also safe calls.
|
||||||
flow.addAllConditionally(bothEvaluated, flowFromRight.approvedTypeStatements)
|
flow.addAllConditionally(bothEvaluated, flowFromRight.approvedTypeStatements)
|
||||||
if (rightVariable != null) {
|
if (rightIsBoolean) {
|
||||||
flow.addAllConditionally(bothEvaluated, logicSystem.approveOperationStatement(flowFromRight, rightVariable eq isAnd))
|
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 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 `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(
|
flow.addAllConditionally(
|
||||||
operatorVariable eq !isAnd,
|
operatorVariable eq !isAnd,
|
||||||
logicSystem.orForTypeStatements(
|
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.
|
// 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) */ }
|
// 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<FLOW : Flow>(
|
|||||||
}
|
}
|
||||||
|
|
||||||
private fun FLOW.addImplication(statement: Implication) {
|
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)
|
logicSystem.addImplication(this, statement)
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1277,12 +1277,6 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
logicSystem.approveOperationStatement(this, statement, removeApprovedOrImpossible = true).values.forEach {
|
logicSystem.approveOperationStatement(this, statement, removeApprovedOrImpossible = true).values.forEach {
|
||||||
addTypeStatement(it)
|
addTypeStatement(it)
|
||||||
}
|
}
|
||||||
if (statement.operation == Operation.NotEqNull) {
|
|
||||||
val variable = statement.variable
|
|
||||||
if (variable is RealVariable) {
|
|
||||||
addTypeStatement(variable typeEq any)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private val CFGNode<*>.previousFlow: FLOW
|
private val CFGNode<*>.previousFlow: FLOW
|
||||||
|
|||||||
@@ -79,12 +79,17 @@ abstract class LogicSystem<FLOW : Flow>(protected val context: ConeInferenceCont
|
|||||||
val intersected = types.map { ConeTypeIntersector.intersectTypes(context, it.toList()) }
|
val intersected = types.map { ConeTypeIntersector.intersectTypes(context, it.toList()) }
|
||||||
val unified = context.commonSuperTypeOrNull(intersected) ?: return null
|
val unified = context.commonSuperTypeOrNull(intersected) ?: return null
|
||||||
return when {
|
return when {
|
||||||
|
unified.isNullableAny -> null
|
||||||
unified.isAcceptableForSmartcast() -> unified
|
unified.isAcceptableForSmartcast() -> unified
|
||||||
unified.canBeNull -> null
|
unified.canBeNull -> null
|
||||||
else -> context.anyType()
|
else -> context.anyType()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
protected operator fun MutableTypeStatement.plusAssign(other: TypeStatement) {
|
||||||
|
exactType += other.exactType
|
||||||
|
}
|
||||||
|
|
||||||
protected fun and(statements: Collection<TypeStatement>): TypeStatement? =
|
protected fun and(statements: Collection<TypeStatement>): TypeStatement? =
|
||||||
statements.singleOrNew { statements.flatMapTo(mutableSetOf()) { it.exactType } }
|
statements.singleOrNew { statements.flatMapTo(mutableSetOf()) { it.exactType } }
|
||||||
|
|
||||||
|
|||||||
+17
-7
@@ -5,7 +5,6 @@
|
|||||||
|
|
||||||
package org.jetbrains.kotlin.fir.resolve.dfa
|
package org.jetbrains.kotlin.fir.resolve.dfa
|
||||||
|
|
||||||
import com.google.common.collect.ArrayListMultimap
|
|
||||||
import kotlinx.collections.immutable.*
|
import kotlinx.collections.immutable.*
|
||||||
import org.jetbrains.kotlin.fir.types.ConeInferenceContext
|
import org.jetbrains.kotlin.fir.types.ConeInferenceContext
|
||||||
import org.jetbrains.kotlin.fir.types.ConeKotlinType
|
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(
|
override fun approveOperationStatement(
|
||||||
flow: PersistentFlow,
|
flow: PersistentFlow,
|
||||||
approvedStatement: OperationStatement,
|
approvedStatement: OperationStatement,
|
||||||
removeApprovedOrImpossible: Boolean,
|
removeApprovedOrImpossible: Boolean,
|
||||||
): TypeStatements {
|
): TypeStatements {
|
||||||
val approvedTypeStatements: ArrayListMultimap<RealVariable, TypeStatement> = ArrayListMultimap.create()
|
val result = mutableMapOf<RealVariable, MutableTypeStatement>()
|
||||||
val queue = LinkedList<OperationStatement>().apply { this += approvedStatement }
|
val queue = LinkedList<OperationStatement>().apply { this += approvedStatement }
|
||||||
val approved = mutableSetOf<OperationStatement>()
|
val approved = mutableSetOf<OperationStatement>()
|
||||||
while (queue.isNotEmpty()) {
|
while (queue.isNotEmpty()) {
|
||||||
val next: OperationStatement = queue.removeFirst()
|
val next = queue.removeFirst()
|
||||||
// Defense from cycles in facts
|
// Defense from cycles in facts
|
||||||
if (!approved.add(next)) continue
|
if (!removeApprovedOrImpossible && !approved.add(next)) continue
|
||||||
|
|
||||||
|
val operation = next.operation
|
||||||
val variable = next.variable
|
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 statements = flow.logicStatements[variable] ?: continue
|
||||||
val stillUnknown = statements.removeAll {
|
val stillUnknown = statements.removeAll {
|
||||||
val knownValue = it.condition.operation.valueIfKnown(next.operation)
|
val knownValue = it.condition.operation.valueIfKnown(operation)
|
||||||
if (knownValue == true) {
|
if (knownValue == true) {
|
||||||
when (val effect = it.effect) {
|
when (val effect = it.effect) {
|
||||||
is OperationStatement -> queue += 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
|
removeApprovedOrImpossible && knownValue != null
|
||||||
@@ -284,7 +294,7 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste
|
|||||||
flow.logicStatements = flow.logicStatements.put(variable, stillUnknown)
|
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) {
|
override fun recordNewAssignment(flow: PersistentFlow, variable: RealVariable, index: Int) {
|
||||||
|
|||||||
@@ -54,7 +54,7 @@ enum class Operation {
|
|||||||
fun valueIfKnown(given: Operation): Boolean? = when (this) {
|
fun valueIfKnown(given: Operation): Boolean? = when (this) {
|
||||||
EqTrue, EqFalse -> if (given == NotEqNull) null else given == this
|
EqTrue, EqFalse -> if (given == NotEqNull) null else given == this
|
||||||
EqNull -> given == EqNull
|
EqNull -> given == EqNull
|
||||||
NotEqNull -> given == NotEqNull
|
NotEqNull -> given != EqNull
|
||||||
}
|
}
|
||||||
|
|
||||||
override fun toString(): String = when (this) {
|
override fun toString(): String = when (this) {
|
||||||
|
|||||||
+3
-1
@@ -1,4 +1,6 @@
|
|||||||
// !LANGUAGE: +InlineClasses
|
// !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
|
// FILE: utils.kt
|
||||||
|
|
||||||
@@ -16,4 +18,4 @@ fun test(x: UInt?, y: UInt) {
|
|||||||
// 3 INVOKEVIRTUAL UInt.unbox
|
// 3 INVOKEVIRTUAL UInt.unbox
|
||||||
|
|
||||||
// 0 valueOf
|
// 0 valueOf
|
||||||
// 0 intValue
|
// 0 intValue
|
||||||
|
|||||||
@@ -19,7 +19,7 @@ fun case_2(x: Int?) {
|
|||||||
|
|
||||||
// TESTCASE NUMBER: 3
|
// TESTCASE NUMBER: 3
|
||||||
fun case_3(x: Boolean?) {
|
fun case_3(x: Boolean?) {
|
||||||
if (x ?: (x != null)) {
|
if (x ?: (<!SENSELESS_COMPARISON!>x != null<!>)) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -11,8 +11,8 @@ fun case_1() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
println(x ?: break)
|
println(x ?: break)
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.String?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.String? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.String?")!>x<!><!UNSAFE_CALL!>.<!>length
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.String? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>length
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -25,8 +25,8 @@ fun case_2(y: MutableList<Int>) {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y[x ?: break] = 10
|
y[x ?: break] = 10
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -39,8 +39,8 @@ fun case_3(y: MutableList<Int>) {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y[0] = x ?: break
|
y[0] = x ?: break
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 4
|
// TESTCASE NUMBER: 4
|
||||||
@@ -49,8 +49,8 @@ fun case_4() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
x ?: break
|
x ?: break
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 5
|
// TESTCASE NUMBER: 5
|
||||||
@@ -59,8 +59,8 @@ fun case_5(y: Boolean) {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y && (x ?: break)
|
y && (x ?: break)
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 6
|
// TESTCASE NUMBER: 6
|
||||||
@@ -69,8 +69,8 @@ fun case_6(y: Boolean) {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y || (x ?: break)
|
y || (x ?: break)
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 7
|
// TESTCASE NUMBER: 7
|
||||||
@@ -94,8 +94,8 @@ fun case_8() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y += x ?: break
|
y += x ?: break
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -109,8 +109,8 @@ fun case_9() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
y -= x ?: break
|
y -= x ?: break
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -124,8 +124,8 @@ fun case_10() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
val z = y - (x ?: break)
|
val z = y - (x ?: break)
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -139,8 +139,8 @@ fun case_11() {
|
|||||||
while (true) {
|
while (true) {
|
||||||
val z = y * (x ?: break)
|
val z = y * (x ?: break)
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Int? & kotlin.Nothing?")!>x<!><!UNSAFE_CALL!>.<!>inv()
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 12
|
// TESTCASE NUMBER: 12
|
||||||
|
|||||||
@@ -19,7 +19,7 @@ fun case_2(x: Int?) {
|
|||||||
|
|
||||||
// TESTCASE NUMBER: 3
|
// TESTCASE NUMBER: 3
|
||||||
fun case_3(x: Boolean?) {
|
fun case_3(x: Boolean?) {
|
||||||
if (x ?: (x != null)) {
|
if (x ?: (<!SENSELESS_COMPARISON!>x != null<!>)) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Boolean?")!>x<!><!UNSAFE_CALL!>.<!>not()
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -48,7 +48,7 @@ fun case_4(x: Any?) {
|
|||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
|
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
||||||
}
|
}
|
||||||
|
|
||||||
// TESTCASE NUMBER: 5
|
// TESTCASE NUMBER: 5
|
||||||
|
|||||||
Reference in New Issue
Block a user