Approximate Math.floor

Author: Lipen

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

@@ -1,5 +1,6 @@
 package org.usvm.machine.expr
 
+import io.ksmt.expr.KFpRoundingMode
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsArrayType
@@ -76,6 +77,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
         }
     }
 
+    // Handle `Math` method calls
+    if (expr.instance.name == "Math") {
+        if (expr.callee.name == "floor") {
+            return from(handleMathFloor(expr))
+        }
+    }
+
     val instance = scope.calcOnState { resolve(expr.instance)?.asExpr(addressSort) }
         ?: return TsExprApproximationResult.ResolveFailure
 
@@ -255,6 +263,27 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr)
     promise
 }
 
+private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
+    check(expr.args.size == 1) {
+        "Math.floor() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val arg = resolve(expr.args.single()) ?: return null
+
+    when (arg.sort) {
+        fp64Sort -> mkFpRoundToIntegralExpr(
+            roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative),
+            value = arg.asExpr(fp64Sort),
+        )
+
+        sizeSort -> arg.asExpr(sizeSort)
+
+        else -> {
+            logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" }
+            null
+        }
+    }
+}
+
 /**
  * Handles the `Array.push(...items)` method call.
  * Appends the specified `items` to the end of the array.