diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt index cb1fadef65..01cf76b348 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt +++ b/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" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/NativeMathGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/NativeMathGlobal.kt new file mode 100644 index 0000000000..c961b7afae --- /dev/null +++ b/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 +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt index d339e86b2f..f662660ff8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadGlobal.kt +++ b/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( 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 f09bbdb844..8455576426 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 @@ -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? { + if (local.name == "Math") { + val currentMethod = scope.calcOnState { lastEnteredMethod } + val sourceParameter = currentMethod.parameters.any { it.name == local.name } + val sourceAssignment = currentMethod.cfg.stmts.filterIsInstance() + .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) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt index 26c84ff885..47f9581a6c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt @@ -51,6 +51,14 @@ internal fun TsContext.tryWriteIntrinsicField( field: EtsFieldSignature, value: UExpr<*>, ): TsIntrinsicFieldResult { + 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)) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt index a92c330a3f..6d8f29397f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineFailurePrefixTest.kt +++ b/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 }) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NativeMathIdentityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NativeMathIdentityTest.kt new file mode 100644 index 0000000000..68f933d0b3 --- /dev/null +++ b/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 = { 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( + 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( + 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( + 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( + method = method(name = "localShadow"), + { result -> result.number == 17.0 }, + invariants = arrayOf({ result -> result.number == 17.0 }), + ) + discoverProperties( + 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") +} diff --git a/usvm-ts/src/test/resources/models/NativeMathIdentity.ts b/usvm-ts/src/test/resources/models/NativeMathIdentity.ts new file mode 100644 index 0000000000..8cfe9f946d --- /dev/null +++ b/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; + } +} diff --git a/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts b/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts index 6dd7305e5d..2eac07f0ff 100644 --- a/usvm-ts/src/test/resources/models/UnmodeledGlobalBinding.ts +++ b/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; } }