[FIR] Add ReturnsImplies effect analyzer

2020-08-11 12:41:43 +03:00
parent 3454ae7ca4
commit 21b8679799
37 changed files with 1110 additions and 89 deletions
@@ -0,0 +1,35 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun foo(x: String?): Any? {
+    <!WRONG_IMPLIES_CONDITION!>contract {
+        returns(null) implies (x != null)
+    }<!>
+
+    if (true) {
+        throw java.lang.IllegalArgumentException()
+    }
+
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun bar(x: String?): Any? {
+    <!WRONG_IMPLIES_CONDITION!>contract {
+        returns() implies (x != null)
+    }<!>
+
+    if (x == null) {
+        return x
+    }
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun baz(x: String?): Any? {
+    <!WRONG_IMPLIES_CONDITION!>contract {
+        returns(null) implies (x != null)
+    }<!>
+
+    return x
+}
@@ -0,0 +1,40 @@
+FILE: notNull.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun foo(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        when () {
+            Boolean(true) ->  {
+                throw Q|java/lang|.R|java/lang/IllegalArgumentException.IllegalArgumentException|()
+            }
+        }
+
+        ^foo R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun bar(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(WILDCARD) -> x != null
+        >
+     {
+        [StubStatement]
+        when () {
+            ==(R|<local>/x|, Null(null)) ->  {
+                ^bar R|<local>/x|
+            }
+        }
+
+        ^bar R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun baz(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^baz R|<local>/x|
+    }
@@ -0,0 +1,18 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun Any?.isNotNull(): Boolean {
+    contract {
+        returns(true) implies (this@isNotNull != null)
+    }
+    return this != null
+}
+
+@OptIn(ExperimentalContracts::class)
+val Any?.isNotNull: Boolean
+    get() {
+        <!WRONG_IMPLIES_CONDITION!>contract {
+            returns(true) implies (this@isNotNull != null)
+        }<!>
+        return this@isNotNull != null
+    }
@@ -0,0 +1,20 @@
+FILE: propertyGetter.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun R|kotlin/Any?|.isNotNull(): R|kotlin/Boolean|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> this != null
+        >
+     {
+        [StubStatement]
+        ^isNotNull !=(this@R|/isNotNull|, Null(null))
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final val R|kotlin/Any?|.isNotNull: R|kotlin/Boolean|
+        public get(): R|kotlin/Boolean|
+            [R|Contract description]
+             <
+                Returns(TRUE) -> this != null
+            >
+         {
+            [StubStatement]
+            ^ !=(this@R|/isNotNull|, Null(null))
+        }
@@ -0,0 +1,121 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun test1(x: String?): Any? {
+    contract {
+        returnsNotNull() implies (!(x == null))
+    }
+
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test2(x: String?): Any? {
+    contract {
+        returnsNotNull() implies (x is String && x != null)
+    }
+
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test3(x: String?): Any? {
+    contract {
+        returnsNotNull() implies (x is String? || x is Any?)
+    }
+
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test4(x: String?, y: String?): Any? {
+    contract {
+        returns(true) implies (x != null && y != null)
+    }
+
+    return x != null && y != null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test5(x: Any?): Any? {
+    contract {
+        returns(true) implies (x != null || x is Any)
+    }
+
+    return x != null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test6(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is String? && x != null)
+    }
+
+    return x is String
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test7(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is String? && x != null || x is Int)
+    }
+
+    return x is String
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test8(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is String || x is Int)
+    }
+
+    return x is String || x is Int
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test9(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is String || x is Int)
+    }
+
+    if(x is String){
+        return true
+    }
+    return x is Int
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test10(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is Comparable<*> || x is CharSequence)
+    }
+
+    return x is String
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test11(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is Comparable<*> && x is CharSequence)
+    }
+
+    return x is String
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test12(x: Any?): Any? {
+    contract {
+        returns(true) implies (x is Comparable<*> && (x is CharSequence || x is Number))
+    }
+
+    return x is String || x is Int
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test13(x: Any?): Any? {
+    contract {
+        returns(true) implies (!(x !is Comparable<*> || (x !is CharSequence && !(x is Number))))
+    }
+
+    return x is String || x is Int
+}
@@ -0,0 +1,118 @@
+FILE: conditionLogic.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test1(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> !x == null
+        >
+     {
+        [StubStatement]
+        ^test1 R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test2(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test2 R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test3(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x is kotlin/String? || x is kotlin/Any?
+        >
+     {
+        [StubStatement]
+        ^test3 R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test4(x: R|kotlin/String?|, y: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null && y != null
+        >
+     {
+        [StubStatement]
+        ^test4 !=(R|<local>/x|, Null(null)) && !=(R|<local>/y|, Null(null))
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test5(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null || x is kotlin/Any
+        >
+     {
+        [StubStatement]
+        ^test5 !=(R|<local>/x|, Null(null))
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test6(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test6 (R|<local>/x| is R|kotlin/String|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test7(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test7 (R|<local>/x| is R|kotlin/String|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test8(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x is kotlin/String || x is kotlin/Int
+        >
+     {
+        [StubStatement]
+        ^test8 (R|<local>/x| is R|kotlin/String|) || (R|<local>/x| is R|kotlin/Int|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test9(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x is kotlin/String || x is kotlin/Int
+        >
+     {
+        [StubStatement]
+        when () {
+            (R|<local>/x| is R|kotlin/String|) ->  {
+                ^test9 Boolean(true)
+            }
+        }
+
+        ^test9 (R|<local>/x| is R|kotlin/Int|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test10(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x is kotlin/Comparable<*> || x is kotlin/CharSequence
+        >
+     {
+        [StubStatement]
+        ^test10 (R|<local>/x| is R|kotlin/String|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test11(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test11 (R|<local>/x| is R|kotlin/String|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test12(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test12 (R|<local>/x| is R|kotlin/String|) || (R|<local>/x| is R|kotlin/Int|)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test13(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+        >
+     {
+        [StubStatement]
+        ^test13 (R|<local>/x| is R|kotlin/String|) || (R|<local>/x| is R|kotlin/Int|)
+    }
@@ -0,0 +1,57 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun wrongFalse(x: String?): Boolean {
+    contract {
+        returns(false) implies (x != null)
+    }
+
+    return true
+}
+
+@OptIn(ExperimentalContracts::class)
+fun wrongTrue(x: String?): Boolean {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    return false
+}
+
+@OptIn(ExperimentalContracts::class)
+fun nullableConstant(x: String?): Any? {
+    contract {
+        returns(null) implies (x != null)
+    }
+
+    return 1
+}
+
+fun string() : String = ""
+
+@OptIn(ExperimentalContracts::class)
+fun nullableReturn(x: String?): Any? {
+    contract {
+        returns(null) implies (x != null)
+    }
+
+    return string()
+}
+
+@OptIn(ExperimentalContracts::class)
+fun returnsNull(x: String?): Any? {
+    contract {
+        returnsNotNull() implies (x != null)
+    }
+
+    return null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun wrongReturnType(x: String?): Any? {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    return "true"
+}
@@ -0,0 +1,58 @@
+FILE: inapplicable.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun wrongFalse(x: R|kotlin/String?|): R|kotlin/Boolean|
+        [R|Contract description]
+         <
+            Returns(FALSE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^wrongFalse Boolean(true)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun wrongTrue(x: R|kotlin/String?|): R|kotlin/Boolean|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^wrongTrue Boolean(false)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun nullableConstant(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^nullableConstant Int(1)
+    }
+    public final fun string(): R|kotlin/String| {
+        ^string String()
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun nullableReturn(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^nullableReturn R|/string|()
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun returnsNull(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^returnsNull Null(null)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun wrongReturnType(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^wrongReturnType String(true)
+    }
@@ -0,0 +1,56 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun test1(x: String?): Boolean {
+    contract {
+        returns(false) implies (x != null)
+    }
+
+    return x == null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test2(x: String?): Boolean {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    return x != null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test3(x: String?): Any? {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    if(x != null){
+        return true
+    }
+
+    return false
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test4(x: String?): Any? {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    val y = x
+
+    if(y != null){
+        return true
+    }
+
+    return false
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test5(x: String?): Any? {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    return test2(x)
+}
@@ -0,0 +1,59 @@
+FILE: notNull.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test1(x: R|kotlin/String?|): R|kotlin/Boolean|
+        [R|Contract description]
+         <
+            Returns(FALSE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test1 ==(R|<local>/x|, Null(null))
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test2(x: R|kotlin/String?|): R|kotlin/Boolean|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test2 !=(R|<local>/x|, Null(null))
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test3(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        when () {
+            !=(R|<local>/x|, Null(null)) ->  {
+                ^test3 Boolean(true)
+            }
+        }
+
+        ^test3 Boolean(false)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test4(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        lval y: R|kotlin/String?| = R|<local>/x|
+        when () {
+            !=(R|<local>/y|, Null(null)) ->  {
+                ^test4 Boolean(true)
+            }
+        }
+
+        ^test4 Boolean(false)
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test5(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test5 R|/test2|(R|<local>/x|)
+    }
@@ -6,16 +6,16 @@ interface A {

 var Any?.isNotNull: Boolean
    get() {
-        contract {
+        <!WRONG_IMPLIES_CONDITION!>contract {
            returns(true) implies (this@isNotNull != null)
-        }
+        }<!>
        return this != null
    }
    set(value) {
-        contract {
+        <!WRONG_IMPLIES_CONDITION!>contract {
            returns() implies (this@isNotNull != null)
            require(this != null)
-        }
+        }<!>
    }

 fun test_1(a: A?) {
@@ -0,0 +1,19 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun test1(x: String?): Int? {
+    contract {
+        returnsNotNull() implies (x != null)
+    }
+
+    return x?.length
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test2(x: String?): Int? {
+    <!WRONG_IMPLIES_CONDITION!>contract {
+        returnsNotNull() implies (x is Boolean)
+    }<!>
+
+    return x?.length
+}
@@ -0,0 +1,19 @@
+FILE: safeCall.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test1(x: R|kotlin/String?|): R|kotlin/Int?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test1 R|<local>/x|?.{ $subj$.R|kotlin/String.length| }
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test2(x: R|kotlin/String?|): R|kotlin/Int?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x is kotlin/Boolean
+        >
+     {
+        [StubStatement]
+        ^test2 R|<local>/x|?.{ $subj$.R|kotlin/String.length| }
+    }
@@ -0,0 +1,39 @@
+import kotlin.contracts.*
+
+@OptIn(ExperimentalContracts::class)
+fun test1(x: String?): Any? {
+    contract {
+        returnsNotNull() implies (x != null)
+    }
+
+    return x
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test2(x: String?): Any? {
+    contract {
+        returns(true) implies (x != null)
+    }
+
+    return if(x != null) true else false
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test3(x: Any?): Any? {
+    contract {
+        returnsNotNull() implies (x != null)
+    }
+    return if(true) x else null
+}
+
+@OptIn(ExperimentalContracts::class)
+fun test4(x: Any?): Any? {
+    contract {
+        returnsNotNull() implies (x != null)
+    }
+    return if(x != null) {
+        if (true) x else false
+    } else {
+        null
+    }
+}
@@ -0,0 +1,69 @@
+FILE: trickyCases.kt
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test1(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test1 R|<local>/x|
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test2(x: R|kotlin/String?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(TRUE) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test2 when () {
+            !=(R|<local>/x|, Null(null)) ->  {
+                Boolean(true)
+            }
+            else ->  {
+                Boolean(false)
+            }
+        }
+
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test3(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test3 when () {
+            Boolean(true) ->  {
+                R|<local>/x|
+            }
+            else ->  {
+                Null(null)
+            }
+        }
+
+    }
+    @R|kotlin/OptIn|(vararg(<getClass>(Q|kotlin/contracts/ExperimentalContracts|))) public final fun test4(x: R|kotlin/Any?|): R|kotlin/Any?|
+        [R|Contract description]
+         <
+            Returns(NOT_NULL) -> x != null
+        >
+     {
+        [StubStatement]
+        ^test4 when () {
+            !=(R|<local>/x|, Null(null)) ->  {
+                when () {
+                    Boolean(true) ->  {
+                        R|<local>/x|
+                    }
+                    else ->  {
+                        Boolean(false)
+                    }
+                }
+
+            }
+            else ->  {
+                Null(null)
+            }
+        }
+
+    }
@@ -590,6 +590,29 @@ public class FirDiagnosticsWithStdlibTestGenerated extends AbstractFirDiagnostic
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/bad/callsInPlace/toLocalVariables.kt");
                    }
                }
+
+                @TestMetadata("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/bad/returnsImplies")
+                @TestDataPath("$PROJECT_ROOT")
+                @RunWith(JUnit3RunnerWithInners.class)
+                public static class ReturnsImplies extends AbstractFirDiagnosticsWithStdlibTest {
+                    private void runTest(String testDataFilePath) throws Exception {
+                        KotlinTestUtils.runTest(this::doTest, this, testDataFilePath);
+                    }
+
+                    public void testAllFilesPresentInReturnsImplies() throws Exception {
+                        KotlinTestUtils.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/bad/returnsImplies"), Pattern.compile("^([^.]+)\\.kt$"), null, true);
+                    }
+
+                    @TestMetadata("notNull.kt")
+                    public void testNotNull() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/bad/returnsImplies/notNull.kt");
+                    }
+
+                    @TestMetadata("propertyGetter.kt")
+                    public void testPropertyGetter() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/bad/returnsImplies/propertyGetter.kt");
+                    }
+                }
            }

            @TestMetadata("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good")
@@ -674,16 +697,31 @@ public class FirDiagnosticsWithStdlibTestGenerated extends AbstractFirDiagnostic
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/booleanOperators.kt");
                    }

+                    @TestMetadata("conditionLogic.kt")
+                    public void testConditionLogic() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/conditionLogic.kt");
+                    }
+
                    @TestMetadata("eqNotEq.kt")
                    public void testEqNotEq() throws Exception {
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/eqNotEq.kt");
                    }

+                    @TestMetadata("inapplicable.kt")
+                    public void testInapplicable() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/inapplicable.kt");
+                    }
+
                    @TestMetadata("namedArguments.kt")
                    public void testNamedArguments() throws Exception {
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/namedArguments.kt");
                    }

+                    @TestMetadata("notNull.kt")
+                    public void testNotNull() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/notNull.kt");
+                    }
+
                    @TestMetadata("propertyAccessors.kt")
                    public void testPropertyAccessors() throws Exception {
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/propertyAccessors.kt");
@@ -694,6 +732,16 @@ public class FirDiagnosticsWithStdlibTestGenerated extends AbstractFirDiagnostic
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/receivers.kt");
                    }

+                    @TestMetadata("safeCall.kt")
+                    public void testSafeCall() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/safeCall.kt");
+                    }
+
+                    @TestMetadata("trickyCases.kt")
+                    public void testTrickyCases() throws Exception {
+                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/trickyCases.kt");
+                    }
+
                    @TestMetadata("typePredicate.kt")
                    public void testTypePredicate() throws Exception {
                        runTest("compiler/fir/analysis-tests/testData/resolveWithStdlib/contracts/fromSource/good/returnsImplies/typePredicate.kt");
@@ -0,0 +1,212 @@
+/*
+ * Copyright 2010-2020 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.analysis.cfa
+
+import org.jetbrains.kotlin.fir.BuiltinTypes
+import org.jetbrains.kotlin.fir.FirSession
+import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker
+import org.jetbrains.kotlin.fir.analysis.diagnostics.DiagnosticReporter
+import org.jetbrains.kotlin.fir.analysis.diagnostics.FirErrors
+import org.jetbrains.kotlin.fir.contracts.FirResolvedContractDescription
+import org.jetbrains.kotlin.fir.contracts.description.*
+import org.jetbrains.kotlin.fir.declarations.FirContractDescriptionOwner
+import org.jetbrains.kotlin.fir.declarations.FirFunction
+import org.jetbrains.kotlin.fir.expressions.*
+import org.jetbrains.kotlin.fir.resolve.dfa.*
+import org.jetbrains.kotlin.fir.resolve.dfa.cfg.BlockExitNode
+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.AbstractFirBasedSymbol
+import org.jetbrains.kotlin.fir.typeContext
+import org.jetbrains.kotlin.fir.types.*
+import org.jetbrains.kotlin.types.AbstractTypeChecker
+import org.jetbrains.kotlin.types.model.KotlinTypeMarker
+import org.jetbrains.kotlin.types.model.TypeCheckerProviderContext
+import org.jetbrains.kotlin.utils.addIfNotNull
+
+object FirReturnsImpliesAnalyzer : FirControlFlowChecker() {
+
+    override fun analyze(graph: ControlFlowGraph, reporter: DiagnosticReporter) {
+        val function = graph.declaration as? FirFunction<*> ?: return
+        val graphRef = function.controlFlowGraphReference as FirControlFlowGraphReferenceImpl
+        val dataFlowInfo = graphRef.dataFlowInfo
+        if (function !is FirContractDescriptionOwner || dataFlowInfo == null) return
+
+        val effects = (function.contractDescription as? FirResolvedContractDescription)?.effects
+            ?.filter { it is ConeConditionalEffectDeclaration && it.effect is ConeReturnsEffectDeclaration }
+
+        if (effects.isNullOrEmpty()) return
+
+        val logicSystem = object : PersistentLogicSystem(function.session.typeContext) {
+            override fun processUpdatedReceiverVariable(flow: PersistentFlow, variable: RealVariable) =
+                throw IllegalStateException("Receiver variable update is not possible for this logic system")
+
+            override fun updateAllReceivers(flow: PersistentFlow) =
+                throw IllegalStateException("Update of all receivers is not possible for this logic system")
+        }
+
+        effects.forEach { effect ->
+            val wrongCondition = graph.exitNode.previousCfgNodes.any {
+                isWrongConditionOnNode(it, effect as ConeConditionalEffectDeclaration, function, logicSystem, dataFlowInfo)
+            }
+
+            if (wrongCondition) {
+                function.contractDescription.source?.let {
+                    reporter.report(FirErrors.WRONG_IMPLIES_CONDITION.on(it))
+                }
+            }
+        }
+    }
+
+    private fun isWrongConditionOnNode(
+        node: CFGNode<*>,
+        effectDeclaration: ConeConditionalEffectDeclaration,
+        function: FirFunction<*>,
+        logicSystem: LogicSystem<PersistentFlow>,
+        dataFlowInfo: DataFlowInfo
+    ): Boolean {
+        val effect = effectDeclaration.effect as ConeReturnsEffectDeclaration
+        val builtinTypes = function.session.builtinTypes
+        val typeContext = function.session.typeContext
+        val flow = dataFlowInfo.flowOnNodes.getValue(node) as PersistentFlow
+
+        val isReturn = node is JumpNode && node.fir is FirReturnExpression
+        val resultExpression = if (isReturn) (node.fir as FirReturnExpression).result else node.fir
+
+        val expressionType = (resultExpression as? FirExpression)?.typeRef?.coneType
+        if (expressionType == builtinTypes.nothingType.type) return false
+
+        if (isReturn && resultExpression is FirWhenExpression) {
+            return node.collectBranchExits().any {
+                isWrongConditionOnNode(it, effectDeclaration, function, logicSystem, dataFlowInfo)
+            }
+        }
+
+        var typeStatements: TypeStatements = flow.approvedTypeStatements
+
+        if (effect.value != ConeConstantReference.WILDCARD) {
+            val operation = effect.value.toOperation()
+            if (expressionType != null && expressionType.isInapplicableWith(operation, function.session)) return false
+
+            if (resultExpression is FirConstExpression<*>) {
+                if (!resultExpression.isApplicableWith(operation)) return false
+            } else {
+                val resultVar = dataFlowInfo.variableStorage.getOrCreateVariable(flow, resultExpression)
+                typeStatements = logicSystem.approveOperationStatement(flow, OperationStatement(resultVar, operation), builtinTypes)
+            }
+        }
+
+        val conditionStatements =
+            effectDeclaration.condition.buildTypeStatements(function, logicSystem, dataFlowInfo.variableStorage, flow) ?: return false
+
+        for ((realVar, requiredTypeStatement) in conditionStatements) {
+            val fixedRealVar = typeStatements.keys.find { it.identifier == realVar.identifier } ?: realVar
+            val resultTypeStatement = typeStatements[fixedRealVar]
+
+            val resultType = mutableListOf<ConeKotlinType>().apply {
+                addIfNotNull(function.getParameterType(fixedRealVar.identifier.symbol))
+                if (resultTypeStatement != null) addAll(resultTypeStatement.exactType)
+            }.let { typeContext.intersectTypesOrNull(it) }
+
+            val requiredType = typeContext.intersectTypesOrNull(requiredTypeStatement.exactType.toList())
+            if (requiredType != null && !requiredType.isSupertypeOf(typeContext, resultType)) return true
+        }
+        return false
+    }
+
+    private fun LogicSystem<PersistentFlow>.approveOperationStatement(
+        flow: PersistentFlow,
+        statement: OperationStatement,
+        builtinTypes: BuiltinTypes
+    ): MutableTypeStatements {
+        val newTypeStatements: MutableTypeStatements = mutableMapOf()
+
+        approveStatementsTo(newTypeStatements, flow, statement, flow.logicStatements.flatMap { it.value })
+        newTypeStatements.mergeTypeStatements(flow.approvedTypeStatements)
+
+        val variable = statement.variable
+        if (variable.isReal()) {
+            if (statement.operation == Operation.NotEqNull) {
+                newTypeStatements.addStatement(variable, simpleTypeStatement(variable, true, builtinTypes.anyType.type))
+            } else if (statement.operation == Operation.EqNull) {
+                newTypeStatements.addStatement(variable, simpleTypeStatement(variable, false, builtinTypes.anyType.type))
+            }
+        }
+
+        return newTypeStatements
+    }
+
+    private fun ConeBooleanExpression.buildTypeStatements(
+        function: FirFunction<*>,
+        logicSystem: LogicSystem<*>,
+        variableStorage: VariableStorage,
+        flow: Flow
+    ): MutableTypeStatements? = when (this) {
+        is ConeBinaryLogicExpression -> {
+            val left = left.buildTypeStatements(function, logicSystem, variableStorage, flow)
+            val right = right.buildTypeStatements(function, logicSystem, variableStorage, flow)
+            if (left != null && right != null) {
+                if (kind == LogicOperationKind.AND) {
+                    left.apply { mergeTypeStatements(right) }
+                } else logicSystem.orForTypeStatements(left, right)
+            } else (left ?: right)
+        }
+        is ConeIsInstancePredicate -> {
+            val fir = function.getParameterSymbol(arg.parameterIndex).fir
+            val realVar = variableStorage.getOrCreateRealVariable(flow, fir.symbol, fir)
+            realVar?.to(simpleTypeStatement(realVar, !isNegated, type))?.let { mutableMapOf(it) }
+        }
+        is ConeIsNullPredicate -> {
+            val fir = function.getParameterSymbol(arg.parameterIndex).fir
+            val realVar = variableStorage.getOrCreateRealVariable(flow, fir.symbol, fir)
+            realVar?.to(simpleTypeStatement(realVar, isNegated, function.session.builtinTypes.anyType.type))?.let { mutableMapOf(it) }
+        }
+        is ConeLogicalNot -> arg.buildTypeStatements(function, logicSystem, variableStorage, flow)
+            ?.mapValuesTo(mutableMapOf()) { (_, value) -> value.invert() }
+
+        else -> null
+    }
+
+    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 {
+        kind == FirConstKind.Null -> operation == Operation.EqNull
+        kind == FirConstKind.Boolean && operation == Operation.EqTrue -> (value as Boolean)
+        kind == FirConstKind.Boolean && operation == Operation.EqFalse -> !(value as Boolean)
+        else -> true
+    }
+
+    fun KotlinTypeMarker.isSupertypeOf(context: TypeCheckerProviderContext, type: KotlinTypeMarker?) =
+        type != null && AbstractTypeChecker.isSubtypeOf(context, type, this)
+
+    private fun simpleTypeStatement(realVar: RealVariable, exactType: Boolean, type: ConeKotlinType): MutableTypeStatement {
+        return MutableTypeStatement(
+            realVar,
+            if (exactType) linkedSetOf(type) else linkedSetOf(),
+            if (!exactType) linkedSetOf(type) else linkedSetOf()
+        )
+    }
+
+    private fun CFGNode<*>.collectBranchExits(nodes: MutableList<CFGNode<*>> = mutableListOf()): List<CFGNode<*>> {
+        if (this is BlockExitNode) {
+            nodes += previousCfgNodes
+        } else previousCfgNodes.forEach { it.collectBranchExits(nodes) }
+        return nodes
+    }
+
+    private fun FirFunction<*>.getParameterType(symbol: AbstractFirBasedSymbol<*>): ConeKotlinType? {
+        return (if (this.symbol == symbol) receiverTypeRef else valueParameters.find { it.symbol == symbol }?.returnTypeRef)?.coneType
+    }
+
+    private fun FirFunction<*>.getParameterSymbol(index: Int): AbstractFirBasedSymbol<*> {
+        return if (index == -1) this.symbol else this.valueParameters[index].symbol
+    }
+}
@@ -7,6 +7,7 @@ package org.jetbrains.kotlin.fir.analysis.checkers.declaration

 import org.jetbrains.kotlin.fir.analysis.cfa.FirCallsEffectAnalyzer
 import org.jetbrains.kotlin.fir.analysis.cfa.FirPropertyInitializationAnalyzer
+import org.jetbrains.kotlin.fir.analysis.cfa.FirReturnsImpliesAnalyzer
 import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker

 object CommonDeclarationCheckers : DeclarationCheckers() {
@@ -42,6 +43,7 @@ object CommonDeclarationCheckers : DeclarationCheckers() {

    override val controlFlowAnalyserCheckers: List<FirControlFlowChecker> = listOf(
        FirPropertyInitializationAnalyzer,
-        FirCallsEffectAnalyzer
+        FirCallsEffectAnalyzer,
+        FirReturnsImpliesAnalyzer
    )
 }
@@ -8,7 +8,6 @@ package org.jetbrains.kotlin.fir.analysis.diagnostics
 import org.jetbrains.kotlin.diagnostics.rendering.DefaultErrorMessages
 import org.jetbrains.kotlin.diagnostics.rendering.DiagnosticFactoryToRendererMap
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirDiagnosticRenderers.DECLARATION_NAME
-import org.jetbrains.kotlin.fir.analysis.diagnostics.FirDiagnosticRenderers.FIR
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirDiagnosticRenderers.NULLABLE_STRING
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirDiagnosticRenderers.PROPERTY_NAME
 import org.jetbrains.kotlin.fir.analysis.diagnostics.FirDiagnosticRenderers.SYMBOL
@@ -255,7 +254,7 @@ class FirDefaultErrorMessages : DefaultErrorMessages.Extension {
                TO_STRING
            )
            map.put(LEAKED_IN_PLACE_LAMBDA, "Leaked in-place lambda: {2}", SYMBOL)
-
+            map.put(FirErrors.WRONG_IMPLIES_CONDITION, "Wrong implies condition")

            // Extended checkers group
 //            map.put(REDUNDANT_VISIBILITY_MODIFIER, ...) // &
@@ -131,6 +131,7 @@ object FirErrors {
    val UNINITIALIZED_VARIABLE by error1<FirSourceElement, PsiElement, FirPropertySymbol>()
    val WRONG_INVOCATION_KIND by warning3<FirSourceElement, PsiElement, AbstractFirBasedSymbol<*>, EventOccurrencesRange, EventOccurrencesRange>()
    val LEAKED_IN_PLACE_LAMBDA by error1<FirSourceElement, PsiElement, AbstractFirBasedSymbol<*>>()
+    val WRONG_IMPLIES_CONDITION by error0<FirSourceElement, PsiElement>()

    // Extended checkers group
    val REDUNDANT_VISIBILITY_MODIFIER by warning0<FirSourceElement, PsiElement>()
@@ -177,7 +177,7 @@ class MutableTypeStatement(
    override val isEmpty: Boolean
        get() = exactType.isEmpty() && exactType.isEmpty()

-    override fun invert(): TypeStatement {
+    override fun invert(): MutableTypeStatement {
        return MutableTypeStatement(
            variable,
            LinkedHashSet(exactNotType),
@@ -79,7 +79,7 @@ internal fun FirFunctionCall.isBooleanNot(): Boolean {
    return symbol.callableId == FirDataFlowAnalyzer.KOTLIN_BOOLEAN_NOT
 }

-internal fun ConeConstantReference.toOperation(): Operation = when (this) {
+fun ConeConstantReference.toOperation(): Operation = when (this) {
    ConeConstantReference.NULL -> Operation.EqNull
    ConeConstantReference.NOT_NULL -> Operation.NotEqNull
    ConeBooleanConstantReference.TRUE -> Operation.EqTrue