Skip to content

Commit befd79f

Browse files
committed
[TS] Truthiness idiom: extend ToBoolean to all operand kinds
The differential oracle immediately caught the second half of the hole: with the ref-only reading, `if (a)` over a numeric NaN still took the then-branch (`NaN != 0` is true, yet NaN is falsy), so andOfUnknown(NaN, x) returned 0 where JS returns 11. The idiom now resolves via mkTruthyExpr for every operand kind (bool/fp/ref/fake), and only for `!=` — front ends never lower truthiness through `==` (negated tests swap branch successors instead), so `==` keeps the literal loose-equality semantics.
1 parent 7c5a6a7 commit befd79f

1 file changed

Lines changed: 10 additions & 15 deletions

File tree

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -787,9 +787,6 @@ class TsExprResolver(
787787
// region RELATION
788788

789789
override fun visit(expr: EtsEqExpr): UExpr<out USort>? {
790-
truthinessIdiomOrNull(expr.left, expr.right)?.let { truthy ->
791-
return ctx.mkNot(truthy)
792-
}
793790
return resolveBinaryOperator(TsBinaryOperator.Eq, expr)
794791
}
795792

@@ -801,15 +798,16 @@ class TsExprResolver(
801798
}
802799

803800
/**
804-
* Front ends lower the truthiness test `if (x)` into the compare-to-zero /
805-
* compare-to-false idiom (`x != 0`, `x != false`), which is byte-identical
806-
* to a genuine loose comparison in the IR. For *reference-like* operands the
807-
* numeric reading diverges from ToBoolean (e.g. `undefined != 0` evaluates
808-
* to `NaN != 0 = true`, although `undefined` is falsy). Follow the idiom
809-
* contract: a compare of a fake/ref operand against literal zero/false is
810-
* ToBoolean. Numeric and boolean operands keep the literal loose-comparison
811-
* semantics (this matches the concrete ArkIR interpreter of the hybrid
812-
* pipeline).
801+
* Front ends lower the truthiness test `if (x)` into the compare idiom
802+
* `x != 0` (ArkAnalyzer) / `x != false` (ts-frontend) — byte-identical to a
803+
* genuine loose comparison in the IR. The numeric reading diverges from
804+
* ToBoolean on both axes: `undefined != 0` evaluates to
805+
* ToNumber(undefined) = NaN != 0 = true although `undefined` is falsy, and
806+
* `NaN != 0` is true although `NaN` is falsy. Follow the idiom contract:
807+
* `!=` against literal zero/false is ToBoolean for ALL operand kinds
808+
* (bool/fp/ref/fake), matching the concrete ArkIR interpreter of the
809+
* hybrid pipeline. Note the idiom only ever uses `!=` (negated tests swap
810+
* the branch successors instead), so `==` keeps the literal semantics.
813811
*
814812
* @return the truthiness expression, or null when the idiom does not apply.
815813
*/
@@ -819,9 +817,6 @@ class TsExprResolver(
819817
if (!isZeroOrFalse) return null
820818

821819
val lhs = resolve(left) ?: return null
822-
val isRefLike = lhs.isFakeObject() || (lhs.sort == addressSort)
823-
if (!isRefLike) return null
824-
825820
mkTruthyExpr(lhs, scope)
826821
}
827822

0 commit comments

Comments
 (0)