Preserve native Math identity and exact constants

usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt

@@ -14,7 +14,7 @@ import org.usvm.util.EtsHierarchy
 import kotlin.io.path.deleteIfExists
 import kotlin.io.path.inputStream
 
-private val coreRuntimeClassNames = setOf("Object", "Function", "Array", "Date")
+private val coreRuntimeClassNames = setOf("Object", "Function", "Array", "Date", "Math")
 
 // JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports
 // declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes.
@@ -53,8 +53,8 @@ internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean =
         signature.name in setOf("Function", "Array")
 
 /**
- * Load Object, Function, Array and Date from the standard declarations bundled in the pinned JacoDB dependency.
- * Keep existing Object/Function/Array members and add nominal Date identity. Preserve SDK declarations
+ * Load Object, Function, Array, Date and Math from the standard declarations bundled in the pinned JacoDB dependency.
+ * Keep existing Object/Function/Array/Math members and add nominal Date identity. Preserve SDK declarations
  * supplied by the caller. Date APIs continue through the existing unknown-call and semantic-model boundary.
  */
 internal fun EtsScene.withCoreRuntimeSdk(): EtsScene {
@@ -71,7 +71,7 @@ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene {
 
 /** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */
 internal fun EtsScene.sdkConstructorForGlobal(local: EtsLocal): EtsClass? =
-    sdkClasses.singleOrNull { it.name == local.name }
+    sdkClasses.singleOrNull { it.name == local.name && it.name != "Math" }
 
 internal fun EtsScene.runtimeFunctionType(): EtsClassType {
     val functionClass = sdkClasses.singleOrNull { it.name == "Function" }

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

@@ -0,0 +1,55 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsFile
+import org.usvm.UConcreteHeapRef
+import org.usvm.UHeapRef
+import org.usvm.machine.interpreter.getGlobals
+import org.usvm.machine.state.TsState
+import org.usvm.util.mkFieldLValue
+
+private const val MATH_E = 2.718281828459045
+private const val MATH_LN10 = 2.302585092994046
+private const val MATH_LN2 = 0.6931471805599453
+private const val MATH_LOG10E = 0.4342944819032518
+private const val MATH_LOG2E = 1.4426950408889634
+private const val MATH_PI = 3.141592653589793
+private const val MATH_SQRT1_2 = 0.7071067811865476
+private const val MATH_SQRT2 = 1.4142135623730951
+
+private val nativeMathConstants = mapOf(
+    "E" to MATH_E,
+    "LN10" to MATH_LN10,
+    "LN2" to MATH_LN2,
+    "LOG10E" to MATH_LOG10E,
+    "LOG2E" to MATH_LOG2E,
+    "PI" to MATH_PI,
+    "SQRT1_2" to MATH_SQRT1_2,
+    "SQRT2" to MATH_SQRT2,
+)
+
+/** The implicit Math global is one ordinary SDK object, rather than a callable constructor. */
+internal fun TsState.nativeMathGlobal(file: EtsFile, name: String): UConcreteHeapRef? {
+    if (name != "Math") return null
+    val sourceBinding = file.getGlobals().any { it.name == name }
+    val importedBinding = file.importInfos.any { it.name == name }
+    if (sourceBinding || importedBinding) return null
+
+    val owner = ctx.scene.sdkClasses.singleOrNull { it.name == "Math" } ?: return null
+    val existing = staticStorage[owner]
+    if (existing != null) return existing
+
+    val instance = getStaticInstance(owner)
+    with(ctx) {
+        for ((field, value) in nativeMathConstants) {
+            memory.write(mkFieldLValue(fp64Sort, instance, field), mkFp64(value), guard = trueExpr)
+        }
+    }
+    return instance
+}
+
+/** Property descriptors of the native constants are not mutable ordinary field storage. */
+internal fun TsState.isNativeMathConstant(instance: UHeapRef, field: String): Boolean {
+    if (field !in nativeMathConstants) return false
+    val owner = ctx.scene.sdkClasses.singleOrNull { it.name == "Math" } ?: return false
+    return staticStorage[owner] == instance
+}

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

@@ -16,6 +16,9 @@ fun TsContext.readGlobal(
 
     val savedSort = getSortForDfltObjectField(file, name)
     if (savedSort == null) {
+        val native = nativeMathGlobal(file = file, name = name)
+        if (native != null) return@calcOnState native
+
         // Missing storage also covers native globals that this runtime has not modeled.
         // It does not establish that the reached path is unsatisfiable.
         terminateAsUnsupported(

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

@@ -522,6 +522,14 @@ class TsExprResolver(
                 checkUndefinedOrNullPropertyRead(scope, rawInstance, operand.field.name) ?: return null
                 val instance = resolveHeapRef(scope, rawInstance) ?: return null
 
+                val nativeMathConstant = scope.calcOnState { isNativeMathConstant(instance, operand.field.name) }
+                if (nativeMathConstant) {
+                    scope.doWithState {
+                        terminateAsUnsupported(reason = "Deleting readonly native Math constants is not modeled")
+                    }
+                    return null
+                }
+
                 val prototypeFallback = prototypeFallbackReason(instance, operand)
                 if (prototypeFallback != null) {
                     throw UnsupportedOperationException(prototypeFallback)
@@ -1760,12 +1768,28 @@ class TsSimpleValueResolver(
             }
         }
 
+        val nativeMath = scope.calcOnState { nativeMathGlobal(file = file, name = local.name) }
+        if (nativeMath != null) return nativeMath
+
         logger.error { "Cannot resolve local variable '$local' in method: $currentMethod" }
         scope.assert(falseExpr)
         return null
     }
 
     override fun visit(local: EtsLocal): UExpr<out USort>? {
+        if (local.name == "Math") {
+            val currentMethod = scope.calcOnState { lastEnteredMethod }
+            val sourceParameter = currentMethod.parameters.any { it.name == local.name }
+            val sourceAssignment = currentMethod.cfg.stmts.filterIsInstance<EtsAssignStmt>()
+                .any { (it.lhv as? EtsLocal)?.name == local.name }
+            // Frontend locals also contain reads of implicit globals; only actual bindings shadow Math.
+            if (!sourceParameter && !sourceAssignment) {
+                val file = requireNotNull(currentMethod.enclosingClass?.declaringFile)
+                val nativeMath = scope.calcOnState { nativeMathGlobal(file = file, name = local.name) }
+                if (nativeMath != null) return nativeMath
+            }
+        }
+
         val isNonFiniteNumericName = local.name == "NaN" || local.name == "Infinity"
         if (isNonFiniteNumericName && hasSourceBinding(local)) {
             return resolveLocal(local)
@@ -1842,6 +1866,8 @@ class TsSimpleValueResolver(
                 throw UnsupportedOperationException("Builtin Symbol values are not modeled")
             }
 
+            if (local.name == "Math") return resolveLocal(local)
+
             val sdkConstructor = ctx.scene.sdkConstructorForGlobal(local)
             if (sdkConstructor != null) return ctx.classConstructorRef(sdkConstructor.signature, scope)
 

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

@@ -51,6 +51,14 @@ internal fun TsContext.tryWriteIntrinsicField(
     field: EtsFieldSignature,
     value: UExpr<*>,
 ): TsIntrinsicFieldResult<Unit> {
+    val nativeMathConstant = scope.calcOnState { isNativeMathConstant(instance, field.name) }
+    if (nativeMathConstant) {
+        scope.doWithState {
+            terminateAsUnsupported(reason = "Writing readonly native Math constants is not modeled")
+        }
+        return TsIntrinsicFieldResult.Stopped
+    }
+
     val regularExpression = intrinsicRegExpReference(scope, instance)
     if (regularExpression != null) {
         return TsIntrinsicFieldResult.from(writeRegExpField(scope, regularExpression, field.name, value))

usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt

@@ -55,7 +55,7 @@ class TsMachineFailurePrefixTest {
         assertFalse(result.engineFailed)
         assertTrue(result.runtimeLimited)
         assertTrue(result.states.isEmpty())
-        assertTrue(result.unsupportedPaths.any { "GLOBAL_BINDING_NOT_MODELED" in it && "Math" in it })
+        assertTrue(result.unsupportedPaths.any { "GLOBAL_BINDING_NOT_MODELED" in it && "JSON" in it })
         assertTrue(prefixes.isNotEmpty())
         assertTrue(prefixes.all { !it.pathConstraints.isFalse && it.models.isNotEmpty() })
         assertTrue(prefixes.all { it.unsupportedReason != null && it.engineFailureReason == null })

usvm-ts/src/test/kotlin/org/usvm/machine/expr/NativeMathIdentityTest.kt

@@ -0,0 +1,120 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsMethod
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+class NativeMathIdentityTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    override val scene = loadScene("/models/NativeMathIdentity.ts")
+
+    override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, machineOptions ->
+        TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+    }
+
+    init {
+        options = options.copy(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            stopOnCoverage = 0,
+            throwExceptionOnStepFailure = true,
+        )
+    }
+
+    @Test
+    fun `module initializer reads exact native Math PI`() {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method(name = "initializedConstant"),
+            { result -> result.number == Math.PI / 180 },
+            invariants = arrayOf({ result -> result.number == Math.PI / 180 }),
+        )
+    }
+
+    @Test
+    fun `closure sees the native Math global`() {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method(name = "closureConstant"),
+            { result -> result.number == Math.PI },
+            invariants = arrayOf({ result -> result.number == Math.PI }),
+        )
+    }
+
+    @Test
+    fun `native Math aliases share one ordinary object and exact constants`() {
+        for (name in listOf("aliasIdentity", "constants")) {
+            discoverProperties<TsTestValue.TsNumber>(
+                method = method(name = name),
+                { result -> result.number == 1.0 },
+                invariants = arrayOf({ result -> result.number == 1.0 }),
+            )
+        }
+    }
+
+    @Test
+    fun `source local and parameter bindings named Math retain their own fields`() {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method(name = "localShadow"),
+            { result -> result.number == 17.0 },
+            invariants = arrayOf({ result -> result.number == 17.0 }),
+        )
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method(name = "parameterShadow"),
+            { result -> result.number == 19.0 },
+            invariants = arrayOf({ result -> result.number == 19.0 }),
+        )
+    }
+
+    @Test
+    fun `native constant descriptor mutations remain explicit unsupported operations`() {
+        for (name in listOf("writeConstant", "deleteConstant")) {
+            val outcome = TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine ->
+                machine.analyzeWithOutcome(methods = listOf(method(name = name)))
+            }
+
+            assertTrue(outcome.states.isEmpty(), name)
+            assertEquals(1, outcome.unsupportedPaths.size, name)
+            assertTrue(outcome.unsupportedPaths.single().contains("readonly native Math constants"), name)
+        }
+    }
+
+    @Test
+    fun `native JavaScript confirms initialized constants alias identity and shadowing`() {
+        val source = getResourcePath("/models/NativeMathIdentity.ts").readText()
+        val checks = """
+            if (NativeMathIdentity.initializedConstant() !== Math.PI / 180) throw Error("module constant");
+            if (NativeMathIdentity.closureConstant() !== Math.PI) throw Error("closure constant");
+            if (NativeMathIdentity.aliasIdentity() !== 1) throw Error("alias identity");
+            if (NativeMathIdentity.constants() !== 1) throw Error("native constants");
+            if (NativeMathIdentity.localShadow() !== 17) throw Error("local shadow");
+            if (NativeMathIdentity.parameterShadow() !== 19) throw Error("parameter shadow");
+        """.trimIndent()
+
+        assertNodeReplay(
+            source = source + checks,
+            directory = directory,
+            name = "native-math-identity",
+            timeoutMessage = "Native Math identity replay timed out",
+        )
+    }
+
+    private fun method(name: String) = getMethod(methodName = name, className = "NativeMathIdentity")
+}

usvm-ts/src/test/resources/models/NativeMathIdentity.ts

@@ -0,0 +1,50 @@
+export const nativeDegreesToRadians = Math.PI / 180;
+const nativePi = () => Math.PI;
+
+export class NativeMathIdentity {
+    static initializedConstant(): number {
+        return nativeDegreesToRadians;
+    }
+
+    static closureConstant(): number {
+        return nativePi();
+    }
+
+    static aliasIdentity(): number {
+        const numeric = Math;
+        return numeric === Math && typeof numeric === "object" ? 1 : 0;
+    }
+
+    static constants(): number {
+        return Math.E === 2.718281828459045 &&
+            Math.LN10 === 2.302585092994046 && Math.LN2 === 0.6931471805599453 &&
+            Math.LOG10E === 0.4342944819032518 && Math.LOG2E === 1.4426950408889634 &&
+            Math.PI === 3.141592653589793 && Math.SQRT1_2 === 0.7071067811865476 &&
+            Math.SQRT2 === 1.4142135623730951 ? 1 : 0;
+    }
+
+    static localShadow(): number {
+        const Math = { PI: 17 };
+        return Math.PI;
+    }
+
+    static parameterShadow(): number {
+        return NativeMathIdentity.readParameterShadow({ PI: 2 });
+    }
+
+    static readParameterShadow(Math: { PI: number }): number {
+        Math.PI = 19;
+        return Math.PI;
+    }
+
+    static writeConstant(): number {
+        const numeric: any = Math;
+        numeric.PI = 4;
+        return numeric.PI;
+    }
+
+    static deleteConstant(): boolean {
+        const numeric: any = Math;
+        return delete numeric.PI;
+    }
+}

usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts

@@ -1,7 +1,7 @@
-const nativeMath = Math;
+const nativeJson = JSON;
 
 export class UnmodeledGlobalBinding {
     read(): any {
-        return nativeMath;
+        return nativeJson;
     }
 }