[FIR] Implement Data Flow Analysis

2019-08-22 15:27:51 +03:00
parent 216b9ad933
commit 2e501e0f97
2 changed files with 423 additions and 45 deletions
@@ -5,157 +5,386 @@

 package org.jetbrains.kotlin.fir.resolve.dfa

+import org.jetbrains.kotlin.fir.FirElement
+import org.jetbrains.kotlin.fir.FirResolvedCallableReference
 import org.jetbrains.kotlin.fir.declarations.FirAnonymousInitializer
 import org.jetbrains.kotlin.fir.declarations.FirFunction
 import org.jetbrains.kotlin.fir.declarations.FirProperty
 import org.jetbrains.kotlin.fir.expressions.*
 import org.jetbrains.kotlin.fir.resolve.BodyResolveComponents
-import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraph
-import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraphBuilder
+import org.jetbrains.kotlin.fir.resolve.dfa.ConditionValue.*
+import org.jetbrains.kotlin.fir.resolve.dfa.cfg.*
 import org.jetbrains.kotlin.fir.resolve.transformers.FirBodyResolveTransformer
-import org.jetbrains.kotlin.fir.types.ConeKotlinType
+import org.jetbrains.kotlin.fir.symbols.CallableId
+import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirCallableSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirNamedFunctionSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol
+import org.jetbrains.kotlin.fir.types.*
+import org.jetbrains.kotlin.ir.expressions.IrConstKind
+import org.jetbrains.kotlin.name.FqName
+import org.jetbrains.kotlin.name.Name
+import org.jetbrains.kotlin.utils.addToStdlib.safeAs

 class FirDataFlowAnalyzerImpl(transformer: FirBodyResolveTransformer) : FirDataFlowAnalyzer(), BodyResolveComponents by transformer {
+    companion object {
+        private val KOTLIN_BOOLEAN_NOT = CallableId(FqName("kotlin"), FqName("Boolean"), Name.identifier("not"))
+    }
+
+    private val context: DataFlowInferenceContext get() = inferenceComponents.ctx as DataFlowInferenceContext
+
    private val graphBuilder = ControlFlowGraphBuilder()
+    private val logicSystem = LogicSystem(context)
+    private val variableStorage = DataFlowVariableStorage(session)
+    private val edges = mutableMapOf<CFGNode<*>, Flow>().withDefault { Flow.EMPTY }

    override fun getTypeUsingSmartcastInfo(qualifiedAccessExpression: FirQualifiedAccessExpression): ConeKotlinType? {
-        return null
+        val symbol: FirBasedSymbol<*> = qualifiedAccessExpression.resolvedSymbol ?: return null
+        val variable = variableStorage[symbol] ?: return null
+        val smartCastTypes = graphBuilder.lastNode.flow.approvedFacts(variable)?.exactType ?: return null
+        val smartCastType = context.myIntersectTypes(smartCastTypes.toList()) ?: return null
+        val originalType = qualifiedAccessExpression.typeRef.coneTypeSafe<ConeKotlinType>() ?: return null
+        return ConeTypeIntersector.intersectTypesFromSmartcasts(context, originalType, smartCastType)
    }

    // ----------------------------------- Named function -----------------------------------

    override fun enterFunction(function: FirFunction<*>) {
-        graphBuilder.enterFunction(function)
+        graphBuilder.enterFunction(function).passFlow()
+
+        for (valueParameter in function.valueParameters) {
+            getRealVariable(valueParameter.symbol)
+        }
    }

    override fun exitFunction(function: FirFunction<*>): ControlFlowGraph {
-        return graphBuilder.exitFunction(function)
+        val (node, graph) = graphBuilder.exitFunction(function)
+        node.passFlow()
+        for (valueParameter in function.valueParameters) {
+            variableStorage.removeRealVariable(valueParameter.symbol)
+        }
+        if (graphBuilder.isTopLevel()) {
+            edges.clear()
+            variableStorage.reset()
+        }
+        return graph
    }

    // ----------------------------------- Property -----------------------------------

    override fun enterProperty(property: FirProperty) {
-        graphBuilder.enterProperty(property)
+        graphBuilder.enterProperty(property).passFlow()
    }

    override fun exitProperty(property: FirProperty): ControlFlowGraph {
-        val (_, graph) = graphBuilder.exitProperty(property)
+        val (node, graph) = graphBuilder.exitProperty(property)
+        node.passFlow()
        return graph
    }

    // ----------------------------------- Block -----------------------------------

    override fun enterBlock(block: FirBlock) {
-        graphBuilder.enterBlock(block)
+        val node = graphBuilder.enterBlock(block).passFlow(false)
+
+        val previousNode = node.usefulPreviousNodes.singleOrNull() as? WhenBranchConditionExitNode
+        if (previousNode != null) {
+            node.flow = logicSystem.approveFactsInsideFlow(previousNode.trueCondition, node.flow)
+        }
+        node.flow.freeze()
    }

    override fun exitBlock(block: FirBlock) {
-        graphBuilder.exitBlock(block)
+        graphBuilder.exitBlock(block).passFlow()
    }

    // ----------------------------------- Operator call -----------------------------------

    override fun exitTypeOperatorCall(typeOperatorCall: FirTypeOperatorCall) {
-        graphBuilder.exitTypeOperatorCall(typeOperatorCall)
+        val node = graphBuilder.exitTypeOperatorCall(typeOperatorCall).passFlow(false)
+        try {
+            if (typeOperatorCall.operation !in FirOperation.TYPES) return
+            val symbol: FirCallableSymbol<*> = typeOperatorCall.argument.toResolvedCallableSymbol() as? FirCallableSymbol<*> ?: return
+            val type = typeOperatorCall.conversionTypeRef.coneTypeSafe<ConeKotlinType>() ?: return
+            val varVariable = getRealVariable(symbol)
+
+            var flow = node.flow
+            when (typeOperatorCall.operation) {
+                FirOperation.IS, FirOperation.NOT_IS -> {
+                    val expressionVariable = getSyntheticVariable(typeOperatorCall)
+
+                    val trueInfo = FirDataFlowInfo(setOf(type), emptySet())
+                    val falseInfo = FirDataFlowInfo(emptySet(), setOf(type))
+
+                    fun chooseInfo(trueBranch: Boolean) = if ((typeOperatorCall.operation == FirOperation.IS) == trueBranch) trueInfo else falseInfo
+
+                    flow = flow.addNotApprovedFact(
+                        expressionVariable,
+                        UnapprovedFirDataFlowInfo(
+                            eq(True), varVariable, chooseInfo(true)
+                        )
+                    )
+
+                    flow = flow.addNotApprovedFact(
+                        expressionVariable,
+                        UnapprovedFirDataFlowInfo(
+                            eq(False), varVariable, chooseInfo(false)
+                        )
+                    )
+                }
+
+                FirOperation.AS -> {
+                    flow = flow.addApprovedFact(varVariable, FirDataFlowInfo(setOf(type), emptySet()))
+                }
+
+                FirOperation.SAFE_AS -> {
+                    val expressionVariable = getSyntheticVariable(typeOperatorCall)
+                    flow = flow.addNotApprovedFact(
+                        expressionVariable,
+                        UnapprovedFirDataFlowInfo(
+                            notEq(Null), varVariable, FirDataFlowInfo(setOf(type), emptySet())
+                        )
+                    ).addNotApprovedFact(
+                        expressionVariable,
+                        UnapprovedFirDataFlowInfo(
+                            eq(Null), varVariable, FirDataFlowInfo(emptySet(), setOf(type))
+                        )
+                    )
+                }
+
+                else -> throw IllegalStateException()
+            }
+
+            node.flow = flow
+        } finally {
+            node.flow.freeze()
+        }
    }

    override fun exitOperatorCall(operatorCall: FirOperatorCall) {
-        graphBuilder.exitOperatorCall(operatorCall)
+        val node = graphBuilder.exitOperatorCall(operatorCall).passFlow(false)
+        try {
+            when (val operation = operatorCall.operation) {
+                FirOperation.EQ, FirOperation.NOT_EQ, FirOperation.IDENTITY, FirOperation.NOT_IDENTITY -> {
+                    val leftOperand = operatorCall.arguments[0]
+                    val rightOperand = operatorCall.arguments[1]
+
+                    val leftConst = leftOperand as? FirConstExpression<*>
+                    val rightConst = rightOperand as? FirConstExpression<*>
+
+                    when {
+                        leftConst?.kind == IrConstKind.Null -> processEqNull(node, rightOperand, operation)
+                        rightConst?.kind == IrConstKind.Null -> processEqNull(node, leftOperand, operation)
+                        operation != FirOperation.EQ && operation != FirOperation.IDENTITY -> return
+                        leftConst != null -> processEqWithConst(node, rightOperand)
+                        rightConst != null -> processEqWithConst(node, leftOperand)
+                        else -> processEq(node, leftOperand, rightOperand, operation)
+                    }
+                }
+            }
+        } finally {
+            node.flow.freeze()
+        }
+    }
+
+    private fun processEqWithConst(node: OperatorCallNode, operand: FirExpression) {
+        val operandVariables = getRealVariablesForSafeCallChain(operand).takeIf { it.isNotEmpty() } ?: return
+        val expressionVariable = getVariable(node.fir)
+        var flow = node.flow
+        operandVariables.forEach { operandVariable ->
+            flow = flow.addNotApprovedFact(
+                expressionVariable, UnapprovedFirDataFlowInfo(
+                    eq(True),
+                    operandVariable,
+                    FirDataFlowInfo(setOf(session.builtinTypes.anyType.coneTypeUnsafe()), emptySet())
+                )
+            )
+        }
+        node.flow = flow
+    }
+
+    private fun processEq(node: OperatorCallNode, leftOperand: FirExpression, rightOperand: FirExpression, operation: FirOperation) {
+        val leftType = leftOperand.typeRef.coneTypeSafe<ConeKotlinType>() ?: return
+        val rightType = rightOperand.typeRef.coneTypeSafe<ConeKotlinType>() ?: return
+        when {
+            leftType.isMarkedNullable && rightType.isMarkedNullable -> return
+            leftType.isMarkedNullable -> processEqWithConst(node, leftOperand)
+            rightType.isMarkedNullable -> processEqWithConst(node, rightOperand)
+        }
+        // TODO: process EQUALITY
+    }
+
+    private fun processEqNull(node: OperatorCallNode, operand: FirExpression, operation: FirOperation) {
+        var flow = node.flow
+        val expressionVariable = getVariable(node.fir)
+
+        variableStorage[operand]?.let { operandVariable ->
+            val operator = when (operation) {
+                FirOperation.EQ, FirOperation.IDENTITY -> ConditionOperator.Eq
+                FirOperation.NOT_EQ, FirOperation.NOT_IDENTITY -> ConditionOperator.NotEq
+                else -> throw IllegalArgumentException()
+            }
+            val facts = logicSystem.approveFact(Condition(operandVariable, operator, Null), flow)
+            facts.forEach { (variable, info) ->
+                flow = flow.addNotApprovedFact(
+                    expressionVariable,
+                    UnapprovedFirDataFlowInfo(
+                        eq(True), variable, info
+                    )
+                ).addNotApprovedFact(
+                    expressionVariable,
+                    UnapprovedFirDataFlowInfo(
+                        eq(False), variable, info.invert()
+                    )
+                )
+            }
+            node.flow = flow
+            return
+        }
+
+        val operandVariables = getRealVariablesForSafeCallChain(operand).takeIf { it.isNotEmpty() } ?: return
+
+        val conditionValue = when (operation) {
+            FirOperation.EQ, FirOperation.IDENTITY -> False
+            FirOperation.NOT_EQ, FirOperation.NOT_IDENTITY -> True
+            else -> throw IllegalArgumentException()
+        }
+
+        operandVariables.forEach { operandVariable ->
+            flow = flow.addNotApprovedFact(
+                expressionVariable, UnapprovedFirDataFlowInfo(
+                    eq(conditionValue),
+                    operandVariable,
+                    FirDataFlowInfo(setOf(session.builtinTypes.anyType.coneTypeUnsafe()), emptySet())
+                )
+            ).addNotApprovedFact(
+                expressionVariable, UnapprovedFirDataFlowInfo(
+                    eq(conditionValue.invert()!!),
+                    operandVariable,
+                    FirDataFlowInfo(setOf(session.builtinTypes.nullableNothingType.coneTypeUnsafe()), emptySet())
+                )
+            )
+
+        }
+        node.flow = flow
    }

    // ----------------------------------- Jump -----------------------------------

    override fun exitJump(jump: FirJump<*>) {
-        graphBuilder.exitJump(jump)
+        graphBuilder.exitJump(jump).passFlow()
    }

    // ----------------------------------- When -----------------------------------

    override fun enterWhenExpression(whenExpression: FirWhenExpression) {
-        graphBuilder.enterWhenExpression(whenExpression)
+        graphBuilder.enterWhenExpression(whenExpression).passFlow()
    }

    override fun enterWhenBranchCondition(whenBranch: FirWhenBranch) {
-        graphBuilder.enterWhenBranchCondition(whenBranch)
+        val node = graphBuilder.enterWhenBranchCondition(whenBranch).passFlow(false)
+        val previousNode = node.previousNodes.single()
+        if (previousNode is WhenBranchConditionExitNode) {
+            node.flow = logicSystem.approveFactsInsideFlow(previousNode.falseCondition, node.flow)
+        }
+        node.flow.freeze()
    }

    override fun exitWhenBranchCondition(whenBranch: FirWhenBranch) {
-        graphBuilder.exitWhenBranchCondition(whenBranch)
+        val node = graphBuilder.exitWhenBranchCondition(whenBranch).passFlow()
+
+        val conditionVariable = getVariable(whenBranch.condition)
+        node.trueCondition = conditionVariable eq True
+        node.falseCondition = conditionVariable eq False
    }

    override fun exitWhenBranchResult(whenBranch: FirWhenBranch) {
-        graphBuilder.exitWhenBranchResult(whenBranch)
+        val node = graphBuilder.exitWhenBranchResult(whenBranch).passFlow(false)
+        val conditionVariable = getVariable(whenBranch.condition)
+        node.flow = node.flow.removeSyntheticVariable(conditionVariable)
    }

    override fun exitWhenExpression(whenExpression: FirWhenExpression) {
-        graphBuilder.exitWhenExpression(whenExpression)
+        val node = graphBuilder.exitWhenExpression(whenExpression)
+        var flow = logicSystem.or(node.usefulPreviousNodes.map { it.flow })
+        val subjectSymbol = whenExpression.subjectVariable?.symbol
+        if (subjectSymbol != null) {
+            variableStorage[subjectSymbol]?.let { flow = flow.removeVariable(it) }
+        }
+        node.flow = flow
    }

    // ----------------------------------- While Loop -----------------------------------

    override fun enterWhileLoop(loop: FirLoop) {
-        graphBuilder.enterWhileLoop(loop)
+        graphBuilder.enterWhileLoop(loop).passFlow()
    }

    override fun exitWhileLoopCondition(loop: FirLoop) {
-        graphBuilder.exitWhileLoopCondition(loop)
+        graphBuilder.exitWhileLoopCondition(loop).passFlow()
    }

    override fun exitWhileLoop(loop: FirLoop) {
-        graphBuilder.exitWhileLoop(loop)
+        graphBuilder.exitWhileLoop(loop).also { (blockExitNode, exitNode) ->
+            blockExitNode.passFlow()
+            exitNode.passFlow()
+        }
    }

    // ----------------------------------- Do while Loop -----------------------------------

    override fun enterDoWhileLoop(loop: FirLoop) {
-        graphBuilder.enterDoWhileLoop(loop)
+        graphBuilder.enterDoWhileLoop(loop).passFlow()
    }

    override fun enterDoWhileLoopCondition(loop: FirLoop) {
-        graphBuilder.enterDoWhileLoopCondition(loop)
+        val (loopBlockExitNode, loopConditionEnterNode) = graphBuilder.enterDoWhileLoopCondition(loop)
+        loopBlockExitNode.passFlow()
+        loopConditionEnterNode.passFlow()
    }

    override fun exitDoWhileLoop(loop: FirLoop) {
-        graphBuilder.exitDoWhileLoop(loop)
+        graphBuilder.exitDoWhileLoop(loop).passFlow()
    }

    // ----------------------------------- Try-catch-finally -----------------------------------

    override fun enterTryExpression(tryExpression: FirTryExpression) {
-        graphBuilder.enterTryExpression(tryExpression)
+        graphBuilder.enterTryExpression(tryExpression).passFlow()
    }

    override fun exitTryMainBlock(tryExpression: FirTryExpression) {
-        graphBuilder.exitTryMainBlock(tryExpression)
+        graphBuilder.exitTryMainBlock(tryExpression).passFlow()
    }

    override fun enterCatchClause(catch: FirCatch) {
-        graphBuilder.enterCatchClause(catch)
+        graphBuilder.enterCatchClause(catch).passFlow()
    }

    override fun exitCatchClause(catch: FirCatch) {
-        graphBuilder.exitCatchClause(catch)
+        graphBuilder.exitCatchClause(catch).passFlow()
    }

    override fun enterFinallyBlock(tryExpression: FirTryExpression) {
        // TODO
-        graphBuilder.enterFinallyBlock(tryExpression)
+        graphBuilder.enterFinallyBlock(tryExpression).passFlow()
    }

    override fun exitFinallyBlock(tryExpression: FirTryExpression) {
        // TODO
-        graphBuilder.exitFinallyBlock(tryExpression)
+        graphBuilder.exitFinallyBlock(tryExpression).passFlow()
    }

    override fun exitTryExpression(tryExpression: FirTryExpression) {
        // TODO
-        graphBuilder.exitTryExpression(tryExpression)
+        graphBuilder.exitTryExpression(tryExpression).passFlow()
    }

    // ----------------------------------- Resolvable call -----------------------------------

    override fun exitQualifiedAccessExpression(qualifiedAccessExpression: FirQualifiedAccessExpression) {
-        graphBuilder.exitQualifiedAccessExpression(qualifiedAccessExpression)
+        graphBuilder.exitQualifiedAccessExpression(qualifiedAccessExpression).passFlow()
    }

    override fun enterFunctionCall(functionCall: FirFunctionCall) {
@@ -163,29 +392,47 @@ class FirDataFlowAnalyzerImpl(transformer: FirBodyResolveTransformer) : FirDataF
    }

    override fun exitFunctionCall(functionCall: FirFunctionCall) {
-        graphBuilder.exitFunctionCall(functionCall)
+        val node = graphBuilder.exitFunctionCall(functionCall).passFlow(false)
+        if (functionCall.isBooleanNot()) {
+            exitBooleanNot(functionCall, node)
+            return
+        }
+    }
+
+    private val FirElement.resolvedSymbol: FirBasedSymbol<*>? get() = this.safeAs<FirResolvable>()?.calleeReference.safeAs<FirResolvedCallableReference>()?.coneSymbol as? FirBasedSymbol<*>
+
+    private fun FirFunctionCall.isBooleanNot(): Boolean {
+        val symbol = calleeReference.safeAs<FirResolvedCallableReference>()?.coneSymbol as? FirNamedFunctionSymbol ?: return false
+        return symbol.callableId == KOTLIN_BOOLEAN_NOT
    }

    override fun exitConstExpresion(constExpression: FirConstExpression<*>) {
-        graphBuilder.exitConstExpresion(constExpression)
+        graphBuilder.exitConstExpresion(constExpression).passFlow()
    }

    override fun exitVariableDeclaration(variable: FirVariable<*>) {
-        graphBuilder.exitVariableDeclaration(variable)
+        val node = graphBuilder.exitVariableDeclaration(variable).passFlow(false)
+        try {
+            val initializerVariable = variableStorage[variable.initializer ?: return] ?: return
+            val realVariable = getRealVariable(variable.symbol)
+            node.flow = node.flow.copyNotApprovedFacts(initializerVariable, realVariable)
+        } finally {
+            node.flow.freeze()
+        }
    }

    override fun exitVariableAssignment(assignment: FirVariableAssignment) {
-        graphBuilder.exitVariableAssignment(assignment)
+        graphBuilder.exitVariableAssignment(assignment).passFlow()
    }

    override fun exitThrowExceptionNode(throwExpression: FirThrowExpression) {
-        graphBuilder.exitThrowExceptionNode(throwExpression)
+        graphBuilder.exitThrowExceptionNode(throwExpression).passFlow()
    }

    // ----------------------------------- Boolean operators -----------------------------------

    override fun enterBinaryAnd(binaryLogicExpression: FirBinaryLogicExpression) {
-        graphBuilder.enterBinaryAnd(binaryLogicExpression)
+        graphBuilder.enterBinaryAnd(binaryLogicExpression).passFlow()
    }

    override fun exitLeftBinaryAndArgument(binaryLogicExpression: FirBinaryLogicExpression) {
@@ -193,7 +440,36 @@ class FirDataFlowAnalyzerImpl(transformer: FirBodyResolveTransformer) : FirDataF
    }

    override fun exitBinaryAnd(binaryLogicExpression: FirBinaryLogicExpression) {
-        graphBuilder.exitBinaryAnd(binaryLogicExpression)
+        val node = graphBuilder.exitBinaryAnd(binaryLogicExpression).passFlow(false)
+        val (leftVariable, rightVariable) = binaryLogicExpression.getVariables()
+
+        val flowFromLeft = node.leftOperandNode.flow
+        val flowFromRight = node.rightOperandNode.flow
+        val flow = node.flow
+
+        val andVariable = getVariable(binaryLogicExpression)
+
+        val leftIsTrue = approveFact(leftVariable, True, flowFromRight)
+        val leftIsFalse = approveFact(leftVariable, False, flowFromRight)
+        val rightIsTrue = approveFact(rightVariable, True, flowFromRight) ?: mutableMapOf()
+        val rightIsFalse = approveFact(rightVariable, False, flowFromRight)
+
+        flowFromRight.approvedFacts.forEach { (variable, info) ->
+            val actualInfo = flowFromLeft.approvedFacts[variable]?.let { info - it } ?: info
+            if (actualInfo.isNotEmpty) rightIsTrue.compute(variable) { _, existingInfo -> info + existingInfo }
+        }
+
+        logicSystem.andForVerifiedFacts(leftIsTrue, rightIsTrue)?.let {
+            for ((variable, info) in it) {
+                flow.addNotApprovedFact(andVariable, UnapprovedFirDataFlowInfo(eq(True), variable, info))
+            }
+        }
+        logicSystem.orForVerifiedFacts(leftIsFalse, rightIsFalse)?.let {
+            for ((variable, info) in it) {
+                flow.addNotApprovedFact(andVariable, UnapprovedFirDataFlowInfo(eq(False), variable, info))
+            }
+        }
+        node.flow = flow.removeSyntheticVariable(leftVariable).removeSyntheticVariable(rightVariable).also { it.freeze() }
    }

    override fun enterBinaryOr(binaryLogicExpression: FirBinaryLogicExpression) {
@@ -201,21 +477,53 @@ class FirDataFlowAnalyzerImpl(transformer: FirBodyResolveTransformer) : FirDataF
    }

    override fun exitLeftBinaryOrArgument(binaryLogicExpression: FirBinaryLogicExpression) {
-        graphBuilder.exitLeftBinaryOrArgument(binaryLogicExpression)
+        val node = graphBuilder.exitLeftBinaryOrArgument(binaryLogicExpression).passFlow(false)
+        val leftOperandVariable = getVariable(node.previousNodes.first().fir)
+        node.flow = logicSystem.approveFactsInsideFlow(leftOperandVariable eq False, node.flow).also { it.freeze() }
    }

    override fun exitBinaryOr(binaryLogicExpression: FirBinaryLogicExpression) {
-        graphBuilder.exitBinaryOr(binaryLogicExpression)
+        val node = graphBuilder.exitBinaryOr(binaryLogicExpression).passFlow(false)
+        val (leftVariable, rightVariable) = binaryLogicExpression.getVariables()
+
+        val flowFromLeft = node.leftOperandNode.flow
+        val flowFromRight = node.rightOperandNode.flow
+        val flow = node.flow
+
+        val orVariable = getVariable(binaryLogicExpression)
+
+        val leftIsTrue = approveFact(leftVariable, True, flowFromLeft)
+        val leftIsFalse = approveFact(leftVariable, False, flowFromLeft)
+        val rightIsTrue = approveFact(rightVariable, True, flowFromRight)
+        val rightIsFalse = approveFact(rightVariable, False, flowFromRight)
+
+        logicSystem.orForVerifiedFacts(leftIsTrue, rightIsTrue)?.let {
+            for ((variable, info) in it) {
+                flow.addNotApprovedFact(orVariable, UnapprovedFirDataFlowInfo(eq(True), variable, info))
+            }
+        }
+        logicSystem.andForVerifiedFacts(leftIsFalse, rightIsFalse)?.let {
+            for ((variable, info) in it) {
+                flow.addNotApprovedFact(orVariable, UnapprovedFirDataFlowInfo(eq(False), variable, info))
+            }
+        }
+        node.flow = flow.removeSyntheticVariable(leftVariable).removeSyntheticVariable(rightVariable).also { it.freeze() }
+    }
+
+    private fun exitBooleanNot(functionCall: FirFunctionCall, node: FunctionCallNode) {
+        val booleanExpressionVariable = getVariable(node.previousNodes.first().fir)
+        val variable = getVariable(functionCall)
+        node.flow = node.flow.copyNotApprovedFacts(booleanExpressionVariable, variable) { it.invert() }.also { it.freeze() }
    }

    // ----------------------------------- Annotations -----------------------------------

    override fun enterAnnotationCall(annotationCall: FirAnnotationCall) {
-        graphBuilder.enterAnnotationCall(annotationCall)
+        graphBuilder.enterAnnotationCall(annotationCall).passFlow()
    }

    override fun exitAnnotationCall(annotationCall: FirAnnotationCall) {
-        graphBuilder.exitAnnotationCall(annotationCall)
+        graphBuilder.exitAnnotationCall(annotationCall).passFlow()
    }

    // ----------------------------------- Init block -----------------------------------
@@ -225,6 +533,75 @@ class FirDataFlowAnalyzerImpl(transformer: FirBodyResolveTransformer) : FirDataF
    }

    override fun exitInitBlock(initBlock: FirAnonymousInitializer) {
-        graphBuilder.exitInitBlock(initBlock)
+        graphBuilder.exitInitBlock(initBlock).passFlow()
+    }
+
+    // -------------------------------------------------------------------------------------------------------------------------
+
+    private fun approveFact(variable: DataFlowVariable, value: ConditionValue, flow: Flow): MutableMap<DataFlowVariable, FirDataFlowInfo>? =
+        logicSystem.approveFact(variable eq value, flow)
+
+    private fun FirBinaryLogicExpression.getVariables(): Pair<DataFlowVariable, DataFlowVariable> =
+        getVariable(leftOperand) to getVariable(rightOperand)
+
+    private var CFGNode<*>.flow: Flow
+        get() = edges.getValue(this)
+        set(value) {
+            edges[this] = value
+        }
+
+    private fun <T : CFGNode<*>> T.passFlow(shouldFreeze: Boolean = true): T = this.also { node ->
+        node.flow = logicSystem.or(node.usefulPreviousNodes.map { it.flow }).also {
+            if (shouldFreeze) it.freeze()
+        }
+    }
+
+    private fun getSyntheticVariable(fir: FirElement): DataFlowVariable = variableStorage.getOrCreateNewSyntheticVariable(fir)
+    private fun getRealVariable(symbol: FirBasedSymbol<*>): DataFlowVariable = variableStorage.getOrCreateNewRealVariable(symbol)
+
+    private fun getVariable(fir: FirElement): DataFlowVariable {
+        val symbol = fir.resolvedSymbol
+        return if (symbol == null)
+            getSyntheticVariable(fir)
+        else
+            getRealVariable(symbol)
+    }
+
+    private fun getRealVariablesForSafeCallChain(call: FirExpression): Collection<DataFlowVariable> {
+        val result = mutableListOf<DataFlowVariable>()
+
+        fun collect(call: FirExpression) {
+            when (call) {
+                is FirQualifiedAccess -> {
+                    if (call.safe) {
+                        val explicitReceiver = call.explicitReceiver
+                        require(explicitReceiver != null)
+                        collect(explicitReceiver)
+                    }
+                    ((call.calleeReference as? FirResolvedCallableReference)?.coneSymbol)?.let { symbol ->
+                        if (symbol is FirVariableSymbol<*> || symbol is FirPropertySymbol) {
+                            result += getRealVariable(symbol as FirBasedSymbol<*>)
+                        }
+                    }
+                }
+                is FirWhenSubjectExpression -> {
+                    call.whenSubject.whenExpression.subjectVariable?.let { result += getRealVariable(it.symbol) }
+                    call.whenSubject.whenExpression.subject?.let { collect(it) }
+                }
+            }
+        }
+
+        collect(call)
+        return result
+    }
+
+    private fun Flow.removeVariable(variable: DataFlowVariable): Flow {
+        variableStorage.removeVariable(variable)
+        return removeVariableFromFlow(variable)
+    }
+
+    private fun Flow.removeSyntheticVariable(variable: DataFlowVariable): Flow {
+        if (!variable.isSynthetic) return this
+        return removeVariable(variable)
    }
 }
@@ -14,6 +14,7 @@ import org.jetbrains.kotlin.fir.references.FirExplicitThisReference
 import org.jetbrains.kotlin.fir.references.FirSimpleNamedReference
 import org.jetbrains.kotlin.fir.resolve.*
 import org.jetbrains.kotlin.fir.resolve.calls.*
+import org.jetbrains.kotlin.fir.resolve.dfa.DataFlowInferenceContext
 import org.jetbrains.kotlin.fir.resolve.dfa.FirDataFlowAnalyzer
 import org.jetbrains.kotlin.fir.resolve.dfa.FirDataFlowAnalyzerImpl
 import org.jetbrains.kotlin.fir.resolve.inference.FirCallCompleter
@@ -926,7 +927,7 @@ open class FirBodyResolveTransformer(
 }

 private fun inferenceComponents(session: FirSession, returnTypeCalculator: ReturnTypeCalculator, scopeSession: ScopeSession) =
-    InferenceComponents(object : ConeInferenceContext, TypeSystemInferenceExtensionContextDelegate {
+    InferenceComponents(object : ConeInferenceContext, TypeSystemInferenceExtensionContextDelegate, DataFlowInferenceContext {
        override fun findCommonIntegerLiteralTypesSuperType(explicitSupertypes: List<SimpleTypeMarker>): SimpleTypeMarker? {
            // TODO: implement
            return null