FIR DFA: x !is T? => x != null

^KT-22996 tag fixed-in-k2
This commit is contained in:
pyos
2022-11-14 17:18:01 +01:00
committed by teamcity
parent 02fedeb9ed
commit f485413cfd
18 changed files with 118 additions and 53 deletions
@@ -401,10 +401,10 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
if (!type.canBeNull) {
// x is (T & Any) => x != null
flow.addImplication((expressionVariable eq isType) implies (operandVariable notEq null))
} else {
// TODO? (KT-22996) x !is T? => x != null; don't forget to change `approveContractStatement`
// flow.addImplication((expressionVariable eq !isType) implies (operandVariable notEq null))
}
} else if (type.isMarkedNullable) {
// x !is T? => x != null
flow.addImplication((expressionVariable eq !isType) implies (operandVariable notEq null))
} // else probably a type parameter, so which implication is correct depends on instantiation
}
}
}
@@ -418,8 +418,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
} else {
val expressionVariable = variableStorage.createSynthetic(typeOperatorCall)
flow.addImplication((expressionVariable notEq null) implies (operandVariable notEq null))
// TODO? (x as T?) == null => x == null
// flow.addImplication((expressionVariable eq null) implies (operandVariable eq null))
flow.addImplication((expressionVariable eq null) implies (operandVariable eq null))
}
}
@@ -45,9 +45,11 @@ fun <F : Flow> LogicSystem<F>.approveContractStatement(
substitutedType.isAny -> it.processEqNull(!isType)
substitutedType.isNullableNothing -> it.processEqNull(isType)
else -> {
// x is (T & Any) => x != null
// TODO? (KT-22996) x !is T? => x != null: change `&&` to `==`
val fromNullability = if (isType && !type.canBeNull) it.processEqNull(false) else mapOf()
// x is (T & Any) || x !is T? => x != null
val fromNullability = if ((isType && !type.canBeNull) || (!isType && type.isMarkedNullable))
it.processEqNull(false)
else
mapOf()
if (isType && it is RealVariable) {
andForTypeStatements(fromNullability, mapOf(it to (it typeEq substitutedType)))
} else {