From 28290b4dad3a2dc9c8431111ad3432de35f87054 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 5 Sep 2025 17:37:59 +0300 Subject: [PATCH 1/8] Handle null == undefined --- .../usvm/machine/operator/TsBinaryOperator.kt | 3 ++ .../org/usvm/samples/operators/Equality.kt | 48 +++++++++++++++++++ .../resources/samples/operators/Equality.ts | 21 ++++++++ 3 files changed, 72 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 8bb49d2ef1..43ae22cf53 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -384,6 +384,9 @@ 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) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt index e9980a2f75..fc7b2f7bcb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt +++ b/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( + method, + { r -> r eq 1 }, + invariants = arrayOf( + { r -> r.number > 0 }, + ) + ) + } + + @Test + fun `test eqUndefinedWithUndefined`() { + val method = getMethod("eqUndefinedWithUndefined") + discoverProperties( + method, + { r -> r eq 1 }, + invariants = arrayOf( + { r -> r.number > 0 }, + ) + ) + } + + @Test + fun `test eqNullWithUndefined`() { + val method = getMethod("eqNullWithUndefined") + discoverProperties( + method, + { r -> r eq 1 }, + invariants = arrayOf( + { r -> r.number > 0 }, + ) + ) + } + + @Test + fun `test eqUndefinedWithNull`() { + val method = getMethod("eqUndefinedWithNull") + discoverProperties( + method, + { r -> r eq 1 }, + invariants = arrayOf( + { r -> r.number > 0 }, + ) + ) + } } diff --git a/usvm-ts/src/test/resources/samples/operators/Equality.ts b/usvm-ts/src/test/resources/samples/operators/Equality.ts index 3a94994a05..05a5d907a7 100644 --- a/usvm-ts/src/test/resources/samples/operators/Equality.ts +++ b/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 + } } From 5b522435387f0ed65cb610f0386485f698356eeb Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Fri, 5 Sep 2025 18:16:51 +0300 Subject: [PATCH 2/8] Handle symbolic objects --- .../usvm/machine/operator/TsBinaryOperator.kt | 14 ++++++++--- .../org/usvm/samples/operators/Equality.kt | 25 +++++++++++++++++++ .../resources/samples/operators/Equality.ts | 24 ++++++++++++++++++ 3 files changed, 59 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 43ae22cf53..9fba5fbfca 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/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( diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt index fc7b2f7bcb..db5c666f36 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt +++ b/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( + 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 }, + ) + ) + } } diff --git a/usvm-ts/src/test/resources/samples/operators/Equality.ts b/usvm-ts/src/test/resources/samples/operators/Equality.ts index 05a5d907a7..be83f31c18 100644 --- a/usvm-ts/src/test/resources/samples/operators/Equality.ts +++ b/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 + } } From 5d6d1da20303b14859dfb41004dded14264ea341 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 12:39:46 +0300 Subject: [PATCH 3/8] Unify --- .../org/usvm/machine/operator/TsBinaryOperator.kt | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 9fba5fbfca..b343e80439 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -447,15 +447,17 @@ sealed interface TsBinaryOperator { // ref == ref if (lhs.sort == addressSort && rhs.sort == addressSort) { - // Note: - // undefined == null - // null == undefined + // Note: in JavaScript, `null == undefined` val lhs = lhs.asExpr(addressSort) val rhs = rhs.asExpr(addressSort) + val lhsIsNull = mkEq(lhs, mkTsNullValue()) + val rhsIsNull = mkEq(rhs, mkTsNullValue()) + val lhsIsUndefined = mkEq(lhs, mkUndefinedValue()) + val rhsIsUndefined = mkEq(rhs, mkUndefinedValue()) return mkOr( - mkEq(lhs, rhs), - mkEq(lhs, mkUndefinedValue()) and mkEq(rhs, mkTsNullValue()), - mkEq(lhs, mkTsNullValue()) and mkEq(rhs, mkUndefinedValue()), + mkAnd(lhsIsUndefined, rhsIsNull), + mkAnd(lhsIsNull, rhsIsUndefined), + mkHeapRefEq(lhs, rhs) ) } From dcd2933825ca6499794a232ab556a109a87a01c9 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 12:40:44 +0300 Subject: [PATCH 4/8] Reuse onRef --- .../org/usvm/machine/operator/TsBinaryOperator.kt | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index b343e80439..0c4927d73e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -447,18 +447,9 @@ sealed interface TsBinaryOperator { // ref == ref if (lhs.sort == addressSort && rhs.sort == addressSort) { - // Note: in JavaScript, `null == undefined` val lhs = lhs.asExpr(addressSort) val rhs = rhs.asExpr(addressSort) - 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) - ) + return onRef(lhs, rhs, scope) } // bool == ref From fd05b024388e5f849ee222979d9e551ce8b77538 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 13:41:09 +0300 Subject: [PATCH 5/8] Remove failing test Unfixable due to the lack of support for typeof operator --- .../org/usvm/samples/operators/Equality.kt | 25 ------------------- .../resources/samples/operators/Equality.ts | 24 ------------------ 2 files changed, 49 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt index db5c666f36..fc7b2f7bcb 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Equality.kt @@ -181,29 +181,4 @@ class Equality : TsMethodTestRunner() { ) ) } - - @Test - fun `test eqAnyWithNull`() { - val method = getMethod("eqAnyWithNull") - discoverProperties( - 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 }, - ) - ) - } } diff --git a/usvm-ts/src/test/resources/samples/operators/Equality.ts b/usvm-ts/src/test/resources/samples/operators/Equality.ts index be83f31c18..05a5d907a7 100644 --- a/usvm-ts/src/test/resources/samples/operators/Equality.ts +++ b/usvm-ts/src/test/resources/samples/operators/Equality.ts @@ -76,28 +76,4 @@ 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 - } } From 3639bfb7a8f733f07f3cc3c98253698d233a3765 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 13:42:04 +0300 Subject: [PATCH 6/8] Fix strict equality for null and undefined --- .../usvm/machine/operator/TsBinaryOperator.kt | 26 +++++++++++++----- .../test/kotlin/org/usvm/samples/lang/Null.kt | 27 ++++++++++++++++--- .../kotlin/org/usvm/samples/lang/Undefined.kt | 17 ++++++++++++ .../src/test/resources/samples/lang/Null.ts | 9 +++++++ .../test/resources/samples/lang/Undefined.ts | 9 +++++++ 5 files changed, 78 insertions(+), 10 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 0c4927d73e..4a5ee9f9b0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/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( diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Null.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Null.kt index 1ca672f9dd..f5913d5d37 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Null.kt +++ b/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( 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( + 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) + }, ) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Undefined.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Undefined.kt index ad2e0768ac..a33bad0d94 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Undefined.kt +++ b/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( + 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) + }, + ) + } } diff --git a/usvm-ts/src/test/resources/samples/lang/Null.ts b/usvm-ts/src/test/resources/samples/lang/Null.ts index dd18bedfb8..bd54e7229f 100644 --- a/usvm-ts/src/test/resources/samples/lang/Null.ts +++ b/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 + } } diff --git a/usvm-ts/src/test/resources/samples/lang/Undefined.ts b/usvm-ts/src/test/resources/samples/lang/Undefined.ts index 88f59c5e25..27039caac2 100644 --- a/usvm-ts/src/test/resources/samples/lang/Undefined.ts +++ b/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 + } } From 56bd4b53c1f583b550f590a63ec906b78b70fbc0 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 15:17:55 +0300 Subject: [PATCH 7/8] Error message --- .../main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 4a5ee9f9b0..493cd66c39 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -633,8 +633,8 @@ sealed interface TsBinaryOperator { } } - check(!lhsValue.isFakeObject()) - check(!rhsValue.isFakeObject()) + check(!lhsValue.isFakeObject()) { "Nested fake objects are not supported" } + check(!rhsValue.isFakeObject()) { "Nested fake objects are not supported" } if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) { val left = lhsValue.asExpr(addressSort) From 7ce170af53d71fb1720a573ddd0de41a404a7990 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 15:18:00 +0300 Subject: [PATCH 8/8] Add comment --- .../main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 493cd66c39..9e4e1db477 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -636,6 +636,10 @@ sealed interface TsBinaryOperator { 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)