From 04570551338337d79cddeab29e5b687b6036dd15 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 28 Aug 2026 23:13:46 +0300 Subject: [PATCH 1/5] [TS Calls] Add guarded semantic model registry and execution --- .../src/main/kotlin/org/usvm/api/TsMock.kt | 46 ++-- .../main/kotlin/org/usvm/machine/TsMachine.kt | 16 +- .../main/kotlin/org/usvm/machine/TsOptions.kt | 2 + .../call/TsIntrinsicUnknownCallModels.kt | 158 +++++++++++++ .../org/usvm/machine/call/TsUnknownCall.kt | 8 + .../usvm/machine/call/TsUnknownCallModel.kt | 116 ++++++++++ .../call/TsUnknownCallModelRegistry.kt | 157 +++++++++++++ .../usvm/machine/call/TsUnknownCallProfile.kt | 189 +++++++++++---- .../usvm/machine/expr/CallApproximations.kt | 33 ++- .../call/TsArrayPopIntrinsicModelTest.kt | 154 +++++++++++++ .../call/TsUnknownCallDispatcherTest.kt | 217 ++++++++++++++++-- .../call/TsUnknownCallModelRegistryTest.kt | 119 ++++++++++ .../baseline/CallFallbackBaseline.ts | 16 ++ .../resources/models/ArrayPopIntrinsic.ts | 24 ++ 14 files changed, 1167 insertions(+), 88 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt create mode 100644 usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index af7236837..237e0f412 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -8,6 +8,7 @@ import org.usvm.UExpr import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.machine.types.mkFakeValue fun mockMethodCall( @@ -16,27 +17,34 @@ fun mockMethodCall( resultType: EtsType = method.returnType, ) { scope.doWithState { - val result: UExpr<*> - if (resultType is EtsVoidType) { - result = ctx.mkUndefinedValue() - } else { - val sort = ctx.typeToSort(resultType) - result = when (sort) { - is UAddressSort -> makeSymbolicRefUntyped() + mockMethodCall(method = method, resultType = resultType) + } +} + +/** Creates a fresh opaque result directly on this state without applying callee effects or exceptions. */ +fun TsState.mockMethodCall( + method: EtsMethodSignature, + resultType: EtsType = method.returnType, +) { + val result = freshUnknownCallResult(resultType) + methodResult = TsMethodResult.Success.MockedCall(result, method) +} + +private fun TsState.freshUnknownCallResult(resultType: EtsType): UExpr<*> { + if (resultType is EtsVoidType) { + return ctx.mkUndefinedValue() + } - is TsUnresolvedSort -> scope.calcOnState { - mkFakeValue( - scope = scope, - boolValue = makeSymbolicPrimitive(ctx.boolSort), - fpValue = makeSymbolicPrimitive(ctx.fp64Sort), - refValue = makeSymbolicRefUntyped(), - ) - } + return when (val sort = ctx.typeToSort(resultType)) { + is UAddressSort -> makeSymbolicRefUntyped() - else -> makeSymbolicPrimitive(sort) - } - } + is TsUnresolvedSort -> mkFakeValue( + scope = null, + boolValue = makeSymbolicPrimitive(ctx.boolSort), + fpValue = makeSymbolicPrimitive(ctx.fp64Sort), + refValue = makeSymbolicRefUntyped(), + ) - methodResult = TsMethodResult.Success.MockedCall(result, method) + else -> makeSymbolicPrimitive(sort) } } 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 3d6b394f3..f08a486a4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -9,6 +9,7 @@ import org.usvm.StateCollectionStrategy import org.usvm.UMachine import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget +import org.usvm.machine.call.TsBuiltInUnknownCallModels import org.usvm.machine.call.TsNoUnknownCallModels import org.usvm.machine.call.TsProfileUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher @@ -45,15 +46,26 @@ class TsMachine( private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, - unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + unknownCallModelProvider: TsUnknownCallModelProvider? = null, ) : UMachine() { private val graph = TsGraph(scene) private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) + private val frozenUnknownCallModels = when { + unknownCallDispatcher != null || unknownCallModelProvider != null -> null + else -> TsBuiltInUnknownCallModels.registry.freeze(tsOptions.unknownCallModels.enabledModelIds) + } + + /** Fingerprint of the frozen built-in catalog, or `null` when custom dispatch/model wiring is used. */ + val unknownCallModelCatalogFingerprint: String? + get() = frozenUnknownCallModels?.fingerprint + + private val resolvedUnknownCallModelProvider = + unknownCallModelProvider ?: frozenUnknownCallModels ?: TsNoUnknownCallModels private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( profile = tsOptions.unknownCallProfile, - modelProvider = unknownCallModelProvider, + modelProvider = resolvedUnknownCallModelProvider, observer = observer, ) private val interpreter = TsInterpreter( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 09c3e6659..6b22c8831 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,5 +1,6 @@ package org.usvm.machine +import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.call.TsUnknownCallProfile import org.usvm.machine.call.TsUnknownCallProfiles @@ -8,4 +9,5 @@ data class TsOptions( val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP, + val unknownCallModels: TsUnknownCallModelSelection = TsUnknownCallModelSelection(), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt new file mode 100644 index 000000000..d2899c1a5 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt @@ -0,0 +1,158 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.usvm.UAddressSort +import org.usvm.UExpr +import org.usvm.USort +import org.usvm.api.typeStreamOf +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.types.firstOrNull +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +/** Builds constraint-level execution plans directly from a TypeScript symbolic state. */ +fun interface TsIntrinsicUnknownCallModel { + fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution +} + +/** Opaque registry handle for a Kotlin intrinsic semantic model. */ +class TsIntrinsicUnknownCallModelImplementation( + val model: TsIntrinsicUnknownCallModel, +) : TsUnknownCallModelImplementation { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC +} + +/** Executes intrinsic model handles without exposing them to the common registry or dispatcher contract. */ +object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC + + override fun execute( + implementation: TsUnknownCallModelImplementation, + state: TsState, + call: TsUnknownCall, + ): TsUnknownCallModelExecution { + val intrinsic = requireNotNull(implementation as? TsIntrinsicUnknownCallModelImplementation) { + "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}" + } + + return intrinsic.model.execute(state = state, call = call) + } +} + +/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */ +object TsBuiltInUnknownCallModels { + const val ARRAY_POP_MODEL_ID: String = "ts.array.pop" + + private val arrayPopDescriptor = TsUnknownCallModelDescriptor( + id = ARRAY_POP_MODEL_ID, + matcher = TsUnknownCallModelMatcher { call -> + call.failureReason == TsUnknownCallFailureReason.PARTIAL_APPROXIMATION && + call.callee.name == "pop" + }, + supportedDomain = TsUnknownCallModelSupportedDomain( + id = "native-array-pop", + description = "Resolved one-dimensional native arrays with no arguments and a resolved element sort", + ), + precision = TsUnknownCallModelPrecision.PARTIAL, + implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, + ) + + val registry = TsUnknownCallModelRegistry( + registrations = listOf( + TsUnknownCallModelRegistration( + descriptor = arrayPopDescriptor, + implementation = TsIntrinsicUnknownCallModelImplementation(TsArrayPopIntrinsicModel), + ), + ), + backends = listOf(TsIntrinsicUnknownCallModelBackend), + ) +} + +private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { + override fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val input = resolveInput(state = state, call = call) + ?: return unsupportedExecution(state) + + val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType) + val length = state.memory.read(lengthLValue) + val zero = state.ctx.mkBv(0) + val emptyGuard = state.ctx.mkEq(length, zero) + val nonEmptyGuard = state.ctx.mkBvSignedLessExpr(zero, length) + val residualGuard = state.ctx.mkNot(state.ctx.mkOr(emptyGuard, nonEmptyGuard)) + val newLength = state.ctx.mkBvSubExpr(length, state.ctx.mkBv(1)) + val lastElementLValue = mkArrayIndexLValue( + sort = input.elementSort, + ref = input.array, + index = newLength, + type = input.arrayType, + ) + + val emptySuccessor = TsUnknownCallModelSuccessor( + guard = emptyGuard, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + val nonEmptySuccessor = TsUnknownCallModelSuccessor( + guard = nonEmptyGuard, + completion = TsUnknownCallModelCompletion.Normal { memory.read(lastElementLValue) }, + applyStateChanges = { + memory.write(lengthLValue, newLength, guard = ctx.trueExpr) + }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(emptySuccessor, nonEmptySuccessor), + residualGuard = residualGuard, + ) + } + + private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayPopInput? { + if (call.arguments.isNotEmpty()) { + return null + } + + val receiverValue = call.receiver?.resolved ?: return null + if (receiverValue.sort != state.ctx.addressSort) { + return null + } + + val array = receiverValue.asExpr(state.ctx.addressSort) + val sourceType = requireNotNull(call.receiver).source.type + val memoryType = state.memory.typeStreamOf(array).firstOrNull() + val arrayType = sequenceOf(memoryType, sourceType) + .mapNotNull { it as? EtsArrayType } + .firstOrNull { candidate -> + candidate.dimensions == 1 && state.ctx.typeToSort(candidate.elementType) !is TsUnresolvedSort + } + ?: return null + + val elementSort = state.ctx.typeToSort(arrayType.elementType) + + return ArrayPopInput( + array = array, + arrayType = arrayType, + elementSort = elementSort, + ) + } + + private fun unsupportedExecution(state: TsState): TsUnknownCallModelExecution { + val unreachableSuccessor = TsUnknownCallModelSuccessor( + guard = state.ctx.falseExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(unreachableSuccessor), + residualGuard = state.ctx.trueExpr, + ) + } + + private class ArrayPopInput( + val array: UExpr, + val arrayType: EtsArrayType, + val elementSort: USort, + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index bb99b6ec9..1497688f8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt @@ -60,6 +60,7 @@ enum class TsUnknownCallFailureReason { METHOD_BODY_UNAVAILABLE, INTERPROCEDURAL_ANALYSIS_DISABLED, LOGGING_CALL, + PARTIAL_APPROXIMATION, } /** Handles TypeScript calls that could not be executed by the regular call pipeline. */ @@ -67,6 +68,9 @@ fun interface TsUnknownCallDispatcher { fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome } +/** Marks profile dispatchers that replace migrated compatibility approximations with registered models. */ +interface TsUnknownCallModelDispatcher : TsUnknownCallDispatcher + /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { @@ -109,6 +113,10 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { scope.assert(falseExpr) return TsUnknownCallOutcome.PATH_STOPPED } + + TsUnknownCallFailureReason.PARTIAL_APPROXIMATION -> { + error("Migrated approximations must not be sent to the compatibility dispatcher") + } } } } 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 new file mode 100644 index 000000000..f1aab3a9c --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -0,0 +1,116 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsType +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.machine.state.TsState + +/** Identifies the backend that executes a semantic model implementation. */ +enum class TsUnknownCallModelImplementationKind { + INTRINSIC, +} + +/** Describes the semantic precision of a model within its declared supported domain. */ +enum class TsUnknownCallModelPrecision { + EXACT, + PARTIAL, +} + +/** Documents the inputs for which a semantic model provides its declared precision. */ +data class TsUnknownCallModelSupportedDomain( + val id: String, + val description: String, +) { + init { + require(id.isNotBlank()) { "Semantic model supported-domain ID must not be blank" } + require(description.isNotBlank()) { "Semantic model supported-domain description must not be blank" } + } +} + +/** Selects calls that are candidates for one semantic model without depending on its implementation backend. */ +fun interface TsUnknownCallModelMatcher { + fun matches(call: TsUnknownCall): Boolean +} + +/** Backend-neutral metadata used to select and audit one semantic model. */ +class TsUnknownCallModelDescriptor( + val id: String, + val matcher: TsUnknownCallModelMatcher, + val supportedDomain: TsUnknownCallModelSupportedDomain, + val precision: TsUnknownCallModelPrecision, + val implementationKind: TsUnknownCallModelImplementationKind, +) { + init { + require(id.isNotBlank()) { "Semantic model ID must not be blank" } + } +} + +/** Describes how a guarded model successor completes the original call. */ +sealed interface TsUnknownCallModelCompletion { + /** Produces a normal result on the selected successor state. */ + class Normal( + val result: TsState.() -> UExpr<*>, + ) : TsUnknownCallModelCompletion + + /** Produces an exceptional result and its TypeScript type on the selected successor state. */ + class Exceptional( + val exception: TsState.() -> Pair, EtsType>, + ) : TsUnknownCallModelCompletion +} + +/** + * One guarded model successor. + * + * Successor guards within one execution must be pairwise disjoint. State changes and completion values are evaluated + * only after the dispatcher has selected the corresponding successor state. + */ +class TsUnknownCallModelSuccessor( + val guard: UBoolExpr, + val completion: TsUnknownCallModelCompletion, + val applyStateChanges: TsState.() -> Unit = {}, +) + +/** + * A backend-neutral semantic-model execution plan. + * + * [residualGuard] denotes the unsupported part of a partial model's domain. Together, successor guards and the + * residual guard must partition the current call domain. + */ +class TsUnknownCallModelExecution( + successors: List, + val residualGuard: UBoolExpr?, +) { + val successors: List = successors.toList() + + init { + require(this.successors.isNotEmpty()) { "A semantic model must declare at least one guarded successor" } + } +} + +/** The result of selecting and executing a semantic model for one call. */ +sealed interface TsUnknownCallModelApplication { + /** A structured guarded plan produced by the selected model. */ + class Applied( + val modelId: String, + val precision: TsUnknownCallModelPrecision, + val execution: TsUnknownCallModelExecution, + ) : TsUnknownCallModelApplication { + init { + require(modelId.isNotBlank()) { "Applied model ID must not be blank" } + require(precision != TsUnknownCallModelPrecision.EXACT || execution.residualGuard == null) { + "Exact semantic model $modelId must not produce a residual guard" + } + require(precision != TsUnknownCallModelPrecision.PARTIAL || execution.residualGuard != null) { + "Partial semantic model $modelId must produce a residual guard" + } + } + } + + /** Indicates that no enabled model matched the call. */ + data object NotApplicable : TsUnknownCallModelApplication +} + +/** Selects and executes models without exposing registry or backend details to the dispatcher. */ +fun interface TsUnknownCallModelProvider { + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt new file mode 100644 index 000000000..e80ed4cca --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -0,0 +1,157 @@ +package org.usvm.machine.call + +import org.usvm.machine.state.TsState +import java.nio.ByteBuffer +import java.nio.charset.StandardCharsets +import java.security.MessageDigest + +private const val BYTE_MASK = 0xff + +/** Opaque semantic-model implementation selected by its [kind]. */ +interface TsUnknownCallModelImplementation { + val kind: TsUnknownCallModelImplementationKind +} + +/** Executes opaque model implementations of one [kind]. */ +interface TsUnknownCallModelBackend { + val kind: TsUnknownCallModelImplementationKind + + fun execute( + implementation: TsUnknownCallModelImplementation, + state: TsState, + call: TsUnknownCall, + ): TsUnknownCallModelExecution +} + +/** Binds backend-neutral model metadata to an opaque backend implementation. */ +data class TsUnknownCallModelRegistration( + val descriptor: TsUnknownCallModelDescriptor, + val implementation: TsUnknownCallModelImplementation, +) { + init { + require(descriptor.implementationKind == implementation.kind) { + "Semantic model ${descriptor.id} declares ${descriptor.implementationKind} " + + "but provides ${implementation.kind}" + } + } +} + +/** Validates semantic-model registrations and freezes deterministic per-run subsets. */ +class TsUnknownCallModelRegistry( + registrations: Collection, + backends: Collection = emptyList(), +) { + private val registrations = registrations.sortedBy { it.descriptor.id } + private val backends = backends.associateBackendKinds() + + init { + val duplicateIds = this.registrations + .groupingBy { it.descriptor.id } + .eachCount() + .filterValues { count -> count > 1 } + .keys + .sorted() + + require(duplicateIds.isEmpty()) { + "Duplicate semantic model IDs: ${duplicateIds.joinToString()}" + } + } + + /** Freezes an immutable enabled subset; `null` enables the complete registered catalog. */ + fun freeze(enabledModelIds: Set? = null): TsFrozenUnknownCallModelRegistry { + val enabledIds = enabledModelIds?.toSet() + val knownIds = registrations.mapTo(mutableSetOf()) { it.descriptor.id } + val unknownIds = enabledIds.orEmpty().subtract(knownIds).sorted() + + require(unknownIds.isEmpty()) { + "Unknown semantic model IDs: ${unknownIds.joinToString()}" + } + + val enabledRegistrations = when (enabledIds) { + null -> registrations + else -> registrations.filter { it.descriptor.id in enabledIds } + } + + return TsFrozenUnknownCallModelRegistry(enabledRegistrations, backends) + } + + private fun Collection.associateBackendKinds(): + Map { + val duplicateKinds = groupingBy { it.kind } + .eachCount() + .filterValues { count -> count > 1 } + .keys + .sortedBy { it.name } + + require(duplicateKinds.isEmpty()) { + "Duplicate semantic model backends: ${duplicateKinds.joinToString()}" + } + + return associateBy { it.kind } + } +} + +/** Selects all registered models or a defensively copied explicit subset for one machine run. */ +class TsUnknownCallModelSelection( + enabledModelIds: Set? = null, +) { + val enabledModelIds: Set? = enabledModelIds?.toSet() +} + +/** An immutable deterministic semantic-model catalog used by one machine run. */ +class TsFrozenUnknownCallModelRegistry internal constructor( + private val registrations: List, + private val backends: Map, +) : TsUnknownCallModelProvider { + val descriptors: List = registrations.map { it.descriptor } + val fingerprint: String = computeFingerprint(registrations) + + internal fun select(call: TsUnknownCall): TsUnknownCallModelRegistration? { + val matches = registrations.filter { it.descriptor.matcher.matches(call) } + + check(matches.size <= 1) { + val modelIds = matches.map { it.descriptor.id }.sorted() + "Ambiguous semantic models matched: ${modelIds.joinToString()}" + } + + return matches.singleOrNull() + } + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val registration = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + val implementationKind = registration.descriptor.implementationKind + val backend = checkNotNull(backends[implementationKind]) { + "No semantic model backend configured for $implementationKind" + } + val execution = backend.execute( + implementation = registration.implementation, + state = state, + call = call, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = registration.descriptor.id, + precision = registration.descriptor.precision, + execution = execution, + ) + } +} + +private fun computeFingerprint(registrations: List): String { + val digest = MessageDigest.getInstance("SHA-256") + + registrations.forEach { registration -> + digest.updateLengthPrefixed(registration.descriptor.id) + digest.updateLengthPrefixed(registration.descriptor.implementationKind.name) + } + + return digest.digest().joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and BYTE_MASK) + } +} + +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/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index 66e4eeb1f..825cd8726 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -4,6 +4,8 @@ import org.jacodb.ets.model.EtsClassSignature import org.usvm.api.mockMethodCall import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.machine.state.newStmt /** The externally observable decision made for a call that could not be executed normally. */ @@ -61,34 +63,9 @@ object TsUnknownCallProfiles { ) } -/** The result of asking a model provider to handle one unknown call. */ -sealed interface TsUnknownCallModelApplication { - /** Identifies the semantic model that produced the successor states. */ - data class Applied( - val modelId: String, - ) : TsUnknownCallModelApplication { - init { - require(modelId.isNotBlank()) { "Applied model ID must not be blank" } - } - } - - /** Indicates that the provider has no semantic model for this call. */ - data object NotApplicable : TsUnknownCallModelApplication -} - -/** - * Applies semantic models without exposing their lookup or registry implementation to the dispatcher. - * - * A provider returning [TsUnknownCallModelApplication.Applied] must update the supplied scope with the model's - * successor states. The deterministic registry and concrete model implementations are introduced separately. - */ -fun interface TsUnknownCallModelProvider { - fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication -} - /** Empty provider used until an explicit model registry is configured. */ object TsNoUnknownCallModels : TsUnknownCallModelProvider { - override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication = + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication = TsUnknownCallModelApplication.NotApplicable } @@ -97,32 +74,39 @@ class TsProfileUnknownCallDispatcher( private val profile: TsUnknownCallProfile, private val modelProvider: TsUnknownCallModelProvider, private val observer: TsInterpreterObserver? = null, -) : TsUnknownCallDispatcher { +) : TsUnknownCallModelDispatcher { override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - val residualReason = when (profile.modelLookup) { - TsUnknownCallModelLookup.DISABLED -> { - TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED - } + if (profile.modelLookup == TsUnknownCallModelLookup.DISABLED) { + return applyResidualFallback( + scope = scope, + call = call, + reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, + ) + } - TsUnknownCallModelLookup.ENABLED -> { - when (val application = modelProvider.apply(scope, call)) { - is TsUnknownCallModelApplication.Applied -> { - val event = event( - call = call, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId), - ) - observer?.onUnknownCallSafely(event) - return TsUnknownCallOutcome.MODEL_APPLIED - } + val application = scope.calcOnState { + modelProvider.apply(state = this, call = call) + } + return when (application) { + is TsUnknownCallModelApplication.Applied -> applyModel( + scope = scope, + call = call, + application = application, + ) - TsUnknownCallModelApplication.NotApplicable -> { - TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE - } - } - } + TsUnknownCallModelApplication.NotApplicable -> applyResidualFallback( + scope = scope, + call = call, + reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, + ) } + } + private fun applyResidualFallback( + scope: TsStepScope, + call: TsUnknownCall, + reason: TsUnknownCallResidualReason, + ): TsUnknownCallOutcome { val residualPolicy = profile.residualPolicyFor(call) val outcome = when (residualPolicy) { TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED @@ -133,7 +117,7 @@ class TsProfileUnknownCallDispatcher( outcome = outcome, decision = TsUnknownCallDecision.ResidualFallback( policy = residualPolicy, - reason = residualReason, + reason = reason, ), ) when (residualPolicy) { @@ -152,6 +136,115 @@ class TsProfileUnknownCallDispatcher( return outcome } + private fun applyModel( + scope: TsStepScope, + call: TsUnknownCall, + application: TsUnknownCallModelApplication.Applied, + ): TsUnknownCallOutcome { + val residualGuard = application.execution.residualGuard + val residualPolicy = profile.residualPolicyFor(call) + val stoppedResidualIsSatisfiable = residualGuard != null && + residualPolicy == TsResidualCallPolicy.STOP_PATH && + scope.checkSat(residualGuard) != null + + var modelApplied = false + var modelEventReported = false + var freshResidualApplied = false + val guardedStateChanges = application.execution.successors.map { successor -> + successor.guard to modelStateChange( + call = call, + application = application, + successor = successor, + onApplied = { + modelApplied = true + if (modelEventReported) { + false + } else { + modelEventReported = true + true + } + }, + ) + }.toMutableList() + + if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + guardedStateChanges += residualGuard to { + mockMethodCall(method = call.callee, resultType = call.resultType) + newStmt(call.callSite) + freshResidualApplied = true + + val event = residualEvent( + call = call, + policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ) + observer?.onUnknownCallSafely(event) + } + } + + scope.forkMulti(guardedStateChanges) + + if (stoppedResidualIsSatisfiable) { + val event = residualEvent( + call = call, + policy = TsResidualCallPolicy.STOP_PATH, + ) + observer?.onUnknownCallSafely(event) + } + + return when { + modelApplied -> TsUnknownCallOutcome.MODEL_APPLIED + freshResidualApplied -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + stoppedResidualIsSatisfiable -> TsUnknownCallOutcome.PATH_STOPPED + else -> error("Semantic model ${application.modelId} produced no satisfiable successor or residual state") + } + } + + private fun modelStateChange( + call: TsUnknownCall, + application: TsUnknownCallModelApplication.Applied, + successor: TsUnknownCallModelSuccessor, + onApplied: () -> Boolean, + ): TsState.() -> Unit = { + successor.applyStateChanges(this) + + when (val completion = successor.completion) { + is TsUnknownCallModelCompletion.Normal -> { + val result = completion.result(this) + methodResult = TsMethodResult.Success.MockedCall(result, call.callee) + newStmt(call.callSite) + } + + is TsUnknownCallModelCompletion.Exceptional -> { + val (exception, type) = completion.exception(this) + methodResult = TsMethodResult.TsException(exception, type) + } + } + + if (onApplied()) { + val event = event( + call = call, + outcome = TsUnknownCallOutcome.MODEL_APPLIED, + decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId), + ) + observer?.onUnknownCallSafely(event) + } + } + + private fun residualEvent( + call: TsUnknownCall, + policy: TsResidualCallPolicy, + ) = event( + call = call, + outcome = when (policy) { + TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + }, + decision = TsUnknownCallDecision.ResidualFallback( + policy = policy, + reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, + ), + ) + private fun event( call: TsUnknownCall, outcome: TsUnknownCallOutcome, 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 0060b4762..9aa5a437c 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 @@ -19,10 +19,14 @@ import org.usvm.api.memcpy import org.usvm.api.typeStreamOf import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsSizeSort +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelDispatcher +import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult.Companion.from import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.markResolved import org.usvm.machine.interpreter.setResolvedValue +import org.usvm.machine.state.lastStmt import org.usvm.sizeSort import org.usvm.types.first import org.usvm.types.firstOrNull @@ -107,7 +111,12 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return from(handleArrayPop(expr, instanceType, elementSort)) + return handleArrayPopCall( + expr = expr, + instanceType = instanceType, + elementSort = elementSort, + resolvedReceiver = instance, + ) } // Handle `Array.fill() method calls @@ -159,6 +168,28 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return TsExprApproximationResult.NoApproximation } +private fun TsExprResolver.handleArrayPopCall( + expr: EtsInstanceCallExpr, + instanceType: EtsArrayType, + elementSort: USort, + resolvedReceiver: UExpr<*>, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return from(handleArrayPop(expr, instanceType, elementSort)) + } + + dispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = resolvedReceiver, + ) + + return TsExprApproximationResult.ResolveFailure +} + private fun TsExprResolver.handleValueOf(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { if (expr.args.isNotEmpty()) { logger.warn { "valueOf() should have no arguments, but got ${expr.args.size}" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt new file mode 100644 index 000000000..279f0bfbf --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt @@ -0,0 +1,154 @@ +package org.usvm.machine.call + +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.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 TsArrayPopIntrinsicModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayPopIntrinsic.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `empty array pop returns undefined through intrinsic 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 returns last element and shrinks array`() { + 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 `array pop preserves a returned reference alias`() { + val result = analyze(methodName = "aliasedElement") + + assertTrue(result.values.isNotEmpty(), "No final states; events=${result.events}") + assertEquals(42.0, assertIs(result.values.single()).number) + assertEquals(listOf("ts.array.pop"), result.modelIds) + } + + @Test + fun `disabled model sends pop to configured residual fallback`() { + val enabledModelIds = mutableSetOf("ts.array.pop") + val selection = TsUnknownCallModelSelection(enabledModelIds = enabledModelIds) + enabledModelIds.clear() + val result = analyze( + methodName = "nonEmptyArray", + tsOptions = TsOptions( + unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + unknownCallModels = TsUnknownCallModelSelection(enabledModelIds = emptySet()), + ), + ) + val selectedResult = analyze( + methodName = "nonEmptyArray", + tsOptions = TsOptions(unknownCallModels = selection), + ) + + assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), result.events.map { it.outcome }) + assertIs(result.events.single().decision) + assertEquals(listOf("ts.array.pop"), selectedResult.modelIds) + } + + @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 method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "ArrayPopIntrinsic" } + .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/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index 5233e5280..e06985687 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call import io.ksmt.utils.asExpr +import io.mockk.mockk import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod @@ -9,6 +10,7 @@ import org.jacodb.ets.model.EtsPtrCallExpr import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsVoidType import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.callExpr @@ -17,9 +19,10 @@ import org.junit.jupiter.api.Test import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy +import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef +import org.usvm.UExpr import org.usvm.UMachineOptions -import org.usvm.api.mockMethodCall import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.machine.TsInterpreterObserver @@ -28,7 +31,6 @@ import org.usvm.machine.TsOptions import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState -import org.usvm.machine.state.newStmt import org.usvm.util.getResourcePath import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -144,13 +146,98 @@ class TsUnknownCallDispatcherTest { @Test fun `applied model decisions require non blank identifiers`() { assertFailsWith { - TsUnknownCallModelApplication.Applied(modelId = " ") + TsUnknownCallModelApplication.Applied( + modelId = " ", + precision = TsUnknownCallModelPrecision.EXACT, + execution = exactExecution(), + ) } assertFailsWith { TsUnknownCallDecision.ModelApplied(modelId = "") } } + @Test + fun `model applications enforce exact and partial residual contracts`() { + assertFailsWith { + TsUnknownCallModelApplication.Applied( + modelId = "invalid-exact", + precision = TsUnknownCallModelPrecision.EXACT, + execution = execution(residualGuard = mockk()), + ) + } + assertFailsWith { + TsUnknownCallModelApplication.Applied( + modelId = "invalid-partial", + precision = TsUnknownCallModelPrecision.PARTIAL, + execution = execution(residualGuard = null), + ) + } + } + + @Test + fun `partial model sends only residual domain to fresh fallback`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + modelProvider = SupportedTrueResidualFalseProvider, + observer = observer, + ) + + assertEquals(2, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), + observer.events.map { it.outcome }, + ) + } + + @Test + fun `partial model sends residual domain to stop fallback`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = SupportedTrueResidualFalseProvider, + observer = observer, + ) + + assertEquals(1, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.PATH_STOPPED), + observer.events.map { it.outcome }, + ) + } + + @Test + fun `exceptional model successor preserves exception state`() { + val states = analyzeAllStates( + methodName = "modeledUnknownCallThrows", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = ExceptionalModelProvider, + ) + + assertIs(states.single().methodResult) + } + + @Test + fun `stateful model can return an existing reference alias`() { + val states = analyzeAllStates( + methodName = "modeledUnknownCallReturnsAlias", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = StatefulAliasModelProvider, + ) + val aliasReturn = method(fullScene, "modeledUnknownCallReturnsAlias") + .cfg + .stmts + .filterIsInstance() + .first() + + val state = states.single() + assertTrue(aliasReturn in state.pathNode.allStatements) + assertTrue(STATE_CHANGE_MARKER in state.addedArtificialLocals) + } + @Test fun `profiles select model lookup independently from residual fallback`() { val cases = listOf( @@ -577,27 +664,106 @@ class TsUnknownCallDispatcherTest { } private object ApplyingModelProvider : TsUnknownCallModelProvider { - override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { - mockMethodCall(scope, call.callee, call.resultType) - scope.doWithState { newStmt(call.callSite) } - return TsUnknownCallModelApplication.Applied(modelId = "applying-model") + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "applying-model", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = null, + ), + ) } } private object ForkingModelProvider : TsUnknownCallModelProvider { - override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { val result = requireNotNull(call.arguments.single().resolved) - val condition = scope.calcOnState { result.asExpr(ctx.boolSort) } - val completeCall: TsState.() -> Unit = { - methodResult = TsMethodResult.Success.MockedCall(result, call.callee) - newStmt(call.callSite) - } - scope.fork( - condition = condition, - blockOnTrueState = completeCall, - blockOnFalseState = completeCall, + val condition = result.asExpr(state.ctx.boolSort) + val completion = TsUnknownCallModelCompletion.Normal { result } + + return TsUnknownCallModelApplication.Applied( + modelId = "forking-model", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = condition, + completion = completion, + ), + TsUnknownCallModelSuccessor( + guard = state.ctx.mkNot(condition), + completion = completion, + ), + ), + residualGuard = null, + ), + ) + } + } + + private object SupportedTrueResidualFalseProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val result = requireNotNull(call.arguments.single().resolved) + val condition = result.asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "partial-model", + precision = TsUnknownCallModelPrecision.PARTIAL, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), + ), + ) + } + } + + private object ExceptionalModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Exceptional { + ctx.mkUndefinedValue() to EtsStringType + }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "exceptional-model", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = null, + ), + ) + } + } + + private object StatefulAliasModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val argument = requireNotNull(call.arguments.single().resolved) + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { argument }, + applyStateChanges = { addedArtificialLocals += STATE_CHANGE_MARKER }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "stateful-alias-model", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = null, + ), ) - return TsUnknownCallModelApplication.Applied(modelId = "forking-model") } } @@ -658,6 +824,21 @@ class TsUnknownCallDispatcherTest { } private companion object { + const val STATE_CHANGE_MARKER = "semantic-model-state-change" + + fun exactExecution(): TsUnknownCallModelExecution = execution(residualGuard = null) + + fun execution(residualGuard: UBoolExpr?): TsUnknownCallModelExecution = + TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = mockk(), + completion = TsUnknownCallModelCompletion.Normal { mockk>() }, + ), + ), + residualGuard = residualGuard, + ) + val machineOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), exceptionsPropagation = true, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt new file mode 100644 index 000000000..6cc5be150 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -0,0 +1,119 @@ +package org.usvm.machine.call + +import io.mockk.mockk +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotEquals +import kotlin.test.assertTrue + +class TsUnknownCallModelRegistryTest { + @Test + fun `descriptor IDs and supported domains must be non blank`() { + assertFailsWith { + descriptor(id = " ") + } + assertFailsWith { + descriptor(id = "model", domainId = "") + } + assertFailsWith { + descriptor(id = "model", domainDescription = " ") + } + } + + @Test + fun `duplicate IDs are rejected`() { + val error = assertFailsWith { + TsUnknownCallModelRegistry( + registrations = listOf(registration("duplicate"), registration("duplicate")), + ) + } + + assertEquals("Duplicate semantic model IDs: duplicate", error.message) + } + + @Test + fun `ambiguous matches report stable sorted IDs`() { + val registry = TsUnknownCallModelRegistry( + registrations = listOf(registration("z-model"), registration("a-model")), + ).freeze() + + val error = assertFailsWith { + registry.select(mockk()) + } + + assertEquals("Ambiguous semantic models matched: a-model, z-model", error.message) + } + + @Test + fun `unknown enabled IDs are rejected`() { + val registry = TsUnknownCallModelRegistry(listOf(registration("known"))) + + val error = assertFailsWith { + registry.freeze(enabledModelIds = setOf("missing")) + } + + assertEquals("Unknown semantic model IDs: missing", error.message) + } + + @Test + fun `selection and fingerprint do not depend on registration order`() { + val forward = listOf( + registration(id = "a", matches = false), + registration(id = "b", matches = true), + ) + val call = mockk() + + val first = TsUnknownCallModelRegistry(forward).freeze() + val second = TsUnknownCallModelRegistry(forward.reversed()).freeze() + + assertEquals("b", first.select(call)?.descriptor?.id) + assertEquals("b", second.select(call)?.descriptor?.id) + assertEquals(first.fingerprint, second.fingerprint) + } + + @Test + fun `frozen subset is detached and changes fingerprint`() { + val mutableIds = mutableSetOf("a") + val registry = TsUnknownCallModelRegistry( + listOf(registration("a"), registration("b")), + ) + + val onlyA = registry.freeze(enabledModelIds = mutableIds) + mutableIds += "b" + val both = registry.freeze() + + assertEquals(listOf("a"), onlyA.descriptors.map { it.id }) + assertNotEquals(onlyA.fingerprint, both.fingerprint) + assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) + } + + private fun registration( + id: String, + matches: Boolean = true, + ) = TsUnknownCallModelRegistration( + descriptor = descriptor(id = id, matches = matches), + implementation = FakeImplementation, + ) + + private fun descriptor( + id: String, + domainId: String = "test-domain", + domainDescription: String = "Test-only supported domain", + matches: Boolean = true, + ) = TsUnknownCallModelDescriptor( + id = id, + matcher = TsUnknownCallModelMatcher { matches }, + supportedDomain = TsUnknownCallModelSupportedDomain( + id = domainId, + description = domainDescription, + ), + precision = TsUnknownCallModelPrecision.EXACT, + implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, + ) + + private object FakeImplementation : TsUnknownCallModelImplementation { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC + } +} diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index c78d4027f..ee46e3e9f 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -18,6 +18,11 @@ declare class ExternalBoolean { static convert(value: boolean): boolean; } +declare class ExternalModeledCall { + static identity(value: ExternalReceiver): ExternalReceiver; + static fail(): number; +} + class KnownReceiver { known(): number { return 1; @@ -68,6 +73,17 @@ class CallFallbackBaseline { return ExternalBoolean.convert(value); } + modeledUnknownCallReturnsAlias(receiver: ExternalReceiver): number { + if (ExternalModeledCall.identity(receiver) === receiver) { + return 122; + } + return 0; + } + + modeledUnknownCallThrows(): number { + return ExternalModeledCall.fail(); + } + anyReceiverWithKnownMethodContinues(receiver: any): number { receiver.known(); return 102; diff --git a/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts new file mode 100644 index 000000000..418576799 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts @@ -0,0 +1,24 @@ +// noinspection JSUnusedGlobalSymbols + +class ArrayElement {} + +export class ArrayPopIntrinsic { + emptyArray(): number | undefined { + const values: number[] = []; + return values.pop(); + } + + nonEmptyArray(): number { + const values = [10, 20, 30]; + return values.pop()! + values.length; + } + + aliasedElement(): number { + const element = new ArrayElement(); + const values: ArrayElement[] = [element]; + if (values.pop() === element) { + return 42; + } + return 0; + } +} From 45ac16c1ae1189fb11c6c74e5d4f619b9ce84899 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 28 Aug 2026 23:58:36 +0300 Subject: [PATCH 2/5] [TS] Document fake value representation invariants --- .../main/kotlin/org/usvm/machine/TsContext.kt | 22 +++++++++++++++++++ .../org/usvm/machine/types/EtsFakeType.kt | 16 ++++++++++++++ .../org/usvm/machine/types/FakeExprUtil.kt | 15 +++++++++++++ 3 files changed, 53 insertions(+) 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 9ae27cb06..52a9f0a9d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -183,6 +183,12 @@ class TsContext( fun UConcreteHeapRef.getFakeType(scope: TsStepScope): EtsFakeType = scope.calcOnState { getFakeType(memory) } + /** + * Returns whether this expression is the storage identity of a synthetic fake-value wrapper. + * + * A positive result says nothing about the wrapper's active runtime kind. In particular, the expression must not + * be used as the represented object reference; inspect [EtsFakeType.refTypeExpr] and extract the reference payload. + */ @OptIn(ExperimentalContracts::class) fun UExpr<*>.isFakeObject(): Boolean { contract { @@ -238,6 +244,12 @@ class TsContext( } } + /** + * Returns the reference payload of a fake-value wrapper without adding a reference-kind constraint. + * + * Use this only when [EtsFakeType.refTypeExpr] is already known or the caller guards the result equivalently. + * Otherwise use [unwrapRefWithPathConstraint]. + */ fun UHeapRef.unwrapRef(scope: TsStepScope): UHeapRef { if (isFakeObject()) { return extractRef(scope) @@ -245,6 +257,9 @@ class TsContext( return this } + /** + * Extracts the reference payload from a fake-value wrapper and constrains that wrapper to the reference kind. + */ fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef { if (isFakeObject()) { scope.assert(getFakeType(scope).refTypeExpr) @@ -285,6 +300,12 @@ class TsContext( return memory.read(lValue) } + /** + * Reads the reference payload without constraining [EtsFakeType.refTypeExpr]. + * + * This operation alone does not prove that the wrapped value is a reference. The caller must either assert the + * discriminator through a live [TsStepScope] or use the payload only under an equivalent guard. + */ fun UConcreteHeapRef.extractRef(memory: UReadOnlyMemory<*>): UHeapRef { check(isFakeObject()) val lValue = getIntermediateRefLValue(address) @@ -299,6 +320,7 @@ class TsContext( return scope.calcOnState { extractFp(memory) } } + /** Reads the reference payload through [scope] without adding a reference-kind constraint. */ fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef { return scope.calcOnState { extractRef(memory) } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt index 151b5d911..a4b7c4e88 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt @@ -6,6 +6,22 @@ import org.usvm.UExpr import org.usvm.USort import org.usvm.machine.TsContext +/** + * Type metadata for a synthetic wrapper representing a TypeScript value whose runtime kind is not known. + * + * The wrapper is identified by a special concrete heap reference, but that reference is only the wrapper's storage + * identity. It is not the object reference represented by the value. The possible boolean, number, and reference + * payloads are stored separately in the wrapper's intermediate fields. + * + * [boolTypeExpr], [fpTypeExpr], and [refTypeExpr] are symbolic discriminators. Exactly one of them must be true for + * every feasible state. Consumers should therefore keep the wrapper intact until the runtime kind is proven. In + * particular, using the reference payload requires constraining [refTypeExpr] and then extracting that payload; + * treating the wrapper reference itself as the payload or narrowing solely from a static TypeScript type is unsound. + * + * If narrowing establishes that the represented value is a particular object, the corresponding discriminator + * constraints must also be propagated to previously materialized fake values that may refer to the same object. + * Constraining only the extracted address breaks alias consistency. + */ class EtsFakeType( val boolTypeExpr: UBoolExpr, val fpTypeExpr: UBoolExpr, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt index 2dcd2bfb8..59fa51a6b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt @@ -15,6 +15,21 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.memory.ULValue +/** + * Creates a fresh synthetic wrapper for a TypeScript value with a not necessarily known runtime kind. + * + * Non-null arguments initialize the corresponding boolean, number, and reference payload fields. When exactly one + * payload is supplied, the wrapper is constrained to that runtime kind. When multiple payloads are supplied, all + * three kind discriminators remain symbolic and [EtsFakeType.mkExactlyOneTypeConstraint] selects exactly one active + * representation. Callers that model a completely unknown value should therefore supply all three payloads. + * + * The returned concrete heap reference identifies the wrapper, not its reference payload. Consumers must preserve + * the wrapper or explicitly constrain the appropriate discriminator before extracting a payload. + * + * [scope] may be `null` only while constructing the initial state, before solver models exist. During symbolic + * execution a live scope is required so that adding the exactly-one constraint also checks satisfiability and updates + * the state's models. + */ fun TsState.mkFakeValue( scope: TsStepScope?, // pass `null` only in the initial state, where `scope` is not available! boolValue: UBoolExpr? = null, From 25f2b985e435154a2bd9c90171f10dce4b50c10d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 01:58:41 +0300 Subject: [PATCH 3/5] [TS Calls] Harden guarded semantic model execution --- .../src/main/kotlin/org/usvm/api/TsMock.kt | 25 ++- .../main/kotlin/org/usvm/machine/TsMachine.kt | 1 + .../call/TsIntrinsicUnknownCallModels.kt | 5 +- .../usvm/machine/call/TsUnknownCallModel.kt | 3 +- .../call/TsUnknownCallModelRegistry.kt | 11 +- .../usvm/machine/call/TsUnknownCallProfile.kt | 99 ++++++++- .../usvm/machine/interpreter/TsInterpreter.kt | 5 + .../call/TsArrayPopIntrinsicModelTest.kt | 76 ++++++- .../call/TsUnknownCallDispatcherTest.kt | 52 +++++ ...UnknownCallExecutionGuardValidationTest.kt | 210 ++++++++++++++++++ .../call/TsUnknownCallModelRegistryTest.kt | 39 +++- .../baseline/CallFallbackBaseline.ts | 8 + .../resources/models/ArrayPopIntrinsic.ts | 51 +++++ 13 files changed, 562 insertions(+), 23 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 237e0f412..1ef5e5f59 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -16,30 +16,33 @@ fun mockMethodCall( method: EtsMethodSignature, resultType: EtsType = method.returnType, ) { + val result = makeFreshUnknownCallResult(scope = scope, resultType = resultType) + scope.doWithState { - mockMethodCall(method = method, resultType = resultType) + setMockMethodCallResult(method = method, result = result) } } -/** Creates a fresh opaque result directly on this state without applying callee effects or exceptions. */ -fun TsState.mockMethodCall( +/** Stores a prepared opaque result on this state without applying callee effects or exceptions. */ +internal fun TsState.setMockMethodCallResult( method: EtsMethodSignature, - resultType: EtsType = method.returnType, + result: UExpr<*>, ) { - val result = freshUnknownCallResult(resultType) methodResult = TsMethodResult.Success.MockedCall(result, method) } -private fun TsState.freshUnknownCallResult(resultType: EtsType): UExpr<*> { - if (resultType is EtsVoidType) { - return ctx.mkUndefinedValue() - } +/** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */ +internal fun makeFreshUnknownCallResult( + scope: TsStepScope, + resultType: EtsType, +): UExpr<*> = scope.calcOnState { + if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() - return when (val sort = ctx.typeToSort(resultType)) { + when (val sort = ctx.typeToSort(resultType)) { is UAddressSort -> makeSymbolicRefUntyped() is TsUnresolvedSort -> mkFakeValue( - scope = null, + scope = scope, boolValue = makeSymbolicPrimitive(ctx.boolSort), fpValue = makeSymbolicPrimitive(ctx.fp64Sort), refValue = makeSymbolicRefUntyped(), 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 f08a486a4..eca353f53 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -74,6 +74,7 @@ class TsMachine( options = tsOptions, observer = observer, unknownCallDispatcher = resolvedUnknownCallDispatcher, + throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) private val cfgStatistics = CfgStatisticsImpl(graph) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt index d2899c1a5..b0a9838e3 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt @@ -55,7 +55,7 @@ object TsBuiltInUnknownCallModels { }, supportedDomain = TsUnknownCallModelSupportedDomain( id = "native-array-pop", - description = "Resolved one-dimensional native arrays with no arguments and a resolved element sort", + description = "Resolved one-dimensional native arrays with no arguments and a primitive element sort", ), precision = TsUnknownCallModelPrecision.PARTIAL, implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, @@ -130,6 +130,9 @@ private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { ?: return null val elementSort = state.ctx.typeToSort(arrayType.elementType) + if (elementSort == state.ctx.addressSort) { + return null + } return ArrayPopInput( array = array, 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 f1aab3a9c..9566b54a0 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 @@ -74,7 +74,8 @@ class TsUnknownCallModelSuccessor( * A backend-neutral semantic-model execution plan. * * [residualGuard] denotes the unsupported part of a partial model's domain. Together, successor guards and the - * residual guard must partition the current call domain. + * residual guard must partition the current call domain. The dispatcher validates disjointness and coverage before + * applying any successor. */ class TsUnknownCallModelExecution( successors: List, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt index e80ed4cca..c30456c62 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -57,7 +57,7 @@ class TsUnknownCallModelRegistry( } } - /** Freezes an immutable enabled subset; `null` enables the complete registered catalog. */ + /** Freezes an immutable enabled subset and validates its backends; `null` enables the complete catalog. */ fun freeze(enabledModelIds: Set? = null): TsFrozenUnknownCallModelRegistry { val enabledIds = enabledModelIds?.toSet() val knownIds = registrations.mapTo(mutableSetOf()) { it.descriptor.id } @@ -71,6 +71,15 @@ class TsUnknownCallModelRegistry( null -> registrations else -> registrations.filter { it.descriptor.id in enabledIds } } + val missingBackendKinds = enabledRegistrations + .map { it.descriptor.implementationKind } + .distinct() + .filterNot(backends::containsKey) + .sortedBy { it.name } + + require(missingBackendKinds.isEmpty()) { + "Missing semantic model backends: ${missingBackendKinds.joinToString()}" + } return TsFrozenUnknownCallModelRegistry(enabledRegistrations, backends) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index 825cd8726..d24b6164c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -1,12 +1,21 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsType +import org.usvm.UBoolExpr +import org.usvm.api.makeFreshUnknownCallResult import org.usvm.api.mockMethodCall +import org.usvm.api.setMockMethodCallResult +import org.usvm.isTrue import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.state.newStmt +import org.usvm.solver.USatResult +import org.usvm.solver.USolverResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult /** The externally observable decision made for a call that could not be executed normally. */ enum class TsUnknownCallOutcome { @@ -141,8 +150,17 @@ class TsProfileUnknownCallDispatcher( call: TsUnknownCall, application: TsUnknownCallModelApplication.Applied, ): TsUnknownCallOutcome { + validateExecutionGuards(scope = scope, application = application) + val residualGuard = application.execution.residualGuard val residualPolicy = profile.residualPolicyFor(call) + val freshResidualResult = if ( + residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + ) { + makeFreshUnknownCallResult(scope = scope, resultType = call.resultType) + } else { + null + } val stoppedResidualIsSatisfiable = residualGuard != null && residualPolicy == TsResidualCallPolicy.STOP_PATH && scope.checkSat(residualGuard) != null @@ -169,7 +187,10 @@ class TsProfileUnknownCallDispatcher( if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { guardedStateChanges += residualGuard to { - mockMethodCall(method = call.callee, resultType = call.resultType) + setMockMethodCallResult( + method = call.callee, + result = requireNotNull(freshResidualResult), + ) newStmt(call.callSite) freshResidualApplied = true @@ -199,6 +220,65 @@ class TsProfileUnknownCallDispatcher( } } + private fun validateExecutionGuards( + scope: TsStepScope, + application: TsUnknownCallModelApplication.Applied, + ) = scope.doWithState { + val namedGuards = buildList { + application.execution.successors.forEachIndexed { index, successor -> + add(NamedGuard(name = "successor[$index]", guard = successor.guard)) + } + application.execution.residualGuard?.let { residualGuard -> + add(NamedGuard(name = "residual", guard = residualGuard)) + } + } + val overlaps = buildList { + namedGuards.forEachIndexed { firstIndex, first -> + namedGuards.drop(firstIndex + 1).forEach { second -> + add( + GuardOverlap( + firstName = first.name, + secondName = second.name, + condition = ctx.mkAnd(first.guard, second.guard), + ) + ) + } + } + } + val coveredDomain = ctx.mkOr(namedGuards.map(NamedGuard::guard)) + val uncoveredDomain = ctx.mkNot(coveredDomain) + val invalidity = ctx.mkOr(overlaps.map(GuardOverlap::condition) + uncoveredDomain) + val validationConstraints = pathConstraints.clone() + validationConstraints += invalidity + + val solverResult = ctx.solver().check(validationConstraints) + solverResult.requireConclusiveGuardValidation(modelId = application.modelId) + + when (solverResult) { + is UUnsatResult -> { + // The invalidity condition is unreachable, so the guards form a partition. + } + + is USatResult -> { + val witnessedOverlap = overlaps.firstOrNull { overlap -> + solverResult.model.eval(overlap.condition).isTrue + } + if (witnessedOverlap != null) { + error( + "Semantic model ${application.modelId} produced overlapping guards: " + + "${witnessedOverlap.firstName}, ${witnessedOverlap.secondName}" + ) + } + + error("Semantic model ${application.modelId} guards do not cover the current call domain") + } + + is UUnknownResult -> { + error("Unreachable after conclusive guard validation") + } + } + } + private fun modelStateChange( call: TsUnknownCall, application: TsUnknownCallModelApplication.Applied, @@ -258,3 +338,20 @@ class TsProfileUnknownCallDispatcher( decision = decision, ) } + +internal fun USolverResult<*>.requireConclusiveGuardValidation(modelId: String) { + check(this !is UUnknownResult) { + "Semantic model $modelId guards could not be validated: solver returned UNKNOWN" + } +} + +private data class NamedGuard( + val name: String, + val guard: UBoolExpr, +) + +private data class GuardOverlap( + val firstName: String, + val secondName: String, + val condition: UBoolExpr, +) 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 0bf9f180b..cc8e915f6 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 @@ -96,6 +96,7 @@ class TsInterpreter( private val options: TsOptions, private val observer: TsInterpreterObserver? = null, private val unknownCallDispatcher: TsUnknownCallDispatcher, + private val throwExceptionOnStepFailure: Boolean = false, ) : UInterpreter() { private val forkBlackList: UForkBlackList = UForkBlackList.createDefault() @@ -146,6 +147,10 @@ class TsInterpreter( } } } catch (e: Exception) { + if (throwExceptionOnStepFailure) { + throw e + } + logger.error { "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { " $it" }}" } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt index 279f0bfbf..67ab848ce 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt @@ -4,6 +4,7 @@ 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.junit.jupiter.api.Disabled import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy @@ -12,6 +13,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.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.util.TsTestResolver import org.usvm.util.getResourcePath import kotlin.test.Test @@ -47,12 +50,54 @@ class TsArrayPopIntrinsicModelTest { } @Test - fun `array pop preserves a returned reference alias`() { - val result = analyze(methodName = "aliasedElement") + fun `allocated reference array uses residual fallback`() { + assertUsesResidualFallback(methodName = "aliasedElement") + } - assertTrue(result.values.isNotEmpty(), "No final states; events=${result.events}") - assertEquals(42.0, assertIs(result.values.single()).number) - assertEquals(listOf("ts.array.pop"), result.modelIds) + @Test + fun `symbolic reference array uses residual fallback`() { + assertUsesResidualFallback(methodName = "symbolicReferenceArray") + } + + @Test + fun `symbolic primitive array remains in the supported domain`() { + val result = analyze(methodName = "symbolicNumberArray") + + assertTrue(result.values.isNotEmpty()) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `symbolic unknown array uses residual fallback`() { + assertUsesResidualFallback(methodName = "symbolicUnknownArray") + } + + @Test + fun `allocated reference array with symbolic write uses residual fallback`() { + val result = analyze(methodName = "allocatedReferenceArrayWithSymbolicWrite") + + val event = result.events.single() + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome) + assertIs(event.decision) + } + + @Test + fun `array pop with arguments uses residual fallback`() { + assertUsesResidualFallback(methodName = "popWithArguments") + } + + @Disabled("Tracked by https://github.com/UnitTestBot/usvm/issues/379") + @Test + fun `symbolic reference array pop preserves fake value representations`() { + val states = analyzeStates(methodName = "symbolicReferenceArrayPreservesFakeValue") + + assertTrue( + states.any { state -> + val result = (state.methodResult as? TsMethodResult.Success)?.value + result == state.ctx.mkFp(44.0, state.ctx.fp64Sort) + }, + "Expected the number representation to reach return 44", + ) } @Test @@ -115,6 +160,27 @@ class TsArrayPopIntrinsicModelTest { } } + private fun assertUsesResidualFallback(methodName: String) { + val result = analyze(methodName = methodName) + + assertTrue(result.values.isEmpty()) + val event = result.events.single() + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome) + assertIs(event.decision) + } + + 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 == "ArrayPopIntrinsic" } .methods diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index e06985687..1ed384901 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -25,6 +25,7 @@ import org.usvm.UExpr import org.usvm.UMachineOptions import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.isTrue import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -175,6 +176,27 @@ class TsUnknownCallDispatcherTest { } } + @Test + fun `fresh fallback keeps fake type constraints in state models`() { + val states = analyzeAllStates( + methodName = "freshUnknownCallResult", + profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + ) + + assertFreshResultModelSatisfiesFakeType(states.single()) + } + + @Test + fun `partial residual fallback keeps fake type constraints in state models`() { + val states = analyzeAllStates( + methodName = "freshUnknownCallResult", + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + modelProvider = UnsupportedPartialModelProvider, + ) + + assertFreshResultModelSatisfiesFakeType(states.single()) + } + @Test fun `partial model sends only residual domain to fresh fallback`() { val observer = RecordingUnknownCallObserver() @@ -611,6 +633,18 @@ class TsUnknownCallDispatcherTest { } } + private fun assertFreshResultModelSatisfiesFakeType(state: TsState) { + val result = assertIs(state.methodResult).value + val fakeValue = assertIs(result) + val exactlyOneType = state.ctx.run { + assertTrue(fakeValue.isFakeObject()) + fakeValue.getFakeType(state.memory).mkExactlyOneTypeConstraint(this) + } + + assertTrue(state.models.isNotEmpty()) + assertTrue(state.models.all { model -> model.eval(exactlyOneType).isTrue }) + } + private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher { val calls = mutableListOf() val receiverIsAssociatedFunction = mutableListOf() @@ -747,6 +781,24 @@ class TsUnknownCallDispatcherTest { } } + private object UnsupportedPartialModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.falseExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "unsupported-partial-model", + precision = TsUnknownCallModelPrecision.PARTIAL, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.trueExpr, + ), + ) + } + } + private object StatefulAliasModelProvider : TsUnknownCallModelProvider { override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { val argument = requireNotNull(call.arguments.single().resolved) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt new file mode 100644 index 000000000..a61370b4b --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt @@ -0,0 +1,210 @@ +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.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsState +import org.usvm.solver.UUnknownResult +import org.usvm.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.time.Duration + +class TsUnknownCallExecutionGuardValidationTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/baseline/CallFallbackBaseline.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `overlapping model successor guards are rejected`() { + assertInvalidModel( + methodName = "declaredMethodWithoutBodyContinues", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = OverlappingSuccessorsModelProvider, + expectedMessage = "Semantic model overlapping-successors produced overlapping guards: " + + "successor[0], successor[1]", + ) + } + + @Test + fun `overlapping model successor and residual guards are rejected`() { + assertInvalidModel( + methodName = "declaredMethodWithoutBodyContinues", + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + modelProvider = OverlappingResidualModelProvider, + expectedMessage = "Semantic model overlapping-residual produced overlapping guards: successor[0], residual", + ) + } + + @Test + fun `exact model successor guards must cover the current call domain`() { + assertInvalidModel( + methodName = "modeledUnknownCallForks", + profile = TsUnknownCallProfiles.MODELS_THEN_STOP, + modelProvider = IncompleteExactModelProvider, + expectedMessage = "Semantic model incomplete-exact guards do not cover the current call domain", + ) + } + + @Test + fun `partial model successor and residual guards must cover the current call domain`() { + assertInvalidModel( + methodName = "modeledUnknownCallForks", + profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, + modelProvider = IncompletePartialModelProvider, + expectedMessage = "Semantic model incomplete-partial guards do not cover the current call domain", + ) + } + + @Test + fun `unknown solver result cannot validate execution guards`() { + val exception = assertFailsWith { + UUnknownResult().requireConclusiveGuardValidation(modelId = "unknown-guards") + } + + assertEquals( + "Semantic model unknown-guards guards could not be validated: solver returned UNKNOWN", + exception.message, + ) + } + + private fun assertInvalidModel( + methodName: String, + profile: TsUnknownCallProfile, + modelProvider: TsUnknownCallModelProvider, + expectedMessage: String, + ) { + val exception = assertFailsWith { + analyzeAllStates( + methodName = methodName, + profile = profile, + modelProvider = modelProvider, + ) + } + + assertEquals(expectedMessage, exception.message) + } + + private fun analyzeAllStates( + methodName: String, + profile: TsUnknownCallProfile, + modelProvider: TsUnknownCallModelProvider, + ): List { + val method = method(methodName) + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallProfile = profile), + unknownCallModelProvider = modelProvider, + ).use { machine -> + machine.analyze(listOf(method)) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "CallFallbackBaseline" } + .methods + .single { it.name == name } + + private object OverlappingSuccessorsModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() } + + return TsUnknownCallModelApplication.Applied( + modelId = "overlapping-successors", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor(guard = state.ctx.trueExpr, completion = completion), + TsUnknownCallModelSuccessor(guard = state.ctx.trueExpr, completion = completion), + ), + residualGuard = null, + ), + ) + } + } + + private object OverlappingResidualModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "overlapping-residual", + precision = TsUnknownCallModelPrecision.PARTIAL, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.trueExpr, + ), + ) + } + } + + private object IncompleteExactModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val condition = requireNotNull(call.arguments.single().resolved).asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "incomplete-exact", + precision = TsUnknownCallModelPrecision.EXACT, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = null, + ), + ) + } + } + + private object IncompletePartialModelProvider : TsUnknownCallModelProvider { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val condition = requireNotNull(call.arguments.single().resolved).asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelApplication.Applied( + modelId = "incomplete-partial", + precision = TsUnknownCallModelPrecision.PARTIAL, + execution = TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.falseExpr, + ), + ) + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + stopOnCoverage = 0, + stopOnTargetsReached = false, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt index 6cc5be150..6684cce0f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call import io.mockk.mockk +import org.usvm.machine.state.TsState import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -36,6 +37,7 @@ class TsUnknownCallModelRegistryTest { fun `ambiguous matches report stable sorted IDs`() { val registry = TsUnknownCallModelRegistry( registrations = listOf(registration("z-model"), registration("a-model")), + backends = listOf(FakeBackend), ).freeze() val error = assertFailsWith { @@ -56,6 +58,19 @@ class TsUnknownCallModelRegistryTest { assertEquals("Unknown semantic model IDs: missing", error.message) } + @Test + fun `enabled implementation kinds require configured backends`() { + val registry = TsUnknownCallModelRegistry( + registrations = listOf(registration("model-without-backend")), + ) + + val error = assertFailsWith { + registry.freeze() + } + + assertEquals("Missing semantic model backends: INTRINSIC", error.message) + } + @Test fun `selection and fingerprint do not depend on registration order`() { val forward = listOf( @@ -64,8 +79,14 @@ class TsUnknownCallModelRegistryTest { ) val call = mockk() - val first = TsUnknownCallModelRegistry(forward).freeze() - val second = TsUnknownCallModelRegistry(forward.reversed()).freeze() + val first = TsUnknownCallModelRegistry( + registrations = forward, + backends = listOf(FakeBackend), + ).freeze() + val second = TsUnknownCallModelRegistry( + registrations = forward.reversed(), + backends = listOf(FakeBackend), + ).freeze() assertEquals("b", first.select(call)?.descriptor?.id) assertEquals("b", second.select(call)?.descriptor?.id) @@ -76,7 +97,8 @@ class TsUnknownCallModelRegistryTest { fun `frozen subset is detached and changes fingerprint`() { val mutableIds = mutableSetOf("a") val registry = TsUnknownCallModelRegistry( - listOf(registration("a"), registration("b")), + registrations = listOf(registration("a"), registration("b")), + backends = listOf(FakeBackend), ) val onlyA = registry.freeze(enabledModelIds = mutableIds) @@ -116,4 +138,15 @@ class TsUnknownCallModelRegistryTest { override val kind: TsUnknownCallModelImplementationKind = TsUnknownCallModelImplementationKind.INTRINSIC } + + private object FakeBackend : TsUnknownCallModelBackend { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC + + override fun execute( + implementation: TsUnknownCallModelImplementation, + state: TsState, + call: TsUnknownCall, + ): TsUnknownCallModelExecution = error("Fake backend must not execute in registry metadata tests") + } } diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index ee46e3e9f..7b80de0eb 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -18,6 +18,10 @@ declare class ExternalBoolean { static convert(value: boolean): boolean; } +declare class ExternalAny { + static value(): any; +} + declare class ExternalModeledCall { static identity(value: ExternalReceiver): ExternalReceiver; static fail(): number; @@ -84,6 +88,10 @@ class CallFallbackBaseline { return ExternalModeledCall.fail(); } + freshUnknownCallResult(): any { + return ExternalAny.value(); + } + anyReceiverWithKnownMethodContinues(receiver: any): number { receiver.known(); return 102; diff --git a/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts index 418576799..0258b3974 100644 --- a/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts +++ b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts @@ -1,3 +1,4 @@ +// @ts-nocheck // noinspection JSUnusedGlobalSymbols class ArrayElement {} @@ -21,4 +22,54 @@ export class ArrayPopIntrinsic { } return 0; } + + symbolicReferenceArray(values: ArrayElement[]): number { + values.pop(); + return 45; + } + + symbolicNumberArray(values: number[]): number { + values.pop(); + return 46; + } + + symbolicUnknownArray(values: any[]): number { + values.pop(); + return 47; + } + + allocatedReferenceArrayWithSymbolicWrite(index: number, value: any): number { + if (index !== 1) { + return 0; + } + + const values: ArrayElement[] = [new ArrayElement(), new ArrayElement()]; + values[index] = value; + const popped: any = values.pop(); + if (typeof popped === "number") { + return 45; + } + + return 0; + } + + popWithArguments(): number { + const values = [1]; + values.pop(0); + return 48; + } + + symbolicReferenceArrayPreservesFakeValue(values: ArrayElement[], value: any): number { + if (values.length !== 1) { + return 0; + } + + values[0] = value; + const popped: any = values.pop(); + if (typeof popped === "number") { + return 44; + } + + return 0; + } } From 176f1887d4ef46899ebbf38a7e449c3852628112 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 19:25:29 +0300 Subject: [PATCH 4/5] [TS Calls] Remove redundant named arguments --- .../src/main/kotlin/org/usvm/api/TsMock.kt | 6 +-- .../call/TsIntrinsicUnknownCallModels.kt | 10 ++-- .../org/usvm/machine/call/TsUnknownCall.kt | 18 +++---- .../call/TsUnknownCallModelRegistry.kt | 6 +-- .../usvm/machine/call/TsUnknownCallProfile.kt | 51 ++++++++----------- .../usvm/machine/expr/CallApproximations.kt | 13 ++--- .../call/TsArrayPopIntrinsicModelTest.kt | 4 +- ...UnknownCallExecutionGuardValidationTest.kt | 8 +-- .../call/TsUnknownCallModelRegistryTest.kt | 2 +- 9 files changed, 47 insertions(+), 71 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt index 1ef5e5f59..7ab3d97d9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -16,10 +16,10 @@ fun mockMethodCall( method: EtsMethodSignature, resultType: EtsType = method.returnType, ) { - val result = makeFreshUnknownCallResult(scope = scope, resultType = resultType) + val result = makeFreshUnknownCallResult(scope, resultType) scope.doWithState { - setMockMethodCallResult(method = method, result = result) + setMockMethodCallResult(method, result) } } @@ -42,7 +42,7 @@ internal fun makeFreshUnknownCallResult( is UAddressSort -> makeSymbolicRefUntyped() is TsUnresolvedSort -> mkFakeValue( - scope = scope, + scope, boolValue = makeSymbolicPrimitive(ctx.boolSort), fpValue = makeSymbolicPrimitive(ctx.fp64Sort), refValue = makeSymbolicRefUntyped(), diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt index b0a9838e3..8e52fa342 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt @@ -39,7 +39,7 @@ object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}" } - return intrinsic.model.execute(state = state, call = call) + return intrinsic.model.execute(state, call) } } @@ -74,7 +74,7 @@ object TsBuiltInUnknownCallModels { private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { override fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { - val input = resolveInput(state = state, call = call) + val input = resolveInput(state, call) ?: return unsupportedExecution(state) val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType) @@ -134,11 +134,7 @@ private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { return null } - return ArrayPopInput( - array = array, - arrayType = arrayType, - elementSort = elementSort, - ) + return ArrayPopInput(array, arrayType, elementSort) } private fun unsupportedExecution(state: TsState): TsUnknownCallModelExecution { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index 1497688f8..238667afd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt @@ -160,10 +160,10 @@ internal fun TsUnknownCallDispatcher.dispatch( failureReason: TsUnknownCallFailureReason, resolvedReceiver: UExpr<*>, ) = dispatch( - scope = scope, - call = call.call, - callSite = call.returnSite, - failureReason = failureReason, + scope, + call.call, + call.returnSite, + failureReason, resolvedReceiver = resolvedReceiver, resolvedArguments = call.args, ) @@ -174,11 +174,11 @@ internal fun TsUnknownCallDispatcher.dispatch( failureReason: TsUnknownCallFailureReason, callee: EtsMethodSignature, ) = dispatch( - scope = scope, - call = call.call, - callSite = call.returnSite, - failureReason = failureReason, - callee = callee, + scope, + call.call, + call.returnSite, + failureReason, + callee, resolvedReceiver = call.resolvedReceiver, resolvedArguments = call.args.takeLast(call.call.args.size), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt index c30456c62..45471e1e8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -132,11 +132,7 @@ class TsFrozenUnknownCallModelRegistry internal constructor( val backend = checkNotNull(backends[implementationKind]) { "No semantic model backend configured for $implementationKind" } - val execution = backend.execute( - implementation = registration.implementation, - state = state, - call = call, - ) + val execution = backend.execute(registration.implementation, state, call) return TsUnknownCallModelApplication.Applied( modelId = registration.descriptor.id, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index d24b6164c..1c763c6a1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt @@ -87,25 +87,21 @@ class TsProfileUnknownCallDispatcher( override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { if (profile.modelLookup == TsUnknownCallModelLookup.DISABLED) { return applyResidualFallback( - scope = scope, - call = call, + scope, + call, reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, ) } val application = scope.calcOnState { - modelProvider.apply(state = this, call = call) + modelProvider.apply(this, call) } return when (application) { - is TsUnknownCallModelApplication.Applied -> applyModel( - scope = scope, - call = call, - application = application, - ) + is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) TsUnknownCallModelApplication.NotApplicable -> applyResidualFallback( - scope = scope, - call = call, + scope, + call, reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, ) } @@ -122,11 +118,11 @@ class TsProfileUnknownCallDispatcher( TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN } val event = event( - call = call, - outcome = outcome, + call, + outcome, decision = TsUnknownCallDecision.ResidualFallback( - policy = residualPolicy, - reason = reason, + residualPolicy, + reason, ), ) when (residualPolicy) { @@ -150,14 +146,14 @@ class TsProfileUnknownCallDispatcher( call: TsUnknownCall, application: TsUnknownCallModelApplication.Applied, ): TsUnknownCallOutcome { - validateExecutionGuards(scope = scope, application = application) + validateExecutionGuards(scope, application) val residualGuard = application.execution.residualGuard val residualPolicy = profile.residualPolicyFor(call) val freshResidualResult = if ( residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { - makeFreshUnknownCallResult(scope = scope, resultType = call.resultType) + makeFreshUnknownCallResult(scope, call.resultType) } else { null } @@ -170,9 +166,9 @@ class TsProfileUnknownCallDispatcher( var freshResidualApplied = false val guardedStateChanges = application.execution.successors.map { successor -> successor.guard to modelStateChange( - call = call, - application = application, - successor = successor, + call, + application, + successor, onApplied = { modelApplied = true if (modelEventReported) { @@ -187,15 +183,12 @@ class TsProfileUnknownCallDispatcher( if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { guardedStateChanges += residualGuard to { - setMockMethodCallResult( - method = call.callee, - result = requireNotNull(freshResidualResult), - ) + setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) newStmt(call.callSite) freshResidualApplied = true val event = residualEvent( - call = call, + call, policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ) observer?.onUnknownCallSafely(event) @@ -206,7 +199,7 @@ class TsProfileUnknownCallDispatcher( if (stoppedResidualIsSatisfiable) { val event = residualEvent( - call = call, + call, policy = TsResidualCallPolicy.STOP_PATH, ) observer?.onUnknownCallSafely(event) @@ -252,7 +245,7 @@ class TsProfileUnknownCallDispatcher( validationConstraints += invalidity val solverResult = ctx.solver().check(validationConstraints) - solverResult.requireConclusiveGuardValidation(modelId = application.modelId) + solverResult.requireConclusiveGuardValidation(application.modelId) when (solverResult) { is UUnsatResult -> { @@ -302,7 +295,7 @@ class TsProfileUnknownCallDispatcher( if (onApplied()) { val event = event( - call = call, + call, outcome = TsUnknownCallOutcome.MODEL_APPLIED, decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId), ) @@ -314,13 +307,13 @@ class TsProfileUnknownCallDispatcher( call: TsUnknownCall, policy: TsResidualCallPolicy, ) = event( - call = call, + call, outcome = when (policy) { TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN }, decision = TsUnknownCallDecision.ResidualFallback( - policy = policy, + policy, reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, ), ) 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 9aa5a437c..8e7c845eb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -111,12 +111,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return handleArrayPopCall( - expr = expr, - instanceType = instanceType, - elementSort = elementSort, - resolvedReceiver = instance, - ) + return handleArrayPopCall(expr, instanceType, elementSort, instance) } // Handle `Array.fill() method calls @@ -180,9 +175,9 @@ private fun TsExprResolver.handleArrayPopCall( } dispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, + scope, + expr, + scope.calcOnState { lastStmt }, failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, resolvedReceiver = resolvedReceiver, ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt index 67ab848ce..ea1dd94d4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt @@ -103,7 +103,7 @@ class TsArrayPopIntrinsicModelTest { @Test fun `disabled model sends pop to configured residual fallback`() { val enabledModelIds = mutableSetOf("ts.array.pop") - val selection = TsUnknownCallModelSelection(enabledModelIds = enabledModelIds) + val selection = TsUnknownCallModelSelection(enabledModelIds) enabledModelIds.clear() val result = analyze( methodName = "nonEmptyArray", @@ -161,7 +161,7 @@ class TsArrayPopIntrinsicModelTest { } private fun assertUsesResidualFallback(methodName: String) { - val result = analyze(methodName = methodName) + val result = analyze(methodName) assertTrue(result.values.isEmpty()) val event = result.events.single() diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt index a61370b4b..f27312644 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt @@ -70,7 +70,7 @@ class TsUnknownCallExecutionGuardValidationTest { @Test fun `unknown solver result cannot validate execution guards`() { val exception = assertFailsWith { - UUnknownResult().requireConclusiveGuardValidation(modelId = "unknown-guards") + UUnknownResult().requireConclusiveGuardValidation("unknown-guards") } assertEquals( @@ -86,11 +86,7 @@ class TsUnknownCallExecutionGuardValidationTest { expectedMessage: String, ) { val exception = assertFailsWith { - analyzeAllStates( - methodName = methodName, - profile = profile, - modelProvider = modelProvider, - ) + analyzeAllStates(methodName, profile, modelProvider) } assertEquals(expectedMessage, exception.message) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt index 6684cce0f..f45624784 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -114,7 +114,7 @@ class TsUnknownCallModelRegistryTest { id: String, matches: Boolean = true, ) = TsUnknownCallModelRegistration( - descriptor = descriptor(id = id, matches = matches), + descriptor = descriptor(id, matches = matches), implementation = FakeImplementation, ) From c996c99677b68add46739562363de42a8d9d46fa Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 31 Aug 2026 12:19:24 +0300 Subject: [PATCH 5/5] [TS Calls] Separate intrinsic model implementations --- .../call/TsBuiltInUnknownCallModels.kt | 14 ++++ .../TsArrayPopIntrinsicModel.kt} | 67 ++++++------------- .../intrinsic/TsIntrinsicUnknownCallModel.kt | 39 +++++++++++ .../TsIntrinsicUnknownCallModelTest.kt | 20 ++++++ 4 files changed, 93 insertions(+), 47 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt rename usvm-ts/src/main/kotlin/org/usvm/machine/call/{TsIntrinsicUnknownCallModels.kt => intrinsic/TsArrayPopIntrinsicModel.kt} (66%) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt new file mode 100644 index 000000000..31fe6a3fc --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt @@ -0,0 +1,14 @@ +package org.usvm.machine.call + +import org.usvm.machine.call.intrinsic.TsArrayPopIntrinsicModel +import org.usvm.machine.call.intrinsic.TsIntrinsicUnknownCallModelBackend + +/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */ +object TsBuiltInUnknownCallModels { + const val ARRAY_POP_MODEL_ID: String = TsArrayPopIntrinsicModel.MODEL_ID + + val registry = TsUnknownCallModelRegistry( + registrations = listOf(TsArrayPopIntrinsicModel.registration), + backends = listOf(TsIntrinsicUnknownCallModelBackend), + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt similarity index 66% rename from usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt rename to usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt index 8e52fa342..e82be0e6b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsIntrinsicUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt @@ -1,4 +1,4 @@ -package org.usvm.machine.call +package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType @@ -6,49 +6,29 @@ import org.usvm.UAddressSort import org.usvm.UExpr import org.usvm.USort import org.usvm.api.typeStreamOf +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelDescriptor +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelImplementationKind +import org.usvm.machine.call.TsUnknownCallModelMatcher +import org.usvm.machine.call.TsUnknownCallModelPrecision +import org.usvm.machine.call.TsUnknownCallModelRegistration +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallModelSupportedDomain import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.state.TsState import org.usvm.types.firstOrNull import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue -/** Builds constraint-level execution plans directly from a TypeScript symbolic state. */ -fun interface TsIntrinsicUnknownCallModel { - fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution -} - -/** Opaque registry handle for a Kotlin intrinsic semantic model. */ -class TsIntrinsicUnknownCallModelImplementation( - val model: TsIntrinsicUnknownCallModel, -) : TsUnknownCallModelImplementation { - override val kind: TsUnknownCallModelImplementationKind = - TsUnknownCallModelImplementationKind.INTRINSIC -} +/** Partial intrinsic model for `Array.pop` on resolved one-dimensional primitive arrays. */ +internal object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { + const val MODEL_ID: String = "ts.array.pop" -/** Executes intrinsic model handles without exposing them to the common registry or dispatcher contract. */ -object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { - override val kind: TsUnknownCallModelImplementationKind = - TsUnknownCallModelImplementationKind.INTRINSIC - - override fun execute( - implementation: TsUnknownCallModelImplementation, - state: TsState, - call: TsUnknownCall, - ): TsUnknownCallModelExecution { - val intrinsic = requireNotNull(implementation as? TsIntrinsicUnknownCallModelImplementation) { - "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}" - } - - return intrinsic.model.execute(state, call) - } -} - -/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */ -object TsBuiltInUnknownCallModels { - const val ARRAY_POP_MODEL_ID: String = "ts.array.pop" - - private val arrayPopDescriptor = TsUnknownCallModelDescriptor( - id = ARRAY_POP_MODEL_ID, + private val descriptor = TsUnknownCallModelDescriptor( + id = MODEL_ID, matcher = TsUnknownCallModelMatcher { call -> call.failureReason == TsUnknownCallFailureReason.PARTIAL_APPROXIMATION && call.callee.name == "pop" @@ -61,18 +41,11 @@ object TsBuiltInUnknownCallModels { implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, ) - val registry = TsUnknownCallModelRegistry( - registrations = listOf( - TsUnknownCallModelRegistration( - descriptor = arrayPopDescriptor, - implementation = TsIntrinsicUnknownCallModelImplementation(TsArrayPopIntrinsicModel), - ), - ), - backends = listOf(TsIntrinsicUnknownCallModelBackend), + val registration = TsUnknownCallModelRegistration( + descriptor = descriptor, + implementation = TsIntrinsicUnknownCallModelImplementation(this), ) -} -private object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { override fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val input = resolveInput(state, call) ?: return unsupportedExecution(state) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt new file mode 100644 index 000000000..0870cb410 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt @@ -0,0 +1,39 @@ +package org.usvm.machine.call.intrinsic + +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallModelBackend +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelImplementation +import org.usvm.machine.call.TsUnknownCallModelImplementationKind +import org.usvm.machine.state.TsState + +/** Builds constraint-level execution plans directly from a TypeScript symbolic state. */ +fun interface TsIntrinsicUnknownCallModel { + fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution +} + +/** Opaque registry handle for a Kotlin intrinsic semantic model. */ +class TsIntrinsicUnknownCallModelImplementation( + val model: TsIntrinsicUnknownCallModel, +) : TsUnknownCallModelImplementation { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC +} + +/** Executes intrinsic model handles without exposing them to the common registry or dispatcher contract. */ +object TsIntrinsicUnknownCallModelBackend : TsUnknownCallModelBackend { + override val kind: TsUnknownCallModelImplementationKind = + TsUnknownCallModelImplementationKind.INTRINSIC + + override fun execute( + implementation: TsUnknownCallModelImplementation, + state: TsState, + call: TsUnknownCall, + ): TsUnknownCallModelExecution { + val intrinsic = requireNotNull(implementation as? TsIntrinsicUnknownCallModelImplementation) { + "INTRINSIC backend requires TsIntrinsicUnknownCallModelImplementation, got ${implementation::class}" + } + + return intrinsic.model.execute(state, call) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt new file mode 100644 index 000000000..30ce632c5 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt @@ -0,0 +1,20 @@ +package org.usvm.machine.call.intrinsic + +import org.usvm.machine.call.TsUnknownCallModelImplementationKind +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs + +class TsIntrinsicUnknownCallModelTest { + @Test + fun `array pop registration binds the intrinsic backend`() { + val registration = TsArrayPopIntrinsicModel.registration + + assertEquals(expected = "ts.array.pop", actual = registration.descriptor.id) + assertEquals( + expected = TsUnknownCallModelImplementationKind.INTRINSIC, + actual = registration.descriptor.implementationKind, + ) + assertIs(registration.implementation) + } +}