FIR DFA: generate type implications on all null comparisons
This commit is contained in:
+41
-45
@@ -388,11 +388,10 @@ digraph jumpFromRhsOfOperator_kt {
|
|||||||
153 [label="Exit when"];
|
153 [label="Exit when"];
|
||||||
}
|
}
|
||||||
154 [label="Access variable R|<local>/a|"];
|
154 [label="Access variable R|<local>/a|"];
|
||||||
155 [label="Smart cast: R|<local>/a|"];
|
155 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
||||||
156 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
156 [label="Exit block"];
|
||||||
157 [label="Exit block"];
|
|
||||||
}
|
}
|
||||||
158 [label="Exit function test_7" style="filled" fillcolor=red];
|
157 [label="Exit function test_7" style="filled" fillcolor=red];
|
||||||
}
|
}
|
||||||
130 -> {131};
|
130 -> {131};
|
||||||
131 -> {132};
|
131 -> {132};
|
||||||
@@ -405,7 +404,7 @@ digraph jumpFromRhsOfOperator_kt {
|
|||||||
138 -> {143 139};
|
138 -> {143 139};
|
||||||
139 -> {140};
|
139 -> {140};
|
||||||
140 -> {141};
|
140 -> {141};
|
||||||
141 -> {158} [label=onUncaughtException];
|
141 -> {157} [label=onUncaughtException];
|
||||||
141 -> {142} [style=dotted];
|
141 -> {142} [style=dotted];
|
||||||
142 -> {143} [style=dotted];
|
142 -> {143} [style=dotted];
|
||||||
143 -> {144};
|
143 -> {144};
|
||||||
@@ -422,55 +421,54 @@ digraph jumpFromRhsOfOperator_kt {
|
|||||||
154 -> {155};
|
154 -> {155};
|
||||||
155 -> {156};
|
155 -> {156};
|
||||||
156 -> {157};
|
156 -> {157};
|
||||||
157 -> {158};
|
|
||||||
|
|
||||||
subgraph cluster_32 {
|
subgraph cluster_32 {
|
||||||
color=red
|
color=red
|
||||||
159 [label="Enter function test_8" style="filled" fillcolor=red];
|
158 [label="Enter function test_8" style="filled" fillcolor=red];
|
||||||
subgraph cluster_33 {
|
subgraph cluster_33 {
|
||||||
color=blue
|
color=blue
|
||||||
160 [label="Enter block"];
|
159 [label="Enter block"];
|
||||||
subgraph cluster_34 {
|
subgraph cluster_34 {
|
||||||
color=blue
|
color=blue
|
||||||
161 [label="Enter when"];
|
160 [label="Enter when"];
|
||||||
subgraph cluster_35 {
|
subgraph cluster_35 {
|
||||||
color=blue
|
color=blue
|
||||||
162 [label="Enter when branch condition "];
|
161 [label="Enter when branch condition "];
|
||||||
subgraph cluster_36 {
|
subgraph cluster_36 {
|
||||||
color=blue
|
color=blue
|
||||||
163 [label="Enter &&"];
|
162 [label="Enter &&"];
|
||||||
164 [label="Access variable R|<local>/a|"];
|
163 [label="Access variable R|<local>/a|"];
|
||||||
165 [label="Const: Null(null)"];
|
164 [label="Const: Null(null)"];
|
||||||
166 [label="Equality operator !="];
|
165 [label="Equality operator !="];
|
||||||
167 [label="Exit left part of &&"];
|
166 [label="Exit left part of &&"];
|
||||||
168 [label="Enter right part of &&"];
|
167 [label="Enter right part of &&"];
|
||||||
169 [label="Function call: R|java/lang/Exception.Exception|()"];
|
168 [label="Function call: R|java/lang/Exception.Exception|()"];
|
||||||
170 [label="Throw: throw R|java/lang/Exception.Exception|()"];
|
169 [label="Throw: throw R|java/lang/Exception.Exception|()"];
|
||||||
171 [label="Stub" style="filled" fillcolor=gray];
|
170 [label="Stub" style="filled" fillcolor=gray];
|
||||||
172 [label="Exit &&"];
|
171 [label="Exit &&"];
|
||||||
}
|
}
|
||||||
173 [label="Exit when branch condition"];
|
172 [label="Exit when branch condition"];
|
||||||
}
|
}
|
||||||
174 [label="Synthetic else branch"];
|
173 [label="Synthetic else branch"];
|
||||||
175 [label="Enter when branch result"];
|
174 [label="Enter when branch result"];
|
||||||
subgraph cluster_37 {
|
subgraph cluster_37 {
|
||||||
color=blue
|
color=blue
|
||||||
176 [label="Enter block"];
|
175 [label="Enter block"];
|
||||||
177 [label="Access variable R|<local>/a|"];
|
176 [label="Access variable R|<local>/a|"];
|
||||||
178 [label="Smart cast: R|<local>/a|"];
|
177 [label="Smart cast: R|<local>/a|"];
|
||||||
179 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
178 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
||||||
180 [label="Exit block"];
|
179 [label="Exit block"];
|
||||||
}
|
}
|
||||||
181 [label="Exit when branch result"];
|
180 [label="Exit when branch result"];
|
||||||
182 [label="Exit when"];
|
181 [label="Exit when"];
|
||||||
}
|
}
|
||||||
183 [label="Access variable R|<local>/a|"];
|
182 [label="Access variable R|<local>/a|"];
|
||||||
184 [label="Smart cast: R|<local>/a|"];
|
183 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
||||||
185 [label="Function call: R|<local>/a|.<Inapplicable(UNSAFE_CALL): /A.foo>#()"];
|
184 [label="Exit block"];
|
||||||
186 [label="Exit block"];
|
|
||||||
}
|
}
|
||||||
187 [label="Exit function test_8" style="filled" fillcolor=red];
|
185 [label="Exit function test_8" style="filled" fillcolor=red];
|
||||||
}
|
}
|
||||||
|
158 -> {159};
|
||||||
159 -> {160};
|
159 -> {160};
|
||||||
160 -> {161};
|
160 -> {161};
|
||||||
161 -> {162};
|
161 -> {162};
|
||||||
@@ -478,16 +476,16 @@ digraph jumpFromRhsOfOperator_kt {
|
|||||||
163 -> {164};
|
163 -> {164};
|
||||||
164 -> {165};
|
164 -> {165};
|
||||||
165 -> {166};
|
165 -> {166};
|
||||||
166 -> {167};
|
166 -> {171 167};
|
||||||
167 -> {172 168};
|
167 -> {168};
|
||||||
168 -> {169};
|
168 -> {169};
|
||||||
169 -> {170};
|
169 -> {185} [label=onUncaughtException];
|
||||||
170 -> {187} [label=onUncaughtException];
|
169 -> {170} [style=dotted];
|
||||||
170 -> {171} [style=dotted];
|
170 -> {171} [style=dotted];
|
||||||
171 -> {172} [style=dotted];
|
171 -> {172};
|
||||||
172 -> {173};
|
172 -> {174 173};
|
||||||
173 -> {175 174};
|
173 -> {181};
|
||||||
174 -> {182};
|
174 -> {175};
|
||||||
175 -> {176};
|
175 -> {176};
|
||||||
176 -> {177};
|
176 -> {177};
|
||||||
177 -> {178};
|
177 -> {178};
|
||||||
@@ -498,7 +496,5 @@ digraph jumpFromRhsOfOperator_kt {
|
|||||||
182 -> {183};
|
182 -> {183};
|
||||||
183 -> {184};
|
183 -> {184};
|
||||||
184 -> {185};
|
184 -> {185};
|
||||||
185 -> {186};
|
|
||||||
186 -> {187};
|
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|||||||
+56
-136
@@ -153,7 +153,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
protected abstract val logicSystem: LogicSystem<FLOW>
|
protected abstract val logicSystem: LogicSystem<FLOW>
|
||||||
|
|
||||||
private val graphBuilder get() = context.graphBuilder
|
private val graphBuilder get() = context.graphBuilder
|
||||||
protected val variableStorage get() = context.variableStorage
|
private val variableStorage get() = context.variableStorage
|
||||||
|
|
||||||
private var contractDescriptionVisitingMode = false
|
private var contractDescriptionVisitingMode = false
|
||||||
|
|
||||||
@@ -423,30 +423,21 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
|
|
||||||
when (val operation = typeOperatorCall.operation) {
|
when (val operation = typeOperatorCall.operation) {
|
||||||
FirOperation.IS, FirOperation.NOT_IS -> {
|
FirOperation.IS, FirOperation.NOT_IS -> {
|
||||||
val expressionVariable = variableStorage.createSyntheticVariable(typeOperatorCall)
|
val isType = operation == FirOperation.IS
|
||||||
val isNotNullCheck = !type.canBeNull
|
when (type) {
|
||||||
val isRegularIs = operation == FirOperation.IS
|
// x is Nothing? <=> x == null
|
||||||
if (operandVariable.isReal()) {
|
nullableNothing -> processEqNull(node, typeOperatorCall.argument, isType)
|
||||||
val hasTypeInfo = operandVariable typeEq type
|
// x is Any <=> x != null
|
||||||
val hasNotTypeInfo = operandVariable typeNotEq type
|
any -> processEqNull(node, typeOperatorCall.argument, !isType)
|
||||||
|
else -> {
|
||||||
fun chooseInfo(trueBranch: Boolean) =
|
val expressionVariable = variableStorage.createSyntheticVariable(typeOperatorCall)
|
||||||
if ((typeOperatorCall.operation == FirOperation.IS) == trueBranch) hasTypeInfo else hasNotTypeInfo
|
if (operandVariable.isReal()) {
|
||||||
|
flow.addImplication((expressionVariable eq isType) implies (operandVariable typeEq type))
|
||||||
flow.addImplication((expressionVariable eq true) implies chooseInfo(true))
|
flow.addImplication((expressionVariable notEq isType) implies (operandVariable typeNotEq type))
|
||||||
flow.addImplication((expressionVariable eq false) implies chooseInfo(false))
|
}
|
||||||
|
if (!type.canBeNull) {
|
||||||
if (operation == FirOperation.NOT_IS && type == nullableNothing) {
|
flow.addImplication((expressionVariable eq isType) implies (operandVariable notEq null))
|
||||||
flow.addTypeStatement(operandVariable typeEq any)
|
}
|
||||||
}
|
|
||||||
if (isNotNullCheck) {
|
|
||||||
flow.addImplication((expressionVariable eq isRegularIs) implies (operandVariable typeEq any))
|
|
||||||
flow.addImplication((expressionVariable eq isRegularIs) implies (operandVariable notEq null))
|
|
||||||
}
|
|
||||||
|
|
||||||
} else {
|
|
||||||
if (isNotNullCheck) {
|
|
||||||
flow.addImplication((expressionVariable eq isRegularIs) implies (operandVariable notEq null))
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -511,8 +502,8 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
|
|
||||||
when {
|
when {
|
||||||
leftConst != null && rightConst != null -> return
|
leftConst != null && rightConst != null -> return
|
||||||
leftIsNull -> processEqNull(node, rightOperand, operation)
|
leftIsNull -> processEqNull(node, rightOperand, operation.isEq())
|
||||||
rightIsNull -> processEqNull(node, leftOperand, operation)
|
rightIsNull -> processEqNull(node, leftOperand, operation.isEq())
|
||||||
leftConst != null -> processEqWithConst(node, rightOperand, leftConst, operation)
|
leftConst != null -> processEqWithConst(node, rightOperand, leftConst, operation)
|
||||||
rightConst != null -> processEqWithConst(node, leftOperand, rightConst, operation)
|
rightConst != null -> processEqWithConst(node, leftOperand, rightConst, operation)
|
||||||
else -> processEq(node, leftOperand, rightOperand, operation)
|
else -> processEq(node, leftOperand, rightOperand, operation)
|
||||||
@@ -581,121 +572,43 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun processEq(
|
private fun processEqNull(node: CFGNode<*>, operand: FirExpression, isEq: Boolean) {
|
||||||
node: EqualityOperatorCallNode, leftOperand: FirExpression, rightOperand: FirExpression, operation: FirOperation
|
|
||||||
) {
|
|
||||||
val leftIsNullable = leftOperand.coneType.isMarkedNullable
|
|
||||||
val rightIsNullable = rightOperand.coneType.isMarkedNullable
|
|
||||||
|
|
||||||
if (leftIsNullable || rightIsNullable) {
|
|
||||||
if (leftIsNullable && rightIsNullable) return
|
|
||||||
processEqNull(
|
|
||||||
node,
|
|
||||||
if (leftIsNullable) leftOperand else rightOperand,
|
|
||||||
operation.invert(),
|
|
||||||
checkAddImplicationForStatement = true
|
|
||||||
)
|
|
||||||
}
|
|
||||||
|
|
||||||
processPossibleIdentity(node, leftOperand, rightOperand, operation)
|
|
||||||
}
|
|
||||||
|
|
||||||
/*
|
|
||||||
* Process x == null in general: add implications for both cases.
|
|
||||||
* E.g., say d1 is an eq operator call node, d2 represents `x`, the variable inside the operator call. So, d1: x == null
|
|
||||||
* This util adds: "d1 == True -> d2 == null" and "d1 == False -> d2 != null"
|
|
||||||
* so that both branches after the operator call can infer the type of x.
|
|
||||||
*
|
|
||||||
* However, users can specify what conditions are of interest.
|
|
||||||
* E.g., say left == right _and_ right != null, then we can conclude left != null.
|
|
||||||
* In this example, say d1 is an eq operator call (left == right), and d2 is left.
|
|
||||||
* Unlike general cases, we want to add: "d1 == True -> d2 != null", and nothing more because the counter part,
|
|
||||||
* "d1 == False -> d2 == null" doesn't hold. That is, left != right and right != null don't mean left == null. It just means, left is
|
|
||||||
* something different from right, including null. By filtering "d1 == True" condition only, all the remaining logic can be shared.
|
|
||||||
*/
|
|
||||||
private fun processEqNull(
|
|
||||||
node: EqualityOperatorCallNode,
|
|
||||||
operand: FirExpression,
|
|
||||||
operation: FirOperation,
|
|
||||||
checkAddImplicationForStatement: Boolean = false
|
|
||||||
) {
|
|
||||||
val flow = node.flow
|
val flow = node.flow
|
||||||
val expressionVariable = variableStorage.createSyntheticVariable(node.fir)
|
val expressionVariable = variableStorage.createSyntheticVariable(node.fir)
|
||||||
val operandVariable = variableStorage.getOrCreateVariable(node.previousFlow, operand)
|
val operandVariable = variableStorage.getOrCreateVariable(node.previousFlow, operand)
|
||||||
|
flow.addImplication((expressionVariable eq isEq) implies (operandVariable eq null))
|
||||||
val isEq = operation.isEq()
|
flow.addImplication((expressionVariable notEq isEq) implies (operandVariable notEq null))
|
||||||
|
|
||||||
val predicate = when (isEq) {
|
|
||||||
true -> operandVariable eq null
|
|
||||||
false -> operandVariable notEq null
|
|
||||||
}
|
|
||||||
|
|
||||||
// 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
|
|
||||||
val operationStatementOp = operationStatement.operation
|
|
||||||
return !isEq && operationStatementOp == Operation.EqTrue || isEq && operationStatementOp == Operation.EqFalse
|
|
||||||
}
|
|
||||||
|
|
||||||
// !checkAddImplicationForStatement || !isEq
|
|
||||||
if (shouldAddImplicationForStatement(expressionVariable eq true)) {
|
|
||||||
logicSystem.approveOperationStatement(flow, predicate).forEach { effect ->
|
|
||||||
flow.addImplication((expressionVariable eq true) implies effect)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// !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))
|
|
||||||
}
|
|
||||||
if (expressionVariableIsNotEq) {
|
|
||||||
flow.addImplication((expressionVariable notEq isEq) implies (operandVariable notEq null))
|
|
||||||
}
|
|
||||||
|
|
||||||
if (operandVariable.isReal()) {
|
|
||||||
if (expressionVariableIsEq) {
|
|
||||||
flow.addImplication((expressionVariable eq isEq) implies (operandVariable typeNotEq any))
|
|
||||||
}
|
|
||||||
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))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
node.flow = flow
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun processPossibleIdentity(
|
private fun processEq(
|
||||||
node: EqualityOperatorCallNode,
|
node: EqualityOperatorCallNode,
|
||||||
leftOperand: FirExpression,
|
leftOperand: FirExpression,
|
||||||
rightOperand: FirExpression,
|
rightOperand: FirExpression,
|
||||||
operation: FirOperation,
|
operation: FirOperation,
|
||||||
) {
|
) {
|
||||||
val flow = node.flow
|
val isEq = operation.isEq()
|
||||||
val expressionVariable = variableStorage.getOrCreateVariable(node.previousFlow, node.fir)
|
|
||||||
val leftOperandVariable = variableStorage.getOrCreateVariable(node.previousFlow, leftOperand)
|
|
||||||
val rightOperandVariable = variableStorage.getOrCreateVariable(node.previousFlow, rightOperand)
|
|
||||||
val leftOperandType = leftOperand.coneType
|
val leftOperandType = leftOperand.coneType
|
||||||
val rightOperandType = rightOperand.coneType
|
val rightOperandType = rightOperand.coneType
|
||||||
|
val leftIsNullable = leftOperandType.isMarkedNullable
|
||||||
|
val rightIsNullable = rightOperandType.isMarkedNullable
|
||||||
|
|
||||||
|
if (leftIsNullable && rightIsNullable) {
|
||||||
|
// The logic system is not complex enough to express a second level of implications this creates:
|
||||||
|
// if either `== null` then this creates the same implications as a constant null comparison,
|
||||||
|
// otherwise the same as if the corresponding `...IsNullable` is false.
|
||||||
|
return
|
||||||
|
}
|
||||||
|
|
||||||
|
val flow = node.flow
|
||||||
|
val expressionVariable = variableStorage.createSyntheticVariable(node.fir)
|
||||||
|
val leftOperandVariable = variableStorage.getOrCreateVariable(node.previousFlow, leftOperand)
|
||||||
|
val rightOperandVariable = variableStorage.getOrCreateVariable(node.previousFlow, rightOperand)
|
||||||
|
|
||||||
|
if (leftIsNullable || rightIsNullable) {
|
||||||
|
// `a == b:Any` => `a != null`; the inverse is not true - we don't know when `a` *is* `null`
|
||||||
|
val nullableOperand = if (leftIsNullable) leftOperandVariable else rightOperandVariable
|
||||||
|
flow.addImplication((expressionVariable eq isEq) implies (nullableOperand notEq null))
|
||||||
|
}
|
||||||
|
|
||||||
if (!leftOperandVariable.isReal() && !rightOperandVariable.isReal()) return
|
if (!leftOperandVariable.isReal() && !rightOperandVariable.isReal()) return
|
||||||
|
|
||||||
@@ -703,8 +616,6 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
if (hasOverriddenEquals(leftOperandType)) return
|
if (hasOverriddenEquals(leftOperandType)) return
|
||||||
}
|
}
|
||||||
|
|
||||||
val isEq = operation.isEq()
|
|
||||||
|
|
||||||
if (leftOperandVariable.isReal()) {
|
if (leftOperandVariable.isReal()) {
|
||||||
flow.addImplication((expressionVariable eq isEq) implies (leftOperandVariable typeEq rightOperandType))
|
flow.addImplication((expressionVariable eq isEq) implies (leftOperandVariable typeEq rightOperandType))
|
||||||
flow.addImplication((expressionVariable notEq isEq) implies (leftOperandVariable typeNotEq rightOperandType))
|
flow.addImplication((expressionVariable notEq isEq) implies (leftOperandVariable typeNotEq rightOperandType))
|
||||||
@@ -714,8 +625,6 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
flow.addImplication((expressionVariable eq isEq) implies (rightOperandVariable typeEq leftOperandType))
|
flow.addImplication((expressionVariable eq isEq) implies (rightOperandVariable typeEq leftOperandType))
|
||||||
flow.addImplication((expressionVariable notEq isEq) implies (rightOperandVariable typeNotEq leftOperandType))
|
flow.addImplication((expressionVariable notEq isEq) implies (rightOperandVariable typeNotEq leftOperandType))
|
||||||
}
|
}
|
||||||
|
|
||||||
node.flow = flow
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private fun hasOverriddenEquals(type: ConeKotlinType): Boolean {
|
private fun hasOverriddenEquals(type: ConeKotlinType): Boolean {
|
||||||
@@ -1051,9 +960,9 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
|
|||||||
is RealVariable -> variable.explicitReceiverVariable ?: return
|
is RealVariable -> variable.explicitReceiverVariable ?: return
|
||||||
is SyntheticVariable -> variableStorage.getOrCreateVariable(flow, safeCall.receiver)
|
is SyntheticVariable -> variableStorage.getOrCreateVariable(flow, safeCall.receiver)
|
||||||
}
|
}
|
||||||
logicSystem.addImplication(flow, (variable notEq null) implies (receiverVariable notEq null))
|
flow.addImplication((variable notEq null) implies (receiverVariable notEq null))
|
||||||
if (receiverVariable.isReal()) {
|
if (receiverVariable.isReal()) {
|
||||||
logicSystem.addImplication(flow, (variable notEq null) implies (receiverVariable typeEq any))
|
flow.addImplication((variable notEq null) implies (receiverVariable typeEq any))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1575,6 +1484,17 @@ 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 andTypeNotEq any
|
||||||
|
Operation.NotEqNull -> variable typeEq any andTypeNotEq nullableNothing
|
||||||
|
else -> null
|
||||||
|
}?.let { logicSystem.addImplication(this, statement.condition implies it) }
|
||||||
|
}
|
||||||
|
}
|
||||||
logicSystem.addImplication(this, statement)
|
logicSystem.addImplication(this, statement)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -72,16 +72,6 @@ abstract class LogicSystem<FLOW : Flow>(protected val context: ConeInferenceCont
|
|||||||
statements: Collection<Implication>,
|
statements: Collection<Implication>,
|
||||||
)
|
)
|
||||||
|
|
||||||
/**
|
|
||||||
* Recursively collects all TypeStatements approved by [approvedStatement] and all predicates
|
|
||||||
* that has been implied by it
|
|
||||||
* TODO: or not recursively?
|
|
||||||
*/
|
|
||||||
fun approveOperationStatement(flow: FLOW, approvedStatement: OperationStatement): Collection<TypeStatement> {
|
|
||||||
val statements = getImplicationsWithVariable(flow, approvedStatement.variable)
|
|
||||||
return approveOperationStatement(flow, approvedStatement, statements).values
|
|
||||||
}
|
|
||||||
|
|
||||||
fun orForTypeStatements(left: TypeStatements, right: TypeStatements): MutableTypeStatements {
|
fun orForTypeStatements(left: TypeStatements, right: TypeStatements): MutableTypeStatements {
|
||||||
if (left.isEmpty() || right.isEmpty()) return mutableMapOf()
|
if (left.isEmpty() || right.isEmpty()) return mutableMapOf()
|
||||||
val map = mutableMapOf<RealVariable, MutableTypeStatement>()
|
val map = mutableMapOf<RealVariable, MutableTypeStatement>()
|
||||||
|
|||||||
@@ -60,18 +60,25 @@ infix fun DataFlowVariable.notEq(constant: Boolean?): OperationStatement {
|
|||||||
|
|
||||||
infix fun OperationStatement.implies(effect: Statement<*>): Implication = Implication(this, effect)
|
infix fun OperationStatement.implies(effect: Statement<*>): Implication = Implication(this, effect)
|
||||||
|
|
||||||
infix fun RealVariable.typeEq(type: ConeKotlinType): TypeStatement =
|
infix fun RealVariable.typeEq(type: ConeKotlinType): MutableTypeStatement =
|
||||||
if (type !is ConeErrorType) {
|
MutableTypeStatement(this) andTypeEq type
|
||||||
MutableTypeStatement(this, linkedSetOf<ConeKotlinType>().apply { this += type }, HashSet())
|
|
||||||
} else {
|
infix fun RealVariable.typeNotEq(type: ConeKotlinType): MutableTypeStatement =
|
||||||
MutableTypeStatement(this)
|
MutableTypeStatement(this) andTypeNotEq type
|
||||||
|
|
||||||
|
infix fun MutableTypeStatement.andTypeEq(type: ConeKotlinType): MutableTypeStatement =
|
||||||
|
this.apply {
|
||||||
|
if (type !is ConeErrorType) {
|
||||||
|
exactType += type
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
infix fun RealVariable.typeNotEq(type: ConeKotlinType): TypeStatement =
|
infix fun MutableTypeStatement.andTypeNotEq(type: ConeKotlinType): MutableTypeStatement =
|
||||||
if (type !is ConeErrorType) {
|
this.apply {
|
||||||
MutableTypeStatement(this, linkedSetOf(), LinkedHashSet<ConeKotlinType>().apply { this += type })
|
require(exactNotType.isEmpty()) { "statement $this already has a negation; use `logicSystem.and`" }
|
||||||
} else {
|
if (type !is ConeErrorType) {
|
||||||
MutableTypeStatement(this)
|
exactNotType += type
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// --------------------------------------- Utils ---------------------------------------
|
// --------------------------------------- Utils ---------------------------------------
|
||||||
|
|||||||
@@ -39,12 +39,12 @@ fun bar(o: Any) {
|
|||||||
|
|
||||||
fun baz(o: Boolean?) {
|
fun baz(o: Boolean?) {
|
||||||
if (o ?: false) {
|
if (o ?: false) {
|
||||||
o<!UNSAFE_CALL!>.<!>hashCode()
|
o.hashCode()
|
||||||
}
|
}
|
||||||
if (o ?: true) {
|
if (o ?: true) {
|
||||||
|
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
o<!UNSAFE_CALL!>.<!>hashCode()
|
o.hashCode()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
+1
-1
@@ -22,7 +22,7 @@ fun foo() : Int {
|
|||||||
<!USELESS_IS_CHECK!>!is Int<!> -> 1
|
<!USELESS_IS_CHECK!>!is Int<!> -> 1
|
||||||
<!USELESS_IS_CHECK!>is Any?<!> -> 1
|
<!USELESS_IS_CHECK!>is Any?<!> -> 1
|
||||||
<!USELESS_IS_CHECK!>is Any<!> -> 1
|
<!USELESS_IS_CHECK!>is Any<!> -> 1
|
||||||
<!INCOMPATIBLE_TYPES!>s<!> -> 1
|
s -> 1
|
||||||
1 -> 1
|
1 -> 1
|
||||||
1 <!OVERLOAD_RESOLUTION_AMBIGUITY!>+<!> <!UNRESOLVED_REFERENCE!>a<!> -> 1
|
1 <!OVERLOAD_RESOLUTION_AMBIGUITY!>+<!> <!UNRESOLVED_REFERENCE!>a<!> -> 1
|
||||||
in 1..<!UNRESOLVED_REFERENCE!>a<!> -> 1
|
in 1..<!UNRESOLVED_REFERENCE!>a<!> -> 1
|
||||||
|
|||||||
+1
-1
@@ -70,7 +70,7 @@ fun case_8(value_1: SealedClassMixed?): String = <!NO_ELSE_IN_WHEN!>when<!>(valu
|
|||||||
*/
|
*/
|
||||||
fun case_9(value_1: Any?): String = <!NO_ELSE_IN_WHEN!>when<!> (value_1) {
|
fun case_9(value_1: Any?): String = <!NO_ELSE_IN_WHEN!>when<!> (value_1) {
|
||||||
is Any -> ""
|
is Any -> ""
|
||||||
null -> ""
|
<!SENSELESS_COMPARISON!>null<!> -> ""
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
|
|||||||
@@ -36,8 +36,8 @@ fun case_4(x: Any) {
|
|||||||
// TESTCASE NUMBER: 5
|
// TESTCASE NUMBER: 5
|
||||||
fun case_5(x: Any?) {
|
fun case_5(x: Any?) {
|
||||||
if (!(x !is Nothing?)) {
|
if (!(x !is Nothing?)) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!><!UNNECESSARY_SAFE_CALL!>?.<!><!UNRESOLVED_REFERENCE!>inv<!>()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.<!UNRESOLVED_REFERENCE!>inv<!>()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -68,8 +68,8 @@ fun case_8(x: Any?) {
|
|||||||
// TESTCASE NUMBER: 9
|
// TESTCASE NUMBER: 9
|
||||||
fun case_9(x: Any?) {
|
fun case_9(x: Any?) {
|
||||||
if (!!(x !is Nothing?)) else {
|
if (!!(x !is Nothing?)) else {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!><!UNNECESSARY_SAFE_CALL!>?.<!><!UNRESOLVED_REFERENCE!>inv<!>()
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.<!UNRESOLVED_REFERENCE!>inv<!>()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -22,8 +22,8 @@ inline fun <reified T> case_2(x: Any?) {
|
|||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
is T -> {
|
is T -> {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & T")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing? & T")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & T")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing? & T")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
||||||
}
|
}
|
||||||
else -> return
|
else -> return
|
||||||
}
|
}
|
||||||
@@ -80,8 +80,8 @@ inline fun <reified T> case_7(x: Any?) {
|
|||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
} else if (x is T) {
|
} else if (x is T) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & T")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing? & T")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & T")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing? & T")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
||||||
} else return
|
} else return
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
||||||
|
|||||||
@@ -102,7 +102,7 @@ fun case_11(x: TypealiasString, y: TypealiasString) {
|
|||||||
if (<!SENSELESS_COMPARISON!>y == null<!>) {
|
if (<!SENSELESS_COMPARISON!>y == null<!>) {
|
||||||
if (<!SENSELESS_COMPARISON!>stringProperty != null<!>) {
|
if (<!SENSELESS_COMPARISON!>stringProperty != null<!>) {
|
||||||
if (false || false || false || <!SENSELESS_COMPARISON!>z == null<!> || false) {
|
if (false || false || false || <!SENSELESS_COMPARISON!>z == null<!> || false) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasString & kotlin.Nothing")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasString")!>x<!>
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -134,8 +134,8 @@ fun case_14(x: Any?) {
|
|||||||
if (x == null) {
|
if (x == null) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.equals(10)
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Nothing")!>x!!<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any")!>x!!<!>.equals(10)
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -148,8 +148,8 @@ fun case_15(x: Any?) {
|
|||||||
if (x !== null) else {
|
if (x !== null) else {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing?")!>x<!>?.equals(10)
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Nothing")!>x!!<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any")!>x!!<!>.equals(10)
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Nothing")!>x<!>.equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -840,8 +840,8 @@ fun case_46(x: TypealiasNullableString<!REDUNDANT_NULLABLE!>?<!>, y: TypealiasNu
|
|||||||
if (y === nullableNothingProperty) {
|
if (y === nullableNothingProperty) {
|
||||||
if (z != nullableStringProperty) {
|
if (z != nullableStringProperty) {
|
||||||
if (z === t || <!SENSELESS_COMPARISON!>t == nullableNothingProperty<!>) {
|
if (z === t || <!SENSELESS_COMPARISON!>t == nullableNothingProperty<!>) {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasNullableString? & kotlin.Nothing?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasNullableString?")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasNullableString? & kotlin.Nothing?")!>x<!>.hashCode()
|
<!DEBUG_INFO_EXPRESSION_TYPE("TypealiasNullableString?")!>x<!>.hashCode()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -20,8 +20,8 @@ fun case_1(x: Any?) {
|
|||||||
*/
|
*/
|
||||||
fun case_2(x: Pair<*, *>?) {
|
fun case_2(x: Pair<*, *>?) {
|
||||||
if (x is Nothing?) return
|
if (x is Nothing?) return
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -31,8 +31,8 @@ fun case_2(x: Pair<*, *>?) {
|
|||||||
*/
|
*/
|
||||||
fun case_3(x: Any?) {
|
fun case_3(x: Any?) {
|
||||||
if (x is Nothing?) throw Exception()
|
if (x is Nothing?) throw Exception()
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -44,12 +44,12 @@ fun case_4(x: Pair<*, *>?) {
|
|||||||
when (x) {
|
when (x) {
|
||||||
is Nothing? -> return
|
is Nothing? -> return
|
||||||
else -> {
|
else -> {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Pair<*, *>? & kotlin.Pair<*, *>")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
|
|
||||||
/*
|
/*
|
||||||
@@ -78,10 +78,10 @@ fun case_6(x: Any?) {
|
|||||||
when (x) {
|
when (x) {
|
||||||
is Nothing? -> return
|
is Nothing? -> return
|
||||||
<!USELESS_IS_CHECK!>is Any?<!> -> {
|
<!USELESS_IS_CHECK!>is Any?<!> -> {
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!>
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!><!UNSAFE_CALL!>.<!>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.Any")!>x<!>
|
||||||
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any?")!>x<!><!UNSAFE_CALL!>.<!>equals(10)
|
<!DEBUG_INFO_EXPRESSION_TYPE("kotlin.Any? & kotlin.Any")!>x<!>.equals(10)
|
||||||
}
|
}
|
||||||
|
|||||||
Reference in New Issue
Block a user