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 eca353f53..c622fb2f2 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 @@ -48,10 +49,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 +60,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).deduplicateEtsFilesBySignature(), + 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 000000000..a77e7b2ac --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModels.kt @@ -0,0 +1,229 @@ +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 = 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 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() + } + 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") + 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 = sourceBytes.sha256(), + 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, + ): 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 when (precision) { + TsUnknownCallModelPrecision.EXACT -> TsUnknownCallModelBackendResult.NotApplicable + TsUnknownCallModelPrecision.PARTIAL -> TsUnknownCallModelBackendResult.Executed( + execution = unsupportedExecution(state), + ) + } + } + + val domainGuard = etsIrImplementation.domainGuard.evaluate( + state = state, + call = call, + inputs = inputs, + ) + if (precision == TsUnknownCallModelPrecision.EXACT && domainGuard != state.ctx.trueExpr) { + return TsUnknownCallModelBackendResult.NotApplicable + } + + val successor = TsUnknownCallModelSuccessor( + guard = domainGuard, + completion = TsUnknownCallModelCompletion.EtsIrBody( + entryPoint = etsIrImplementation.artifact.entryPoint, + inputs = inputs, + ), + ) + + 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): TsUnknownCallModelExecution { + 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 b0a9838e3..a5b399107 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,14 +32,17 @@ object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { override fun execute( implementation: TsUnknownCallModelImplementation, + 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/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 9566b54a0..bad987eb4 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 c30456c62..5b726990c 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,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 @@ -10,6 +12,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,9 +28,19 @@ interface TsUnknownCallModelBackend { fun execute( implementation: TsUnknownCallModelImplementation, + 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. */ @@ -114,6 +134,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 } + .deduplicateEtsFilesBySignature() internal fun select(call: TsUnknownCall): TsUnknownCallModelRegistration? { val matches = registrations.filter { it.descriptor.matcher.matches(call) } @@ -128,30 +151,55 @@ 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( + 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") registrations.forEach { registration -> 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 d24b6164c..3f41ec084 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 cc8e915f6..7750694a3 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 172da6329..f24e8ef3b 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,21 @@ class TsState( localToSortStack.removeLast() } + fun isUnknownCallModelActive(modelId: String): Boolean = + activeUnknownCallModels.any { (activeModelId, _, _) -> activeModelId == modelId } + + fun enterUnknownCallModel(modelId: String, entryPoint: EtsMethod) { + val entryCallDepth = callStack.size + 1 + activeUnknownCallModels += Triple(modelId, entryPoint, entryCallDepth) + } + + fun leaveUnknownCallModelIfReturning(method: EtsMethod) { + val activeModel = activeUnknownCallModels.lastOrNull() + if (activeModel?.second == method && activeModel.third == callStack.size) { + 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 +310,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 09ac54368..209ddec8e 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 000000000..666617144 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -0,0 +1,147 @@ +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 + +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) + } + + @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", + 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 000000000..556bfaf2b --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -0,0 +1,264 @@ +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 = 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", + 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 `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") + + 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 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, + 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 6684cce0f..e79a25c08 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 } @@ -145,8 +209,15 @@ class TsUnknownCallModelRegistryTest { override fun execute( implementation: TsUnknownCallModelImplementation, + 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 new file mode 100644 index 000000000..35c8d567f --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -0,0 +1,56 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +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; +} + +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); + } + + 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); + } + + 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 000000000..10060c30f --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts @@ -0,0 +1,48 @@ +export class EtsIrSemanticModels { + instanceIdentity(value: number): number { + return value; + } + + 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 { + if (value <= 0) { + return 0; + } + + EtsIrSemanticModels.recurse(value - 1); + return ExternalModels.recursive(value); + } +} + +declare class ExternalModels { + static double(value: number): number; + static recursive(value: number): number; +}