[TS] Handle null == undefined

usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt

@@ -384,7 +384,16 @@ sealed interface TsBinaryOperator {
             rhs: UHeapRef,
             scope: TsStepScope,
         ): UBoolExpr {
-            return mkEq(lhs, rhs)
+            // Note: in JavaScript, `null == undefined`
+            val lhsIsNull = mkEq(lhs, mkTsNullValue())
+            val rhsIsNull = mkEq(rhs, mkTsNullValue())
+            val lhsIsUndefined = mkEq(lhs, mkUndefinedValue())
+            val rhsIsUndefined = mkEq(rhs, mkUndefinedValue())
+            return mkOr(
+                mkAnd(lhsIsUndefined, rhsIsNull),
+                mkAnd(lhsIsNull, rhsIsUndefined),
+                mkHeapRefEq(lhs, rhs)
+            )
         }
 
         override fun TsContext.resolveFakeObject(
@@ -412,42 +421,35 @@ sealed interface TsBinaryOperator {
             if (lhs.sort == boolSort && rhs.sort == boolSort) {
                 val lhs = lhs.asExpr(boolSort)
                 val rhs = rhs.asExpr(boolSort)
-                return mkEq(lhs, rhs)
+                return onBool(lhs, rhs, scope)
             }
 
             // fp == fp
             if (lhs.sort == fp64Sort && rhs.sort == fp64Sort) {
                 val lhs = lhs.asExpr(fp64Sort)
                 val rhs = rhs.asExpr(fp64Sort)
-                return mkFpEqualExpr(lhs, rhs)
+                return onFp(lhs, rhs, scope)
             }
 
             // bool == fp
             if (lhs.sort == boolSort && rhs.sort == fp64Sort) {
                 val lhs = lhs.asExpr(boolSort)
                 val rhs = rhs.asExpr(fp64Sort)
-                return mkFpEqualExpr(boolToFp(lhs), rhs)
+                return onFp(boolToFp(lhs), rhs, scope)
             }
 
             // fp == bool
             if (lhs.sort == fp64Sort && rhs.sort == boolSort) {
                 val lhs = lhs.asExpr(fp64Sort)
                 val rhs = rhs.asExpr(boolSort)
-                return mkFpEqualExpr(lhs, boolToFp(rhs))
+                return onFp(lhs, boolToFp(rhs), scope)
             }
 
             // ref == ref
             if (lhs.sort == addressSort && rhs.sort == addressSort) {
-                // Note:
-                //  undefined == null
-                //  null == undefined
                 val lhs = lhs.asExpr(addressSort)
                 val rhs = rhs.asExpr(addressSort)
-                return mkOr(
-                    mkEq(lhs, rhs),
-                    mkEq(lhs, mkUndefinedValue()) and mkEq(rhs, mkTsNullValue()),
-                    mkEq(lhs, mkTsNullValue()) and mkEq(rhs, mkUndefinedValue()),
-                )
+                return onRef(lhs, rhs, scope)
             }
 
             // bool == ref
@@ -576,7 +578,7 @@ sealed interface TsBinaryOperator {
                         lhsType.boolTypeExpr eq rhsType.boolTypeExpr,
                         lhsType.fpTypeExpr eq rhsType.fpTypeExpr,
                         // TODO support type equality
-                        lhsType.refTypeExpr eq rhsType.refTypeExpr
+                        lhsType.refTypeExpr eq rhsType.refTypeExpr,
                     )
                 }
 
@@ -631,11 +633,27 @@ sealed interface TsBinaryOperator {
                 }
             }
 
-            val loosyEqualityConstraint = with(Eq) {
+            check(!lhsValue.isFakeObject()) { "Nested fake objects are not supported" }
+            check(!rhsValue.isFakeObject()) { "Nested fake objects are not supported" }
+
+            // Note: this is the case 'ref === ref',
+            // which should be `true` only if both have the same reference.
+            // It is not correct to delegate to `Eq.resolve` in this case,
+            // since `==` treats `null == undefined`, while `null !== undefined`.
+            if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) {
+                val left = lhsValue.asExpr(addressSort)
+                val right = rhsValue.asExpr(addressSort)
+                return mkAnd(
+                    typeConstraint,
+                    mkHeapRefEq(left, right)
+                )
+            }
+
+            val looseEqualityConstraint = with(Eq) {
                 resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered")
             }
 
-            return mkAnd(typeConstraint, loosyEqualityConstraint)
+            return mkAnd(typeConstraint, looseEqualityConstraint)
         }
 
         override fun TsContext.internalResolve(

usvm-ts/src/test/kotlin/org/usvm/samples/lang/Null.kt

@@ -1,10 +1,10 @@
 package org.usvm.samples.lang
 
 import org.jacodb.ets.model.EtsScene
-import org.junit.jupiter.api.Test
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.eq
+import kotlin.test.Test
 
 class Null : TsMethodTestRunner() {
     private val tsPath = "/samples/lang/Null.ts"
@@ -16,8 +16,29 @@ class Null : TsMethodTestRunner() {
         val method = getMethod("isNull")
         discoverProperties<TsTestValue, TsTestValue.TsNumber>(
             method,
-            { a, r -> (r eq 1) && (a is TsTestValue.TsNull) },
-            { a, r -> (r eq 2) && (a !is TsTestValue.TsNull) },
+            { a, r ->
+                (r eq 1) && (a is TsTestValue.TsNull)
+            },
+            { a, r ->
+                (r eq 2) && (a !is TsTestValue.TsNull)
+            },
+        )
+    }
+
+    @Test
+    fun `test isNullOrUndefined`() {
+        val method = getMethod("isNullOrUndefined")
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method,
+            { a, r ->
+                (r eq 1) && (a is TsTestValue.TsNull)
+            },
+            { a, r ->
+                (r eq 2) && (a is TsTestValue.TsUndefined)
+            },
+            { a, r ->
+                (r eq 3) && (a !is TsTestValue.TsNull) && (a !is TsTestValue.TsUndefined)
+            },
         )
     }
 }

usvm-ts/src/test/kotlin/org/usvm/samples/lang/Undefined.kt

@@ -24,4 +24,21 @@ class Undefined : TsMethodTestRunner() {
             },
         )
     }
+
+    @Test
+    fun `test isUndefinedOrNull`() {
+        val method = getMethod("isUndefinedOrNull")
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method,
+            { a, r ->
+                (r eq 1) && (a is TsTestValue.TsUndefined)
+            },
+            { a, r ->
+                (r eq 2) && (a is TsTestValue.TsNull)
+            },
+            { a, r ->
+                (r eq 3) && (a !is TsTestValue.TsUndefined) && (a !is TsTestValue.TsNull)
+            },
+        )
+    }
 }

usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt

@@ -133,4 +133,52 @@ class Equality : TsMethodTestRunner() {
             )
         )
     }
+
+    @Test
+    fun `test eqNullWithNull`() {
+        val method = getMethod("eqNullWithNull")
+        discoverProperties<TsTestValue.TsNumber>(
+            method,
+            { r -> r eq 1 },
+            invariants = arrayOf(
+                { r -> r.number > 0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test eqUndefinedWithUndefined`() {
+        val method = getMethod("eqUndefinedWithUndefined")
+        discoverProperties<TsTestValue.TsNumber>(
+            method,
+            { r -> r eq 1 },
+            invariants = arrayOf(
+                { r -> r.number > 0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test eqNullWithUndefined`() {
+        val method = getMethod("eqNullWithUndefined")
+        discoverProperties<TsTestValue.TsNumber>(
+            method,
+            { r -> r eq 1 },
+            invariants = arrayOf(
+                { r -> r.number > 0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test eqUndefinedWithNull`() {
+        val method = getMethod("eqUndefinedWithNull")
+        discoverProperties<TsTestValue.TsNumber>(
+            method,
+            { r -> r eq 1 },
+            invariants = arrayOf(
+                { r -> r.number > 0 },
+            )
+        )
+    }
 }

usvm-ts/src/test/resources/samples/lang/Null.ts

@@ -6,4 +6,13 @@ class Null {
         if (x === null) return 1;
         return 2;
     }
+
+    isNullOrUndefined(x): number {
+        if (x == null) {
+            if (x === null) return 1;
+            if (x === undefined) return 2;
+            return -1; // unreachable
+        }
+        return 3; // not null or undefined
+    }
 }

usvm-ts/src/test/resources/samples/lang/Undefined.ts

@@ -6,4 +6,13 @@ class Undefined {
         if (x === undefined) return 1;
         return 2;
     }
+
+    isUndefinedOrNull(x): number {
+        if (x == undefined) {
+            if (x === undefined) return 1;
+            if (x === null) return 2;
+            return -1; // unreachable
+        }
+        return 3; // not null or undefined
+    }
 }

usvm-ts/src/test/resources/samples/operators/Equality.ts

@@ -1,5 +1,6 @@
 // @ts-nocheck
 // noinspection JSUnusedGlobalSymbols
+// noinspection PointlessBooleanExpressionJS
 
 class Equality {
     eqBoolWithBool(a: boolean): number {
@@ -55,4 +56,24 @@ class Equality {
         if ([42] == false) return -1; // unreachable
         return 0;
     }
+
+    eqNullWithNull(): number {
+        if (null == null) return 1;
+        return -1; // unreachable
+    }
+
+    eqUndefinedWithUndefined(): number {
+        if (undefined == undefined) return 1;
+        return -1; // unreachable
+    }
+
+    eqNullWithUndefined(): number {
+        if (null == undefined) return 1;
+        return -1; // unreachable
+    }
+
+    eqUndefinedWithNull(): number {
+        if (undefined == null) return 1;
+        return -1; // unreachable
+    }
 }