From c51b303acb9c5835bd40c3d9d165373ae06df119 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 7 Sep 2026 22:16:03 +0300 Subject: [PATCH] [TS Calls] Execute TypeScript semantic models --- usvm-ts/UNKNOWN_CALL_MODELS.md | 160 ++++++++---- .../main/kotlin/org/usvm/machine/TsMachine.kt | 20 +- .../call/TsBuiltInUnknownCallModels.kt | 53 +++- .../machine/call/TsEtsIrUnknownCallModel.kt | 213 +++++++++++++++ .../usvm/machine/call/TsUnknownCallModel.kt | 14 + .../machine/call/TsUnknownCallModelCatalog.kt | 25 ++ .../call/TsUnknownCallModelDispatcher.kt | 9 + .../usvm/machine/expr/CallApproximations.kt | 24 +- .../org/usvm/machine/expr/WriteField.kt | 55 ++++ .../usvm/machine/interpreter/TsInterpreter.kt | 2 + .../kotlin/org/usvm/machine/state/TsState.kt | 17 ++ .../org/usvm/machine/state/TsStateUtils.kt | 1 + .../usvm/machine/call/models/ArrayModels.ts | 12 + .../machine/call/TsArrayPopEtsIrModelTest.kt | 228 ++++++++++++++++ .../TsEtsIrUnknownCallModelArtifactTest.kt | 96 +++++++ .../TsEtsIrUnknownCallModelExecutionTest.kt | 244 ++++++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 67 +++++ .../test/resources/models/ArrayPopEtsIr.ts | 47 ++++ .../models/EtsIrSemanticModelCalls.ts | 51 ++++ .../resources/models/EtsIrSemanticModels.ts | 48 ++++ 20 files changed, 1328 insertions(+), 58 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt create mode 100644 usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.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/ArrayPopEtsIr.ts 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/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 70dbb9c4d6..39aae8b626 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -35,7 +35,7 @@ Unknown-call behavior is configured directly in `TsOptions`: ```kotlin TsOptions( - enabledUnknownCallModelIds = setOf("ts.array.shift"), + enabledUnknownCallModelIds = setOf("ts.array.pop"), unknownCallFallback = TsResidualCallPolicy.STOP_PATH, ) ``` @@ -53,18 +53,20 @@ This is the only model-selection setting. Unknown IDs are rejected when the machine creates its immutable per-run catalog. The input set is copied at that point, so later mutations cannot change an active run. -Use the model's `id`, for example `ts.array.shift`. A target method name, class name, source filename, or fingerprint is +Use the model's `id`, for example `ts.array.pop`. A target method name, class name, source filename, or artifact hash is not a model ID. -The built-in catalog currently contains one model: +The built-in catalog currently contains: | ID | Implementation | Accepted calls | | --- | --- | --- | | `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. | +| `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a statically proven `number[]` receiver that also satisfies the symbolic runtime type guard. | An `any`/unknown receiver, a fake-value wrapper, and a non-array receiver do not become applicable merely because the -method is named `shift`; they use fallback. A definitely-array receiver with an unresolved element sort remains -applicable and uses the fake-value representation described below. +method is named `pop` or `shift`; they use fallback. A definitely-array `shift` receiver with an unresolved element sort +remains applicable and uses the fake-value representation described below. An array outside the `pop` model's +`number[]` domain uses fallback. ### `unknownCallFallback` @@ -72,7 +74,8 @@ The fallback is applied when: - no enabled model target matches the call; - the selected model returns `null` because it cannot safely handle the concrete inputs; -- a model returns a satisfiable `residualGuard`. +- a model returns a satisfiable `residualGuard`; +- recursive redirection attempts to enter the same model again. The available policies are: @@ -106,18 +109,18 @@ Use a stable semantic name: Examples: -- `ts.array.shift` - `ts.array.pop` +- `ts.array.shift` - `node.buffer.copy` -The ID is used for configuration, observer events, and catalog fingerprints. Do not include: +The ID is used for configuration, observer events, recursion prevention, and catalog fingerprints. Do not include: -- an implementation mechanism such as `intrinsic`; -- a hash; +- an implementation mechanism such as `intrinsic` or `ets-ir`; +- a source or EtsIR hash; - a version number; - a supported-domain label. -Keep the same ID if an equivalent model is later reimplemented by another mechanism. +Keep the same ID when an equivalent model moves from Kotlin to TypeScript. ### Choosing a target @@ -125,7 +128,7 @@ Keep the same ID if an equivalent model is later reimplemented by another mechan ```kotlin TsUnknownCallTarget( - methodName = "shift", + methodName = "pop", failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, ) ``` @@ -134,12 +137,13 @@ Only `methodName` is required. Add `enclosingClassName` or `failureReason` when The catalog rejects overlapping enabled targets before execution, so catalog order is never a priority rule. The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in -`apply`. +`apply` or in an EtsIR model's domain guard. -The built-in array target intentionally combines the method name with `PARTIAL_APPROXIMATION` instead of a class name. +The built-in array targets intentionally combine the method name with `PARTIAL_APPROXIMATION` instead of a class name. That failure reason is emitted only after the regular approximation path has classified the receiver as an -`EtsArrayType`. Calls on `any`/unknown receivers reach another failure reason and cannot match this target. The model -still validates the resolved receiver and array shape before changing memory. +`EtsArrayType`. Calls on `any`/unknown receivers reach another failure reason and cannot match these targets. Each model +still validates the resolved receiver and its supported domain before changing memory. `shift` accepts an unresolved +element sort, while `pop` currently accepts only `number[]`. ## Applicability and residual states @@ -167,44 +171,88 @@ Model authors are responsible for making successor guards and the residual guard property belongs in focused model tests; the dispatcher does not invoke the solver a second time merely to validate a model on every call. -## When to write an intrinsic +## TypeScript bodies and intrinsics + +Use a TypeScript body by default. Use a Kotlin intrinsic only for an operation that TypeScript cannot express without +losing symbolic efficiency or correctness. + +### TypeScript/EtsIR model + +A TypeScript model is ordinary source code: + +```typescript +export class ArrayModels { + static pop(receiver: number[]): number | undefined { + const length = receiver.length; + if (length === 0) { + return undefined; + } + + const result = receiver[length - 1]; + receiver.length = length - 1; + return result; + } +} +``` + +Load the source and put the resulting model directly in the catalog: + +```kotlin +val artifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = modelPath, + entryPointClassName = "ArrayModels", + entryPointMethodName = "pop", +) + +val model = TsEtsIrUnknownCallModel( + id = "ts.array.pop", + target = TsUnknownCallTarget(methodName = "pop"), + artifact = artifact, + domainGuard = numberArrayGuard, +) + +val catalog = TsUnknownCallModelCatalog(models = listOf(model)) +``` + +The normal EtsIR interpreter executes the body. Receiver and arguments become entry-point parameters; ordinary return, +exception, field and array writes, and reference aliases flow back through the normal call stack. + +The entry point must be static and have a non-empty body. Its parameter count must equal the resolved receiver plus +argument count. Unresolved inputs or an arity mismatch make the model not applicable. + +The domain guard has three useful outcomes: -An intrinsic directly builds guarded successors and symbolic-memory operations in Kotlin. Use it only for an operation -that TypeScript cannot express without losing symbolic efficiency or correctness. +| Guard | Result | +| --- | --- | +| Concrete `false` | The model is not applicable; fallback handles the complete state. | +| Concrete `true` | The interpreter enters the TypeScript body; there is no residual state. | +| Symbolic expression | The true branch enters the body and the complementary branch uses fallback. | + +### Kotlin intrinsic + +An intrinsic is simply another `TsUnknownCallModel` implementation. It directly builds guarded successors and symbolic +memory operations. `Array.shift` is the built-in example because shifting a symbolic array is naturally represented by symbolic-memory `memcpy` operations. A resolved element sort uses one array region. A symbolic array with an unresolved element sort uses the boolean, number, and address regions that back a fake value; its removed element is materialized before -forking so the exactly-one type constraint and updated solver models are inherited by every successor. +forking so the exactly-one type constraint and updated solver models are inherited by every successor. In contrast, +`Array.pop` is expressed as the TypeScript body shown above. Good intrinsic candidates include: - bulk symbolic-memory copy or fill; - symbolic collection primitives; -- solver operations unavailable in the modeled language; -- type-system operations that cannot be represented faithfully by ordinary code. - -Do not write an intrinsic merely because a library method is stateful. +- solver operations unavailable in TypeScript; +- type-system operations that cannot be represented faithfully in EtsIR. -## Source-model migration - -A source model uses the same `TsUnknownCallModel` object and the same ID, target, successor, and residual contract. -The source-model work in PR #380 should extend a successor completion with the EtsIR entry point and resolved inputs, -make the model's EtsIR files visible in the analysis scene, and enter that method through the regular interpreter. -Receiver binding, arguments, returns, exceptions, heap changes, aliases, and nested calls then use normal interpreter -semantics. They must not be reimplemented in a source-specific dispatcher or backend registry. - -The model checks its supported domain before entering EtsIR. An unsupported call returns `null`; a guarded supported -subdomain uses the complementary residual guard and the same configured fallback. Recursive redirection is prevented -by tracking the active model ID in execution state, not by creating a second catalog. - -`Array.pop` is the source-model example. Its TypeScript body uses indexing and `length`; it must not call `pop` again. -The existing `Array.shift` intrinsic remains the example for engine-only symbolic-memory `memcpy`. +Do not write a Kotlin intrinsic merely because a library method is stateful. If ordinary TypeScript can express the +semantics, keep the model in TypeScript. ## Dynamic receivers -A method name does not prove the receiver type. In particular, `value.shift()` may call a user-defined property rather -than `Array.prototype.shift`. +A method name does not prove the receiver type. In particular, `value.pop()` may call a user-defined property rather +than `Array.prototype.pop`. Use this decision rule: @@ -219,17 +267,31 @@ Never choose `typeStreamOf(receiver).firstOrNull()` as proof. It returns one pos possible type. Use a statically proven type, `singleOrNull()` where uniqueness is guaranteed, or an explicit symbolic type guard. -## Fingerprints +## Nested calls and recursion + +Unknown calls made inside a TypeScript model body use the same catalog and fallback as the original program. This lets +source models compose with other source models and intrinsics. + +The state tracks each active model ID together with its call-stack depth. If the same model would redirect recursively, +lookup declines that redirection and fallback is applied instead of entering an infinite loop. + +Do not implement `Array.pop` by calling `receiver.pop()` inside its own model body. Implement it through `length` and +indexed access, as in the example above. + +## Artifacts and fingerprints + +The loader snapshots the source bytes, invokes the native JacoDB TypeScript frontend, and rejects source mutation during +generation. The resulting artifact records source and EtsIR SHA-256 hashes for reproducibility. The catalog sorts enabled models by ID and hashes their length-prefixed IDs. Therefore model registration order does -not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries. - -The fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a -manually maintained configuration value. Experiment metadata records the tool revision separately. If model source -can change independently of that revision, the runner also records a content hash for the external source or generated -artifact; that content identity is experiment metadata, not another model ID, version, or compatibility setting. Keep -the catalog fingerprint based only on enabled model IDs rather than adding implementation-specific fingerprint fields -to the common model contract. +not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries. The +fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a manually +maintained configuration value. Experiment metadata records the tool revision separately. If model source can change +independently of that revision, the runner also records the artifact's content hashes as experiment metadata; those +hashes are not another model ID, version, compatibility setting, or part of the common model contract. + +EtsIR files are merged into the analysis scene by file signature. Reusing the same file object is deduplicated; +distinct files with the same signature are rejected. ## Observation 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 15e4804470..8435a7eda5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -13,6 +13,7 @@ import org.usvm.machine.call.TsBuiltInUnknownCallModels import org.usvm.machine.call.TsModelUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallModelCatalog +import org.usvm.machine.call.deduplicateEtsFilesBySignature import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -39,7 +40,7 @@ import kotlin.time.Duration.Companion.seconds private val logger = KotlinLogging.logger {} class TsMachine( - private val scene: EtsScene, + scene: EtsScene, override val options: UMachineOptions, private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, @@ -57,10 +58,21 @@ class TsMachine( val unknownCallModelCatalogFingerprint: String? get() = resolvedUnknownCallModels?.fingerprint - private val graph = TsGraph(scene) - private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) + private val analysisScene = resolvedUnknownCallModels + ?.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(scene, components) + private val ctx = TsContext(analysisScene, components) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), fallback = tsOptions.unknownCallFallback, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt index 51fd7c34e6..61dad8bbaf 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt @@ -1,13 +1,58 @@ package org.usvm.machine.call +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel /** The intentionally small built-in semantic-model catalog. */ object TsBuiltInUnknownCallModels { const val ARRAY_SHIFT_MODEL_ID: String = TsArrayShiftIntrinsicModel.MODEL_ID + const val ARRAY_POP_MODEL_ID: String = "ts.array.pop" - fun catalog(enabledModelIds: Set? = null) = TsUnknownCallModelCatalog( - models = listOf(TsArrayShiftIntrinsicModel), - enabledModelIds = enabledModelIds, - ) + private val arrayPopModel: TsUnknownCallModel by lazy { + val artifact = loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/ArrayModels.ts", + sourceFileName = "ArrayModels.ts", + entryPointClassName = "ArrayModels", + entryPointMethodName = "pop", + ) + + TsEtsIrUnknownCallModel( + id = ARRAY_POP_MODEL_ID, + target = TsUnknownCallTarget( + methodName = "pop", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ), + artifact = artifact, + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiver = inputs.singleOrNull() + val receiverType = call.receiver?.source?.type as? EtsArrayType + val isNumberArray = receiverType?.dimensions == 1 && receiverType.elementType == EtsNumberType + if (receiver?.sort != addressSort || receiver.containsFakeObject() || !isNumberArray) { + falseExpr + } else { + state.memory.types.evalIsSubtype( + receiver.asExpr(addressSort), + EtsArrayType(EtsNumberType, dimensions = 1), + ) + } + } + }, + ) + } + + fun catalog(enabledModelIds: Set? = null): TsUnknownCallModelCatalog { + val models = buildList { + if (enabledModelIds == null || ARRAY_SHIFT_MODEL_ID in enabledModelIds) { + add(TsArrayShiftIntrinsicModel) + } + if (enabledModelIds == null || ARRAY_POP_MODEL_ID in enabledModelIds) { + add(arrayPopModel) + } + } + + return TsUnknownCallModelCatalog(models, enabledModelIds) + } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt new file mode 100644 index 0000000000..876a0bd866 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -0,0 +1,213 @@ +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.createTempDirectory +import kotlin.io.path.deleteIfExists +import kotlin.io.path.inputStream +import kotlin.io.path.outputStream +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 TypeScript semantic-model entry point. */ +data class TsEtsIrUnknownCallModelArtifact( + val file: EtsFile, + val entryPoint: EtsMethod, + val sourceHash: String, + val etsIrHash: String, +) { + 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() + } +} + +internal fun loadBundledEtsIrUnknownCallModelArtifact( + resourceName: String, + sourceFileName: String, + entryPointClassName: String, + entryPointMethodName: String, +): TsEtsIrUnknownCallModelArtifact { + val sourceDirectory = createTempDirectory(prefix = "usvm-ts-model-") + val sourcePath = sourceDirectory.resolve(sourceFileName) + + return try { + val source = checkNotNull(TsEtsIrUnknownCallModel::class.java.getResourceAsStream(resourceName)) { + "Bundled TypeScript semantic model resource not found: $resourceName" + } + source.use { input -> + sourcePath.outputStream().use { output -> input.copyTo(output) } + } + + loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = entryPointClassName, + entryPointMethodName = entryPointMethodName, + ) + } finally { + sourcePath.deleteIfExists() + sourceDirectory.deleteIfExists() + } +} + +/** A model body written in TypeScript and executed by the normal EtsIR interpreter. */ +class TsEtsIrUnknownCallModel( + override val id: String, + override val target: TsUnknownCallTarget, + val artifact: TsEtsIrUnknownCallModelArtifact, + val domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, +) : TsUnknownCallModel { + override val additionalSceneFiles: List = listOf(artifact.file) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + val inputs = call.resolvedInputs() ?: return null + if (inputs.size != artifact.entryPoint.parameters.size) { + return null + } + + val guard = domainGuard.evaluate( + state = state, + call = call, + inputs = inputs, + ) + if (guard == state.ctx.falseExpr) { + return null + } + + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.EtsIrBody( + entryPoint = artifact.entryPoint, + inputs = inputs, + ), + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it == state.ctx.trueExpr }?.let(state.ctx::mkNot), + ) + } +} + +/** Builds the symbolic input guard for one TypeScript model body. */ +fun interface TsEtsIrUnknownCallModelDomainGuard { + fun evaluate( + state: TsState, + call: TsUnknownCall, + inputs: List>, + ): UBoolExpr + + companion object { + val ALWAYS = TsEtsIrUnknownCallModelDomainGuard { state, _, _ -> 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) + 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/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 240f4f003e..69cbfccb4d 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 @@ -46,6 +48,10 @@ interface TsUnknownCallModel { val id: String val target: TsUnknownCallTarget + /** EtsIR files that must be visible to the interpreter while this model is enabled. */ + val additionalSceneFiles: List + get() = emptyList() + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? } @@ -65,6 +71,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() + } } /** One guarded model successor. */ diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt index dd74e93431..3320cc5064 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.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 @@ -18,6 +20,7 @@ class TsUnknownCallModelCatalog( get() = models.map(TsUnknownCallModel::id) val fingerprint: String + val additionalSceneFiles: List init { val allModels = models.sortedBy(TsUnknownCallModel::id) @@ -44,6 +47,9 @@ class TsUnknownCallModelCatalog( validateUnambiguousTargets(this.models) fingerprint = computeFingerprint(this.models) + additionalSceneFiles = this.models + .flatMap(TsUnknownCallModel::additionalSceneFiles) + .deduplicateEtsFilesBySignature() } internal fun select(call: TsUnknownCall): TsUnknownCallModel? = @@ -51,6 +57,10 @@ class TsUnknownCallModelCatalog( fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + if (state.isUnknownCallModelActive(model.id)) { + return TsUnknownCallModelApplication.NotApplicable + } + val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable return TsUnknownCallModelApplication.Applied( @@ -73,6 +83,21 @@ private fun validateUnambiguousTargets(models: List) { } } +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(models: List): String { val digest = MessageDigest.getInstance("SHA-256") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 5a524e6ded..7674ec064b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -169,6 +169,15 @@ class TsModelUnknownCallDispatcher( val (exception, type) = completion.exception(this) methodResult = TsMethodResult.TsException(exception, type) } + + is TsUnknownCallModelCompletion.EtsIrBody -> { + enterEtsIrUnknownCallModel( + modelId = modelId, + entryPoint = completion.entryPoint, + inputs = completion.inputs, + returnSite = call.callSite, + ) + } } if (onApplied()) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index c48b2c5529..5dbe685137 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -111,7 +111,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return from(handleArrayPop(expr, instanceType, elementSort)) + return handleArrayPopCall(expr, instanceType, elementSort, instance) } // Handle `Array.fill() method calls @@ -163,6 +163,28 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return TsExprApproximationResult.NoApproximation } +private fun TsExprResolver.handleArrayPopCall( + expr: EtsInstanceCallExpr, + instanceType: EtsArrayType, + elementSort: USort, + resolvedReceiver: UExpr<*>, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return from(handleArrayPop(expr, instanceType, elementSort)) + } + + dispatcher.dispatch( + scope, + expr, + scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = resolvedReceiver, + ) + + return TsExprApproximationResult.ResolveFailure +} + private fun TsExprResolver.handleArrayShiftCall( expr: EtsInstanceCallExpr, instanceType: EtsArrayType, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index c553668414..b2227f7e50 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -2,6 +2,7 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr import mu.KotlinLogging +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsInstanceFieldRef @@ -14,8 +15,10 @@ import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType +import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult +import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.resolveEtsField @@ -48,10 +51,62 @@ internal fun TsExprResolver.handleAssignToInstanceField( // Check for undefined or null field access. checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null + val arrayType = instanceLocal.type as? EtsArrayType + if (field.name == "length" && arrayType != null) { + return assignToArrayLength( + scope = scope, + array = instance, + arrayType = arrayType, + value = expr, + maxArraySize = options.maxArraySize, + ) + } + // Assign to the field. assignToInstanceField(scope, instanceLocal, instance, field, expr, hierarchy) } +private fun TsContext.assignToArrayLength( + scope: TsStepScope, + array: UHeapRef, + arrayType: EtsArrayType, + value: UExpr<*>, + maxArraySize: Int, +): Unit? = with(this) { + if (value.sort != fp64Sort) { + return null + } + + val fpLength = value.asExpr(fp64Sort) + val convertedLength = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = fpLength, + bvSize = 32, + isSigned = true, + ) + val roundTrip = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = convertedLength, + signed = true, + ) + val length = convertedLength.asExpr(sizeSort) + val lengthIsIntegral = mkEq(roundTrip, fpLength) + val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxArraySize)) + val validLength = mkAnd( + lengthIsIntegral, + lengthIsNonNegative, + lengthIsWithinLimit, + ) + scope.assert(validLength) ?: return null + + val lengthLValue = mkArrayLengthLValue(array, arrayType) + return scope.doWithState { + memory.write(lengthLValue, length, guard = trueExpr) + } +} + fun TsContext.assignToInstanceField( scope: TsStepScope, instanceLocal: EtsLocal, 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..e9779d339c 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,10 +109,12 @@ class TsInterpreter( if (result is TsMethodResult.TsException) { // TODO catch processing scope.doWithState { + leaveUnknownCallModelIfReturning() val returnSite = callStack.pop() if (callStack.isNotEmpty()) { memory.stack.pop() + popLocalToSortStack() } if (returnSite != null) { 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..019257dd38 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) { + val entryCallDepth = callStack.size + 1 + activeUnknownCallModels += modelId to entryCallDepth + } + + fun leaveUnknownCallModelIfReturning() { + val activeModel = activeUnknownCallModels.lastOrNull() + if (activeModel?.second == 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 09ac543689..eae28f6e14 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() val returnSite = callStack.pop() if (callStack.isNotEmpty()) { memory.stack.pop() diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts new file mode 100644 index 0000000000..573ad98ee7 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -0,0 +1,12 @@ +export class ArrayModels { + static pop(receiver: number[]): number | undefined { + const length = receiver.length; + if (length === 0) { + return undefined; + } + + const result = receiver[length - 1]; + receiver.length = length - 1; + return result; + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt new file mode 100644 index 0000000000..cd58e66ef1 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -0,0 +1,228 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +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.machine.state.TsState +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.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayPopEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayPopEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `empty array pop returns undefined through TypeScript model`() { + val result = analyze(methodName = "emptyArray") + + assertIs(result.values.single()) + assertEquals(listOf("ts.array.pop"), result.modelIds) + assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}"))) + } + + @Test + fun `non empty array pop executes source body and updates real array length`() { + val result = analyze(methodName = "nonEmptyArray") + + assertEquals(32.0, assertIs(result.values.single()).number) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `symbolic number array uses the source model`() { + val result = analyze(methodName = "symbolicNumberArray") + + assertTrue(result.values.isNotEmpty()) + assertEquals(listOf("ts.array.pop"), result.modelIds.distinct()) + } + + @Test + fun `arrays outside the source model domain use fallback`() { + assertUsesResidualFallback(methodName = "referenceArray") + assertUsesResidualFallback(methodName = "symbolicUnknownArray") + } + + @Test + fun `unknown receiver does not prove an Array pop call`() { + val result = analyze(methodName = "unknownReceiver") + + assertTrue(result.modelIds.isEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map { it.outcome }) + } + + @Test + fun `fake wrapper receiver is outside the Array pop model domain`() { + val state = analyzeStates(methodName = "unknownValue").single() + val fakeReceiver = makeFakeReceiver(state) + val models = TsBuiltInUnknownCallModels.catalog( + enabledModelIds = setOf(TsBuiltInUnknownCallModels.ARRAY_POP_MODEL_ID), + ) + + val application = models.apply(state, arrayPopCall(fakeReceiver)) + + assertIs(application) + } + + @Test + fun `arity mismatch uses fallback`() { + assertUsesResidualFallback(methodName = "popWithArguments") + } + + @Test + fun `disabled pop model uses configured fallback`() { + val result = analyze( + methodName = "nonEmptyArray", + tsOptions = TsOptions( + enabledUnknownCallModelIds = setOf(TsBuiltInUnknownCallModels.ARRAY_SHIFT_MODEL_ID), + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), + ) + + assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), result.events.map { it.outcome }) + } + + @Test + fun `compatibility dispatcher keeps the legacy pop approximation`() { + val result = analyze( + methodName = "nonEmptyArray", + dispatcher = TsCompatibilityUnknownCallDispatcher, + ) + + assertEquals(32.0, assertIs(result.values.single()).number) + assertTrue(result.events.isEmpty()) + assertNull(result.catalogFingerprint) + } + + private fun analyze( + methodName: String, + tsOptions: TsOptions = TsOptions(), + dispatcher: TsUnknownCallDispatcher? = null, + ): AnalysisResult { + val method = method(methodName) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + observer = observer, + unknownCallDispatcher = dispatcher, + ).use { machine -> + val states = machine.analyze(listOf(method)) + val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue } + + AnalysisResult( + values = values, + events = observer.events.toList(), + catalogFingerprint = machine.unknownCallModelCatalogFingerprint, + ) + } + } + + private fun assertUsesResidualFallback(methodName: String) { + val result = analyze(methodName) + + assertTrue( + result.values.isEmpty(), + "Expected fallback to stop the path, got values=${result.values}, events=${result.events}", + ) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + private fun makeFakeReceiver(state: TsState): UConcreteHeapRef { + val result = assertIs(state.methodResult).value + val fakeReceiver = assertIs(result) + + assertTrue(with(state.ctx) { fakeReceiver.isFakeObject() }) + return fakeReceiver + } + + private fun arrayPopCall(resolvedReceiver: UExpr<*>): TsUnknownCall { + val callSite = method("nonEmptyArray").cfg.stmts.single { stmt -> + stmt.callExpr?.callee?.name == "pop" + } + val sourceCall = assertIs(assertNotNull(callSite.callExpr)) + + return TsUnknownCall( + callee = sourceCall.callee, + receiver = TsUnknownCallValue(source = sourceCall.instance, resolved = resolvedReceiver), + arguments = emptyList(), + resultType = sourceCall.type, + callSite = callSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + } + + private fun analyzeStates(methodName: String): List { + val method = method(methodName) + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze(listOf(method)) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "ArrayPopEtsIr" } + .methods + .single { it.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: List, + val events: List, + val catalogFingerprint: String?, + ) { + 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/TsEtsIrUnknownCallModelArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt new file mode 100644 index 0000000000..6bc6f622e7 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -0,0 +1,96 @@ +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.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("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 `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")) + } +} 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..2f097ea3c3 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -0,0 +1,244 @@ +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 = TsUnknownCallModelCatalog( + models = listOf( + model( + id = "test.ets-ir.absolute", + targetName = "absolute", + entryPointName = "absolute", + ), + model( + id = "test.ets-ir.increment", + targetName = "modeledIncrement", + entryPointName = "increment", + ), + model( + id = "test.ets-ir.fail", + targetName = "fail", + entryPointName = "fail", + ), + model( + id = "test.ets-ir.positive-identity", + targetName = "positiveIdentity", + entryPointName = "positiveIdentity", + domainGuard = positiveInputGuard, + ), + model( + id = "test.ets-ir.arity-mismatch", + targetName = "arityMismatch", + entryPointName = "positiveIdentity", + ), + model( + id = "test.ets-ir.unresolved-argument", + targetName = "unresolvedInput", + entryPointName = "positiveIdentity", + ), + model( + id = "test.ets-ir.outer", + targetName = "outer", + entryPointName = "outer", + ), + model( + id = "test.ets-ir.double", + targetName = "double", + entryPointName = "double", + ), + model( + id = "test.ets-ir.recursive", + targetName = "recursive", + entryPointName = "recurse", + ), + ), + ) + + @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(1, result.states.single().localToSortStack.size) + 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 `unresolved or arity mismatched inputs use configured residual fallback`() { + val unsupportedMethods = listOf( + "arityMismatch", + "unresolvedArgument", + ) + + 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 model( + id: String, + targetName: String, + entryPointName: String, + domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, + ): TsUnknownCallModel { + val artifact = baseArtifact.copy( + entryPoint = modelClass.methods.single { it.name == entryPointName }, + ) + + return TsEtsIrUnknownCallModel( + id = id, + target = TsUnknownCallTarget(methodName = targetName), + 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(), + observer = observer, + unknownCallModels = 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/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index cde61a23c2..233ab88004 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -1,5 +1,11 @@ package org.usvm.machine.call +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 @@ -96,23 +102,84 @@ class TsUnknownCallModelCatalogTest { assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) } + @Test + fun `same model EtsIR file object is merged once`() { + val modelFile = etsFile(fileName = "model.ts") + val catalog = TsUnknownCallModelCatalog( + models = listOf( + model(id = "a", methodName = "first", additionalSceneFiles = listOf(modelFile)), + model(id = "b", methodName = "second", additionalSceneFiles = listOf(modelFile)), + ) + ) + + assertEquals(listOf(modelFile), catalog.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 { + TsUnknownCallModelCatalog( + models = listOf( + model(id = "a", methodName = "first", additionalSceneFiles = listOf(first)), + model(id = "b", methodName = "second", additionalSceneFiles = listOf(second)), + ) + ) + } + + 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 catalog = TsUnknownCallModelCatalog( + models = listOf( + model(id = "model", additionalSceneFiles = listOf(modelFile)), + ) + ) + + val error = assertFailsWith { + TsMachine( + scene = EtsScene(projectFiles = listOf(applicationFile)), + options = UMachineOptions(), + tsOptions = TsOptions(), + unknownCallModels = catalog, + ) + } + + assertEquals("Conflicting EtsIR files share signature @test/shared", error.message) + } + private fun model( id: String, methodName: String = "target-$id", failureReason: TsUnknownCallFailureReason? = null, + additionalSceneFiles: List = emptyList(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( methodName = methodName, failureReason = failureReason, ), + additionalSceneFiles = additionalSceneFiles, ) private class FakeModel( override val id: String, override val target: TsUnknownCallTarget, + override val additionalSceneFiles: List, ) : TsUnknownCallModel { override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution = error("Fake model must not execute in catalog 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/ArrayPopEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts new file mode 100644 index 0000000000..cd8554ac64 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -0,0 +1,47 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class ArrayElement {} + +export class ArrayPopEtsIr { + unknownValue(value: unknown): unknown { + return value; + } + + emptyArray(): number | undefined { + const values: number[] = []; + return values.pop(); + } + + nonEmptyArray(): number { + const values = [10, 20, 30]; + return values.pop()! + values.length; + } + + referenceArray(): number { + const values: ArrayElement[] = [new ArrayElement()]; + values.pop(); + return 42; + } + + symbolicNumberArray(values: number[]): number { + values.pop(); + return 46; + } + + symbolicUnknownArray(values: any[]): number { + values.pop(); + return 47; + } + + unknownReceiver(value: any): number { + value.pop(); + return 48; + } + + popWithArguments(): number { + const values = [1]; + values.pop(0); + return 49; + } +} 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..9648cf3152 --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -0,0 +1,51 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +declare class ExternalModels { + static absolute(value: number): number; + static fail(value: number): number; + static positiveIdentity(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); + } + + arityMismatch(): number { + return ExternalModels.arityMismatch(1, 2); + } + + unresolvedArgument(): number { + return MissingModels.unresolvedInput(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..10060c30f0 --- /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; +}