From a15dc8fd56866ae7fafb69c6e83a2c7d27c58cbd Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 6 Jul 2026 16:02:36 +0300 Subject: [PATCH 1/6] [TS] Mock unresolved virtual calls instead of killing the state Coverage investigation on an open-source corpus showed that 155 of 172 unreached symbolic targets died in under 100ms: TsInterpreter killed the state (assert(false)) on ANY unresolved callee (e.g. Number.isInteger), making everything after such a call unreachable. All three unresolved-call sites in visitVirtualMethodCall now fall back to mockMethodCall + returnSite, mirroring the pre-existing unresolved-constructor approximation. Full usvm-ts suite stays green (422 tests). NOTE: an engine fix, staged to be extracted into a separate PR. --- .../org/usvm/machine/interpreter/TsInterpreter.kt | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 850f97e9de..8cac3003aa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -183,7 +183,11 @@ class TsInterpreter( } return } - scope.assert(falseExpr) + // Approximate a call on an unresolved class with a mock instead of + // killing the state: otherwise a single unmodeled call (e.g. an SDK + // function) makes everything after it unreachable. + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } if (classes.size > 1) { @@ -203,7 +207,9 @@ class TsInterpreter( logger.warn { "Could not resolve method: ${stmt.callee} on type: $type" } - scope.assert(falseExpr) + // Mock instead of killing the state (see the comment above). + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } } else { @@ -212,7 +218,9 @@ class TsInterpreter( if (stmt.callee.name !in listOf("then")) { logger.warn { "Could not resolve method: ${stmt.callee}" } } - scope.assert(falseExpr) + // Mock instead of killing the state (see the comment above). + mockMethodCall(scope, stmt.callee) + scope.doWithState { newStmt(stmt.returnSite) } return } concreteMethods += methods From b690eb25a9c8cea08fd810b73c9d1f9dd320fd35 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 8 Jul 2026 12:39:57 +0300 Subject: [PATCH 2/6] [TS] Implement inc/dec unary expressions in TsExprResolver Front ends lower the side effect of `x++`/`--x` into an explicit assignment (the native ts-frontend emits `%t := x; x := ++x`, ArkAnalyzer expands to `x := x + 1`), and the jacodb DTO conversion maps both `++` and `--` to the Pre* model classes only. The resolver previously crashed on them ("Not supported"), killing every state in loops written with `x--`/`--x` under the ts-frontend. Pre* now evaluate to ToNumber(arg) +- 1 and Post* (never produced by the converter, but part of the model) to the old value. Tests: direct machine tests over programmatically built IR (ArkAnalyzer cannot exercise these visits since it never emits the unary forms) plus an ArkAnalyzer-lowered sample. A `const old = x++` sample case is deliberately absent: ArkAnalyzer lowers it as `x := x + 1; old := x`, i.e. `old` receives the new value - a frontend lowering bug found while writing these tests. --- .../org/usvm/machine/expr/TsExprResolver.kt | 32 +++-- .../kotlin/org/usvm/machine/IncDecExprTest.kt | 122 ++++++++++++++++++ .../org/usvm/samples/operators/IncDec.kt | 55 ++++++++ .../resources/samples/operators/IncDec.ts | 42 ++++++ 4 files changed, 239 insertions(+), 12 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt create mode 100644 usvm-ts/src/test/resources/samples/operators/IncDec.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index b283ae66cc..d7f408560b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -248,24 +248,32 @@ class TsExprResolver( return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPostIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + // NOTE on inc/dec: front ends lower the *side effect* of `x++`/`--x` into an + // explicit assignment (`%t := x; x := ++x`), and the jacodb DTO conversion maps + // both `++` and `--` to the Pre* classes only. Therefore the expressions below + // are pure value computations: Pre* yield ToNumber(arg) +- 1, Post* (which never + // come from the converter, but are part of the model) yield the old value. + + override fun visit(expr: EtsPostIncExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPostDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPostDecExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + return mkNumericExpr(arg, scope) } - override fun visit(expr: EtsPreIncExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPreIncExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort) + return mkFpAddExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0)) } - override fun visit(expr: EtsPreDecExpr): UExpr? { - logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" } - error("Not supported $expr") + override fun visit(expr: EtsPreDecExpr): UExpr? = with(ctx) { + val arg = resolve(expr.arg) ?: return null + val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort) + return mkFpSubExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0)) } override fun visit(expr: EtsBitNotExpr): UExpr? = with(ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt new file mode 100644 index 0000000000..d1ef32f653 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt @@ -0,0 +1,122 @@ +package org.usvm.machine + +import org.jacodb.ets.model.BasicBlock +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsBlockCfg +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsEntity +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsMethodParameter +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsPostDecExpr +import org.jacodb.ets.model.EtsPostIncExpr +import org.jacodb.ets.model.EtsPreDecExpr +import org.jacodb.ets.model.EtsPreIncExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmtLocation +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.util.TsTestResolver +import kotlin.time.Duration.Companion.seconds + +/** + * Direct tests for the inc/dec expression resolution. + * + * The IR is built programmatically: ArkAnalyzer never emits `++`/`--` unary + * expressions (it expands them into `x := x + 1`), while the native ts-frontend + * does emit them (as the value part, with an explicit write-back assignment), + * so sample-based tests cannot exercise these visits. + */ +class IncDecExprTest { + + private fun buildMethod(name: String, makeExpr: (EtsEntity) -> EtsEntity): Pair { + val fileSig = EtsFileSignature(projectName = "test", fileName = "IncDec.ts") + val classSig = EtsClassSignature(name = "T", file = fileSig) + val method = EtsMethodImpl( + signature = EtsMethodSignature( + enclosingClass = classSig, + name = name, + parameters = listOf(EtsMethodParameter(0, "a", EtsNumberType)), + returnType = EtsNumberType, + ), + ) + + fun loc(i: Int) = EtsStmtLocation(method, i) + val a = EtsLocal("a", EtsNumberType) + val res = EtsLocal("res", EtsNumberType) + val stmts = listOf( + EtsAssignStmt(loc(0), a, EtsParameterRef(0, EtsNumberType)), + EtsAssignStmt(loc(1), res, makeExpr(a)), + EtsReturnStmt(loc(2), res), + ) + method.body.cfg = EtsBlockCfg( + blocks = listOf(BasicBlock(0, stmts)), + successors = mapOf(0 to emptyList()), + ) + method.body.locals = listOf(a, res) + + val cls = EtsClassImpl(signature = classSig, fields = emptyList(), methods = listOf(method)) + val file = EtsFile(signature = fileSig, classes = listOf(cls), namespaces = emptyList()) + return EtsScene(listOf(file)) to method + } + + private fun run(name: String, makeExpr: (EtsEntity) -> EtsEntity): List> { + val (scene, method) = buildMethod(name, makeExpr) + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + exceptionsPropagation = true, + timeout = 20.seconds, + solverType = SolverType.YICES, + ) + val states = TsMachine(scene, options, TsOptions()).use { machine -> + machine.analyze(listOf(method)) + } + assertTrue(states.isNotEmpty()) { "no states collected for $name" } + return states.mapNotNull { state -> + val test = TsTestResolver().resolve(method, state) + val input = (test.before.parameters.firstOrNull() as? TsTestValue.TsNumber)?.number + val result = (test.returnValue as? TsTestValue.TsNumber)?.number + if (input != null && result != null) input to result else null + }.also { assertTrue(it.isNotEmpty()) { "no numeric executions for $name" } } + } + + @Test + fun `pre-increment yields arg plus one`() { + for ((input, result) in run("preInc") { EtsPreIncExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input + 1, result, 0.0) { "++($input)" } + } + } + + @Test + fun `pre-decrement yields arg minus one`() { + for ((input, result) in run("preDec") { EtsPreDecExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input - 1, result, 0.0) { "--($input)" } + } + } + + @Test + fun `post-increment and post-decrement yield the old value`() { + for ((input, result) in run("postInc") { EtsPostIncExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input, result, 0.0) { "($input)++" } + } + for ((input, result) in run("postDec") { EtsPostDecExpr(it, EtsNumberType) }) { + if (input.isNaN()) assertTrue(result.isNaN()) + else assertEquals(input, result, 0.0) { "($input)--" } + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt new file mode 100644 index 0000000000..fe3a1a31f5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt @@ -0,0 +1,55 @@ +package org.usvm.samples.operators + +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 org.usvm.util.isNaN + +class IncDec : TsMethodTestRunner() { + private val tsPath = "/samples/operators/IncDec.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `test preIncrement`() { + val method = getMethod("preIncrement") + discoverProperties( + method = method, + { a, r -> a.isNaN() && r.isNaN() }, + { a, r -> !a.isNaN() && (r.number eq a.number + 1) }, + invariants = arrayOf( + { a, r -> + if (a.isNaN()) r.isNaN() else r.number eq a.number + 1 + }, + ) + ) + } + + @Test + fun `test preDecrement`() { + val method = getMethod("preDecrement") + discoverProperties( + method = method, + { a, r -> a.isNaN() && r.isNaN() }, + { a, r -> !a.isNaN() && (r.number eq a.number - 1) }, + invariants = arrayOf( + { a, r -> + if (a.isNaN()) r.isNaN() else r.number eq a.number - 1 + }, + ) + ) + } + + @Test + fun `test decrementLoop`() { + val method = getMethod("decrementLoop") + discoverProperties( + method = method, + { n, r -> (n.number <= 0 || n.isNaN()) && (r eq 0) }, + { n, r -> n.number >= 3 && (r eq 3) }, + { n, r -> n.number > 0 && n.number <= 2 && r.number > 0 && r.number <= 2 }, + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/operators/IncDec.ts b/usvm-ts/src/test/resources/samples/operators/IncDec.ts new file mode 100644 index 0000000000..5dfa95d54d --- /dev/null +++ b/usvm-ts/src/test/resources/samples/operators/IncDec.ts @@ -0,0 +1,42 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class IncDec { + preIncrement(a: number): number { + let x = a; + ++x; + if (Number.isNaN(a)) return x; // NaN + 1 == NaN + if (a == 0) return x; // ++0 == 1 + if (a > 0) return x; + if (a < 0) return x; + // unreachable + } + + // NOTE: a `const old = x++` case is deliberately absent: ArkAnalyzer + // (neo/2025-09-03) lowers it as `x := x + 1; old := x`, i.e. `old` receives + // the *new* value — a frontend lowering bug that no engine semantics can fix. + + preDecrement(a: number): number { + let x = a; + --x; + if (Number.isNaN(a)) return x; // NaN - 1 == NaN + if (a == 0) return x; // --0 == -1 + if (a > 0) return x; + if (a < 0) return x; + // unreachable + } + + decrementLoop(n: number): number { + let count = 0; + let x = n; + while (x > 0 && count < 3) { + x--; + count++; + } + // Each loop depth is a distinct branch so that full coverage requires + // the engine to actually unroll the decrementing loop. + if (count == 0) return count; + if (count == 3) return count; + return count; // 1 or 2 iterations + } +} From b68e7aaf4b7345bcf9cc9e9086d9648872bdcd6f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 10 Jul 2026 13:08:06 +0300 Subject: [PATCH 3/6] [TS] Precise approximations for frequent builtins; log every mock fallback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Frequency data from open-source corpora (TheAlgorithms/TypeScript maths and loiane/javascript-datastructures-algorithms, full-log probes) shows that unresolved calls split into three groups: in-project cross-file targets (a scene-construction problem, not the engine's), a small set of very hot builtins (Math.abs — 208 occurrences, Number.isInteger — 55, Math.sqrt — 13 on the maths corpus alone), and a tail of genuinely unmodelable calls. This change shrinks the over-approximation surface of the mock fallback by modeling the hot builtins precisely in the fp theory: - Number.isInteger / isSafeInteger (2^53 bound not modeled) / isFinite, with the same fake-object discriminator handling as Number.isNaN - Math.floor/ceil/trunc via fp round-to-integral in the matching mode (floor generalized), Math.round as floor(x + 0.5) per JS semantics, Math.abs, Math.sqrt - Math.min/max with JS NaN semantics (NaN if any argument is NaN, unlike IEEE minNum/maxNum) - console.* treated as side-effect-free undefined, like Logger Every remaining mock fallback now logs a distinct "Mocking an unresolved call: (over-approximation)" line, so the residual over-approximation stays measurable on corpus runs. decrementLoop test properties are reclassified by the observed loop depth: non-integral inputs (n = 2.5) legitimately reach depth ceil(n), and the solver started picking such models once the approximations changed the search. --- .../usvm/machine/expr/CallApproximations.kt | 167 ++++++++++++++++-- .../usvm/machine/interpreter/TsInterpreter.kt | 3 + .../org/usvm/samples/operators/IncDec.kt | 9 +- 3 files changed, 166 insertions(+), 13 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index c651b676ca..e7d003d8c3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -1,6 +1,7 @@ package org.usvm.machine.expr import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType @@ -28,6 +29,7 @@ import org.usvm.types.first import org.usvm.types.firstOrNull import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.boolToFp import org.usvm.util.resolveEtsMethods private val logger = KotlinLogging.logger {} @@ -58,6 +60,17 @@ internal fun TsExprResolver.tryApproximateInstanceCall( if (expr.callee.name == "isNaN") { return from(handleNumberIsNaN(expr)) } + if (expr.callee.name == "isInteger" || expr.callee.name == "isSafeInteger") { + return from(handleNumberIsInteger(expr)) + } + if (expr.callee.name == "isFinite") { + return from(handleNumberIsFinite(expr)) + } + } + + // `console.*` is side-effect-free for the analysis, like `Logger` + if (expr.instance.name == "console") { + return from(mkUndefinedValue()) } // Handle 'Boolean' constructor calls @@ -79,8 +92,15 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Math` method calls if (expr.instance.name == "Math") { - if (expr.callee.name == "floor") { - return from(handleMathFloor(expr)) + when (expr.callee.name) { + "floor" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardNegative)) + "ceil" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardPositive)) + "trunc" -> return from(handleMathRounding(expr, KFpRoundingMode.RoundTowardZero)) + "round" -> return from(handleMathRound(expr)) + "abs" -> return from(handleMathAbs(expr)) + "sqrt" -> return from(handleMathSqrt(expr)) + "min" -> return from(handleMathMinMax(expr, isMin = true)) + "max" -> return from(handleMathMinMax(expr, isMin = false)) } } @@ -263,27 +283,152 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr) promise } -private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { +/** Resolve the single argument of a Math function as an fp64 value, when possible. */ +private fun TsExprResolver.resolveSingleFpArg(expr: EtsInstanceCallExpr): UExpr? = with(ctx) { check(expr.args.size == 1) { - "Math.floor() should have exactly one argument, but got ${expr.args.size}" + "Math.${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}" } val arg = resolve(expr.args.single()) ?: return null + when { + arg.isFakeObject() -> { + // Constrain the fake object to its numeric alternative: precise Math + // semantics for non-number arguments (ToNumber coercions) is future work. + scope.assert(arg.getFakeType(scope).fpTypeExpr) ?: return null + arg.extractFp(scope) + } - when (arg.sort) { - fp64Sort -> mkFpRoundToIntegralExpr( - roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), - value = arg.asExpr(fp64Sort), - ) + arg.sort == fp64Sort -> arg.asExpr(fp64Sort) - sizeSort -> arg.asExpr(sizeSort) + arg.sort == boolSort -> boolToFp(arg.asExpr(boolSort)) else -> { - logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" } + logger.warn { "Unsupported argument sort for Math.${expr.callee.name}(): ${arg.sort}" } null } } } +/** `Math.floor` / `Math.ceil` / `Math.trunc`: fp round-to-integral in the corresponding mode. */ +private fun TsExprResolver.handleMathRounding( + expr: EtsInstanceCallExpr, + mode: KFpRoundingMode, +): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(mode), value) +} + +/** + * `Math.round(x)` in JS is `floor(x + 0.5)` (halfway cases round towards +Infinity), + * which differs from the IEEE round-to-nearest-even mode. + * (The sign of a `-0` result is not preserved by this encoding.) + */ +private fun TsExprResolver.handleMathRound(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + val plusHalf = mkFpAddExpr( + mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven), + value, + mkFp64(0.5), + ) + mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), plusHalf) +} + +private fun TsExprResolver.handleMathAbs(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpAbsExpr(value) +} + +private fun TsExprResolver.handleMathSqrt(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + val value = resolveSingleFpArg(expr) ?: return null + mkFpSqrtExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven), value) +} + +/** + * `Math.min` / `Math.max`. Unlike the IEEE minNum/maxNum operations (which prefer + * the non-NaN operand), JS returns NaN if *any* argument is NaN. + */ +private fun TsExprResolver.handleMathMinMax(expr: EtsInstanceCallExpr, isMin: Boolean): UExpr<*>? = with(ctx) { + val args = expr.args.map { arg -> + val resolved = resolve(arg) ?: return null + when { + resolved.isFakeObject() -> { + scope.assert(resolved.getFakeType(scope).fpTypeExpr) ?: return null + resolved.extractFp(scope) + } + + resolved.sort == fp64Sort -> resolved.asExpr(fp64Sort) + resolved.sort == boolSort -> boolToFp(resolved.asExpr(boolSort)) + else -> { + logger.warn { "Unsupported argument sort for Math.min/max: ${resolved.sort}" } + return null + } + } + } + if (args.isEmpty()) { + // Math.min() == +Infinity, Math.max() == -Infinity + return mkFp64(if (isMin) Double.POSITIVE_INFINITY else Double.NEGATIVE_INFINITY) + } + val anyNaN = args.map { mkFpIsNaNExpr(it) }.reduce { a, b -> mkOr(a, b) } + val pure = args.reduce { a, b -> if (isMin) mkFpMinExpr(a, b) else mkFpMaxExpr(a, b) } + mkIte(anyNaN, mkFp64(Double.NaN), pure) +} + +/** + * 21.1.2.3 `Number.isInteger ( number )`: false for non-numbers, NaN and infinities; + * true iff the value equals its integral rounding. `isSafeInteger` is approximated + * the same way (the 2^53 bound is not modeled). + */ +private fun TsExprResolver.handleNumberIsInteger(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + check(expr.args.size == 1) { "Number.isInteger should have one argument" } + val arg = resolve(expr.args.single()) ?: return null + + fun isIntegral(value: UExpr): UBoolExpr { + val rounded = mkFpRoundToIntegralExpr(mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), value) + return mkAnd( + mkNot(mkFpIsInfiniteExpr(value)), + mkFpEqualExpr(rounded, value), // false for NaN by IEEE equality + ) + } + + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + return mkIte( + condition = fakeType.fpTypeExpr, + trueBranch = isIntegral(arg.extractFp(scope)), + falseBranch = mkFalse(), + ) + } + + if (arg.sort == fp64Sort) { + isIntegral(arg.asExpr(fp64Sort)) + } else { + mkFalse() + } +} + +/** 21.1.2.2 `Number.isFinite ( number )`: false for non-numbers, NaN and infinities. */ +private fun TsExprResolver.handleNumberIsFinite(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + check(expr.args.size == 1) { "Number.isFinite should have one argument" } + val arg = resolve(expr.args.single()) ?: return null + + fun isFinite(value: UExpr): UBoolExpr = + mkAnd(mkNot(mkFpIsNaNExpr(value)), mkNot(mkFpIsInfiniteExpr(value))) + + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + return mkIte( + condition = fakeType.fpTypeExpr, + trueBranch = isFinite(arg.extractFp(scope)), + falseBranch = mkFalse(), + ) + } + + if (arg.sort == fp64Sort) { + isFinite(arg.asExpr(fp64Sort)) + } else { + mkFalse() + } +} + /** * Handles the `Array.push(...items)` method call. * Appends the specified `items` to the end of the array. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 8cac3003aa..2933befcac 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -186,6 +186,7 @@ class TsInterpreter( // Approximate a call on an unresolved class with a mock instead of // killing the state: otherwise a single unmodeled call (e.g. an SDK // function) makes everything after it unreachable. + logger.warn { "Mocking a call on an unresolved class: ${stmt.callee} (over-approximation)" } mockMethodCall(scope, stmt.callee) scope.doWithState { newStmt(stmt.returnSite) } return @@ -208,6 +209,7 @@ class TsInterpreter( "Could not resolve method: ${stmt.callee} on type: $type" } // Mock instead of killing the state (see the comment above). + logger.warn { "Mocking an unresolved call: ${stmt.callee} (over-approximation)" } mockMethodCall(scope, stmt.callee) scope.doWithState { newStmt(stmt.returnSite) } return @@ -219,6 +221,7 @@ class TsInterpreter( logger.warn { "Could not resolve method: ${stmt.callee}" } } // Mock instead of killing the state (see the comment above). + logger.warn { "Mocking an unresolved call: ${stmt.callee} (over-approximation)" } mockMethodCall(scope, stmt.callee) scope.doWithState { newStmt(stmt.returnSite) } return diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt index fe3a1a31f5..91ef1bdb6c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt @@ -47,9 +47,14 @@ class IncDec : TsMethodTestRunner() { val method = getMethod("decrementLoop") discoverProperties( method = method, + // Classify by the observed depth, not by n: non-integral inputs + // (e.g. n = 2.5) legitimately reach depth ceil(n). { n, r -> (n.number <= 0 || n.isNaN()) && (r eq 0) }, - { n, r -> n.number >= 3 && (r eq 3) }, - { n, r -> n.number > 0 && n.number <= 2 && r.number > 0 && r.number <= 2 }, + { n, r -> r eq 3 }, + { n, r -> r.number > 0 && r.number < 3 }, + invariants = arrayOf( + { _, r -> r.number >= 0 && r.number <= 3 }, + ), ) } } From 3df3c83a438189f23a882d54acc5a4961a443a77 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 10 Jul 2026 15:16:19 +0300 Subject: [PATCH 4/6] [TS] Model the Array constructor `new Array(n)` used to allocate an object of an unresolved class (8 occurrences on the maths corpus probe), so none of the array approximations applied to it and every subsequent operation on the array was mocked. Now: - `new Array` in EtsNewExpr allocates a genuine array object (EtsArrayType, length 0), so the array method approximations and the constructor handling apply to it; - the `constructor` call on an array-typed instance is approximated: the zero-argument form keeps the empty length, the single-argument form sets the length with the same size-validity fork as EtsNewArrayExpr (non-integral or negative sizes throw, as in JS); the multi-argument literal form is left to the logged mock fallback. --- .../usvm/machine/expr/CallApproximations.kt | 67 +++++++++++++++++++ .../org/usvm/machine/expr/TsExprResolver.kt | 12 ++++ 2 files changed, 79 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index e7d003d8c3..f46523dc73 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -11,10 +11,12 @@ import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArray +import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.memcpy import org.usvm.api.typeStreamOf @@ -120,6 +122,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort + // Handle the `Array` constructor: `new Array()` / `new Array(n)` + if (expr.callee.name == CONSTRUCTOR_NAME) { + return from(handleArrayConstructor(expr, instanceType)) + } + // Handle 'Array.push()' method calls if (expr.callee.name == "push") { return from(handleArrayPush(expr, instanceType, elementSort)) @@ -574,6 +581,66 @@ private fun TsExprResolver.handleArrayPop( * * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.fill */ +/** + * The `Array` constructor. `new Array()` keeps the zero length set at allocation; + * `new Array(n)` sets the length to `n`, forking on the validity of the size + * (a non-integral or out-of-range `n` throws a RangeError in JS). + * The multi-argument literal form `new Array(a, b, ...)` is not approximated. + */ +private fun TsExprResolver.handleArrayConstructor( + expr: EtsInstanceCallExpr, + arrayType: EtsArrayType, +): UExpr<*>? = with(ctx) { + val resolved = resolve(expr.instance)?.asExpr(addressSort) ?: return null + val array = resolved as? UConcreteHeapRef ?: run { + logger.warn { "Array constructor on a non-concrete instance is not approximated" } + return null + } + + when (expr.args.size) { + 0 -> array + + 1 -> { + val size = resolve(expr.args.single()) ?: return null + if (size.sort != fp64Sort) { + logger.warn { "Unsupported sort for the Array constructor size: ${size.sort}" } + return null + } + val bvSize = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = size.asExpr(fp64Sort), + bvSize = 32, + isSigned = true, + ) + val isValidSize = mkAnd( + mkEq( + mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = bvSize, + signed = true, + ), + size.asExpr(fp64Sort), + ), + mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)), + ) + scope.fork( + isValidSize, + blockOnFalseState = { throwException("Invalid array length: ${size.asExpr(fp64Sort)}") }, + ) ?: return null + scope.doWithState { + memory.initializeArrayLength(array, arrayType, sizeSort, bvSize.asExpr(sizeSort)) + } + array + } + + else -> { + logger.warn { "The literal form of the Array constructor is not approximated: ${expr.args.size} args" } + null + } + } +} + private fun TsExprResolver.handleArrayFill( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index d7f408560b..5ff06d443a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -973,6 +973,18 @@ class TsExprResolver( expr.type } + if (expr.type.typeName == "Array") { + // `new Array(...)`: allocate a genuine array object so that the array + // approximations apply; the length is set by the constructor call + // that immediately follows the allocation. + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + return@with scope.calcOnState { + val address = memory.allocConcrete(arrayType) + memory.initializeArrayLength(address, arrayType, sizeSort, mkBv(0).asExpr(sizeSort)) + address + } + } + if (expr.type.typeName == "Boolean") { val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxByOrNull { it.methods.size } ?: error("No Boolean class found in SDK") From 7c5a6a7c5a2998b8dff9fc67418bdc50c1d3ec4b Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 10 Jul 2026 18:29:09 +0300 Subject: [PATCH 5/6] [TS] Resolve the compare-to-zero truthiness idiom as ToBoolean for ref-like operands Front ends lower `if (x)` into `x != 0` / `x != false`, byte-identical to a genuine loose comparison in the IR. For reference-like operands the numeric reading diverges from ToBoolean: `undefined != 0` evaluated as ToNumber(undefined) = NaN != 0 = true, making `undefined` truthy (found by the differential oracle: And.andOfUnknown(0, undefined) returned 21 where JS returns 0). A compare of a fake-object or reference operand against literal zero/false now resolves via mkTruthyExpr; numeric and boolean operands keep the literal loose-comparison semantics, matching the convention of the concrete ArkIR interpreter in the hybrid pipeline. --- .../org/usvm/machine/expr/TsExprResolver.kt | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 5ff06d443a..0bc8586a07 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -77,6 +77,7 @@ import org.jacodb.ets.model.EtsYieldExpr import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.getDeclaredLocals +import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UIteExpr import org.usvm.USort @@ -786,13 +787,44 @@ class TsExprResolver( // region RELATION override fun visit(expr: EtsEqExpr): UExpr? { + truthinessIdiomOrNull(expr.left, expr.right)?.let { truthy -> + return ctx.mkNot(truthy) + } return resolveBinaryOperator(TsBinaryOperator.Eq, expr) } override fun visit(expr: EtsNotEqExpr): UExpr? { + truthinessIdiomOrNull(expr.left, expr.right)?.let { truthy -> + return truthy + } return resolveBinaryOperator(TsBinaryOperator.Neq, expr) } + /** + * Front ends lower the truthiness test `if (x)` into the compare-to-zero / + * compare-to-false idiom (`x != 0`, `x != false`), which is byte-identical + * to a genuine loose comparison in the IR. For *reference-like* operands the + * numeric reading diverges from ToBoolean (e.g. `undefined != 0` evaluates + * to `NaN != 0 = true`, although `undefined` is falsy). Follow the idiom + * contract: a compare of a fake/ref operand against literal zero/false is + * ToBoolean. Numeric and boolean operands keep the literal loose-comparison + * semantics (this matches the concrete ArkIR interpreter of the hybrid + * pipeline). + * + * @return the truthiness expression, or null when the idiom does not apply. + */ + private fun truthinessIdiomOrNull(left: EtsEntity, right: EtsEntity): UBoolExpr? = with(ctx) { + val isZeroOrFalse = (right is EtsNumberConstant && right.value == 0.0) || + (right is EtsBooleanConstant && !right.value) + if (!isZeroOrFalse) return null + + val lhs = resolve(left) ?: return null + val isRefLike = lhs.isFakeObject() || (lhs.sort == addressSort) + if (!isRefLike) return null + + mkTruthyExpr(lhs, scope) + } + override fun visit(expr: EtsStrictEqExpr): UExpr? { return resolveBinaryOperator(TsBinaryOperator.StrictEq, expr) } From befd79f6fa6ba50f63d7ab5148eb1579fa9e90c3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 10 Jul 2026 18:32:17 +0300 Subject: [PATCH 6/6] [TS] Truthiness idiom: extend ToBoolean to all operand kinds MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .../org/usvm/machine/expr/TsExprResolver.kt | 25 ++++++++----------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 0bc8586a07..541f7cb1b1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -787,9 +787,6 @@ class TsExprResolver( // region RELATION override fun visit(expr: EtsEqExpr): UExpr? { - truthinessIdiomOrNull(expr.left, expr.right)?.let { truthy -> - return ctx.mkNot(truthy) - } return resolveBinaryOperator(TsBinaryOperator.Eq, expr) } @@ -801,15 +798,16 @@ class TsExprResolver( } /** - * Front ends lower the truthiness test `if (x)` into the compare-to-zero / - * compare-to-false idiom (`x != 0`, `x != false`), which is byte-identical - * to a genuine loose comparison in the IR. For *reference-like* operands the - * numeric reading diverges from ToBoolean (e.g. `undefined != 0` evaluates - * to `NaN != 0 = true`, although `undefined` is falsy). Follow the idiom - * contract: a compare of a fake/ref operand against literal zero/false is - * ToBoolean. Numeric and boolean operands keep the literal loose-comparison - * semantics (this matches the concrete ArkIR interpreter of the hybrid - * pipeline). + * Front ends lower the truthiness test `if (x)` into the compare idiom + * `x != 0` (ArkAnalyzer) / `x != false` (ts-frontend) — byte-identical to a + * genuine loose comparison in the IR. The numeric reading diverges from + * ToBoolean on both axes: `undefined != 0` evaluates to + * ToNumber(undefined) = NaN != 0 = true although `undefined` is falsy, and + * `NaN != 0` is true although `NaN` is falsy. Follow the idiom contract: + * `!=` against literal zero/false is ToBoolean for ALL operand kinds + * (bool/fp/ref/fake), matching the concrete ArkIR interpreter of the + * hybrid pipeline. Note the idiom only ever uses `!=` (negated tests swap + * the branch successors instead), so `==` keeps the literal semantics. * * @return the truthiness expression, or null when the idiom does not apply. */ @@ -819,9 +817,6 @@ class TsExprResolver( if (!isZeroOrFalse) return null val lhs = resolve(left) ?: return null - val isRefLike = lhs.isFakeObject() || (lhs.sort == addressSort) - if (!isRefLike) return null - mkTruthyExpr(lhs, scope) }