diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt index 6bc1c30b6f..5aabcb08cb 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt @@ -276,6 +276,7 @@ internal class CallsExperimentRunner( private val symbolicEngine: CallsSymbolicEngine, private val targetReplayer: CallsTargetReplayer, private val runtimeToolRevision: String = CallsBuildIdentity.toolRevision, + private val eventRecordWriter: ((Path, CallsRawRecord) -> Unit)? = null, ) { fun run( manifest: CallsExperimentManifest, @@ -387,7 +388,10 @@ internal class CallsExperimentRunner( target = target, seed = seed, profile = profile, - appendUnknownCall = { event -> append(rawOutput, event) }, + appendUnknownCall = { event -> + val writer = eventRecordWriter + if (writer == null) append(rawOutput, event) else writer(rawOutput, event) + }, ) append(rawOutput, result) @@ -417,18 +421,22 @@ internal class CallsExperimentRunner( seed = seed, budget = manifest.perTargetBudgetMillis.milliseconds, ) + val eventWrites = CallsEventWriteTracker() + val unknownCallSink = callsUnknownCallEventSink( + cell = request.cellIdentity(experimentId = manifest.experimentId), + appendAndFlush = appendUnknownCall, + ) + val runtimeLimitationSink = callsRuntimeLimitationEventSink( + cell = request.cellIdentity(experimentId = manifest.experimentId), + appendAndFlush = appendUnknownCall, + ) val symbolic = symbolicEngine.search( request.copy( - unknownCallEventSink = callsUnknownCallEventSink( - cell = request.cellIdentity(experimentId = manifest.experimentId), - appendAndFlush = appendUnknownCall, - ), - runtimeLimitationEventSink = callsRuntimeLimitationEventSink( - cell = request.cellIdentity(experimentId = manifest.experimentId), - appendAndFlush = appendUnknownCall, - ), + unknownCallEventSink = eventWrites.track(unknownCallSink), + runtimeLimitationEventSink = eventWrites.track(runtimeLimitationSink), ), ) + eventWrites.requireComplete() val replay = symbolic.inputs?.let { inputs -> targetReplayer.replay( sourceRoots = listOf(sourceRoot), @@ -477,6 +485,23 @@ internal class CallsExperimentRunner( } } +private class CallsEventWriteTracker { + private var firstFailure: Throwable? = null + + fun track(sink: (T) -> Unit): (T) -> Unit = { event -> + runCatching { sink(event) }.getOrElse { error -> + if (firstFailure == null) firstFailure = error + throw error + } + } + + fun requireComplete() { + firstFailure?.let { error -> + throw IllegalStateException("Could not persist a Calls event", error) + } + } +} + internal data class CallsValidatedRawResults( val metadata: CallsRunMetadata, val results: List, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt index acfad26830..23bfa160e4 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt @@ -187,6 +187,7 @@ internal class OriginalTypeScriptTargetReplayer : CallsTargetReplayer { marker = marker, resultPath = resultPath, targetMode = target.mode, + sourceArgumentCount = inputs.size, ), ) val replayRoots = sourceRoots.mapIndexed { index, root -> @@ -344,6 +345,7 @@ internal class OriginalTypeScriptTargetReplayer : CallsTargetReplayer { marker: String, resultPath: Path, targetMode: CallsSourceTargetMode, + sourceArgumentCount: Int, ): String = """ import { writeFileSync } from 'node:fs'; import * as targetModule from ${jsString("./$sourcePath")}; @@ -361,7 +363,7 @@ internal class OriginalTypeScriptTargetReplayer : CallsTargetReplayer { let invocation: 'returned' | 'threw' = 'returned'; let caught: unknown; try { - const result = callable(...args); + const result = callable(...args.slice(0, $sourceArgumentCount)); if (result !== null && (typeof result === 'object' || typeof result === 'function') && typeof (result as { then?: unknown }).then === 'function') { void Promise.resolve(result).catch(() => undefined); diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 5d309c1c6d..05cbfe76c5 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -109,8 +109,8 @@ internal class CurrentTsCallsSymbolicEngine( ) : CallsSymbolicEngine { private val verifiedProjects = mutableMapOf() private val preparedFunctions = mutableMapOf() - private val preparedTargets = mutableMapOf() private val loadedSources = mutableMapOf() + private var preparedTarget: Pair? = null private var verifiedNativeFrontendIdentity: String? = null override fun search(request: CallsSymbolicSearchRequest): CallsSymbolicSearchResult { @@ -372,9 +372,8 @@ internal class CurrentTsCallsSymbolicEngine( } private fun prepareSafely(request: CallsSymbolicPreflightRequest): CallsTargetPreparation { - preparedTargets[request]?.takeIf { - verifiedProjects[request.sourceRoot] == request.project.revision - }?.let { preparation -> return preparation } + preparedTarget?.takeIf { (cachedRequest, _) -> cachedRequest == request } + ?.let { (_, preparation) -> return preparation } val preparation = runCatching { prepare(request) }.getOrElse { error -> CallsTargetPreparation.Rejected( @@ -383,7 +382,9 @@ internal class CurrentTsCallsSymbolicEngine( diagnostic = error.message ?: error::class.java.name, ) } - preparedTargets[request] = preparation + if (preparation !is CallsTargetPreparation.Rejected || preparation.status != CallsSymbolicStatus.TOOL_ERROR) { + preparedTarget = request to preparation + } return preparation } diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt index 97f4fdb237..3c17bc6916 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt @@ -62,6 +62,42 @@ class CallsExperimentTest { assertEquals(4, CallsExperimentAggregator.summarize(rawOutput).resultRows) } + @Test + fun `runner does not publish completion after an observer write failure`(@TempDir directory: Path) { + val source = Path.of(checkNotNull(javaClass.getResource("/calls/SourceTargetReplayFixture.ts")).toURI()) + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val method = file.allClasses.flatMap { cls -> cls.methods } + .single { candidate -> candidate.name == "completesReturnExpression" } + val callSite = method.cfg.stmts.first { statement -> statement.location.origin != null } + val event = TsUnknownCallEvent( + callSite = callSite, + callee = method.signature, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + decision = TsUnknownCallDecision.ResidualFallback(policy = TsResidualCallPolicy.STOP_PATH), + ) + val engine = CallsSymbolicEngine { request -> + runCatching { checkNotNull(request.unknownCallEventSink).invoke(event) } + result(status = CallsSymbolicStatus.UNREACHED) + } + val rawOutput = directory.resolve("results.jsonl") + + val failure = assertFailsWith { + CallsExperimentRunner( + symbolicEngine = engine, + targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> error("No witness to replay") }, + runtimeToolRevision = FIXTURE_TOOL_REVISION, + eventRecordWriter = { _, _ -> error("Event write failed") }, + ).run( + manifest = manifest(sourceRoot = ".", seeds = listOf(17L)), + manifestDirectory = directory, + rawOutput = rawOutput, + ) + } + + assertTrue(failure.message.orEmpty().contains("Calls event")) + assertFalse(Files.exists(rawOutput)) + } + @Test fun `legacy source target defaults to entry mode`() { val encoded = """ diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt index 6ed05bab21..82615b6b23 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsSourceReplayTest.kt @@ -30,6 +30,23 @@ class CallsSourceReplayTest { assertEquals(CallsReplayStatus.REJECTED, replacement.status, replacement.toString()) } + @Test + fun `replays a zero-input export without the FastCheck placeholder`() { + val fixture = fixture() + val zeroArguments = fixture.target(functionName = "checksArgumentCount", statement = "return 0;") + val extraArgument = fixture.target(functionName = "checksArgumentCount", statement = "return 1;") + + val reached = fixture.replay(exportName = "checksArgumentCount", inputs = emptyList(), target = zeroArguments) + val notReached = fixture.replay( + exportName = "checksArgumentCount", + inputs = emptyList(), + target = extraArgument, + ) + + assertEquals(CallsReplayStatus.CONFIRMED, reached.status, reached.toString()) + assertEquals(CallsReplayStatus.REJECTED, notReached.status, notReached.toString()) + } + @Test fun `confirms only the exact source statement reached by original TypeScript`() { val fixture = fixture() diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt index eae4461b3d..dd03abcbc2 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngineTest.kt @@ -240,6 +240,35 @@ class CurrentTsCallsSymbolicEngineTest { } } + @Test + fun `preflight retries a transient tool error for the same target`() { + val fixture = fixture( + source = "export function answer(): number { return 42; }", + exportName = "answer", + inputs = emptyList(), + targetStatement = "return 42;", + ) + val environment = mutableMapOf("ETS_FRONTEND_DIR" to "/unused/frontend") + val engine = CurrentTsCallsSymbolicEngine( + environment = environment::get, + bundledNativeFrontendRevision = "bundled:test", + ) + val request = CallsSymbolicPreflightRequest( + sourceRoot = fixture.sourceRoot, + project = fixture.project, + function = fixture.function, + target = fixture.target, + expectedNativeFrontendRevision = "bundled:test", + ) + + val first = engine.preflight(request) + environment.clear() + val second = engine.preflight(request) + + assertEquals(CallsSymbolicPreflightStatus.TOOL_ERROR, first.status) + assertTrue(second.status != CallsSymbolicPreflightStatus.TOOL_ERROR, second.toString()) + } + @Test fun `extracts nonempty generic number array containing zero and replays source`() { val fixture = fixture( diff --git a/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts index fe695f2760..847ca6aa25 100644 --- a/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts +++ b/usvm-ts-calls/src/test/resources/calls/SourceTargetReplayFixture.ts @@ -11,6 +11,13 @@ export function throwsAtTarget(): never { throw new Error('expected'); } +export function checksArgumentCount(): number { + if (arguments.length !== 0) { + return 1; + } + return 0; +} + export function importOnlyTarget(): number { return 7; } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt index 5db429b4d2..b278d498dc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt @@ -22,6 +22,18 @@ object TsBuiltInUnknownCallModels { } private val allModels by lazy { TsUnknownCallModelCatalog(models) } + internal fun hasPartialApproximationModel( + methodName: String, + enclosingClassName: String, + allowUnqualifiedTarget: Boolean = false, + ): Boolean = + allModels.hasTarget( + methodName = methodName, + enclosingClassName = enclosingClassName, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + allowUnqualifiedTarget = allowUnqualifiedTarget, + ) + 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 c2acf85443..73488da1b5 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 @@ -1,27 +1,20 @@ package org.usvm.machine.call -import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsCallExpr -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsInstanceCallExpr import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsPtrCallExpr import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UExpr import org.usvm.api.mockMethodCall -import org.usvm.api.typeStreamOf import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsVirtualMethodCallStmt 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.types.singleOrNull /** * A call that the regular TypeScript execution pipeline could not execute. @@ -150,12 +143,8 @@ internal fun TsUnknownCallDispatcher.dispatch( is EtsPtrCallExpr -> call.ptr else -> null } - val receiverIsDate = (call as? EtsInstanceCallExpr)?.let { instanceCall -> - scope.calcOnState { isDateReceiver(instanceCall, resolvedReceiver) } - } ?: false - val normalizedCallee = call.canonicalizeDateCallee(callee, receiverIsDate) val unknownCall = TsUnknownCall( - callee = normalizedCallee, + callee = callee, receiver = receiverSource?.let { TsUnknownCallValue(it, resolvedReceiver) }, arguments = call.args.zip(resolvedArguments) { source, resolved -> TsUnknownCallValue(source, resolved) @@ -168,43 +157,6 @@ internal fun TsUnknownCallDispatcher.dispatch( return dispatch(scope, unknownCall) } -internal fun EtsInstanceCallExpr.hasDateReceiver(): Boolean = - instance.name == "Date" || when (val type = instance.type) { - is EtsClassType -> type.signature.name == "Date" - is EtsUnclearRefType -> type.typeName == "Date" - else -> false - } - -internal fun TsState.isDateReceiver( - call: EtsInstanceCallExpr, - receiver: UExpr<*>?, -): Boolean { - if (call.hasDateReceiver()) { - return true - } - if (receiver?.sort != ctx.addressSort) { - return false - } - - val runtimeType = memory.typeStreamOf(receiver.asExpr(ctx.addressSort)).singleOrNull() - return (runtimeType as? EtsClassType)?.signature?.name == "Date" -} - -private fun EtsCallExpr.canonicalizeDateCallee( - callee: EtsMethodSignature, - receiverIsDate: Boolean, -): EtsMethodSignature { - if (callee.enclosingClass.name == "Date") { - return callee - } - - if (!receiverIsDate) { - return callee - } - - return callee.copy(enclosingClass = EtsClassSignature.UNKNOWN.copy(name = "Date")) -} - internal fun TsUnknownCallDispatcher.dispatch( scope: TsStepScope, call: TsVirtualMethodCallStmt, 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 index c55afe0251..50c4d5eb5b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt @@ -2,6 +2,7 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature +import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily import org.usvm.machine.state.TsState import java.util.Collections import java.util.IdentityHashMap @@ -74,13 +75,29 @@ class TsUnknownCallModelCatalog( return candidates[call.callee.enclosingClass.name] ?: candidates[null] } + internal fun hasTarget( + methodName: String, + enclosingClassName: String, + failureReason: TsUnknownCallFailureReason, + allowUnqualifiedTarget: Boolean, + ): Boolean { + val candidates = index[methodName]?.get(failureReason) ?: return false + return enclosingClassName in candidates || (allowUnqualifiedTarget && null in candidates) + } + fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication { - val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable + val directModel = select(call) + val modelCall = if (directModel == null) { + TsDateEtsIrModelFamily.canonicalModelCall(state, call) ?: call + } else { + call + } + val model = directModel ?: select(modelCall) ?: return TsUnknownCallModelApplication.NotApplicable if (state.isUnknownCallModelActive(model.id)) { return TsUnknownCallModelApplication.NotApplicable } - val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable + val execution = model.apply(state, modelCall) ?: return TsUnknownCallModelApplication.NotApplicable return TsUnknownCallModelApplication.Applied( modelId = model.id, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index c3fcd9ae5a..cd96f81b75 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -10,6 +10,7 @@ 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.initializeArray import org.usvm.api.initializeArrayLength import org.usvm.machine.call.TsEtsIrUnknownCallModel @@ -52,59 +53,74 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } - private val arrayDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> - with(state.ctx) { - val receiver = inputs.firstOrNull() - val staticType = call.receiver?.source?.type - if (staticType == null || receiver?.sort != addressSort) { - falseExpr - } else { - val array = receiver.asExpr(addressSort) - val receiverType = state.arrayStorageType(array, staticType) as? EtsArrayType + // A guard states when the source model agrees with JavaScript. Other states use the residual policy. + private val arrayReceiverGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + val (array, arrayType) = state.arrayReceiver(call, inputs) + ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + + state.memory.types.evalIsSubtype(array, arrayType) + } + + private val indexSearchGuard = missingSlotSearchGuard(skipUndefinedHoles = true) + private val includesSearchGuard = missingSlotSearchGuard(skipUndefinedHoles = false) + + private fun missingSlotSearchGuard(skipUndefinedHoles: Boolean): TsEtsIrUnknownCallModelDomainGuard { + return TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val (array, arrayType) = state.arrayReceiver(call, inputs) + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val searchElement = inputs.getOrNull(1) - val searchRef = searchElement - ?.takeIf { it.sort == addressSort } - ?.asExpr(addressSort) - if ( - array.hasFakeValueBranch() || receiverType?.dimensions != 1 || - searchRef?.hasFakeValueBranch() == true - ) { - falseExpr - } else { - val elementSort = typeToSort(receiverType.elementType) - val hasNoMissingSlots = array is UConcreteHeapRef && - state.isUnmodifiedDenseInputArray(array, receiverType) - val excludesMissingSlot = when { - searchElement == mkUndefinedValue() && - ( - call.callee.name in setOf("indexOf", "lastIndexOf") || - elementSort == fp64Sort || elementSort == boolSort - ) -> mkBool(hasNoMissingSlots) - - elementSort == fp64Sort && searchElement?.sort == fp64Sort -> { - val searchNumber = searchElement.asExpr(fp64Sort) - val zero = mkFp64(0.0) - - mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, zero))) - } - - elementSort == boolSort && searchElement?.sort == boolSort -> { - mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort)) - } - - else -> trueExpr + val searchRef = searchElement?.takeIf { it.sort == addressSort }?.asExpr(addressSort) + if (searchRef?.hasFakeValueBranch() == true) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + + val elementSort = typeToSort(arrayType.elementType) + val hasNoMissingSlots = array is UConcreteHeapRef && + state.isUnmodifiedDenseInputArray(array, arrayType) + + // Sparse slots are absent in JavaScript, but typed storage can read them as zero or false. + // indexOf/lastIndexOf skip holes when searching for undefined; includes sees holes as undefined. + val missingSlotGuard = when { + searchElement == mkUndefinedValue() && + (skipUndefinedHoles || elementSort == fp64Sort || elementSort == boolSort) -> { + mkBool(hasNoMissingSlots) } - mkAnd( - state.memory.types.evalIsSubtype(array, receiverType), - excludesMissingSlot, - ) + elementSort == fp64Sort && searchElement?.sort == fp64Sort -> { + val searchNumber = searchElement.asExpr(fp64Sort) + mkOr(mkBool(hasNoMissingSlots), mkNot(mkFpEqualExpr(searchNumber, mkFp64(0.0)))) + } + + elementSort == boolSort && searchElement?.sort == boolSort -> { + mkOr(mkBool(hasNoMissingSlots), searchElement.asExpr(boolSort)) + } + + else -> trueExpr } + + mkAnd(state.memory.types.evalIsSubtype(array, arrayType), missingSlotGuard) } } } - private val pushDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + private fun TsState.arrayReceiver( + call: TsUnknownCall, + inputs: List>, + ): Pair? = with(ctx) { + val receiver = inputs.firstOrNull() + ?.takeIf { it.sort == addressSort } + ?.asExpr(addressSort) + ?: return null + val staticType = call.receiver?.source?.type ?: return null + val arrayType = arrayStorageType(receiver, staticType) as? EtsArrayType ?: return null + if (receiver.hasFakeValueBranch() || arrayType.dimensions != 1) return null + + receiver to arrayType + } + + private val pushGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr val arguments = call.arguments.map { argument -> @@ -117,22 +133,24 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state.boundedArrayGuard(array, arrayType, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY - arguments.size) } - private val fillDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + private val fillGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr val value = call.arguments.firstOrNull()?.resolved ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - val valueMatchesArrayType = state.argumentsMatchArrayType(arrayType, listOf(value)) - val fillsWholeArray = call.arguments.size == 1 - val hasKnownSlotValues = fillsWholeArray || state.isUnmodifiedDenseInputArray(array, arrayType) - if (!valueMatchesArrayType || !hasKnownSlotValues) { + if (!state.argumentsMatchArrayType(arrayType, listOf(value))) { + return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr + } + + // A whole-array fill overwrites holes. A range fill must preserve slots outside its range. + if (call.arguments.size != 1 && !state.isUnmodifiedDenseInputArray(array, arrayType)) { return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr } state.boundedArrayGuard(array, arrayType, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY) } - private val denseReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + private val denseInputGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr if (!state.isUnmodifiedDenseInputArray(array, arrayType)) { @@ -142,7 +160,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state.boundedArrayGuard(array, arrayType, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY) } - private val unshiftDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + private val unshiftGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr val arguments = call.arguments.map { argument -> @@ -158,7 +176,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state.boundedArrayGuard(array, arrayType, maximumLength = SOURCE_ARRAY_MODEL_CAPACITY - arguments.size) } - private val concatDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + private val concatGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr val other = inputs.getOrNull(1) as? UConcreteHeapRef @@ -335,51 +353,54 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { id = "ts.array.indexOf", methodName = "indexOf", inputAdapter = optionalFromIndexAdapter, + domainGuard = indexSearchGuard, ), sourceModel( id = "ts.array.includes", methodName = "includes", inputAdapter = optionalFromIndexAdapter, + domainGuard = includesSearchGuard, ), sourceModel( id = "ts.array.lastIndexOf", methodName = "lastIndexOf", inputAdapter = optionalLastIndexAdapter, + domainGuard = indexSearchGuard, ), sourceModel( id = "ts.array.push", methodName = "push", inputAdapter = variadicMutationAdapter, - domainGuard = pushDomain, + domainGuard = pushGuard, ), sourceModel( id = "ts.array.fill", methodName = "fill", inputAdapter = fillAdapter, - domainGuard = fillDomain, + domainGuard = fillGuard, ), sourceModel( id = "ts.array.reverse", methodName = "reverse", inputAdapter = noArgumentsAdapter, - domainGuard = TsDenseArrayModelSupport.denseReceiverDomain, + domainGuard = denseInputGuard, ), sourceModel( id = "ts.array.unshift", methodName = "unshift", inputAdapter = variadicMutationAdapter, - domainGuard = unshiftDomain, + domainGuard = unshiftGuard, ), sourceModel( id = "ts.array.slice", methodName = "slice", inputAdapter = sliceAdapter, - domainGuard = denseReceiverDomain, + domainGuard = denseInputGuard, ), sourceModel( id = "ts.array.concat", methodName = "concat", - domainGuard = concatDomain, + domainGuard = concatGuard, ), primitiveModel( methodName = "grow", @@ -403,7 +424,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { id: String, methodName: String, inputAdapter: TsEtsIrUnknownCallModelInputAdapter = TsEtsIrUnknownCallModelInputAdapter.IDENTITY, - domainGuard: TsEtsIrUnknownCallModelDomainGuard = arrayDomain, + domainGuard: TsEtsIrUnknownCallModelDomainGuard = arrayReceiverGuard, ): TsUnknownCallModel { val target = TsUnknownCallTarget( methodName = methodName, @@ -461,8 +482,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName: String, arity: Int, implementation: (TsState, List>) -> TsUnknownCallModelExecution?, - ): TsUnknownCallModel = ArrayPrimitiveModel( + ): TsUnknownCallModel = TsPrimitiveUnknownCallModel( + idPrefix = "ts.array.primitive", methodName = methodName, + enclosingClassName = PRIMITIVES_CLASS_NAME, arity = arity, implementation = implementation, ) @@ -637,28 +660,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { callReturnType.dimensions == 1 } - private class ArrayPrimitiveModel( - methodName: String, - private val arity: Int, - private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, - ) : TsUnknownCallModel { - override val id: String = "ts.array.primitive.$methodName" - override val target = TsUnknownCallTarget( - methodName = methodName, - enclosingClassName = PRIMITIVES_CLASS_NAME, - failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, - ) - - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { - if (call.receiver != null || call.arguments.size != arity) { - return null - } - - val inputs = call.arguments.map { argument -> argument.resolved ?: return null } - return implementation(state, inputs) - } - } - private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" private const val ARRAY_FROM_LENGTH_ID = "ts.array.fromLength" private const val PRIMITIVE_GROW_ID = "ts.array.primitive.grow" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt index 4e32ab274b..5040590247 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDateEtsIrModelFamily.kt @@ -6,6 +6,8 @@ import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsValue import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UExpr import org.usvm.api.typeStreamOf @@ -27,6 +29,51 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val RESOURCE = "/org/usvm/machine/call/models/DateModels.ts" private val builtinDateSignature = EtsClassSignature.UNKNOWN.copy(name = DATE_CLASS) private val builtinDateType = EtsClassType(signature = builtinDateSignature) + private val getterNames = listOf( + "getDate", + "getDay", + "getFullYear", + "getHours", + "getMilliseconds", + "getMinutes", + "getMonth", + "getSeconds", + "getTime", + "getTimezoneOffset", + "getUTCDate", + "getUTCDay", + "getUTCFullYear", + "getUTCHours", + "getUTCMilliseconds", + "getUTCMinutes", + "getUTCMonth", + "getUTCSeconds", + "toISOString", + "valueOf", + ) + + /** Normalize only model lookup; residual calls and observation retain the frontend signature. */ + internal fun canonicalModelCall(state: TsState, call: TsUnknownCall): TsUnknownCall? { + if (call.callee.enclosingClass.name == DATE_CLASS) return null + + val receiverValue = call.receiver ?: return null + if (!isDateReceiver(state, receiverValue.source, receiverValue.resolved)) return null + + return call.copy(callee = call.callee.copy(enclosingClass = builtinDateSignature)) + } + + internal fun isDateReceiver(state: TsState, source: EtsValue, receiver: UExpr<*>?): Boolean { + val sourceLooksDate = (source as? EtsLocal)?.name == DATE_CLASS || when (val type = source.type) { + is EtsClassType -> type.signature.name == DATE_CLASS + is EtsUnclearRefType -> type.typeName == DATE_CLASS + else -> false + } + if (sourceLooksDate) return true + if (receiver?.sort != state.ctx.addressSort) return false + + val runtimeType = state.memory.typeStreamOf(receiver.asExpr(state.ctx.addressSort)).singleOrNull() + return (runtimeType as? EtsClassType)?.signature?.name == DATE_CLASS + } private val artifact by lazy { loadBundledEtsIrUnknownCallModelArtifact( @@ -43,28 +90,7 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { add(utcModel()) add(nowModel()) - for (methodName in listOf( - "getDate", - "getDay", - "getFullYear", - "getHours", - "getMilliseconds", - "getMinutes", - "getMonth", - "getSeconds", - "getTime", - "getTimezoneOffset", - "getUTCDate", - "getUTCDay", - "getUTCFullYear", - "getUTCHours", - "getUTCMilliseconds", - "getUTCMinutes", - "getUTCMonth", - "getUTCSeconds", - "toISOString", - "valueOf", - )) { + for (methodName in getterNames) { add(instanceModel(idSuffix = methodName, methodName = methodName, consumedArgs = 0)) } @@ -195,14 +221,15 @@ internal object TsDateEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { while (arguments.size < MAX_CONSTRUCTOR_ARGUMENTS) { arguments += mkFp64(0.0) } - val argumentCount = mkFp64(call.arguments.size.toDouble()) - val clock = mkFp64(nowMilliseconds ?: 0.0) + val providedArgumentCount = mkFp64(call.arguments.size.toDouble()) + val fallbackClock = mkFp64(nowMilliseconds ?: 0.0) - listOf( - receiver, - argumentCount, - clock, - ) + arguments + buildList { + add(receiver) + add(providedArgumentCount) + add(fallbackClock) + addAll(arguments) + } } }, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt new file mode 100644 index 0000000000..02d61c91e7 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt @@ -0,0 +1,34 @@ +package org.usvm.machine.call.intrinsic + +import org.usvm.UExpr +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.state.TsState + +/** Dispatches a helper method used by an EtsIR source model. */ +internal class TsPrimitiveUnknownCallModel( + idPrefix: String, + methodName: String, + enclosingClassName: String, + private val arity: Int, + private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, +) : TsUnknownCallModel { + override val id: String = "$idPrefix.$methodName" + override val target = TsUnknownCallTarget( + methodName = methodName, + enclosingClassName = enclosingClassName, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + if (call.receiver != null || call.arguments.size != arity) { + return null + } + + val inputs = call.arguments.map { argument -> argument.resolved ?: return null } + return implementation(state, inputs) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index 2cccaf1233..58e708feba 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -432,8 +432,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { methodName: String, arity: Int, implementation: (TsState, List>) -> TsUnknownCallModelExecution?, - ): TsUnknownCallModel = StringPrimitiveModel( + ): TsUnknownCallModel = TsPrimitiveUnknownCallModel( + idPrefix = "ts.string.primitive", methodName = methodName, + enclosingClassName = PRIMITIVES_CLASS_NAME, arity = arity, implementation = implementation, ) @@ -586,28 +588,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { return listOf(resolvedReceiver) + resolvedArguments } - private class StringPrimitiveModel( - methodName: String, - private val arity: Int, - private val implementation: (TsState, List>) -> TsUnknownCallModelExecution?, - ) : TsUnknownCallModel { - override val id: String = "ts.string.primitive.$methodName" - override val target = TsUnknownCallTarget( - methodName = methodName, - enclosingClassName = PRIMITIVES_CLASS_NAME, - failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, - ) - - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { - if (call.receiver != null || call.arguments.size != arity) { - return null - } - - val inputs = call.arguments.map { argument -> argument.resolved ?: return null } - return implementation(state, inputs) - } - } - private const val PRIMITIVE_LENGTH_ID = "ts.string.primitive.length" private const val PRIMITIVE_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt" private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit" 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 aa9aec6e02..9c4b0c97e9 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 @@ -23,11 +23,12 @@ import org.usvm.getIntValue import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.TsBuiltInUnknownCallModels import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModelDispatcher import org.usvm.machine.call.dispatch import org.usvm.machine.call.hasBuiltinGlobalOwner -import org.usvm.machine.call.isDateReceiver +import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily import org.usvm.machine.expr.TsExprApproximationResult.Companion.from import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.markResolved @@ -48,26 +49,6 @@ import org.usvm.util.mkArrayLengthLValue import org.usvm.util.resolveEtsMethods private val logger = KotlinLogging.logger {} -private val legacyArrayMethods = setOf("concat", "fill", "join", "push", "reduce", "reverse", "slice", "unshift") - -private val modeledStringMethods = setOf( - "split", - "replaceAll", - "substring", - "trim", - "trimStart", - "trimEnd", - "charAt", - "charCodeAt", - "endsWith", - "includes", - "indexOf", - "lastIndexOf", - "slice", - "startsWith", - "toLowerCase", - "toUpperCase", -) internal fun TsExprResolver.tryApproximateGlobalInstanceCall( expr: EtsInstanceCallExpr, @@ -168,7 +149,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `.valueOf()` method calls if (expr.callee.name == "valueOf") { - val receiverIsDate = scope.calcOnState { isDateReceiver(expr, instance) } + val receiverIsDate = scope.calcOnState { + TsDateEtsIrModelFamily.isDateReceiver( + state = this, + source = expr.instance, + receiver = instance, + ) + } if (!receiverIsDate) { return from(handleValueOf(expr, instance)) } @@ -184,7 +171,15 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort - if (expr.callee.name in legacyArrayMethods && unknownCallDispatcher is TsUnknownCallModelDispatcher) { + val usesModelDispatcher = unknownCallDispatcher is TsUnknownCallModelDispatcher + val modeledArrayCall = usesModelDispatcher && TsBuiltInUnknownCallModels.hasPartialApproximationModel( + methodName = expr.callee.name, + enclosingClassName = "Array", + allowUnqualifiedTarget = true, + ) + + // join has no source model yet; the model run intentionally sends it to the residual policy. + if (modeledArrayCall || (usesModelDispatcher && expr.callee.name == "join")) { dispatchArrayModel(stmt) return TsExprApproximationResult.ResolveFailure } @@ -245,12 +240,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } - if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) { - val dispatcher = unknownCallDispatcher - if (dispatcher !is TsUnknownCallModelDispatcher) { - return TsExprApproximationResult.NoApproximation - } - + val dispatcher = unknownCallDispatcher + if (instanceType is EtsStringType && dispatcher is TsUnknownCallModelDispatcher && + TsBuiltInUnknownCallModels.hasPartialApproximationModel( + methodName = expr.callee.name, + enclosingClassName = "String", + ) + ) { dispatcher.dispatch( scope = scope, call = stmt.call, diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts index 701bb52013..bdd2433458 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/DateModels.ts @@ -178,7 +178,12 @@ export class DateModels { } static setDate(receiver: DateValue, date: number): number { - return DateModels.setDateFields(receiver, 1, date, 0, 0); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + return DateModels.replaceDate(receiver, current.year, current.month, date, current); } static setFullYear( @@ -206,11 +211,26 @@ export class DateModels { seconds: number, milliseconds: number, ): number { - return DateModels.setTimeFields(receiver, argumentCount, hours, minutes, seconds, milliseconds, 0); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + const nextMinutes = argumentCount >= 2 ? minutes : current.minutes; + const nextSeconds = argumentCount >= 3 ? seconds : current.seconds; + const nextMilliseconds = argumentCount >= 4 ? milliseconds : current.milliseconds; + return DateModels.replaceTime(receiver, current, hours, nextMinutes, nextSeconds, nextMilliseconds); } static setMilliseconds(receiver: DateValue, milliseconds: number): number { - return DateModels.setTimeFields(receiver, 4, 0, 0, 0, milliseconds, 3); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + return DateModels.replaceTime( + receiver, current, current.hours, current.minutes, current.seconds, milliseconds, + ); } static setMinutes( @@ -220,15 +240,36 @@ export class DateModels { seconds: number, milliseconds: number, ): number { - return DateModels.setTimeFields(receiver, argumentCount + 1, 0, minutes, seconds, milliseconds, 1); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + const nextSeconds = argumentCount >= 2 ? seconds : current.seconds; + const nextMilliseconds = argumentCount >= 3 ? milliseconds : current.milliseconds; + return DateModels.replaceTime(receiver, current, current.hours, minutes, nextSeconds, nextMilliseconds); } static setMonth(receiver: DateValue, argumentCount: number, month: number, date: number): number { - return DateModels.setDateFields(receiver, argumentCount + 1, 0, month, date); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + const nextDate = argumentCount >= 2 ? date : current.date; + return DateModels.replaceDate(receiver, current.year, month, nextDate, current); } static setSeconds(receiver: DateValue, argumentCount: number, seconds: number, milliseconds: number): number { - return DateModels.setTimeFields(receiver, argumentCount + 2, 0, 0, seconds, milliseconds, 2); + if (DateModels.isInvalid(receiver.timestamp)) { + return DateModels.invalidate(receiver); + } + + const current = DateModels.parts(receiver.timestamp); + const nextMilliseconds = argumentCount >= 2 ? milliseconds : current.milliseconds; + return DateModels.replaceTime( + receiver, current, current.hours, current.minutes, seconds, nextMilliseconds, + ); } static setTime(receiver: DateValue, timestamp: number): number { @@ -302,58 +343,22 @@ export class DateModels { return receiver.timestamp; } - private static setDateFields( + private static replaceTime( receiver: DateValue, - argumentCount: number, - first: number, - second: number, - third: number, - ): number { - if (DateModels.isInvalid(receiver.timestamp)) { - return DateModels.invalidate(receiver); - } - - const current = DateModels.parts(receiver.timestamp); - if (argumentCount === 1) { - return DateModels.replaceDate(receiver, current.year, current.month, first, current); - } - - return DateModels.replaceDate( - receiver, - current.year, - second, - argumentCount >= 3 ? third : current.date, - current, - ); - } - - private static setTimeFields( - receiver: DateValue, - argumentCount: number, + current: DateParts, hours: number, minutes: number, seconds: number, milliseconds: number, - firstField: number, ): number { - if (DateModels.isInvalid(receiver.timestamp)) { - return DateModels.invalidate(receiver); - } - - const current = DateModels.parts(receiver.timestamp); - const nextHours = firstField === 0 ? hours : current.hours; - const nextMinutes = firstField <= 1 && argumentCount >= 2 ? minutes : current.minutes; - const nextSeconds = firstField <= 2 && argumentCount >= 3 ? seconds : current.seconds; - const nextMilliseconds = argumentCount >= 4 ? milliseconds : current.milliseconds; - receiver.timestamp = DateModels.makeDate( current.year, current.month, current.date, - nextHours, - nextMinutes, - nextSeconds, - nextMilliseconds, + hours, + minutes, + seconds, + milliseconds, ); return receiver.timestamp; } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt index ea86f94357..67802a48a3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsDateEtsIrModelTest.kt @@ -3,12 +3,14 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr import org.jacodb.ets.utils.loadEtsFileAutoConvert import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsTestResolver @@ -16,6 +18,7 @@ import org.usvm.util.getResourcePath import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertIs +import kotlin.test.assertNotNull import kotlin.test.assertTrue import kotlin.time.Duration @@ -75,6 +78,34 @@ class TsDateEtsIrModelTest { assertNumber(methodName = "anyAliasGetTime", expected = 456.0) } + @Test + fun `Date alias model observation keeps the frontend callee`() { + val method = method("anyAliasGetTime") + val sourceCall = assertNotNull( + method.cfg.stmts.single { stmt -> stmt.callExpr?.callee?.name == "getTime" }.callExpr + ) + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + assertTrue(states.isNotEmpty()) + val dateEvents = events.filter { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId == "ts.date.getTime" + } + assertTrue(dateEvents.isNotEmpty()) + assertTrue(dateEvents.all { event -> event.callee == sourceCall.callee }) + } + @Test fun `Date model does not accept a foreign receiver cast to Date`() { assertTrue(analyze(method("castForeignReceiver")).isEmpty())