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..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 @@ -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( 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/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/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 + } } 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 + } }