Handle symbolic objects

Author: Lipen

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

@@ -384,10 +384,16 @@ sealed interface TsBinaryOperator {
             rhs: UHeapRef,
             scope: TsStepScope,
         ): UBoolExpr {
-            // Note: in JavaScript, `undefined == null`
-            if (lhs == mkUndefinedValue() && rhs == mkTsNullValue()) return mkTrue()
-            if (lhs == mkTsNullValue() && rhs == mkUndefinedValue()) return mkTrue()
-            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(

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

@@ -181,4 +181,29 @@ class Equality : TsMethodTestRunner() {
             )
         )
     }
+
+    @Test
+    fun `test eqAnyWithNull`() {
+        val method = getMethod("eqAnyWithNull")
+        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 5) && (a !is TsTestValue.TsNull)
+            },
+            { a, r ->
+                (r eq 10) && (a !is TsTestValue.TsNull) && (a !is TsTestValue.TsUndefined)
+            },
+            invariants = arrayOf(
+                { _, r -> r.number > 0 },
+                { a, r -> if (r eq 1) a is TsTestValue.TsNull else true },
+                { a, r -> if (r eq 2) a is TsTestValue.TsUndefined else true },
+            )
+        )
+    }
 }

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

@@ -76,4 +76,28 @@ class Equality {
         if (undefined == null) return 1;
         return -1; // unreachable
     }
+
+    eqAnyWithNull(a: any): number {
+        if (typeof a === "object") {
+            // Note: `a == null` is true when `a` is null or undefined,
+            // but here `a` cannot be undefined because `typeof undefined` is "undefined".
+            // Thus, `a == null` is true only if `a === null`.
+            if (a == null) {
+                if (a === null) return 1; // null
+                return -1; // unreachable
+            }
+            return 5; // non-null object
+        }
+        if (typeof a === "undefined") {
+            // Note: `a == null` is true when `a` is null or undefined,
+            // but here `a` cannot be null because `typeof null` is "object".
+            // Thus, `a == null` is true only if `a === undefined`.
+            if (a == null) {
+                if (a === undefined) return 2; // undefined
+                return -1; // unreachable
+            }
+            return -1; // unreachable
+        }
+        return 100; // non-object, non-undefined
+    }
 }