diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index f598c5c99..b4506e3f6 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 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 @@ -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, and recursion prevention. 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, ) ``` @@ -139,17 +141,16 @@ 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`. +`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. Both models preserve the array's storage type, including reference and unresolved elements. ## Applicability and residual states @@ -177,10 +178,71 @@ 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: any[]): any { + 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 = arrayGuard, +) + +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. + +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. + +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 +263,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. +- solver operations unavailable in TypeScript; +- type-system operations that cannot be represented faithfully in EtsIR. -Do not write an intrinsic merely because a library method is stateful. - -## 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 +300,24 @@ 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 -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 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. -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. +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. ## Observation 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 12f4cbde2..e58f45f47 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 0e8e6d537..637b91d3d 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, @@ -51,16 +52,28 @@ class TsMachine( unknownCallDispatcher != null -> null unknownCallModels != null -> unknownCallModels else -> TsBuiltInUnknownCallModels.catalog(tsOptions.unknownCallModelSelection) - } - - /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */ - val unknownCallModelCatalogFingerprint: String? - get() = resolvedUnknownCallModels?.fingerprint - - private val graph = TsGraph(scene) - private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) + }?.materializeForMachine() + + private val analysisScene = resolvedUnknownCallModels + ?.additionalSceneFiles + ?.takeIf { modelFiles -> modelFiles.isNotEmpty() } + ?.let { modelFiles -> + val files = (scene.projectFiles + scene.sdkFiles + modelFiles).deduplicateEtsFilesBySignature() + EtsScene( + projectFiles = files.filter { it !in scene.sdkFiles }, + 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( + 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/call/TsEtsIrUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt new file mode 100644 index 000000000..c0b11f8be --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModel.kt @@ -0,0 +1,222 @@ +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.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.util.IdentityHashMap +import kotlin.io.path.createTempDirectory +import kotlin.io.path.deleteIfExists +import kotlin.io.path.outputStream +import kotlin.io.path.readText + +/** Native-frontend artifact for one TypeScript semantic-model entry point. */ +data class TsEtsIrUnknownCallModelArtifact( + val file: EtsFile, + val entryPoint: EtsMethod, + internal val etsIrJson: String, +) { + 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. */ +fun loadEtsIrUnknownCallModelArtifact( + sourcePath: Path, + entryPointClassName: String, + entryPointMethodName: String, +): TsEtsIrUnknownCallModelArtifact { + val irPath = generateEtsIR( + projectPath = sourcePath, + isProject = false, + loadEntrypoints = true, + useArkAnalyzerTypeInference = null, + provider = EtsIrProvider.TS_FRONTEND, + ) + + return try { + val etsIrJson = irPath.readText() + val file = etsIrJson.byteInputStream().use { stream -> + EtsFileDto.loadFromJson(stream).toEtsFile() + } + val entryPoint = findEntryPoint(file, entryPointClassName, entryPointMethodName) + + TsEtsIrUnknownCallModelArtifact( + file = file, + entryPoint = entryPoint, + etsIrJson = etsIrJson, + ) + } 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, TsMachineLocalUnknownCallModel { + 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.isFalse) { + return null + } + + val successor = TsUnknownCallModelSuccessor( + guard = guard, + completion = TsUnknownCallModelCompletion.EtsIrBody( + entryPoint = artifact.entryPoint, + inputs = inputs, + ), + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it.isTrue }?.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. */ +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) } +} + +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, + 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()) +} 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 6334fa48a..15d6f5c33 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,10 +1,13 @@ 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 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( @@ -30,9 +33,18 @@ 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? } +/** 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. */ @@ -49,6 +61,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 ee825bced..ff7db78c3 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,12 +1,10 @@ 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 - -private const val BYTE_MASK = 0xff +import java.util.IdentityHashMap /** An immutable deterministic set of semantic models used by one machine run. */ class TsUnknownCallModelCatalog( @@ -14,9 +12,10 @@ class TsUnknownCallModelCatalog( selection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, ) { private val index: Map>> + private val selectedModels: List val modelIds: List - val fingerprint: String + val additionalSceneFiles: List init { val modelsById = hashMapOf() @@ -25,7 +24,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) @@ -36,7 +35,23 @@ class TsUnknownCallModelCatalog( modelIds = Collections.unmodifiableList(selectedModels.map(TsUnknownCallModel::id)) index = indexModels(selectedModels) - fingerprint = computeFingerprint(modelIds) + additionalSceneFiles = selectedModels + .flatMap(TsUnknownCallModel::additionalSceneFiles) + .deduplicateEtsFilesBySignature() + .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? { @@ -46,6 +61,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,18 +99,17 @@ private fun indexModels( return index } -private fun computeFingerprint(modelIds: List): String { - val digest = MessageDigest.getInstance("SHA-256") - modelIds.forEach { digest.updateLengthPrefixed(it) } +internal fun Iterable.deduplicateEtsFilesBySignature(): List { + val filesBySignature = linkedMapOf() - return digest.digest().joinToString(separator = "") { byte -> - "%02x".format(byte.toInt() and BYTE_MASK) + 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) } -} -/** 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) + return filesBySignature.values.toList() } 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 474494651..5ab9ad977 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, @@ -178,6 +180,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 000000000..e6e0ad88c --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopEtsIrModel.kt @@ -0,0 +1,66 @@ +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, TsMachineLocalUnknownCallModel { + override val id: String = "ts.array.pop" + override val target = TsUnknownCallTarget( + methodName = "pop", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + private val model by lazy { + 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 { + 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/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 841a7fc2b..385cd3867 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/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt index 89c75972b..154d9555a 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 c55366841..2a465cc79 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,12 @@ 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 +import org.usvm.util.arrayStorageType +import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.resolveEtsField @@ -48,10 +53,82 @@ internal fun TsExprResolver.handleAssignToInstanceField( // Check for undefined or null field access. checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null + val arrayType = scope.calcOnState { arrayStorageType(instance, 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) { + val (fpLength, numericTypeGuard) = scope.calcOnState { + with(ctx) { + 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 { + "Unsupported array length assignment: runtime value is not numeric (storage sort: ${value.sort})" + } + return null + } + + 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 lengthLValue = mkArrayLengthLValue(array, arrayType) + val currentLength = scope.calcOnState { + memory.read(lengthLValue) + } + val lengthIsIntegral = mkFpEqualExpr(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) ?: run { + logger.warn { + "Unsupported array length assignment: expected an integral length in [0, current length], " + + "but the constraint is UNSAT: $validLength" + } + return null + } + + 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 70ad6909f..423f5dde7 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 172da6329..019257dd3 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 09ac54368..eae28f6e1 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 000000000..0e22541d9 --- /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: any[]): any { + 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 000000000..8cd7b0764 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopEtsIrModelTest.kt @@ -0,0 +1,363 @@ +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 +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.isTrue +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 +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +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) + } + + @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 `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 `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 `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 + 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") + + 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") + + assertTrue(result.values.isNotEmpty()) + assertEquals(listOf("ts.array.pop"), result.modelIds.distinct()) + } + + @Test + 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 + fun `unknown receiver does not prove an Array pop call`() { + val result = analyze(methodName = "unknownReceiver") + + assertTrue(result.modelIds.isEmpty()) + assertTrue(result.events.isNotEmpty()) + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.PATH_STOPPED }) + } + + @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()) + } + + 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(), + ) + } + } + + 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, + ) { + 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 + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = 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/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index ad65cc64a..6974094ca 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/TsArrayShiftMatrixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt index b4633a6c0..312b88dbd 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/TsEtsIrUnknownCallModelArtifactTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt new file mode 100644 index 000000000..16b6c786f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelArtifactTest.kt @@ -0,0 +1,53 @@ +package org.usvm.machine.call + +import org.usvm.util.getResourcePath +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 loads a reusable model entry point`() { + val artifact = loadEtsIrUnknownCallModelArtifact( + sourcePath = sourcePath, + entryPointClassName = "EtsIrSemanticModels", + entryPointMethodName = "absolute", + ) + + val materialized = artifact.materializeFile() + val materializedArtifact = artifact.materializeWith(materialized) + + assertEquals("absolute", artifact.entryPoint.name) + assertEquals(artifact.entryPoint.signature, materializedArtifact.entryPoint.signature) + assertTrue(materializedArtifact.entryPoint.cfg.instructions.isNotEmpty()) + } + + @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 000000000..67e215516 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsEtsIrUnknownCallModelExecutionTest.kt @@ -0,0 +1,282 @@ +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.assertNotSame +import kotlin.test.assertNull +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", + ), + model( + id = "test.ets-ir.guarded", + targetName = "guarded", + entryPointName = "guarded", + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, _, _ -> state.ctx.falseExpr }, + ), + ), + ) + + @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) + } + + @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) + } + + @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, + 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 658e1e0bd..e0083ed8e 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,15 +2,20 @@ package org.usvm.machine.call import io.mockk.mockk import org.jacodb.ets.model.EtsClassSignature +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 import kotlin.test.assertFailsWith -import kotlin.test.assertNotEquals import kotlin.test.assertNull import kotlin.test.assertSame import kotlin.test.assertTrue @@ -76,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"), @@ -87,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"), @@ -99,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 @@ -149,20 +150,21 @@ 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()) } @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( @@ -179,11 +181,87 @@ 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) + assertFailsWith { + (catalog.additionalSceneFiles as MutableList).clear() + } + } + + @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) + } + + @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", failureReason: TsUnknownCallFailureReason? = null, className: String? = null, + additionalSceneFiles: List = emptyList(), ): TsUnknownCallModel = FakeModel( id = id, target = TsUnknownCallTarget( @@ -191,13 +269,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 000000000..afdc20492 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayPopEtsIr.ts @@ -0,0 +1,139 @@ +// @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; + } + + 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; + } + + 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; + } + + shrinkFromUnconstrainedAny(length: any): number { + const values = [10, 20]; + values.length = length; + return values.length; + } + + unsupportedLengthValue(): number { + const values = [10]; + values.length = "0"; + return 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(); + 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 000000000..3c9c667e5 --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModelCalls.ts @@ -0,0 +1,55 @@ +// @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); + } + + 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 new file mode 100644 index 000000000..c60217e2b --- /dev/null +++ b/usvm-ts/src/test/resources/models/EtsIrSemanticModels.ts @@ -0,0 +1,52 @@ +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 guarded(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; +}