From 94e8f2b4cf2187e7cb49a73e799da94fe0145122 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 02:25:10 +0300 Subject: [PATCH 1/2] [TS Calls] Execute TypeScript semantic models --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 18 +- .../machine/call/TsEtsIrUnknownCallModels.kt | 200 ++++++++++++++++ .../call/TsIntrinsicUnknownCallModels.kt | 1 + .../usvm/machine/call/TsUnknownCallModel.kt | 15 ++ .../call/TsUnknownCallModelRegistry.kt | 19 ++ .../usvm/machine/call/TsUnknownCallProfile.kt | 9 + .../usvm/machine/interpreter/TsInterpreter.kt | 1 + .../kotlin/org/usvm/machine/state/TsState.kt | 15 ++ .../org/usvm/machine/state/TsStateUtils.kt | 1 + .../TsEtsIrUnknownCallModelArtifactTest.kt | 82 +++++++ .../TsEtsIrUnknownCallModelExecutionTest.kt | 226 ++++++++++++++++++ .../call/TsUnknownCallModelRegistryTest.kt | 1 + .../models/EtsIrSemanticModelCalls.ts | 42 ++++ .../resources/models/EtsIrSemanticModels.ts | 39 +++ 14 files changed, 665 insertions(+), 4 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt create mode 100644 usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts create mode 100644 usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index eca353f534..4d85db6a93 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -48,10 +48,6 @@ class TsMachine( unknownCallDispatcher: TsUnknownCallDispatcher? = null, unknownCallModelProvider: TsUnknownCallModelProvider? = null, ) : UMachine() { - private val graph = TsGraph(scene) - private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) - private val components = TsComponents(typeSystem, options) - private val ctx = TsContext(scene, components) private val frozenUnknownCallModels = when { unknownCallDispatcher != null || unknownCallModelProvider != null -> null else -> TsBuiltInUnknownCallModels.registry.freeze(tsOptions.unknownCallModels.enabledModelIds) @@ -63,6 +59,20 @@ class TsMachine( private val resolvedUnknownCallModelProvider = unknownCallModelProvider ?: frozenUnknownCallModels ?: TsNoUnknownCallModels + private val analysisScene = resolvedUnknownCallModelProvider.additionalSceneFiles + .takeIf { modelFiles -> modelFiles.isNotEmpty() } + ?.let { modelFiles -> + EtsScene( + projectFiles = (scene.projectFiles + modelFiles).distinctBy { file -> file.signature }, + sdkFiles = scene.sdkFiles, + projectName = scene.projectName, + ) + } + ?: scene + private val graph = TsGraph(analysisScene) + private val typeSystem = TsTypeSystem(analysisScene, typeOperationsTimeout = 1.seconds, graph.hierarchy) + private val components = TsComponents(typeSystem, options) + private val ctx = TsContext(analysisScene, components) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( profile = tsOptions.unknownCallProfile, modelProvider = resolvedUnknownCallModelProvider, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt new file mode 100644 index 0000000000..5fd9be1c73 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt @@ -0,0 +1,200 @@ +package org.usvm.machine.call + +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.machine.state.TsState +import org.usvm.machine.state.localsCount +import org.usvm.machine.state.newStmt +import java.nio.file.Path +import java.security.MessageDigest +import kotlin.io.path.deleteIfExists +import kotlin.io.path.inputStream +import kotlin.io.path.readBytes + +private const val BYTE_MASK = 0xff +private val sha256Regex = Regex("[0-9a-f]{64}") + +/** Reproducible native-frontend artifact for one stable TypeScript semantic-model entry point. */ +data class TsEtsIrUnknownCallModelArtifact( + val file: EtsFile, + val entryPoint: EtsMethod, + val sourceHash: String, + val etsIrHash: String, +) { + val implementationKind: TsUnknownCallModelImplementationKind + get() = TsUnknownCallModelImplementationKind.ETS_IR_BODY + + init { + require(sourceHash.matches(sha256Regex)) { "TypeScript model source hash must be a lowercase SHA-256" } + require(etsIrHash.matches(sha256Regex)) { "TypeScript model EtsIR hash must be a lowercase SHA-256" } + } +} + +/** Loads one TypeScript model source with JacoDB's bundled native TypeScript frontend. */ +fun loadEtsIrUnknownCallModelArtifact( + sourcePath: Path, + entryPointClassName: String, + entryPointMethodName: String, +): TsEtsIrUnknownCallModelArtifact { + val sourceHash = sourcePath.readBytes().sha256() + val irPath = generateEtsIR( + projectPath = sourcePath, + isProject = false, + loadEntrypoints = true, + useArkAnalyzerTypeInference = null, + provider = EtsIrProvider.TS_FRONTEND, + ) + + return try { + val irBytes = irPath.readBytes() + val file = irPath.inputStream().use { stream -> + EtsFileDto.loadFromJson(stream).toEtsFile() + } + val entryPointClass = file.allClasses.singleOrNull { it.name == entryPointClassName } + ?: error("Expected one TypeScript model class named $entryPointClassName") + val entryPoint = entryPointClass.methods.singleOrNull { it.name == entryPointMethodName } + ?: error("Expected one TypeScript model entry point named $entryPointClassName::$entryPointMethodName") + + TsEtsIrUnknownCallModelArtifact( + file = file, + entryPoint = entryPoint, + sourceHash = sourceHash, + etsIrHash = irBytes.sha256(), + ) + } finally { + irPath.deleteIfExists() + } +} + +/** Registry handle for a TypeScript semantic model compiled to EtsIR. */ +class TsEtsIrUnknownCallModelImplementation( + val artifact: TsEtsIrUnknownCallModelArtifact, + val domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, +) : TsUnknownCallModelImplementation { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.ETS_IR_BODY + override val fingerprintComponents: List = + listOf( + artifact.entryPoint.signature.enclosingClass.file.toString(), + artifact.entryPoint.signature.toString(), + artifact.sourceHash, + artifact.etsIrHash, + ) + override val additionalSceneFiles: List = listOf(artifact.file) +} + +/** Builds the symbolic guard for inputs supported by one EtsIR model body. */ +fun interface TsEtsIrUnknownCallModelDomainGuard { + fun evaluate( + state: TsState, + call: TsUnknownCall, + inputs: List>, + ): UBoolExpr + + companion object { + val ALWAYS = TsEtsIrUnknownCallModelDomainGuard { state, _, _ -> state.ctx.trueExpr } + } +} + +/** Executes TypeScript semantic-model bodies through the normal EtsIR interpreter. */ +object TsEtsIrUnknownCallModelBackend : TsUnknownCallModelBackend { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.ETS_IR_BODY + + override fun execute( + implementation: TsUnknownCallModelImplementation, + precision: TsUnknownCallModelPrecision, + state: TsState, + call: TsUnknownCall, + ): TsUnknownCallModelExecution { + val etsIrImplementation = requireNotNull(implementation as? TsEtsIrUnknownCallModelImplementation) { + "ETS_IR_BODY backend requires TsEtsIrUnknownCallModelImplementation, got ${implementation::class}" + } + val inputs = call.resolvedInputs() + if (inputs == null || inputs.size != etsIrImplementation.artifact.entryPoint.parameters.size) { + return unsupportedExecution(state = state, precision = precision) + } + + val domainGuard = etsIrImplementation.domainGuard.evaluate( + state = state, + call = call, + inputs = inputs, + ) + val successor = TsUnknownCallModelSuccessor( + guard = domainGuard, + completion = TsUnknownCallModelCompletion.EtsIrBody( + entryPoint = etsIrImplementation.artifact.entryPoint, + inputs = inputs, + ), + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = when (precision) { + TsUnknownCallModelPrecision.EXACT -> null + TsUnknownCallModelPrecision.PARTIAL -> state.ctx.mkNot(domainGuard) + }, + ) + } + + private fun unsupportedExecution( + state: TsState, + precision: TsUnknownCallModelPrecision, + ): TsUnknownCallModelExecution { + check(precision == TsUnknownCallModelPrecision.PARTIAL) { + "Exact EtsIR semantic models require every receiver and argument to be resolved" + } + val unreachableSuccessor = TsUnknownCallModelSuccessor( + guard = state.ctx.falseExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(unreachableSuccessor), + residualGuard = state.ctx.trueExpr, + ) + } +} + +private fun TsUnknownCall.resolvedInputs(): List>? = buildList { + receiver?.let { receiver -> add(receiver.resolved ?: return null) } + arguments.forEach { argument -> add(argument.resolved ?: return null) } +} + +internal fun TsState.enterEtsIrUnknownCallModel( + modelId: String, + entryPoint: EtsMethod, + inputs: List>, + returnSite: EtsStmt, +) { + val modelClass = requireNotNull(entryPoint.enclosingClass) { + "EtsIR semantic-model entry point must belong to a class" + } + val arguments = buildList { + add(getStaticInstance(modelClass)) + addAll(inputs) + } + + check(inputs.size == entryPoint.parameters.size) { + "Expected ${entryPoint.parameters.size} EtsIR model inputs, got ${inputs.size}" + } + + registerCallee(returnSite, entryPoint.cfg) + enterUnknownCallModel(modelId = modelId, entryPoint = entryPoint) + pushSortsForActualArguments(arguments) + callStack.push(entryPoint, returnSite) + memory.stack.push(arguments.toTypedArray(), entryPoint.localsCount) + newStmt(entryPoint.cfg.instructions.first()) +} + +private fun ByteArray.sha256(): String = + MessageDigest.getInstance("SHA-256") + .digest(this) + .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and BYTE_MASK) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt index b0a9838e3f..270658acb2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt @@ -32,6 +32,7 @@ object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { override fun execute( implementation: TsUnknownCallModelImplementation, + precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, ): TsUnknownCallModelExecution { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 9566b54a02..bad987eb44 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -1,5 +1,7 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsType import org.usvm.UBoolExpr import org.usvm.UExpr @@ -8,6 +10,7 @@ import org.usvm.machine.state.TsState /** Identifies the backend that executes a semantic model implementation. */ enum class TsUnknownCallModelImplementationKind { INTRINSIC, + ETS_IR_BODY, } /** Describes the semantic precision of a model within its declared supported domain. */ @@ -56,6 +59,14 @@ sealed interface TsUnknownCallModelCompletion { class Exceptional( val exception: TsState.() -> Pair, EtsType>, ) : TsUnknownCallModelCompletion + + /** Enters a TypeScript model body through the normal EtsIR interpreter. */ + class EtsIrBody( + val entryPoint: EtsMethod, + inputs: List>, + ) : TsUnknownCallModelCompletion { + val inputs: List> = inputs.toList() + } } /** @@ -114,4 +125,8 @@ sealed interface TsUnknownCallModelApplication { /** Selects and executes models without exposing registry or backend details to the dispatcher. */ fun interface TsUnknownCallModelProvider { fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication + + /** EtsIR files that must be merged into the machine scene before analysis starts. */ + val additionalSceneFiles: List + get() = emptyList() } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt index c30456c628..21468b984a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -1,5 +1,6 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsFile import org.usvm.machine.state.TsState import java.nio.ByteBuffer import java.nio.charset.StandardCharsets @@ -10,6 +11,14 @@ private const val BYTE_MASK = 0xff /** Opaque semantic-model implementation selected by its [kind]. */ interface TsUnknownCallModelImplementation { val kind: TsUnknownCallModelImplementationKind + + /** Stable implementation-specific inputs included in the frozen catalog fingerprint. */ + val fingerprintComponents: List + get() = emptyList() + + /** EtsIR files that must be visible to the normal interpreter when this implementation is enabled. */ + val additionalSceneFiles: List + get() = emptyList() } /** Executes opaque model implementations of one [kind]. */ @@ -18,6 +27,7 @@ interface TsUnknownCallModelBackend { fun execute( implementation: TsUnknownCallModelImplementation, + precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, ): TsUnknownCallModelExecution @@ -114,6 +124,9 @@ class TsFrozenUnknownCallModelRegistry internal constructor( ) : TsUnknownCallModelProvider { val descriptors: List = registrations.map { it.descriptor } val fingerprint: String = computeFingerprint(registrations) + override val additionalSceneFiles: List = registrations + .flatMap { registration -> registration.implementation.additionalSceneFiles } + .distinctBy { file -> file.signature } internal fun select(call: TsUnknownCall): TsUnknownCallModelRegistration? { val matches = registrations.filter { it.descriptor.matcher.matches(call) } @@ -128,12 +141,17 @@ class TsFrozenUnknownCallModelRegistry internal constructor( override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { val registration = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + if (state.isUnknownCallModelActive(registration.descriptor.id)) { + return TsUnknownCallModelApplication.NotApplicable + } + val implementationKind = registration.descriptor.implementationKind val backend = checkNotNull(backends[implementationKind]) { "No semantic model backend configured for $implementationKind" } val execution = backend.execute( implementation = registration.implementation, + precision = registration.descriptor.precision, state = state, call = call, ) @@ -152,6 +170,7 @@ private fun computeFingerprint(registrations: List digest.updateLengthPrefixed(registration.descriptor.id) digest.updateLengthPrefixed(registration.descriptor.implementationKind.name) + registration.implementation.fingerprintComponents.forEach(digest::updateLengthPrefixed) } return digest.digest().joinToString(separator = "") { byte -> diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index d24b6164c5..3f41ec0840 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -298,6 +298,15 @@ class TsProfileUnknownCallDispatcher( val (exception, type) = completion.exception(this) methodResult = TsMethodResult.TsException(exception, type) } + + is TsUnknownCallModelCompletion.EtsIrBody -> { + enterEtsIrUnknownCallModel( + modelId = application.modelId, + entryPoint = completion.entryPoint, + inputs = completion.inputs, + returnSite = call.callSite, + ) + } } if (onApplied()) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index cc8e915f6c..7750694a35 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -109,6 +109,7 @@ class TsInterpreter( if (result is TsMethodResult.TsException) { // TODO catch processing scope.doWithState { + leaveUnknownCallModelIfReturning(callStack.lastMethod()) val returnSite = callStack.pop() if (callStack.isNotEmpty()) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 172da63294..8f4d1cc501 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -81,6 +81,7 @@ class TsState( * for identical string values. */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), + private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -118,6 +119,19 @@ class TsState( localToSortStack.removeLast() } + fun isUnknownCallModelActive(modelId: String): Boolean = + activeUnknownCallModels.any { (activeModelId, _) -> activeModelId == modelId } + + fun enterUnknownCallModel(modelId: String, entryPoint: EtsMethod) { + activeUnknownCallModels += modelId to entryPoint + } + + fun leaveUnknownCallModelIfReturning(method: EtsMethod) { + if (activeUnknownCallModels.lastOrNull()?.second == method) { + activeUnknownCallModels.removeLast() + } + } + fun registerCallee(stmt: EtsStmt, cfg: EtsBlockCfg) { val parentId = stmt.location.method.cfg.blocks.indexOfFirst { it.statements.contains(stmt) } .takeIf { it >= 0 } ?: error("Statement $stmt is not found in the method CFG") @@ -294,6 +308,7 @@ class TsState( dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, + activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt index 09ac543689..209ddec8e3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt @@ -14,6 +14,7 @@ fun TsState.newStmt(stmt: EtsStmt) { fun TsState.returnValue(valueToReturn: UExpr) { val returnFromMethod = callStack.lastMethod() + leaveUnknownCallModelIfReturning(returnFromMethod) val returnSite = callStack.pop() if (callStack.isNotEmpty()) { memory.stack.pop() diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt new file mode 100644 index 0000000000..4c7fd781fc --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -0,0 +1,82 @@ +package org.usvm.machine.call + +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertNotEquals +import kotlin.test.assertTrue + +class TsEtsIrUnknownCallModelArtifactTest { + private val sourcePath = getResourcePath("/models/EtsIrSemanticModels.ts") + + @Test + fun `native frontend produces reproducible model artifacts`() { + val first = loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + ) + val second = loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + ) + + assertEquals(TsUnknownCallModelImplementationKind.ETS_IR_BODY, first.implementationKind) + assertEquals("absolute", first.entryPoint.name) + assertEquals(first.entryPoint.signature, second.entryPoint.signature) + assertEquals(first.sourceHash, second.sourceHash) + assertEquals(first.etsIrHash, second.etsIrHash) + assertTrue(first.sourceHash.matches(Regex("[0-9a-f]{64}"))) + assertTrue(first.etsIrHash.matches(Regex("[0-9a-f]{64}"))) + } + + @Test + fun `catalog fingerprint includes source and EtsIR hashes`() { + val artifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + ) + val originalFingerprint = fingerprint( + implementation = TsEtsIrUnknownCallModelImplementation(artifact), + ) + val changedSourceFingerprint = fingerprint( + implementation = TsEtsIrUnknownCallModelImplementation( + artifact.copy(sourceHash = "0".repeat(64)), + ), + ) + val changedIrFingerprint = fingerprint( + implementation = TsEtsIrUnknownCallModelImplementation( + artifact.copy(etsIrHash = "f".repeat(64)), + ), + ) + + assertNotEquals(originalFingerprint, changedSourceFingerprint) + assertNotEquals(originalFingerprint, changedIrFingerprint) + } + + private fun fingerprint(implementation: TsEtsIrUnknownCallModelImplementation): String { + val descriptor = TsUnknownCallModelDescriptor( + id = "test.ets-ir.absolute", + matcher = TsUnknownCallModelMatcher { true }, + supportedDomain = TsUnknownCallModelSupportedDomain( + id = "number", + description = "A resolved numeric argument", + ), + precision = TsUnknownCallModelPrecision.EXACT, + implementationKind = TsUnknownCallModelImplementationKind.ETS_IR_BODY, + ) + val registry = TsUnknownCallModelRegistry( + registrations = listOf( + TsUnknownCallModelRegistration( + descriptor = descriptor, + implementation = implementation, + ), + ), + backends = listOf(TsEtsIrUnknownCallModelBackend), + ) + + return registry.freeze().fingerprint + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt new file mode 100644 index 0000000000..f8a08c26f9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -0,0 +1,226 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsEtsIrUnknownCallModelExecutionTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/EtsIrSemanticModelCalls.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + private val baseArtifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = getResourcePath("/models/EtsIrSemanticModels.ts"), + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + ) + private val modelClass = baseArtifact.file.allClasses.single { it.name == "EtsIrSemanticModels" } + private val models = TsUnknownCallModelRegistry( + registrations = listOf( + registration( + id = "test.ets-ir.absolute", + targetName = "absolute", + entryPointName = "absolute", + ), + registration( + id = "test.ets-ir.increment", + targetName = "modeledIncrement", + entryPointName = "increment", + ), + registration( + id = "test.ets-ir.fail", + targetName = "fail", + entryPointName = "fail", + ), + registration( + id = "test.ets-ir.positive-identity", + targetName = "positiveIdentity", + entryPointName = "positiveIdentity", + precision = TsUnknownCallModelPrecision.PARTIAL, + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + val zero = state.ctx.mkFp(0.0, state.ctx.fp64Sort) + val value = inputs.single().asExpr(state.ctx.fp64Sort) + state.ctx.mkFpLessExpr(zero, value) + }, + ), + registration( + id = "test.ets-ir.outer", + targetName = "outer", + entryPointName = "outer", + ), + registration( + id = "test.ets-ir.double", + targetName = "double", + entryPointName = "double", + ), + registration( + id = "test.ets-ir.recursive", + targetName = "recursive", + entryPointName = "recurse", + ), + ), + backends = listOf(TsEtsIrUnknownCallModelBackend), + ).freeze() + + @Test + fun `pure EtsIR body maps argument and return value`() { + val result = analyze(methodName = "pureArgumentAndReturn") + + assertEquals(42.0, assertIs(result.values.single()).number) + assertEquals(listOf("test.ets-ir.absolute"), result.modelIds) + } + + @Test + fun `stateful EtsIR body maps receiver argument state and return alias`() { + val result = analyze(methodName = "receiverStateArgumentAndAlias") + + assertEquals(42.0, assertIs(result.values.single()).number) + assertEquals(listOf("test.ets-ir.increment"), result.modelIds) + } + + @Test + fun `exception from EtsIR body propagates through original call`() { + val result = analyze(methodName = "exception") + + assertTrue(result.values.single() is TsTestValue.TsException) + assertIs(result.states.single().methodResult) + assertEquals(listOf("test.ets-ir.fail"), result.modelIds) + } + + @Test + fun `unsupported input uses configured residual fallback`() { + val result = analyze(methodName = "unsupportedInput") + + assertTrue(result.states.isEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map { it.outcome }) + assertIs(result.events.single().decision) + } + + @Test + fun `unknown call inside EtsIR body uses the same dispatcher`() { + val result = analyze(methodName = "nestedUnknownCall") + + assertEquals(42.0, assertIs(result.values.single()).number) + assertEquals(listOf("test.ets-ir.outer", "test.ets-ir.double"), result.modelIds) + } + + @Test + fun `recursive model redirection uses residual fallback instead of looping`() { + val result = analyze(methodName = "recursiveRedirection") + + assertTrue(result.states.isEmpty()) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.PATH_STOPPED), + result.events.map { it.outcome }, + ) + assertIs(result.events.last().decision) + } + + private fun registration( + id: String, + targetName: String, + entryPointName: String, + precision: TsUnknownCallModelPrecision = TsUnknownCallModelPrecision.EXACT, + domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, + ): TsUnknownCallModelRegistration { + val artifact = baseArtifact.copy( + entryPoint = modelClass.methods.single { it.name == entryPointName }, + ) + val descriptor = TsUnknownCallModelDescriptor( + id = id, + matcher = TsUnknownCallModelMatcher { call -> call.callee.name == targetName }, + supportedDomain = TsUnknownCallModelSupportedDomain( + id = "$targetName-resolved-inputs", + description = "Resolved receiver and arguments accepted by $entryPointName", + ), + precision = precision, + implementationKind = TsUnknownCallModelImplementationKind.ETS_IR_BODY, + ) + + return TsUnknownCallModelRegistration( + descriptor = descriptor, + implementation = TsEtsIrUnknownCallModelImplementation( + artifact = artifact, + domainGuard = domainGuard, + ), + ) + } + + private fun analyze(methodName: String): AnalysisResult { + val method = method(methodName) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP), + observer = observer, + unknownCallModelProvider = models, + ).use { machine -> + val states = machine.analyze(listOf(method)) + val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue } + + AnalysisResult( + states = states, + values = values, + events = observer.events.toList(), + ) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "EtsIrSemanticModelCalls" } + .methods + .single { it.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val states: List, + val values: List, + val events: List, + ) { + val modelIds: List + get() = events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt index 6684cce0f3..83adf28cca 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -145,6 +145,7 @@ class TsUnknownCallModelRegistryTest { override fun execute( implementation: TsUnknownCallModelImplementation, + precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, ): TsUnknownCallModelExecution = error("Fake backend must not execute in registry metadata tests") diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts new file mode 100644 index 0000000000..38ce413db6 --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -0,0 +1,42 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +declare class ExternalModels { + static absolute(value: number): number; + static fail(value: number): number; + static positiveIdentity(value: number): number; + static outer(value: number): number; + static recursive(value: number): number; +} + +export class EtsIrSemanticModelCalls { + pureArgumentAndReturn(): number { + return ExternalModels.absolute(-42); + } + + receiverStateArgumentAndAlias(): number { + const receiver = [40]; + const alias = receiver.modeledIncrement(2); + if (alias === receiver) { + return receiver[0]; + } + + return 0; + } + + exception(): number { + return ExternalModels.fail(7); + } + + unsupportedInput(): number { + return ExternalModels.positiveIdentity(-1); + } + + nestedUnknownCall(): number { + return ExternalModels.outer(21); + } + + recursiveRedirection(): number { + return ExternalModels.recursive(1); + } +} diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts new file mode 100644 index 0000000000..15f7186af1 --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts @@ -0,0 +1,39 @@ +export class EtsIrSemanticModels { + static absolute(value: number): number { + if (value < 0) { + return -value; + } + + return value; + } + + static increment(receiver: number[], delta: number): number[] { + receiver[0] = receiver[0] + delta; + return receiver; + } + + static fail(value: number): number { + throw value; + } + + static positiveIdentity(value: number): number { + return value; + } + + static outer(value: number): number { + return ExternalModels.double(value); + } + + static double(value: number): number { + return value * 2; + } + + static recurse(value: number): number { + return ExternalModels.recursive(value); + } +} + +declare class ExternalModels { + static double(value: number): number; + static recursive(value: number): number; +} From 26b63f37161a6f3735b1518c1aca28c2710e7281 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 02:50:53 +0300 Subject: [PATCH 2/2] [TS Calls] Harden TypeScript semantic model execution --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 3 +- .../machine/call/TsEtsIrUnknownCallModels.kt | 77 +++++++++++++------ .../call/TsIntrinsicUnknownCallModels.kt | 6 +- .../call/TsUnknownCallModelRegistry.kt | 45 +++++++++-- .../kotlin/org/usvm/machine/state/TsState.kt | 10 ++- .../TsEtsIrUnknownCallModelArtifactTest.kt | 65 ++++++++++++++++ .../TsEtsIrUnknownCallModelExecutionTest.kt | 48 ++++++++++-- .../call/TsUnknownCallModelRegistryTest.kt | 76 +++++++++++++++++- .../models/EtsIrSemanticModelCalls.ts | 14 ++++ .../resources/models/EtsIrSemanticModels.ts | 9 +++ 10 files changed, 306 insertions(+), 47 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 4d85db6a93..c622fb2f22 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -14,6 +14,7 @@ import org.usvm.machine.call.TsNoUnknownCallModels import org.usvm.machine.call.TsProfileUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallModelProvider +import org.usvm.machine.call.deduplicateEtsFilesBySignature import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -63,7 +64,7 @@ class TsMachine( .takeIf { modelFiles -> modelFiles.isNotEmpty() } ?.let { modelFiles -> EtsScene( - projectFiles = (scene.projectFiles + modelFiles).distinctBy { file -> file.signature }, + projectFiles = (scene.projectFiles + modelFiles).deduplicateEtsFilesBySignature(), sdkFiles = scene.sdkFiles, projectName = scene.projectName, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt index 5fd9be1c73..a77e7b2ac8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt @@ -42,17 +42,35 @@ fun loadEtsIrUnknownCallModelArtifact( sourcePath: Path, entryPointClassName: String, entryPointMethodName: String, +): TsEtsIrUnknownCallModelArtifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = entryPointClassName, + entryPointMethodName = entryPointMethodName, + generateIr = { path -> + generateEtsIR( + projectPath = path, + isProject = false, + loadEntrypoints = true, + useArkAnalyzerTypeInference = null, + provider = EtsIrProvider.TS_FRONTEND, + ) + }, +) + +internal fun loadEtsIrUnknownCallModelArtifact( + sourcePath: Path, + entryPointClassName: String, + entryPointMethodName: String, + generateIr: (Path) -> Path, ): TsEtsIrUnknownCallModelArtifact { - val sourceHash = sourcePath.readBytes().sha256() - val irPath = generateEtsIR( - projectPath = sourcePath, - isProject = false, - loadEntrypoints = true, - useArkAnalyzerTypeInference = null, - provider = EtsIrProvider.TS_FRONTEND, - ) + val sourceBytes = sourcePath.readBytes() + val irPath = generateIr(sourcePath) return try { + check(sourcePath.readBytes().contentEquals(sourceBytes)) { + "TypeScript model source changed while generating EtsIR: $sourcePath" + } + val irBytes = irPath.readBytes() val file = irPath.inputStream().use { stream -> EtsFileDto.loadFromJson(stream).toEtsFile() @@ -61,11 +79,17 @@ fun loadEtsIrUnknownCallModelArtifact( ?: error("Expected one TypeScript model class named $entryPointClassName") val entryPoint = entryPointClass.methods.singleOrNull { it.name == entryPointMethodName } ?: error("Expected one TypeScript model entry point named $entryPointClassName::$entryPointMethodName") + check(entryPoint.isStatic) { + "TypeScript model entry point $entryPointClassName::$entryPointMethodName must be static" + } + check(entryPoint.cfg.instructions.isNotEmpty()) { + "TypeScript model entry point $entryPointClassName::$entryPointMethodName must have a body" + } TsEtsIrUnknownCallModelArtifact( file = file, entryPoint = entryPoint, - sourceHash = sourceHash, + sourceHash = sourceBytes.sha256(), etsIrHash = irBytes.sha256(), ) } finally { @@ -113,13 +137,18 @@ object TsEtsIrUnknownCallModelBackend : TsUnknownCallModelBackend { precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, - ): TsUnknownCallModelExecution { + ): TsUnknownCallModelBackendResult { val etsIrImplementation = requireNotNull(implementation as? TsEtsIrUnknownCallModelImplementation) { "ETS_IR_BODY backend requires TsEtsIrUnknownCallModelImplementation, got ${implementation::class}" } val inputs = call.resolvedInputs() if (inputs == null || inputs.size != etsIrImplementation.artifact.entryPoint.parameters.size) { - return unsupportedExecution(state = state, precision = precision) + return when (precision) { + TsUnknownCallModelPrecision.EXACT -> TsUnknownCallModelBackendResult.NotApplicable + TsUnknownCallModelPrecision.PARTIAL -> TsUnknownCallModelBackendResult.Executed( + execution = unsupportedExecution(state), + ) + } } val domainGuard = etsIrImplementation.domainGuard.evaluate( @@ -127,6 +156,10 @@ object TsEtsIrUnknownCallModelBackend : TsUnknownCallModelBackend { call = call, inputs = inputs, ) + if (precision == TsUnknownCallModelPrecision.EXACT && domainGuard != state.ctx.trueExpr) { + return TsUnknownCallModelBackendResult.NotApplicable + } + val successor = TsUnknownCallModelSuccessor( guard = domainGuard, completion = TsUnknownCallModelCompletion.EtsIrBody( @@ -135,22 +168,18 @@ object TsEtsIrUnknownCallModelBackend : TsUnknownCallModelBackend { ), ) - return TsUnknownCallModelExecution( - successors = listOf(successor), - residualGuard = when (precision) { - TsUnknownCallModelPrecision.EXACT -> null - TsUnknownCallModelPrecision.PARTIAL -> state.ctx.mkNot(domainGuard) - }, + return TsUnknownCallModelBackendResult.Executed( + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = when (precision) { + TsUnknownCallModelPrecision.EXACT -> null + TsUnknownCallModelPrecision.PARTIAL -> state.ctx.mkNot(domainGuard) + }, + ), ) } - private fun unsupportedExecution( - state: TsState, - precision: TsUnknownCallModelPrecision, - ): TsUnknownCallModelExecution { - check(precision == TsUnknownCallModelPrecision.PARTIAL) { - "Exact EtsIR semantic models require every receiver and argument to be resolved" - } + private fun unsupportedExecution(state: TsState): TsUnknownCallModelExecution { val unreachableSuccessor = TsUnknownCallModelSuccessor( guard = state.ctx.falseExpr, completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt index 270658acb2..a5b3991074 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt @@ -35,12 +35,14 @@ object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, - ): TsUnknownCallModelExecution { + ): TsUnknownCallModelBackendResult { val intrinsic = requireNotNull(implementation as? TsIntrinsicUnknownCallModelImplementation) { "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}" } - return intrinsic.model.execute(state = state, call = call) + return TsUnknownCallModelBackendResult.Executed( + execution = intrinsic.model.execute(state = state, call = call), + ) } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt index 21468b984a..5b726990c6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature import org.usvm.machine.state.TsState import java.nio.ByteBuffer import java.nio.charset.StandardCharsets @@ -30,7 +31,16 @@ interface TsUnknownCallModelBackend { precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, - ): TsUnknownCallModelExecution + ): TsUnknownCallModelBackendResult +} + +/** Result of attempting to execute one selected backend implementation. */ +sealed interface TsUnknownCallModelBackendResult { + data class Executed( + val execution: TsUnknownCallModelExecution, + ) : TsUnknownCallModelBackendResult + + data object NotApplicable : TsUnknownCallModelBackendResult } /** Binds backend-neutral model metadata to an opaque backend implementation. */ @@ -126,7 +136,7 @@ class TsFrozenUnknownCallModelRegistry internal constructor( val fingerprint: String = computeFingerprint(registrations) override val additionalSceneFiles: List = registrations .flatMap { registration -> registration.implementation.additionalSceneFiles } - .distinctBy { file -> file.signature } + .deduplicateEtsFilesBySignature() internal fun select(call: TsUnknownCall): TsUnknownCallModelRegistration? { val matches = registrations.filter { it.descriptor.matcher.matches(call) } @@ -149,21 +159,40 @@ class TsFrozenUnknownCallModelRegistry internal constructor( val backend = checkNotNull(backends[implementationKind]) { "No semantic model backend configured for $implementationKind" } - val execution = backend.execute( + val backendResult = backend.execute( implementation = registration.implementation, precision = registration.descriptor.precision, state = state, call = call, ) - return TsUnknownCallModelApplication.Applied( - modelId = registration.descriptor.id, - precision = registration.descriptor.precision, - execution = execution, - ) + return when (backendResult) { + is TsUnknownCallModelBackendResult.Executed -> TsUnknownCallModelApplication.Applied( + modelId = registration.descriptor.id, + precision = registration.descriptor.precision, + execution = backendResult.execution, + ) + + TsUnknownCallModelBackendResult.NotApplicable -> TsUnknownCallModelApplication.NotApplicable + } } } +internal fun Iterable.deduplicateEtsFilesBySignature(): List { + val filesBySignature = linkedMapOf() + + for (file in this) { + val existingFile = filesBySignature[file.signature] + require(existingFile == null || existingFile === file) { + "Conflicting EtsIR files share signature ${file.signature}" + } + + filesBySignature.putIfAbsent(file.signature, file) + } + + return filesBySignature.values.toList() +} + private fun computeFingerprint(registrations: List): String { val digest = MessageDigest.getInstance("SHA-256") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 8f4d1cc501..f24e8ef3bf 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -81,7 +81,7 @@ class TsState( * for identical string values. */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), - private val activeUnknownCallModels: MutableList> = mutableListOf(), + private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, initOwnership = ownership, @@ -120,14 +120,16 @@ class TsState( } fun isUnknownCallModelActive(modelId: String): Boolean = - activeUnknownCallModels.any { (activeModelId, _) -> activeModelId == modelId } + activeUnknownCallModels.any { (activeModelId, _, _) -> activeModelId == modelId } fun enterUnknownCallModel(modelId: String, entryPoint: EtsMethod) { - activeUnknownCallModels += modelId to entryPoint + val entryCallDepth = callStack.size + 1 + activeUnknownCallModels += Triple(modelId, entryPoint, entryCallDepth) } fun leaveUnknownCallModelIfReturning(method: EtsMethod) { - if (activeUnknownCallModels.lastOrNull()?.second == method) { + val activeModel = activeUnknownCallModels.lastOrNull() + if (activeModel?.second == method && activeModel.third == callStack.size) { activeUnknownCallModels.removeLast() } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt index 4c7fd781fc..6666171446 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -1,8 +1,16 @@ package org.usvm.machine.call +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR import org.usvm.util.getResourcePath +import kotlin.io.path.copyTo +import kotlin.io.path.createTempFile +import kotlin.io.path.deleteIfExists +import kotlin.io.path.readBytes +import kotlin.io.path.writeBytes import kotlin.test.Test import kotlin.test.assertEquals +import kotlin.test.assertFailsWith import kotlin.test.assertNotEquals import kotlin.test.assertTrue @@ -56,6 +64,63 @@ class TsEtsIrUnknownCallModelArtifactTest { assertNotEquals(originalFingerprint, changedIrFingerprint) } + @Test + fun `loader rejects source changed while EtsIR is generated`() { + val mutableSourcePath = createTempFile(prefix = "EtsIrSemanticModels", suffix = ".ts") + sourcePath.copyTo(mutableSourcePath, overwrite = true) + + try { + val error = assertFailsWith { + loadEtsIrUnknownCallModelArtifact( + sourcePath = mutableSourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + generateIr = { path -> + val irPath = generateEtsIR( + projectPath = path, + isProject = false, + loadEntrypoints = true, + useArkAnalyzerTypeInference = null, + provider = EtsIrProvider.TS_FRONTEND, + ) + path.writeBytes(path.readBytes() + byteArrayOf('\n'.code.toByte())) + irPath + }, + ) + } + + assertTrue(error.message.orEmpty().contains("changed while generating EtsIR")) + } finally { + mutableSourcePath.deleteIfExists() + } + } + + @Test + fun `loader rejects instance entry points`() { + val error = assertFailsWith { + loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "instanceIdentity", + ) + } + + assertTrue(error.message.orEmpty().contains("must be static")) + } + + @Test + fun `loader rejects declaration-only entry points`() { + val error = assertFailsWith { + loadEtsIrUnknownCallModelArtifact( + sourcePath = getResourcePath("/models/EtsIrSemanticModelCalls.ts"), + entryPointClassName = "ExternalModels", + entryPointMethodName = "absolute", + ) + } + + assertTrue(error.message.orEmpty().contains("must have a body")) + } + private fun fingerprint(implementation: TsEtsIrUnknownCallModelImplementation): String { val descriptor = TsUnknownCallModelDescriptor( id = "test.ets-ir.absolute", diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt index f8a08c26f9..556bfaf2b1 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -56,11 +56,23 @@ class TsEtsIrUnknownCallModelExecutionTest { targetName = "positiveIdentity", entryPointName = "positiveIdentity", precision = TsUnknownCallModelPrecision.PARTIAL, - domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> - val zero = state.ctx.mkFp(0.0, state.ctx.fp64Sort) - val value = inputs.single().asExpr(state.ctx.fp64Sort) - state.ctx.mkFpLessExpr(zero, value) - }, + domainGuard = positiveInputGuard, + ), + registration( + id = "test.ets-ir.exact-positive-identity", + targetName = "exactPositiveIdentity", + entryPointName = "positiveIdentity", + domainGuard = positiveInputGuard, + ), + registration( + id = "test.ets-ir.arity-mismatch", + targetName = "arityMismatch", + entryPointName = "positiveIdentity", + ), + registration( + id = "test.ets-ir.unresolved-argument", + targetName = "unresolvedExactInput", + entryPointName = "positiveIdentity", ), registration( id = "test.ets-ir.outer", @@ -115,6 +127,26 @@ class TsEtsIrUnknownCallModelExecutionTest { assertIs(result.events.single().decision) } + @Test + fun `unsupported exact model inputs use configured residual fallback`() { + val unsupportedMethods = listOf( + "exactGuardRejectsInput", + "exactArityMismatch", + "exactUnresolvedArgument", + ) + + unsupportedMethods.forEach { methodName -> + val result = analyze(methodName = methodName) + + assertEquals( + listOf(TsUnknownCallOutcome.PATH_STOPPED), + result.events.map { it.outcome }, + methodName, + ) + assertIs(result.events.single().decision, methodName) + } + } + @Test fun `unknown call inside EtsIR body uses the same dispatcher`() { val result = analyze(methodName = "nestedUnknownCall") @@ -212,6 +244,12 @@ class TsEtsIrUnknownCallModelExecutionTest { } private companion object { + val positiveInputGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + val zero = state.ctx.mkFp(0.0, state.ctx.fp64Sort) + val value = inputs.single().asExpr(state.ctx.fp64Sort) + state.ctx.mkFpLessExpr(zero, value) + } + val machineOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), stateCollectionStrategy = StateCollectionStrategy.ALL, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt index 83adf28cca..e79a25c083 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -1,6 +1,12 @@ package org.usvm.machine.call import io.mockk.mockk +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions import org.usvm.machine.state.TsState import kotlin.test.Test import kotlin.test.assertEquals @@ -110,12 +116,68 @@ class TsUnknownCallModelRegistryTest { assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) } + @Test + fun `same model EtsIR file reference is included once`() { + val modelFile = etsFile(fileName = "model.ts") + val registry = TsUnknownCallModelRegistry( + registrations = listOf( + registration(id = "a", implementation = FakeImplementation(listOf(modelFile))), + registration(id = "b", implementation = FakeImplementation(listOf(modelFile))), + ), + backends = listOf(FakeBackend), + ).freeze() + + assertEquals(listOf(modelFile), registry.additionalSceneFiles) + } + + @Test + fun `distinct model EtsIR files with the same signature are rejected`() { + val first = etsFile(fileName = "model.ts") + val second = etsFile(fileName = "model.ts") + + val error = assertFailsWith { + TsUnknownCallModelRegistry( + registrations = listOf( + registration(id = "a", implementation = FakeImplementation(listOf(first))), + registration(id = "b", implementation = FakeImplementation(listOf(second))), + ), + backends = listOf(FakeBackend), + ).freeze() + } + + assertEquals("Conflicting EtsIR files share signature @test/model", error.message) + } + + @Test + fun `application and model EtsIR files with the same signature are rejected`() { + val applicationFile = etsFile(fileName = "shared.ts") + val modelFile = etsFile(fileName = "shared.ts") + val modelProvider = object : TsUnknownCallModelProvider { + override val additionalSceneFiles: List = listOf(modelFile) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication = + error("Model provider must not execute while constructing a machine") + } + + val error = assertFailsWith { + TsMachine( + scene = EtsScene(projectFiles = listOf(applicationFile)), + options = UMachineOptions(), + tsOptions = TsOptions(), + unknownCallModelProvider = modelProvider, + ) + } + + assertEquals("Conflicting EtsIR files share signature @test/shared", error.message) + } + private fun registration( id: String, matches: Boolean = true, + implementation: TsUnknownCallModelImplementation = FakeImplementation(), ) = TsUnknownCallModelRegistration( descriptor = descriptor(id = id, matches = matches), - implementation = FakeImplementation, + implementation = implementation, ) private fun descriptor( @@ -134,7 +196,9 @@ class TsUnknownCallModelRegistryTest { implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, ) - private object FakeImplementation : TsUnknownCallModelImplementation { + private class FakeImplementation( + override val additionalSceneFiles: List = emptyList(), + ) : TsUnknownCallModelImplementation { override val kind: TsUnknownCallModelImplementationKind = TsUnknownCallModelImplementationKind.INTRINSIC } @@ -148,6 +212,12 @@ class TsUnknownCallModelRegistryTest { precision: TsUnknownCallModelPrecision, state: TsState, call: TsUnknownCall, - ): TsUnknownCallModelExecution = error("Fake backend must not execute in registry metadata tests") + ): TsUnknownCallModelBackendResult = error("Fake backend must not execute in registry metadata tests") } + + private fun etsFile(fileName: String): EtsFile = EtsFile( + signature = EtsFileSignature(projectName = "test", fileName = fileName), + classes = emptyList(), + namespaces = emptyList(), + ) } diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts index 38ce413db6..35c8d567f9 100644 --- a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -5,6 +5,8 @@ declare class ExternalModels { static absolute(value: number): number; static fail(value: number): number; static positiveIdentity(value: number): number; + static exactPositiveIdentity(value: number): number; + static arityMismatch(first: number, second: number): number; static outer(value: number): number; static recursive(value: number): number; } @@ -32,6 +34,18 @@ export class EtsIrSemanticModelCalls { return ExternalModels.positiveIdentity(-1); } + exactGuardRejectsInput(): number { + return ExternalModels.exactPositiveIdentity(-1); + } + + exactArityMismatch(): number { + return ExternalModels.arityMismatch(1, 2); + } + + exactUnresolvedArgument(): number { + return MissingModels.unresolvedExactInput(1); + } + nestedUnknownCall(): number { return ExternalModels.outer(21); } diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts index 15f7186af1..10060c30f0 100644 --- a/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts @@ -1,4 +1,8 @@ export class EtsIrSemanticModels { + instanceIdentity(value: number): number { + return value; + } + static absolute(value: number): number { if (value < 0) { return -value; @@ -29,6 +33,11 @@ export class EtsIrSemanticModels { } static recurse(value: number): number { + if (value <= 0) { + return 0; + } + + EtsIrSemanticModels.recurse(value - 1); return ExternalModels.recursive(value); } }