[TS] Precise approximations for frequent builtins; log every mock fallback

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: <callee> (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.

Author: CaelmBleidd

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<KFp64Sort>? = 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<KFp64Sort>): 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<KFp64Sort>): 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.

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

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

@@ -47,9 +47,14 @@ class IncDec : TsMethodTestRunner() {
         val method = getMethod("decrementLoop")
         discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
             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 },
+            ),
         )
     }
 }