From bd53dade20d90c55de4ba278dea8f6beff717177 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 28 Aug 2026 23:13:46 +0300 Subject: [PATCH 1/8] [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 7fb29a74d39b75a20ef3196e45cce6b25151c1de Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 28 Aug 2026 23:58:36 +0300 Subject: [PATCH 2/8] [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 67ed3251337ab5190f04b5d8c95bd17cd6858e94 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 01:58:41 +0300 Subject: [PATCH 3/8] [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 160e43eaf88a51c7e8e29a520bdf6cd82c2e05b3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 29 Aug 2026 19:25:29 +0300 Subject: [PATCH 4/8] [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 fad3d155bac070f5c37215f479285a4e9f012681 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 31 Aug 2026 12:19:24 +0300 Subject: [PATCH 5/8] [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) + } +} From 34597f57ef03429c9ff190fc2d8e90740f19f3b8 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 7 Sep 2026 22:14:09 +0300 Subject: [PATCH 6/8] [TS Calls] Simplify guarded semantic models --- usvm-ts/UNKNOWN_CALL_MODELS.md | 237 ++++++++++ .../main/kotlin/org/usvm/machine/TsContext.kt | 10 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 35 +- .../main/kotlin/org/usvm/machine/TsOptions.kt | 11 +- .../call/TsBuiltInUnknownCallModels.kt | 13 +- .../org/usvm/machine/call/TsUnknownCall.kt | 2 +- .../usvm/machine/call/TsUnknownCallModel.kt | 100 ++--- .../machine/call/TsUnknownCallModelCatalog.kt | 92 ++++ .../call/TsUnknownCallModelDispatcher.kt | 175 ++++++++ .../call/TsUnknownCallModelRegistry.kt | 162 ------- .../machine/call/TsUnknownCallObservation.kt | 23 +- .../usvm/machine/call/TsUnknownCallProfile.kt | 350 --------------- .../intrinsic/TsArrayPopIntrinsicModel.kt | 130 ------ .../intrinsic/TsArrayShiftIntrinsicModel.kt | 108 +++++ .../intrinsic/TsIntrinsicUnknownCallModel.kt | 39 -- .../usvm/machine/expr/CallApproximations.kt | 12 +- ...t.kt => TsArrayShiftIntrinsicModelTest.kt} | 116 ++--- .../call/TsUnknownCallDispatcherTest.kt | 407 +++++++----------- ...UnknownCallExecutionGuardValidationTest.kt | 206 --------- .../call/TsUnknownCallModelCatalogTest.kt | 118 +++++ .../call/TsUnknownCallModelRegistryTest.kt | 152 ------- .../TsIntrinsicUnknownCallModelTest.kt | 20 - .../resources/models/ArrayPopIntrinsic.ts | 75 ---- .../resources/models/ArrayShiftIntrinsic.ts | 46 ++ 24 files changed, 1092 insertions(+), 1547 deletions(-) create mode 100644 usvm-ts/UNKNOWN_CALL_MODELS.md create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt delete mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt rename usvm-ts/src/test/kotlin/org/usvm/machine/call/{TsArrayPopIntrinsicModelTest.kt => TsArrayShiftIntrinsicModelTest.kt} (60%) delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt delete mode 100644 usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts create mode 100644 usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md new file mode 100644 index 000000000..578e3fe5b --- /dev/null +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -0,0 +1,237 @@ +# TypeScript unknown-call models + +This document describes the semantic-model path used when the normal TypeScript interpreter cannot execute a call. + +## Mental model + +There are only three stages: + +1. The regular interpreter and existing compatibility approximations try to execute the call. +2. If execution cannot continue, `TsUnknownCallModelCatalog` selects one enabled semantic model by its target. +3. If no model handles the call or a model leaves a residual state, the configured fallback is applied. + +```text +normal execution + | + | cannot execute + v +enabled model with matching target? -- no --> fallback + | + yes + v +model accepts these inputs? -------- no --> fallback + | + yes + v +model successors + optional residual ----> residual uses fallback +``` + +The catalog contains model objects directly. There are no implementation-kind values, backend registrations, or +separate descriptor and implementation IDs. + +## Configuration + +Unknown-call behavior is configured directly in `TsOptions`: + +```kotlin +TsOptions( + enabledUnknownCallModelIds = setOf("ts.array.shift"), + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, +) +``` + +### `enabledUnknownCallModelIds` + +This is the only model-selection setting. + +| Value | Meaning | +| --- | --- | +| `null` | Enable every built-in model. This is the default. | +| `emptySet()` | Disable every built-in model. | +| `setOf("id", ...)` | Enable exactly the listed built-in model IDs. | + +Unknown IDs are rejected when the machine creates its immutable per-run catalog. The input set is copied at that +point, so later mutations cannot change an active run. + +Use the model's `id`, for example `ts.array.shift`. A target method name, class name, source filename, or fingerprint is +not a model ID. + +The built-in catalog currently contains one model: + +| ID | Implementation | Accepted calls | +| --- | --- | --- | +| `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array whose element sort is known. | + +An `any`/unknown receiver, a fake-value wrapper, a non-array receiver, and an array whose element sort is unresolved do +not become applicable merely because the method is named `shift`; they use fallback. + +### `unknownCallFallback` + +The fallback is applied when: + +- no enabled model target matches the call; +- the selected model returns `null` because it cannot safely handle the concrete inputs; +- a model returns a satisfiable `residualGuard`. + +The available policies are: + +| Policy | Behavior | +| --- | --- | +| `STOP_PATH` | Prune the unsupported state. This is the default. | +| `FRESH_SYMBOLIC_RETURN` | Continue with a fresh symbolic result and ignore unknown side effects and exceptions. | + +`FRESH_SYMBOLIC_RETURN` is deliberately imprecise. Use it only when opaque continuation is preferable to pruning. + +### Per-family fallback overrides + +`unknownCallFallbackOverrides` changes the fallback for calls whose callee has a particular +`EtsClassSignature`: + +```kotlin +TsOptions( + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, + unknownCallFallbackOverrides = mapOf( + externalApiSignature to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), +) +``` + +An override applies both when no model accepts the call and to a residual state returned by a model. Prefer the global +fallback unless one call family has a concrete reason to differ. + +## Model identity and target + +Every model implements `TsUnknownCallModel`: + +```kotlin +interface TsUnknownCallModel { + val id: String + val target: TsUnknownCallTarget + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? +} +``` + +### Choosing an ID + +Use a stable semantic name: + +```text +..[.] +``` + +Examples: + +- `ts.array.shift` +- `ts.array.pop` +- `node.buffer.copy` + +The ID is used for configuration, observer events, and catalog fingerprints. Do not include: + +- an implementation mechanism such as `intrinsic`; +- a hash; +- a version number; +- a supported-domain label. + +Keep the same ID if an equivalent model is later reimplemented by another mechanism. + +### Choosing a target + +`TsUnknownCallTarget` matches stable call metadata declaratively: + +```kotlin +TsUnknownCallTarget( + methodName = "shift", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, +) +``` + +Only `methodName` is required. Add `enclosingClassName` or `failureReason` when the method name alone is too broad. +The catalog rejects overlapping enabled targets before execution, so catalog order is never a priority rule. + +The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in +`apply`. + +The built-in array target intentionally combines the method name with `PARTIAL_APPROXIMATION` instead of a class name. +That failure reason is emitted only after the regular approximation path has classified the receiver as an +`EtsArrayType`. Calls on `any`/unknown receivers reach another failure reason and cannot match this target. The model +still validates the resolved receiver and its element sort before changing memory. + +## Applicability and residual states + +There is no separate `EXACT` or `PARTIAL` flag. + +- `apply(...) == null` means the model rejects the complete call. The dispatcher uses fallback. +- `residualGuard == null` means the returned execution completely handles the accepted state. +- A non-null `residualGuard` sends precisely that symbolic subdomain to fallback. + +For example, a model may handle an array receiver under `isArray` and leave `!isArray` as residual: + +```kotlin +TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = isArray, + completion = completion, + ), + ), + residualGuard = ctx.mkNot(isArray), +) +``` + +Model authors are responsible for making successor guards and the residual guard disjoint and exhaustive. This +property belongs in focused model tests; the dispatcher does not invoke the solver a second time merely to validate a +model on every call. + +## When to write an intrinsic + +An intrinsic directly builds guarded successors and symbolic-memory operations in Kotlin. Use it only for an operation +that TypeScript cannot express without losing symbolic efficiency or correctness. + +`Array.shift` is the built-in example because shifting a symbolic array is naturally represented by one +`memory.memcpy` operation. + +Good intrinsic candidates include: + +- bulk symbolic-memory copy or fill; +- symbolic collection primitives; +- solver operations unavailable in the modeled language; +- type-system operations that cannot be represented faithfully by ordinary code. + +Do not write an intrinsic merely because a library method is stateful. + +## Dynamic receivers + +A method name does not prove the receiver type. In particular, `value.shift()` may call a user-defined property rather +than `Array.prototype.shift`. + +Use this decision rule: + +| Receiver knowledge | Action | +| --- | --- | +| Definitely the modeled built-in receiver type | Apply the model. | +| Definitely another type | Return `null`; use fallback. | +| Possibly the modeled type, with a trustworthy built-in target | Use a type guard and residual complement. | +| `any`/unknown without proof of the built-in target | Return `null`; use fallback. | + +Never choose `typeStreamOf(receiver).firstOrNull()` as proof. It returns one possible type, not necessarily the only +possible type. Use a statically proven type, `singleOrNull()` where uniqueness is guaranteed, or an explicit symbolic +type guard. + +## Fingerprints + +The catalog sorts enabled models by ID and hashes their length-prefixed IDs. Therefore model registration order does +not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries. + +The fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a +manually maintained configuration value. + +## Observation + +Every applied model or fallback produces `TsUnknownCallEvent` through `TsInterpreterObserver.onUnknownCall`. + +- `ModelApplied(modelId)` identifies the semantic model. +- `ResidualFallback(policy)` records the effective fallback. +- `event.outcome` is derived from the decision and is not stored as a second independent value. + +Observer failures are logged and cannot alter symbolic exploration. 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 52a9f0a9d..0248715fa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -9,8 +9,8 @@ import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType -import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsLexicalEnvType +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType @@ -34,6 +34,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.allocateStaticRef @@ -198,6 +199,13 @@ class TsContext( return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET } + /** Returns whether this expression contains a fake-value wrapper as itself or as a conditional branch. */ + fun UExpr<*>.containsFakeObject(): Boolean = when { + isFakeObject() -> true + this is UIteExpr<*> -> trueBranch.containsFakeObject() || falseBranch.containsFakeObject() + else -> false + } + fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef { if (isFakeObject()) { return this diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index eca353f53..edc5c5b5e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -10,10 +10,9 @@ 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.TsModelUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher -import org.usvm.machine.call.TsUnknownCallModelProvider +import org.usvm.machine.call.TsUnknownCallModelCatalog import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -46,26 +45,26 @@ class TsMachine( private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, - unknownCallModelProvider: TsUnknownCallModelProvider? = null, + unknownCallModels: TsUnknownCallModelCatalog? = 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) + private val resolvedUnknownCallModels = when { + unknownCallDispatcher != null -> null + unknownCallModels != null -> unknownCallModels + else -> TsBuiltInUnknownCallModels.catalog(tsOptions.enabledUnknownCallModelIds) } - /** Fingerprint of the frozen built-in catalog, or `null` when custom dispatch/model wiring is used. */ + /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */ val unknownCallModelCatalogFingerprint: String? - get() = frozenUnknownCallModels?.fingerprint + get() = resolvedUnknownCallModels?.fingerprint - private val resolvedUnknownCallModelProvider = - unknownCallModelProvider ?: frozenUnknownCallModels ?: TsNoUnknownCallModels - private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( - profile = tsOptions.unknownCallProfile, - modelProvider = resolvedUnknownCallModelProvider, + 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 resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( + models = requireNotNull(resolvedUnknownCallModels), + fallback = tsOptions.unknownCallFallback, + fallbackOverrides = tsOptions.unknownCallFallbackOverrides, 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 6b22c8831..fedf989c0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,13 +1,14 @@ package org.usvm.machine -import org.usvm.machine.call.TsUnknownCallModelSelection -import org.usvm.machine.call.TsUnknownCallProfile -import org.usvm.machine.call.TsUnknownCallProfiles +import org.jacodb.ets.model.EtsClassSignature +import org.usvm.machine.call.TsResidualCallPolicy data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, - val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP, - val unknownCallModels: TsUnknownCallModelSelection = TsUnknownCallModelSelection(), + /** `null` enables every built-in model; an empty set disables all models. */ + val enabledUnknownCallModelIds: Set? = null, + val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, + val unknownCallFallbackOverrides: Map = emptyMap(), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt index 31fe6a3fc..51fd7c34e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt @@ -1,14 +1,13 @@ package org.usvm.machine.call -import org.usvm.machine.call.intrinsic.TsArrayPopIntrinsicModel -import org.usvm.machine.call.intrinsic.TsIntrinsicUnknownCallModelBackend +import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel -/** The intentionally small built-in catalog enabled by default for profile-based unknown-call dispatch. */ +/** The intentionally small built-in semantic-model catalog. */ object TsBuiltInUnknownCallModels { - const val ARRAY_POP_MODEL_ID: String = TsArrayPopIntrinsicModel.MODEL_ID + const val ARRAY_SHIFT_MODEL_ID: String = TsArrayShiftIntrinsicModel.MODEL_ID - val registry = TsUnknownCallModelRegistry( - registrations = listOf(TsArrayPopIntrinsicModel.registration), - backends = listOf(TsIntrinsicUnknownCallModelBackend), + fun catalog(enabledModelIds: Set? = null) = TsUnknownCallModelCatalog( + models = listOf(TsArrayShiftIntrinsicModel), + enabledModelIds = enabledModelIds, ) } 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 238667afd..48bffe05a 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 @@ -68,7 +68,7 @@ fun interface TsUnknownCallDispatcher { fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome } -/** Marks profile dispatchers that replace migrated compatibility approximations with registered models. */ +/** Marks dispatchers that replace migrated compatibility approximations with semantic models. */ interface TsUnknownCallModelDispatcher : TsUnknownCallDispatcher /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */ diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt index 9566b54a0..923236737 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 @@ -5,46 +5,49 @@ 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, +/** Declaratively identifies the calls handled by one semantic model. */ +data class TsUnknownCallTarget( + val methodName: String, + val enclosingClassName: String? = null, + val failureReason: TsUnknownCallFailureReason? = null, ) { 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" } + require(methodName.isNotBlank()) { "Semantic model target method name must not be blank" } + require(enclosingClassName == null || enclosingClassName.isNotBlank()) { + "Semantic model target class name 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 -} + internal fun matches(call: TsUnknownCall): Boolean = + call.callee.name == methodName && + (enclosingClassName == null || call.callee.enclosingClass.name == enclosingClassName) && + (failureReason == null || call.failureReason == failureReason) -/** 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" } + internal fun overlaps(other: TsUnknownCallTarget): Boolean { + val classNamesOverlap = enclosingClassName == null || + other.enclosingClassName == null || + enclosingClassName == other.enclosingClassName + val failureReasonsOverlap = failureReason == null || + other.failureReason == null || + failureReason == other.failureReason + + return methodName == other.methodName && classNamesOverlap && failureReasonsOverlap } } +/** + * A semantic model selected by a stable [id] and a declarative [target]. + * + * Returning `null` from [apply] means that the call is outside the model's supported input domain. The dispatcher + * then applies the configured fallback. A non-null execution may additionally contain a guarded residual domain. + */ +interface TsUnknownCallModel { + val id: String + val target: TsUnknownCallTarget + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? +} + /** Describes how a guarded model successor completes the original call. */ sealed interface TsUnknownCallModelCompletion { /** Produces a normal result on the selected successor state. */ @@ -58,12 +61,7 @@ sealed interface TsUnknownCallModelCompletion { ) : 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. - */ +/** One guarded model successor. */ class TsUnknownCallModelSuccessor( val guard: UBoolExpr, val completion: TsUnknownCallModelCompletion, @@ -71,15 +69,14 @@ class TsUnknownCallModelSuccessor( ) /** - * A backend-neutral semantic-model execution plan. + * A 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. The dispatcher validates disjointness and coverage before - * applying any successor. + * [residualGuard] is the input domain not covered by the model. `null` means that the model completely handles every + * state accepted by [TsUnknownCallModel.apply]. */ class TsUnknownCallModelExecution( successors: List, - val residualGuard: UBoolExpr?, + val residualGuard: UBoolExpr? = null, ) { val successors: List = successors.toList() @@ -88,30 +85,17 @@ class TsUnknownCallModelExecution( } } -/** The result of selecting and executing a semantic model for one call. */ +/** The result of model lookup 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. */ + /** No enabled model accepted 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/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt new file mode 100644 index 000000000..dd74e9343 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt @@ -0,0 +1,92 @@ +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 + +/** An immutable deterministic set of semantic models used by one machine run. */ +class TsUnknownCallModelCatalog( + models: Collection, + enabledModelIds: Set? = null, +) { + private val models: List + + val modelIds: List + get() = models.map(TsUnknownCallModel::id) + + val fingerprint: String + + init { + val allModels = models.sortedBy(TsUnknownCallModel::id) + val duplicateIds = allModels + .groupingBy(TsUnknownCallModel::id) + .eachCount() + .filterValues { count -> count > 1 } + .keys + .sorted() + + require(allModels.none { model -> model.id.isBlank() }) { "Semantic model ID must not be blank" } + require(duplicateIds.isEmpty()) { "Duplicate semantic model IDs: ${duplicateIds.joinToString()}" } + + val selectedIds = enabledModelIds?.toSet() + val knownIds = allModels.mapTo(mutableSetOf(), TsUnknownCallModel::id) + val unknownIds = selectedIds.orEmpty().subtract(knownIds).sorted() + + require(unknownIds.isEmpty()) { "Unknown semantic model IDs: ${unknownIds.joinToString()}" } + + this.models = when (selectedIds) { + null -> allModels + else -> allModels.filter { model -> model.id in selectedIds } + } + + validateUnambiguousTargets(this.models) + fingerprint = computeFingerprint(this.models) + } + + internal fun select(call: TsUnknownCall): TsUnknownCallModel? = + models.singleOrNull { model -> model.target.matches(call) } + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable + + return TsUnknownCallModelApplication.Applied( + modelId = model.id, + execution = execution, + ) + } +} + +private fun validateUnambiguousTargets(models: List) { + models.forEachIndexed { index, model -> + val conflictingModel = models.drop(index + 1).firstOrNull { other -> + model.target.overlaps(other.target) + } ?: return@forEachIndexed + + error( + "Ambiguous semantic model targets: " + + listOf(model.id, conflictingModel.id).sorted().joinToString() + ) + } +} + +private fun computeFingerprint(models: List): String { + val digest = MessageDigest.getInstance("SHA-256") + + models.forEach { model -> + digest.updateLengthPrefixed(model.id) + } + + 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/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt new file mode 100644 index 000000000..c8933340f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -0,0 +1,175 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsClassSignature +import org.usvm.api.makeFreshUnknownCallResult +import org.usvm.api.mockMethodCall +import org.usvm.api.setMockMethodCallResult +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 effect of an unknown-call decision. */ +enum class TsUnknownCallOutcome { + MODEL_APPLIED, + FRESH_SYMBOLIC_RETURN, + PATH_STOPPED, +} + +/** Selects what happens when no semantic model handles an unknown call. */ +enum class TsResidualCallPolicy { + STOP_PATH, + FRESH_SYMBOLIC_RETURN, +} + +/** Selects a semantic model and sends unsupported states to one configured fallback. */ +class TsModelUnknownCallDispatcher( + private val models: TsUnknownCallModelCatalog, + private val fallback: TsResidualCallPolicy, + fallbackOverrides: Map = emptyMap(), + private val observer: TsInterpreterObserver? = null, +) : TsUnknownCallModelDispatcher { + private val fallbackOverrides = fallbackOverrides.toMap() + + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + val application = scope.calcOnState { + this@TsModelUnknownCallDispatcher.models.apply(this, call) + } + + return when (application) { + is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) + TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call) + } + } + + private fun applyFallback( + scope: TsStepScope, + call: TsUnknownCall, + ): TsUnknownCallOutcome { + val policy = fallbackFor(call) + val decision = TsUnknownCallDecision.ResidualFallback(policy) + + when (policy) { + TsResidualCallPolicy.STOP_PATH -> { + val falseExpr = scope.calcOnState { ctx.falseExpr } + scope.assert(falseExpr) + } + + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { + mockMethodCall(scope, call.callee, call.resultType) + scope.doWithState { newStmt(call.callSite) } + } + } + + observer?.onUnknownCallSafely(event(call, decision)) + return decision.outcome + } + + private fun applyModel( + scope: TsStepScope, + call: TsUnknownCall, + application: TsUnknownCallModelApplication.Applied, + ): TsUnknownCallOutcome { + val residualGuard = application.execution.residualGuard + val residualPolicy = fallbackFor(call) + // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone + // inherits both the constraints and their solver models. + val freshResidualResult = if ( + residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + ) { + makeFreshUnknownCallResult(scope, call.resultType) + } else { + null + } + 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, + modelId = application.modelId, + successor = successor, + onApplied = { + modelApplied = true + if (modelEventReported) { + false + } else { + modelEventReported = true + true + } + }, + ) + }.toMutableList() + + if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + guardedStateChanges += residualGuard to { + setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) + newStmt(call.callSite) + freshResidualApplied = true + + observer?.onUnknownCallSafely( + event(call, TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN)) + ) + } + } + + scope.forkMulti(guardedStateChanges) + + if (stoppedResidualIsSatisfiable) { + observer?.onUnknownCallSafely( + event(call, TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH)) + ) + } + + 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, + modelId: String, + 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()) { + observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(modelId))) + } + } + + private fun fallbackFor(call: TsUnknownCall): TsResidualCallPolicy = + fallbackOverrides[call.callee.enclosingClass] ?: fallback + + private fun event( + call: TsUnknownCall, + decision: TsUnknownCallDecision, + ) = TsUnknownCallEvent( + callSite = call.callSite, + callee = call.callee, + failureReason = call.failureReason, + decision = decision, + ) +} 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 deleted file mode 100644 index 45471e1e8..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt +++ /dev/null @@ -1,162 +0,0 @@ -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 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 } - 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 } - } - 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) - } - - 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(registration.implementation, state, 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/TsUnknownCallObservation.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt index 7adf43527..2ae84bffd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt @@ -7,12 +7,6 @@ import org.usvm.machine.TsInterpreterObserver private val logger = KotlinLogging.logger {} -/** Explains why a call reached the residual fallback instead of a semantic model. */ -enum class TsUnknownCallResidualReason { - MODEL_LOOKUP_DISABLED, - MODEL_NOT_APPLICABLE, -} - /** Describes the model or fallback action selected for one unknown call. */ sealed interface TsUnknownCallDecision { data class ModelApplied( @@ -25,19 +19,28 @@ sealed interface TsUnknownCallDecision { data class ResidualFallback( val policy: TsResidualCallPolicy, - val reason: TsUnknownCallResidualReason, ) : TsUnknownCallDecision } +val TsUnknownCallDecision.outcome: TsUnknownCallOutcome + get() = when (this) { + is TsUnknownCallDecision.ModelApplied -> TsUnknownCallOutcome.MODEL_APPLIED + is TsUnknownCallDecision.ResidualFallback -> when (policy) { + TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + } + } + /** A structured decision reported for one unknown call. */ data class TsUnknownCallEvent( val callSite: EtsStmt, val callee: EtsMethodSignature, val failureReason: TsUnknownCallFailureReason, - val profile: TsUnknownCallProfile, - val outcome: TsUnknownCallOutcome, val decision: TsUnknownCallDecision, -) +) { + val outcome: TsUnknownCallOutcome + get() = decision.outcome +} internal fun TsInterpreterObserver.onUnknownCallSafely(event: TsUnknownCallEvent) { runCatching { onUnknownCall(event) } 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 deleted file mode 100644 index 1c763c6a1..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ /dev/null @@ -1,350 +0,0 @@ -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 { - MODEL_APPLIED, - FRESH_SYMBOLIC_RETURN, - PATH_STOPPED, -} - -/** Controls whether the dispatcher asks the configured model provider to handle a call. */ -enum class TsUnknownCallModelLookup { - DISABLED, - ENABLED, -} - -/** - * Selects what happens when model lookup is disabled or no model applies. - * - * [FRESH_SYMBOLIC_RETURN] creates a new symbolic value of the call expression's result type and advances past the - * call. It deliberately ignores all callee side effects and exceptions, so it is an opaque continuation rather than - * a semantic model of the callee. - */ -enum class TsResidualCallPolicy { - STOP_PATH, - FRESH_SYMBOLIC_RETURN, -} - -/** Independently configures model lookup and the fallback for residual calls. */ -data class TsUnknownCallProfile( - val modelLookup: TsUnknownCallModelLookup, - val residualPolicy: TsResidualCallPolicy, - val residualOverrides: Map = emptyMap(), -) { - internal fun residualPolicyFor(call: TsUnknownCall): TsResidualCallPolicy = - residualOverrides[call.callee.enclosingClass] ?: residualPolicy -} - -/** Ready-to-use profiles for the four supported model/fallback combinations. */ -object TsUnknownCallProfiles { - val STOP_ALL = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.DISABLED, - residualPolicy = TsResidualCallPolicy.STOP_PATH, - ) - val FRESH_SYMBOLIC_FOR_ALL = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.DISABLED, - residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) - val MODELS_THEN_STOP = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.ENABLED, - residualPolicy = TsResidualCallPolicy.STOP_PATH, - ) - val MODELS_THEN_FRESH_SYMBOLIC = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.ENABLED, - residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) -} - -/** Empty provider used until an explicit model registry is configured. */ -object TsNoUnknownCallModels : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication = - TsUnknownCallModelApplication.NotApplicable -} - -/** Applies the selected model/fallback profile to every residual call. */ -class TsProfileUnknownCallDispatcher( - private val profile: TsUnknownCallProfile, - private val modelProvider: TsUnknownCallModelProvider, - private val observer: TsInterpreterObserver? = null, -) : TsUnknownCallModelDispatcher { - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - if (profile.modelLookup == TsUnknownCallModelLookup.DISABLED) { - return applyResidualFallback( - scope, - call, - reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, - ) - } - - val application = scope.calcOnState { - modelProvider.apply(this, call) - } - return when (application) { - is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) - - TsUnknownCallModelApplication.NotApplicable -> applyResidualFallback( - scope, - 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 - TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN - } - val event = event( - call, - outcome, - decision = TsUnknownCallDecision.ResidualFallback( - residualPolicy, - reason, - ), - ) - when (residualPolicy) { - TsResidualCallPolicy.STOP_PATH -> { - val falseExpr = scope.calcOnState { ctx.falseExpr } - scope.assert(falseExpr) - } - - TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { - mockMethodCall(scope, call.callee, call.resultType) - scope.doWithState { newStmt(call.callSite) } - } - } - - observer?.onUnknownCallSafely(event) - return outcome - } - - private fun applyModel( - scope: TsStepScope, - call: TsUnknownCall, - application: TsUnknownCallModelApplication.Applied, - ): TsUnknownCallOutcome { - 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, call.resultType) - } else { - null - } - 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, - application, - successor, - onApplied = { - modelApplied = true - if (modelEventReported) { - false - } else { - modelEventReported = true - true - } - }, - ) - }.toMutableList() - - if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { - guardedStateChanges += residualGuard to { - setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) - newStmt(call.callSite) - freshResidualApplied = true - - val event = residualEvent( - call, - policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) - observer?.onUnknownCallSafely(event) - } - } - - scope.forkMulti(guardedStateChanges) - - if (stoppedResidualIsSatisfiable) { - val event = residualEvent( - 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 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(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, - 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, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId), - ) - observer?.onUnknownCallSafely(event) - } - } - - private fun residualEvent( - call: TsUnknownCall, - policy: TsResidualCallPolicy, - ) = event( - call, - outcome = when (policy) { - TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED - TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN - }, - decision = TsUnknownCallDecision.ResidualFallback( - policy, - reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, - ), - ) - - private fun event( - call: TsUnknownCall, - outcome: TsUnknownCallOutcome, - decision: TsUnknownCallDecision, - ) = TsUnknownCallEvent( - callSite = call.callSite, - callee = call.callee, - failureReason = call.failureReason, - profile = profile.copy(residualOverrides = profile.residualOverrides.toMap()), - outcome = outcome, - 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/call/intrinsic/TsArrayPopIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt deleted file mode 100644 index e82be0e6b..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt +++ /dev/null @@ -1,130 +0,0 @@ -package org.usvm.machine.call.intrinsic - -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.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 - -/** Partial intrinsic model for `Array.pop` on resolved one-dimensional primitive arrays. */ -internal object TsArrayPopIntrinsicModel : TsIntrinsicUnknownCallModel { - const val MODEL_ID: String = "ts.array.pop" - - private val descriptor = TsUnknownCallModelDescriptor( - id = 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 primitive element sort", - ), - precision = TsUnknownCallModelPrecision.PARTIAL, - implementationKind = TsUnknownCallModelImplementationKind.INTRINSIC, - ) - - val registration = TsUnknownCallModelRegistration( - descriptor = descriptor, - implementation = TsIntrinsicUnknownCallModelImplementation(this), - ) - - override fun execute(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { - val input = resolveInput(state, 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) - if (elementSort == state.ctx.addressSort) { - return null - } - - return ArrayPopInput(array, arrayType, 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/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt new file mode 100644 index 000000000..cf86b6041 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -0,0 +1,108 @@ +package org.usvm.machine.call.intrinsic + +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.memcpy +import org.usvm.api.typeStreamOf +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.types.singleOrNull +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +/** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */ +internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { + const val MODEL_ID: String = "ts.array.shift" + + override val id: String = MODEL_ID + override val target = TsUnknownCallTarget( + methodName = "shift", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) { + val input = resolveInput(state, call) ?: return@with null + val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType) + val length = state.memory.read(lengthLValue) + val zero = mkBv(0) + val emptyGuard = mkEq(length, zero) + val nonEmptyGuard = mkBvSignedLessExpr(zero, length) + val newLength = mkBvSubExpr(length, mkBv(1)) + val firstElementLValue = mkArrayIndexLValue( + sort = input.elementSort, + ref = input.array, + index = zero, + type = input.arrayType, + ) + val firstElement = state.memory.read(firstElementLValue) + + val emptySuccessor = TsUnknownCallModelSuccessor( + guard = emptyGuard, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + val nonEmptySuccessor = TsUnknownCallModelSuccessor( + guard = nonEmptyGuard, + completion = TsUnknownCallModelCompletion.Normal { firstElement }, + applyStateChanges = { + memory.memcpy( + srcRef = input.array, + dstRef = input.array, + type = input.arrayType, + elementSort = input.elementSort, + fromSrc = mkBv(1), + fromDst = zero, + length = newLength, + ) + memory.write(lengthLValue, newLength, guard = trueExpr) + }, + ) + + TsUnknownCallModelExecution( + successors = listOf(emptySuccessor, nonEmptySuccessor), + residualGuard = mkNot(mkOr(emptyGuard, nonEmptyGuard)), + ) + } + + private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayShiftInput? = with(state.ctx) { + if (call.arguments.isNotEmpty()) { + return@with null + } + + val receiver = call.receiver ?: return@with null + val receiverValue = receiver.resolved ?: return@with null + if (receiverValue.sort != addressSort || receiverValue.containsFakeObject()) { + return@with null + } + + val array = receiverValue.asExpr(addressSort) + val arrayType = (receiver.source.type as? EtsArrayType) + ?: (state.memory.typeStreamOf(array).singleOrNull() as? EtsArrayType) + ?: return@with null + if (arrayType.dimensions != 1) { + return@with null + } + + val elementSort = typeToSort(arrayType.elementType) + if (elementSort is TsUnresolvedSort) { + return@with null + } + + ArrayShiftInput(array, arrayType, elementSort) + } + + private class ArrayShiftInput( + val array: UExpr, + val arrayType: EtsArrayType, + val elementSort: USort, + ) +} 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 deleted file mode 100644 index 0870cb410..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModel.kt +++ /dev/null @@ -1,39 +0,0 @@ -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/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 8e7c845eb..c48b2c552 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 @@ -29,7 +29,7 @@ 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 +import org.usvm.types.singleOrNull import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.resolveEtsMethods @@ -93,7 +93,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val instanceType = if (instance.sort == addressSort && isAllocatedConcreteHeapRef(instance)) { scope.calcOnState { - memory.typeStreamOf(instance.asExpr(addressSort)).firstOrNull() ?: expr.instance.type + memory.typeStreamOf(instance.asExpr(addressSort)).singleOrNull() ?: expr.instance.type } } else { expr.instance.type @@ -111,7 +111,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return handleArrayPopCall(expr, instanceType, elementSort, instance) + return from(handleArrayPop(expr, instanceType, elementSort)) } // Handle `Array.fill() method calls @@ -126,7 +126,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.shift() method calls if (expr.callee.name == "shift") { - return from(handleArrayShift(expr, instanceType, elementSort)) + return handleArrayShiftCall(expr, instanceType, elementSort, instance) } // Handle `Array.join() method calls @@ -163,7 +163,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return TsExprApproximationResult.NoApproximation } -private fun TsExprResolver.handleArrayPopCall( +private fun TsExprResolver.handleArrayShiftCall( expr: EtsInstanceCallExpr, instanceType: EtsArrayType, elementSort: USort, @@ -171,7 +171,7 @@ private fun TsExprResolver.handleArrayPopCall( ): TsExprApproximationResult { val dispatcher = unknownCallDispatcher if (dispatcher !is TsUnknownCallModelDispatcher) { - return from(handleArrayPop(expr, instanceType, elementSort)) + return from(handleArrayShift(expr, instanceType, elementSort)) } dispatcher.dispatch( diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt similarity index 60% rename from usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt rename to usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index ea1dd94d4..a0d16c22b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -1,18 +1,23 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsInstanceCallExpr import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.loadEtsFileAutoConvert -import org.junit.jupiter.api.Disabled import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr import org.usvm.UMachineOptions import org.usvm.api.TsTestValue +import org.usvm.api.makeSymbolicRefUntyped import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.util.TsTestResolver @@ -25,24 +30,24 @@ import kotlin.test.assertNull import kotlin.test.assertTrue import kotlin.time.Duration -class TsArrayPopIntrinsicModelTest { +class TsArrayShiftIntrinsicModelTest { private val sourceFile = loadEtsFileAutoConvert( - getResourcePath("/models/ArrayPopIntrinsic.ts"), + getResourcePath("/models/ArrayShiftIntrinsic.ts"), provider = EtsIrProvider.TS_FRONTEND, ) private val scene = EtsScene(listOf(sourceFile)) @Test - fun `empty array pop returns undefined through intrinsic model`() { + fun `empty array shift returns undefined through intrinsic model`() { val result = analyze(methodName = "emptyArray") assertIs(result.values.single()) - assertEquals(listOf("ts.array.pop"), result.modelIds) + assertEquals(listOf("ts.array.shift"), result.modelIds) assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}"))) } @Test - fun `non empty array pop returns last element and shrinks array`() { + fun `non empty array shift returns first element moves tail and shrinks array`() { val result = analyze(methodName = "nonEmptyArray") assertEquals(32.0, assertIs(result.values.single()).number) @@ -50,13 +55,10 @@ class TsArrayPopIntrinsicModelTest { } @Test - fun `allocated reference array uses residual fallback`() { - assertUsesResidualFallback(methodName = "aliasedElement") - } + fun `reference array preserves removed element alias`() { + val result = analyze(methodName = "aliasedElement") - @Test - fun `symbolic reference array uses residual fallback`() { - assertUsesResidualFallback(methodName = "symbolicReferenceArray") + assertEquals(42.0, assertIs(result.values.single()).number) } @Test @@ -73,57 +75,51 @@ class TsArrayPopIntrinsicModelTest { } @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) + fun `array shift with arguments uses residual fallback`() { + assertUsesResidualFallback(methodName = "shiftWithArguments") } @Test - fun `array pop with arguments uses residual fallback`() { - assertUsesResidualFallback(methodName = "popWithArguments") + fun `fake wrapper receiver is not accepted as an array`() { + val state = analyzeStates(methodName = "unknownValue").single() + val fakeReceiver = makeFakeReceiver(state) + + val execution = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(fakeReceiver)) + + assertNull(execution) } - @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", + fun `conditional receiver containing fake wrapper is not accepted as an array`() { + val state = analyzeStates(methodName = "unknownValue").single() + val fakeReceiver = makeFakeReceiver(state) + val fakeType = with(state.ctx) { fakeReceiver.getFakeType(state.memory) } + val conditionalReceiver = state.ctx.mkIte( + condition = fakeType.boolTypeExpr, + trueBranch = fakeReceiver, + falseBranch = state.makeSymbolicRefUntyped(), ) + + val execution = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(conditionalReceiver)) + + assertNull(execution) } @Test - fun `disabled model sends pop to configured residual fallback`() { - val enabledModelIds = mutableSetOf("ts.array.pop") - val selection = TsUnknownCallModelSelection(enabledModelIds) - enabledModelIds.clear() - val result = analyze( + fun `empty enabled set sends shift to configured fallback`() { + val disabledResult = analyze( methodName = "nonEmptyArray", tsOptions = TsOptions( - unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - unknownCallModels = TsUnknownCallModelSelection(enabledModelIds = emptySet()), + enabledUnknownCallModelIds = emptySet(), + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ), ) - 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) + assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), disabledResult.events.map { it.outcome }) } @Test - fun `compatibility dispatcher keeps the legacy pop approximation`() { + fun `compatibility dispatcher keeps the legacy shift approximation`() { val result = analyze( methodName = "nonEmptyArray", dispatcher = TsCompatibilityUnknownCallDispatcher, @@ -164,9 +160,31 @@ class TsArrayPopIntrinsicModelTest { val result = analyze(methodName) assertTrue(result.values.isEmpty()) - val event = result.events.single() - assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome) - assertIs(event.decision) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome) + } + + private fun makeFakeReceiver(state: TsState): UConcreteHeapRef { + val result = assertIs(state.methodResult).value + val fakeReceiver = assertIs(result) + + assertTrue(with(state.ctx) { fakeReceiver.isFakeObject() }) + return fakeReceiver + } + + private fun arrayShiftCall(resolvedReceiver: UExpr<*>): TsUnknownCall { + val callSite = method("nonEmptyArray").cfg.stmts.single { stmt -> + stmt.callExpr?.callee?.name == "shift" + } + val sourceCall = assertIs(assertNotNull(callSite.callExpr)) + + return TsUnknownCall( + callee = sourceCall.callee, + receiver = TsUnknownCallValue(source = sourceCall.instance, resolved = resolvedReceiver), + arguments = emptyList(), + resultType = sourceCall.type, + callSite = callSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) } private fun analyzeStates(methodName: String): List { @@ -182,7 +200,7 @@ class TsArrayPopIntrinsicModelTest { } private fun method(name: String): EtsMethod = scene.projectClasses - .single { it.name == "ArrayPopIntrinsic" } + .single { it.name == "ArrayShiftIntrinsic" } .methods .single { it.name == name } 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 1ed384901..9a29604ea 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 @@ -11,6 +11,7 @@ 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.EtsType import org.jacodb.ets.model.EtsVoidType import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.callExpr @@ -19,7 +20,6 @@ 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 @@ -32,6 +32,7 @@ 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.solver.USatResult import org.usvm.util.getResourcePath import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -50,31 +51,25 @@ class TsUnknownCallDispatcherTest { private val fullScene = EtsScene(listOf(sourceFile)) @Test - fun `every profile decision is reported through the interpreter observer`() { + fun `every model or fallback decision is reported through the interpreter observer`() { val cases = listOf( ObservationCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.STOP_PATH, + models = noModels, outcome = TsUnknownCallOutcome.PATH_STOPPED, - decision = TsUnknownCallDecision.ResidualFallback( - policy = TsResidualCallPolicy.STOP_PATH, - reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, - ), + decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH), finalStateCount = 0, ), ObservationCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = noModels, outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - decision = TsUnknownCallDecision.ResidualFallback( - policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, - ), + decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), finalStateCount = 1, ), ObservationCase( - profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, - modelProvider = ApplyingModelProvider, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(ApplyingModel), outcome = TsUnknownCallOutcome.MODEL_APPLIED, decision = TsUnknownCallDecision.ModelApplied(modelId = "applying-model"), finalStateCount = 1, @@ -85,17 +80,16 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "declaredMethodWithoutBodyContinues", - profile = case.profile, - modelProvider = case.modelProvider, + fallback = case.fallback, + models = case.models, observer = observer, ) - assertEquals(case.finalStateCount, states.size, case.profile.toString()) + assertEquals(case.finalStateCount, states.size, case.fallback.toString()) val event = observer.events.single() assertEquals("declaredMethodWithoutBodyContinues", event.callSite.location.method.name) assertEquals("external", event.callee.name) assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, event.failureReason) - assertEquals(case.profile, event.profile) assertEquals(case.outcome, event.outcome) assertEquals(case.decision, event.decision) } @@ -106,8 +100,7 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "modeledUnknownCallForks", - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = ForkingModelProvider, + models = catalog(ForkingModel), observer = observer, ) @@ -120,13 +113,13 @@ class TsUnknownCallDispatcherTest { fun `throwing observer cannot change fresh or modeled exploration`() { val cases = listOf( ObservationFailureCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = noModels, expectedFinalStateCount = 1, ), ObservationFailureCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = ForkingModelProvider, + fallback = TsResidualCallPolicy.STOP_PATH, + models = catalog(ForkingModel), expectedFinalStateCount = 2, methodName = "modeledUnknownCallForks", ), @@ -135,12 +128,12 @@ class TsUnknownCallDispatcherTest { cases.forEach { case -> val states = analyzeAllStates( methodName = case.methodName, - profile = case.profile, - modelProvider = case.modelProvider, + fallback = case.fallback, + models = case.models, observer = ThrowingUnknownCallObserver, ) - assertEquals(case.expectedFinalStateCount, states.size, case.profile.toString()) + assertEquals(case.expectedFinalStateCount, states.size, case.fallback.toString()) } } @@ -149,8 +142,7 @@ class TsUnknownCallDispatcherTest { assertFailsWith { TsUnknownCallModelApplication.Applied( modelId = " ", - precision = TsUnknownCallModelPrecision.EXACT, - execution = exactExecution(), + execution = completeExecution(), ) } assertFailsWith { @@ -159,42 +151,30 @@ class TsUnknownCallDispatcherTest { } @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), + fun `model execution plans require at least one successor`() { + val error = assertFailsWith { + TsUnknownCallModelExecution( + successors = emptyList(), + residualGuard = mockk(), ) } + + assertEquals("A semantic model must declare at least one guarded successor", error.message) } @Test - fun `fresh fallback keeps fake type constraints in state models`() { - val states = analyzeAllStates( - methodName = "freshUnknownCallResult", - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, + fun `fresh fallback preserves all fake value representations`() { + assertFreshResultPreservesAllFakeRepresentations( + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ) - - 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, + fun `partial residual fallback preserves all fake value representations`() { + assertFreshResultPreservesAllFakeRepresentations( + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(UnsupportedPartialModel), ) - - assertFreshResultModelSatisfiesFakeType(states.single()) } @Test @@ -202,8 +182,8 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "modeledUnknownCallForks", - profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, - modelProvider = SupportedTrueResidualFalseProvider, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(SupportedTrueResidualFalseModel), observer = observer, ) @@ -219,8 +199,7 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "modeledUnknownCallForks", - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = SupportedTrueResidualFalseProvider, + models = catalog(SupportedTrueResidualFalseModel), observer = observer, ) @@ -235,8 +214,7 @@ class TsUnknownCallDispatcherTest { fun `exceptional model successor preserves exception state`() { val states = analyzeAllStates( methodName = "modeledUnknownCallThrows", - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = ExceptionalModelProvider, + models = catalog(ExceptionalModel), ) assertIs(states.single().methodResult) @@ -246,8 +224,7 @@ class TsUnknownCallDispatcherTest { fun `stateful model can return an existing reference alias`() { val states = analyzeAllStates( methodName = "modeledUnknownCallReturnsAlias", - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = StatefulAliasModelProvider, + models = catalog(StatefulAliasModel), ) val aliasReturn = method(fullScene, "modeledUnknownCallReturnsAlias") .cfg @@ -261,76 +238,22 @@ class TsUnknownCallDispatcherTest { } @Test - fun `profiles select model lookup independently from residual fallback`() { - val cases = listOf( - ProfileCase( - profile = TsUnknownCallProfiles.STOP_ALL, - withoutModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - withModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - withoutModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - withoutModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, - withoutModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - ), - ), - ) - - cases.forEach { case -> - assertEquals(case.withoutModel, runProfile(case.profile, TsNoUnknownCallModels), case.profile.toString()) - assertEquals(case.withModel, runProfile(case.profile, ApplyingModelProvider), case.profile.toString()) - } - } - - @Test - fun `TsOptions profile configures the machine dispatcher`() { - assertEquals(TsUnknownCallProfiles.MODELS_THEN_STOP, TsOptions().unknownCallProfile) - assertTrue(TsOptions().unknownCallProfile.residualOverrides.isEmpty()) + fun `TsOptions configures one fallback without profiles`() { + assertEquals(TsResidualCallPolicy.STOP_PATH, TsOptions().unknownCallFallback) + assertNull(TsOptions().enabledUnknownCallModelIds) + assertTrue(TsOptions().unknownCallFallbackOverrides.isEmpty()) assertFalse(reachesReturn("declaredMethodWithoutBodyContinues")) assertTrue( reachesReturn( "declaredMethodWithoutBodyContinues", - tsOptions = TsOptions(unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL), + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), ) ) } @Test - fun `explicit family override replaces the profile residual fallback`() { + fun `explicit family override replaces the default residual fallback`() { val family = method(fullScene, "declaredMethodWithoutBodyContinues") .cfg .stmts @@ -338,16 +261,15 @@ class TsUnknownCallDispatcherTest { .single { it.callee.name == "external" } .callee .enclosingClass - val profile = TsUnknownCallProfiles.STOP_ALL.copy( - residualOverrides = mapOf( - family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) - ) assertTrue( reachesReturn( "declaredMethodWithoutBodyContinues", - tsOptions = TsOptions(unknownCallProfile = profile), + tsOptions = TsOptions( + unknownCallFallbackOverrides = mapOf( + family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), + ), ) ) } @@ -355,9 +277,9 @@ class TsUnknownCallDispatcherTest { @Test fun `fresh symbolic return uses the source call result type`() { val dispatcher = RecordingResultSortDispatcher( - TsProfileUnknownCallDispatcher( - TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - TsNoUnknownCallModels, + TsModelUnknownCallDispatcher( + models = noModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ) ) @@ -463,7 +385,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor keeps typed call data without eagerly resolving arguments`() { + fun `unknown call keeps typed data without eagerly resolving arguments`() { val dispatcher = RecordingUnknownCallDispatcher() val scene = sceneWithout("ExternalStatic") @@ -478,7 +400,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor preserves source and resolved values available at dispatch`() { + fun `unknown call preserves source and resolved values available at dispatch`() { val dispatcher = RecordingUnknownCallDispatcher() assertFalse(reachesReturn("nonReferenceInstanceCallPrunes", dispatcher = dispatcher)) @@ -519,7 +441,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `pointer descriptor pairs its source with the resolved function pointer`() { + fun `pointer call pairs its source with the resolved function pointer`() { val dispatcher = RecordingUnknownCallDispatcher() val pointerCall = method(fullScene, "associatedLoggingPointerContinues", className = "Log") .cfg @@ -543,7 +465,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor result type comes from the source overload`() { + fun `unknown call result type comes from the source overload`() { val dispatcher = RecordingUnknownCallDispatcher() assertTrue(reachesReturn("overloadedDeclaredMethodWithoutBodyContinues", dispatcher = dispatcher)) @@ -561,17 +483,17 @@ class TsUnknownCallDispatcherTest { scene: EtsScene = fullScene, tsOptions: TsOptions = TsOptions(), dispatcher: TsUnknownCallDispatcher? = null, - modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + models: TsUnknownCallModelCatalog = noModels, className: String = "CallFallbackBaseline", ): Boolean = returnStatement(scene, methodName, className) in - reachedStatements(methodName, scene, tsOptions, dispatcher, modelProvider, className) + reachedStatements(methodName, scene, tsOptions, dispatcher, models, className) private fun reachedStatements( methodName: String, scene: EtsScene, tsOptions: TsOptions, dispatcher: TsUnknownCallDispatcher?, - modelProvider: TsUnknownCallModelProvider, + models: TsUnknownCallModelCatalog, className: String, ): Set { val method = method(scene, methodName, className) @@ -585,7 +507,7 @@ class TsUnknownCallDispatcherTest { tsOptions = tsOptions, machineObserver = ReachabilityObserver(), unknownCallDispatcher = dispatcher, - unknownCallModelProvider = modelProvider, + unknownCallModels = models, ).use { machine -> machine.analyze(listOf(method), listOf(initialTarget)) .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } @@ -617,32 +539,58 @@ class TsUnknownCallDispatcherTest { private fun analyzeAllStates( methodName: String, - profile: TsUnknownCallProfile, - modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + fallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, + models: TsUnknownCallModelCatalog = noModels, observer: TsInterpreterObserver? = null, ): List { val method = method(fullScene, methodName) return TsMachine( scene = fullScene, options = allStatesMachineOptions, - tsOptions = TsOptions(unknownCallProfile = profile), + tsOptions = TsOptions(unknownCallFallback = fallback), observer = observer, - unknownCallModelProvider = modelProvider, + unknownCallModels = models, ).use { machine -> machine.analyze(listOf(method)) } } - 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) - } + private fun assertFreshResultPreservesAllFakeRepresentations( + fallback: TsResidualCallPolicy, + models: TsUnknownCallModelCatalog = noModels, + ) { + val method = method(fullScene, "freshUnknownCallResult") + TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(unknownCallFallback = fallback), + unknownCallModels = models, + ).use { machine -> + val state = machine.analyze(listOf(method)).single() + val result = assertIs(state.methodResult).value + val fakeValue = assertIs(result) + val fakeType = with(state.ctx) { + assertTrue(fakeValue.isFakeObject()) + fakeValue.getFakeType(state.memory) + } + val discriminators = mapOf( + "boolean" to fakeType.boolTypeExpr, + "number" to fakeType.fpTypeExpr, + "reference" to fakeType.refTypeExpr, + ) - assertTrue(state.models.isNotEmpty()) - assertTrue(state.models.all { model -> model.eval(exactlyOneType).isTrue }) + discriminators.forEach { (kind, discriminator) -> + val constraints = state.pathConstraints.clone() + constraints += discriminator + val solverResult = state.ctx.solver().check(constraints) + + assertIs>(solverResult, "Fresh fake result lost its $kind representation") + } + + val exactlyOneType = fakeType.mkExactlyOneTypeConstraint(state.ctx) + assertTrue(state.models.isNotEmpty()) + assertTrue(state.models.all { model -> model.eval(exactlyOneType).isTrue }) + } } private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher { @@ -659,27 +607,6 @@ class TsUnknownCallDispatcherTest { } } - private fun runProfile( - profile: TsUnknownCallProfile, - modelProvider: TsUnknownCallModelProvider, - ): ProfileResult { - val dispatcher = RecordingOutcomeDispatcher(TsProfileUnknownCallDispatcher(profile, modelProvider)) - val reachesReturn = reachesReturn( - "declaredMethodWithoutBodyContinues", - dispatcher = dispatcher, - ) - return ProfileResult(reachesReturn, dispatcher.outcomes.single()) - } - - private class RecordingOutcomeDispatcher( - private val delegate: TsUnknownCallDispatcher, - ) : TsUnknownCallDispatcher { - val outcomes = mutableListOf() - - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome = - delegate.dispatch(scope, call).also(outcomes::add) - } - private class RecordingResultSortDispatcher( private val delegate: TsUnknownCallDispatcher, ) : TsUnknownCallDispatcher { @@ -697,52 +624,40 @@ class TsUnknownCallDispatcherTest { } } - private object ApplyingModelProvider : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + private object ApplyingModel : TestModel(id = "applying-model", methodName = "external") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { 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, - ), - ) + return TsUnknownCallModelExecution(successors = listOf(successor)) } } - private object ForkingModelProvider : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + private object ForkingModel : TestModel(id = "forking-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val result = requireNotNull(call.arguments.single().resolved) 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, - ), + return 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 { + private object SupportedTrueResidualFalseModel : TestModel(id = "partial-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val result = requireNotNull(call.arguments.single().resolved) val condition = result.asExpr(state.ctx.boolSort) val successor = TsUnknownCallModelSuccessor( @@ -750,19 +665,15 @@ class TsUnknownCallDispatcherTest { completion = TsUnknownCallModelCompletion.Normal { result }, ) - return TsUnknownCallModelApplication.Applied( - modelId = "partial-model", - precision = TsUnknownCallModelPrecision.PARTIAL, - execution = TsUnknownCallModelExecution( - successors = listOf(successor), - residualGuard = state.ctx.mkNot(condition), - ), + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), ) } } - private object ExceptionalModelProvider : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + private object ExceptionalModel : TestModel(id = "exceptional-model", methodName = "fail") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val successor = TsUnknownCallModelSuccessor( guard = state.ctx.trueExpr, completion = TsUnknownCallModelCompletion.Exceptional { @@ -770,37 +681,26 @@ class TsUnknownCallDispatcherTest { }, ) - return TsUnknownCallModelApplication.Applied( - modelId = "exceptional-model", - precision = TsUnknownCallModelPrecision.EXACT, - execution = TsUnknownCallModelExecution( - successors = listOf(successor), - residualGuard = null, - ), - ) + return TsUnknownCallModelExecution(successors = listOf(successor)) } } - private object UnsupportedPartialModelProvider : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + private object UnsupportedPartialModel : TestModel(id = "unsupported-partial-model", methodName = "value") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { 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, - ), + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.trueExpr, ) } } - private object StatefulAliasModelProvider : TsUnknownCallModelProvider { - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + private object StatefulAliasModel : TestModel(id = "stateful-alias-model", methodName = "identity") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val argument = requireNotNull(call.arguments.single().resolved) val successor = TsUnknownCallModelSuccessor( guard = state.ctx.trueExpr, @@ -808,17 +708,17 @@ class TsUnknownCallDispatcherTest { applyStateChanges = { addedArtificialLocals += STATE_CHANGE_MARKER }, ) - return TsUnknownCallModelApplication.Applied( - modelId = "stateful-alias-model", - precision = TsUnknownCallModelPrecision.EXACT, - execution = TsUnknownCallModelExecution( - successors = listOf(successor), - residualGuard = null, - ), - ) + return TsUnknownCallModelExecution(successors = listOf(successor)) } } + private abstract class TestModel( + override val id: String, + methodName: String, + ) : TsUnknownCallModel { + override val target = TsUnknownCallTarget(methodName = methodName) + } + private class RecordingUnknownCallObserver : TsInterpreterObserver { val events = mutableListOf() @@ -833,28 +733,17 @@ class TsUnknownCallDispatcherTest { } } - private data class ProfileCase( - val profile: TsUnknownCallProfile, - val withoutModel: ProfileResult, - val withModel: ProfileResult, - ) - - private data class ProfileResult( - val reachesReturn: Boolean, - val outcome: TsUnknownCallOutcome, - ) - private data class ObservationCase( - val profile: TsUnknownCallProfile, - val modelProvider: TsUnknownCallModelProvider, + val fallback: TsResidualCallPolicy, + val models: TsUnknownCallModelCatalog, val outcome: TsUnknownCallOutcome, val decision: TsUnknownCallDecision, val finalStateCount: Int, ) private data class ObservationFailureCase( - val profile: TsUnknownCallProfile, - val modelProvider: TsUnknownCallModelProvider, + val fallback: TsResidualCallPolicy, + val models: TsUnknownCallModelCatalog, val expectedFinalStateCount: Int, val methodName: String = "declaredMethodWithoutBodyContinues", ) @@ -878,9 +767,12 @@ class TsUnknownCallDispatcherTest { private companion object { const val STATE_CHANGE_MARKER = "semantic-model-state-change" - fun exactExecution(): TsUnknownCallModelExecution = execution(residualGuard = null) + val noModels = TsUnknownCallModelCatalog(emptyList()) + + fun catalog(vararg models: TsUnknownCallModel): TsUnknownCallModelCatalog = + TsUnknownCallModelCatalog(models.toList()) - fun execution(residualGuard: UBoolExpr?): TsUnknownCallModelExecution = + fun completeExecution(): TsUnknownCallModelExecution = TsUnknownCallModelExecution( successors = listOf( TsUnknownCallModelSuccessor( @@ -888,7 +780,6 @@ class TsUnknownCallDispatcherTest { completion = TsUnknownCallModelCompletion.Normal { mockk>() }, ), ), - residualGuard = residualGuard, ) val machineOptions = UMachineOptions( 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 deleted file mode 100644 index f27312644..000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt +++ /dev/null @@ -1,206 +0,0 @@ -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("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, profile, 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/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt new file mode 100644 index 000000000..cde61a23c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -0,0 +1,118 @@ +package org.usvm.machine.call + +import org.usvm.machine.state.TsState +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotEquals +import kotlin.test.assertTrue + +class TsUnknownCallModelCatalogTest { + @Test + fun `model IDs and target names must be non blank`() { + assertFailsWith { + TsUnknownCallModelCatalog(listOf(model(id = " "))) + } + assertFailsWith { + TsUnknownCallTarget(methodName = " ") + } + assertFailsWith { + TsUnknownCallTarget(methodName = "method", enclosingClassName = " ") + } + } + + @Test + fun `duplicate IDs are rejected`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf( + model(id = "duplicate", methodName = "first"), + model(id = "duplicate", methodName = "second"), + ) + ) + } + + assertEquals("Duplicate semantic model IDs: duplicate", error.message) + } + + @Test + fun `overlapping declarative targets are rejected before execution`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf( + model(id = "z-model", methodName = "target"), + model( + id = "a-model", + methodName = "target", + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ), + ) + ) + } + + assertEquals("Ambiguous semantic model targets: a-model, z-model", error.message) + } + + @Test + fun `unknown enabled IDs are rejected`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf(model(id = "known")), + enabledModelIds = setOf("missing"), + ) + } + + assertEquals("Unknown semantic model IDs: missing", error.message) + } + + @Test + fun `selection and fingerprint do not depend on model order`() { + val forward = listOf( + model(id = "a", methodName = "first"), + model(id = "b", methodName = "second"), + ) + + val first = TsUnknownCallModelCatalog(forward) + val second = TsUnknownCallModelCatalog(forward.reversed()) + + assertEquals(listOf("a", "b"), first.modelIds) + assertEquals(first.modelIds, second.modelIds) + assertEquals(first.fingerprint, second.fingerprint) + } + + @Test + fun `enabled subset is detached and changes fingerprint`() { + val mutableIds = mutableSetOf("a") + val models = listOf( + model(id = "a", methodName = "first"), + model(id = "b", methodName = "second"), + ) + val onlyA = TsUnknownCallModelCatalog(models, enabledModelIds = mutableIds) + mutableIds += "b" + val both = TsUnknownCallModelCatalog(models) + + assertEquals(listOf("a"), onlyA.modelIds) + assertNotEquals(onlyA.fingerprint, both.fingerprint) + assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) + } + + private fun model( + id: String, + methodName: String = "target-$id", + failureReason: TsUnknownCallFailureReason? = null, + ): TsUnknownCallModel = FakeModel( + id = id, + target = TsUnknownCallTarget( + methodName = methodName, + failureReason = failureReason, + ), + ) + + private class FakeModel( + override val id: String, + override val target: TsUnknownCallTarget, + ) : TsUnknownCallModel { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution = + error("Fake model must not execute in catalog metadata tests") + } +} 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 deleted file mode 100644 index f45624784..000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt +++ /dev/null @@ -1,152 +0,0 @@ -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 -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")), - backends = listOf(FakeBackend), - ).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 `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( - registration(id = "a", matches = false), - registration(id = "b", matches = true), - ) - val call = mockk() - - 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) - assertEquals(first.fingerprint, second.fingerprint) - } - - @Test - fun `frozen subset is detached and changes fingerprint`() { - val mutableIds = mutableSetOf("a") - val registry = TsUnknownCallModelRegistry( - registrations = listOf(registration("a"), registration("b")), - backends = listOf(FakeBackend), - ) - - 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, 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 - } - - 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/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt deleted file mode 100644 index 30ce632c5..000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/intrinsic/TsIntrinsicUnknownCallModelTest.kt +++ /dev/null @@ -1,20 +0,0 @@ -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) - } -} diff --git a/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts deleted file mode 100644 index 0258b3974..000000000 --- a/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts +++ /dev/null @@ -1,75 +0,0 @@ -// @ts-nocheck -// 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; - } - - 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; - } -} diff --git a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts new file mode 100644 index 000000000..b6fbaee65 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts @@ -0,0 +1,46 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class ArrayElement {} + +export class ArrayShiftIntrinsic { + unknownValue(value: any): any { + return value; + } + + emptyArray(): number | undefined { + const values: number[] = []; + return values.shift(); + } + + nonEmptyArray(): number { + const values = [10, 20, 30]; + return values.shift()! + values[0] + values.length; + } + + aliasedElement(): number { + const element = new ArrayElement(); + const values: ArrayElement[] = [element]; + if (values.shift() === element) { + return 42; + } + + return 0; + } + + symbolicNumberArray(values: number[]): number { + values.shift(); + return 46; + } + + symbolicUnknownArray(values: any[]): number { + values.shift(); + return 47; + } + + shiftWithArguments(): number { + const values = [1]; + values.shift(0); + return 48; + } +} From bcc9d62bf0aeb67433a4cd23f3612b99d1637439 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 7 Sep 2026 23:47:42 +0300 Subject: [PATCH 7/8] [TS Calls] Finish model contract simplification --- usvm-ts/UNKNOWN_CALL_MODELS.md | 38 ++++++++++--------- .../org/usvm/machine/TsInterpreterObserver.kt | 2 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 1 - .../main/kotlin/org/usvm/machine/TsOptions.kt | 2 - .../call/TsUnknownCallModelDispatcher.kt | 19 +++------- .../intrinsic/TsArrayShiftIntrinsicModel.kt | 7 +--- .../call/TsArrayShiftIntrinsicModelTest.kt | 14 +++++++ .../call/TsUnknownCallDispatcherTest.kt | 23 ----------- 8 files changed, 42 insertions(+), 64 deletions(-) diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 578e3fe5b..2e2c6182e 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -82,23 +82,6 @@ The available policies are: `FRESH_SYMBOLIC_RETURN` is deliberately imprecise. Use it only when opaque continuation is preferable to pruning. -### Per-family fallback overrides - -`unknownCallFallbackOverrides` changes the fallback for calls whose callee has a particular -`EtsClassSignature`: - -```kotlin -TsOptions( - unknownCallFallback = TsResidualCallPolicy.STOP_PATH, - unknownCallFallbackOverrides = mapOf( - externalApiSignature to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ), -) -``` - -An override applies both when no model accepts the call and to a residual state returned by a model. Prefer the global -fallback unless one call family has a concrete reason to differ. - ## Model identity and target Every model implements `TsUnknownCallModel`: @@ -200,6 +183,21 @@ Good intrinsic candidates include: Do not write an intrinsic merely because a library method is stateful. +## Source-model migration + +A source model uses the same `TsUnknownCallModel` object and the same ID, target, successor, and residual contract. +The source-model work in PR #380 should extend a successor completion with the EtsIR entry point and resolved inputs, +make the model's EtsIR files visible in the analysis scene, and enter that method through the regular interpreter. +Receiver binding, arguments, returns, exceptions, heap changes, aliases, and nested calls then use normal interpreter +semantics. They must not be reimplemented in a source-specific dispatcher or backend registry. + +The model checks its supported domain before entering EtsIR. An unsupported call returns `null`; a guarded supported +subdomain uses the complementary residual guard and the same configured fallback. Recursive redirection is prevented +by tracking the active model ID in execution state, not by creating a second catalog. + +`Array.pop` is the source-model example. Its TypeScript body uses indexing and `length`; it must not call `pop` again. +The existing `Array.shift` intrinsic remains the example for engine-only symbolic-memory `memcpy`. + ## Dynamic receivers A method name does not prove the receiver type. In particular, `value.shift()` may call a user-defined property rather @@ -224,7 +222,11 @@ The catalog sorts enabled models by ID and hashes their length-prefixed IDs. The not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries. The fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a -manually maintained configuration value. +manually maintained configuration value. Experiment metadata records the tool revision separately. If model source +can change independently of that revision, the runner also records a content hash for the external source or generated +artifact; that content identity is experiment metadata, not another model ID, version, or compatibility setting. Keep +the catalog fingerprint based only on enabled model IDs rather than adding implementation-specific fingerprint fields +to the common model contract. ## Observation diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index df1ad1961..6b6c45168 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -13,7 +13,7 @@ import org.usvm.statistics.UInterpreterObserver @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { - /** Called after the profile dispatcher selects an outcome for an unknown call. */ + /** Called after the dispatcher selects a model or fallback decision for an unknown call. */ fun onUnknownCall(event: TsUnknownCallEvent) { // default empty implementation } 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 edc5c5b5e..15e480447 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -64,7 +64,6 @@ class TsMachine( private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), fallback = tsOptions.unknownCallFallback, - fallbackOverrides = tsOptions.unknownCallFallbackOverrides, 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 fedf989c0..c3213f3a8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,6 +1,5 @@ package org.usvm.machine -import org.jacodb.ets.model.EtsClassSignature import org.usvm.machine.call.TsResidualCallPolicy data class TsOptions( @@ -10,5 +9,4 @@ data class TsOptions( /** `null` enables every built-in model; an empty set disables all models. */ val enabledUnknownCallModelIds: Set? = null, val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, - val unknownCallFallbackOverrides: Map = emptyMap(), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index c8933340f..d5d8681d6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -1,6 +1,5 @@ package org.usvm.machine.call -import org.jacodb.ets.model.EtsClassSignature import org.usvm.api.makeFreshUnknownCallResult import org.usvm.api.mockMethodCall import org.usvm.api.setMockMethodCallResult @@ -27,11 +26,8 @@ enum class TsResidualCallPolicy { class TsModelUnknownCallDispatcher( private val models: TsUnknownCallModelCatalog, private val fallback: TsResidualCallPolicy, - fallbackOverrides: Map = emptyMap(), private val observer: TsInterpreterObserver? = null, ) : TsUnknownCallModelDispatcher { - private val fallbackOverrides = fallbackOverrides.toMap() - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { val application = scope.calcOnState { this@TsModelUnknownCallDispatcher.models.apply(this, call) @@ -47,10 +43,9 @@ class TsModelUnknownCallDispatcher( scope: TsStepScope, call: TsUnknownCall, ): TsUnknownCallOutcome { - val policy = fallbackFor(call) - val decision = TsUnknownCallDecision.ResidualFallback(policy) + val decision = TsUnknownCallDecision.ResidualFallback(fallback) - when (policy) { + when (fallback) { TsResidualCallPolicy.STOP_PATH -> { val falseExpr = scope.calcOnState { ctx.falseExpr } scope.assert(falseExpr) @@ -72,18 +67,17 @@ class TsModelUnknownCallDispatcher( application: TsUnknownCallModelApplication.Applied, ): TsUnknownCallOutcome { val residualGuard = application.execution.residualGuard - val residualPolicy = fallbackFor(call) // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone // inherits both the constraints and their solver models. val freshResidualResult = if ( - residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { makeFreshUnknownCallResult(scope, call.resultType) } else { null } val stoppedResidualIsSatisfiable = residualGuard != null && - residualPolicy == TsResidualCallPolicy.STOP_PATH && + fallback == TsResidualCallPolicy.STOP_PATH && scope.checkSat(residualGuard) != null var modelApplied = false @@ -106,7 +100,7 @@ class TsModelUnknownCallDispatcher( ) }.toMutableList() - if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { guardedStateChanges += residualGuard to { setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) newStmt(call.callSite) @@ -160,9 +154,6 @@ class TsModelUnknownCallDispatcher( } } - private fun fallbackFor(call: TsUnknownCall): TsResidualCallPolicy = - fallbackOverrides[call.callee.enclosingClass] ?: fallback - private fun event( call: TsUnknownCall, decision: TsUnknownCallDecision, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index cf86b6041..cd80fa71b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -36,7 +36,7 @@ internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { val length = state.memory.read(lengthLValue) val zero = mkBv(0) val emptyGuard = mkEq(length, zero) - val nonEmptyGuard = mkBvSignedLessExpr(zero, length) + val nonEmptyGuard = mkNot(emptyGuard) val newLength = mkBvSubExpr(length, mkBv(1)) val firstElementLValue = mkArrayIndexLValue( sort = input.elementSort, @@ -67,10 +67,7 @@ internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { }, ) - TsUnknownCallModelExecution( - successors = listOf(emptySuccessor, nonEmptySuccessor), - residualGuard = mkNot(mkOr(emptyGuard, nonEmptyGuard)), - ) + TsUnknownCallModelExecution(successors = listOf(emptySuccessor, nonEmptySuccessor)) } private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayShiftInput? = with(state.ctx) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index a0d16c22b..32ac35267 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -69,6 +69,20 @@ class TsArrayShiftIntrinsicModelTest { assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) } + @Test + fun `empty and non empty guards are complementary`() { + val state = analyzeStates(methodName = "unknownValue").single() + val symbolicArray = state.makeSymbolicRefUntyped() + + val application = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(symbolicArray)) + val execution = assertNotNull(application) + val (emptyArray, nonEmptyArray) = execution.successors + + assertEquals(2, execution.successors.size) + assertEquals(state.ctx.mkNot(emptyArray.guard), nonEmptyArray.guard) + assertNull(execution.residualGuard) + } + @Test fun `symbolic unknown array uses residual fallback`() { assertUsesResidualFallback(methodName = "symbolicUnknownArray") 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 9a29604ea..81ae7a03b 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 @@ -241,7 +241,6 @@ class TsUnknownCallDispatcherTest { fun `TsOptions configures one fallback without profiles`() { assertEquals(TsResidualCallPolicy.STOP_PATH, TsOptions().unknownCallFallback) assertNull(TsOptions().enabledUnknownCallModelIds) - assertTrue(TsOptions().unknownCallFallbackOverrides.isEmpty()) assertFalse(reachesReturn("declaredMethodWithoutBodyContinues")) assertTrue( @@ -252,28 +251,6 @@ class TsUnknownCallDispatcherTest { ) } - @Test - fun `explicit family override replaces the default residual fallback`() { - val family = method(fullScene, "declaredMethodWithoutBodyContinues") - .cfg - .stmts - .mapNotNull { it.callExpr } - .single { it.callee.name == "external" } - .callee - .enclosingClass - - assertTrue( - reachesReturn( - "declaredMethodWithoutBodyContinues", - tsOptions = TsOptions( - unknownCallFallbackOverrides = mapOf( - family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ), - ), - ) - ) - } - @Test fun `fresh symbolic return uses the source call result type`() { val dispatcher = RecordingResultSortDispatcher( From eba8e4e69bab023a99d09371467796ac56b9e3f7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 8 Sep 2026 16:27:35 +0300 Subject: [PATCH 8/8] [TS Calls] Support unresolved Array.shift elements --- usvm-ts/UNKNOWN_CALL_MODELS.md | 15 +- .../usvm/machine/call/TsUnknownCallModel.kt | 6 + .../call/TsUnknownCallModelDispatcher.kt | 36 +++- .../intrinsic/TsArrayShiftIntrinsicModel.kt | 190 ++++++++++++++++-- .../kotlin/org/usvm/machine/expr/ReadArray.kt | 52 +++-- .../org/usvm/machine/types/FakeExprUtil.kt | 13 ++ .../usvm/machine/types/TsUnresolvedValue.kt | 13 ++ .../call/TsArrayShiftIntrinsicModelTest.kt | 103 +++++++++- .../resources/models/ArrayShiftIntrinsic.ts | 38 +++- 9 files changed, 408 insertions(+), 58 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 2e2c6182e..70dbb9c4d 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -60,10 +60,11 @@ The built-in catalog currently contains one model: | ID | Implementation | Accepted calls | | --- | --- | --- | -| `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array whose element sort is known. | +| `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. | -An `any`/unknown receiver, a fake-value wrapper, a non-array receiver, and an array whose element sort is unresolved do -not become applicable merely because the method is named `shift`; they use fallback. +An `any`/unknown receiver, a fake-value wrapper, and a non-array receiver do not become applicable merely because the +method is named `shift`; they use fallback. A definitely-array receiver with an unresolved element sort remains +applicable and uses the fake-value representation described below. ### `unknownCallFallback` @@ -138,7 +139,7 @@ The target identifies a call family. State-dependent checks, such as the receive The built-in array target intentionally combines the method name with `PARTIAL_APPROXIMATION` instead of a class name. That failure reason is emitted only after the regular approximation path has classified the receiver as an `EtsArrayType`. Calls on `any`/unknown receivers reach another failure reason and cannot match this target. The model -still validates the resolved receiver and its element sort before changing memory. +still validates the resolved receiver and array shape before changing memory. ## Applicability and residual states @@ -171,8 +172,10 @@ model on every call. An intrinsic directly builds guarded successors and symbolic-memory operations in Kotlin. Use it only for an operation that TypeScript cannot express without losing symbolic efficiency or correctness. -`Array.shift` is the built-in example because shifting a symbolic array is naturally represented by one -`memory.memcpy` operation. +`Array.shift` is the built-in example because shifting a symbolic array is naturally represented by symbolic-memory +`memcpy` operations. A resolved element sort uses one array region. A symbolic array with an unresolved element sort +uses the boolean, number, and address regions that back a fake value; its removed element is materialized before +forking so the exactly-one type constraint and updated solver models are inherited by every successor. Good intrinsic candidates include: 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 923236737..240f4f003 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 @@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsType import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedValue /** Declaratively identifies the calls handled by one semantic model. */ data class TsUnknownCallTarget( @@ -55,6 +56,11 @@ sealed interface TsUnknownCallModelCompletion { val result: TsState.() -> UExpr<*>, ) : TsUnknownCallModelCompletion + /** Produces a normal fake-wrapped result for a value whose runtime kind is unresolved. */ + class Unresolved( + val value: TsUnresolvedValue, + ) : TsUnknownCallModelCompletion + /** Produces an exceptional result and its TypeScript type on the selected successor state. */ class Exceptional( val exception: TsState.() -> Pair, EtsType>, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index d5d8681d6..5a524e6de 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -1,5 +1,6 @@ package org.usvm.machine.call +import org.usvm.UExpr import org.usvm.api.makeFreshUnknownCallResult import org.usvm.api.mockMethodCall import org.usvm.api.setMockMethodCallResult @@ -8,6 +9,7 @@ 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.machine.types.mkFakeValue /** The externally observable effect of an unknown-call decision. */ enum class TsUnknownCallOutcome { @@ -83,11 +85,22 @@ class TsModelUnknownCallDispatcher( var modelApplied = false var modelEventReported = false var freshResidualApplied = false - val guardedStateChanges = application.execution.successors.map { successor -> + // Materializing an unresolved result adds its exactly-one constraint. Do it before forking so every + // successor that uses the wrapper inherits both the constraint and the refreshed solver models. + val preparedUnresolvedResults = application.execution.successors.map { successor -> + val completion = successor.completion as? TsUnknownCallModelCompletion.Unresolved + ?: return@map null + + scope.calcOnState { + mkFakeValue(scope = scope, value = completion.value) + } + } + val guardedStateChanges = application.execution.successors.mapIndexed { index, successor -> successor.guard to modelStateChange( call = call, modelId = application.modelId, successor = successor, + preparedUnresolvedResult = preparedUnresolvedResults[index], onApplied = { modelApplied = true if (modelEventReported) { @@ -106,18 +119,18 @@ class TsModelUnknownCallDispatcher( newStmt(call.callSite) freshResidualApplied = true - observer?.onUnknownCallSafely( - event(call, TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN)) - ) + val decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) + val fallbackEvent = event(call, decision) + observer?.onUnknownCallSafely(fallbackEvent) } } scope.forkMulti(guardedStateChanges) if (stoppedResidualIsSatisfiable) { - observer?.onUnknownCallSafely( - event(call, TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH)) - ) + val decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH) + val fallbackEvent = event(call, decision) + observer?.onUnknownCallSafely(fallbackEvent) } return when { @@ -132,6 +145,7 @@ class TsModelUnknownCallDispatcher( call: TsUnknownCall, modelId: String, successor: TsUnknownCallModelSuccessor, + preparedUnresolvedResult: UExpr<*>?, onApplied: () -> Boolean, ): TsState.() -> Unit = { successor.applyStateChanges(this) @@ -143,6 +157,14 @@ class TsModelUnknownCallDispatcher( newStmt(call.callSite) } + is TsUnknownCallModelCompletion.Unresolved -> { + val result = requireNotNull(preparedUnresolvedResult) { + "Unresolved semantic-model result was not materialized" + } + methodResult = TsMethodResult.Success.MockedCall(result, call.callee) + newStmt(call.callSite) + } + is TsUnknownCallModelCompletion.Exceptional -> { val (exception, type) = completion.exception(this) methodResult = TsMethodResult.TsException(exception, type) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index cd80fa71b..5c8608af1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -2,11 +2,17 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsUnknownType import org.usvm.UAddressSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.USort import org.usvm.api.memcpy import org.usvm.api.typeStreamOf +import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.machine.TsSizeSort import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel @@ -15,7 +21,10 @@ import org.usvm.machine.call.TsUnknownCallModelExecution import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.readSymbolicUnresolvedArrayElement import org.usvm.machine.state.TsState +import org.usvm.machine.types.findMaterializedFakeValue +import org.usvm.sizeSort import org.usvm.types.singleOrNull import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue @@ -35,16 +44,11 @@ internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType) val length = state.memory.read(lengthLValue) val zero = mkBv(0) + val one = mkBv(1) val emptyGuard = mkEq(length, zero) val nonEmptyGuard = mkNot(emptyGuard) - val newLength = mkBvSubExpr(length, mkBv(1)) - val firstElementLValue = mkArrayIndexLValue( - sort = input.elementSort, - ref = input.array, - index = zero, - type = input.arrayType, - ) - val firstElement = state.memory.read(firstElementLValue) + val newLength = mkBvSubExpr(length, one) + val firstElementCompletion = state.firstElementCompletion(input, zero) val emptySuccessor = TsUnknownCallModelSuccessor( guard = emptyGuard, @@ -52,17 +56,9 @@ internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { ) val nonEmptySuccessor = TsUnknownCallModelSuccessor( guard = nonEmptyGuard, - completion = TsUnknownCallModelCompletion.Normal { firstElement }, + completion = firstElementCompletion, applyStateChanges = { - memory.memcpy( - srcRef = input.array, - dstRef = input.array, - type = input.arrayType, - elementSort = input.elementSort, - fromSrc = mkBv(1), - fromDst = zero, - length = newLength, - ) + shiftElements(input, fromSrc = one, fromDst = zero, length = newLength) memory.write(lengthLValue, newLength, guard = trueExpr) }, ) @@ -90,11 +86,163 @@ internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel { } val elementSort = typeToSort(arrayType.elementType) - if (elementSort is TsUnresolvedSort) { - return@with null + ArrayShiftInput(array, arrayType, elementSort) + } + + private fun TsState.firstElementCompletion( + input: ArrayShiftInput, + index: UExpr, + ): TsUnknownCallModelCompletion = with(ctx) { + if (input.elementSort !is TsUnresolvedSort) { + val firstElementLValue = mkArrayIndexLValue( + sort = input.elementSort, + ref = input.array, + index = index, + type = input.arrayType, + ) + val firstElement = memory.read(firstElementLValue) + + return@with TsUnknownCallModelCompletion.Normal { firstElement } } - ArrayShiftInput(array, arrayType, elementSort) + if (input.array is UConcreteHeapRef) { + val firstElementLValue = mkArrayIndexLValue( + sort = addressSort, + ref = input.array, + index = index, + type = input.arrayType, + ) + val firstElement = memory.read(firstElementLValue) + + return@with TsUnknownCallModelCompletion.Normal { + check(firstElement.isFakeObject()) { + "Expected fake object in concrete array with unresolved element type, got: $firstElement" + } + firstElement + } + } + + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val firstElementLValue = mkArrayIndexLValue(addressSort, input.array, index, unknownArrayType) + val materializedFirstElement = findMaterializedFakeValue(firstElementLValue) + if (materializedFirstElement != null) { + return@with TsUnknownCallModelCompletion.Normal { materializedFirstElement } + } + + val firstElement = readSymbolicUnresolvedArrayElement(input.array, index) + TsUnknownCallModelCompletion.Unresolved(firstElement) + } + + private fun TsState.shiftElements( + input: ArrayShiftInput, + fromSrc: UExpr, + fromDst: UExpr, + length: UExpr, + ) = with(ctx) { + if (input.elementSort !is TsUnresolvedSort) { + copyArrayRegion( + input = input, + arrayType = input.arrayType, + elementSort = input.elementSort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + return@with + } + + if (input.array is UConcreteHeapRef) { + copyArrayRegion( + input = input, + arrayType = input.arrayType, + elementSort = addressSort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + shiftMaterializedFakeValues(input) + return@with + } + + copyArrayRegion( + input = input, + arrayType = EtsArrayType(EtsBooleanType, dimensions = 1), + elementSort = boolSort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + copyArrayRegion( + input = input, + arrayType = EtsArrayType(EtsNumberType, dimensions = 1), + elementSort = fp64Sort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + copyArrayRegion( + input = input, + arrayType = EtsArrayType(EtsUnknownType, dimensions = 1), + elementSort = addressSort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + shiftMaterializedFakeValues(input) + } + + private fun TsState.copyArrayRegion( + input: ArrayShiftInput, + arrayType: EtsArrayType, + elementSort: USort, + fromSrc: UExpr, + fromDst: UExpr, + length: UExpr, + ) { + memory.memcpy( + srcRef = input.array, + dstRef = input.array, + type = ctx.arrayDescriptorOf(arrayType), + elementSort = elementSort, + fromSrc = fromSrc, + fromDst = fromDst, + length = length, + ) + } + + private fun TsState.shiftMaterializedFakeValues(input: ArrayShiftInput) = with(ctx) { + val arrayDescriptor = if (input.array is UConcreteHeapRef) { + arrayDescriptorOf(input.arrayType) + } else { + arrayDescriptorOf(EtsArrayType(EtsUnknownType, dimensions = 1)) + } + val zero = mkBv(0) + val one = mkBv(1) + val shiftedValues = lValuesToAllocatedFakeObjects.mapNotNull { (lValue, fakeValue) -> + if ( + lValue !is UArrayIndexLValue<*, *, *> || + lValue.ref != input.array || + lValue.arrayType != arrayDescriptor + ) { + return@mapNotNull null + } + + val sourceIndex = lValue.index.asExpr(sizeSort) + if (sourceIndex == zero) { + return@mapNotNull null + } + + val destinationIndex = mkBvSubExpr(sourceIndex, one) + val destinationLValue = UArrayIndexLValue( + addressSort, + input.array, + destinationIndex, + arrayDescriptor, + ) + destinationLValue to fakeValue + } + + lValuesToAllocatedFakeObjects += shiftedValues } private class ArrayShiftInput( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 684c8902d..3b097ad1a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -15,6 +15,9 @@ import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.findMaterializedFakeValue import org.usvm.machine.types.mkFakeValue import org.usvm.sizeSort import org.usvm.types.first @@ -127,28 +130,49 @@ fun TsContext.readArray( // that can hold boolean, number, and reference values. // We read all three types from the array and combine them into a fake object. return scope.calcOnState { - val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) - val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType) - val bool = memory.read(boolLValue) - - val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) - val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType) - val fp = memory.read(fpLValue) - val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType) - val ref = memory.read(refLValue) + val materializedValue = findMaterializedFakeValue(refLValue) + if (materializedValue != null) { + return@calcOnState materializedValue + } + + val value = readSymbolicUnresolvedArrayElement(array, index) - // If the read reference is already a fake object, we can return it directly. - // Otherwise, we need to create a new fake object and write it back to the memory. + // Reuse an existing fake object or materialize a flat wrapper for all three payloads. // TODO: Think about the type constraint to get a consistent array resolution later - if (ref.isFakeObject()) { - ref + if (value.refValue.isFakeObject()) { + value.refValue } else { - val fakeObj = mkFakeValue(scope, bool, fp, ref) + val fakeObj = mkFakeValue(scope = scope, value = value) lValuesToAllocatedFakeObjects += refLValue to fakeObj memory.write(refLValue, fakeObj, guard = trueExpr) fakeObj } } } + +internal fun TsState.readSymbolicUnresolvedArrayElement( + array: UHeapRef, + index: UExpr, +): TsUnresolvedValue = with(ctx) { + check(array !is UConcreteHeapRef) { "A concrete unresolved array stores fake-value wrappers directly" } + + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType) + val boolValue = memory.read(boolLValue) + + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType) + val fpValue = memory.read(fpLValue) + + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType) + val refValue = memory.read(refLValue) + + TsUnresolvedValue( + boolValue = boolValue, + fpValue = fpValue, + refValue = refValue, + ) +} 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 59fa51a6b..3c75494d9 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,9 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsState import org.usvm.memory.ULValue +internal fun TsState.findMaterializedFakeValue(lValue: ULValue<*, *>): UConcreteHeapRef? = + lValuesToAllocatedFakeObjects.lastOrNull { (recordedLValue) -> recordedLValue == lValue }?.second + /** * Creates a fresh synthetic wrapper for a TypeScript value with a not necessarily known runtime kind. * @@ -84,6 +87,16 @@ fun TsState.mkFakeValue( fakeValueRef } +fun TsState.mkFakeValue( + scope: TsStepScope?, + value: TsUnresolvedValue, +): UConcreteHeapRef = mkFakeValue( + scope = scope, + boolValue = value.boolValue, + fpValue = value.fpValue, + refValue = value.refValue, +) + fun TsState.extractValue( value: UExpr, sort: T, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt new file mode 100644 index 000000000..7d7f7bb65 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt @@ -0,0 +1,13 @@ +package org.usvm.machine.types + +import io.ksmt.sort.KFp64Sort +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef + +/** The three backing payloads of a TypeScript value whose active runtime kind is not resolved yet. */ +data class TsUnresolvedValue( + val boolValue: UBoolExpr, + val fpValue: UExpr, + val refValue: UHeapRef, +) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt index 32ac35267..7b8bdd69a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -1,8 +1,12 @@ package org.usvm.machine.call +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsInstanceCallExpr import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.loadEtsFileAutoConvert @@ -22,6 +26,8 @@ import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.util.TsTestResolver import org.usvm.util.getResourcePath +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertIs @@ -55,7 +61,7 @@ class TsArrayShiftIntrinsicModelTest { } @Test - fun `reference array preserves removed element alias`() { + fun `reference array preserves removed element alias and moves tail`() { val result = analyze(methodName = "aliasedElement") assertEquals(42.0, assertIs(result.values.single()).number) @@ -84,8 +90,92 @@ class TsArrayShiftIntrinsicModelTest { } @Test - fun `symbolic unknown array uses residual fallback`() { - assertUsesResidualFallback(methodName = "symbolicUnknownArray") + fun `symbolic unknown array preserves removed element and moves all value regions`() { + val result = analyze(methodName = "symbolicUnknownArray") + val reachesExpectedResult = result.values.any { value -> + (value as? TsTestValue.TsNumber)?.number == 47.0 + } + + assertTrue(reachesExpectedResult) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `symbolic unknown array copies boolean number and address regions`() { + val state = analyzeStates(methodName = "unknownValue").single() + val symbolicArray = state.makeSymbolicRefUntyped() + + with(state.ctx) { + val zero = mkBv(0) + val one = mkBv(1) + val boolValue = trueExpr + val fpValue = mkFp64(17.0) + val refValue = state.makeSymbolicRefUntyped() + + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + + val lengthLValue = mkArrayLengthLValue(symbolicArray, unknownArrayType) + state.memory.write(lengthLValue, mkBv(2), guard = trueExpr) + state.memory.write( + mkArrayIndexLValue(boolSort, symbolicArray, one, boolArrayType), + boolValue, + guard = trueExpr, + ) + state.memory.write( + mkArrayIndexLValue(fp64Sort, symbolicArray, one, numberArrayType), + fpValue, + guard = trueExpr, + ) + state.memory.write( + mkArrayIndexLValue(addressSort, symbolicArray, one, unknownArrayType), + refValue, + guard = trueExpr, + ) + + val execution = assertNotNull( + TsArrayShiftIntrinsicModel.apply( + state, + arrayShiftCall(symbolicArray, methodName = "symbolicUnknownArray"), + ) + ) + val nonEmptySuccessor = execution.successors.last() + assertIs(nonEmptySuccessor.completion) + + nonEmptySuccessor.applyStateChanges(state) + + val shiftedBoolValue = state.memory.read( + mkArrayIndexLValue(boolSort, symbolicArray, zero, boolArrayType) + ) + val shiftedFpValue = state.memory.read( + mkArrayIndexLValue(fp64Sort, symbolicArray, zero, numberArrayType) + ) + val shiftedRefValue = state.memory.read( + mkArrayIndexLValue(addressSort, symbolicArray, zero, unknownArrayType) + ) + + assertEquals(boolValue, shiftedBoolValue) + assertEquals(fpValue, shiftedFpValue) + assertEquals(refValue, shiftedRefValue) + assertEquals(one, state.memory.read(lengthLValue)) + } + } + + @Test + fun `concrete unknown array shifts fake wrapped values`() { + val result = analyze(methodName = "mixedUnknownArray") + + assertEquals(49.0, assertIs(result.values.single()).number) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `empty concrete unknown array returns undefined`() { + val result = analyze(methodName = "emptyUnknownArray") + + assertIs(result.values.single()) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) } @Test @@ -185,8 +275,11 @@ class TsArrayShiftIntrinsicModelTest { return fakeReceiver } - private fun arrayShiftCall(resolvedReceiver: UExpr<*>): TsUnknownCall { - val callSite = method("nonEmptyArray").cfg.stmts.single { stmt -> + private fun arrayShiftCall( + resolvedReceiver: UExpr<*>, + methodName: String = "nonEmptyArray", + ): TsUnknownCall { + val callSite = method(methodName).cfg.stmts.single { stmt -> stmt.callExpr?.callee?.name == "shift" } val sourceCall = assertIs(assertNotNull(callSite.callExpr)) diff --git a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts index b6fbaee65..52f114978 100644 --- a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts +++ b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts @@ -19,9 +19,10 @@ export class ArrayShiftIntrinsic { } aliasedElement(): number { - const element = new ArrayElement(); - const values: ArrayElement[] = [element]; - if (values.shift() === element) { + const first = new ArrayElement(); + const second = new ArrayElement(); + const values: ArrayElement[] = [first, second]; + if (values.shift() === first && values[0] === second && values.length === 1) { return 42; } @@ -34,8 +35,35 @@ export class ArrayShiftIntrinsic { } symbolicUnknownArray(values: any[]): number { - values.shift(); - return 47; + if (values.length < 2) { + return 0; + } + + const oldLength = values.length; + const firstType = typeof values[0]; + const secondType = typeof values[1]; + const removedType = typeof values.shift(); + if (removedType === firstType && typeof values[0] === secondType && values.length === oldLength - 1) { + return 47; + } + + return 1; + } + + mixedUnknownArray(): number { + const element = new ArrayElement(); + const values: any[] = [10, true, element]; + const removed = values.shift(); + if (removed === 10 && values[0] === true && values[1] === element && values.length === 2) { + return 49; + } + + return 0; + } + + emptyUnknownArray(): any { + const values: any[] = []; + return values.shift(); } shiftWithArguments(): number {