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; + } +}