[TS] Model Math and Number builtins

usvm-ts-calls/build.gradle.kts

@@ -30,6 +30,7 @@ val toolStatus = providers.exec {
 val generateBuildMetadata = tasks.register("generateBuildMetadata") {
     inputs.property("toolRevision", toolRevision)
     inputs.property("toolStatus", toolStatus)
+    inputs.property("jacodbVersion", Versions.jacodb)
     outputs.dir(generatedBuildMetadataDirectory)
 
     doLast {
@@ -39,7 +40,11 @@ val generateBuildMetadata = tasks.register("generateBuildMetadata") {
             .file("org/usvm/ts/calls/build.properties")
             .asFile
         metadataFile.parentFile.mkdirs()
-        metadataFile.writeText("tool.revision=$buildIdentity\n", Charsets.UTF_8)
+        metadataFile.writeText(
+            "tool.revision=$buildIdentity\n" +
+                "native.frontend.revision=bundled:${Versions.jacodb}\n",
+            Charsets.UTF_8,
+        )
     }
 }
 

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt

@@ -244,16 +244,25 @@ internal object CallsExperimentJson {
 }
 
 internal object CallsBuildIdentity {
-    val toolRevision: String by lazy {
+    private val properties: Properties by lazy {
         val properties = Properties()
         val resource = checkNotNull(javaClass.getResourceAsStream("/org/usvm/ts/calls/build.properties")) {
             "Missing calls build identity"
         }
         resource.use(properties::load)
 
+        properties
+    }
+
+    val toolRevision: String by lazy {
         checkNotNull(properties.getProperty("tool.revision")).takeIf(String::isNotBlank)
             ?: error("Missing tool revision in calls build identity")
     }
+
+    val nativeFrontendRevision: String by lazy {
+        checkNotNull(properties.getProperty("native.frontend.revision")).takeIf(String::isNotBlank)
+            ?: error("Missing native frontend revision in calls build identity")
+    }
 }
 
 internal class CallsExperimentRunner(

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt

@@ -30,9 +30,12 @@ import org.usvm.util.mkRegisterStackLValue
 import java.nio.file.Path
 import kotlin.time.TimeSource
 
-internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
+internal class CurrentTsCallsSymbolicEngine(
+    private val environment: (String) -> String? = System::getenv,
+    private val bundledNativeFrontendRevision: String = CallsBuildIdentity.nativeFrontendRevision,
+) : CallsSymbolicEngine {
     private val verifiedProjects = mutableMapOf<Path, String>()
-    private var verifiedNativeFrontend: Pair<Path, String>? = null
+    private var verifiedNativeFrontendIdentity: String? = null
 
     override fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult {
         val startedAt = TimeSource.Monotonic.markNow()
@@ -248,22 +251,34 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
         diagnostic = diagnostic,
     )
 
-    private fun verifyNativeFrontendOnce(expectedRevision: String) {
-        require(System.getenv("ETS_FRONTEND_SCRIPT") == null) {
+    internal fun verifyNativeFrontendOnce(expectedRevision: String) {
+        val configuredScript = environment("ETS_FRONTEND_SCRIPT")
+        require(configuredScript == null) {
             "ETS_FRONTEND_SCRIPT must be unset so the frozen native frontend runtime is used"
         }
-        val configuredFrontend = requireNotNull(System.getenv("ETS_FRONTEND_DIR")) {
+        if (expectedRevision.startsWith(BUNDLED_FRONTEND_PREFIX)) {
+            require(environment("ETS_FRONTEND_DIR") == null) {
+                "ETS_FRONTEND_DIR must be unset when the bundled native frontend is selected"
+            }
+            require(expectedRevision == bundledNativeFrontendRevision) {
+                "Bundled native frontend revision $expectedRevision does not match running build " +
+                    bundledNativeFrontendRevision
+            }
+            verifiedNativeFrontendIdentity = expectedRevision
+            return
+        }
+
+        val configuredFrontend = requireNotNull(environment("ETS_FRONTEND_DIR")) {
             "ETS_FRONTEND_DIR is required to verify the frozen native frontend revision"
         }
         val frontendDirectory = Path.of(configuredFrontend).toRealPath()
-        val cached = verifiedNativeFrontend
-        val expectedIdentity = expectedRevision
-        if (cached == Pair(frontendDirectory, expectedIdentity)) {
+        val expectedIdentity = "$frontendDirectory@$expectedRevision"
+        if (verifiedNativeFrontendIdentity == expectedIdentity) {
             return
         }
 
         verifyCallsGitCheckout(frontendDirectory, expectedRevision)
-        verifiedNativeFrontend = frontendDirectory to expectedIdentity
+        verifiedNativeFrontendIdentity = expectedIdentity
     }
 
     private fun verifyGitCheckoutOnce(
@@ -296,6 +311,10 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
         val stopReason: TsAnalysisStopReason,
         val unsupportedPaths: List<String>,
     )
+
+    private companion object {
+        const val BUNDLED_FRONTEND_PREFIX: String = "bundled:"
+    }
 }
 
 internal data class SourceStatementEntry(

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt

@@ -0,0 +1,33 @@
+package org.usvm.ts.calls
+
+import kotlin.test.Test
+import kotlin.test.assertFailsWith
+
+class CurrentTsCallsSymbolicEngineTest {
+    @Test
+    fun `bundled frontend accepts only the revision baked into the running build`() {
+        val engine = CurrentTsCallsSymbolicEngine(
+            environment = emptyMap<String, String>()::get,
+            bundledNativeFrontendRevision = "bundled:published-jacodb",
+        )
+
+        engine.verifyNativeFrontendOnce(expectedRevision = "bundled:published-jacodb")
+
+        assertFailsWith<IllegalArgumentException> {
+            engine.verifyNativeFrontendOnce(expectedRevision = "bundled:different-jacodb")
+        }
+    }
+
+    @Test
+    fun `bundled frontend rejects native frontend environment overrides`() {
+        val environment = mapOf("ETS_FRONTEND_DIR" to "/unused/frontend")
+        val engine = CurrentTsCallsSymbolicEngine(
+            environment = environment::get,
+            bundledNativeFrontendRevision = "bundled:published-jacodb",
+        )
+
+        assertFailsWith<IllegalArgumentException> {
+            engine.verifyNativeFrontendOnce(expectedRevision = "bundled:published-jacodb")
+        }
+    }
+}

usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt

@@ -0,0 +1,43 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsAnyType
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsLocal
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
+import org.jacodb.ets.model.EtsUnknownType
+import org.jacodb.ets.model.EtsValue
+
+internal fun hasBuiltinGlobalOwner(
+    owner: EtsValue,
+    callee: EtsMethodSignature,
+    expectedName: String,
+): Boolean = owner.type.isBuiltinGlobalType(expectedName) ||
+    owner.isLegacyBuiltinGlobal(expectedName = expectedName, callee = callee)
+
+internal fun EtsType.isBuiltinGlobalType(expectedName: String): Boolean = when (expectedName) {
+    "Math" -> this is EtsUnclearRefType && name == expectedName
+    "Number" -> this is EtsFunctionType && isBuiltinNumberType()
+    else -> false
+}
+
+private fun EtsFunctionType.isBuiltinNumberType(): Boolean {
+    val parameter = signature.parameters.singleOrNull() ?: return false
+    return signature.enclosingClass == EtsClassSignature.UNKNOWN &&
+        signature.name.isEmpty() &&
+        signature.returnType == EtsNumberType &&
+        parameter.type == EtsAnyType &&
+        parameter.isOptional &&
+        !parameter.isRest
+}
+
+private fun EtsValue.isLegacyBuiltinGlobal(
+    expectedName: String,
+    callee: EtsMethodSignature,
+): Boolean = this is EtsLocal &&
+    name == expectedName &&
+    type == EtsUnknownType &&
+    callee.enclosingClass == EtsClassSignature.UNKNOWN.copy(name = expectedName)