Skip to content

Commit f43c77a

Browse files
committed
[TS] Whitelist Less.lessUnknown in the differential suite
The engine resolves relational operators on mixed-type fake-object operands per sort pair (Lt.onBool = !lhs && rhs) instead of the JS ToNumber coercion, so e.g. `false < 0.0` is reported true while JS gives `0 < 0 === false`. The divergence surfaces nondeterministically depending on which input models the machine samples, making the suite flaky without the whitelist entry.
1 parent 2741f34 commit f43c77a

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/interpreter/ConcreteVsSymbolicDifferentialTest.kt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,13 +63,18 @@ class ConcreteVsSymbolicDifferentialTest {
6363
* numerically (e.g. `null + {}` becomes fp NaN), while JS applies ToPrimitive
6464
* and string concatenation (`null + {} === "null[object Object]"`), so the
6565
* engine follows the `res != res` (NaN) branch that is concretely unreachable.
66+
* - `Less.lessUnknown`: for mixed-type fake-object operands the engine resolves
67+
* relational operators per sort pair (`Lt.onBool = !lhs && rhs`, see
68+
* TsBinaryOperator.Lt) instead of the JS ToNumber coercion, so e.g.
69+
* `false < 0.0` is reported `true` while JS gives `0 < 0 === false`.
6670
*
6771
* NOTE: requires the CI-pinned ArkAnalyzer (`neo/2025-09-03`). Older/newer AA
6872
* builds may emit a different if-successor order in the DTO, which inverts
6973
* every branch after the jacodb lift (observed with `lipen/usvm`).
7074
*/
7175
private val knownEngineDivergences: Set<String> = setOf(
7276
"Add.addUnknownValues",
77+
"Less.lessUnknown",
7378
)
7479

7580
private fun runDifferential(resourcePath: String, className: String): Verdict {

0 commit comments

Comments
 (0)