Skip to content

Commit ebe4365

Browse files
LipenLipen
authored
[TS] Handle null == undefined (#330)
1 parent 75f0bfe commit ebe4365

7 files changed

Lines changed: 162 additions & 19 deletions

File tree

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

Lines changed: 34 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -384,7 +384,16 @@ sealed interface TsBinaryOperator {
384384
rhs: UHeapRef,
385385
scope: TsStepScope,
386386
): UBoolExpr {
387-
return mkEq(lhs, rhs)
387+
// Note: in JavaScript, `null == undefined`
388+
val lhsIsNull = mkEq(lhs, mkTsNullValue())
389+
val rhsIsNull = mkEq(rhs, mkTsNullValue())
390+
val lhsIsUndefined = mkEq(lhs, mkUndefinedValue())
391+
val rhsIsUndefined = mkEq(rhs, mkUndefinedValue())
392+
return mkOr(
393+
mkAnd(lhsIsUndefined, rhsIsNull),
394+
mkAnd(lhsIsNull, rhsIsUndefined),
395+
mkHeapRefEq(lhs, rhs)
396+
)
388397
}
389398

390399
override fun TsContext.resolveFakeObject(
@@ -412,42 +421,35 @@ sealed interface TsBinaryOperator {
412421
if (lhs.sort == boolSort && rhs.sort == boolSort) {
413422
val lhs = lhs.asExpr(boolSort)
414423
val rhs = rhs.asExpr(boolSort)
415-
return mkEq(lhs, rhs)
424+
return onBool(lhs, rhs, scope)
416425
}
417426

418427
// fp == fp
419428
if (lhs.sort == fp64Sort && rhs.sort == fp64Sort) {
420429
val lhs = lhs.asExpr(fp64Sort)
421430
val rhs = rhs.asExpr(fp64Sort)
422-
return mkFpEqualExpr(lhs, rhs)
431+
return onFp(lhs, rhs, scope)
423432
}
424433

425434
// bool == fp
426435
if (lhs.sort == boolSort && rhs.sort == fp64Sort) {
427436
val lhs = lhs.asExpr(boolSort)
428437
val rhs = rhs.asExpr(fp64Sort)
429-
return mkFpEqualExpr(boolToFp(lhs), rhs)
438+
return onFp(boolToFp(lhs), rhs, scope)
430439
}
431440

432441
// fp == bool
433442
if (lhs.sort == fp64Sort && rhs.sort == boolSort) {
434443
val lhs = lhs.asExpr(fp64Sort)
435444
val rhs = rhs.asExpr(boolSort)
436-
return mkFpEqualExpr(lhs, boolToFp(rhs))
445+
return onFp(lhs, boolToFp(rhs), scope)
437446
}
438447

439448
// ref == ref
440449
if (lhs.sort == addressSort && rhs.sort == addressSort) {
441-
// Note:
442-
// undefined == null
443-
// null == undefined
444450
val lhs = lhs.asExpr(addressSort)
445451
val rhs = rhs.asExpr(addressSort)
446-
return mkOr(
447-
mkEq(lhs, rhs),
448-
mkEq(lhs, mkUndefinedValue()) and mkEq(rhs, mkTsNullValue()),
449-
mkEq(lhs, mkTsNullValue()) and mkEq(rhs, mkUndefinedValue()),
450-
)
452+
return onRef(lhs, rhs, scope)
451453
}
452454

453455
// bool == ref
@@ -576,7 +578,7 @@ sealed interface TsBinaryOperator {
576578
lhsType.boolTypeExpr eq rhsType.boolTypeExpr,
577579
lhsType.fpTypeExpr eq rhsType.fpTypeExpr,
578580
// TODO support type equality
579-
lhsType.refTypeExpr eq rhsType.refTypeExpr
581+
lhsType.refTypeExpr eq rhsType.refTypeExpr,
580582
)
581583
}
582584

@@ -631,11 +633,27 @@ sealed interface TsBinaryOperator {
631633
}
632634
}
633635

634-
val loosyEqualityConstraint = with(Eq) {
636+
check(!lhsValue.isFakeObject()) { "Nested fake objects are not supported" }
637+
check(!rhsValue.isFakeObject()) { "Nested fake objects are not supported" }
638+
639+
// Note: this is the case 'ref === ref',
640+
// which should be `true` only if both have the same reference.
641+
// It is not correct to delegate to `Eq.resolve` in this case,
642+
// since `==` treats `null == undefined`, while `null !== undefined`.
643+
if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) {
644+
val left = lhsValue.asExpr(addressSort)
645+
val right = rhsValue.asExpr(addressSort)
646+
return mkAnd(
647+
typeConstraint,
648+
mkHeapRefEq(left, right)
649+
)
650+
}
651+
652+
val looseEqualityConstraint = with(Eq) {
635653
resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered")
636654
}
637655

638-
return mkAnd(typeConstraint, loosyEqualityConstraint)
656+
return mkAnd(typeConstraint, looseEqualityConstraint)
639657
}
640658

641659
override fun TsContext.internalResolve(

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

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
package org.usvm.samples.lang
22

33
import org.jacodb.ets.model.EtsScene
4-
import org.junit.jupiter.api.Test
54
import org.usvm.api.TsTestValue
65
import org.usvm.util.TsMethodTestRunner
76
import org.usvm.util.eq
7+
import kotlin.test.Test
88

99
class Null : TsMethodTestRunner() {
1010
private val tsPath = "/samples/lang/Null.ts"
@@ -16,8 +16,29 @@ class Null : TsMethodTestRunner() {
1616
val method = getMethod("isNull")
1717
discoverProperties<TsTestValue, TsTestValue.TsNumber>(
1818
method,
19-
{ a, r -> (r eq 1) && (a is TsTestValue.TsNull) },
20-
{ a, r -> (r eq 2) && (a !is TsTestValue.TsNull) },
19+
{ a, r ->
20+
(r eq 1) && (a is TsTestValue.TsNull)
21+
},
22+
{ a, r ->
23+
(r eq 2) && (a !is TsTestValue.TsNull)
24+
},
25+
)
26+
}
27+
28+
@Test
29+
fun `test isNullOrUndefined`() {
30+
val method = getMethod("isNullOrUndefined")
31+
discoverProperties<TsTestValue, TsTestValue.TsNumber>(
32+
method,
33+
{ a, r ->
34+
(r eq 1) && (a is TsTestValue.TsNull)
35+
},
36+
{ a, r ->
37+
(r eq 2) && (a is TsTestValue.TsUndefined)
38+
},
39+
{ a, r ->
40+
(r eq 3) && (a !is TsTestValue.TsNull) && (a !is TsTestValue.TsUndefined)
41+
},
2142
)
2243
}
2344
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,21 @@ class Undefined : TsMethodTestRunner() {
2424
},
2525
)
2626
}
27+
28+
@Test
29+
fun `test isUndefinedOrNull`() {
30+
val method = getMethod("isUndefinedOrNull")
31+
discoverProperties<TsTestValue, TsTestValue.TsNumber>(
32+
method,
33+
{ a, r ->
34+
(r eq 1) && (a is TsTestValue.TsUndefined)
35+
},
36+
{ a, r ->
37+
(r eq 2) && (a is TsTestValue.TsNull)
38+
},
39+
{ a, r ->
40+
(r eq 3) && (a !is TsTestValue.TsUndefined) && (a !is TsTestValue.TsNull)
41+
},
42+
)
43+
}
2744
}

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

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,4 +133,52 @@ class Equality : TsMethodTestRunner() {
133133
)
134134
)
135135
}
136+
137+
@Test
138+
fun `test eqNullWithNull`() {
139+
val method = getMethod("eqNullWithNull")
140+
discoverProperties<TsTestValue.TsNumber>(
141+
method,
142+
{ r -> r eq 1 },
143+
invariants = arrayOf(
144+
{ r -> r.number > 0 },
145+
)
146+
)
147+
}
148+
149+
@Test
150+
fun `test eqUndefinedWithUndefined`() {
151+
val method = getMethod("eqUndefinedWithUndefined")
152+
discoverProperties<TsTestValue.TsNumber>(
153+
method,
154+
{ r -> r eq 1 },
155+
invariants = arrayOf(
156+
{ r -> r.number > 0 },
157+
)
158+
)
159+
}
160+
161+
@Test
162+
fun `test eqNullWithUndefined`() {
163+
val method = getMethod("eqNullWithUndefined")
164+
discoverProperties<TsTestValue.TsNumber>(
165+
method,
166+
{ r -> r eq 1 },
167+
invariants = arrayOf(
168+
{ r -> r.number > 0 },
169+
)
170+
)
171+
}
172+
173+
@Test
174+
fun `test eqUndefinedWithNull`() {
175+
val method = getMethod("eqUndefinedWithNull")
176+
discoverProperties<TsTestValue.TsNumber>(
177+
method,
178+
{ r -> r eq 1 },
179+
invariants = arrayOf(
180+
{ r -> r.number > 0 },
181+
)
182+
)
183+
}
136184
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,13 @@ class Null {
66
if (x === null) return 1;
77
return 2;
88
}
9+
10+
isNullOrUndefined(x): number {
11+
if (x == null) {
12+
if (x === null) return 1;
13+
if (x === undefined) return 2;
14+
return -1; // unreachable
15+
}
16+
return 3; // not null or undefined
17+
}
918
}

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,13 @@ class Undefined {
66
if (x === undefined) return 1;
77
return 2;
88
}
9+
10+
isUndefinedOrNull(x): number {
11+
if (x == undefined) {
12+
if (x === undefined) return 1;
13+
if (x === null) return 2;
14+
return -1; // unreachable
15+
}
16+
return 3; // not null or undefined
17+
}
918
}

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

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
// @ts-nocheck
22
// noinspection JSUnusedGlobalSymbols
3+
// noinspection PointlessBooleanExpressionJS
34

45
class Equality {
56
eqBoolWithBool(a: boolean): number {
@@ -55,4 +56,24 @@ class Equality {
5556
if ([42] == false) return -1; // unreachable
5657
return 0;
5758
}
59+
60+
eqNullWithNull(): number {
61+
if (null == null) return 1;
62+
return -1; // unreachable
63+
}
64+
65+
eqUndefinedWithUndefined(): number {
66+
if (undefined == undefined) return 1;
67+
return -1; // unreachable
68+
}
69+
70+
eqNullWithUndefined(): number {
71+
if (null == undefined) return 1;
72+
return -1; // unreachable
73+
}
74+
75+
eqUndefinedWithNull(): number {
76+
if (undefined == null) return 1;
77+
return -1; // unreachable
78+
}
5879
}

0 commit comments

Comments
 (0)