diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md new file mode 100644 index 000000000..f598c5c99 --- /dev/null +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -0,0 +1,275 @@ +# TypeScript unknown-call models + +This document describes the semantic-model path used when the normal TypeScript interpreter cannot execute a call. + +## Mental model + +There are only three stages: + +1. The regular interpreter and existing compatibility approximations try to execute the call. +2. If execution cannot continue, `TsUnknownCallModelCatalog` selects one enabled semantic model by its target. +3. If no model handles the call or a model leaves a residual state, the configured fallback is applied. + +```text +normal execution + | + | cannot execute + v +enabled model with matching target? -- no --> fallback + | + yes + v +model accepts these inputs? -------- no --> fallback + | + yes + v +model successors + optional residual ----> residual uses fallback +``` + +The catalog contains model objects directly. There are no implementation-kind values, backend registrations, or +separate descriptor and implementation IDs. + +## Configuration + +Unknown-call behavior is configured directly in `TsOptions`: + +```kotlin +TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf("ts.array.shift")), + unknownCallFallback = TsResidualCallPolicy.STOP_PATH, +) +``` + +### `unknownCallModelSelection` + +This is the only model-selection setting. + +| Value | Meaning | +| --- | --- | +| `TsUnknownCallModelSelection.All` | Enable every built-in model. This is the default. | +| `TsUnknownCallModelSelection.Only(emptySet())` | Disable every built-in model. | +| `TsUnknownCallModelSelection.Only(setOf("id", ...))` | Enable exactly the listed built-in model IDs. | + +Unknown IDs are rejected when the machine creates its immutable per-run catalog. The selected models are captured at that +point, so later mutations of the selection set cannot change an active run. + +Use the model's `id`, for example `ts.array.shift`. A target method name, class name, source filename, or fingerprint is +not a model ID. + +Built-ins are `object` implementations of the sealed `TsBuiltInUnknownCallModel` interface in the +`org.usvm.machine.call.intrinsic` package. Kotlin's sealed-subclass metadata discovers them automatically; adding a +model requires no manual registry entry. Discovery and the default catalog are computed once. + +The built-in catalog currently contains one model: + +| ID | Implementation | Accepted calls | +| --- | --- | --- | +| `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. | + +The common instance-call pipeline splits fake-value wrappers and conditional references under their runtime-kind +and branch guards before selecting an approximation or resolving a method. A wrapped array can therefore use the +model, including through an `any` alias. An unknown or non-array receiver does not become an array merely because +the method is named `shift`. A definitely-array receiver with an unresolved element sort remains applicable and uses +the fake-value representation described below. + +### `unknownCallFallback` + +The fallback is applied when: + +- no enabled model target matches the call; +- the selected model returns `null` because it cannot safely handle the concrete inputs; +- a model returns a satisfiable `residualGuard`. + +The available policies are: + +| Policy | Behavior | +| --- | --- | +| `STOP_PATH` | Prune the unsupported state. This is the default. | +| `FRESH_SYMBOLIC_RETURN` | Continue with a fresh symbolic result and ignore unknown side effects and exceptions. | + +`FRESH_SYMBOLIC_RETURN` is deliberately imprecise. Use it only when opaque continuation is preferable to pruning. + +## Model identity and target + +Every model implements `TsUnknownCallModel`: + +```kotlin +interface TsUnknownCallModel { + val id: String + val target: TsUnknownCallTarget + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? +} +``` + +### Choosing an ID + +Use a stable semantic name: + +```text +..[.] +``` + +Examples: + +- `ts.array.shift` +- `ts.array.pop` +- `node.buffer.copy` + +The ID is used for configuration, observer events, and catalog fingerprints. Do not include: + +- an implementation mechanism such as `intrinsic`; +- a hash; +- a version number; +- a supported-domain label. + +Keep the same ID if an equivalent model is later reimplemented by another mechanism. + +### Choosing a target + +`TsUnknownCallTarget` matches stable call metadata declaratively: + +```kotlin +TsUnknownCallTarget( + methodName = "shift", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, +) +``` + +Only `methodName` is required. Add `enclosingClassName` or `failureReason` when the method name alone is too broad. +The catalog indexes method names, failure reasons, and enclosing classes. Overlapping enabled targets fail while +building that index; lookup returns either one model or no match, and never hides ambiguity. Catalog order is never +a priority rule. IDs and their SHA-256 fingerprint are computed once; byte-length prefixes distinguish ID sequences +such as `["ab", "c"]` and `["a", "bc"]`. + +The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in +`apply`. + +The built-in array target intentionally combines the method name with `PARTIAL_APPROXIMATION` instead of a class name. +That failure reason is emitted only after the regular approximation path has classified the receiver as an +`EtsArrayType` using the normalized receiver's storage type. An `any` alias of a known array can satisfy that check; +a receiver without array-type evidence cannot. The model still validates the resolved receiver and array shape +before changing memory. + +## Applicability and residual states + +There is no separate `EXACT` or `PARTIAL` flag. + +- `apply(...) == null` means the model rejects the complete call. The dispatcher uses fallback. +- `residualGuard == null` means the returned execution completely handles the accepted state. +- A non-null `residualGuard` sends precisely that symbolic subdomain to fallback. + +For example, a model may handle an array receiver under `isArray` and leave `!isArray` as residual: + +```kotlin +TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = isArray, + completion = completion, + ), + ), + residualGuard = ctx.mkNot(isArray), +) +``` + +Model authors are responsible for making successor guards and the residual guard disjoint and exhaustive. This +property belongs in focused model tests; the dispatcher does not invoke the solver a second time merely to validate a +model on every call. + +## When to write an intrinsic + +An intrinsic directly builds guarded successors and symbolic-memory operations in Kotlin. Use it only for an operation +that TypeScript cannot express without losing symbolic efficiency or correctness. + +`Array.shift` is the built-in example because shifting a symbolic array is naturally represented by symbolic-memory +`memcpy` operations. A resolved element sort uses one canonical array region. Unresolved elements use three +payload regions (boolean, number, and address) and two boolean kind selectors. Reference kind is derived as +`!(booleanKind || numberKind)`; the exactly-one constraint excludes both primitive selectors being true. Default +allocated slots therefore represent references, including undefined. `Unknown[]` names the canonical reference +storage region, not a claim that every TypeScript array has unresolved elements. + +`copyArrayElements` moves all five regions for unresolved arrays, including allocated arrays created by `slice` or +`concat`. `reverse` applies the same index permutation to every region. Scalar writes store complete fake wrappers +in the reference region, overriding older payloads and selectors. Reads and test reconstruction use the same reader. +The removed `shift` element is materialized before forking so its kind constraint and updated solver models are +inherited by every successor. + +`concat` handles arrays with compatible storage sorts and scalar elements that fit the destination. Calls requiring +conversion between storage sorts, or runtime spreading of a fake/untyped argument, use normal call resolution and +fallback. Existing `fill` bounds and the finite `reverse`/`fill` caps remain approximation limitations. +Array reads, writes, length access, and `shift` use the storage type known to symbolic memory when it is unique. +Widening a local from `number[]` to `any[]` therefore keeps the same element and length regions. + +Good intrinsic candidates include: + +- bulk symbolic-memory copy or fill; +- symbolic collection primitives; +- solver operations unavailable in the modeled language; +- type-system operations that cannot be represented faithfully by ordinary code. + +Do not write an intrinsic merely because a library method is stateful. + +## Source-model migration + +A source model uses the same `TsUnknownCallModel` object and the same ID, target, successor, and residual contract. +The source-model work in PR #380 should extend a successor completion with the EtsIR entry point and resolved inputs, +make the model's EtsIR files visible in the analysis scene, and enter that method through the regular interpreter. +Receiver binding, arguments, returns, exceptions, heap changes, aliases, and nested calls then use normal interpreter +semantics. They must not be reimplemented in a source-specific dispatcher or backend registry. + +The model checks its supported domain before entering EtsIR. An unsupported call returns `null`; a guarded supported +subdomain uses the complementary residual guard and the same configured fallback. Recursive redirection is prevented +by tracking the active model ID in execution state, not by creating a second catalog. + +`Array.pop` is the source-model example. Its TypeScript body uses indexing and `length`; it must not call `pop` again. +The existing `Array.shift` intrinsic remains the example for engine-only symbolic-memory `memcpy`. + +## Dynamic receivers + +A method name does not prove the receiver type. In particular, `value.shift()` may call a user-defined property rather +than `Array.prototype.shift`. + +Instance calls share receiver normalization before built-in approximations and ordinary method lookup. It reuses +`extractValue` to select a fake payload together with its kind constraint and `splitUHeapRef` to retain conditional +reference guards. Each feasible alternative continues through the existing virtual-call statement. This preserves +supported primitive calls such as `valueOf` and the existing `toString` approximation, while null and undefined +receivers take the property-access exception path. Other primitive calls use `NON_REFERENCE_RECEIVER` fallback. +Receiver normalization does not make the existing built-in approximations exact. + +Use this decision rule after normalization: + +| Receiver knowledge | Action | +| --- | --- | +| Definitely the modeled built-in receiver type | Apply the model. | +| Definitely another type | Return `null`; use fallback. | +| Possibly the modeled type, with a trustworthy built-in target | Use a type guard and residual complement. | +| `any`/unknown without proof of the built-in target | Return `null`; use fallback. | + +Never choose `typeStreamOf(receiver).firstOrNull()` as proof. It returns one possible type, not necessarily the only +possible type. Use a statically proven type, `singleOrNull()` where uniqueness is guaranteed, or an explicit symbolic +type guard. + +## Fingerprints + +The catalog sorts enabled models by ID and hashes their length-prefixed IDs. Therefore model registration order does +not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries. + +The fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a +manually maintained configuration value. Experiment metadata records the tool revision separately. If model source +can change independently of that revision, the runner also records a content hash for the external source or generated +artifact; that content identity is experiment metadata, not another model ID, version, or compatibility setting. Keep +the catalog fingerprint based only on enabled model IDs rather than adding implementation-specific fingerprint fields +to the common model contract. + +## Observation + +Every completed model or fallback decision produces `TsUnknownCallEvent` through `TsInterpreterObserver.onUnknownCall`. +A model event is emitted once after all satisfiable successor callbacks complete. If a callback throws, dispatch does +not report success for the discarded step. A partially supported call may report both a model and a fallback event. + +- `ModelApplied(modelId)` identifies the semantic model. +- `ResidualFallback(policy)` records the effective fallback. +- `event.outcome` is derived from the decision and is not stored as a second independent value. + +Observer failures are logged and cannot alter symbolic exploration. diff --git a/usvm-ts/src/main/kotlin/org/usvm/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..12f4cbde2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -9,8 +9,8 @@ import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType -import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsLexicalEnvType +import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType @@ -34,6 +34,7 @@ import org.usvm.UConcreteHeapRef import org.usvm.UContext import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.allocateStaticRef @@ -170,7 +171,6 @@ class TsContext( is EtsBooleanType -> EtsArrayType(EtsBooleanType, dimensions = 1) is EtsNumberType -> EtsArrayType(EtsNumberType, dimensions = 1) is EtsArrayType -> TODO("Unsupported yet: $type") - is EtsUnionType -> EtsArrayType(type.elementType, dimensions = 1) else -> EtsArrayType(EtsUnknownType, dimensions = 1) } } @@ -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 { @@ -192,6 +198,17 @@ class TsContext( return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET } + /** + * Checks result alternatives for fake-wrapper identities. Address-region reads lift stored concrete references + * into ITE branches; wrappers in a guard or read key are dependencies, not possible results of the expression. + */ + fun UHeapRef.hasFakeValueBranch(): Boolean = when { + isFakeObject() -> true + this is UIteExpr<*> -> trueBranch.asExpr(addressSort).hasFakeValueBranch() || + falseBranch.asExpr(addressSort).hasFakeValueBranch() + else -> false + } + fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef { if (isFakeObject()) { return this @@ -238,6 +255,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 +268,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 +311,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 +331,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/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index df1ad1961..132c6413b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -13,7 +13,10 @@ import org.usvm.statistics.UInterpreterObserver @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { - /** Called after the profile dispatcher selects an outcome for an unknown call. */ + /** + * Called after the dispatcher completes a model or fallback decision for an unknown call. + * A model decision is reported once after all its satisfiable successor callbacks complete. + */ fun onUnknownCall(event: TsUnknownCallEvent) { // default empty implementation } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 3d6b394f3..0e8e6d537 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -9,10 +9,10 @@ import org.usvm.StateCollectionStrategy import org.usvm.UMachine import org.usvm.UMachineOptions import org.usvm.api.targets.TsTarget -import org.usvm.machine.call.TsNoUnknownCallModels -import org.usvm.machine.call.TsProfileUnknownCallDispatcher +import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsModelUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallDispatcher -import org.usvm.machine.call.TsUnknownCallModelProvider +import org.usvm.machine.call.TsUnknownCallModelCatalog import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -45,15 +45,25 @@ class TsMachine( private val machineObserver: UMachineObserver? = null, observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, - unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + unknownCallModels: TsUnknownCallModelCatalog? = null, ) : UMachine() { + private val resolvedUnknownCallModels = when { + unknownCallDispatcher != null -> null + unknownCallModels != null -> unknownCallModels + else -> TsBuiltInUnknownCallModels.catalog(tsOptions.unknownCallModelSelection) + } + + /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */ + val unknownCallModelCatalogFingerprint: String? + get() = resolvedUnknownCallModels?.fingerprint + private val graph = TsGraph(scene) private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext(scene, components) - private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher( - profile = tsOptions.unknownCallProfile, - modelProvider = unknownCallModelProvider, + private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( + models = requireNotNull(resolvedUnknownCallModels), + fallback = tsOptions.unknownCallFallback, observer = observer, ) private val interpreter = TsInterpreter( @@ -62,6 +72,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/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt index e8f2ec65a..abb6d42cb 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt @@ -22,6 +22,7 @@ sealed interface TsMethodCall : EtsStmt { } } +/** [instance] is an extracted payload; the receiver's branch and runtime-kind guards are already asserted. */ class TsVirtualMethodCallStmt( override val call: EtsInstanceCallExpr, override val instance: UExpr<*>, 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..aca3a3d54 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -1,11 +1,12 @@ package org.usvm.machine -import org.usvm.machine.call.TsUnknownCallProfile -import org.usvm.machine.call.TsUnknownCallProfiles +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallModelSelection data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, - val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP, + val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, + val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, ) 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..935d768c3 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt @@ -0,0 +1,18 @@ +package org.usvm.machine.call + +import org.usvm.machine.call.intrinsic.TsBuiltInUnknownCallModel + +/** Discovers built-in model objects from the sealed hierarchy. */ +object TsBuiltInUnknownCallModels { + private val models by lazy { + TsBuiltInUnknownCallModel::class.sealedSubclasses.map { modelClass -> + requireNotNull(modelClass.objectInstance) { + "Built-in semantic model must be an object: ${modelClass.qualifiedName}" + } + } + } + private val allModels by lazy { TsUnknownCallModelCatalog(models) } + + fun catalog(selection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All): TsUnknownCallModelCatalog = + if (selection == TsUnknownCallModelSelection.All) allModels else TsUnknownCallModelCatalog(models, selection) +} 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..a46c7d9d6 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 @@ -19,6 +19,8 @@ import org.usvm.machine.state.newStmt /** * A call that the regular TypeScript execution pipeline could not execute. * + * Instance receivers are normalized under their runtime-kind and conditional-reference guards before method + * lookup and receiver-dependent approximations. Null and undefined receivers fail at property access. * Frontend call resolution and the existing built-in approximations run before this boundary. A call reaches the * dispatcher only after one of those stages cannot continue normally. Successful compatibility approximations such * as `toString`, `valueOf`, `Math.floor`, and `$r` therefore remain outside this boundary until they are classified @@ -60,6 +62,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 +70,9 @@ fun interface TsUnknownCallDispatcher { fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome } +/** Marks dispatchers that replace migrated compatibility approximations with semantic models. */ +interface TsUnknownCallModelDispatcher : TsUnknownCallDispatcher + /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { @@ -109,6 +115,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 +162,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 +176,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..6334fa48a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt @@ -0,0 +1,91 @@ +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 +import org.usvm.machine.types.TsUnresolvedValue + +/** Declaratively identifies the calls handled by one semantic model. */ +data class TsUnknownCallTarget( + val methodName: String, + val enclosingClassName: String? = null, + val failureReason: TsUnknownCallFailureReason? = null, +) { + init { + require(methodName.isNotBlank()) { "Semantic model target method name must not be blank" } + require(enclosingClassName == null || enclosingClassName.isNotBlank()) { + "Semantic model target class name must not be blank" + } + } +} + +/** + * A semantic model selected by a stable [id] and a declarative [target]. + * + * Returning `null` from [apply] means that the call is outside the model's supported input domain. The dispatcher + * then applies the configured fallback. A non-null execution may additionally contain a guarded residual domain. + */ +interface TsUnknownCallModel { + val id: String + val target: TsUnknownCallTarget + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? +} + +/** Describes how a guarded model successor completes the original call. */ +sealed interface TsUnknownCallModelCompletion { + /** Produces a normal result on the selected successor state. */ + class Normal( + val result: TsState.() -> UExpr<*>, + ) : TsUnknownCallModelCompletion + + /** Produces a normal fake-wrapped result for a value whose runtime kind is unresolved. */ + class Unresolved( + val value: TsUnresolvedValue, + ) : TsUnknownCallModelCompletion + + /** Produces an exceptional result and its TypeScript type on the selected successor state. */ + class Exceptional( + val exception: TsState.() -> Pair, EtsType>, + ) : TsUnknownCallModelCompletion +} + +/** One guarded model successor. */ +class TsUnknownCallModelSuccessor( + val guard: UBoolExpr, + val completion: TsUnknownCallModelCompletion, + val applyStateChanges: TsState.() -> Unit = {}, +) + +/** + * A semantic-model execution plan. + * + * [residualGuard] is the input domain not covered by the model. `null` means that the model completely handles every + * state accepted by [TsUnknownCallModel.apply]. + */ +class TsUnknownCallModelExecution( + successors: List, + val residualGuard: UBoolExpr? = null, +) { + val successors: List = successors.toList() + + init { + require(this.successors.isNotEmpty()) { "A semantic model must declare at least one guarded successor" } + } +} + +/** The result of model lookup for one call. */ +sealed interface TsUnknownCallModelApplication { + class Applied( + val modelId: String, + val execution: TsUnknownCallModelExecution, + ) : TsUnknownCallModelApplication { + init { + require(modelId.isNotBlank()) { "Applied model ID must not be blank" } + } + } + + /** No enabled model accepted the call. */ + data object NotApplicable : TsUnknownCallModelApplication +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt new file mode 100644 index 000000000..ee825bced --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt @@ -0,0 +1,97 @@ +package org.usvm.machine.call + +import org.usvm.machine.state.TsState +import java.nio.ByteBuffer +import java.nio.charset.StandardCharsets +import java.security.MessageDigest +import java.util.Collections + +private const val BYTE_MASK = 0xff + +/** An immutable deterministic set of semantic models used by one machine run. */ +class TsUnknownCallModelCatalog( + models: Collection, + selection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, +) { + private val index: Map>> + + val modelIds: List + val fingerprint: String + + init { + val modelsById = hashMapOf() + models.forEach { model -> + require(model.id.isNotBlank()) { "Semantic model ID must not be blank" } + require(modelsById.put(model.id, model) == null) { "Duplicate semantic model ID: ${model.id}" } + } + + val selectedModels = when (selection) { + TsUnknownCallModelSelection.All -> modelsById.values + is TsUnknownCallModelSelection.Only -> { + val unknownIds = selection.ids.subtract(modelsById.keys) + require(unknownIds.isEmpty()) { "Unknown semantic model IDs: ${unknownIds.sorted().joinToString()}" } + selection.ids.map(modelsById::getValue) + } + }.sortedBy(TsUnknownCallModel::id) + + modelIds = Collections.unmodifiableList(selectedModels.map(TsUnknownCallModel::id)) + index = indexModels(selectedModels) + fingerprint = computeFingerprint(modelIds) + } + + internal fun select(call: TsUnknownCall): TsUnknownCallModel? { + val candidates = index[call.callee.name]?.get(call.failureReason) ?: return null + return candidates[call.callee.enclosingClass.name] ?: candidates[null] + } + + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { + val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable + + return TsUnknownCallModelApplication.Applied( + modelId = model.id, + execution = execution, + ) + } +} + +private fun indexModels( + models: List, +): Map>> { + val index = hashMapOf>>() + models.forEach { model -> + val target = model.target + val methods = index.getOrPut(target.methodName) { hashMapOf() } + val reasons = target.failureReason?.let(::listOf) ?: TsUnknownCallFailureReason.entries + reasons.forEach { reason -> + val classes = methods.getOrPut(reason) { hashMapOf() } + val conflict = if (target.enclosingClassName == null) { + classes.values.firstOrNull() + } else { + classes[target.enclosingClassName] ?: classes[null] + } + if (conflict != null) { + error("Ambiguous semantic model targets: ${listOf(model.id, conflict.id).sorted().joinToString()}") + } + + classes[target.enclosingClassName] = model + } + } + return index +} + +private fun computeFingerprint(modelIds: List): String { + val digest = MessageDigest.getInstance("SHA-256") + modelIds.forEach { digest.updateLengthPrefixed(it) } + + return digest.digest().joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and BYTE_MASK) + } +} + +/** Length prefixes distinguish ID sequences such as ["ab", "c"] and ["a", "bc"]. */ +private fun MessageDigest.updateLengthPrefixed(value: String) { + val bytes = value.toByteArray(StandardCharsets.UTF_8) + update(ByteBuffer.allocate(Int.SIZE_BYTES).putInt(bytes.size).array()) + update(bytes) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt new file mode 100644 index 000000000..474494651 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -0,0 +1,195 @@ +package org.usvm.machine.call + +import mu.KotlinLogging +import org.usvm.UExpr +import org.usvm.api.makeFreshUnknownCallResult +import org.usvm.api.mockMethodCall +import org.usvm.api.setMockMethodCallResult +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.state.newStmt +import org.usvm.machine.types.mkFakeValue + +private val logger = KotlinLogging.logger {} + +/** The externally observable effect of an unknown-call decision. */ +enum class TsUnknownCallOutcome { + MODEL_APPLIED, + FRESH_SYMBOLIC_RETURN, + PATH_STOPPED, +} + +/** Selects what happens when no semantic model handles an unknown call. */ +enum class TsResidualCallPolicy { + STOP_PATH, + FRESH_SYMBOLIC_RETURN, +} + +/** Selects a semantic model and sends unsupported states to one configured fallback. */ +class TsModelUnknownCallDispatcher( + private val models: TsUnknownCallModelCatalog, + private val fallback: TsResidualCallPolicy, + private val observer: TsInterpreterObserver? = null, +) : TsUnknownCallModelDispatcher { + override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { + val application = scope.calcOnState { + this@TsModelUnknownCallDispatcher.models.apply(this, call) + } + + return when (application) { + is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application) + TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call) + } + } + + private fun applyFallback( + scope: TsStepScope, + call: TsUnknownCall, + ): TsUnknownCallOutcome { + val decision = TsUnknownCallDecision.ResidualFallback(fallback) + + when (fallback) { + TsResidualCallPolicy.STOP_PATH -> { + val falseExpr = scope.calcOnState { ctx.falseExpr } + logger.warn { + "Stopping path for unknown call ${call.callee} at ${call.callSite.location}: " + + "reason=${call.failureReason}" + } + scope.assert(falseExpr) + } + + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { + mockMethodCall(scope, call.callee, call.resultType) + scope.doWithState { newStmt(call.callSite) } + } + } + + reportFallback(call) + return decision.outcome + } + + private fun applyModel( + scope: TsStepScope, + call: TsUnknownCall, + application: TsUnknownCallModelApplication.Applied, + ): TsUnknownCallOutcome { + val residualGuard = application.execution.residualGuard + // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone + // inherits both the constraints and their solver models. + val freshResidualResult = if ( + residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + ) { + makeFreshUnknownCallResult(scope, call.resultType) + } else { + null + } + val stoppedResidualIsSatisfiable = residualGuard != null && + fallback == TsResidualCallPolicy.STOP_PATH && + scope.checkSat(residualGuard) != null + + var modelApplied = false + var freshResidualApplied = false + // Materializing an unresolved result adds its exactly-one constraint. Do it before forking so every + // successor that uses the wrapper inherits both the constraint and the refreshed solver models. + val preparedUnresolvedResults = application.execution.successors.map { successor -> + val completion = successor.completion as? TsUnknownCallModelCompletion.Unresolved + ?: return@map null + + scope.calcOnState { + mkFakeValue(scope = scope, value = completion.value) + } + } + val guardedStateChanges = application.execution.successors.mapIndexed { index, successor -> + successor.guard to modelStateChange( + call = call, + successor = successor, + preparedUnresolvedResult = preparedUnresolvedResults[index], + onApplied = { modelApplied = true }, + ) + }.toMutableList() + + if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + guardedStateChanges += residualGuard to { + setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) + newStmt(call.callSite) + freshResidualApplied = true + } + } + + if (stoppedResidualIsSatisfiable) { + logger.warn { + "Stopping residual path for unknown call ${call.callee} at ${call.callSite.location}: " + + "reason=${call.failureReason}" + } + } + scope.forkMulti(guardedStateChanges) + + if (modelApplied) { + observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(application.modelId))) + } + if (freshResidualApplied || stoppedResidualIsSatisfiable) { + reportFallback(call) + } + + 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 reportFallback(call: TsUnknownCall) { + if (fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { + logger.debug { + "Unknown call ${call.callee} at ${call.callSite.location}: " + + "fallback=$fallback, reason=${call.failureReason}" + } + } + observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ResidualFallback(fallback))) + } + + private fun modelStateChange( + call: TsUnknownCall, + successor: TsUnknownCallModelSuccessor, + preparedUnresolvedResult: UExpr<*>?, + onApplied: () -> Unit, + ): 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.Unresolved -> { + val result = requireNotNull(preparedUnresolvedResult) { + "Unresolved semantic-model result was not materialized" + } + methodResult = TsMethodResult.Success.MockedCall(result, call.callee) + newStmt(call.callSite) + } + + is TsUnknownCallModelCompletion.Exceptional -> { + val (exception, type) = completion.exception(this) + methodResult = TsMethodResult.TsException(exception, type) + } + } + + onApplied() + } + + private fun event( + call: TsUnknownCall, + decision: TsUnknownCallDecision, + ) = TsUnknownCallEvent( + callSite = call.callSite, + callee = call.callee, + failureReason = call.failureReason, + decision = decision, + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelSelection.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelSelection.kt new file mode 100644 index 000000000..23131cd9c --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelSelection.kt @@ -0,0 +1,9 @@ +package org.usvm.machine.call + +/** Selects all registered models or an explicit set of model IDs; an empty set disables models. */ +sealed interface TsUnknownCallModelSelection { + /** Enables every discovered built-in model. */ + data object All : TsUnknownCallModelSelection + + data class Only(val ids: Set) : TsUnknownCallModelSelection +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt index 7adf43527..2ae84bffd 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt @@ -7,12 +7,6 @@ import org.usvm.machine.TsInterpreterObserver private val logger = KotlinLogging.logger {} -/** Explains why a call reached the residual fallback instead of a semantic model. */ -enum class TsUnknownCallResidualReason { - MODEL_LOOKUP_DISABLED, - MODEL_NOT_APPLICABLE, -} - /** Describes the model or fallback action selected for one unknown call. */ sealed interface TsUnknownCallDecision { data class ModelApplied( @@ -25,19 +19,28 @@ sealed interface TsUnknownCallDecision { data class ResidualFallback( val policy: TsResidualCallPolicy, - val reason: TsUnknownCallResidualReason, ) : TsUnknownCallDecision } +val TsUnknownCallDecision.outcome: TsUnknownCallOutcome + get() = when (this) { + is TsUnknownCallDecision.ModelApplied -> TsUnknownCallOutcome.MODEL_APPLIED + is TsUnknownCallDecision.ResidualFallback -> when (policy) { + TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED + TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + } + } + /** A structured decision reported for one unknown call. */ data class TsUnknownCallEvent( val callSite: EtsStmt, val callee: EtsMethodSignature, val failureReason: TsUnknownCallFailureReason, - val profile: TsUnknownCallProfile, - val outcome: TsUnknownCallOutcome, val decision: TsUnknownCallDecision, -) +) { + val outcome: TsUnknownCallOutcome + get() = decision.outcome +} internal fun TsInterpreterObserver.onUnknownCallSafely(event: TsUnknownCallEvent) { runCatching { onUnknownCall(event) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt deleted file mode 100644 index 66e4eeb1f..000000000 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt +++ /dev/null @@ -1,167 +0,0 @@ -package org.usvm.machine.call - -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.newStmt - -/** The externally observable decision made for a call that could not be executed normally. */ -enum class TsUnknownCallOutcome { - MODEL_APPLIED, - FRESH_SYMBOLIC_RETURN, - PATH_STOPPED, -} - -/** Controls whether the dispatcher asks the configured model provider to handle a call. */ -enum class TsUnknownCallModelLookup { - DISABLED, - ENABLED, -} - -/** - * Selects what happens when model lookup is disabled or no model applies. - * - * [FRESH_SYMBOLIC_RETURN] creates a new symbolic value of the call expression's result type and advances past the - * call. It deliberately ignores all callee side effects and exceptions, so it is an opaque continuation rather than - * a semantic model of the callee. - */ -enum class TsResidualCallPolicy { - STOP_PATH, - FRESH_SYMBOLIC_RETURN, -} - -/** Independently configures model lookup and the fallback for residual calls. */ -data class TsUnknownCallProfile( - val modelLookup: TsUnknownCallModelLookup, - val residualPolicy: TsResidualCallPolicy, - val residualOverrides: Map = emptyMap(), -) { - internal fun residualPolicyFor(call: TsUnknownCall): TsResidualCallPolicy = - residualOverrides[call.callee.enclosingClass] ?: residualPolicy -} - -/** Ready-to-use profiles for the four supported model/fallback combinations. */ -object TsUnknownCallProfiles { - val STOP_ALL = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.DISABLED, - residualPolicy = TsResidualCallPolicy.STOP_PATH, - ) - val FRESH_SYMBOLIC_FOR_ALL = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.DISABLED, - residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) - val MODELS_THEN_STOP = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.ENABLED, - residualPolicy = TsResidualCallPolicy.STOP_PATH, - ) - val MODELS_THEN_FRESH_SYMBOLIC = TsUnknownCallProfile( - modelLookup = TsUnknownCallModelLookup.ENABLED, - residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) -} - -/** 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 = - TsUnknownCallModelApplication.NotApplicable -} - -/** Applies the selected model/fallback profile to every residual call. */ -class TsProfileUnknownCallDispatcher( - private val profile: TsUnknownCallProfile, - private val modelProvider: TsUnknownCallModelProvider, - private val observer: TsInterpreterObserver? = null, -) : TsUnknownCallDispatcher { - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome { - val residualReason = when (profile.modelLookup) { - TsUnknownCallModelLookup.DISABLED -> { - 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 - } - - TsUnknownCallModelApplication.NotApplicable -> { - TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE - } - } - } - } - - 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, - decision = TsUnknownCallDecision.ResidualFallback( - policy = residualPolicy, - reason = residualReason, - ), - ) - when (residualPolicy) { - TsResidualCallPolicy.STOP_PATH -> { - val falseExpr = scope.calcOnState { ctx.falseExpr } - scope.assert(falseExpr) - } - - TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { - mockMethodCall(scope, call.callee, call.resultType) - scope.doWithState { newStmt(call.callSite) } - } - } - - observer?.onUnknownCallSafely(event) - return outcome - } - - private fun event( - call: TsUnknownCall, - outcome: TsUnknownCallOutcome, - decision: TsUnknownCallDecision, - ) = TsUnknownCallEvent( - callSite = call.callSite, - callee = call.callee, - failureReason = call.failureReason, - profile = profile.copy(residualOverrides = profile.residualOverrides.toMap()), - outcome = outcome, - decision = decision, - ) -} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt new file mode 100644 index 000000000..e060ff41f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -0,0 +1,114 @@ +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.machine.TsSizeSort +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.machine.types.readUnresolvedArrayElement +import org.usvm.util.arrayStorageType +import org.usvm.util.copyArrayElements +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue + +/** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */ +internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { + const val MODEL_ID: String = "ts.array.shift" + + override val id: String = MODEL_ID + override val target = TsUnknownCallTarget( + methodName = "shift", + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) { + val input = resolveInput(state, call) ?: return@with null + val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType) + val length = state.memory.read(lengthLValue) + val zero = mkBv(0) + val one = mkBv(1) + val emptyGuard = mkEq(length, zero) + val nonEmptyGuard = mkNot(emptyGuard) + val newLength = mkBvSubExpr(length, one) + val firstElementCompletion = state.firstElementCompletion(input, zero) + + val emptySuccessor = TsUnknownCallModelSuccessor( + guard = emptyGuard, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + val nonEmptySuccessor = TsUnknownCallModelSuccessor( + guard = nonEmptyGuard, + completion = firstElementCompletion, + applyStateChanges = { + copyArrayElements( + srcRef = input.array, + dstRef = input.array, + arrayType = input.arrayType, + fromSrc = one, + fromDst = zero, + length = newLength, + ) + memory.write(lengthLValue, newLength, guard = trueExpr) + }, + ) + + TsUnknownCallModelExecution(successors = listOf(emptySuccessor, nonEmptySuccessor)) + } + + private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayShiftInput? = with(state.ctx) { + if (call.arguments.isNotEmpty()) { + return@with null + } + + val receiver = call.receiver ?: return@with null + val receiverValue = receiver.resolved ?: return@with null + if (receiverValue.sort != addressSort) { + return@with null + } + + val array = receiverValue.asExpr(addressSort) + val arrayType = state.arrayStorageType(array, receiver.source.type) as? EtsArrayType + ?: return@with null + if (arrayType.dimensions != 1) { + return@with null + } + + val elementSort = typeToSort(arrayType.elementType) + ArrayShiftInput(array, arrayType, elementSort) + } + + private fun TsState.firstElementCompletion( + input: ArrayShiftInput, + index: UExpr, + ): TsUnknownCallModelCompletion = with(ctx) { + if (input.elementSort !is TsUnresolvedSort) { + val firstElementLValue = mkArrayIndexLValue( + sort = input.elementSort, + ref = input.array, + index = index, + type = input.arrayType, + ) + val firstElement = memory.read(firstElementLValue) + + return@with TsUnknownCallModelCompletion.Normal { firstElement } + } + + val firstElement = readUnresolvedArrayElement(memory, input.array, index) + TsUnknownCallModelCompletion.Unresolved(firstElement) + } + + private class ArrayShiftInput( + val array: UExpr, + val arrayType: EtsArrayType, + val elementSort: USort, + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt new file mode 100644 index 000000000..ce29d46e5 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsBuiltInUnknownCallModel.kt @@ -0,0 +1,6 @@ +package org.usvm.machine.call.intrinsic + +import org.usvm.machine.call.TsUnknownCallModel + +/** Implement as an object in this package; the sealed hierarchy registers every built-in automatically. */ +internal sealed interface TsBuiltInUnknownCallModel : TsUnknownCallModel diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt index 5aaa33b7b..81fd2b27b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Call.kt @@ -1,22 +1,24 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr -import mu.KotlinLogging import org.jacodb.ets.model.EtsInstanceCallExpr +import org.usvm.UBoolExpr import org.usvm.UExpr +import org.usvm.UIteExpr +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.TsVirtualMethodCallStmt -import org.usvm.machine.call.TsUnknownCallFailureReason -import org.usvm.machine.call.dispatch import org.usvm.machine.expr.TsExprApproximationResult.NoApproximation import org.usvm.machine.expr.TsExprApproximationResult.ResolveFailure import org.usvm.machine.expr.TsExprApproximationResult.SuccessfulApproximation import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt import org.usvm.machine.state.newStmt - -private val logger = KotlinLogging.logger {} +import org.usvm.machine.types.extractValue +import org.usvm.memory.splitUHeapRef internal fun TsExprResolver.handleInstanceCall( expr: EtsInstanceCallExpr, @@ -36,47 +38,13 @@ internal fun TsExprResolver.handleInstanceCall( } // Try to approximate the call. - when (val result = tryApproximateInstanceCall(expr)) { + when (val result = tryApproximateGlobalInstanceCall(expr)) { is SuccessfulApproximation -> return result.expr is ResolveFailure -> return null is NoApproximation -> {} } - // Resolve the instance. - val instance = run { - val resolved = resolve(expr.instance) ?: return null - if (resolved.isFakeObject()) { - val fakeType = resolved.getFakeType(scope) - scope.assert(fakeType.refTypeExpr) ?: run { - logger.warn { "Calls on non-ref (fake) instance is not supported: $expr" } - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, - resolvedReceiver = resolved, - ) - return null - } - resolved.extractRef(scope) - } else { - if (resolved.sort != addressSort) { - logger.warn { "Calling method on non-ref instance is not yet supported: $expr" } - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER, - resolvedReceiver = resolved, - ) - return null - } - resolved.asExpr(addressSort) - } - } - - // Check for undefined or null property access. - checkUndefinedOrNullPropertyRead(scope, instance, expr.callee.name) ?: return null + val instance = resolve(expr.instance) ?: return null // Resolve arguments. val args = expr.args.map { resolve(it) ?: return null } @@ -91,15 +59,56 @@ fun TsContext.callInstanceMethod( instance: UExpr<*>, args: List>, ): UExpr<*>? { - // Create the virtual call statement. - val virtualCall = TsVirtualMethodCallStmt( - call = call, - instance = instance, - args = args, - returnSite = scope.calcOnState { lastStmt }, - ) - scope.doWithState { newStmt(virtualCall) } + val returnSite = scope.calcOnState { lastStmt } + val alternatives = scope.calcOnState { receiverAlternatives(instance) } + val successors = alternatives.map { (guard, receiver) -> + val callStmt = TsVirtualMethodCallStmt( + call = call, + instance = receiver, + args = args, + returnSite = returnSite, + ) + val advance: TsState.() -> Unit = { newStmt(callStmt) } + guard to advance + } + + if (successors.size == 1 && successors.single().first.isTrue) { + scope.doWithState(successors.single().second) + } else { + scope.forkMulti(successors) + } - // Return null to indicate that we are waiting for the call to be executed. return null } + +/** Keeps the type constraints attached to every receiver passed to the common instance-call pipeline. */ +private fun TsState.receiverAlternatives( + value: UExpr<*>, + guard: UBoolExpr = ctx.trueExpr, +): List>> = with(ctx) { + if (guard.isFalse) return emptyList() + + when { + value.isFakeObject() -> listOf( + extractValue(value, boolSort, ::getIntermediateBoolLValue), + extractValue(value, fp64Sort, ::getIntermediateFpLValue), + extractValue(value, addressSort, ::getIntermediateRefLValue), + ).flatMap { (payload, typeGuard) -> + receiverAlternatives(requireNotNull(payload), mkAnd(guard, typeGuard)) + } + + value.sort == addressSort && value is UIteExpr<*> -> { + val refs = splitUHeapRef( + ref = value.asExpr(addressSort), + initialGuard = guard, + ignoreNullRefs = false, + collapseHeapRefs = false, + ) + (refs.concreteHeapRefs + refs.symbolicHeapRef).flatMap { (ref, refGuard) -> + receiverAlternatives(ref, refGuard) + } + } + + else -> listOf(guard to value) + } +} 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..841a7fc2b 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 @@ -11,28 +11,41 @@ import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UBoolExpr import org.usvm.UExpr +import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.api.initializeArray import org.usvm.api.makeSymbolicPrimitive import org.usvm.api.memcpy -import org.usvm.api.typeStreamOf +import org.usvm.api.readArrayIndex +import org.usvm.getIntValue import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsSizeSort +import org.usvm.machine.TsVirtualMethodCallStmt +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.TsMethodResult +import org.usvm.machine.state.newStmt +import org.usvm.machine.types.TsUnresolvedArrayKind +import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort -import org.usvm.types.first -import org.usvm.types.firstOrNull +import org.usvm.util.arrayStorageType +import org.usvm.util.copyArrayElements +import org.usvm.util.forEachArrayPayloadRegion +import org.usvm.util.initializeArrayKind import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.resolveEtsMethods private val logger = KotlinLogging.logger {} -internal fun TsExprResolver.tryApproximateInstanceCall( +internal fun TsExprResolver.tryApproximateGlobalInstanceCall( expr: EtsInstanceCallExpr, ): TsExprApproximationResult = with(ctx) { // Mock all calls to `Logger` methods @@ -40,19 +53,6 @@ internal fun TsExprResolver.tryApproximateInstanceCall( return from(mkUndefinedValue()) } - // Mock `.toString()` method calls - if (expr.callee.name == "toString") { - if (expr.args.isNotEmpty()) { - logger.warn { "toString() should have no arguments, but got ${expr.args.size}" } - } - return from(mkStringConstant("I am a string", scope)) - } - - // Handle `.valueOf()` method calls - if (expr.callee.name == "valueOf") { - return from(handleValueOf(expr)) - } - // Handle `Number.isNaN()` calls if (expr.instance.name == "Number") { if (expr.callee.name == "isNaN") { @@ -84,17 +84,33 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } - val instance = resolve(expr.instance) - ?: return TsExprApproximationResult.ResolveFailure + return TsExprApproximationResult.NoApproximation +} - val instanceType = if (instance.sort == addressSort && isAllocatedConcreteHeapRef(instance)) { - scope.calcOnState { - memory.typeStreamOf(instance.asExpr(addressSort)).firstOrNull() ?: expr.instance.type +internal fun TsExprResolver.tryApproximateInstanceCall( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + val expr = stmt.call + val instance = stmt.instance + + // Mock `.toString()` method calls + if (expr.callee.name == "toString") { + if (expr.args.isNotEmpty()) { + logger.warn { "toString() should have no arguments, but got ${expr.args.size}" } } - } else { - expr.instance.type + return from(mkStringConstant("I am a string", scope)) + } + + // Handle `.valueOf()` method calls + if (expr.callee.name == "valueOf") { + return from(handleValueOf(expr, instance)) } + if (instance.sort != addressSort) return TsExprApproximationResult.NoApproximation + + val array = instance.asExpr(addressSort) + val instanceType = scope.calcOnState { arrayStorageType(array, expr.instance.type) } + if (instanceType is EtsArrayType) { val elementSort = typeToSort(instanceType.elementType) .takeIf { it !is TsUnresolvedSort } @@ -102,70 +118,89 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle 'Array.push()' method calls if (expr.callee.name == "push") { - return from(handleArrayPush(expr, instanceType, elementSort)) + return from(handleArrayPush(expr, instanceType, elementSort, array)) } // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return from(handleArrayPop(expr, instanceType, elementSort)) + return from(handleArrayPop(stmt, instanceType, elementSort, array)) } // Handle `Array.fill() method calls if (expr.callee.name == "fill") { - return from(handleArrayFill(expr, instanceType, elementSort)) + return from(handleArrayFill(expr, instanceType, elementSort, array)) } // Handle `Array.unshift() method calls if (expr.callee.name == "unshift") { - return from(handleArrayUnshift(expr, instanceType, elementSort)) + return from(handleArrayUnshift(expr, instanceType, array)) } // Handle `Array.shift() method calls if (expr.callee.name == "shift") { - return from(handleArrayShift(expr, instanceType, elementSort)) + return handleArrayShiftCall(stmt, instanceType, elementSort) } // Handle `Array.join() method calls if (expr.callee.name == "join") { - return from(handleArrayJoin(expr, instanceType, elementSort)) + return from(handleArrayJoin(expr)) } // Handle `Array.slice() method calls if (expr.callee.name == "slice") { - return from(handleArraySlice(expr, instanceType, elementSort)) + return from(handleArraySlice(expr, instanceType, array)) } // Handle `Array.concat() method calls if (expr.callee.name == "concat") { - return from(handleArrayConcat(expr, instanceType, elementSort)) + return handleArrayConcat(stmt, instanceType, array) } // Handle `Array.indexOf() method calls if (expr.callee.name == "indexOf") { - return from(handleArrayIndexOf(expr, instanceType, elementSort)) + return from(handleArrayIndexOf(expr, instanceType, elementSort, array)) } // Handle `Array.includes() method calls if (expr.callee.name == "includes") { - return from(handleArrayIncludes(expr, instanceType, elementSort)) + return from(handleArrayIncludes(expr)) } // Handle `Array.reverse() method calls if (expr.callee.name == "reverse") { - return from(handleArrayReverse(expr, instanceType, elementSort)) + return from(handleArrayReverse(expr, instanceType, array)) } } return TsExprApproximationResult.NoApproximation } -private fun TsExprResolver.handleValueOf(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { +private fun TsExprResolver.handleArrayShiftCall( + stmt: TsVirtualMethodCallStmt, + instanceType: EtsArrayType, + elementSort: USort, +): TsExprApproximationResult { + val dispatcher = unknownCallDispatcher + if (dispatcher !is TsUnknownCallModelDispatcher) { + return from(handleArrayShift(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort))) + } + + dispatcher.dispatch( + scope, + stmt, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = stmt.instance, + ) + + return TsExprApproximationResult.ResolveFailure +} + +private fun TsExprResolver.handleValueOf(expr: EtsInstanceCallExpr, instance: UExpr<*>): UExpr<*> { if (expr.args.isNotEmpty()) { logger.warn { "valueOf() should have no arguments, but got ${expr.args.size}" } } - val instance = resolve(expr.instance) ?: return null - instance + return instance } private fun TsExprResolver.handleNumberIsNaN(expr: EtsInstanceCallExpr): UBoolExpr? = with(ctx) { @@ -306,8 +341,8 @@ private fun TsExprResolver.handleArrayPush( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size == 1) { "Array.push() should have exactly one argument, but got ${expr.args.size}" } @@ -364,43 +399,51 @@ private fun TsExprResolver.handleArrayPush( * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.pop */ private fun TsExprResolver.handleArrayPop( - expr: EtsInstanceCallExpr, + stmt: TsVirtualMethodCallStmt, arrayType: EtsArrayType, elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null - check(expr.args.isEmpty()) { - "Array.pop() should have no arguments, but got ${expr.args.size}" + check(stmt.args.isEmpty()) { + "Array.pop() should have no arguments, but got ${stmt.args.size}" } - checkNotFake(array) + removeArrayElement(stmt, array, arrayType, elementSort, first = false) +} - scope.calcOnState { - // Read the length of the array - val lengthLValue = mkArrayLengthLValue(array, arrayType) - val length = memory.read(lengthLValue) +private fun TsExprResolver.removeArrayElement( + stmt: TsVirtualMethodCallStmt, + array: UHeapRef, + arrayType: EtsArrayType, + elementSort: USort, + first: Boolean, +): UExpr<*>? = with(ctx) { + val lengthLValue = mkArrayLengthLValue(array, arrayType) + val length = scope.calcOnState { memory.read(lengthLValue) } + val nonEmpty = mkNot(mkEq(length, mkBv(0))) + scope.fork( + nonEmpty, + blockOnFalseState = { + methodResult = TsMethodResult.Success.MockedCall(mkUndefinedValue(), stmt.call.callee) + newStmt(stmt.returnSite) + }, + ) ?: return null - // Decrease the length of the array - // TODO: Only decrease the length if it is not zero. - // It is not an error/exception to pop from an empty array! - // If the array is empty, `pop` returns `undefined`. + scope.calcOnState { val newLength = mkBvSubExpr(length, mkBv(1)) + val index = if (first) mkBv(0) else newLength + val removed = if (typeToSort(arrayType.elementType) is TsUnresolvedSort) { + mkFakeValue(scope, readUnresolvedArrayElement(memory, array, index)) + } else { + memory.read(mkArrayIndexLValue(elementSort, array, index, arrayType)) + } - // Read the last element of the array (to be removed) - val lastIndexLValue = mkArrayIndexLValue( - sort = elementSort, - ref = array, - index = newLength, - type = arrayType, - ) - // TODO: If the array is empty, return `undefined` instead of the last element. - val removedElement = memory.read(lastIndexLValue) - - // Update the length of the array (AFTER reading the last element) + if (first) { + copyArrayElements(array, array, arrayType, fromSrc = mkBv(1), fromDst = mkBv(0), length = newLength) + } memory.write(lengthLValue, newLength, guard = trueExpr) - // Return the removed element - removedElement + removed } } @@ -433,12 +476,17 @@ private fun TsExprResolver.handleArrayFill( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size >= 1 && expr.args.size <= 3) { "Array.fill() should have 1 to 3 arguments, but got ${expr.args.size}" } - val value = resolve(expr.args[0]) ?: return null + val resolvedValue = resolve(expr.args[0]) ?: return null + val value = if (typeToSort(arrayType.elementType) is TsUnresolvedSort) { + resolvedValue.toFakeObject(scope) + } else { + resolvedValue + } // TODO: Support negative `start` and `end` indices. val start = if (expr.args.size > 1) { @@ -490,7 +538,9 @@ private fun TsExprResolver.handleArrayFill( // Calculate the length of the range to fill val fillLength = mkBvSubExpr(endBv, startBv) - // TODO: check that `fillLength` is less than `ARRAY_FILL_MAX_SIZE` + // Concrete ranges need no unused entries in the temporary array. + val tempSize = getIntValue(fillLength)?.coerceIn(0, ARRAY_FILL_MAX_SIZE) ?: ARRAY_FILL_MAX_SIZE + // TODO: check that symbolic `fillLength` is less than `ARRAY_FILL_MAX_SIZE`. // Allocate a temporary array to hold the filled values val tempArray = memory.allocConcrete(descriptor) @@ -501,7 +551,7 @@ private fun TsExprResolver.handleArrayFill( descriptor, elementSort, sizeSort, - (0 until ARRAY_FILL_MAX_SIZE).asSequence().map { value.asExpr(elementSort) } + (0 until tempSize).asSequence().map { value.asExpr(elementSort) } ) // Copy the filled values to the specified range in the original array @@ -545,51 +595,16 @@ private const val ARRAY_FILL_MAX_SIZE = 10_000 * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.shift */ private fun TsExprResolver.handleArrayShift( - expr: EtsInstanceCallExpr, + stmt: TsVirtualMethodCallStmt, arrayType: EtsArrayType, elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null - check(expr.args.isEmpty()) { - "Array.shift() should have no arguments, but got ${expr.args.size}" + check(stmt.args.isEmpty()) { + "Array.shift() should have no arguments, but got ${stmt.args.size}" } - scope.calcOnState { - // Store the first element of the array (to be removed) - // TODO: If the array is empty, return `undefined` instead of the first element. - val firstIndexLValue = mkArrayIndexLValue( - sort = elementSort, - ref = array, - index = mkBv(0), - type = arrayType, - ) - val firstElement = memory.read(firstIndexLValue) - - // Read the length of the array - val lengthLValue = mkArrayLengthLValue(array, arrayType) - val length = memory.read(lengthLValue) - - // Decrease the length of the array - // TODO: Only decrease the length if it is not zero. - // It is not an error/exception to shift an empty array! - // If the array is empty, `shift` returns `undefined`. - val newLength = mkBvSubExpr(length, mkBv(1)) - memory.write(lengthLValue, newLength, guard = trueExpr) - - // Shift elements to the left - memory.memcpy( - srcRef = array, - dstRef = array, - type = arrayType, - elementSort = elementSort, - fromSrc = mkBv(1), - fromDst = mkBv(0), - length = newLength, - ) - - // Return the removed element - firstElement - } + removeArrayElement(stmt, array, arrayType, elementSort, first = true) } /** @@ -613,9 +628,8 @@ private fun TsExprResolver.handleArrayShift( private fun TsExprResolver.handleArrayUnshift( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, - elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null // TODO: support vararg check(expr.args.size == 1) { "Array.unshift() should have exactly one argument, but got ${expr.args.size}" @@ -632,24 +646,18 @@ private fun TsExprResolver.handleArrayUnshift( memory.write(lengthLValue, newLength, guard = trueExpr) // Shift elements to the right - memory.memcpy( + copyArrayElements( srcRef = array, dstRef = array, - type = arrayType, - elementSort = elementSort, + arrayType = arrayType, fromSrc = mkBv(0), fromDst = mkBv(1), length = length, ) // Write the new element to the start of the array - val startIndexLValue = mkArrayIndexLValue( - sort = elementSort, - ref = array, - index = mkBv(0), - type = arrayType, - ) - memory.write(startIndexLValue, arg.asExpr(elementSort), guard = trueExpr) + assignToArrayIndex(scope, array, index = mkBv(0), expr = arg, arrayType = arrayType) + ?: return@calcOnState null // Return the new length of the array (as per ECMAScript spec for Array.unshift) mkBvToFpExpr( @@ -683,10 +691,7 @@ private fun TsExprResolver.handleArrayUnshift( */ private fun TsExprResolver.handleArrayJoin( expr: EtsInstanceCallExpr, - arrayType: EtsArrayType, - elementSort: USort, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size <= 1) { "Array.join() should have at most one argument, but got ${expr.args.size}" } @@ -727,14 +732,12 @@ private const val ARRAY_JOIN_RESULT = "joined_array_result" private fun TsExprResolver.handleArraySlice( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, - elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size <= 2) { "Array.slice() should have at most two arguments, but got ${expr.args.size}" } - // TODO: Support negative `start` and `end` indices. val start = if (expr.args.isNotEmpty()) { resolve(expr.args[0]) ?: return null } else { @@ -781,23 +784,34 @@ private fun TsExprResolver.handleArraySlice( scope.calcOnState { val descriptor = arrayDescriptorOf(arrayType) - // Calculate the new length of the sliced array - val newLength = mkBvSubExpr(endBv, startBv) + val length = memory.read(mkArrayLengthLValue(array, arrayType)) + val zero = mkBv(0) + + fun normalizeIndex(index: UExpr): UExpr { + val relative = mkIte(mkBvSignedLessExpr(index, zero), mkBvAddExpr(length, index), index) + val capped = mkIte(mkBvSignedGreaterExpr(relative, length), length, relative) + return mkIte(mkBvSignedLessExpr(relative, zero), zero, capped) + } + + val from = normalizeIndex(startBv) + val to = normalizeIndex(endBv) + val newLength = mkIte(mkBvSignedLessExpr(from, to), mkBvSubExpr(to, from), zero) // Allocate a new array for the slice val slicedArray = memory.allocConcrete(descriptor) // Copy the specified range from the original array to the new array - memory.memcpy( + copyArrayElements( srcRef = array, dstRef = slicedArray, - type = descriptor, - elementSort = elementSort, - fromSrc = startBv, + arrayType = arrayType, + fromSrc = from, fromDst = mkBv(0), length = newLength, ) + memory.write(mkArrayLengthLValue(slicedArray, arrayType), newLength, guard = trueExpr) + // Return the new array containing the slice slicedArray } @@ -822,85 +836,75 @@ private fun TsExprResolver.handleArraySlice( * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.concat */ private fun TsExprResolver.handleArrayConcat( - expr: EtsInstanceCallExpr, + stmt: TsVirtualMethodCallStmt, arrayType: EtsArrayType, - elementSort: USort, -): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null - check(expr.args.isNotEmpty()) { - "Array.concat() should have at least one argument, but got ${expr.args.size}" + array: UHeapRef, +): TsExprApproximationResult = with(ctx) { + val elementSort = typeToSort(arrayType.elementType) + val arrayTypes = stmt.args.mapIndexed { index, arg -> + if (arg.sort == addressSort) { + val ref = arg.asExpr(addressSort) + // A fake or an untyped reference may itself contain an array; spreading requires runtime dispatch. + if (ref.hasFakeValueBranch()) return TsExprApproximationResult.NoApproximation + val type = scope.calcOnState { arrayStorageType(ref, stmt.call.args[index].type) } + if (typeToSort(type) is TsUnresolvedSort) return TsExprApproximationResult.NoApproximation + type as? EtsArrayType + } else { + null + } + } + if (arrayTypes.withIndex().any { (index, type) -> + if (type != null) { + typeToSort(type.elementType) != elementSort + } else { + elementSort !is TsUnresolvedSort && stmt.args[index].sort != elementSort + } + } + ) { + logger.debug { "Array.concat requires conversion between different element storage sorts" } + return TsExprApproximationResult.NoApproximation } - val args = expr.args.map { resolve(it) ?: return null } - - scope.calcOnState { - val descriptor = arrayDescriptorOf(arrayType) - - // Allocate a new array for the concatenated result - val resultArray = memory.allocConcrete(descriptor) - - // Read the length of the original array - val originalLengthLValue = mkArrayLengthLValue(array, arrayType) - val originalLength = memory.read(originalLengthLValue) - - // Copy the original array to the result array - memory.memcpy( - srcRef = array, - dstRef = resultArray, - type = descriptor, - elementSort = elementSort, - fromSrc = mkBv(0), - fromDst = mkBv(0), - length = originalLength, - ) + from( + scope.calcOnState { + val resultArray = memory.allocConcrete(arrayDescriptorOf(arrayType)) + val originalLength = memory.read(mkArrayLengthLValue(array, arrayType)) + copyArrayElements( + srcRef = array, + dstRef = resultArray, + arrayType = arrayType, + fromSrc = mkBv(0), + fromDst = mkBv(0), + length = originalLength, + ) - // Handle each argument in the `concat` call - var totalLength = originalLength - for (arg in args) { - // For array arguments, copy their elements to the result array - if (arg.sort == addressSort) { - // TODO: handle empty type stream - val argType = memory.typeStreamOf(arg.asExpr(addressSort)).first() - if (argType is EtsArrayType) { - val argLengthLValue = mkArrayLengthLValue(arg.asExpr(addressSort), argType) - val argLength = memory.read(argLengthLValue) - - // Copy the elements of the argument array to the result array - memory.memcpy( - srcRef = arg.asExpr(addressSort), + var totalLength = originalLength + stmt.args.forEachIndexed { index, arg -> + val argType = arrayTypes[index] + if (argType != null) { + val ref = arg.asExpr(addressSort) + val length = memory.read(mkArrayLengthLValue(ref, argType)) + copyArrayElements( + srcRef = ref, dstRef = resultArray, - type = descriptor, - elementSort = elementSort, + arrayType = argType, fromSrc = mkBv(0), fromDst = totalLength, - length = argLength, + length = length, ) - - // Add the length of the argument array to the total length - totalLength = mkBvAddExpr(totalLength, argLength) - - continue + totalLength = mkBvAddExpr(totalLength, length) + } else { + val newLength = mkBvAddExpr(totalLength, mkBv(1)) + memory.write(mkArrayLengthLValue(resultArray, arrayType), newLength, guard = trueExpr) + assignToArrayIndex(scope, resultArray, totalLength, arg, arrayType) ?: return@calcOnState null + totalLength = newLength } } + memory.write(mkArrayLengthLValue(resultArray, arrayType), totalLength, guard = trueExpr) - // For non-array arguments, treat them as a single element - val newIndexLValue = mkArrayIndexLValue( - sort = elementSort, - ref = resultArray, - index = totalLength, - type = arrayType, - ) - memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr) - totalLength = mkBvAddExpr(totalLength, mkBv(1)) + resultArray } - - // Set the length of the result array - val resultLengthLValue = mkArrayLengthLValue(resultArray, arrayType) - memory.write(resultLengthLValue, totalLength, guard = trueExpr) - - // Return the new concatenated array - resultArray - } + ) } /** @@ -926,8 +930,8 @@ private fun TsExprResolver.handleArrayIndexOf( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size == 1) { "Array.indexOf() should have exactly one argument, but got ${expr.args.size}" } @@ -985,10 +989,7 @@ private fun TsExprResolver.handleArrayIndexOf( */ private fun TsExprResolver.handleArrayIncludes( expr: EtsInstanceCallExpr, - arrayType: EtsArrayType, - elementSort: USort, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.size == 1) { "Array.includes() should have exactly one argument, but got ${expr.args.size}" } @@ -1035,9 +1036,8 @@ private fun TsExprResolver.handleArrayIncludes( private fun TsExprResolver.handleArrayReverse( expr: EtsInstanceCallExpr, arrayType: EtsArrayType, - elementSort: USort, + array: UHeapRef, ): UExpr<*>? = with(ctx) { - val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null check(expr.args.isEmpty()) { "Array.reverse() should have no arguments, but got ${expr.args.size}" } @@ -1052,40 +1052,29 @@ private fun TsExprResolver.handleArrayReverse( val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = memory.read(lengthLValue) - // Initialize the reversed array with symbolic elements - memory.initializeArray( - reversedArray, - descriptor, - elementSort, - sizeSort, - (0 until ARRAY_REVERSE_MAX_SIZE).asSequence().map { index -> - // reversedIndex := length - 1 - index - val reversedIndex = mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index.toBv()) - val elementLValue = mkArrayIndexLValue( - sort = elementSort, - ref = array, - index = reversedIndex, - type = arrayType, - ) - memory.read(elementLValue) + val reversedIndices = (0 until ARRAY_REVERSE_MAX_SIZE).map { index -> + mkBvSubExpr(mkBvSubExpr(length, mkBv(1)), index.toBv()) + } + forEachArrayPayloadRegion(arrayType) { region, sort -> + val contents = reversedIndices.asSequence().map { index -> + memory.readArrayIndex(array, index, region, sort) } - ) - - //! Note: `reversedArray` is a temporary object not used outside this function, - // so it is not necessary to set the "correct" length for it. - // Set the length of the reversed array - // val reversedLengthLValue = mkArrayLengthLValue(reversedArray, arrayType) - // memory.write(reversedLengthLValue, length, guard = trueExpr) + memory.initializeArray(reversedArray, region, sort, sizeSort, contents) + } + if (typeToSort(arrayType.elementType) is TsUnresolvedSort) { + TsUnresolvedArrayKind.entries.forEach { kind -> + val contents = reversedIndices.map { index -> memory.readArrayIndex(array, index, kind, boolSort) } + initializeArrayKind(reversedArray, kind, contents) + } + } - // Copy the reversed array back to the original array (in-place modification) - memory.memcpy( + copyArrayElements( + arrayType = arrayType, srcRef = reversedArray, dstRef = array, - type = descriptor, - elementSort = elementSort, fromSrc = mkBv(0), fromDst = mkBv(0), - length = length, + length = length ) // Return the modified original array diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 684c8902d..4ffb6e227 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -4,20 +4,15 @@ import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsBooleanType -import org.jacodb.ets.model.EtsNumberType -import org.jacodb.ets.model.EtsUnknownType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.api.typeStreamOf -import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort -import org.usvm.types.first +import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue @@ -61,12 +56,7 @@ internal fun TsExprResolver.handleArrayAccess( isSigned = true, ).asExpr(sizeSort) - // Determine the array type. - val arrayType = if (isAllocatedConcreteHeapRef(array)) { - scope.calcOnState { memory.typeStreamOf(array).first() } - } else { - value.array.type - } + val arrayType = scope.calcOnState { arrayStorageType(array, value.array.type) } check(arrayType is EtsArrayType) { "Expected EtsArrayType, got: ${value.array.type}" } @@ -107,48 +97,14 @@ fun TsContext.readArray( return scope.calcOnState { memory.read(lValue) } } - // Concrete arrays with the unresolved sort should consist of fake objects only. - if (array is UConcreteHeapRef) { - // Read a fake object from the array. - val lValue = mkArrayIndexLValue( - sort = addressSort, - ref = array, - index = index, - type = arrayType, - ) - val fake = scope.calcOnState { memory.read(lValue) } - check(fake.isFakeObject()) { - "Expected fake object in concrete array with unresolved element type, got: $fake" - } - return fake - } - - // If the element type is unresolved, we need to create a fake object - // that can hold boolean, number, and reference values. - // We read all three types from the array and combine them into a fake object. return scope.calcOnState { - val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) - val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType) - val bool = memory.read(boolLValue) - - val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) - val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType) - val fp = memory.read(fpLValue) - - val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) - val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType) - val ref = memory.read(refLValue) - - // If the read reference is already a fake object, we can return it directly. - // Otherwise, we need to create a new fake object and write it back to the memory. - // TODO: Think about the type constraint to get a consistent array resolution later - if (ref.isFakeObject()) { - ref - } else { - val fakeObj = mkFakeValue(scope, bool, fp, ref) - lValuesToAllocatedFakeObjects += refLValue to fakeObj + val value = readUnresolvedArrayElement(memory, array, index) + val fakeObj = mkFakeValue(scope = scope, value = value) + if (fakeObj != value.refValue) { + val refLValue = mkArrayIndexLValue(addressSort, array, index, arrayType) memory.write(refLValue, fakeObj, guard = trueExpr) - fakeObj } + + fakeObj } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index fa4d83b68..86444e105 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -12,6 +12,7 @@ import org.usvm.UHeapRef import org.usvm.machine.TsContext import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort +import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue // Handles reading the `length` property. @@ -22,7 +23,8 @@ fun TsContext.readLengthProperty( maxArraySize: Int, ): UExpr<*>? { // Determine the array type. - val arrayType: EtsArrayType = when (val type = instanceLocal.type) { + val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } + val arrayType: EtsArrayType = when (val type = storageType) { is EtsArrayType -> type is EtsAnyType, is EtsUnknownType -> { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index b6ad444ea..f24700c2f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -5,13 +5,11 @@ import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.api.typeStreamOf -import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort -import org.usvm.types.first +import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue @@ -44,14 +42,7 @@ internal fun TsExprResolver.handleAssignToArrayIndex( isSigned = true, ).asExpr(sizeSort) - // Determine the array type. - // TODO: handle the case when `lhv.array.type` is NOT an array. - // In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`. - val arrayType = if (isAllocatedConcreteHeapRef(array)) { - scope.calcOnState { memory.typeStreamOf(array).first() } - } else { - lhv.array.type - } + val arrayType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } check(arrayType is EtsArrayType) { "Expected EtsArrayType, got: ${lhv.array.type}" } @@ -106,7 +97,6 @@ fun TsContext.assignToArrayIndex( ) val fakeExpr = expr.toFakeObject(scope) return scope.doWithState { - lValuesToAllocatedFakeObjects += lValue to fakeExpr memory.write(lValue, fakeExpr, guard = trueExpr) } } 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..70ad6909f 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 @@ -35,7 +35,6 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter -import org.usvm.UIteExpr import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.targets.TsTarget @@ -52,14 +51,17 @@ import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsUnknownCallDispatcher import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.dispatch +import org.usvm.machine.expr.TsExprApproximationResult import org.usvm.machine.expr.TsExprResolver import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.expr.checkUndefinedOrNullPropertyRead import org.usvm.machine.expr.handleAssignToArrayIndex import org.usvm.machine.expr.handleAssignToInstanceField import org.usvm.machine.expr.handleAssignToLocal import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.expr.readGlobal +import org.usvm.machine.expr.tryApproximateInstanceCall import org.usvm.machine.expr.writeGlobal import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -96,6 +98,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 +149,10 @@ class TsInterpreter( } } } catch (e: Exception) { + if (throwExceptionOnStepFailure) { + throw e + } + logger.error { "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { " $it" }}" } @@ -160,25 +167,39 @@ class TsInterpreter( val instance = stmt.instance val callee = stmt.call.callee - val unwrappedInstance = if (instance.isFakeObject()) { - // TODO support primitives calls - // We ignore the possibility of method call on primitives. - // Therefore, the fake object should be unwrapped. - scope.assert(instance.getFakeType(scope).refTypeExpr) - instance.extractRef(scope) - } else { - instance.asExpr(addressSort) + if (instance.sort == addressSort) { + checkUndefinedOrNullPropertyRead(scope, instance.asExpr(addressSort), callee.name) ?: return } + val resolver = exprResolverWithScope(scope) + when (val result = resolver.tryApproximateInstanceCall(stmt)) { + is TsExprApproximationResult.SuccessfulApproximation -> { + scope.doWithState { + methodResult = TsMethodResult.Success.MockedCall(result.expr, callee) + newStmt(stmt.returnSite) + } + return + } + + TsExprApproximationResult.ResolveFailure -> return + TsExprApproximationResult.NoApproximation -> {} + } + + if (instance.sort != addressSort) { + unknownCallDispatcher.dispatch(scope, stmt, Reason.NON_REFERENCE_RECEIVER, instance) + return + } + val receiver = instance.asExpr(addressSort) + val concreteMethods: MutableList = mutableListOf() - if (isAllocatedConcreteHeapRef(unwrappedInstance)) { - val type = scope.calcOnState { memory.typeStreamOf(unwrappedInstance) }.single() + if (isAllocatedConcreteHeapRef(receiver)) { + val type = scope.calcOnState { memory.typeStreamOf(receiver) }.single() if (type is EtsClassType) { val classes = graph.hierarchy.classesForType(type) if (classes.isEmpty()) { logger.warn { "Could not resolve class: ${type.typeName}" } - unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_CLASS_NOT_FOUND, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_CLASS_NOT_FOUND, receiver) return } if (classes.size > 1) { @@ -198,7 +219,7 @@ class TsInterpreter( logger.warn { "Could not resolve method: $callee on type: $type" } - unknownCallDispatcher.dispatch(scope, stmt, Reason.UNSUPPORTED_RECEIVER_TYPE, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.UNSUPPORTED_RECEIVER_TYPE, receiver) return } } else { @@ -207,25 +228,25 @@ class TsInterpreter( if (callee.name !in listOf("then")) { logger.warn { "Could not resolve method: $callee" } } - unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.VIRTUAL_METHOD_NOT_FOUND, receiver) return } concreteMethods += methods } val possibleTypes = scope.calcOnState { - memory.typeStreamOf(unwrappedInstance).take(scene.projectAndSdkClasses.size) + memory.typeStreamOf(receiver).take(scene.projectAndSdkClasses.size) } if (possibleTypes !is TypesResult.SuccessfulTypesResult) { - unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_TYPE_STREAM_UNAVAILABLE, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.RECEIVER_TYPE_STREAM_UNAVAILABLE, receiver) return } val possibleTypesSet = possibleTypes.types.toSet() if (possibleTypesSet.singleOrNull() == EtsAnyType) { - unknownCallDispatcher.dispatch(scope, stmt, Reason.ANY_RECEIVER, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.ANY_RECEIVER, receiver) return } @@ -265,30 +286,11 @@ class TsInterpreter( val type = requireNotNull(method.enclosingClass).type val constraint = scope.calcOnState { - val ref = stmt.instance.asExpr(addressSort) - .takeIf { !it.isFakeObject() } - ?: unwrappedInstance.asExpr(addressSort) - - // TODO: adhoc: "expand" ITE - if (ref is UIteExpr<*>) { - val trueBranch = ref.trueBranch - val falseBranch = ref.falseBranch - if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { - val unwrappedTrueExpr = trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - val unwrappedFalseExpr = falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - return@calcOnState mkIte( - condition = ref.condition, - trueBranch = memory.types.evalIsSubtype(unwrappedTrueExpr, type), - falseBranch = memory.types.evalIsSubtype(unwrappedFalseExpr, type), - ) - } - } - // TODO mistake, should be separated into several hierarchies // or evalTypeEqual with several concrete types mkAnd( - memory.types.evalIsSubtype(ref, clazz), - memory.types.evalIsSupertype(ref, type) + memory.types.evalIsSubtype(receiver, clazz), + memory.types.evalIsSupertype(receiver, type) ) } constraint to block @@ -296,9 +298,9 @@ class TsInterpreter( if (conditionsWithBlocks.isEmpty()) { logger.warn { - "No suitable methods found for call: $callee with instance: $unwrappedInstance" + "No suitable methods found for call: $callee with instance: $receiver" } - unknownCallDispatcher.dispatch(scope, stmt, Reason.NO_SUITABLE_VIRTUAL_TARGET, unwrappedInstance) + unknownCallDispatcher.dispatch(scope, stmt, Reason.NO_SUITABLE_VIRTUAL_TARGET, receiver) return } 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..0917e2dfc 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 @@ -6,6 +6,7 @@ import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.USort import org.usvm.api.makeSymbolicPrimitive import org.usvm.collection.field.UFieldLValue @@ -15,11 +16,28 @@ 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. [valueType], when provided, preserves existing kind selectors instead of creating fresh ones. + * Callers that model a completely unknown value should 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, fpValue: UExpr? = null, refValue: UHeapRef? = null, + valueType: EtsFakeType? = null, ): UConcreteHeapRef = with(ctx) { require(boolValue != null || fpValue != null || refValue != null) { "Fake object should contain at least one value" @@ -28,20 +46,22 @@ fun TsState.mkFakeValue( val fakeValueRef = createFakeObjectRef() val address = fakeValueRef.address - val boolTypeExpr = trueExpr - .takeIf { boolValue != null && fpValue == null && refValue == null } - ?: makeSymbolicPrimitive(boolSort) - val fpTypeExpr = trueExpr - .takeIf { boolValue == null && fpValue != null && refValue == null } - ?: makeSymbolicPrimitive(boolSort) - val refTypeExpr = trueExpr - .takeIf { boolValue == null && fpValue == null && refValue != null } - ?: makeSymbolicPrimitive(boolSort) - - val type = EtsFakeType( - boolTypeExpr = boolTypeExpr, - fpTypeExpr = fpTypeExpr, - refTypeExpr = refTypeExpr, + val type = valueType ?: EtsFakeType( + boolTypeExpr = if (boolValue != null && fpValue == null && refValue == null) { + trueExpr + } else { + makeSymbolicPrimitive(boolSort) + }, + fpTypeExpr = if (boolValue == null && fpValue != null && refValue == null) { + trueExpr + } else { + makeSymbolicPrimitive(boolSort) + }, + refTypeExpr = if (boolValue == null && fpValue == null && refValue != null) { + trueExpr + } else { + makeSymbolicPrimitive(boolSort) + }, ) memory.types.allocate(address, type) val constraint = type.mkExactlyOneTypeConstraint(ctx) @@ -69,6 +89,43 @@ fun TsState.mkFakeValue( fakeValueRef } +fun TsState.mkFakeValue( + scope: TsStepScope, + value: TsUnresolvedValue, +): UConcreteHeapRef = materializeFakeValue(scope, value, value.refValue) + +private fun TsState.materializeFakeValue( + scope: TsStepScope, + value: TsUnresolvedValue, + refValue: UHeapRef, +): UConcreteHeapRef = with(ctx) { + when { + refValue.isFakeObject() -> refValue + + !refValue.hasFakeValueBranch() -> mkFakeValue( + scope = scope, + boolValue = value.boolValue, + fpValue = value.fpValue, + refValue = refValue, + valueType = value.type, + ) + + refValue is UIteExpr<*> -> { + val trueValue = materializeFakeValue(scope, value, refValue.trueBranch.asExpr(addressSort)) + val falseValue = materializeFakeValue(scope, value, refValue.falseBranch.asExpr(addressSort)) + + iteWriteIntoFakeObject( + scope = scope, + condition = refValue.condition, + trueBranchValue = trueValue, + falseBranchValue = falseValue, + ) + } + + else -> error("Unsupported fake-value reference expression: $refValue") + } +} + fun TsState.extractValue( value: UExpr, sort: T, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedArrayKind.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedArrayKind.kt new file mode 100644 index 000000000..795c78106 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedArrayKind.kt @@ -0,0 +1,47 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.readArrayIndex +import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort +import org.usvm.memory.UReadOnlyMemory + +/** Kind selectors live with input elements, so copying elements also preserves their runtime types. */ +internal enum class TsUnresolvedArrayKind { + BOOLEAN, + NUMBER, +} + +internal fun TsContext.readUnresolvedArrayElement( + memory: UReadOnlyMemory<*>, + array: UHeapRef, + index: UExpr, +): TsUnresolvedValue { + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val boolKind = memory.readArrayIndex(array, index, TsUnresolvedArrayKind.BOOLEAN, boolSort) + val fpKind = memory.readArrayIndex(array, index, TsUnresolvedArrayKind.NUMBER, boolSort) + // Default allocated cells represent references (undefined), including cells written with complete fake wrappers. + val refKind = mkNot(mkOr(boolKind, fpKind)) + val type = EtsFakeType( + boolTypeExpr = boolKind, + fpTypeExpr = fpKind, + refTypeExpr = refKind, + ) + val boolValue = memory.readArrayIndex(array, index, boolArrayType, boolSort) + val fpValue = memory.readArrayIndex(array, index, numberArrayType, fp64Sort) + val refValue = memory.readArrayIndex(array, index, unknownArrayType, addressSort) + + return TsUnresolvedValue( + boolValue = boolValue, + fpValue = fpValue, + refValue = refValue, + type = type, + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt new file mode 100644 index 000000000..9e77ec777 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt @@ -0,0 +1,17 @@ +package org.usvm.machine.types + +import io.ksmt.sort.KFp64Sort +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef + +/** + * A read-only snapshot of payloads and kind selectors, without a heap identity or allocation. + * [mkFakeValue] materializes it as a fake wrapper and constrains its kind through a live execution scope. + */ +data class TsUnresolvedValue( + val boolValue: UBoolExpr, + val fpValue: UExpr, + val refValue: UHeapRef, + val type: EtsFakeType, +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt new file mode 100644 index 000000000..3cd941ce4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -0,0 +1,75 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr +import org.usvm.UBoolSort +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.api.memcpy +import org.usvm.collection.array.UArrayRegion +import org.usvm.collection.array.UArrayRegionId +import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort +import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedArrayKind + +/** Enumerates payload regions independently of whether an array was allocated or came from the input. */ +internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) { + val elementSort = typeToSort(arrayType.elementType) + if (elementSort !is TsUnresolvedSort) { + action(arrayDescriptorOf(arrayType), elementSort) + return + } + + action(EtsArrayType(EtsBooleanType, dimensions = 1), boolSort) + action(EtsArrayType(EtsNumberType, dimensions = 1), fp64Sort) + action(EtsArrayType(EtsUnknownType, dimensions = 1), addressSort) +} + +internal fun TsState.copyArrayElements( + srcRef: UHeapRef, + dstRef: UHeapRef, + arrayType: EtsArrayType, + fromSrc: UExpr, + fromDst: UExpr, + length: UExpr, +) { + ctx.forEachArrayPayloadRegion(arrayType) { region, sort -> + memory.memcpy(srcRef, dstRef, region, sort, fromSrc, fromDst, length) + } + if (ctx.typeToSort(arrayType.elementType) is TsUnresolvedSort) { + TsUnresolvedArrayKind.entries.forEach { kind -> + memory.memcpy(srcRef, dstRef, kind, ctx.boolSort, fromSrc, fromDst, length) + } + } +} + +/** Initializes a selector region; selectors have no separate array length or heap type. */ +internal fun TsState.initializeArrayKind( + array: UConcreteHeapRef, + kind: TsUnresolvedArrayKind, + values: List, +) { + val regionId = UArrayRegionId(kind, ctx.boolSort) + val region = memory.getRegion(regionId) + check(region is UArrayRegion) { + "Cannot initialize array kind in $region" + } + + val initialized = region.initializeAllocatedArray( + address = array.address, + arrayType = kind, + sort = ctx.boolSort, + content = values, + operationGuard = ctx.trueExpr, + ownership = memory.ownership, + ) + memory.setRegion(regionId, initialized) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt index abedd267c..8b319bd53 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -4,17 +4,35 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsType +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort +import org.usvm.USymbolicHeapRef +import org.usvm.api.typeStreamOf import org.usvm.collection.array.UArrayIndexLValue import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.collection.field.UFieldLValue +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.IntermediateLValueField import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.tctx +import org.usvm.machine.state.TsState import org.usvm.memory.URegisterStackLValue import org.usvm.sizeSort +import org.usvm.types.singleOrNull + +/** Local type widening does not change the regions backing an array. */ +internal fun TsState.arrayStorageType(ref: UHeapRef, staticType: EtsType): EtsType { + if (ref !is UConcreteHeapRef && ref !is USymbolicHeapRef) return staticType + + val memoryType = memory.typeStreamOf(ref).singleOrNull() + return if (memoryType is EtsArrayType || isAllocatedConcreteHeapRef(ref)) { + memoryType ?: staticType + } else { + staticType + } +} fun mkFieldLValue( sort: Sort, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt new file mode 100644 index 000000000..ad65cc64a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt @@ -0,0 +1,419 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnknownType +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.ValueSource +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.api.makeSymbolicRefUntyped +import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedArrayKind +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkArrayLengthLValue +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayShiftIntrinsicModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayShiftIntrinsic.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `empty array shift returns undefined through intrinsic model`() { + val result = analyze(methodName = "emptyArray") + + assertIs(result.values.single()) + assertEquals(listOf("ts.array.shift"), result.modelIds) + assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}"))) + } + + @Test + fun `non empty array shift returns first element moves tail and shrinks array`() { + val result = analyze(methodName = "nonEmptyArray") + + assertEquals(32.0, assertIs(result.values.single()).number) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `reference array preserves removed element alias and moves tail`() { + val result = analyze(methodName = "aliasedElement") + + assertEquals(42.0, assertIs(result.values.single()).number) + } + + @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 `empty and non empty guards are complementary`() { + val state = analyzeStates(methodName = "unknownValue").single() + val symbolicArray = state.makeSymbolicRefUntyped() + + val application = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(symbolicArray)) + val execution = assertNotNull(application) + val (emptyArray, nonEmptyArray) = execution.successors + + assertEquals(2, execution.successors.size) + assertEquals(state.ctx.mkNot(emptyArray.guard), nonEmptyArray.guard) + assertNull(execution.residualGuard) + } + + @Test + fun `symbolic unknown array preserves removed element and moves all value regions`() { + val result = analyze(methodName = "symbolicUnknownArray") + val numbers = result.values.mapNotNull { value -> (value as? TsTestValue.TsNumber)?.number } + + assertEquals(setOf(0.0, 47.0), numbers.toSet()) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `shift reads the moved element from current memory`() { + val result = analyze(methodName = "readBeforeShift") + val numbers = result.values.mapNotNull { value -> (value as? TsTestValue.TsNumber)?.number } + + assertEquals(setOf(0.0, 1.0, 2.0), numbers.toSet()) + } + + @Test + fun `array read observes a write through an aliased symbolic index`() { + val result = analyze(methodName = "writeThroughSymbolicIndex") + val numbers = result.values.mapNotNull { value -> (value as? TsTestValue.TsNumber)?.number } + + assertTrue(20.0 in numbers) + assertTrue(10.0 !in numbers) + } + + @Test + fun `current resolver observes a shifted fake wrapper`() { + val result = analyze(methodName = "shiftedWrittenUnknownArray") + val arrays = result.values.filterIsInstance>() + val shiftedValues = arrays.mapNotNull { array -> + (array.values.singleOrNull() as? TsTestValue.TsNumber)?.number + } + + assertEquals(listOf(20.0), shiftedValues) + } + + @Test + fun `symbolic unknown array copies payload and runtime kind regions`() { + val state = analyzeStates(methodName = "unknownValue").single() + val symbolicArray = state.makeSymbolicRefUntyped() + + with(state.ctx) { + val zero = mkBv(0) + val one = mkBv(1) + val boolValue = trueExpr + val fpValue = mkFp64(17.0) + val refValue = state.makeSymbolicRefUntyped() + + val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1) + val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1) + val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + + val lengthLValue = mkArrayLengthLValue(symbolicArray, unknownArrayType) + state.memory.write(lengthLValue, mkBv(2), guard = trueExpr) + state.memory.write( + mkArrayIndexLValue(boolSort, symbolicArray, one, boolArrayType), + boolValue, + guard = trueExpr, + ) + state.memory.write( + mkArrayIndexLValue(fp64Sort, symbolicArray, one, numberArrayType), + fpValue, + guard = trueExpr, + ) + state.memory.write( + mkArrayIndexLValue(addressSort, symbolicArray, one, unknownArrayType), + refValue, + guard = trueExpr, + ) + + TsUnresolvedArrayKind.entries.forEach { kind -> + val selector = UArrayIndexLValue(boolSort, symbolicArray, one, kind) + state.memory.write(selector, mkBool(kind == TsUnresolvedArrayKind.NUMBER), guard = trueExpr) + } + + val execution = assertNotNull( + TsArrayShiftIntrinsicModel.apply( + state, + arrayShiftCall(symbolicArray, methodName = "symbolicUnknownArray"), + ) + ) + val nonEmptySuccessor = execution.successors.last() + assertIs(nonEmptySuccessor.completion) + + nonEmptySuccessor.applyStateChanges(state) + + val shiftedBoolValue = state.memory.read( + mkArrayIndexLValue(boolSort, symbolicArray, zero, boolArrayType) + ) + val shiftedFpValue = state.memory.read( + mkArrayIndexLValue(fp64Sort, symbolicArray, zero, numberArrayType) + ) + val shiftedRefValue = state.memory.read( + mkArrayIndexLValue(addressSort, symbolicArray, zero, unknownArrayType) + ) + + assertEquals(boolValue, shiftedBoolValue) + assertEquals(fpValue, shiftedFpValue) + assertEquals(refValue, shiftedRefValue) + TsUnresolvedArrayKind.entries.forEach { kind -> + val shiftedSelector = UArrayIndexLValue(boolSort, symbolicArray, zero, kind) + assertEquals(mkBool(kind == TsUnresolvedArrayKind.NUMBER), state.memory.read(shiftedSelector)) + } + assertEquals(one, state.memory.read(lengthLValue)) + } + } + + @Test + fun `concrete unknown array shifts fake wrapped values`() { + val result = analyze(methodName = "mixedUnknownArray") + + assertEquals(49.0, assertIs(result.values.single()).number) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `repeated shifts do not copy fake allocation history`() { + val state = analyzeStates(methodName = "unknownValue").single() + val symbolicArray = state.makeSymbolicRefUntyped() + val fakeValue = makeFakeReceiver(state) + + with(state.ctx) { + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + val materializedElement = mkArrayIndexLValue(addressSort, symbolicArray, mkBv(19), arrayType) + state.lValuesToAllocatedFakeObjects += materializedElement to fakeValue + state.memory.write(materializedElement, fakeValue, guard = trueExpr) + state.memory.write( + mkArrayLengthLValue(symbolicArray, arrayType), + mkBv(20), + guard = trueExpr, + ) + val historyBeforeShift = state.lValuesToAllocatedFakeObjects.toList() + + repeat(12) { + val execution = assertNotNull( + TsArrayShiftIntrinsicModel.apply( + state, + arrayShiftCall(symbolicArray, methodName = "symbolicUnknownArray"), + ) + ) + execution.successors.last().applyStateChanges(state) + } + + assertEquals(historyBeforeShift, state.lValuesToAllocatedFakeObjects) + } + } + + @Test + fun `empty concrete unknown array returns undefined`() { + val result = analyze(methodName = "emptyUnknownArray") + + assertIs(result.values.single()) + assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome }) + } + + @Test + fun `array shift with arguments uses residual fallback`() { + assertUsesResidualFallback(methodName = "shiftWithArguments") + } + + @Test + fun `empty enabled set sends shift to configured fallback`() { + val disabledResult = analyze( + methodName = "nonEmptyArray", + tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), + ) + + assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), disabledResult.events.map { it.outcome }) + } + + @Test + fun `compatibility dispatcher keeps the legacy shift approximation`() { + val result = analyze( + methodName = "nonEmptyArray", + dispatcher = TsCompatibilityUnknownCallDispatcher, + ) + + assertEquals(32.0, assertIs(result.values.single()).number) + assertTrue(result.events.isEmpty()) + assertNull(result.catalogFingerprint) + } + + @ParameterizedTest + @ValueSource( + strings = [ + "numberArrayThroughAnyAlias", + "booleanArrayThroughUnknownAlias", + "conditionalArray", + "conditionalEmptyArray", + "pushAfterShift", + ], + ) + fun `aliases and mutated mixed arrays preserve values`(methodName: String) { + val result = analyze(methodName) + + assertTrue(result.values.isNotEmpty()) + assertEquals(setOf(1.0), result.values.map { assertIs(it).number }.toSet()) + if (methodName == "conditionalArray" || methodName == "conditionalEmptyArray") { + assertEquals(2, result.values.size, "Both receiver choices must be explored") + } + assertTrue(result.events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `conditional fake elements retain both possible writes`() { + val result = analyze(methodName = "conditionalFakeElement") + + assertEquals(setOf(0.0, 1.0), result.values.map { assertIs(it).number }.toSet()) + } + + 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()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome) + } + + private fun makeFakeReceiver(state: TsState): UConcreteHeapRef { + val result = assertIs(state.methodResult).value + val fakeReceiver = assertIs(result) + + assertTrue(with(state.ctx) { fakeReceiver.isFakeObject() }) + return fakeReceiver + } + + private fun arrayShiftCall( + resolvedReceiver: UExpr<*>, + methodName: String = "nonEmptyArray", + ): TsUnknownCall { + val callSite = method(methodName).cfg.stmts.single { stmt -> + stmt.callExpr?.callee?.name == "shift" + } + val sourceCall = assertIs(assertNotNull(callSite.callExpr)) + + return TsUnknownCall( + callee = sourceCall.callee, + receiver = TsUnknownCallValue(source = sourceCall.instance, resolved = resolvedReceiver), + arguments = emptyList(), + resultType = sourceCall.type, + callSite = callSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + } + + private fun analyzeStates(methodName: String): List { + 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 == "ArrayShiftIntrinsic" } + .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, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt new file mode 100644 index 000000000..b4633a6c0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftMatrixTest.kt @@ -0,0 +1,181 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.DynamicTest +import org.junit.jupiter.api.TestFactory +import org.junit.jupiter.api.io.TempDir +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 java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayShiftMatrixTest { + @TempDir + lateinit var directory: Path + + @TestFactory + fun `concrete array matrix agrees with JavaScript`(): List { + val cases = concreteCases() + val source = directory.resolve("ArrayShiftMatrix.ts") + source.writeText(renderSource(cases, typed = true)) + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val methods = scene.projectClasses.single { it.name == "ArrayShiftMatrix" }.methods.associateBy { it.name } + val invocations = cases.indices.joinToString(separator = ",") { "new ArrayShiftMatrix().case$it()" } + val oracleSource = renderSource(cases, typed = false) + "\nconsole.log([$invocations].join('\\n'));\n" + val expected = runJavaScript(oracleSource) + + assertEquals(cases.size, expected.size) + assertTrue(expected.all { it == "1" }, "Generated invariants must hold in native JavaScript") + + return cases.mapIndexed { index, case -> + DynamicTest.dynamicTest(case.label) { + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + val method = methods.getValue("case$index") + + val values = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(), observer = observer) + .use { machine -> + machine.analyze(listOf(method)).map { state -> + TsTestResolver().resolve(method, state).returnValue + } + } + + val actual = values.map { assertIs(it).number } + assertEquals(listOf(expected[index].toDouble()), actual) + assertEquals(case.shiftCount, events.size) + assertTrue(events.all { it.decision == TsUnknownCallDecision.ModelApplied("ts.array.shift") }) + } + } + } + + private fun concreteCases(): List { + val families = listOf( + Family(name = "numbers", type = "number", values = listOf("-3", "0", "17")), + Family(name = "booleans", type = "boolean", values = listOf("true", "false", "true")), + Family(name = "strings", type = "string", values = listOf("'left'", "''", "'right'")), + Family(name = "references", type = "ShiftElement", values = listOf("first", "second", "first")), + Family(name = "nulls", type = "null", values = listOf("null", "null")), + Family(name = "undefineds", type = "undefined", values = listOf("undefined", "undefined")), + Family(name = "mixed", type = "any", values = listOf("17", "true", "first", "'left'", "null", "undefined")), + Family(name = "union", type = "(number | boolean)", values = listOf("17", "true", "-3", "false")), + Family( + name = "nullable", + type = "(ShiftElement | null | undefined)", + values = listOf("null", "first", "undefined"), + ), + Family(name = "nested values", type = "any", values = listOf("true", "nested", "first")), + Family(name = "function values", type = "any", values = listOf("false", "callback", "undefined")), + Family(name = "special numbers", type = "number", values = listOf("NaN", "Infinity", "-Infinity", "-0.0")), + ) + + return buildList { + for (family in families) { + for (size in listOf(0, 1, family.values.size).distinct()) { + for (type in listOf(family.type, "any", "unknown").distinct()) { + val values = family.values.take(size) + for (drain in listOf(false, true)) { + add( + ShiftCase( + label = "${family.name}, $type[], size=$size, drain=$drain", + type = type, + values = values, + drain = drain, + ) + ) + } + } + } + } + } + } + + private fun renderSource(cases: List, typed: Boolean): String = buildString { + appendLine("class ShiftElement {}") + appendLine("class ArrayShiftMatrix {") + cases.forEachIndexed { index, case -> + appendLine("case$index() {") + appendLine("const first = new ShiftElement(); const second = new ShiftElement();") + appendLine("const nested = [7, 8]; const callback = () => 1;") + val annotation = if (typed) ": ${case.type}[]" else "" + appendLine("const original$annotation = [${case.values.joinToString()}];") + appendLine("const values$annotation = original;") + + repeat(case.shiftCount) { shift -> + appendLine("const removed$shift = values.shift();") + val value = case.values.getOrElse(shift) { "undefined" } + appendLine("if (!(${sameValue("removed$shift", value)})) return -1;") + val tail = case.values.drop(shift + 1) + appendLine("if (original.length !== ${tail.size} || values.length !== ${tail.size}) return -2;") + tail.forEachIndexed { tailIndex, tailValue -> + appendLine("if (!(${sameValue("original[$tailIndex]", tailValue)})) return -3;") + } + } + appendLine("return 1;") + appendLine("}") + } + appendLine("}") + } + + private fun sameValue(actual: String, expected: String): String = when (expected) { + "NaN" -> "Number.isNaN($actual)" + "-0.0" -> "1 / $actual === -Infinity" + else -> "$actual === $expected" + } + + private fun runJavaScript(source: String): List { + val script = directory.resolve("oracle.js") + val output = directory.resolve("oracle.out") + script.writeText(source) + val process = ProcessBuilder("node", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "JavaScript oracle timed out") + assertEquals(0, process.exitValue(), output.readText()) + return output.readText().trim().lines() + } finally { + if (process.isAlive) process.destroyForcibly() + } + } + + private data class Family(val name: String, val type: String, val values: List) + + private data class ShiftCase(val label: String, val type: String, val values: List, val drain: Boolean) { + val shiftCount: Int get() = if (drain) values.size + 1 else 1 + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt new file mode 100644 index 000000000..2a844e606 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt @@ -0,0 +1,492 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.DynamicTest +import org.junit.jupiter.api.TestFactory +import org.junit.jupiter.api.io.TempDir +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.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsTestResolver +import java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayShiftReplayTest { + @TempDir + lateinit var directory: Path + + @TestFactory + fun `symbolic shift inputs results and heap changes replay in JavaScript`(): List { + val cases = replayCases() + val source = directory.resolve("ArrayShiftReplay.ts") + source.writeText(renderSource(cases)) + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val methods = scene.projectClasses.single { it.name == "ArrayShiftReplay" }.methods.associateBy { it.name } + + return cases.mapIndexed { index, case -> + DynamicTest.dynamicTest(case.name) { + val method = methods.getValue("case$index") + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + + assertTrue(tests.isNotEmpty()) + val results = tests.map { + assertIs(it.returnValue, message = it.toString()).number + }.toSet() + assertEquals((0..case.maxResult).map { it.toDouble() }.toSet(), results) + + val script = buildString { + appendLine(renderSource(cases)) + appendLine(JS_SAME_VALUE) + tests.forEachIndexed { stateIndex, test -> + val arguments = test.before.parameters.joinToString(transform = ::jsValue) + val expectedAfter = test.after.parameters.joinToString(transform = ::jsValue) + appendLine("{") + appendLine("const args = [$arguments];") + appendLine("const actual = new ArrayShiftReplay().case$index(...args);") + val expectedResult = jsValue(test.returnValue) + appendLine("if (!same(actual, $expectedResult)) throw Error('result $stateIndex');") + appendLine("if (!same(args, [$expectedAfter])) throw Error('heap $stateIndex');") + appendLine("}") + } + } + assertReplay(script, index) + } + } + } + + private fun replayCases(): List = buildList { + for (type in listOf("any", "unknown")) { + add( + ReplayCase( + name = "first $type read", + parameters = "values: $type[]", + maxResult = 6, + body = """ + if (values.length !== 1) return 0; + const removed = values.shift(); + if (removed === 42) return 1; + if (removed === true) return 2; + if (removed === false) return 3; + if (removed === null) return 4; + if (removed === undefined) return 5; + return 6; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "repeated mixed $type shifts", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 2) return 0; + const first = values.shift(); + const second = values.shift(); + if (first === 42 && second === true) return 1; + if (first === false && second === 17) return 2; + return 3; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "read shifted $type tail", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 2) return 0; + values.shift(); + if (values[0] === 42) return 1; + if (values[0] === true) return 2; + return 3; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "overwrite $type then shift", + parameters = "values: $type[], index: number", + maxResult = 3, + body = """ + if (values.length !== 2 || (index !== 0 && index !== 1)) return 0; + values[index] = true; + const first = values.shift(); + if (first === 42 && values[0] === true) return 1; + if (first === true && values[0] === 17) return 2; + return 3; + """.trimIndent(), + ) + ) + } + add( + ReplayCase( + name = "typed pop payload remains usable as number and array index", + parameters = "values: number[]", + maxResult = 2, + body = """ + if (values.length !== 1) return 0; + const n = values.pop(); + if (n !== 1) return 1; + const target = [10, 20]; + return Math.floor(n) === 1 && target[n] === 20 ? 2 : -1; + """.trimIndent(), + ) + ) + addAll(storageOperationCases()) + addAll(pairCases()) + addAll(typedCases()) + } + + private fun storageOperationCases(): List = listOf("any", "unknown").flatMap { type -> + copyCases(type) + mutationCases(type) + concatCases(type) + } + + private fun copyCases(type: String): List = listOf( + ReplayCase( + name = "$type slice() retains all runtime kinds", + parameters = "values: $type[]", + maxResult = 6, + body = """ + if (values.length !== 1) return 0; + const copy = values.slice(); + const value = copy[0]; + if (value === 42) return 1; + if (value === true) return 2; + if (value === false) return 3; + if (value === null) return 4; + if (value === undefined) return 5; + return 6; + """.trimIndent(), + ), + ReplayCase( + name = "$type slice().reverse() retains all runtime kinds", + parameters = "values: $type[]", + maxResult = 6, + body = """ + if (values.length !== 1) return 0; + const copy = values.slice().reverse(); + const value = copy[0]; + if (value === 42) return 1; + if (value === true) return 2; + if (value === false) return 3; + if (value === null) return 4; + if (value === undefined) return 5; + return 6; + """.trimIndent(), + ), + ReplayCase( + name = "$type sliced input mixed with appended wrapper", + parameters = "values: $type[], index: number", + maxResult = 4, + body = """ + if (values.length !== 1) return 0; + const i = Math.floor(index); + if (!(i >= 0 && i <= 1)) return 0; + const copy = values.slice(); + copy.push(true); + const value = copy[i]; + if (i === 1 && value === true) return 1; + if (i === 0 && value === 42) return 2; + if (i === 0 && value === false) return 3; + return 4; + """.trimIndent(), + ), + ReplayCase( + name = "$type copied payload moves through two shifts", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 2) return 0; + const copy = values.slice(); + const first = copy.shift(); + const second = copy.shift(); + if (first === 42 && second === true) return 1; + if (first === false && second === 17) return 2; + return 3; + """.trimIndent(), + ), + ) + + private fun mutationCases(type: String): List = listOf( + ReplayCase( + name = "$type unshift preserves unread tail and pop kind", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 1) return 0; + const alias = values; + values.unshift(true); + const tail = alias.pop(); + if (alias[0] !== true || alias.length !== 1) return -1; + if (tail === 42) return 1; + if (tail === false) return 2; + return 3; + """.trimIndent(), + ), + ReplayCase( + name = "$type reverse permutes payloads and kinds", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 2) return 0; + const copy = values.slice(); + copy.reverse(); + if (copy[0] === 42 && copy[1] === true) return 1; + if (copy[0] === false && copy[1] === 17) return 2; + return 3; + """.trimIndent(), + ), + ReplayCase( + name = "$type fill overrides input kind selectors", + parameters = "values: $type[], index: number", + maxResult = 4, + body = """ + if (values.length !== 2) return 0; + const i = Math.floor(index); + if (!(i >= 0 && i <= 1)) return 0; + values.fill(true, 1, 2); + const value = values[i]; + if (i === 1 && value === true) return 1; + if (i === 0 && value === 42) return 2; + if (i === 0 && value === false) return 3; + return 4; + """.trimIndent(), + ), + ) + + private fun concatCases(type: String): List = listOf( + ReplayCase( + name = "$type concat copies unread input arrays", + parameters = "left: $type[], right: $type[]", + maxResult = 3, + body = """ + if (left.length !== 1 || right.length !== 1) return 0; + const copy = left.concat(right); + const first = copy.shift(); + const second = copy.shift(); + if (first === 42 && second === true) return 1; + if (first === false && second === 17) return 2; + return 3; + """.trimIndent(), + ), + ReplayCase( + name = "$type concat wraps scalar primitives", + parameters = "values: $type[]", + maxResult = 3, + body = """ + if (values.length !== 1) return 0; + const copy = values.concat(true); + if (copy[1] !== true) return -1; + if (copy[0] === 42) return 1; + if (copy[0] === false) return 2; + return 3; + """.trimIndent(), + ), + ReplayCase( + name = "$type empty pop returns undefined and retains length", + parameters = "values: $type[]", + maxResult = 1, + body = """ + if (values.length !== 0) return 0; + const result = values.pop(); + return result === undefined && values.length === 0 ? 1 : -1; + """.trimIndent(), + ), + ) + + private fun pairCases(): List = buildList { + val literals = listOf("42", "true", "false", "null", "undefined", "'left'") + for (type in listOf("any", "unknown")) { + for (first in literals) { + for (second in literals) { + // Unconstrained string equality is not modeled yet; write string slots before shifting. + val writes = listOf(first, second).mapIndexedNotNull { index, literal -> + if (literal == "'left'") "values[$index] = $literal;" else null + }.joinToString(separator = "\n") + val label = if (writes.isEmpty()) "input pair" else "pair with written string" + val maxResult = if (first == "'left'" && second == "'left'") 1 else 2 + add( + ReplayCase( + name = "$type $label $first then $second", + parameters = "values: $type[]", + maxResult = maxResult, + body = """ + if (values.length !== 2) return 0; + $writes + const first = values.shift(); + const second = values.shift(); + return first === $first && second === $second ? 1 : 2; + """.trimIndent(), + ) + ) + } + } + } + } + + private fun typedCases(): List = buildList { + for ((type, literal) in listOf("number" to "42", "boolean" to "true")) { + add( + ReplayCase( + name = "homogeneous $type", + parameters = "values: $type[]", + maxResult = 2, + body = """ + if (values.length !== 2) return 0; + const first = values.shift(); + return first === $literal && values[0] === $literal ? 1 : 2; + """.trimIndent(), + ) + ) + } + add( + ReplayCase( + name = "written homogeneous string", + parameters = "values: string[]", + maxResult = 1, + body = """ + if (values.length !== 2) return 0; + values[0] = 'left'; + values[1] = 'right'; + return values.shift() === 'left' && values[0] === 'right' ? 1 : 2; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "written symbolic union", + parameters = "values: (number | boolean)[]", + maxResult = 1, + body = """ + if (values.length !== 2) return 0; + values[0] = 42; + values[1] = true; + return values.shift() === 42 && values[0] === true ? 1 : 2; + """.trimIndent(), + ) + ) + for (type in listOf("number", "boolean")) { + for (aliasType in listOf("any", "unknown")) { + add( + ReplayCase( + name = "symbolic $type array through $aliasType alias", + parameters = "values: $type[]", + maxResult = if (type == "number") 2 else 1, + body = """ + if (values.length !== 2) return 0; + const alias: $aliasType[] = values; + const first = values[0]; + const second = values[1]; + return alias.shift() === first && values[0] === second && alias.length === 1 ? 1 : 2; + """.trimIndent(), + ) + ) + } + } + add( + ReplayCase( + name = "symbolic object array preserves references", + parameters = "values: ReplayElement[]", + maxResult = 2, + body = """ + if (values.length !== 2) return 0; + const first = values[0]; + const second = values[1]; + if (first == null || second == null) return 2; + return values.shift() === first && values[0] === second ? 1 : 3; + """.trimIndent(), + ) + ) + } + + private fun renderSource(cases: List): String = buildString { + appendLine("class ReplayElement {}") + appendLine("class ArrayShiftReplay {") + cases.forEachIndexed { index, case -> + appendLine("case$index(${case.parameters}) { ${case.body} }") + } + appendLine("}") + } + + private fun jsValue(value: TsTestValue): String = when (value) { + TsTestValue.TsUndefined -> "undefined" + TsTestValue.TsNull -> "null" + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsArray<*> -> value.values.joinToString(prefix = "[", postfix = "]", transform = ::jsValue) + is TsTestValue.TsClass -> value.properties.entries.joinToString(prefix = "({", postfix = "})") { + "${jsString(it.key)}: ${jsValue(it.value)}" + } + else -> error("Unsupported replay value: $value") + } + + private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( + separator = "", + prefix = "\"", + postfix = "\"", + ) + + private fun assertReplay(source: String, index: Int) { + val script = directory.resolve("replay$index.ts") + val output = directory.resolve("replay$index.out") + script.writeText(source) + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Replay timed out") + assertEquals(0, process.exitValue(), "${output.readText()}\n$source") + } finally { + if (process.isAlive) process.destroyForcibly() + } + } + + private data class ReplayCase( + val name: String, + val parameters: String, + val maxResult: Int, + val body: String, + ) + + private companion object { + const val JS_SAME_VALUE = """ + function same(a, b) { + if (Object.is(a, b)) return true; + if (!a || !b || typeof a !== 'object' || typeof b !== 'object') return false; + if (Array.isArray(a) !== Array.isArray(b)) return false; + const keys = Object.keys(a); + return keys.length === Object.keys(b).length && keys.every(k => same(a[k], b[k])); + } + """ + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt new file mode 100644 index 000000000..a38ba9b3f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt @@ -0,0 +1,173 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.DynamicTest +import org.junit.jupiter.api.TestFactory +import org.junit.jupiter.api.io.TempDir +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 java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsInstanceCallReceiverTest { + @TempDir + lateinit var directory: Path + + @TestFactory + fun `normalized receivers preserve supported calls and exceptional branches`(): List { + val source = getResourcePath("/models/InstanceCallReceiver.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val methods = scene.projectClasses.single { it.name == "InstanceCallReceiver" }.methods.associateBy { it.name } + + return cases.map { case -> + DynamicTest.dynamicTest(case.method) { + val method = methods.getValue(case.method) + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(), observer = observer) + .use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + + val results = tests.mapNotNull { (it.returnValue as? TsTestValue.TsNumber)?.number }.toSet() + assertEquals(case.results, results) + assertEquals(case.throws, tests.any { it.returnValue is TsTestValue.TsException }) + assertTrue(tests.isNotEmpty()) + if (method.parameters.singleOrNull()?.name == "index") { + val indices = tests.map { assertIs(it.before.parameters.single()).number } + assertTrue(indices.containsAll(listOf(0.0, 1.0)), "Both receiver alternatives must be explored") + } + + if (case.method == "wrappedShift") { + assertEquals(TsUnknownCallDecision.ModelApplied("ts.array.shift"), events.single().decision) + } + if (case.method == "customShift") assertTrue(events.isEmpty()) + + val replay = buildString { + appendLine(source.readText()) + tests.forEachIndexed { index, test -> + val args = test.before.parameters.joinToString(transform = ::jsValue) + val expected = if (test.returnValue is TsTestValue.TsException) { + "'throws'" + } else { + assertIs(test.returnValue).number.toString() + } + appendLine("{") + appendLine("let actual;") + appendLine("try { actual = new InstanceCallReceiver().${case.method}($args); }") + appendLine("catch { actual = 'throws'; }") + appendLine("if (actual !== $expected) throw Error('case ${case.method}, state $index');") + appendLine("}") + } + } + assertReplay(replay, case.method) + } + } + } + + private fun jsValue(value: TsTestValue): String = when (value) { + TsTestValue.TsUndefined -> "undefined" + TsTestValue.TsNull -> "null" + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsClass -> value.properties.entries.joinToString(prefix = "({", postfix = "})") { + "${jsString(it.key)}: ${jsValue(it.value)}" + } + else -> error("Unsupported receiver input: $value") + } + + private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( + separator = "", + prefix = "\"", + postfix = "\"", + ) + + private fun assertReplay(source: String, name: String) { + val script = directory.resolve("$name.ts") + val output = directory.resolve("$name.out") + script.writeText(source) + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Receiver replay timed out") + assertEquals(0, process.exitValue(), "${output.readText()}\n$source") + } finally { + if (process.isAlive) process.destroyForcibly() + } + } + + private data class Case( + val method: String, + val results: Set, + val throws: Boolean = false, + ) + + private companion object { + val cases = listOf( + Case(method = "wrappedShift", results = setOf(1.0)), + Case(method = "wrappedPop", results = setOf(1.0)), + Case(method = "wrappedPush", results = setOf(1.0)), + Case(method = "wrappedReverse", results = setOf(1.0)), + Case(method = "wrappedFill", results = setOf(1.0)), + Case(method = "wrappedUnshift", results = setOf(1.0)), + Case(method = "wrappedSlice", results = setOf(1.0)), + Case(method = "wrappedSliceReversed", results = setOf(1.0)), + Case(method = "wrappedSlicePastEnd", results = setOf(1.0)), + Case(method = "wrappedSlicePastStart", results = setOf(1.0)), + Case(method = "wrappedSliceNegative", results = setOf(1.0)), + Case(method = "wrappedSliceEmpty", results = setOf(1.0)), + Case(method = "wrappedConcat", results = setOf(1.0)), + Case(method = "wrappedUserMethod", results = setOf(1.0)), + Case(method = "customShift", results = setOf(1.0)), + Case(method = "conditionalArrays", results = setOf(0.0, 1.0)), + Case(method = "conditionalEmptyArray", results = setOf(0.0, 1.0)), + Case(method = "arrayOrUserMethod", results = setOf(0.0, 1.0)), + Case(method = "primitiveValueOf", results = setOf(0.0, 1.0)), + Case(method = "primitiveToString", results = setOf(0.0, 1.0)), + Case(method = "constrainedFake", results = setOf(0.0, 1.0, 2.0)), + Case(method = "nullableReceiver", results = setOf(0.0, 1.0), throws = true), + Case(method = "undefinedReceiver", results = setOf(0.0, 1.0), throws = true), + Case(method = "nullToString", results = emptySet(), throws = true), + Case(method = "undefinedValueOf", results = emptySet(), throws = true), + Case(method = "nullShift", results = emptySet(), throws = true), + Case(method = "undefinedShift", results = emptySet(), throws = true), + ) + + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index 5233e5280..4abb82bb0 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,8 @@ package org.usvm.machine.call +import io.ksmt.sort.KFp64Sort 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 +11,8 @@ 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.EtsType import org.jacodb.ets.model.EtsVoidType import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.callExpr @@ -17,18 +21,20 @@ import org.junit.jupiter.api.Test import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy +import org.usvm.UBoolSort 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.solver.USatResult import org.usvm.util.getResourcePath import kotlin.test.assertEquals import kotlin.test.assertFailsWith @@ -47,31 +53,25 @@ class TsUnknownCallDispatcherTest { private val fullScene = EtsScene(listOf(sourceFile)) @Test - fun `every profile decision is reported through the interpreter observer`() { + fun `every model or fallback decision is reported through the interpreter observer`() { val cases = listOf( ObservationCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.STOP_PATH, + models = noModels, outcome = TsUnknownCallOutcome.PATH_STOPPED, - decision = TsUnknownCallDecision.ResidualFallback( - policy = TsResidualCallPolicy.STOP_PATH, - reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE, - ), + decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH), finalStateCount = 0, ), ObservationCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = noModels, outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - decision = TsUnknownCallDecision.ResidualFallback( - policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED, - ), + decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), finalStateCount = 1, ), ObservationCase( - profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, - modelProvider = ApplyingModelProvider, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(ApplyingModel), outcome = TsUnknownCallOutcome.MODEL_APPLIED, decision = TsUnknownCallDecision.ModelApplied(modelId = "applying-model"), finalStateCount = 1, @@ -82,17 +82,16 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "declaredMethodWithoutBodyContinues", - profile = case.profile, - modelProvider = case.modelProvider, + fallback = case.fallback, + models = case.models, observer = observer, ) - assertEquals(case.finalStateCount, states.size, case.profile.toString()) + assertEquals(case.finalStateCount, states.size, case.fallback.toString()) val event = observer.events.single() assertEquals("declaredMethodWithoutBodyContinues", event.callSite.location.method.name) assertEquals("external", event.callee.name) assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, event.failureReason) - assertEquals(case.profile, event.profile) assertEquals(case.outcome, event.outcome) assertEquals(case.decision, event.decision) } @@ -103,8 +102,7 @@ class TsUnknownCallDispatcherTest { val observer = RecordingUnknownCallObserver() val states = analyzeAllStates( methodName = "modeledUnknownCallForks", - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = ForkingModelProvider, + models = catalog(ForkingModel), observer = observer, ) @@ -113,17 +111,30 @@ class TsUnknownCallDispatcherTest { assertEquals(TsUnknownCallOutcome.MODEL_APPLIED, event.outcome) } + @Test + fun `failed fork callback does not report a completed model decision`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + models = catalog(FailingSecondSuccessorModel), + observer = observer, + ) + + assertTrue(states.isEmpty()) + assertTrue(observer.events.isEmpty()) + } + @Test fun `throwing observer cannot change fresh or modeled exploration`() { val cases = listOf( ObservationFailureCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - modelProvider = TsNoUnknownCallModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = noModels, expectedFinalStateCount = 1, ), ObservationFailureCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - modelProvider = ForkingModelProvider, + fallback = TsResidualCallPolicy.STOP_PATH, + models = catalog(ForkingModel), expectedFinalStateCount = 2, methodName = "modeledUnknownCallForks", ), @@ -132,19 +143,22 @@ class TsUnknownCallDispatcherTest { cases.forEach { case -> val states = analyzeAllStates( methodName = case.methodName, - profile = case.profile, - modelProvider = case.modelProvider, + fallback = case.fallback, + models = case.models, observer = ThrowingUnknownCallObserver, ) - assertEquals(case.expectedFinalStateCount, states.size, case.profile.toString()) + assertEquals(case.expectedFinalStateCount, states.size, case.fallback.toString()) } } @Test fun `applied model decisions require non blank identifiers`() { assertFailsWith { - TsUnknownCallModelApplication.Applied(modelId = " ") + TsUnknownCallModelApplication.Applied( + modelId = " ", + execution = completeExecution(), + ) } assertFailsWith { TsUnknownCallDecision.ModelApplied(modelId = "") @@ -152,93 +166,102 @@ class TsUnknownCallDispatcherTest { } @Test - fun `profiles select model lookup independently from residual fallback`() { - val cases = listOf( - ProfileCase( - profile = TsUnknownCallProfiles.STOP_ALL, - withoutModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - withModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - withoutModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.MODELS_THEN_STOP, - withoutModel = ProfileResult( - reachesReturn = false, - outcome = TsUnknownCallOutcome.PATH_STOPPED, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - ), - ), - ProfileCase( - profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC, - withoutModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN, - ), - withModel = ProfileResult( - reachesReturn = true, - outcome = TsUnknownCallOutcome.MODEL_APPLIED, - ), - ), + fun `model execution plans require at least one successor`() { + val error = assertFailsWith { + TsUnknownCallModelExecution( + successors = emptyList(), + residualGuard = mockk(), + ) + } + + assertEquals("A semantic model must declare at least one guarded successor", error.message) + } + + @Test + fun `fresh fallback preserves all fake value representations`() { + assertFreshResultPreservesAllFakeRepresentations( + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ) + } - cases.forEach { case -> - assertEquals(case.withoutModel, runProfile(case.profile, TsNoUnknownCallModels), case.profile.toString()) - assertEquals(case.withModel, runProfile(case.profile, ApplyingModelProvider), case.profile.toString()) - } + @Test + fun `partial residual fallback preserves all fake value representations`() { + assertFreshResultPreservesAllFakeRepresentations( + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(UnsupportedPartialModel), + ) + } + + @Test + fun `partial model sends only residual domain to fresh fallback`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(SupportedTrueResidualFalseModel), + observer = observer, + ) + + assertEquals(2, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), + observer.events.map { it.outcome }, + ) } @Test - fun `TsOptions profile configures the machine dispatcher`() { - assertEquals(TsUnknownCallProfiles.MODELS_THEN_STOP, TsOptions().unknownCallProfile) - assertTrue(TsOptions().unknownCallProfile.residualOverrides.isEmpty()) + fun `partial model sends residual domain to stop fallback`() { + val observer = RecordingUnknownCallObserver() + val states = analyzeAllStates( + methodName = "modeledUnknownCallForks", + models = catalog(SupportedTrueResidualFalseModel), + observer = observer, + ) - assertFalse(reachesReturn("declaredMethodWithoutBodyContinues")) - assertTrue( - reachesReturn( - "declaredMethodWithoutBodyContinues", - tsOptions = TsOptions(unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL), - ) + assertEquals(1, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.PATH_STOPPED), + observer.events.map { it.outcome }, ) } @Test - fun `explicit family override replaces the profile residual fallback`() { - val family = method(fullScene, "declaredMethodWithoutBodyContinues") + fun `exceptional model successor preserves exception state`() { + val states = analyzeAllStates( + methodName = "modeledUnknownCallThrows", + models = catalog(ExceptionalModel), + ) + + assertIs(states.single().methodResult) + } + + @Test + fun `stateful model can return an existing reference alias`() { + val states = analyzeAllStates( + methodName = "modeledUnknownCallReturnsAlias", + models = catalog(StatefulAliasModel), + ) + val aliasReturn = method(fullScene, "modeledUnknownCallReturnsAlias") .cfg .stmts - .mapNotNull { it.callExpr } - .single { it.callee.name == "external" } - .callee - .enclosingClass - val profile = TsUnknownCallProfiles.STOP_ALL.copy( - residualOverrides = mapOf( - family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, - ) - ) + .filterIsInstance() + .first() + val state = states.single() + assertTrue(aliasReturn in state.pathNode.allStatements) + assertTrue(STATE_CHANGE_MARKER in state.addedArtificialLocals) + } + + @Test + fun `TsOptions configures one fallback without profiles`() { + assertEquals(TsResidualCallPolicy.STOP_PATH, TsOptions().unknownCallFallback) + assertEquals(TsUnknownCallModelSelection.All, TsOptions().unknownCallModelSelection) + + assertFalse(reachesReturn("declaredMethodWithoutBodyContinues")) assertTrue( reachesReturn( "declaredMethodWithoutBodyContinues", - tsOptions = TsOptions(unknownCallProfile = profile), + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN), ) ) } @@ -246,9 +269,9 @@ class TsUnknownCallDispatcherTest { @Test fun `fresh symbolic return uses the source call result type`() { val dispatcher = RecordingResultSortDispatcher( - TsProfileUnknownCallDispatcher( - TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL, - TsNoUnknownCallModels, + TsModelUnknownCallDispatcher( + models = noModels, + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, ) ) @@ -354,7 +377,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor keeps typed call data without eagerly resolving arguments`() { + fun `unknown call keeps typed data without eagerly resolving arguments`() { val dispatcher = RecordingUnknownCallDispatcher() val scene = sceneWithout("ExternalStatic") @@ -369,7 +392,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor preserves source and resolved values available at dispatch`() { + fun `unknown call preserves source and resolved values available at dispatch`() { val dispatcher = RecordingUnknownCallDispatcher() assertFalse(reachesReturn("nonReferenceInstanceCallPrunes", dispatcher = dispatcher)) @@ -384,8 +407,7 @@ class TsUnknownCallDispatcherTest { @Test fun `normally executable and compatibility-approximated calls bypass unknown dispatch`() { val methods = listOf( - // The native frontend gives this call a concrete executable target despite the legacy baseline name. - "anyReceiverWithKnownMethodContinues", + "knownReceiverMethodContinues", "loggerCallSkipsBody", "toStringUsesPlaceholder", "valueOfReturnsReceiver", @@ -401,6 +423,46 @@ class TsUnknownCallDispatcherTest { } } + @Test + fun `unknown receiver preserves primitive fallbacks and executes the reference method`() { + val dispatcher = RecordingUnknownCallDispatcher() + + assertTrue(reachesReturn("anyReceiverWithKnownMethodContinues", dispatcher = dispatcher)) + + assertEquals(2, dispatcher.calls.size) + assertTrue(dispatcher.calls.all { it.failureReason == TsUnknownCallFailureReason.NON_REFERENCE_RECEIVER }) + val sorts = dispatcher.calls.map { assertNotNull(it.receiver?.resolved).sort } + assertTrue(sorts.any { it is UBoolSort }) + assertTrue(sorts.any { it is KFp64Sort }) + dispatcher.calls.forEach { call -> + assertEquals("known", call.callee.name) + assertEquals("anyReceiverWithKnownMethodContinues", call.callSite.location.method.name) + assertEquals(call.callee, assertNotNull(call.callSite.callExpr).callee) + } + } + + @Test + fun `partial approximation preserves resolved arguments and original call site`() { + val calls = mutableListOf() + var expectedArgument: UExpr<*>? = null + val model = object : TestModel(id = "recording-shift", methodName = "shift") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + calls += call + expectedArgument = state.ctx.mkFp64(17.0) + return null + } + } + + assertFalse(reachesReturn("arrayShiftWithArgument", models = catalog(model))) + + val call = calls.single() + assertEquals(assertNotNull(expectedArgument), call.arguments.single().resolved) + assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, call.failureReason) + assertNotNull(call.receiver?.resolved) + assertEquals("arrayShiftWithArgument", call.callSite.location.method.name) + assertEquals(call.arguments.single().source, assertNotNull(call.callSite.callExpr).args.single()) + } + @Test fun `pre-call allocation failures are documented dispatcher exclusions`() { val dispatcher = RecordingUnknownCallDispatcher() @@ -410,7 +472,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `pointer descriptor pairs its source with the resolved function pointer`() { + fun `pointer call pairs its source with the resolved function pointer`() { val dispatcher = RecordingUnknownCallDispatcher() val pointerCall = method(fullScene, "associatedLoggingPointerContinues", className = "Log") .cfg @@ -434,7 +496,7 @@ class TsUnknownCallDispatcherTest { } @Test - fun `descriptor result type comes from the source overload`() { + fun `unknown call result type comes from the source overload`() { val dispatcher = RecordingUnknownCallDispatcher() assertTrue(reachesReturn("overloadedDeclaredMethodWithoutBodyContinues", dispatcher = dispatcher)) @@ -452,17 +514,17 @@ class TsUnknownCallDispatcherTest { scene: EtsScene = fullScene, tsOptions: TsOptions = TsOptions(), dispatcher: TsUnknownCallDispatcher? = null, - modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + models: TsUnknownCallModelCatalog = noModels, className: String = "CallFallbackBaseline", ): Boolean = returnStatement(scene, methodName, className) in - reachedStatements(methodName, scene, tsOptions, dispatcher, modelProvider, className) + reachedStatements(methodName, scene, tsOptions, dispatcher, models, className) private fun reachedStatements( methodName: String, scene: EtsScene, tsOptions: TsOptions, dispatcher: TsUnknownCallDispatcher?, - modelProvider: TsUnknownCallModelProvider, + models: TsUnknownCallModelCatalog, className: String, ): Set { val method = method(scene, methodName, className) @@ -476,7 +538,7 @@ class TsUnknownCallDispatcherTest { tsOptions = tsOptions, machineObserver = ReachabilityObserver(), unknownCallDispatcher = dispatcher, - unknownCallModelProvider = modelProvider, + unknownCallModels = models, ).use { machine -> machine.analyze(listOf(method), listOf(initialTarget)) .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } @@ -508,22 +570,60 @@ class TsUnknownCallDispatcherTest { private fun analyzeAllStates( methodName: String, - profile: TsUnknownCallProfile, - modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels, + fallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, + models: TsUnknownCallModelCatalog = noModels, observer: TsInterpreterObserver? = null, ): List { val method = method(fullScene, methodName) return TsMachine( scene = fullScene, options = allStatesMachineOptions, - tsOptions = TsOptions(unknownCallProfile = profile), + tsOptions = TsOptions(unknownCallFallback = fallback), observer = observer, - unknownCallModelProvider = modelProvider, + unknownCallModels = models, ).use { machine -> machine.analyze(listOf(method)) } } + private fun assertFreshResultPreservesAllFakeRepresentations( + fallback: TsResidualCallPolicy, + models: TsUnknownCallModelCatalog = noModels, + ) { + val method = method(fullScene, "freshUnknownCallResult") + TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(unknownCallFallback = fallback), + unknownCallModels = models, + ).use { machine -> + val state = machine.analyze(listOf(method)).single() + val result = assertIs(state.methodResult).value + val fakeValue = assertIs(result) + val fakeType = with(state.ctx) { + assertTrue(fakeValue.isFakeObject()) + fakeValue.getFakeType(state.memory) + } + val discriminators = mapOf( + "boolean" to fakeType.boolTypeExpr, + "number" to fakeType.fpTypeExpr, + "reference" to fakeType.refTypeExpr, + ) + + discriminators.forEach { (kind, discriminator) -> + val constraints = state.pathConstraints.clone() + constraints += discriminator + val solverResult = state.ctx.solver().check(constraints) + + assertIs>(solverResult, "Fresh fake result lost its $kind representation") + } + + val exactlyOneType = fakeType.mkExactlyOneTypeConstraint(state.ctx) + assertTrue(state.models.isNotEmpty()) + assertTrue(state.models.all { model -> model.eval(exactlyOneType).isTrue }) + } + } + private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher { val calls = mutableListOf() val receiverIsAssociatedFunction = mutableListOf() @@ -538,27 +638,6 @@ class TsUnknownCallDispatcherTest { } } - private fun runProfile( - profile: TsUnknownCallProfile, - modelProvider: TsUnknownCallModelProvider, - ): ProfileResult { - val dispatcher = RecordingOutcomeDispatcher(TsProfileUnknownCallDispatcher(profile, modelProvider)) - val reachesReturn = reachesReturn( - "declaredMethodWithoutBodyContinues", - dispatcher = dispatcher, - ) - return ProfileResult(reachesReturn, dispatcher.outcomes.single()) - } - - private class RecordingOutcomeDispatcher( - private val delegate: TsUnknownCallDispatcher, - ) : TsUnknownCallDispatcher { - val outcomes = mutableListOf() - - override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome = - delegate.dispatch(scope, call).also(outcomes::add) - } - private class RecordingResultSortDispatcher( private val delegate: TsUnknownCallDispatcher, ) : TsUnknownCallDispatcher { @@ -576,31 +655,115 @@ 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") + private object ApplyingModel : TestModel(id = "applying-model", methodName = "external") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelExecution(successors = listOf(successor)) } } - private object ForkingModelProvider : TsUnknownCallModelProvider { - override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication { + private object ForkingModel : TestModel(id = "forking-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { val result = requireNotNull(call.arguments.single().resolved) - val condition = 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 TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = condition, + completion = completion, + ), + TsUnknownCallModelSuccessor( + guard = state.ctx.mkNot(condition), + completion = completion, + ), + ), ) - return TsUnknownCallModelApplication.Applied(modelId = "forking-model") } } + private object FailingSecondSuccessorModel : TestModel(id = "failing-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val execution = ForkingModel.apply(state, call) + val (first, second) = execution.successors + val failingSecond = TsUnknownCallModelSuccessor( + guard = second.guard, + completion = second.completion, + applyStateChanges = { error("second successor failed") }, + ) + + return TsUnknownCallModelExecution(successors = listOf(first, failingSecond)) + } + } + + private object SupportedTrueResidualFalseModel : TestModel(id = "partial-model", methodName = "convert") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val result = requireNotNull(call.arguments.single().resolved) + val condition = result.asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.mkNot(condition), + ) + } + } + + private object ExceptionalModel : TestModel(id = "exceptional-model", methodName = "fail") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Exceptional { + ctx.mkUndefinedValue() to EtsStringType + }, + ) + + return TsUnknownCallModelExecution(successors = listOf(successor)) + } + } + + private object UnsupportedPartialModel : TestModel(id = "unsupported-partial-model", methodName = "value") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.falseExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + ) + + return TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = state.ctx.trueExpr, + ) + } + } + + private object StatefulAliasModel : TestModel(id = "stateful-alias-model", methodName = "identity") { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val argument = requireNotNull(call.arguments.single().resolved) + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { argument }, + applyStateChanges = { addedArtificialLocals += STATE_CHANGE_MARKER }, + ) + + return TsUnknownCallModelExecution(successors = listOf(successor)) + } + } + + private abstract class TestModel( + override val id: String, + methodName: String, + ) : TsUnknownCallModel { + override val target = TsUnknownCallTarget(methodName = methodName) + } + private class RecordingUnknownCallObserver : TsInterpreterObserver { val events = mutableListOf() @@ -615,28 +778,17 @@ class TsUnknownCallDispatcherTest { } } - private data class ProfileCase( - val profile: TsUnknownCallProfile, - val withoutModel: ProfileResult, - val withModel: ProfileResult, - ) - - private data class ProfileResult( - val reachesReturn: Boolean, - val outcome: TsUnknownCallOutcome, - ) - private data class ObservationCase( - val profile: TsUnknownCallProfile, - val modelProvider: TsUnknownCallModelProvider, + val fallback: TsResidualCallPolicy, + val models: TsUnknownCallModelCatalog, val outcome: TsUnknownCallOutcome, val decision: TsUnknownCallDecision, val finalStateCount: Int, ) private data class ObservationFailureCase( - val profile: TsUnknownCallProfile, - val modelProvider: TsUnknownCallModelProvider, + val fallback: TsResidualCallPolicy, + val models: TsUnknownCallModelCatalog, val expectedFinalStateCount: Int, val methodName: String = "declaredMethodWithoutBodyContinues", ) @@ -658,6 +810,23 @@ class TsUnknownCallDispatcherTest { } private companion object { + const val STATE_CHANGE_MARKER = "semantic-model-state-change" + + val noModels = TsUnknownCallModelCatalog(emptyList()) + + fun catalog(vararg models: TsUnknownCallModel): TsUnknownCallModelCatalog = + TsUnknownCallModelCatalog(models.toList()) + + fun completeExecution(): TsUnknownCallModelExecution = + TsUnknownCallModelExecution( + successors = listOf( + TsUnknownCallModelSuccessor( + guard = mockk(), + completion = TsUnknownCallModelCompletion.Normal { mockk>() }, + ), + ), + ) + val machineOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), exceptionsPropagation = true, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt new file mode 100644 index 000000000..658e1e0bd --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -0,0 +1,203 @@ +package org.usvm.machine.call + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel +import org.usvm.machine.state.TsState +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNotEquals +import kotlin.test.assertNull +import kotlin.test.assertSame +import kotlin.test.assertTrue + +class TsUnknownCallModelCatalogTest { + private val callSite = mockk() + + @Test + fun `model IDs and target names must be non blank`() { + assertFailsWith { + TsUnknownCallModelCatalog(listOf(model(id = " "))) + } + assertFailsWith { + TsUnknownCallTarget(methodName = " ") + } + assertFailsWith { + TsUnknownCallTarget(methodName = "method", enclosingClassName = " ") + } + } + + @Test + fun `duplicate IDs are rejected`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf( + model(id = "duplicate", methodName = "first"), + model(id = "duplicate", methodName = "second"), + ) + ) + } + + assertEquals("Duplicate semantic model ID: duplicate", error.message) + } + + @Test + fun `overlapping declarative targets are rejected before execution`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf( + model(id = "z-model", methodName = "target"), + model( + id = "a-model", + methodName = "target", + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ), + ) + ) + } + + assertEquals("Ambiguous semantic model targets: a-model, z-model", error.message) + } + + @Test + fun `unknown enabled IDs are rejected`() { + val error = assertFailsWith { + TsUnknownCallModelCatalog( + models = listOf(model(id = "known")), + selection = TsUnknownCallModelSelection.Only(setOf("missing")), + ) + } + + assertEquals("Unknown semantic model IDs: missing", error.message) + } + + @Test + fun `selection and fingerprint do not depend on model order`() { + val forward = listOf( + model(id = "a", methodName = "first"), + model(id = "b", methodName = "second"), + ) + + val first = TsUnknownCallModelCatalog(forward) + val second = TsUnknownCallModelCatalog(forward.reversed()) + + assertEquals(listOf("a", "b"), first.modelIds) + assertEquals(first.modelIds, second.modelIds) + assertEquals(first.fingerprint, second.fingerprint) + } + + @Test + fun `enabled subset is detached and changes fingerprint`() { + val mutableIds = mutableSetOf("a") + val models = listOf( + model(id = "a", methodName = "first"), + model(id = "b", methodName = "second"), + ) + val onlyA = TsUnknownCallModelCatalog(models, selection = TsUnknownCallModelSelection.Only(mutableIds)) + mutableIds += "b" + val both = TsUnknownCallModelCatalog(models) + + assertEquals(listOf("a"), onlyA.modelIds) + assertNotEquals(onlyA.fingerprint, both.fingerprint) + assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}"))) + } + + @Test + fun `class and reason wildcards reject exactly overlapping targets in either ID order`() { + val reasons = listOf(null) + TsUnknownCallFailureReason.entries + val targets = reasons.flatMap { reason -> + listOf(null, "A", "B").map { klass -> + TsUnknownCallTarget(methodName = "method", failureReason = reason, enclosingClassName = klass) + } + } + for (left in targets) for (right in targets) { + val reasonOverlaps = left.failureReason == null || right.failureReason == null || + left.failureReason == right.failureReason + val classOverlaps = left.enclosingClassName == null || right.enclosingClassName == null || + left.enclosingClassName == right.enclosingClassName + val models = listOf(FakeModel(id = "a", target = left), FakeModel(id = "b", target = right)) + + if (reasonOverlaps && classOverlaps) { + assertFailsWith { TsUnknownCallModelCatalog(models) } + assertFailsWith { + TsUnknownCallModelCatalog( + listOf(FakeModel(id = "b", target = left), FakeModel(id = "a", target = right)) + ) + } + } else { + assertSelections(models) + } + } + } + + private fun assertSelections(models: List) { + val catalog = TsUnknownCallModelCatalog(models) + for (reason in TsUnknownCallFailureReason.entries) for (klass in listOf("A", "B", "C")) { + val expected = models.singleOrNull { + (it.target.failureReason == null || it.target.failureReason == reason) && + (it.target.enclosingClassName == null || it.target.enclosingClassName == klass) + } + assertSame(expected, catalog.select(call(klass, reason))) + } + } + + @Test + fun `built in models are discovered once and an explicit empty selection disables all`() { + val catalog = TsBuiltInUnknownCallModels.catalog() + + assertEquals(listOf(TsArrayShiftIntrinsicModel.MODEL_ID), catalog.modelIds) + assertSame(catalog, TsBuiltInUnknownCallModels.catalog()) + assertFailsWith { (catalog.modelIds as MutableList).clear() } + assertEquals(listOf(TsArrayShiftIntrinsicModel.MODEL_ID), TsBuiltInUnknownCallModels.catalog().modelIds) + assertTrue(TsBuiltInUnknownCallModels.catalog(TsUnknownCallModelSelection.Only(emptySet())).modelIds.isEmpty()) + } + + @Test + fun `fingerprints preserve ID boundaries and no match remains distinct from ambiguity`() { + val left = TsUnknownCallModelCatalog(listOf(model(id = "ab"), model(id = "c"))) + val right = TsUnknownCallModelCatalog(listOf(model(id = "a"), model(id = "bc"))) + + assertNotEquals(left.fingerprint, right.fingerprint) + assertNull(left.select(call(className = "A", reason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION))) + } + + private fun call(className: String, reason: TsUnknownCallFailureReason) = TsUnknownCall( + callee = EtsMethodSignature( + enclosingClass = EtsClassSignature.UNKNOWN.copy(name = className), + name = "method", + parameters = emptyList(), + returnType = EtsUnknownType, + ), + receiver = null, + arguments = emptyList(), + resultType = EtsUnknownType, + callSite = callSite, + failureReason = reason, + ) + + private fun model( + id: String, + methodName: String = "target-$id", + failureReason: TsUnknownCallFailureReason? = null, + className: String? = null, + ): TsUnknownCallModel = FakeModel( + id = id, + target = TsUnknownCallTarget( + methodName = methodName, + failureReason = failureReason, + enclosingClassName = className, + ), + ) + + private class FakeModel( + override val id: String, + override val target: TsUnknownCallTarget, + ) : TsUnknownCallModel { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution = + error("Fake model must not execute in catalog metadata tests") + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 3e81ed3d1..2f950432f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -45,6 +45,7 @@ import org.usvm.machine.expr.extractInt import org.usvm.machine.expr.toConcreteBoolValue import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.memory.ULValue import org.usvm.memory.UReadOnlyMemory import org.usvm.mkSizeExpr @@ -241,7 +242,7 @@ open class TsTestStateResolver( } is EtsArrayType -> { - resolveTsArray(concreteRef, heapRef, type) + resolveTsArray(heapRef, type) } is EtsUnknownType -> { @@ -261,7 +262,6 @@ open class TsTestStateResolver( } private fun resolveTsArray( - concreteRef: UConcreteHeapRef, heapRef: UHeapRef, type: EtsArrayType, ): TsTestValue.TsArray<*> = with(ctx) { @@ -273,38 +273,21 @@ open class TsTestStateResolver( val sort = typeToSort(type.elementType) if (sort is TsUnresolvedSort) { - val arrayIndexLValue = mkArrayIndexLValue(addressSort, concreteRef, index, type) - val fakeObject = if (memory is UModel) { - resolvedLValuesToFakeObjects.firstOrNull { it.first == arrayIndexLValue }?.second - } else { - resolvedLValuesToFakeObjects.lastOrNull { it.first == arrayIndexLValue }?.second + val value = readUnresolvedArrayElement(memory, heapRef, index) + val currentRef = evaluateInModel(value.refValue) + if (currentRef.isFakeObject()) { + return@map resolveFakeObject(currentRef) } - fakeObject ?: return@map TsTestValue.TsUndefined - - check(fakeObject.isFakeObject()) - - val fakeType = fakeObject.getFakeType(finalStateMemory) return@map when { - model.eval(fakeType.fpTypeExpr).isTrue -> { - resolveExpr(fakeObject.extractFp(finalStateMemory)) - } - - model.eval(fakeType.boolTypeExpr).isTrue -> { - resolveExpr(fakeObject.extractBool(finalStateMemory)) - } - - model.eval(fakeType.refTypeExpr).isTrue -> { - resolveExpr(fakeObject.extractRef(finalStateMemory)) - } - - else -> { - error("Unsupported fake object type: $fakeType") - } + model.eval(value.type.fpTypeExpr).isTrue -> resolveExpr(value.fpValue) + model.eval(value.type.boolTypeExpr).isTrue -> resolveExpr(value.boolValue) + model.eval(value.type.refTypeExpr).isTrue -> resolveExpr(value.refValue) + else -> TsTestValue.TsUndefined // An unread input element is unconstrained. } } - require(sort is UFpSort || sort is UBoolSort) { + require(sort is UFpSort || sort is UBoolSort || sort is UAddressSort) { "Other sorts must be resolved above, but got: $sort" } diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index c78d4027f..e37b10172 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,31 @@ 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(); + } + + knownReceiverMethodContinues(receiver: KnownReceiver): number { + receiver.known(); + return 102; + } + + arrayShiftWithArgument(): number { + const values = [10, 20]; + return values.shift(17); + } + anyReceiverWithKnownMethodContinues(receiver: any): number { receiver.known(); return 102; diff --git a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts new file mode 100644 index 000000000..146989eed --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts @@ -0,0 +1,153 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +class ArrayElement {} + +export class ArrayShiftIntrinsic { + unknownValue(value: any): any { + return value; + } + + emptyArray(): number | undefined { + const values: number[] = []; + return values.shift(); + } + + nonEmptyArray(): number { + const values = [10, 20, 30]; + return values.shift()! + values[0] + values.length; + } + + aliasedElement(): number { + const first = new ArrayElement(); + const second = new ArrayElement(); + const values: ArrayElement[] = [first, second]; + if (values.shift() === first && values[0] === second && values.length === 1) { + return 42; + } + + return 0; + } + + symbolicNumberArray(values: number[]): number { + values.shift(); + return 46; + } + + symbolicUnknownArray(values: any[]): number { + if (values.length < 2) { + return 0; + } + + const oldLength = values.length; + const firstType = typeof values[0]; + const secondType = typeof values[1]; + const removedType = typeof values.shift(); + if (removedType === firstType && typeof values[0] === secondType && values.length === oldLength - 1) { + return 47; + } + + return 1; + } + + mixedUnknownArray(): number { + const element = new ArrayElement(); + const values: any[] = [10, true, element]; + const removed = values.shift(); + if (removed === 10 && values[0] === true && values[1] === element && values.length === 2) { + return 49; + } + + return 0; + } + + emptyUnknownArray(): any { + const values: any[] = []; + return values.shift(); + } + + shiftWithArguments(): number { + const values = [1]; + values.shift(0); + return 48; + } + + readBeforeShift(values: any[]): number { + if (values.length !== 2) { + return 0; + } + + values[0] = 10; + values.shift(); + return values[0] === 20 ? 1 : 2; + } + + writeThroughSymbolicIndex(values: any[], index: number): any { + if (values.length !== 2 || index !== 0) { + return 0; + } + + values[0] = 10; + values[index] = 20; + return values[0]; + } + + shiftedWrittenUnknownArray(values: any[]): any[] { + if (values.length !== 2) { + return []; + } + + values[0] = 10; + values[1] = 20; + values.shift(); + return values; + } + + numberArrayThroughAnyAlias(): number { + const original: number[] = [10, 20]; + const values: any[] = original; + return values.shift() === 10 && original[0] === 20 && values.length === 1 ? 1 : 0; + } + + booleanArrayThroughUnknownAlias(): number { + const original: boolean[] = [true, false]; + const values: unknown[] = original; + return values.shift() === true && original[0] === false && values.length === 1 ? 1 : 0; + } + + conditionalFakeElement(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values: any[] = [10, true]; + values[index] = 20; + const removed = values.shift(); + if (index === 0) return removed === 20 && values[0] === true ? 1 : -1; + return removed === 10 && values[0] === 20 ? 1 : -1; + } + + conditionalArray(flag: boolean): number { + const first: any[] = [10, true]; + const second: any[] = [false, 20]; + const values: any[] = flag ? first : second; + const removed = values.shift(); + if (flag) return removed === 10 && values[0] === true && first.length === 1 && second.length === 2 ? 1 : 0; + return removed === false && values[0] === 20 && second.length === 1 && first.length === 2 ? 1 : 0; + } + + conditionalEmptyArray(flag: boolean): number { + const first: any[] = [10, true]; + const second: any[] = []; + const values: any[] = flag ? first : second; + const removed = values.shift(); + if (flag) return removed === 10 && values[0] === true && first.length === 1 && second.length === 0 ? 1 : 0; + return removed === undefined && first.length === 2 && second.length === 0 ? 1 : 0; + } + + pushAfterShift(): number { + const element = new ArrayElement(); + const values: any[] = [10, true, element]; + const first = values.shift(); + values.push(null); + return first === 10 && values.shift() === true && values.shift() === element && + values.shift() === null && values.shift() === undefined && values.length === 0 ? 1 : 0; + } +} diff --git a/usvm-ts/src/test/resources/models/InstanceCallReceiver.ts b/usvm-ts/src/test/resources/models/InstanceCallReceiver.ts new file mode 100644 index 000000000..b78f1321e --- /dev/null +++ b/usvm-ts/src/test/resources/models/InstanceCallReceiver.ts @@ -0,0 +1,204 @@ +// @ts-nocheck +class ReceiverObject { + value: number = 42; + read(): number { return this.value; } + shift(): number { return 99; } +} + +export class InstanceCallReceiver { + wrappedShift(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const receiver = box[0]; + return receiver.shift() === 10 && values[0] === 20 && values.length === 1 ? 1 : -1; + } + + wrappedPop(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const receiver = box[0]; + return receiver.pop() === 20 && values[0] === 10 && values.length === 1 ? 1 : -1; + } + + wrappedPush(): number { + const values = [10]; + const box: any[] = [values, true]; + const receiver = box[0]; + return receiver.push(20) === 2 && values[1] === 20 ? 1 : -1; + } + + wrappedReverse(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const receiver = box[0]; + receiver.reverse(); + return values[0] === 20 && values[1] === 10 ? 1 : -1; + } + + wrappedFill(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + box[0].fill(7); + return values[0] === 7 && values[1] === 7 ? 1 : -1; + } + + wrappedUnshift(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + return box[0].unshift(7) === 3 && values[0] === 7 && values[1] === 10 ? 1 : -1; + } + + wrappedSlice(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(1); + return result.length === 1 && result[0] === 20 && values.length === 2 ? 1 : -1; + } + + wrappedSliceReversed(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(1, 0); + return result.length === 0 && values.length === 2 ? 1 : -1; + } + + wrappedSlicePastEnd(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(1, 10); + return result.length === 1 && result[0] === 20 && values.length === 2 ? 1 : -1; + } + + wrappedSlicePastStart(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(10); + return result.length === 0 && values.length === 2 ? 1 : -1; + } + + wrappedSliceNegative(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(-10, -1); + return result.length === 1 && result[0] === 10 && values.length === 2 ? 1 : -1; + } + + wrappedSliceEmpty(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].slice(1, 1); + return result.length === 0 && values.length === 2 ? 1 : -1; + } + + wrappedConcat(): number { + const values = [10, 20]; + const box: any[] = [values, true]; + const result = box[0].concat([30]); + return result.length === 3 && result[2] === 30 && values.length === 2 ? 1 : -1; + } + + wrappedUserMethod(): number { + const object = new ReceiverObject(); + const box: any[] = [object, true]; + return box[0].read() === 42 ? 1 : -1; + } + + customShift(): number { + const object = new ReceiverObject(); + const box: any[] = [object, true]; + return box[0].shift() === 99 ? 1 : -1; + } + + conditionalArrays(index: number): number { + if (index !== 0 && index !== 1) return 0; + const numbers = [10, 20]; + const booleans = [true, false]; + const box: any[] = [numbers, true]; + box[index] = booleans; + const receiver = box[0]; + const result = receiver.shift(); + if (index === 0) return result === true && booleans[0] === false && numbers.length === 2 ? 1 : -1; + return result === 10 && numbers[0] === 20 && booleans.length === 2 ? 1 : -1; + } + + conditionalEmptyArray(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values: any[] = [10, true]; + const empty: any[] = []; + const box: any[] = [values, false]; + box[index] = empty; + const result = box[0].shift(); + if (index === 0) return result === undefined && values.length === 2 ? 1 : -1; + return result === 10 && values[0] === true && empty.length === 0 ? 1 : -1; + } + + arrayOrUserMethod(index: number): number { + if (index !== 0 && index !== 1) return 0; + const values = [10, 20]; + const object = new ReceiverObject(); + const box: any[] = [values, true]; + box[index] = object; + const result = box[0].shift(); + if (index === 0) return result === 99 && values.length === 2 ? 1 : -1; + return result === 10 && values.length === 1 ? 1 : -1; + } + + primitiveValueOf(index: number): number { + if (index !== 0 && index !== 1) return 0; + const box: any[] = [17, true]; + const receiver = box[index]; + return receiver.valueOf() === receiver ? 1 : -1; + } + + primitiveToString(index: number): number { + if (index !== 0 && index !== 1) return 0; + const box: any[] = [17, true]; + return typeof box[index].toString() === 'string' ? 1 : -1; + } + + constrainedFake(value: any): number { + if (value !== 17 && value !== true) return 0; + const result = value.valueOf(); + if (result === 17) return 1; + if (result === true) return 2; + return -1; + } + + nullableReceiver(index: number): number { + if (index !== 0 && index !== 1) return 0; + const object = new ReceiverObject(); + const box: any[] = [object, null]; + return box[index].read() === 42 ? 1 : -1; + } + + undefinedReceiver(index: number): number { + if (index !== 0 && index !== 1) return 0; + const object = new ReceiverObject(); + const box: any[] = [object, undefined]; + return box[index].read() === 42 ? 1 : -1; + } + + nullToString(): number { + const box: any[] = [null, 17, true]; + box[0].toString(); + return -1; + } + + undefinedValueOf(): number { + const box: any[] = [undefined, 17, true]; + box[0].valueOf(); + return -1; + } + + nullShift(): number { + const box: any[] = [null, 17, true]; + box[0].shift(); + return -1; + } + + undefinedShift(): number { + const box: any[] = [undefined, 17, true]; + box[0].shift(); + return -1; + } +}