[TS] Mock unresolved virtual calls instead of killing the state

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
@@ -10,10 +11,12 @@
 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
@@ -28,6 +31,7 @@
 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 +62,17 @@
         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 +94,15 @@
 
     // 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))
         }
     }
 
@@ -100,6 +122,11 @@
             .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))
@@ -263,27 +290,152 @@
     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.
@@ -429,6 +581,66 @@
  *
  * 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,