FIR DFA: do not generate nodes (and flows) for contracts on calls

The code was already duplicated between FirDataFlowAnalyzer and
FirReturnsImpliesAnalyzer, so might as well use the latter to slightly
speed up the former.

compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromLibrary/conditionalEffects.dot

@@ -12,19 +12,12 @@ digraph conditionalEffects_kt {
             2 [label="Access variable R|<local>/x|"];
             3 [label="Type operator: (R|<local>/x| is R|kotlin/Int|)"];
             4 [label="Function call: R|kotlin/require|(...)"];
-            subgraph cluster_2 {
+            5 [label="Access variable R|<local>/x|"];
-                color=blue
+            6 [label="Smart cast: R|<local>/x|"];
-                5 [label="Enter contract"];
+            7 [label="Function call: R|<local>/x|.R|kotlin/Int.inc|()"];
-                6 [label="Access variable R|<local>/x|"];
+            8 [label="Exit block"];
-                7 [label="Type operator: (R|<local>/x| is R|kotlin/Int|)"];
-                8 [label="Exit contract"];
-            }
-            9 [label="Access variable R|<local>/x|"];
-            10 [label="Smart cast: R|<local>/x|"];
-            11 [label="Function call: R|<local>/x|.R|kotlin/Int.inc|()"];
-            12 [label="Exit block"];
         }
-        13 [label="Exit function test_1" style="filled" fillcolor=red];
+        9 [label="Exit function test_1" style="filled" fillcolor=red];
     }
     0 -> {1};
     1 -> {2};
@@ -35,39 +28,48 @@ digraph conditionalEffects_kt {
     6 -> {7};
     7 -> {8};
     8 -> {9};
-    9 -> {10};
+
+    subgraph cluster_2 {
+        color=red
+        10 [label="Enter function test_2" style="filled" fillcolor=red];
+        subgraph cluster_3 {
+            color=blue
+            11 [label="Enter block"];
+            12 [label="Access variable R|<local>/x|"];
+            13 [label="Function call: R|kotlin/requireNotNull|<R|kotlin/String|>(...)"];
+            14 [label="Access variable R|<local>/x|"];
+            15 [label="Smart cast: R|<local>/x|"];
+            16 [label="Access variable R|kotlin/String.length|"];
+            17 [label="Exit block"];
+        }
+        18 [label="Exit function test_2" style="filled" fillcolor=red];
+    }
     10 -> {11};
     11 -> {12};
     12 -> {13};
-
+    13 -> {14};
-    subgraph cluster_3 {
-        color=red
-        14 [label="Enter function test_2" style="filled" fillcolor=red];
-        subgraph cluster_4 {
-            color=blue
-            15 [label="Enter block"];
-            16 [label="Access variable R|<local>/x|"];
-            17 [label="Function call: R|kotlin/requireNotNull|<R|kotlin/String|>(...)"];
-            subgraph cluster_5 {
-                color=blue
-                18 [label="Enter contract"];
-                19 [label="Access variable R|<local>/x|"];
-                20 [label="Const: Null(null)"];
-                21 [label="Equality operator !="];
-                22 [label="Exit contract"];
-            }
-            23 [label="Access variable R|<local>/x|"];
-            24 [label="Smart cast: R|<local>/x|"];
-            25 [label="Access variable R|kotlin/String.length|"];
-            26 [label="Exit block"];
-        }
-        27 [label="Exit function test_2" style="filled" fillcolor=red];
-    }
     14 -> {15};
     15 -> {16};
     16 -> {17};
     17 -> {18};
-    18 -> {19};
+
+    subgraph cluster_4 {
+        color=red
+        19 [label="Enter function test_3" style="filled" fillcolor=red];
+        subgraph cluster_5 {
+            color=blue
+            20 [label="Enter block"];
+            21 [label="Access variable R|<local>/x|"];
+            22 [label="Const: Null(null)"];
+            23 [label="Equality operator !="];
+            24 [label="Function call: R|kotlin/require|(...)"];
+            25 [label="Access variable R|<local>/x|"];
+            26 [label="Smart cast: R|<local>/x|"];
+            27 [label="Access variable R|kotlin/String.length|"];
+            28 [label="Exit block"];
+        }
+        29 [label="Exit function test_3" style="filled" fillcolor=red];
+    }
     19 -> {20};
     20 -> {21};
     21 -> {22};
@@ -76,40 +78,44 @@ digraph conditionalEffects_kt {
     24 -> {25};
     25 -> {26};
     26 -> {27};
+    27 -> {28};
+    28 -> {29};
 
     subgraph cluster_6 {
         color=red
-        28 [label="Enter function test_3" style="filled" fillcolor=red];
+        30 [label="Enter function test_4" style="filled" fillcolor=red];
         subgraph cluster_7 {
             color=blue
-            29 [label="Enter block"];
+            31 [label="Enter block"];
-            30 [label="Access variable R|<local>/x|"];
-            31 [label="Const: Null(null)"];
-            32 [label="Equality operator !="];
-            33 [label="Function call: R|kotlin/require|(...)"];
             subgraph cluster_8 {
                 color=blue
-                34 [label="Enter contract"];
+                32 [label="Enter &&"];
-                35 [label="Access variable R|<local>/x|"];
+                33 [label="Access variable R|<local>/x|"];
-                36 [label="Const: Null(null)"];
+                34 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                37 [label="Equality operator !="];
+                35 [label="Exit left part of &&"];
-                38 [label="Exit contract"];
+                36 [label="Enter right part of &&"];
+                37 [label="Access variable R|<local>/y|"];
+                38 [label="Const: Null(null)"];
+                39 [label="Equality operator !="];
+                40 [label="Exit &&"];
             }
-            39 [label="Access variable R|<local>/x|"];
+            41 [label="Function call: R|kotlin/require|(...)"];
-            40 [label="Smart cast: R|<local>/x|"];
+            42 [label="Access variable R|<local>/x|"];
-            41 [label="Access variable R|kotlin/String.length|"];
+            43 [label="Smart cast: R|<local>/x|"];
-            42 [label="Exit block"];
+            44 [label="Access variable R|kotlin/String.length|"];
+            45 [label="Access variable R|<local>/y|"];
+            46 [label="Smart cast: R|<local>/y|"];
+            47 [label="Access variable R|kotlin/String.length|"];
+            48 [label="Exit block"];
         }
-        43 [label="Exit function test_3" style="filled" fillcolor=red];
+        49 [label="Exit function test_4" style="filled" fillcolor=red];
     }
-    28 -> {29};
-    29 -> {30};
     30 -> {31};
     31 -> {32};
     32 -> {33};
     33 -> {34};
     34 -> {35};
-    35 -> {36};
+    35 -> {40 36};
     36 -> {37};
     37 -> {38};
     38 -> {39};
@@ -117,73 +123,77 @@ digraph conditionalEffects_kt {
     40 -> {41};
     41 -> {42};
     42 -> {43};
-
+    43 -> {44};
-    subgraph cluster_9 {
-        color=red
-        44 [label="Enter function test_4" style="filled" fillcolor=red];
-        subgraph cluster_10 {
-            color=blue
-            45 [label="Enter block"];
-            subgraph cluster_11 {
-                color=blue
-                46 [label="Enter &&"];
-                47 [label="Access variable R|<local>/x|"];
-                48 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                49 [label="Exit left part of &&"];
-                50 [label="Enter right part of &&"];
-                51 [label="Access variable R|<local>/y|"];
-                52 [label="Const: Null(null)"];
-                53 [label="Equality operator !="];
-                54 [label="Exit &&"];
-            }
-            55 [label="Function call: R|kotlin/require|(...)"];
-            subgraph cluster_12 {
-                color=blue
-                56 [label="Enter contract"];
-                subgraph cluster_13 {
-                    color=blue
-                    57 [label="Enter &&"];
-                    58 [label="Access variable R|<local>/x|"];
-                    59 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                    60 [label="Exit left part of &&"];
-                    61 [label="Enter right part of &&"];
-                    62 [label="Access variable R|<local>/y|"];
-                    63 [label="Const: Null(null)"];
-                    64 [label="Equality operator !="];
-                    65 [label="Exit &&"];
-                }
-                66 [label="Exit contract"];
-            }
-            67 [label="Access variable R|<local>/x|"];
-            68 [label="Smart cast: R|<local>/x|"];
-            69 [label="Access variable R|kotlin/String.length|"];
-            70 [label="Access variable R|<local>/y|"];
-            71 [label="Smart cast: R|<local>/y|"];
-            72 [label="Access variable R|kotlin/String.length|"];
-            73 [label="Exit block"];
-        }
-        74 [label="Exit function test_4" style="filled" fillcolor=red];
-    }
     44 -> {45};
     45 -> {46};
     46 -> {47};
     47 -> {48};
     48 -> {49};
-    49 -> {54 50};
+
+    subgraph cluster_9 {
+        color=red
+        50 [label="Enter function test_5" style="filled" fillcolor=red];
+        subgraph cluster_10 {
+            color=blue
+            51 [label="Enter block"];
+            subgraph cluster_11 {
+                color=blue
+                52 [label="Enter when"];
+                subgraph cluster_12 {
+                    color=blue
+                    53 [label="Enter when branch condition "];
+                    54 [label="Access variable R|<local>/b|"];
+                    55 [label="Exit when branch condition"];
+                }
+                subgraph cluster_13 {
+                    color=blue
+                    56 [label="Enter when branch condition else"];
+                    57 [label="Exit when branch condition"];
+                }
+                58 [label="Enter when branch result"];
+                subgraph cluster_14 {
+                    color=blue
+                    59 [label="Enter block"];
+                    60 [label="Access variable R|<local>/x|"];
+                    61 [label="Access variable <Unresolved name: length>#"];
+                    62 [label="Exit block"];
+                }
+                63 [label="Exit when branch result"];
+                64 [label="Enter when branch result"];
+                subgraph cluster_15 {
+                    color=blue
+                    65 [label="Enter block"];
+                    66 [label="Access variable R|<local>/x|"];
+                    67 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
+                    68 [label="Function call: R|kotlin/require|(...)"];
+                    69 [label="Access variable R|<local>/x|"];
+                    70 [label="Smart cast: R|<local>/x|"];
+                    71 [label="Access variable R|kotlin/String.length|"];
+                    72 [label="Exit block"];
+                }
+                73 [label="Exit when branch result"];
+                74 [label="Exit when"];
+            }
+            75 [label="Access variable R|<local>/x|"];
+            76 [label="Access variable <Unresolved name: length>#"];
+            77 [label="Exit block"];
+        }
+        78 [label="Exit function test_5" style="filled" fillcolor=red];
+    }
     50 -> {51};
     51 -> {52};
     52 -> {53};
     53 -> {54};
     54 -> {55};
-    55 -> {56};
+    55 -> {64 56};
     56 -> {57};
     57 -> {58};
     58 -> {59};
     59 -> {60};
-    60 -> {65 61};
+    60 -> {61};
     61 -> {62};
     62 -> {63};
-    63 -> {64};
+    63 -> {74};
     64 -> {65};
     65 -> {66};
     66 -> {67};
@@ -194,78 +204,76 @@ digraph conditionalEffects_kt {
     71 -> {72};
     72 -> {73};
     73 -> {74};
-
+    74 -> {75};
-    subgraph cluster_14 {
-        color=red
-        75 [label="Enter function test_5" style="filled" fillcolor=red];
-        subgraph cluster_15 {
-            color=blue
-            76 [label="Enter block"];
-            subgraph cluster_16 {
-                color=blue
-                77 [label="Enter when"];
-                subgraph cluster_17 {
-                    color=blue
-                    78 [label="Enter when branch condition "];
-                    79 [label="Access variable R|<local>/b|"];
-                    80 [label="Exit when branch condition"];
-                }
-                subgraph cluster_18 {
-                    color=blue
-                    81 [label="Enter when branch condition else"];
-                    82 [label="Exit when branch condition"];
-                }
-                83 [label="Enter when branch result"];
-                subgraph cluster_19 {
-                    color=blue
-                    84 [label="Enter block"];
-                    85 [label="Access variable R|<local>/x|"];
-                    86 [label="Access variable <Unresolved name: length>#"];
-                    87 [label="Exit block"];
-                }
-                88 [label="Exit when branch result"];
-                89 [label="Enter when branch result"];
-                subgraph cluster_20 {
-                    color=blue
-                    90 [label="Enter block"];
-                    91 [label="Access variable R|<local>/x|"];
-                    92 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                    93 [label="Function call: R|kotlin/require|(...)"];
-                    subgraph cluster_21 {
-                        color=blue
-                        94 [label="Enter contract"];
-                        95 [label="Access variable R|<local>/x|"];
-                        96 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                        97 [label="Exit contract"];
-                    }
-                    98 [label="Access variable R|<local>/x|"];
-                    99 [label="Smart cast: R|<local>/x|"];
-                    100 [label="Access variable R|kotlin/String.length|"];
-                    101 [label="Exit block"];
-                }
-                102 [label="Exit when branch result"];
-                103 [label="Exit when"];
-            }
-            104 [label="Access variable R|<local>/x|"];
-            105 [label="Access variable <Unresolved name: length>#"];
-            106 [label="Exit block"];
-        }
-        107 [label="Exit function test_5" style="filled" fillcolor=red];
-    }
     75 -> {76};
     76 -> {77};
     77 -> {78};
-    78 -> {79};
+
+    subgraph cluster_16 {
+        color=red
+        79 [label="Enter function test_6" style="filled" fillcolor=red];
+        subgraph cluster_17 {
+            color=blue
+            80 [label="Enter block"];
+            subgraph cluster_18 {
+                color=blue
+                81 [label="Enter when"];
+                subgraph cluster_19 {
+                    color=blue
+                    82 [label="Enter when branch condition "];
+                    83 [label="Access variable R|<local>/b|"];
+                    84 [label="Exit when branch condition"];
+                }
+                subgraph cluster_20 {
+                    color=blue
+                    85 [label="Enter when branch condition else"];
+                    86 [label="Exit when branch condition"];
+                }
+                87 [label="Enter when branch result"];
+                subgraph cluster_21 {
+                    color=blue
+                    88 [label="Enter block"];
+                    89 [label="Access variable R|<local>/x|"];
+                    90 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
+                    91 [label="Function call: R|kotlin/require|(...)"];
+                    92 [label="Access variable R|<local>/x|"];
+                    93 [label="Smart cast: R|<local>/x|"];
+                    94 [label="Access variable R|kotlin/String.length|"];
+                    95 [label="Exit block"];
+                }
+                96 [label="Exit when branch result"];
+                97 [label="Enter when branch result"];
+                subgraph cluster_22 {
+                    color=blue
+                    98 [label="Enter block"];
+                    99 [label="Access variable R|<local>/x|"];
+                    100 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
+                    101 [label="Function call: R|kotlin/require|(...)"];
+                    102 [label="Access variable R|<local>/x|"];
+                    103 [label="Smart cast: R|<local>/x|"];
+                    104 [label="Access variable R|kotlin/String.length|"];
+                    105 [label="Exit block"];
+                }
+                106 [label="Exit when branch result"];
+                107 [label="Exit when"];
+            }
+            108 [label="Access variable R|<local>/x|"];
+            109 [label="Smart cast: R|<local>/x|"];
+            110 [label="Access variable R|kotlin/String.length|"];
+            111 [label="Exit block"];
+        }
+        112 [label="Exit function test_6" style="filled" fillcolor=red];
+    }
     79 -> {80};
-    80 -> {89 81};
+    80 -> {81};
     81 -> {82};
     82 -> {83};
     83 -> {84};
-    84 -> {85};
+    84 -> {97 85};
     85 -> {86};
     86 -> {87};
     87 -> {88};
-    88 -> {103};
+    88 -> {89};
     89 -> {90};
     90 -> {91};
     91 -> {92};
@@ -273,7 +281,7 @@ digraph conditionalEffects_kt {
     93 -> {94};
     94 -> {95};
     95 -> {96};
-    96 -> {97};
+    96 -> {107};
     97 -> {98};
     98 -> {99};
     99 -> {100};
@@ -284,116 +292,10 @@ digraph conditionalEffects_kt {
     104 -> {105};
     105 -> {106};
     106 -> {107};
-
+    107 -> {108};
-    subgraph cluster_22 {
-        color=red
-        108 [label="Enter function test_6" style="filled" fillcolor=red];
-        subgraph cluster_23 {
-            color=blue
-            109 [label="Enter block"];
-            subgraph cluster_24 {
-                color=blue
-                110 [label="Enter when"];
-                subgraph cluster_25 {
-                    color=blue
-                    111 [label="Enter when branch condition "];
-                    112 [label="Access variable R|<local>/b|"];
-                    113 [label="Exit when branch condition"];
-                }
-                subgraph cluster_26 {
-                    color=blue
-                    114 [label="Enter when branch condition else"];
-                    115 [label="Exit when branch condition"];
-                }
-                116 [label="Enter when branch result"];
-                subgraph cluster_27 {
-                    color=blue
-                    117 [label="Enter block"];
-                    118 [label="Access variable R|<local>/x|"];
-                    119 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                    120 [label="Function call: R|kotlin/require|(...)"];
-                    subgraph cluster_28 {
-                        color=blue
-                        121 [label="Enter contract"];
-                        122 [label="Access variable R|<local>/x|"];
-                        123 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                        124 [label="Exit contract"];
-                    }
-                    125 [label="Access variable R|<local>/x|"];
-                    126 [label="Smart cast: R|<local>/x|"];
-                    127 [label="Access variable R|kotlin/String.length|"];
-                    128 [label="Exit block"];
-                }
-                129 [label="Exit when branch result"];
-                130 [label="Enter when branch result"];
-                subgraph cluster_29 {
-                    color=blue
-                    131 [label="Enter block"];
-                    132 [label="Access variable R|<local>/x|"];
-                    133 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                    134 [label="Function call: R|kotlin/require|(...)"];
-                    subgraph cluster_30 {
-                        color=blue
-                        135 [label="Enter contract"];
-                        136 [label="Access variable R|<local>/x|"];
-                        137 [label="Type operator: (R|<local>/x| is R|kotlin/String|)"];
-                        138 [label="Exit contract"];
-                    }
-                    139 [label="Access variable R|<local>/x|"];
-                    140 [label="Smart cast: R|<local>/x|"];
-                    141 [label="Access variable R|kotlin/String.length|"];
-                    142 [label="Exit block"];
-                }
-                143 [label="Exit when branch result"];
-                144 [label="Exit when"];
-            }
-            145 [label="Access variable R|<local>/x|"];
-            146 [label="Smart cast: R|<local>/x|"];
-            147 [label="Access variable R|kotlin/String.length|"];
-            148 [label="Exit block"];
-        }
-        149 [label="Exit function test_6" style="filled" fillcolor=red];
-    }
     108 -> {109};
     109 -> {110};
     110 -> {111};
     111 -> {112};
-    112 -> {113};
-    113 -> {130 114};
-    114 -> {115};
-    115 -> {116};
-    116 -> {117};
-    117 -> {118};
-    118 -> {119};
-    119 -> {120};
-    120 -> {121};
-    121 -> {122};
-    122 -> {123};
-    123 -> {124};
-    124 -> {125};
-    125 -> {126};
-    126 -> {127};
-    127 -> {128};
-    128 -> {129};
-    129 -> {144};
-    130 -> {131};
-    131 -> {132};
-    132 -> {133};
-    133 -> {134};
-    134 -> {135};
-    135 -> {136};
-    136 -> {137};
-    137 -> {138};
-    138 -> {139};
-    139 -> {140};
-    140 -> {141};
-    141 -> {142};
-    142 -> {143};
-    143 -> {144};
-    144 -> {145};
-    145 -> {146};
-    146 -> {147};
-    147 -> {148};
-    148 -> {149};
 
 }

compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/propertyAccessors.kt

@@ -12,10 +12,10 @@ var Any?.isNotNull: Boolean
         return this != null
     }
     set(value) {
-        contract {
+        <!WRONG_IMPLIES_CONDITION!>contract {
             returns() implies (this@isNotNull != null)
             <!ERROR_IN_CONTRACT_DESCRIPTION!>require(<!SENSELESS_COMPARISON!>this != null<!>)<!>
-        }
+        }<!>
     }
 
 fun test_1(a: A?) {

compiler/fir/checkers/src/org/jetbrains/kotlin/fir/analysis/cfa/FirReturnsImpliesAnalyzer.kt

@@ -7,12 +7,10 @@ package org.jetbrains.kotlin.fir.analysis.cfa
 
 import org.jetbrains.kotlin.diagnostics.DiagnosticReporter
 import org.jetbrains.kotlin.diagnostics.reportOn
-import org.jetbrains.kotlin.fir.BuiltinTypes
 import org.jetbrains.kotlin.fir.FirSession
 import org.jetbrains.kotlin.fir.analysis.cfa.util.previousCfgNodes
 import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker
 import org.jetbrains.kotlin.fir.analysis.checkers.context.CheckerContext
-import org.jetbrains.kotlin.fir.analysis.checkers.isSupertypeOf
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors
 import org.jetbrains.kotlin.fir.contracts.FirResolvedContractDescription
 import org.jetbrains.kotlin.fir.contracts.coneEffects
@@ -27,10 +25,11 @@ import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode
 import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraph
 import org.jetbrains.kotlin.fir.resolve.dfa.cfg.JumpNode
 import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirCallableSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirPropertyAccessorSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirValueParameterSymbol
 import org.jetbrains.kotlin.fir.types.*
 import org.jetbrains.kotlin.types.AbstractTypeChecker
-import org.jetbrains.kotlin.types.ConstantValueKind
 
 object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
 
@@ -47,11 +46,10 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
 
         val logicSystem = object : PersistentLogicSystem(context.session.typeContext) {
             override val variableStorage: VariableStorageImpl
-                get() = dataFlowInfo.variableStorage as VariableStorageImpl
+                get() = throw IllegalStateException("shouldn't be called")
 
-            override fun ConeKotlinType.isAcceptableForSmartcast(): Boolean {
+            override fun ConeKotlinType.isAcceptableForSmartcast(): Boolean =
-                return !isNullableNothing
+                !isNullableNothing
-            }
         }
 
         effects.forEach { effect ->
@@ -89,94 +87,70 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
             }
         }
 
-        // TODO: create separate variable storage and don't modify existing one
-        val variableStorage = dataFlowInfo.variableStorage as VariableStorageImpl
         val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow
         var typeStatements: TypeStatements = flow.approvedTypeStatements
 
-        if (effect.value != ConeConstantReference.WILDCARD) {
+        val operation = effect.value.toOperation()
-            val operation = effect.value.toOperation()
+        if (operation != null) {
-            if (expressionType != null && expressionType.isInapplicableWith(operation, context.session)) return false
-
             if (resultExpression is FirConstExpression<*>) {
-                if (!resultExpression.isApplicableWith(operation)) return false
+                if (!operation.isTrueFor(resultExpression.value)) return false
             } else {
-                val resultVar = variableStorage.getOrCreate(flow, resultExpression)
+                if (expressionType != null && !operation.canBeTrueFor(context.session, expressionType)) return false
-                typeStatements = logicSystem.andForTypeStatements(
+                // TODO: avoid modifying the storage
-                    typeStatements,
+                val variableStorage = dataFlowInfo.variableStorage as VariableStorageImpl
-                    logicSystem.approveOperationStatement(flow, OperationStatement(resultVar, operation))
+                val resultVar = variableStorage.getOrCreateIfReal(flow, resultExpression)
-                )
+                if (resultVar != null) {
-            }
+                    typeStatements = logicSystem.andForTypeStatements(
-        }
+                        typeStatements,
-
+                        logicSystem.approveOperationStatement(flow, OperationStatement(resultVar, operation))
-        val conditionStatements = effectDeclaration.condition.buildTypeStatements(
+                    )
-            function, logicSystem, variableStorage, context
-        ) ?: return false
-
-        for ((realVar, requiredTypeStatement) in conditionStatements) {
-            val fixedRealVar = typeStatements.keys.find { it.identifier == realVar.identifier } ?: realVar
-            val originalType = function.getParameterType(fixedRealVar.identifier.symbol, context) ?: continue
-            val resultType = typeStatements[fixedRealVar]?.exactType.intersectWith(typeContext, originalType)
-            val requiredType = typeContext.intersectTypesOrNull(requiredTypeStatement.exactType.toList())
-            if (requiredType != null && !requiredType.isSupertypeOf(typeContext, resultType)) return true
-        }
-        return false
-    }
-
-    private fun ConeBooleanExpression.buildTypeStatements(
-        function: FirFunction,
-        logicSystem: LogicSystem<*>,
-        variableStorage: VariableStorage,
-        context: CheckerContext
-    ): TypeStatements? {
-        fun ConeValueParameterReference.toVariable(): RealVariable {
-            val parameterSymbol = function.getParameterSymbol(parameterIndex, context)
-            return variableStorage.getLocalVariable(parameterSymbol)
-                ?: RealVariable(
-                    Identifier(parameterSymbol, null, null),
-                    parameterIndex < 0, null, parameterIndex + 1, PropertyStability.STABLE_VALUE
-                )
-        }
-
-        fun ConeBooleanExpression.toTypeStatements(inverted: Boolean): TypeStatements? = when (this) {
-            is ConeBinaryLogicExpression -> {
-                val left = left.toTypeStatements(inverted)
-                val right = right.toTypeStatements(inverted)
-                when {
-                    left == null -> right
-                    right == null -> left
-                    (kind == LogicOperationKind.AND) == !inverted -> logicSystem.andForTypeStatements(left, right)
-                    else -> logicSystem.orForTypeStatements(left, right)
                 }
             }
-            is ConeIsInstancePredicate ->
-                if (isNegated == inverted) (arg.toVariable() typeEq type).singleton() else mapOf()
-            is ConeIsNullPredicate ->
-                arg.toVariable().nullabilityStatement(context.session.builtinTypes, isNull = isNegated == inverted).singleton()
-            is ConeLogicalNot -> arg.toTypeStatements(!inverted)
-            else -> null
         }
 
-        return toTypeStatements(inverted = false)
+        // TODO: if this is not a top-level function, `FirDataFlowAnalyzer` has erased its value parameters
+        //  from `dataFlowInfo.variableStorage` for some reason, so its `getLocalVariable` doesn't work.
+        val knownVariables = typeStatements.keys.associateBy { it.identifier }
+        val argumentVariables = Array(function.valueParameters.size + 1) { i ->
+            val parameterSymbol = if (i > 0) {
+                function.valueParameters[i - 1].symbol
+            } else {
+                if (function.symbol is FirPropertyAccessorSymbol) {
+                    context.containingProperty?.symbol
+                } else {
+                    null
+                } ?: function.symbol
+            }
+            val identifier = Identifier(parameterSymbol, null, null)
+            // Might be unknown if there are no statements made about that parameter, but it's still possible that trivial
+            // contracts are valid. E.g. `returns() implies (x is String)` when `x`'s *original type* is already `String`.
+            knownVariables[identifier] ?: RealVariable(identifier, i == 0, null, i, PropertyStability.STABLE_VALUE)
+        }
+
+        val conditionStatements = logicSystem.approveContractStatement(
+            flow, effectDeclaration.condition, argumentVariables, substitutor = null
+        ) ?: return true
+
+        return !conditionStatements.values.all { requirement ->
+            val originalType = requirement.variable.identifier.symbol.correspondingParameterType ?: return@all true
+            val requiredType = requirement.smartCastedType(typeContext, originalType)
+            val actualType = typeStatements[requirement.variable].smartCastedType(typeContext, originalType)
+            actualType.isSubtypeOf(typeContext, requiredType)
+        }
     }
 
-    private fun RealVariable.nullabilityStatement(builtinTypes: BuiltinTypes, isNull: Boolean) =
+    private fun Operation.canBeTrueFor(session: FirSession, type: ConeKotlinType): Boolean = when (this) {
-        this typeEq (if (isNull) builtinTypes.nullableNothingType.type else builtinTypes.anyType.type)
+        Operation.EqTrue, Operation.EqFalse ->
-
+            AbstractTypeChecker.isSubtypeOf(session.typeContext, session.builtinTypes.booleanType.type, type)
-    private fun TypeStatement.singleton(): TypeStatements =
+        Operation.EqNull -> type.canBeNull
-        mapOf(variable to this)
+        Operation.NotEqNull -> !type.isNullableNothing
-
-    private fun ConeKotlinType.isInapplicableWith(operation: Operation, session: FirSession): Boolean {
-        return (operation == Operation.EqFalse || operation == Operation.EqTrue)
-                && !AbstractTypeChecker.isSubtypeOf(session.typeContext, session.builtinTypes.booleanType.type, this)
-                || operation == Operation.EqNull && !isNullable
     }
 
-    private fun FirConstExpression<*>.isApplicableWith(operation: Operation): Boolean = when {
+    private fun Operation.isTrueFor(value: Any?) = when (this) {
-        kind == ConstantValueKind.Null -> operation == Operation.EqNull
+        Operation.EqTrue -> value == true
-        kind == ConstantValueKind.Boolean && operation == Operation.EqTrue -> (value as Boolean)
+        Operation.EqFalse -> value == false
-        kind == ConstantValueKind.Boolean && operation == Operation.EqFalse -> !(value as Boolean)
+        Operation.EqNull -> value == null
-        else -> true
+        Operation.NotEqNull -> value != null
     }
 
     private fun CFGNode<*>.collectBranchExits(nodes: MutableList<CFGNode<*>> = mutableListOf()): List<CFGNode<*>> {
@@ -189,28 +163,10 @@ object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
     private val CheckerContext.containingProperty: FirProperty?
         get() = (containingDeclarations.lastOrNull { it is FirProperty } as? FirProperty)
 
-    private fun FirFunction.getParameterType(symbol: FirBasedSymbol<*>, context: CheckerContext): ConeKotlinType? {
+    private val FirBasedSymbol<*>.correspondingParameterType: ConeKotlinType?
-        val typeRef = if (this.symbol == symbol) {
+        get() = when (this) {
-            if (symbol is FirPropertyAccessorSymbol) {
+            is FirValueParameterSymbol -> resolvedReturnType
-                context.containingProperty?.receiverParameter?.typeRef
+            is FirCallableSymbol<*> -> resolvedReceiverTypeRef?.coneType
-            } else {
+            else -> null
-                receiverParameter?.typeRef
-            }
-        } else {
-            valueParameters.find { it.symbol == symbol }?.returnTypeRef
         }
-        return typeRef?.coneType
-    }
-
-    private fun FirFunction.getParameterSymbol(index: Int, context: CheckerContext): FirBasedSymbol<*> {
-        return if (index == -1) {
-            if (symbol !is FirPropertyAccessorSymbol) {
-                symbol
-            } else {
-                context.containingProperty?.symbol ?: symbol
-            }
-        } else {
-            this.valueParameters[index].symbol
-        }
-    }
 }

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/FirDataFlowAnalyzer.kt

@@ -11,19 +11,16 @@ import org.jetbrains.kotlin.descriptors.Modality
 import org.jetbrains.kotlin.fir.*
 import org.jetbrains.kotlin.fir.contracts.FirResolvedContractDescription
 import org.jetbrains.kotlin.fir.contracts.description.ConeConditionalEffectDeclaration
-import org.jetbrains.kotlin.fir.contracts.description.ConeConstantReference
 import org.jetbrains.kotlin.fir.contracts.description.ConeReturnsEffectDeclaration
 import org.jetbrains.kotlin.fir.declarations.*
 import org.jetbrains.kotlin.fir.declarations.impl.FirDefaultPropertyAccessor
 import org.jetbrains.kotlin.fir.declarations.utils.isLocal
 import org.jetbrains.kotlin.fir.expressions.*
+import org.jetbrains.kotlin.fir.expressions.impl.FirNoReceiverExpression
 import org.jetbrains.kotlin.fir.references.FirControlFlowGraphReference
 import org.jetbrains.kotlin.fir.resolve.*
 import org.jetbrains.kotlin.fir.resolve.calls.ImplicitReceiverValue
 import org.jetbrains.kotlin.fir.resolve.dfa.cfg.*
-import org.jetbrains.kotlin.fir.resolve.dfa.contracts.buildContractFir
-import org.jetbrains.kotlin.fir.resolve.dfa.contracts.createArgumentsMapping
-import org.jetbrains.kotlin.fir.resolve.substitution.ConeSubstitutor
 import org.jetbrains.kotlin.fir.resolve.substitution.ConeSubstitutorByMap
 import org.jetbrains.kotlin.fir.resolve.transformers.body.resolve.FirAbstractBodyResolveTransformer
 import org.jetbrains.kotlin.fir.resolve.transformers.body.resolve.resultType
@@ -35,7 +32,6 @@ import org.jetbrains.kotlin.fir.symbols.impl.FirRegularClassSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirTypeParameterSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol
 import org.jetbrains.kotlin.fir.types.*
-import org.jetbrains.kotlin.fir.visitors.transformSingle
 import org.jetbrains.kotlin.name.StandardClassIds
 import org.jetbrains.kotlin.types.ConstantValueKind
 import org.jetbrains.kotlin.util.OperatorNameConventions
@@ -99,7 +95,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
                 override fun receiverUpdated(symbol: FirBasedSymbol<*>, info: TypeStatement?) {
                     val index = receiverStack.getReceiverIndex(symbol) ?: return
                     val originalType = receiverStack.getOriginalType(index)
-                    receiverStack.replaceReceiverType(index, info?.exactType.intersectWith(typeContext, originalType))
+                    receiverStack.replaceReceiverType(index, info.smartCastedType(typeContext, originalType))
                 }
 
                 override val logicSystem: PersistentLogicSystem =
@@ -139,8 +135,6 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
     private val graphBuilder get() = context.graphBuilder
     private val variableStorage get() = context.variableStorage
 
-    private var contractDescriptionVisitingMode = false
-
     private val any = components.session.builtinTypes.anyType.type
     private val nullableNothing = components.session.builtinTypes.nullableNothingType.type
 
@@ -393,7 +387,11 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
                             flow.addImplication((expressionVariable eq isType) implies (operandVariable typeEq type))
                         }
                         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))
                         }
                     }
                 }
@@ -408,7 +406,8 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
                 } else {
                     val expressionVariable = variableStorage.createSynthetic(typeOperatorCall)
                     flow.addImplication((expressionVariable notEq null) implies (operandVariable notEq null))
-                    // TODO? flow.addImplication((expressionVariable eq null) implies (operandVariable eq null))
+                    // TODO? (x as T?) == null => x == null
+                    // flow.addImplication((expressionVariable eq null) implies (operandVariable eq null))
                 }
             }
 
@@ -771,8 +770,8 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
     fun enterQualifiedAccessExpression() {}
 
     fun exitQualifiedAccessExpression(qualifiedAccessExpression: FirQualifiedAccessExpression) {
-        graphBuilder.exitQualifiedAccessExpression(qualifiedAccessExpression).mergeIncomingFlow()
+        val flow = graphBuilder.exitQualifiedAccessExpression(qualifiedAccessExpression).mergeIncomingFlow()
-        processConditionalContract(qualifiedAccessExpression)
+        processConditionalContract(flow, qualifiedAccessExpression)
     }
 
     fun exitSmartCastExpression(smartCastExpression: FirSmartCastExpression) {
@@ -843,10 +842,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
         val (functionCallNode, unionNode) = graphBuilder.exitFunctionCall(functionCall, callCompleted)
         unionNode?.unionFlowFromArguments()
         val flow = functionCallNode.mergeIncomingFlow()
-        if (functionCall.isBooleanNot()) {
+        processConditionalContract(flow, functionCall)
-            exitBooleanNot(flow, functionCall, functionCallNode)
-        }
-        processConditionalContract(functionCall)
     }
 
     fun exitDelegatedConstructorCall(call: FirDelegatedConstructorCall, callCompleted: Boolean) {
@@ -865,69 +861,74 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
         flow = logicSystem.unionFlow(previousNodes.map { it.flow })
     }
 
-    private fun processConditionalContract(qualifiedAccess: FirQualifiedAccess) {
+    private fun FirQualifiedAccess.orderedArguments(callee: FirFunction): Array<out FirExpression?>? {
-        val owner: FirContractDescriptionOwner? = when (qualifiedAccess) {
+        val receiver = extensionReceiver.takeIf { it != FirNoReceiverExpression }
+            ?: dispatchReceiver.takeIf { it != FirNoReceiverExpression }
+        return when (this) {
+            is FirFunctionCall -> {
+                val argumentToParameter = resolvedArgumentMapping ?: return null
+                val parameterToArgument = argumentToParameter.entries.associate { it.value to it.key.unwrapArgument() }
+                Array(callee.valueParameters.size + 1) { i ->
+                    if (i > 0) parameterToArgument[callee.valueParameters[i - 1]] else receiver
+                }
+            }
+            is FirQualifiedAccessExpression -> arrayOf(receiver)
+            is FirVariableAssignment -> arrayOf(receiver, rValue)
+            else -> return null
+        }
+    }
+
+    private fun processConditionalContract(flow: FLOW, qualifiedAccess: FirQualifiedAccess) {
+        val callee = when (qualifiedAccess) {
             is FirFunctionCall -> qualifiedAccess.toResolvedCallableSymbol()?.fir as? FirSimpleFunction
-            is FirQualifiedAccessExpression -> {
+            is FirQualifiedAccessExpression -> (qualifiedAccess.calleeReference.resolvedSymbol?.fir as? FirProperty)?.getter
-                val property = qualifiedAccess.calleeReference.resolvedSymbol?.fir as? FirProperty
+            is FirVariableAssignment -> (qualifiedAccess.lValue.resolvedSymbol?.fir as? FirProperty)?.setter
-                property?.getter
-            }
-            is FirVariableAssignment -> {
-                val property = qualifiedAccess.lValue.resolvedSymbol?.fir as? FirProperty
-                property?.setter
-            }
             else -> null
+        } ?: return
+
+        if (callee.symbol.callableId == StandardClassIds.Callables.not) {
+            // Special hardcoded contract for Boolean.not():
+            //   returns(true) implies (this == false)
+            //   returns(false) implies (this == true)
+            return exitBooleanNot(flow, qualifiedAccess as FirFunctionCall)
         }
 
-        val contractDescription = owner?.contractDescription as? FirResolvedContractDescription ?: return
+        val contractDescription = callee.contractDescription as? FirResolvedContractDescription ?: return
-        val conditionalEffects = contractDescription.effects.map { it.effect }.filterIsInstance<ConeConditionalEffectDeclaration>()
+        val conditionalEffects = contractDescription.effects.mapNotNull { it.effect as? ConeConditionalEffectDeclaration }
         if (conditionalEffects.isEmpty()) return
-        val argumentsMapping = createArgumentsMapping(qualifiedAccess) ?: return
 
-        val typeParameters = (owner as? FirTypeParameterRefsOwner)?.typeParameters
+        val arguments = qualifiedAccess.orderedArguments(callee) ?: return
-        val substitutor = if (!typeParameters.isNullOrEmpty()) {
+        val argumentVariables = Array(arguments.size) { i -> arguments[i]?.let { variableStorage.getOrCreateIfReal(flow, it) } }
+        if (argumentVariables.all { it == null }) return
+
+        val typeParameters = callee.typeParameters
+        val substitutor = if (typeParameters.isNotEmpty()) {
             @Suppress("UNCHECKED_CAST")
             val substitutionFromArguments = typeParameters.zip(qualifiedAccess.typeArguments).map { (typeParameterRef, typeArgument) ->
                 typeParameterRef.symbol to typeArgument.toConeTypeProjection().type
             }.filter { it.second != null }.toMap() as Map<FirTypeParameterSymbol, ConeKotlinType>
             ConeSubstitutorByMap(substitutionFromArguments, components.session)
         } else {
-            ConeSubstitutor.Empty
+            null
         }
 
-        contractDescriptionVisitingMode = true
-        graphBuilder.enterContract(qualifiedAccess).mergeIncomingFlow()
-        val lastFlow = graphBuilder.lastNode.flow
-        val functionCallVariable = variableStorage.getOrCreate(lastFlow, qualifiedAccess)
         for (conditionalEffect in conditionalEffects) {
-            val fir = conditionalEffect.buildContractFir(argumentsMapping, substitutor) ?: continue
             val effect = conditionalEffect.effect as? ConeReturnsEffectDeclaration ?: continue
-            fir.transformSingle(components.transformer, ResolutionMode.ContextDependent)
+            val operation = effect.value.toOperation()
-            val argumentVariable = variableStorage.get(lastFlow, fir) ?: continue
+            val statements = logicSystem.approveContractStatement(
-            val lastNode = graphBuilder.lastNode
+                flow, conditionalEffect.condition, argumentVariables, substitutor, removeApprovedOrImpossible = operation == null
-            when (val value = effect.value) {
+            ) ?: continue // TODO: do what if the result is known to be false?
-                ConeConstantReference.WILDCARD -> {
+            if (operation == null) {
-                    lastNode.flow.commitOperationStatement(argumentVariable eq true)
+                statements.values.forEach { flow.addTypeStatement(it) }
-                }
+            } else {
-
+                val functionCallVariable = variableStorage.getOrCreate(flow, qualifiedAccess)
-                else -> {
+                flow.addAllConditionally(OperationStatement(functionCallVariable, operation), statements)
-                    logicSystem.translateVariableFromConditionInStatements(
-                        lastNode.flow,
-                        argumentVariable,
-                        functionCallVariable,
-                        shouldRemoveOriginalStatements = true,
-                        filter = { it.condition.operation == Operation.EqTrue },
-                        transform = { OperationStatement(it.condition.variable, value.toOperation()) implies it.effect }
-                    )
-                }
             }
         }
-        graphBuilder.exitContract(qualifiedAccess).mergeIncomingFlow()
-        contractDescriptionVisitingMode = false
     }
 
     fun exitConstExpression(constExpression: FirConstExpression<*>) {
-        if (constExpression.resultType is FirResolvedTypeRef && !contractDescriptionVisitingMode) return
+        if (constExpression.resultType is FirResolvedTypeRef) return
         graphBuilder.exitConstExpression(constExpression).mergeIncomingFlow()
     }
 
@@ -949,7 +950,7 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
                 logicSystem.recordNewAssignment(flow, variable, context.newAssignmentIndex())
             }
         }
-        processConditionalContract(assignment)
+        processConditionalContract(flow, assignment)
     }
 
     private fun exitVariableInitialization(
@@ -1089,9 +1090,9 @@ abstract class FirDataFlowAnalyzer<FLOW : Flow>(
         }
     }
 
-    private fun exitBooleanNot(flow: FLOW, functionCall: FirFunctionCall, node: FunctionCallNode) {
+    private fun exitBooleanNot(flow: FLOW, expression: FirFunctionCall) {
-        val argumentVariable = variableStorage.get(flow, node.firstPreviousNode.fir) ?: return
+        val argumentVariable = variableStorage.get(flow, expression.dispatchReceiver) ?: return
-        val expressionVariable = variableStorage.createSynthetic(functionCall)
+        val expressionVariable = variableStorage.createSynthetic(expression)
         // Alternatively: (expression == true => argument == false) && (expression == false => argument == true)
         // Which implementation is faster and/or consumes less memory is an open question.
         logicSystem.translateVariableFromConditionInStatements(flow, argumentVariable, expressionVariable) {

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/ControlFlowGraphBuilder.kt

@@ -888,14 +888,6 @@ class ControlFlowGraphBuilder {
         return leftExitNode to rightExitNode
     }
 
-    fun enterContract(qualifiedAccess: FirQualifiedAccess): EnterContractNode {
-        return createEnterContractNode(qualifiedAccess).also { addNewSimpleNode(it) }
-    }
-
-    fun exitContract(qualifiedAccess: FirQualifiedAccess): ExitContractNode {
-        return createExitContractNode(qualifiedAccess).also { addNewSimpleNode(it) }
-    }
-
     fun exitBinaryOr(binaryLogicExpression: FirBinaryLogicExpression): BinaryOrExitNode {
         assert(binaryLogicExpression.kind == LogicOperationKind.OR)
         levelCounter--

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/ControlFlowGraphNodeBuilder.kt

@@ -166,12 +166,6 @@ fun ControlFlowGraphBuilder.createElvisExitNode(fir: FirElvisExpression): ElvisE
 fun ControlFlowGraphBuilder.createVariableDeclarationNode(fir: FirProperty): VariableDeclarationNode =
     VariableDeclarationNode(currentGraph, fir, levelCounter, createId())
 
-fun ControlFlowGraphBuilder.createExitContractNode(fir: FirQualifiedAccess): ExitContractNode =
-    ExitContractNode(currentGraph, fir, levelCounter, createId())
-
-fun ControlFlowGraphBuilder.createEnterContractNode(fir: FirQualifiedAccess): EnterContractNode =
-    EnterContractNode(currentGraph, fir, levelCounter, createId())
-
 fun ControlFlowGraphBuilder.createConstExpressionNode(fir: FirConstExpression<*>): ConstExpressionNode =
     ConstExpressionNode(currentGraph, fir, levelCounter, createId())
 

compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/dfa/contracts/ConeConditionalEffectToFirVisitor.kt

@@ -1,116 +0,0 @@
-/*
- * Copyright 2010-2019 JetBrains s.r.o. and Kotlin Programming Language contributors.
- * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
- */
-
-package org.jetbrains.kotlin.fir.resolve.dfa.contracts
-
-import org.jetbrains.kotlin.fir.contracts.description.*
-import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
-import org.jetbrains.kotlin.fir.expressions.*
-import org.jetbrains.kotlin.fir.expressions.builder.*
-import org.jetbrains.kotlin.fir.expressions.impl.FirNoReceiverExpression
-import org.jetbrains.kotlin.fir.references.builder.buildSimpleNamedReference
-import org.jetbrains.kotlin.fir.resolve.substitution.ConeSubstitutor
-import org.jetbrains.kotlin.fir.types.builder.buildResolvedTypeRef
-import org.jetbrains.kotlin.types.ConstantValueKind
-import org.jetbrains.kotlin.util.OperatorNameConventions
-
-private class ConeConditionalEffectToFirVisitor(
-    val valueParametersMapping: Map<Int, FirExpression>,
-    val substitutor: ConeSubstitutor
-) : ConeContractDescriptionVisitor<FirExpression?, Nothing?>() {
-    override fun visitConditionalEffectDeclaration(conditionalEffect: ConeConditionalEffectDeclaration, data: Nothing?): FirExpression? {
-        return conditionalEffect.condition.accept(this, data)
-    }
-
-    override fun visitConstantDescriptor(constantReference: ConeConstantReference, data: Nothing?): FirExpression? {
-        return when (constantReference) {
-            ConeBooleanConstantReference.TRUE -> buildConstExpression(null, ConstantValueKind.Boolean, true)
-            ConeBooleanConstantReference.FALSE -> buildConstExpression(null, ConstantValueKind.Boolean, false)
-            ConeConstantReference.NULL -> createConstNull()
-            else -> null
-        }
-    }
-
-    override fun visitLogicalBinaryOperationContractExpression(
-        binaryLogicExpression: ConeBinaryLogicExpression,
-        data: Nothing?
-    ): FirExpression? {
-        val leftExpression = binaryLogicExpression.left.accept(this, data) ?: return null
-        val rightExpression = binaryLogicExpression.right.accept(this, data) ?: return null
-        return buildBinaryLogicExpression {
-            leftOperand = leftExpression
-            rightOperand = rightExpression
-            kind = binaryLogicExpression.kind
-        }
-    }
-
-    override fun visitLogicalNot(logicalNot: ConeLogicalNot, data: Nothing?): FirExpression? {
-        val explicitReceiver = logicalNot.arg.accept(this, data) ?: return null
-        return buildFunctionCall {
-            calleeReference = buildSimpleNamedReference { name = OperatorNameConventions.NOT }
-            this.explicitReceiver = explicitReceiver
-            origin = FirFunctionCallOrigin.Operator
-        }
-    }
-
-    override fun visitIsInstancePredicate(isInstancePredicate: ConeIsInstancePredicate, data: Nothing?): FirExpression? {
-        val argument = isInstancePredicate.arg.accept(this@ConeConditionalEffectToFirVisitor, data) ?: return null
-        return buildTypeOperatorCall {
-            argumentList = buildUnaryArgumentList(argument)
-            operation = if (isInstancePredicate.isNegated) {
-                FirOperation.NOT_IS
-            } else {
-                FirOperation.IS
-            }
-            conversionTypeRef = buildResolvedTypeRef { type = substitutor.substituteOrSelf(isInstancePredicate.type) }
-        }
-    }
-
-    override fun visitIsNullPredicate(isNullPredicate: ConeIsNullPredicate, data: Nothing?): FirExpression? {
-        val argument = isNullPredicate.arg.accept(this, data) ?: return null
-        return buildEqualityOperatorCall {
-            operation = if (isNullPredicate.isNegated) {
-                FirOperation.NOT_EQ
-            } else {
-                FirOperation.EQ
-            }
-            argumentList = buildBinaryArgumentList(argument, createConstNull())
-        }
-    }
-
-    override fun visitValueParameterReference(valueParameterReference: ConeValueParameterReference, data: Nothing?): FirExpression? {
-        return valueParametersMapping[valueParameterReference.parameterIndex]
-    }
-
-    private fun createConstNull(): FirConstExpression<*> = buildConstExpression(null, ConstantValueKind.Null, null)
-}
-
-fun ConeConditionalEffectDeclaration.buildContractFir(
-    argumentMapping: Map<Int, FirExpression>,
-    substitutor: ConeSubstitutor
-): FirExpression? {
-    return condition.accept(ConeConditionalEffectToFirVisitor(argumentMapping, substitutor), null)
-}
-
-fun createArgumentsMapping(qualifiedAccess: FirQualifiedAccess): Map<Int, FirExpression>? {
-    val argumentsMapping = mutableMapOf<Int, FirExpression>()
-    qualifiedAccess.extensionReceiver.takeIf { it != FirNoReceiverExpression }?.let { argumentsMapping[-1] = it }
-        ?: qualifiedAccess.dispatchReceiver.takeIf { it != FirNoReceiverExpression }?.let { argumentsMapping[-1] = it }
-    when (qualifiedAccess) {
-        is FirFunctionCall -> {
-            val function = qualifiedAccess.toResolvedCallableSymbol()?.fir as? FirSimpleFunction ?: return null
-            val parameterToIndex = function.valueParameters.mapIndexed { index, parameter -> parameter to index }.toMap()
-            val callArgumentMapping = qualifiedAccess.resolvedArgumentMapping ?: return null
-            for (argument in qualifiedAccess.arguments) {
-                argumentsMapping[parameterToIndex.getValue(callArgumentMapping.getValue(argument))] = argument.unwrapArgument()
-            }
-        }
-        is FirVariableAssignment -> {
-            argumentsMapping[0] = qualifiedAccess.rValue
-        }
-    }
-    return argumentsMapping
-}
-

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/LogicSystem.kt

@@ -28,7 +28,6 @@ abstract class LogicSystem<FLOW : Flow>(protected val context: ConeInferenceCont
         originalVariable: DataFlowVariable,
         newVariable: DataFlowVariable,
         shouldRemoveOriginalStatements: Boolean = originalVariable.isSynthetic(),
-        filter: (Implication) -> Boolean = { true },
         transform: (Implication) -> Implication? = { it },
     )
 

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/PersistentLogicSystem.kt

@@ -237,12 +237,11 @@ abstract class PersistentLogicSystem(context: ConeInferenceContext) : LogicSyste
         originalVariable: DataFlowVariable,
         newVariable: DataFlowVariable,
         shouldRemoveOriginalStatements: Boolean,
-        filter: (Implication) -> Boolean,
         transform: (Implication) -> Implication?
     ) {
         with(flow) {
             val statements = logicStatements[originalVariable]?.takeIf { it.isNotEmpty() } ?: return
-            val newStatements = statements.filter(filter).mapNotNull {
+            val newStatements = statements.mapNotNull {
                 val newStatement = OperationStatement(newVariable, it.condition.operation) implies it.effect
                 transform(newStatement)
             }.toPersistentList()

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/CFGNode.kt

@@ -761,19 +761,6 @@ class VariableAssignmentNode(owner: ControlFlowGraph, override val fir: FirVaria
     }
 }
 
-class EnterContractNode(owner: ControlFlowGraph, override val fir: FirQualifiedAccess, level: Int, id: Int) : CFGNode<FirQualifiedAccess>(owner, level, id),
-    EnterNodeMarker {
-    override fun <R, D> accept(visitor: ControlFlowGraphVisitor<R, D>, data: D): R {
-        return visitor.visitEnterContractNode(this, data)
-    }
-}
-class ExitContractNode(owner: ControlFlowGraph, override val fir: FirQualifiedAccess, level: Int, id: Int) : CFGNode<FirQualifiedAccess>(owner, level, id),
-    ExitNodeMarker {
-    override fun <R, D> accept(visitor: ControlFlowGraphVisitor<R, D>, data: D): R {
-        return visitor.visitExitContractNode(this, data)
-    }
-}
-
 class EnterSafeCallNode(owner: ControlFlowGraph, override val fir: FirSafeCallExpression, level: Int, id: Int) : CFGNode<FirSafeCallExpression>(owner, level, id) {
     override fun <R, D> accept(visitor: ControlFlowGraphVisitor<R, D>, data: D): R {
         return visitor.visitEnterSafeCallNode(this, data)

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/CFGNodeRenderer.kt

@@ -92,9 +92,6 @@ fun CFGNode<*>.render(): String =
                 is AnnotationEnterNode -> "Enter annotation"
                 is AnnotationExitNode -> "Exit annotation"
 
-                is EnterContractNode -> "Enter contract"
-                is ExitContractNode -> "Exit contract"
-
                 is EnterSafeCallNode -> "Enter safe call"
                 is ExitSafeCallNode -> "Exit safe call"
 

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/ControlFlowGraphVisitor.kt

@@ -339,14 +339,6 @@ abstract class ControlFlowGraphVisitor<out R, in D> {
         return visitNode(node, data)
     }
 
-    open fun visitEnterContractNode(node: EnterContractNode, data: D): R {
-        return visitNode(node, data)
-    }
-
-    open fun visitExitContractNode(node: ExitContractNode, data: D): R {
-        return visitNode(node, data)
-    }
-
     open fun visitEnterSafeCallNode(node: EnterSafeCallNode, data: D): R {
         return visitNode(node, data)
     }

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/cfg/ControlFlowGraphVisitorVoid.kt

@@ -273,14 +273,6 @@ abstract class ControlFlowGraphVisitorVoid : ControlFlowGraphVisitor<Unit, Nothi
         visitNode(node)
     }
 
-    open fun visitEnterContractNode(node: EnterContractNode) {
-        visitNode(node)
-    }
-
-    open fun visitExitContractNode(node: ExitContractNode) {
-        visitNode(node)
-    }
-
     open fun visitEnterSafeCallNode(node: EnterSafeCallNode) {
         visitNode(node)
     }
@@ -570,14 +562,6 @@ abstract class ControlFlowGraphVisitorVoid : ControlFlowGraphVisitor<Unit, Nothi
         visitVariableAssignmentNode(node)
     }
 
-    final override fun visitEnterContractNode(node: EnterContractNode, data: Nothing?) {
-        visitEnterContractNode(node)
-    }
-
-    final override fun visitExitContractNode(node: ExitContractNode, data: Nothing?) {
-        visitExitContractNode(node)
-    }
-
     final override fun visitEnterSafeCallNode(node: EnterSafeCallNode, data: Nothing?) {
         visitEnterSafeCallNode(node)
     }

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/contracts.kt

@@ -0,0 +1,80 @@
+/*
+ * Copyright 2010-2022 JetBrains s.r.o. and Kotlin Programming Language contributors.
+ * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
+ */
+
+package org.jetbrains.kotlin.fir.resolve.dfa
+
+import org.jetbrains.kotlin.fir.contracts.description.*
+import org.jetbrains.kotlin.fir.expressions.LogicOperationKind
+import org.jetbrains.kotlin.fir.resolve.substitution.ConeSubstitutor
+import org.jetbrains.kotlin.fir.types.*
+
+fun ConeConstantReference.toOperation(): Operation? = when (this) {
+    ConeConstantReference.WILDCARD -> null
+    ConeConstantReference.NULL -> Operation.EqNull
+    ConeConstantReference.NOT_NULL -> Operation.NotEqNull
+    ConeBooleanConstantReference.TRUE -> Operation.EqTrue
+    ConeBooleanConstantReference.FALSE -> Operation.EqFalse
+    else -> throw IllegalArgumentException("$this can not be transformed to Operation")
+}
+
+// Returns `null` if the statement is always false.
+fun <F : Flow> LogicSystem<F>.approveContractStatement(
+    flow: F,
+    statement: ConeBooleanExpression,
+    arguments: Array<out DataFlowVariable?>, // 0 = receiver (null if doesn't exist)
+    substitutor: ConeSubstitutor?,
+    removeApprovedOrImpossible: Boolean = false,
+): TypeStatements? {
+    fun OperationStatement.approve() =
+        approveOperationStatement(flow, this, removeApprovedOrImpossible)
+
+    fun DataFlowVariable.processEqNull(isEq: Boolean): TypeStatements =
+        OperationStatement(this, if (isEq) Operation.EqNull else Operation.NotEqNull).approve()
+
+    fun ConeBooleanExpression.visit(inverted: Boolean): TypeStatements? = when (this) {
+        is ConeBooleanConstantReference ->
+            if (inverted == (this == ConeBooleanConstantReference.TRUE)) null else mapOf()
+        is ConeLogicalNot -> arg.visit(inverted = !inverted)
+        is ConeIsInstancePredicate ->
+            arguments.getOrNull(arg.parameterIndex + 1)?.let {
+                val isType = inverted == isNegated
+                val substitutedType = substitutor?.substituteOrNull(type) ?: type
+                when {
+                    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()
+                        if (isType && it is RealVariable) {
+                            andForTypeStatements(fromNullability, mapOf(it to (it typeEq substitutedType)))
+                        } else {
+                            fromNullability
+                        }
+                    }
+                }
+            } ?: mapOf()
+        is ConeIsNullPredicate ->
+            arguments.getOrNull(arg.parameterIndex + 1)?.processEqNull(inverted == isNegated) ?: mapOf()
+        is ConeBooleanValueParameterReference ->
+            arguments.getOrNull(parameterIndex + 1)?.let {
+                OperationStatement(it, if (inverted) Operation.EqFalse else Operation.EqTrue).approve()
+            } ?: mapOf()
+        is ConeBinaryLogicExpression -> {
+            val a = left.visit(inverted)
+            val b = right.visit(inverted)
+            val isAnd = inverted != (kind == LogicOperationKind.AND)
+            when {
+                a == null -> b.takeIf { !isAnd } // false || b == b; false && b = false
+                b == null -> a.takeIf { !isAnd } // a || false == a; a && false = false
+                isAnd -> andForTypeStatements(a, b)
+                else -> orForTypeStatements(a, b)
+            }
+        }
+        else -> mapOf()
+    }
+
+    return statement.visit(inverted = false)
+}

compiler/fir/semantics/src/org/jetbrains/kotlin/fir/resolve/dfa/util.kt

@@ -7,8 +7,6 @@ package org.jetbrains.kotlin.fir.resolve.dfa
 
 import kotlinx.collections.immutable.PersistentMap
 import org.jetbrains.kotlin.fir.FirElement
-import org.jetbrains.kotlin.fir.contracts.description.ConeBooleanConstantReference
-import org.jetbrains.kotlin.fir.contracts.description.ConeConstantReference
 import org.jetbrains.kotlin.fir.declarations.FirDeclaration
 import org.jetbrains.kotlin.fir.expressions.*
 import org.jetbrains.kotlin.fir.references.FirResolvedNamedReference
@@ -16,12 +14,8 @@ import org.jetbrains.kotlin.fir.references.FirThisReference
 import org.jetbrains.kotlin.fir.references.impl.FirSimpleNamedReference
 import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol
-import org.jetbrains.kotlin.fir.symbols.impl.FirNamedFunctionSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirSyntheticPropertySymbol
-import org.jetbrains.kotlin.fir.types.ConeKotlinType
+import org.jetbrains.kotlin.fir.types.*
-import org.jetbrains.kotlin.fir.types.ConeTypeContext
-import org.jetbrains.kotlin.fir.types.coneType
-import org.jetbrains.kotlin.name.StandardClassIds
 import kotlin.contracts.ExperimentalContracts
 import kotlin.contracts.InvocationKind
 import kotlin.contracts.contract
@@ -58,9 +52,9 @@ internal inline fun <K, V> PersistentMap<K, V>.put(
     }
 }
 
-fun Set<ConeKotlinType>?.intersectWith(context: ConeTypeContext, originalType: ConeKotlinType): ConeKotlinType =
+fun TypeStatement?.smartCastedType(context: ConeTypeContext, originalType: ConeKotlinType): ConeKotlinType =
-    if (!isNullOrEmpty()) {
+    if (this != null && exactType.isNotEmpty()) {
-        context.intersectTypes(toMutableList().also { it += originalType })
+        context.intersectTypes(exactType.toMutableList().also { it += originalType })
     } else {
         originalType
     }
@@ -74,19 +68,6 @@ fun FirOperation.isEq(): Boolean {
     }
 }
 
-fun FirFunctionCall.isBooleanNot(): Boolean {
-    val symbol = (calleeReference as? FirResolvedNamedReference)?.resolvedSymbol as? FirNamedFunctionSymbol ?: return false
-    return symbol.callableId == StandardClassIds.Callables.not
-}
-
-fun ConeConstantReference.toOperation(): Operation = when (this) {
-    ConeConstantReference.NULL -> Operation.EqNull
-    ConeConstantReference.NOT_NULL -> Operation.NotEqNull
-    ConeBooleanConstantReference.TRUE -> Operation.EqTrue
-    ConeBooleanConstantReference.FALSE -> Operation.EqFalse
-    else -> throw IllegalArgumentException("$this can not be transformed to Operation")
-}
-
 @DfaInternals
 val FirExpression.coneType: ConeKotlinType
     get() = typeRef.coneType