From c9b6d3e0bb5c5c67db12d79aaffbf5c4bf1f4754 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 7 Sep 2026 22:16:03 +0300 Subject: [PATCH 1/6] [TS Calls] Execute TypeScript semantic models --- usvm-ts/UNKNOWN_CALL_MODELS.md | 151 +++++++---- .../main/kotlin/org/usvm/machine/TsMachine.kt | 20 +- .../machine/call/TsEtsIrUnknownCallModel.kt | 213 +++++++++++++++ .../usvm/machine/call/TsUnknownCallModel.kt | 14 + .../machine/call/TsUnknownCallModelCatalog.kt | 25 ++ .../call/TsUnknownCallModelDispatcher.kt | 9 + .../call/intrinsic/TsArrayPopEtsIrModel.kt | 55 ++++ .../usvm/machine/expr/CallApproximations.kt | 22 +- .../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 | 71 ++++- .../test/resources/models/ArrayPopEtsIr.ts | 47 ++++ .../models/EtsIrSemanticModelCalls.ts | 51 ++++ .../resources/models/EtsIrSemanticModels.ts | 48 ++++ 20 files changed, 1329 insertions(+), 52 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.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 f598c5c990..58c7ed8b7c 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( - unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.array.shift")), + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.array.pop")), unknownCallFallback = TsResidualCallPolicy.STOP_PATH, ) ``` @@ -53,18 +53,19 @@ This is the only model-selection setting. Unknown IDs are rejected when the machine creates its immutable per-run catalog. The selected models are captured at that point, so later mutations of the selection set 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. Built-ins are `object` implementations of the sealed `TsBuiltInUnknownCallModel` interface in the `org.usvm.machine.call.intrinsic` package. Kotlin's sealed-subclass metadata discovers them automatically; adding a model requires no manual registry entry. Discovery and the default catalog are computed once. -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. | The common instance-call pipeline splits fake-value wrappers and conditional references under their runtime-kind and branch guards before selecting an approximation or resolving a method. A wrapped array can therefore use the @@ -78,7 +79,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: @@ -112,18 +114,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 @@ -131,7 +133,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, ) ``` @@ -143,13 +145,13 @@ a priority rule. IDs and their SHA-256 fingerprint are computed once; byte-lengt such as `["ab", "c"]` and `["a", "bc"]`. 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` using the normalized receiver's storage type. An `any` alias of a known array can satisfy that check; a receiver without array-type evidence cannot. The model still validates the resolved receiver and array shape -before changing memory. +before changing memory. `pop` currently accepts only arrays stored as `number[]`. ## Applicability and residual states @@ -177,10 +179,67 @@ 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)) +``` -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. +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: + +| 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 canonical array region. Unresolved elements use three @@ -201,34 +260,22 @@ fallback. Existing `fill` bounds and the finite `reverse`/`fill` caps remain app Array reads, writes, length access, and `shift` use the storage type known to symbolic memory when it is unique. Widening a local from `number[]` to `any[]` therefore keeps the same element and length regions. +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`. Instance calls share receiver normalization before built-in approximations and ordinary method lookup. It reuses `extractValue` to select a fake payload together with its kind constraint and `splitUHeapRef` to retain conditional @@ -250,17 +297,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 0e8e6d5370..ec806cabc5 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/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 6334fa48a5..c5eaef5038 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 @@ -30,6 +32,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? } @@ -49,6 +55,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 ee825bced1..2189765540 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 @@ -17,6 +19,7 @@ class TsUnknownCallModelCatalog( val modelIds: List val fingerprint: String + val additionalSceneFiles: List init { val modelsById = hashMapOf() @@ -37,6 +40,9 @@ class TsUnknownCallModelCatalog( modelIds = Collections.unmodifiableList(selectedModels.map(TsUnknownCallModel::id)) index = indexModels(selectedModels) fingerprint = computeFingerprint(modelIds) + additionalSceneFiles = selectedModels + .flatMap(TsUnknownCallModel::additionalSceneFiles) + .deduplicateEtsFilesBySignature() } internal fun select(call: TsUnknownCall): TsUnknownCallModel? { @@ -46,6 +52,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( @@ -80,6 +90,21 @@ private fun indexModels( return index } +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(modelIds: List): String { val digest = MessageDigest.getInstance("SHA-256") modelIds.forEach { digest.updateLengthPrefixed(it) } 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 4744946513..4e075e54e6 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 @@ -178,6 +178,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, + ) + } } onApplied() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt new file mode 100644 index 0000000000..22832f9301 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt @@ -0,0 +1,55 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.usvm.machine.call.TsEtsIrUnknownCallModel +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.state.TsState +import org.usvm.util.arrayStorageType + +/** Built-in `Array.pop` implemented by an ordinary TypeScript body. */ +internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel { + override val id: String = "ts.array.pop" + override val target = TsUnknownCallTarget( + methodName = "pop", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + private val model by lazy { + TsEtsIrUnknownCallModel( + id = id, + target = target, + artifact = loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/ArrayModels.ts", + sourceFileName = "ArrayModels.ts", + entryPointClassName = "ArrayModels", + entryPointMethodName = "pop", + ), + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiver = inputs.singleOrNull() + if (receiver?.sort != addressSort || receiver.containsFakeObject()) { + falseExpr + } else { + val array = receiver.asExpr(addressSort) + val receiverType = state.arrayStorageType(array, call.receiver?.source?.type) as? EtsArrayType + if (receiverType?.dimensions != 1 || receiverType.elementType != EtsNumberType) { + falseExpr + } else { + state.memory.types.evalIsSubtype(array, receiverType) + } + } + } + }, + ) + } + + override val additionalSceneFiles get() = model.additionalSceneFiles + + override fun apply(state: TsState, call: TsUnknownCall) = model.apply(state, call) +} 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 841a7fc2b3..385cd38679 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 @@ -123,7 +123,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return from(handleArrayPop(stmt, instanceType, elementSort, array)) + return handleArrayPopCall(stmt, instanceType, elementSort) } // Handle `Array.fill() method calls @@ -175,6 +175,26 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return TsExprApproximationResult.NoApproximation } +private fun TsExprResolver.handleArrayPopCall( + stmt: TsVirtualMethodCallStmt, + instanceType: EtsArrayType, + elementSort: USort, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return from(handleArrayPop(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort))) + } + + dispatcher.dispatch( + scope, + stmt, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = stmt.instance, + ) + + return TsExprApproximationResult.ResolveFailure +} + private fun TsExprResolver.handleArrayShiftCall( stmt: TsVirtualMethodCallStmt, 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 70ad6909f9..423f5dde71 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 @@ -111,10 +111,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..177d2bd587 --- /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( + selection = TsUnknownCallModelSelection.Only(setOf("ts.array.pop")), + ) + + 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( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.array.shift")), + 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 658e1e0bd9..b1d1029474 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 @@ -6,6 +6,12 @@ import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsUnknownType import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel +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 @@ -149,10 +155,10 @@ class TsUnknownCallModelCatalogTest { fun `built in models are discovered once and an explicit empty selection disables all`() { val catalog = TsBuiltInUnknownCallModels.catalog() - assertEquals(listOf(TsArrayShiftIntrinsicModel.MODEL_ID), catalog.modelIds) + assertEquals(listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), catalog.modelIds) assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) assertFailsWith { (catalog.modelIds as MutableList).clear() } - assertEquals(listOf(TsArrayShiftIntrinsicModel.MODEL_ID), TsBuiltInUnknownCallModels.catalog().modelIds) + assertEquals(listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), TsBuiltInUnknownCallModels.catalog().modelIds) assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) } @@ -179,11 +185,64 @@ class TsUnknownCallModelCatalogTest { failureReason = reason, ) + @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, className: String? = null, + additionalSceneFiles: List = emptyList(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( @@ -191,13 +250,21 @@ class TsUnknownCallModelCatalogTest { failureReason = failureReason, enclosingClassName = className, ), + additionalSceneFiles = additionalSceneFiles, ) private class FakeModel( override val id: String, override val target: TsUnknownCallTarget, + override val additionalSceneFiles: List = emptyList(), ) : 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; +} From 78ca2fd8430f1a3cc0196b96fb739c5f0806eff5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 17 Sep 2026 23:06:35 +0300 Subject: [PATCH 2/6] [TS Calls] Prevent EtsIR model dispatch bypasses --- .../main/kotlin/org/usvm/machine/TsContext.kt | 2 ++ .../main/kotlin/org/usvm/machine/TsMachine.kt | 6 +++++- .../kotlin/org/usvm/machine/expr/CallStatic.kt | 2 +- .../kotlin/org/usvm/machine/expr/WriteField.kt | 15 +++++++++++++-- .../machine/call/TsArrayPopEtsIrModelTest.kt | 16 ++++++++++++++++ .../call/TsEtsIrUnknownCallModelExecutionTest.kt | 16 ++++++++++++++++ .../src/test/resources/models/ArrayPopEtsIr.ts | 13 +++++++++++++ .../resources/models/EtsIrSemanticModelCalls.ts | 4 ++++ .../test/resources/models/EtsIrSemanticModels.ts | 4 ++++ 9 files changed, 74 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 12f4cbde26..e58f45f474 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -7,6 +7,7 @@ import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsLexicalEnvType @@ -59,6 +60,7 @@ typealias TsSizeSort = UBv32Sort class TsContext( val scene: EtsScene, components: TsComponents, + internal val applicationAndSdkClasses: List = scene.projectAndSdkClasses, ) : UContext(components) { val undefinedSort: TsUndefinedSort by lazy { TsUndefinedSort(this) } 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 ec806cabc5..3c45d045ab 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -72,7 +72,11 @@ class TsMachine( 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 ctx = TsContext( + scene = analysisScene, + components = components, + applicationAndSdkClasses = scene.projectAndSdkClasses, + ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), fallback = tsOptions.unknownCallFallback, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt index 89c75972b2..154d9555ac 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt @@ -95,7 +95,7 @@ private fun TsExprResolver.resolveStaticMethod( } // Unknown signature: - val methods = ctx.scene.projectAndSdkClasses + val methods = ctx.applicationAndSdkClasses .flatMap { it.methods } .filter { it.name == method.name } .canonicalizeExecutableOverloads() 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 b2227f7e50..9d40f28e96 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 @@ -91,17 +91,28 @@ private fun TsContext.assignToArrayLength( signed = true, ) val length = convertedLength.asExpr(sizeSort) + val lengthLValue = mkArrayLengthLValue(array, arrayType) + val currentLength = scope.calcOnState { + memory.read(lengthLValue) + } val lengthIsIntegral = mkEq(roundTrip, fpLength) val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxArraySize)) + val lengthIsNotGrowing = mkBvSignedLessOrEqualExpr(length, currentLength) val validLength = mkAnd( lengthIsIntegral, lengthIsNonNegative, lengthIsWithinLimit, + lengthIsNotGrowing, ) - scope.assert(validLength) ?: return null + scope.assert(validLength) ?: run { + logger.warn { + "Unsupported array length assignment: expected an integral length in [0, current length], " + + "but the constraint is UNSAT: $validLength" + } + return null + } - val lengthLValue = mkArrayLengthLValue(array, arrayType) return scope.doWithState { memory.write(lengthLValue, length, guard = trueExpr) } 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 index 177d2bd587..aff5ccb938 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -52,6 +52,22 @@ class TsArrayPopEtsIrModelTest { assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) } + @Test + fun `array length growth after pop is unsupported`() { + val result = analyze(methodName = "popThenGrow") + + assertTrue(result.values.isEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `fresh array length growth is unsupported`() { + val result = analyze(methodName = "growFreshArray") + + assertTrue(result.values.isEmpty()) + assertTrue(result.events.isEmpty()) + } + @Test fun `symbolic number array uses the source model`() { val result = analyze(methodName = "symbolicNumberArray") diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt index 2f097ea3c3..11921093c0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -82,6 +82,12 @@ class TsEtsIrUnknownCallModelExecutionTest { targetName = "recursive", entryPointName = "recurse", ), + model( + id = "test.ets-ir.guarded", + targetName = "guarded", + entryPointName = "guarded", + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, _ -> state.ctx.falseExpr }, + ), ), ) @@ -159,6 +165,16 @@ class TsEtsIrUnknownCallModelExecutionTest { assertIs(result.events.last().decision) } + @Test + fun `model body cannot bypass dispatcher when domain guard is false`() { + val result = analyze(methodName = "guardedModelBodyCannotBypassDispatcher") + + assertTrue(result.states.isEmpty()) + assertTrue(result.modelIds.isEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map { it.outcome }) + assertIs(result.events.single().decision) + } + private fun model( id: String, targetName: String, diff --git a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts index cd8554ac64..f14a9b4c2e 100644 --- a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -18,6 +18,19 @@ export class ArrayPopEtsIr { return values.pop()! + values.length; } + popThenGrow(): number { + const values = [10, 20]; + values.pop(); + values.length = 2; + return 50; + } + + growFreshArray(): number { + const values: number[] = []; + values.length = 1; + return 51; + } + referenceArray(): number { const values: ArrayElement[] = [new ArrayElement()]; values.pop(); diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts index 9648cf3152..3c9c667e55 100644 --- a/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -48,4 +48,8 @@ export class EtsIrSemanticModelCalls { recursiveRedirection(): number { return ExternalModels.recursive(1); } + + guardedModelBodyCannotBypassDispatcher(): number { + return guarded(-1); + } } diff --git a/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts index 10060c30f0..c60217e2b8 100644 --- a/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts @@ -24,6 +24,10 @@ export class EtsIrSemanticModels { return value; } + static guarded(value: number): number { + return value; + } + static outer(value: number): number { return ExternalModels.double(value); } From 41961f7b66c30c8a2a7507c67a79396f495f4520 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 18 Sep 2026 19:26:30 +0300 Subject: [PATCH 3/6] [TS Calls] Preserve array semantics on the current model API --- usvm-ts/UNKNOWN_CALL_MODELS.md | 14 ++-- .../main/kotlin/org/usvm/machine/TsMachine.kt | 3 +- .../machine/call/TsEtsIrUnknownCallModel.kt | 3 +- .../machine/call/TsUnknownCallModelCatalog.kt | 1 + .../call/TsUnknownCallModelDispatcher.kt | 2 + .../call/intrinsic/TsArrayPopEtsIrModel.kt | 8 +- .../org/usvm/machine/expr/WriteField.kt | 7 +- .../usvm/machine/call/models/ArrayModels.ts | 2 +- .../machine/call/TsArrayPopEtsIrModelTest.kt | 78 ++++++++++++++++++- .../machine/call/TsArrayShiftMatrixTest.kt | 29 ++++--- .../call/TsUnknownCallModelCatalogTest.kt | 36 +++++++-- .../test/resources/models/ArrayPopEtsIr.ts | 45 +++++++++++ 12 files changed, 195 insertions(+), 33 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 58c7ed8b7c..be224ae8ea 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -65,7 +65,7 @@ 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. | +| `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. | The common instance-call pipeline splits fake-value wrappers and conditional references under their runtime-kind and branch guards before selecting an approximation or resolving a method. A wrapped array can therefore use the @@ -151,7 +151,7 @@ The built-in array targets intentionally combine the method name with `PARTIAL_A That failure reason is emitted only after the regular approximation path has classified the receiver as an `EtsArrayType` using the normalized receiver's storage type. An `any` alias of a known array can satisfy that check; a receiver without array-type evidence cannot. The model still validates the resolved receiver and array shape -before changing memory. `pop` currently accepts only arrays stored as `number[]`. +before changing memory. Both models preserve the array's storage type, including reference and unresolved elements. ## Applicability and residual states @@ -190,7 +190,7 @@ A TypeScript model is ordinary source code: ```typescript export class ArrayModels { - static pop(receiver: number[]): number | undefined { + static pop(receiver: any[]): any { const length = receiver.length; if (length === 0) { return undefined; @@ -216,7 +216,7 @@ val model = TsEtsIrUnknownCallModel( id = "ts.array.pop", target = TsUnknownCallTarget(methodName = "pop"), artifact = artifact, - domainGuard = numberArrayGuard, + domainGuard = arrayGuard, ) val catalog = TsUnknownCallModelCatalog(models = listOf(model)) @@ -225,6 +225,10 @@ 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. +Array indexing and `length` assignment use the receiver's storage type. Writing `length` supports integral values from +zero through the current length, within the configured array-size limit. Growth remains unsupported because the +engine does not represent newly created holes; those paths are pruned. + 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. @@ -321,7 +325,7 @@ independently of that revision, the runner also records the artifact's content h 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. +distinct files with the same signature are rejected, including collisions with application and SDK files. ## 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 3c45d045ab..ed4afa19ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -62,8 +62,9 @@ class TsMachine( ?.additionalSceneFiles ?.takeIf { modelFiles -> modelFiles.isNotEmpty() } ?.let { modelFiles -> + val files = (scene.projectFiles + scene.sdkFiles + modelFiles).deduplicateEtsFilesBySignature() EtsScene( - projectFiles = (scene.projectFiles + modelFiles).deduplicateEtsFilesBySignature(), + projectFiles = files.filter { it !in scene.sdkFiles }, sdkFiles = scene.sdkFiles, projectName = scene.projectName, ) 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 index 876a0bd866..12e51fc3a6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -16,7 +16,6 @@ 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 @@ -71,7 +70,7 @@ internal fun loadEtsIrUnknownCallModelArtifact( } val irBytes = irPath.readBytes() - val file = irPath.inputStream().use { stream -> + val file = irBytes.inputStream().use { stream -> EtsFileDto.loadFromJson(stream).toEtsFile() } val entryPointClass = file.allClasses.singleOrNull { it.name == entryPointClassName } 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 2189765540..609c871413 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 @@ -43,6 +43,7 @@ class TsUnknownCallModelCatalog( additionalSceneFiles = selectedModels .flatMap(TsUnknownCallModel::additionalSceneFiles) .deduplicateEtsFilesBySignature() + .let(Collections::unmodifiableList) } internal fun select(call: TsUnknownCall): TsUnknownCallModel? { 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 4e075e54e6..5ab9ad9772 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 @@ -104,6 +104,7 @@ class TsModelUnknownCallDispatcher( val guardedStateChanges = application.execution.successors.mapIndexed { index, successor -> successor.guard to modelStateChange( call = call, + modelId = application.modelId, successor = successor, preparedUnresolvedResult = preparedUnresolvedResults[index], onApplied = { modelApplied = true }, @@ -153,6 +154,7 @@ class TsModelUnknownCallDispatcher( private fun modelStateChange( call: TsUnknownCall, + modelId: String, successor: TsUnknownCallModelSuccessor, preparedUnresolvedResult: UExpr<*>?, onApplied: () -> Unit, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt index 22832f9301..39f556ab10 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt @@ -2,7 +2,6 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsNumberType import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard import org.usvm.machine.call.TsUnknownCall @@ -33,12 +32,13 @@ internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel { domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiver = inputs.singleOrNull() - if (receiver?.sort != addressSort || receiver.containsFakeObject()) { + val staticType = call.receiver?.source?.type + if (staticType == null || receiver?.sort != addressSort) { falseExpr } else { val array = receiver.asExpr(addressSort) - val receiverType = state.arrayStorageType(array, call.receiver?.source?.type) as? EtsArrayType - if (receiverType?.dimensions != 1 || receiverType.elementType != EtsNumberType) { + val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType + if (array.hasFakeValueBranch() || receiverType?.dimensions != 1) { falseExpr } else { state.memory.types.evalIsSubtype(array, receiverType) 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 9d40f28e96..bbb32d07c0 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 @@ -18,6 +18,7 @@ import org.usvm.machine.types.EtsAuxiliaryType import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult +import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.resolveEtsField @@ -51,7 +52,7 @@ internal fun TsExprResolver.handleAssignToInstanceField( // Check for undefined or null field access. checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null - val arrayType = instanceLocal.type as? EtsArrayType + val arrayType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } as? EtsArrayType if (field.name == "length" && arrayType != null) { return assignToArrayLength( scope = scope, @@ -74,6 +75,8 @@ private fun TsContext.assignToArrayLength( maxArraySize: Int, ): Unit? = with(this) { if (value.sort != fp64Sort) { + logger.warn { "Unsupported array length assignment: expected a numeric value, got ${value.sort}" } + scope.assert(falseExpr) return null } @@ -95,7 +98,7 @@ private fun TsContext.assignToArrayLength( val currentLength = scope.calcOnState { memory.read(lengthLValue) } - val lengthIsIntegral = mkEq(roundTrip, fpLength) + val lengthIsIntegral = mkFpEqualExpr(roundTrip, fpLength) val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxArraySize)) val lengthIsNotGrowing = mkBvSignedLessOrEqualExpr(length, currentLength) 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 index 573ad98ee7..0e22541d97 100644 --- 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 @@ -1,5 +1,5 @@ export class ArrayModels { - static pop(receiver: number[]): number | undefined { + static pop(receiver: any[]): any { const length = receiver.length; if (length === 0) { return undefined; 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 index aff5ccb938..16ba6328a2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -1,6 +1,8 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider @@ -16,6 +18,8 @@ import org.usvm.api.TsTestValue import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.expr.TsSimpleValueResolver +import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.util.TsTestResolver @@ -52,6 +56,66 @@ class TsArrayPopEtsIrModelTest { assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) } + @Test + fun `widened and wrapped receivers retain number array storage`() { + for (methodName in listOf("widenedReceiver", "wrappedReceiver")) { + val result = analyze(methodName = methodName) + + assertEquals(32.0, assertIs(result.values.single()).number, methodName) + assertEquals(listOf("ts.array.pop"), result.modelIds, methodName) + } + } + + @Test + fun `model can be entered again after returning`() { + val result = analyze(methodName = "sequentialPops") + + assertEquals(51.0, assertIs(result.values.single()).number) + assertEquals(listOf("ts.array.pop", "ts.array.pop"), result.modelIds) + } + + @Test + fun `length assignment through aliases updates the original array`() { + for (methodName in listOf("shrinkThroughWidenedAlias", "shrinkThroughWrappedAlias")) { + val result = analyze(methodName = methodName) + + assertEquals(11.0, assertIs(result.values.single()).number, methodName) + } + } + + @Test + fun `negative zero is a valid zero array length`() { + val result = analyze(methodName = "negativeZeroLength") + + assertEquals(0.0, assertIs(result.values.single()).number) + } + + @Test + fun `unsupported length value stops without repeating the assignment`() { + var lengthAssignments = 0 + val observer = object : TsInterpreterObserver { + override fun onAssignStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope, + ) { + if ((stmt.lhv as? EtsInstanceFieldRef)?.field?.name == "length") { + lengthAssignments++ + } + } + } + + val states = TsMachine( + scene = scene, + options = machineOptions.copy(stepLimit = 100uL), + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method("unsupportedLengthValue"))) } + + assertTrue(states.isEmpty()) + assertEquals(1, lengthAssignments) + } + @Test fun `array length growth after pop is unsupported`() { val result = analyze(methodName = "popThenGrow") @@ -77,9 +141,14 @@ class TsArrayPopEtsIrModelTest { } @Test - fun `arrays outside the source model domain use fallback`() { - assertUsesResidualFallback(methodName = "referenceArray") - assertUsesResidualFallback(methodName = "symbolicUnknownArray") + fun `reference and unresolved arrays use the source model`() { + for ((methodName, expected) in listOf("referenceArray" to 42.0, "symbolicUnknownArray" to 47.0)) { + val result = analyze(methodName = methodName) + + assertTrue(result.values.filterIsInstance().any { it.number == expected }, methodName) + assertEquals(listOf("ts.array.pop"), result.modelIds.distinct(), methodName) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }, methodName) + } } @Test @@ -87,7 +156,8 @@ class TsArrayPopEtsIrModelTest { val result = analyze(methodName = "unknownReceiver") assertTrue(result.modelIds.isEmpty()) - assertEquals(listOf(TsUnknownCallOutcome.PATH_STOPPED), result.events.map { it.outcome }) + assertTrue(result.events.isNotEmpty()) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.PATH_STOPPED }) } @Test diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt index b4633a6c04..312b88dbd7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt @@ -29,14 +29,20 @@ class TsArrayShiftMatrixTest { lateinit var directory: Path @TestFactory - fun `concrete array matrix agrees with JavaScript`(): List { + fun `concrete array matrix agrees with JavaScript`(): List = concreteArrayMatrix(methodName = "shift") + + @TestFactory + fun `concrete pop matrix agrees with JavaScript`(): List = concreteArrayMatrix(methodName = "pop") + + private fun concreteArrayMatrix(methodName: String): List { val cases = concreteCases() - val source = directory.resolve("ArrayShiftMatrix.ts") - source.writeText(renderSource(cases, typed = true)) + val source = directory.resolve("ArrayRemovalMatrix-$methodName.ts") + source.writeText(renderSource(cases, typed = true, methodName = methodName)) val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) val methods = scene.projectClasses.single { it.name == "ArrayShiftMatrix" }.methods.associateBy { it.name } val invocations = cases.indices.joinToString(separator = ",") { "new ArrayShiftMatrix().case$it()" } - val oracleSource = renderSource(cases, typed = false) + "\nconsole.log([$invocations].join('\\n'));\n" + val oracleSource = renderSource(cases, typed = false, methodName = methodName) + + "\nconsole.log([$invocations].join('\\n'));\n" val expected = runJavaScript(oracleSource) assertEquals(cases.size, expected.size) @@ -62,7 +68,7 @@ class TsArrayShiftMatrixTest { val actual = values.map { assertIs(it).number } assertEquals(listOf(expected[index].toDouble()), actual) assertEquals(case.shiftCount, events.size) - assertTrue(events.all { it.decision == TsUnknownCallDecision.ModelApplied("ts.array.shift") }) + assertTrue(events.all { it.decision == TsUnknownCallDecision.ModelApplied("ts.array.$methodName") }) } } } @@ -108,7 +114,7 @@ class TsArrayShiftMatrixTest { } } - private fun renderSource(cases: List, typed: Boolean): String = buildString { + private fun renderSource(cases: List, typed: Boolean, methodName: String): String = buildString { appendLine("class ShiftElement {}") appendLine("class ArrayShiftMatrix {") cases.forEachIndexed { index, case -> @@ -120,10 +126,15 @@ class TsArrayShiftMatrixTest { appendLine("const values$annotation = original;") repeat(case.shiftCount) { shift -> - appendLine("const removed$shift = values.shift();") - val value = case.values.getOrElse(shift) { "undefined" } + appendLine("const removed$shift = values.$methodName();") + val removedIndex = if (methodName == "pop") case.values.lastIndex - shift else shift + val value = case.values.getOrElse(removedIndex) { "undefined" } appendLine("if (!(${sameValue("removed$shift", value)})) return -1;") - val tail = case.values.drop(shift + 1) + val tail = if (methodName == "pop") { + case.values.dropLast(shift + 1) + } else { + case.values.drop(shift + 1) + } appendLine("if (original.length !== ${tail.size} || values.length !== ${tail.size}) return -2;") tail.forEachIndexed { tailIndex, tailValue -> appendLine("if (!(${sameValue("original[$tailIndex]", tailValue)})) return -3;") 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 b1d1029474..7a087c90ed 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 @@ -2,16 +2,16 @@ package org.usvm.machine.call import io.mockk.mockk import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsMethodSignature -import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsUnknownType -import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsUnknownType import org.usvm.UMachineOptions import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel import org.usvm.machine.state.TsState import kotlin.test.Test import kotlin.test.assertEquals @@ -158,7 +158,10 @@ class TsUnknownCallModelCatalogTest { assertEquals(listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), catalog.modelIds) assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) assertFailsWith { (catalog.modelIds as MutableList).clear() } - assertEquals(listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), TsBuiltInUnknownCallModels.catalog().modelIds) + assertEquals( + listOf("ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID), + TsBuiltInUnknownCallModels.catalog().modelIds, + ) assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) } @@ -196,6 +199,9 @@ class TsUnknownCallModelCatalogTest { ) assertEquals(listOf(modelFile), catalog.additionalSceneFiles) + assertFailsWith { + (catalog.additionalSceneFiles as MutableList).clear() + } } @Test @@ -237,6 +243,26 @@ class TsUnknownCallModelCatalogTest { assertEquals("Conflicting EtsIR files share signature @test/shared", error.message) } + @Test + fun `SDK and model EtsIR files with the same signature are rejected`() { + val sdkFile = 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 = emptyList(), sdkFiles = listOf(sdkFile)), + options = UMachineOptions(), + tsOptions = TsOptions(), + unknownCallModels = catalog, + ).close() + } + + assertEquals("Conflicting EtsIR files share signature @test/shared", error.message) + } + private fun model( id: String, methodName: String = "target-$id", diff --git a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts index f14a9b4c2e..76424bd250 100644 --- a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -18,6 +18,51 @@ export class ArrayPopEtsIr { return values.pop()! + values.length; } + widenedReceiver(): number { + const values = [10, 20, 30]; + const alias: any[] = values; + return alias.pop() + values.length; + } + + wrappedReceiver(): number { + const values = [10, 20, 30]; + const alias: any = values; + return alias.pop() + values.length; + } + + sequentialPops(): number { + const values = [10, 20, 30]; + const first = values.pop()!; + const second = values.pop()!; + return first + second + values.length; + } + + shrinkThroughWidenedAlias(): number { + const values = [10, 20, 30]; + const alias: any[] = values; + alias.length = 1; + return values.length * 10 + alias.length; + } + + shrinkThroughWrappedAlias(): number { + const values = [10, 20, 30]; + const alias: any = values; + alias.length = 1; + return values.length * 10 + alias.length; + } + + negativeZeroLength(): number { + const values = [10]; + values.length = -0; + return values.length; + } + + unsupportedLengthValue(): number { + const values = [10]; + values.length = "0"; + return values.length; + } + popThenGrow(): number { const values = [10, 20]; values.pop(); From 47048f115d560799e7f130d1cd6ce2921bf04c41 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 13:07:18 +0300 Subject: [PATCH 4/6] Fix EtsIR model ownership and numeric array lengths --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 2 +- .../machine/call/TsEtsIrUnknownCallModel.kt | 70 +++++++++++++++---- .../usvm/machine/call/TsUnknownCallModel.kt | 6 ++ .../machine/call/TsUnknownCallModelCatalog.kt | 17 ++++- .../call/intrinsic/TsArrayPopEtsIrModel.kt | 57 +++++++++------ .../org/usvm/machine/expr/WriteField.kt | 13 ++-- .../machine/call/TsArrayPopEtsIrModelTest.kt | 28 ++++++++ .../TsEtsIrUnknownCallModelExecutionTest.kt | 22 ++++++ .../test/resources/models/ArrayPopEtsIr.ts | 28 ++++++++ 9 files changed, 202 insertions(+), 41 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index ed4afa19ee..1a66df44cc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -52,7 +52,7 @@ class TsMachine( unknownCallDispatcher != null -> null unknownCallModels != null -> unknownCallModels else -> TsBuiltInUnknownCallModels.catalog(tsOptions.unknownCallModelSelection) - } + }?.materializeForMachine() /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */ val unknownCallModelCatalogFingerprint: String? 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 index 12e51fc3a6..0c26bd8579 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -14,6 +14,7 @@ import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt import java.nio.file.Path import java.security.MessageDigest +import java.util.IdentityHashMap import kotlin.io.path.createTempDirectory import kotlin.io.path.deleteIfExists import kotlin.io.path.outputStream @@ -28,11 +29,30 @@ data class TsEtsIrUnknownCallModelArtifact( val entryPoint: EtsMethod, val sourceHash: String, val etsIrHash: String, + internal val etsIrJson: 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" } } + + internal fun materializeFile(): EtsFile = + etsIrJson.byteInputStream().use { stream -> + EtsFileDto.loadFromJson(stream).toEtsFile() + } + + internal fun materializeWith(file: EtsFile): TsEtsIrUnknownCallModelArtifact { + val entryPointClassName = requireNotNull(entryPoint.enclosingClass) { + "EtsIR semantic-model entry point must belong to a class" + }.name + val materializedEntryPoint = findEntryPoint( + file = file, + entryPointClassName = entryPointClassName, + entryPointMethodName = entryPoint.name, + ) + + return copy(file = file, entryPoint = materializedEntryPoint) + } } /** Loads one TypeScript model source with JacoDB's bundled native TypeScript frontend. */ @@ -70,25 +90,18 @@ internal fun loadEtsIrUnknownCallModelArtifact( } val irBytes = irPath.readBytes() - val file = irBytes.inputStream().use { stream -> + val etsIrJson = irBytes.toString(Charsets.UTF_8) + val file = etsIrJson.byteInputStream().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" - } + val entryPoint = findEntryPoint(file, entryPointClassName, entryPointMethodName) TsEtsIrUnknownCallModelArtifact( file = file, entryPoint = entryPoint, sourceHash = sourceBytes.sha256(), etsIrHash = irBytes.sha256(), + etsIrJson = etsIrJson, ) } finally { irPath.deleteIfExists() @@ -129,7 +142,7 @@ class TsEtsIrUnknownCallModel( override val target: TsUnknownCallTarget, val artifact: TsEtsIrUnknownCallModelArtifact, val domainGuard: TsEtsIrUnknownCallModelDomainGuard = TsEtsIrUnknownCallModelDomainGuard.ALWAYS, -) : TsUnknownCallModel { +) : TsUnknownCallModel, TsMachineLocalUnknownCallModel { override val additionalSceneFiles: List = listOf(artifact.file) override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { @@ -160,6 +173,20 @@ class TsEtsIrUnknownCallModel( residualGuard = guard.takeUnless { it == state.ctx.trueExpr }?.let(state.ctx::mkNot), ) } + + override fun materializeForMachine( + materializedFiles: IdentityHashMap, + ): TsUnknownCallModel { + val file = materializedFiles.getOrPut(artifact.file, artifact::materializeFile) + val materializedArtifact = artifact.materializeWith(file) + + return TsEtsIrUnknownCallModel( + id = id, + target = target, + artifact = materializedArtifact, + domainGuard = domainGuard, + ) + } } /** Builds the symbolic input guard for one TypeScript model body. */ @@ -180,6 +207,25 @@ private fun TsUnknownCall.resolvedInputs(): List>? = buildList { arguments.forEach { argument -> add(argument.resolved ?: return null) } } +private fun findEntryPoint( + file: EtsFile, + entryPointClassName: String, + entryPointMethodName: String, +): EtsMethod { + 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" + } + + return entryPoint +} + internal fun TsState.enterEtsIrUnknownCallModel( modelId: String, entryPoint: EtsMethod, 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 c5eaef5038..15d6f5c334 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 @@ -7,6 +7,7 @@ import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.machine.state.TsState import org.usvm.machine.types.TsUnresolvedValue +import java.util.IdentityHashMap /** Declaratively identifies the calls handled by one semantic model. */ data class TsUnknownCallTarget( @@ -39,6 +40,11 @@ interface TsUnknownCallModel { fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? } +/** A model whose mutable EtsIR graph must be materialized for one machine scene. */ +internal interface TsMachineLocalUnknownCallModel : TsUnknownCallModel { + fun materializeForMachine(materializedFiles: IdentityHashMap): TsUnknownCallModel +} + /** Describes how a guarded model successor completes the original call. */ sealed interface TsUnknownCallModelCompletion { /** Produces a normal result on the selected successor state. */ 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 609c871413..f332f2d3dc 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 @@ -7,6 +7,7 @@ import java.nio.ByteBuffer import java.nio.charset.StandardCharsets import java.security.MessageDigest import java.util.Collections +import java.util.IdentityHashMap private const val BYTE_MASK = 0xff @@ -16,6 +17,7 @@ class TsUnknownCallModelCatalog( selection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, ) { private val index: Map>> + private val selectedModels: List val modelIds: List val fingerprint: String @@ -28,7 +30,7 @@ class TsUnknownCallModelCatalog( require(modelsById.put(model.id, model) == null) { "Duplicate semantic model ID: ${model.id}" } } - val selectedModels = when (selection) { + selectedModels = when (selection) { TsUnknownCallModelSelection.All -> modelsById.values is TsUnknownCallModelSelection.Only -> { val unknownIds = selection.ids.subtract(modelsById.keys) @@ -46,6 +48,19 @@ class TsUnknownCallModelCatalog( .let(Collections::unmodifiableList) } + internal fun materializeForMachine(): TsUnknownCallModelCatalog { + val materializedFiles = IdentityHashMap() + val materializedModels = selectedModels.map { model -> + if (model is TsMachineLocalUnknownCallModel) { + model.materializeForMachine(materializedFiles) + } else { + model + } + } + + return TsUnknownCallModelCatalog(materializedModels) + } + internal fun select(call: TsUnknownCall): TsUnknownCallModel? { val candidates = index[call.callee.name]?.get(call.failureReason) ?: return null return candidates[call.callee.enclosingClass.name] ?: candidates[null] diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt index 39f556ab10..e6e0ad88c0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt @@ -2,17 +2,21 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsFile import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsMachineLocalUnknownCallModel import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.state.TsState import org.usvm.util.arrayStorageType +import java.util.IdentityHashMap /** Built-in `Array.pop` implemented by an ordinary TypeScript body. */ -internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel { +internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel, TsMachineLocalUnknownCallModel { override val id: String = "ts.array.pop" override val target = TsUnknownCallTarget( methodName = "pop", @@ -20,36 +24,43 @@ internal object TsArrayPopEtsIrModel : TsBuiltInUnknownCallModel { ) private val model by lazy { - TsEtsIrUnknownCallModel( - id = id, - target = target, - artifact = loadBundledEtsIrUnknownCallModelArtifact( - resourceName = "/org/usvm/machine/call/models/ArrayModels.ts", - sourceFileName = "ArrayModels.ts", - entryPointClassName = "ArrayModels", - entryPointMethodName = "pop", - ), - domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> - with(state.ctx) { - val receiver = inputs.singleOrNull() - val staticType = call.receiver?.source?.type - if (staticType == null || receiver?.sort != addressSort) { + val artifact = loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/ArrayModels.ts", + sourceFileName = "ArrayModels.ts", + entryPointClassName = "ArrayModels", + entryPointMethodName = "pop", + ) + val domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiver = inputs.singleOrNull() + val staticType = call.receiver?.source?.type + if (staticType == null || receiver?.sort != addressSort) { + falseExpr + } else { + val array = receiver.asExpr(addressSort) + val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType + if (array.hasFakeValueBranch() || receiverType?.dimensions != 1) { falseExpr } else { - val array = receiver.asExpr(addressSort) - val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType - if (array.hasFakeValueBranch() || receiverType?.dimensions != 1) { - falseExpr - } else { - state.memory.types.evalIsSubtype(array, receiverType) - } + state.memory.types.evalIsSubtype(array, receiverType) } } - }, + } + } + + TsEtsIrUnknownCallModel( + id = id, + target = target, + artifact = artifact, + domainGuard = domainGuard, ) } override val additionalSceneFiles get() = model.additionalSceneFiles override fun apply(state: TsState, call: TsUnknownCall) = model.apply(state, call) + + override fun materializeForMachine( + materializedFiles: IdentityHashMap, + ): TsUnknownCallModel = model.materializeForMachine(materializedFiles) } 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 bbb32d07c0..8389e205be 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 @@ -15,6 +15,7 @@ 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.machine.types.extractValue import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult @@ -74,13 +75,17 @@ private fun TsContext.assignToArrayLength( value: UExpr<*>, maxArraySize: Int, ): Unit? = with(this) { - if (value.sort != fp64Sort) { - logger.warn { "Unsupported array length assignment: expected a numeric value, got ${value.sort}" } - scope.assert(falseExpr) + val (fpLength, numericTypeGuard) = scope.calcOnState { + with(ctx) { + extractValue(value, fp64Sort, ::getIntermediateFpLValue) + } + } + val numericTypeIsPossible = scope.assert(numericTypeGuard) + if (fpLength == null || numericTypeIsPossible == null) { + logger.warn { "Unsupported array length assignment: runtime value is not numeric (storage sort: ${value.sort})" } return null } - val fpLength = value.asExpr(fp64Sort) val convertedLength = mkFpToBvExpr( roundingMode = fpRoundingModeSortDefaultValue(), value = fpLength, 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 index 16ba6328a2..12b4a37664 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -90,6 +90,31 @@ class TsArrayPopEtsIrModelTest { assertEquals(0.0, assertIs(result.values.single()).number) } + @Test + fun `proven numeric any values can shrink array length`() { + val result = analyze(methodName = "shrinkFromAny") + + assertTrue(result.hasNumber(1.0), "Expected numeric any branch to preserve length 1: ${result.values}") + assertTrue(result.events.isEmpty()) + } + + @Test + fun `symbolic any array pop can shrink array length`() { + val result = analyze(methodName = "shrinkFromSymbolicAnyArray") + + assertTrue(result.hasNumber(1.0), "Expected popped numeric branch to preserve length 1: ${result.values}") + assertEquals(listOf("ts.array.pop"), result.modelIds.distinct()) + } + + @Test + fun `ordinary numeric and concrete any array length controls still shrink`() { + for (methodName in listOf("shrinkFromNumber", "shrinkFromConcreteAnyArray")) { + val result = analyze(methodName = methodName) + + assertTrue(result.hasNumber(1.0), "$methodName did not preserve length 1: ${result.values}") + } + } + @Test fun `unsupported length value stops without repeating the assignment`() { var lengthAssignments = 0 @@ -293,6 +318,9 @@ class TsArrayPopEtsIrModelTest { val events: List, val catalogFingerprint: String?, ) { + fun hasNumber(expected: Double): Boolean = + values.filterIsInstance().any { value -> value.number == expected } + val modelIds: List get() = events.mapNotNull { event -> (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt index 11921093c0..67e2155165 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -19,6 +19,8 @@ import org.usvm.util.getResourcePath import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertIs +import kotlin.test.assertNotSame +import kotlin.test.assertNull import kotlin.test.assertTrue import kotlin.time.Duration @@ -175,6 +177,26 @@ class TsEtsIrUnknownCallModelExecutionTest { assertIs(result.events.single().decision) } + @Test + fun `reused catalog materializes independent model scenes with matching entry points`() { + assertNull(baseArtifact.file.scene) + + val firstMaterialization = models.materializeForMachine() + val secondMaterialization = models.materializeForMachine() + val firstModelFile = firstMaterialization.additionalSceneFiles.single() + val secondModelFile = secondMaterialization.additionalSceneFiles.single() + + assertNotSame(baseArtifact.file, firstModelFile) + assertNotSame(firstModelFile, secondModelFile) + + val absoluteResult = analyze(methodName = "pureArgumentAndReturn") + val incrementResult = analyze(methodName = "receiverStateArgumentAndAlias") + + assertEquals(42.0, assertIs(absoluteResult.values.single()).number) + assertEquals(42.0, assertIs(incrementResult.values.single()).number) + assertNull(baseArtifact.file.scene) + } + private fun model( id: String, targetName: String, diff --git a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts index 76424bd250..853efaf2d1 100644 --- a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -57,6 +57,34 @@ export class ArrayPopEtsIr { return values.length; } + shrinkFromAny(length: any): number { + if (length !== 1) return -1; + const values = [10, 20]; + values.length = length; + return values.length; + } + + shrinkFromSymbolicAnyArray(lengths: any[]): number { + if (lengths.length !== 1 || lengths[0] !== 1) return -1; + const values = [10, 20]; + values.length = lengths.pop(); + return values.length; + } + + shrinkFromNumber(length: number): number { + if (length !== 1) return -1; + const values = [10, 20]; + values.length = length; + return values.length; + } + + shrinkFromConcreteAnyArray(): number { + const lengths: any[] = [1]; + const values = [10, 20]; + values.length = lengths.pop(); + return values.length; + } + unsupportedLengthValue(): number { const values = [10]; values.length = "0"; From 3134d06515bca61ba2a357a67697ac8620b0e420 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 13:10:51 +0300 Subject: [PATCH 5/6] Satisfy array length logging style --- usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 8389e205be..8b9ccee50c 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 @@ -82,7 +82,9 @@ private fun TsContext.assignToArrayLength( } val numericTypeIsPossible = scope.assert(numericTypeGuard) if (fpLength == null || numericTypeIsPossible == null) { - logger.warn { "Unsupported array length assignment: runtime value is not numeric (storage sort: ${value.sort})" } + logger.warn { + "Unsupported array length assignment: runtime value is not numeric (storage sort: ${value.sort})" + } return null } From 8188fecd0c25374439f83bf2e30f153b8d717240 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 17:29:09 +0300 Subject: [PATCH 6/6] [TS Calls] Remove semantic model fingerprints --- usvm-ts/UNKNOWN_CALL_MODELS.md | 18 ++---- .../main/kotlin/org/usvm/machine/TsMachine.kt | 4 -- .../machine/call/TsEtsIrUnknownCallModel.kt | 64 ++++--------------- .../machine/call/TsUnknownCallModelCatalog.kt | 23 ------- .../org/usvm/machine/expr/WriteField.kt | 1 + .../machine/call/TsArrayPopEtsIrModelTest.kt | 31 +++++++-- .../call/TsArrayShiftIntrinsicModelTest.kt | 4 -- .../TsEtsIrUnknownCallModelArtifactTest.kt | 57 ++--------------- .../call/TsUnknownCallModelCatalogTest.kt | 17 ++--- .../test/resources/models/ArrayPopEtsIr.ts | 6 ++ 10 files changed, 64 insertions(+), 161 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index be224ae8ea..b4506e3f6f 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -118,7 +118,7 @@ Examples: - `ts.array.shift` - `node.buffer.copy` -The ID is used for configuration, observer events, recursion prevention, and catalog fingerprints. Do not include: +The ID is used for configuration, observer events, and recursion prevention. Do not include: - an implementation mechanism such as `intrinsic` or `ets-ir`; - a source or EtsIR hash; @@ -141,8 +141,7 @@ TsUnknownCallTarget( Only `methodName` is required. Add `enclosingClassName` or `failureReason` when the method name alone is too broad. The catalog indexes method names, failure reasons, and enclosing classes. Overlapping enabled targets fail while building that index; lookup returns either one model or no match, and never hides ambiguity. Catalog order is never -a priority rule. IDs and their SHA-256 fingerprint are computed once; byte-length prefixes distinguish ID sequences -such as `["ab", "c"]` and `["a", "bc"]`. +a priority rule. The enabled model set is frozen and sorted by ID when the catalog is built. The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in `apply` or in an EtsIR model's domain guard. @@ -312,17 +311,10 @@ lookup declines that redirection and fallback is applied instead of entering an 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 +## Artifacts -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 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. +The loader invokes the native JacoDB TypeScript frontend and keeps an immutable EtsIR JSON snapshot. Each machine +materializes its own EtsIR objects from that snapshot so interpreter-local state cannot leak between analyses. 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, including collisions with application and SDK files. 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 1a66df44cc..637b91d3d2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -54,10 +54,6 @@ class TsMachine( else -> TsBuiltInUnknownCallModels.catalog(tsOptions.unknownCallModelSelection) }?.materializeForMachine() - /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */ - val unknownCallModelCatalogFingerprint: String? - get() = resolvedUnknownCallModels?.fingerprint - private val analysisScene = resolvedUnknownCallModels ?.additionalSceneFiles ?.takeIf { modelFiles -> modelFiles.isNotEmpty() } 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 index 0c26bd8579..c0b11f8be2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -9,33 +9,24 @@ import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.generateEtsIR import org.usvm.UBoolExpr import org.usvm.UExpr +import org.usvm.isFalse +import org.usvm.isTrue 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 java.util.IdentityHashMap import kotlin.io.path.createTempDirectory import kotlin.io.path.deleteIfExists import kotlin.io.path.outputStream -import kotlin.io.path.readBytes +import kotlin.io.path.readText -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. */ +/** 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, internal val etsIrJson: 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" } - } - internal fun materializeFile(): EtsFile = etsIrJson.byteInputStream().use { stream -> EtsFileDto.loadFromJson(stream).toEtsFile() @@ -60,37 +51,17 @@ 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) + val irPath = generateEtsIR( + projectPath = sourcePath, + isProject = false, + loadEntrypoints = true, + useArkAnalyzerTypeInference = null, + provider = EtsIrProvider.TS_FRONTEND, + ) return try { - check(sourcePath.readBytes().contentEquals(sourceBytes)) { - "TypeScript model source changed while generating EtsIR: $sourcePath" - } - - val irBytes = irPath.readBytes() - val etsIrJson = irBytes.toString(Charsets.UTF_8) + val etsIrJson = irPath.readText() val file = etsIrJson.byteInputStream().use { stream -> EtsFileDto.loadFromJson(stream).toEtsFile() } @@ -99,8 +70,6 @@ internal fun loadEtsIrUnknownCallModelArtifact( TsEtsIrUnknownCallModelArtifact( file = file, entryPoint = entryPoint, - sourceHash = sourceBytes.sha256(), - etsIrHash = irBytes.sha256(), etsIrJson = etsIrJson, ) } finally { @@ -156,7 +125,7 @@ class TsEtsIrUnknownCallModel( call = call, inputs = inputs, ) - if (guard == state.ctx.falseExpr) { + if (guard.isFalse) { return null } @@ -170,7 +139,7 @@ class TsEtsIrUnknownCallModel( return TsUnknownCallModelExecution( successors = listOf(successor), - residualGuard = guard.takeUnless { it == state.ctx.trueExpr }?.let(state.ctx::mkNot), + residualGuard = guard.takeUnless { it.isTrue }?.let(state.ctx::mkNot), ) } @@ -251,8 +220,3 @@ internal fun TsState.enterEtsIrUnknownCallModel( 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/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt index f332f2d3dc..ff7db78c35 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 @@ -3,14 +3,9 @@ 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 -import java.security.MessageDigest import java.util.Collections import java.util.IdentityHashMap -private const val BYTE_MASK = 0xff - /** An immutable deterministic set of semantic models used by one machine run. */ class TsUnknownCallModelCatalog( models: Collection, @@ -20,7 +15,6 @@ class TsUnknownCallModelCatalog( private val selectedModels: List val modelIds: List - val fingerprint: String val additionalSceneFiles: List init { @@ -41,7 +35,6 @@ class TsUnknownCallModelCatalog( modelIds = Collections.unmodifiableList(selectedModels.map(TsUnknownCallModel::id)) index = indexModels(selectedModels) - fingerprint = computeFingerprint(modelIds) additionalSceneFiles = selectedModels .flatMap(TsUnknownCallModel::additionalSceneFiles) .deduplicateEtsFilesBySignature() @@ -120,19 +113,3 @@ internal fun Iterable.deduplicateEtsFilesBySignature(): List { return filesBySignature.values.toList() } - -private fun computeFingerprint(modelIds: List): String { - val digest = MessageDigest.getInstance("SHA-256") - modelIds.forEach { digest.updateLengthPrefixed(it) } - - return digest.digest().joinToString(separator = "") { byte -> - "%02x".format(byte.toInt() and BYTE_MASK) - } -} - -/** Length prefixes distinguish ID sequences such as ["ab", "c"] and ["a", "bc"]. */ -private fun MessageDigest.updateLengthPrefixed(value: String) { - val bytes = value.toByteArray(StandardCharsets.UTF_8) - update(ByteBuffer.allocate(Int.SIZE_BYTES).putInt(bytes.size).array()) - update(bytes) -} 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 8b9ccee50c..2a465cc790 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 @@ -80,6 +80,7 @@ private fun TsContext.assignToArrayLength( extractValue(value, fp64Sort, ::getIntermediateFpLValue) } } + // Assertions update both path constraints and cached models through the state forker. val numericTypeIsPossible = scope.assert(numericTypeGuard) if (fpLength == null || numericTypeIsPossible == null) { logger.warn { 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 index 12b4a37664..8cd7b0764c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -15,6 +15,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UMachineOptions import org.usvm.api.TsTestValue +import org.usvm.isTrue import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -28,7 +29,6 @@ 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 @@ -45,7 +45,6 @@ class TsArrayPopEtsIrModelTest { assertIs(result.values.single()) assertEquals(listOf("ts.array.pop"), result.modelIds) - assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}"))) } @Test @@ -115,6 +114,30 @@ class TsArrayPopEtsIrModelTest { } } + @Test + fun `array length assertions update cached models for an unconstrained any value`() { + val method = method(name = "shrinkFromUnconstrainedAny") + + val states = TsMachine( + scene = scene, + options = machineOptions.copy(useSoftConstraints = false), + tsOptions = TsOptions(), + ).use { machine -> machine.analyze(listOf(method)) } + + assertTrue(states.isNotEmpty()) + states.forEach { state -> + val constraints = state.pathConstraints.softConstraintsSourceSequence.toList() + + assertTrue(constraints.isNotEmpty()) + assertTrue(state.models.isNotEmpty()) + assertTrue( + state.models.all { model -> + constraints.all { constraint -> model.eval(constraint).isTrue } + } + ) + } + } + @Test fun `unsupported length value stops without repeating the assignment`() { var lengthAssignments = 0 @@ -225,7 +248,6 @@ class TsArrayPopEtsIrModelTest { assertEquals(32.0, assertIs(result.values.single()).number) assertTrue(result.events.isEmpty()) - assertNull(result.catalogFingerprint) } private fun analyze( @@ -249,7 +271,6 @@ class TsArrayPopEtsIrModelTest { AnalysisResult( values = values, events = observer.events.toList(), - catalogFingerprint = machine.unknownCallModelCatalogFingerprint, ) } } @@ -316,7 +337,6 @@ class TsArrayPopEtsIrModelTest { private data class AnalysisResult( val values: List, val events: List, - val catalogFingerprint: String?, ) { fun hasNumber(expected: Double): Boolean = values.filterIsInstance().any { value -> value.number == expected } @@ -332,6 +352,7 @@ class TsArrayPopEtsIrModelTest { pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), stateCollectionStrategy = StateCollectionStrategy.ALL, exceptionsPropagation = true, + throwExceptionOnStepFailure = true, timeout = Duration.INFINITE, stepsFromLastCovered = 3_500L, solverType = SolverType.YICES, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index ad65cc64ad..6974094ca6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -53,7 +53,6 @@ class TsArrayShiftIntrinsicModelTest { assertIs(result.values.single()) assertEquals(listOf("ts.array.shift"), result.modelIds) - assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}"))) } @Test @@ -276,7 +275,6 @@ class TsArrayShiftIntrinsicModelTest { assertEquals(32.0, assertIs(result.values.single()).number) assertTrue(result.events.isEmpty()) - assertNull(result.catalogFingerprint) } @ParameterizedTest @@ -328,7 +326,6 @@ class TsArrayShiftIntrinsicModelTest { AnalysisResult( values = values, events = observer.events.toList(), - catalogFingerprint = machine.unknownCallModelCatalogFingerprint, ) } } @@ -395,7 +392,6 @@ class TsArrayShiftIntrinsicModelTest { private data class AnalysisResult( val values: List, val events: List, - val catalogFingerprint: String?, ) { val modelIds: List get() = events.mapNotNull { event -> diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt index 6bc6f622e7..16b6c786f3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -1,13 +1,6 @@ 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 @@ -17,55 +10,19 @@ 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( + fun `native frontend loads a reusable model entry point`() { + val artifact = 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}"))) - } + val materialized = artifact.materializeFile() + val materializedArtifact = artifact.materializeWith(materialized) - @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() - } + assertEquals("absolute", artifact.entryPoint.name) + assertEquals(artifact.entryPoint.signature, materializedArtifact.entryPoint.signature) + assertTrue(materializedArtifact.entryPoint.cfg.instructions.isNotEmpty()) } @Test 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 7a087c90ed..e0083ed8ea 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 @@ -16,7 +16,6 @@ import org.usvm.machine.state.TsState import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertFailsWith -import kotlin.test.assertNotEquals import kotlin.test.assertNull import kotlin.test.assertSame import kotlin.test.assertTrue @@ -82,7 +81,7 @@ class TsUnknownCallModelCatalogTest { } @Test - fun `selection and fingerprint do not depend on model order`() { + fun `selection does not depend on model order`() { val forward = listOf( model(id = "a", methodName = "first"), model(id = "b", methodName = "second"), @@ -93,11 +92,10 @@ class TsUnknownCallModelCatalogTest { assertEquals(listOf("a", "b"), first.modelIds) assertEquals(first.modelIds, second.modelIds) - assertEquals(first.fingerprint, second.fingerprint) } @Test - fun `enabled subset is detached and changes fingerprint`() { + fun `enabled subset is detached from mutable selection`() { val mutableIds = mutableSetOf("a") val models = listOf( model(id = "a", methodName = "first"), @@ -105,11 +103,8 @@ class TsUnknownCallModelCatalogTest { ) val onlyA = TsUnknownCallModelCatalog(models, selection = TsUnknownCallModelSelection.Only(mutableIds)) mutableIds += "b" - val both = TsUnknownCallModelCatalog(models) assertEquals(listOf("a"), onlyA.modelIds) - assertNotEquals(onlyA.fingerprint, both.fingerprint) - assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) } @Test @@ -166,12 +161,10 @@ class TsUnknownCallModelCatalogTest { } @Test - fun `fingerprints preserve ID boundaries and no match remains distinct from ambiguity`() { - val left = TsUnknownCallModelCatalog(listOf(model(id = "ab"), model(id = "c"))) - val right = TsUnknownCallModelCatalog(listOf(model(id = "a"), model(id = "bc"))) + fun `unmatched call selects no model`() { + val catalog = TsUnknownCallModelCatalog(listOf(model(id = "known", methodName = "known"))) - assertNotEquals(left.fingerprint, right.fingerprint) - assertNull(left.select(call(className = "A", reason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION))) + assertNull(catalog.select(call(className = "A", reason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION))) } private fun call(className: String, reason: TsUnknownCallFailureReason) = TsUnknownCall( diff --git a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts index 853efaf2d1..afdc204929 100644 --- a/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -85,6 +85,12 @@ export class ArrayPopEtsIr { return values.length; } + shrinkFromUnconstrainedAny(length: any): number { + const values = [10, 20]; + values.length = length; + return values.length; + } + unsupportedLengthValue(): number { const values = [10]; values.length = "0";