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..7ab3d97d9 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( @@ -15,28 +16,38 @@ fun mockMethodCall( method: EtsMethodSignature, resultType: EtsType = method.returnType, ) { + val result = makeFreshUnknownCallResult(scope, resultType) + scope.doWithState { - val result: UExpr<*> - if (resultType is EtsVoidType) { - result = ctx.mkUndefinedValue() - } else { - val sort = ctx.typeToSort(resultType) - result = when (sort) { - is UAddressSort -> makeSymbolicRefUntyped() - - is TsUnresolvedSort -> scope.calcOnState { - mkFakeValue( - scope = scope, - boolValue = makeSymbolicPrimitive(ctx.boolSort), - fpValue = makeSymbolicPrimitive(ctx.fp64Sort), - refValue = makeSymbolicRefUntyped(), - ) - } - - else -> makeSymbolicPrimitive(sort) - } - } - - methodResult = TsMethodResult.Success.MockedCall(result, method) + setMockMethodCallResult(method, result) + } +} + +/** Stores a prepared opaque result on this state without applying callee effects or exceptions. */ +internal fun TsState.setMockMethodCallResult( + method: EtsMethodSignature, + result: UExpr<*>, +) { + methodResult = TsMethodResult.Success.MockedCall(result, method) +} + +/** 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() + + when (val sort = ctx.typeToSort(resultType)) { + is UAddressSort -> makeSymbolicRefUntyped() + + is TsUnresolvedSort -> mkFakeValue( + scope, + boolValue = makeSymbolicPrimitive(ctx.boolSort), + fpValue = makeSymbolicPrimitive(ctx.fp64Sort), + refValue = makeSymbolicRefUntyped(), + ) + + else -> makeSymbolicPrimitive(sort) } } 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/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 3d6b394f3..eca353f53 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( @@ -62,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/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/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/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt index bb99b6ec9..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 @@ -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") + } } } } @@ -152,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, ) @@ -166,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/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt new file mode 100644 index 000000000..9566b54a0 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -0,0 +1,117 @@ +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. The dispatcher validates disjointness and coverage before + * applying any successor. + */ +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..45471e1e8 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistry.kt @@ -0,0 +1,162 @@ +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/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt index 66e4eeb1f..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 @@ -1,10 +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 { @@ -61,34 +72,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,43 +83,46 @@ 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, + 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(this, call) + } + return when (application) { + is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) - TsUnknownCallModelApplication.NotApplicable -> { - TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE - } - } - } + 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 = call, - outcome = outcome, + call, + outcome, decision = TsUnknownCallDecision.ResidualFallback( - policy = residualPolicy, - reason = residualReason, + residualPolicy, + reason, ), ) when (residualPolicy) { @@ -152,6 +141,183 @@ class TsProfileUnknownCallDispatcher( 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, @@ -165,3 +331,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/call/intrinsic/TsArrayPopIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt new file mode 100644 index 000000000..e82be0e6b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayPopIntrinsicModel.kt @@ -0,0 +1,130 @@ +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/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/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 0060b4762..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 @@ -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,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return from(handleArrayPop(expr, instanceType, elementSort)) + return handleArrayPopCall(expr, instanceType, elementSort, instance) } // Handle `Array.fill() method calls @@ -159,6 +163,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, + expr, + 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/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/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, 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..ea1dd94d4 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayPopIntrinsicModelTest.kt @@ -0,0 +1,220 @@ +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.junit.jupiter.api.Disabled +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class 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 `allocated reference array uses residual fallback`() { + assertUsesResidualFallback(methodName = "aliasedElement") + } + + @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 + fun `disabled model sends pop to configured residual fallback`() { + val enabledModelIds = mutableSetOf("ts.array.pop") + val selection = TsUnknownCallModelSelection(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 assertUsesResidualFallback(methodName: String) { + val result = analyze(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 + .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..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 @@ -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,18 +19,19 @@ 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.isTrue import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine 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 +147,119 @@ 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 `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() + 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( @@ -524,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() @@ -577,27 +698,124 @@ 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 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) + 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 +876,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/TsUnknownCallExecutionGuardValidationTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt new file mode 100644 index 000000000..f27312644 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallExecutionGuardValidationTest.kt @@ -0,0 +1,206 @@ +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/TsUnknownCallModelRegistryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt new file mode 100644 index 000000000..f45624784 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelRegistryTest.kt @@ -0,0 +1,152 @@ +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 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) + } +} diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index c78d4027f..7b80de0eb 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -18,6 +18,15 @@ 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; +} + class KnownReceiver { known(): number { return 1; @@ -68,6 +77,21 @@ class CallFallbackBaseline { return ExternalBoolean.convert(value); } + modeledUnknownCallReturnsAlias(receiver: ExternalReceiver): number { + if (ExternalModeledCall.identity(receiver) === receiver) { + return 122; + } + return 0; + } + + modeledUnknownCallThrows(): number { + 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 new file mode 100644 index 000000000..0258b3974 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayPopIntrinsic.ts @@ -0,0 +1,75 @@ +// @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; + } +}