Fix strict equality for null and undefined

Author: Lipen

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

@@ -421,28 +421,28 @@ 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
@@ -578,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,
                     )
                 }
 
@@ -633,11 +633,23 @@ sealed interface TsBinaryOperator {
                 }
             }
 
-            val loosyEqualityConstraint = with(Eq) {
+            check(!lhsValue.isFakeObject())
+            check(!rhsValue.isFakeObject())
+
+            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/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
+    }
 }