diff --git a/usvm-ts-calls/build.gradle.kts b/usvm-ts-calls/build.gradle.kts index 3d7f8f67dd..07dcd5170b 100644 --- a/usvm-ts-calls/build.gradle.kts +++ b/usvm-ts-calls/build.gradle.kts @@ -26,11 +26,13 @@ val toolStatus = providers.exec { workingDir(rootProject.projectDir) commandLine("git", "status", "--porcelain", "--untracked-files=all") }.standardOutput.asText.map(String::trim) +val nativeFrontendRevision = providers.gradleProperty("nativeFrontendRevision") + .orElse("bundled:${Versions.jacodb}") val generateBuildMetadata = tasks.register("generateBuildMetadata") { inputs.property("toolRevision", toolRevision) inputs.property("toolStatus", toolStatus) - inputs.property("jacodbVersion", Versions.jacodb) + inputs.property("nativeFrontendRevision", nativeFrontendRevision) outputs.dir(generatedBuildMetadataDirectory) doLast { @@ -42,7 +44,7 @@ val generateBuildMetadata = tasks.register("generateBuildMetadata") { metadataFile.parentFile.mkdirs() metadataFile.writeText( "tool.revision=$buildIdentity\n" + - "native.frontend.revision=bundled:${Versions.jacodb}\n", + "native.frontend.revision=${nativeFrontendRevision.get()}\n", Charsets.UTF_8, ) } 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 4d23e38cf5..5babc2eab0 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 @@ -14,6 +14,7 @@ import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.state.TsMethodResult @@ -149,6 +150,7 @@ internal class CurrentTsCallsSymbolicEngine( stateCollectionStrategy = StateCollectionStrategy.REACHED_TARGET, randomSeed = request.seed, timeout = request.budget, + solverTimeout = request.budget, solverType = SolverType.Z3, stopOnCoverage = CALLS_STOP_ON_COVERAGE, stopOnTargetsReached = false, @@ -624,19 +626,26 @@ internal class CurrentTsCallsSymbolicEngine( } } - private class UnknownCallEventSinkObserver( + internal class UnknownCallEventSinkObserver( private val sink: ((TsUnknownCallEvent) -> Unit)?, private val runtimeLimitationSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)?, ) : TsInterpreterObserver { val runtimeLimitations = linkedSetOf() + // Keep one telemetry record per unsupported storage and statement in this analysis. + private val reportedArrayStorageLimitations = hashSetOf>() + override fun onUnknownCall(event: TsUnknownCallEvent) { sink?.invoke(event) } override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { runtimeLimitations += event.reason.name - runtimeLimitationSink?.invoke(event) + if (event.reason != TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE || + reportedArrayStorageLimitations.add(event.statement to event.detail) + ) { + runtimeLimitationSink?.invoke(event) + } } } diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetryTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetryTest.kt index 82004909cf..7497bd22ba 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetryTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsUnknownCallTelemetryTest.kt @@ -4,6 +4,8 @@ import kotlinx.serialization.decodeFromString import kotlinx.serialization.encodeToString import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallEvent @@ -17,6 +19,54 @@ import kotlin.test.assertNotNull import kotlin.test.assertNull class CallsUnknownCallTelemetryTest { + @Test + fun `observer records array storage limitation once per statement and detail`() { + val source = resourcePath("/calls/SourceTargetReplayFixture.ts") + val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND) + val method = file.allClasses.flatMap { cls -> cls.methods } + .single { candidate -> candidate.name == "completesReturnExpression" } + val statements = method.cfg.stmts.take(2) + val records = mutableListOf() + val observer = CurrentTsCallsSymbolicEngine.UnknownCallEventSinkObserver( + sink = null, + runtimeLimitationSink = records::add, + ) + val arrayStorage = TsRuntimeFeatureLimitationEvent( + statement = statements[0], + reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + detail = "storage=Uint8Array", + ) + val otherStorage = arrayStorage.copy(detail = "storage=Uint16Array") + val otherStatement = arrayStorage.copy(statement = statements[1]) + val otherReason = arrayStorage.copy(reason = TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_READ) + + // Repeated callbacks represent different states reaching the same unsupported access. + observer.onRuntimeFeatureLimitation(arrayStorage) + observer.onRuntimeFeatureLimitation(arrayStorage) + observer.onRuntimeFeatureLimitation(otherStorage) + observer.onRuntimeFeatureLimitation(otherStatement) + observer.onRuntimeFeatureLimitation(otherReason) + observer.onRuntimeFeatureLimitation(otherReason) + + assertEquals( + listOf(arrayStorage, otherStorage, otherStatement, otherReason, otherReason), + records, + ) + assertEquals( + setOf("ARRAY_STORAGE_TYPE", "ARRAY_NAMED_PROPERTY_READ"), + observer.runtimeLimitations, + ) + + val nextAnalysisRecords = mutableListOf() + val nextAnalysis = CurrentTsCallsSymbolicEngine.UnknownCallEventSinkObserver( + sink = null, + runtimeLimitationSink = nextAnalysisRecords::add, + ) + nextAnalysis.onRuntimeFeatureLimitation(arrayStorage) + + assertEquals(listOf(arrayStorage), nextAnalysisRecords) + } + @Test fun `sink converts unknown call events into ordered serializable cell records`() { val source = resourcePath("/calls/SourceTargetReplayFixture.ts") 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 2560a01af9..eae4461b3d 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 @@ -19,6 +19,7 @@ import kotlin.test.assertFailsWith import kotlin.test.assertIs import kotlin.test.assertNotNull import kotlin.test.assertTrue +import kotlin.time.Duration import kotlin.time.Duration.Companion.seconds private const val ERROR_CONSTRUCTOR_MODEL_ID: String = "ts.error.constructor" @@ -94,6 +95,65 @@ class CurrentTsCallsSymbolicEngineTest { assertEquals(emptyList(), result.inputs) } + @Test + fun `partial array join with fresh string residual does not fail search`() { + val fixture = fixture( + source = """ + export function lineWrap(text: string, MAX: number = 15): string[] { + const lines: string[] = [] + + const segments = text.split(' ') + + const l = segments.length + + let line_segments: string[] = [] + let line_segments_char_count = 0 + + for (let i = 0; i < l; i++) { + const segment = segments[i] + const segment_l = segment.length + + if (line_segments_char_count + line_segments.length - 1 + segment_l > MAX) { + lines.push(line_segments.join(' ')) + line_segments = [] + line_segments_char_count = 0 + } + + line_segments.push(segment) + line_segments_char_count += segment_l + } + + if (line_segments.length > 0) { + lines.push(line_segments.join(' ')) + } + + return lines + } + """.trimIndent(), + exportName = "lineWrap", + inputs = listOf( + PropertyInput(name = "text", domain = StringDomain(maxLength = 10)), + PropertyInput(name = "MAX", domain = NumberDomain()), + ), + targetStatement = "return lines", + targetMode = CallsSourceTargetMode.COMPLETED_RETURN, + returnExpression = "lines", + sourceFileName = "src/spec/lineWrap.ts", + ) + val unknownCalls = mutableListOf() + + val result = fixture.search( + modelIds = setOf("ts.string.split", "ts.array.join", "ts.array.push"), + profile = CallsExperimentProfile.FROZEN_FRESH, + unknownCallEventSink = unknownCalls::add, + seed = 29, + budget = 30.seconds, + ) + + assertTrue(result.status != CallsSymbolicStatus.TOOL_ERROR, result.toString()) + assertTrue(unknownCalls.any { it.callee.name == "join" }, "Array.join was not exercised") + } + @Test fun `fresh array element can be assigned to numeric object field`() { val returnExpression = "{ major: parts[0] || 0, minor: parts[1] || 0, patch: parts[2] || 0 }" @@ -1180,6 +1240,8 @@ class CurrentTsCallsSymbolicEngineTest { profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null, runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null, + seed: Long = 0, + budget: Duration = 10.seconds, ): CallsSymbolicSearchResult = engine.search( CallsSymbolicSearchRequest( sourceRoot = sourceRoot, @@ -1189,8 +1251,8 @@ class CurrentTsCallsSymbolicEngineTest { profile = profile, frozenModelIds = modelIds, expectedNativeFrontendRevision = "bundled:test", - seed = 0, - budget = 10.seconds, + seed = seed, + budget = budget, unknownCallEventSink = unknownCallEventSink, runtimeLimitationEventSink = runtimeLimitationEventSink, ) 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 7ab3d97d96..4f1bef93db 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt @@ -1,26 +1,45 @@ package org.usvm.api import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsVoidType import org.usvm.UAddressSort +import org.usvm.UBoolExpr 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 +import org.usvm.solver.USatResult +import org.usvm.solver.UUnknownResult +import org.usvm.solver.UUnsatResult fun mockMethodCall( scope: TsStepScope, method: EtsMethodSignature, resultType: EtsType = method.returnType, -) { - val result = makeFreshUnknownCallResult(scope, resultType) +): Boolean { + val prepared = prepareFreshUnknownCallResult(scope, resultType) + prepared.admissibilityGuard?.let { guard -> + val state = scope.calcOnState { this } + if (scope.assert(guard) == null) { + val constraints = state.pathConstraints.clone() + constraints += guard + + when (state.ctx.solver().check(constraints)) { + is UUnsatResult -> return false + is UUnknownResult -> error("Solver could not decide fresh string type for $method") + is USatResult -> error("Fresh string type was satisfiable after its fork failed for $method") + } + } + } scope.doWithState { - setMockMethodCallResult(method, result) + setMockMethodCallResult(method, prepared.value) } + return true } /** Stores a prepared opaque result on this state without applying callee effects or exceptions. */ @@ -31,23 +50,39 @@ internal fun TsState.setMockMethodCallResult( methodResult = TsMethodResult.Success.MockedCall(result, method) } -/** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */ -internal fun makeFreshUnknownCallResult( +internal data class PreparedFreshUnknownCallResult( + val value: UExpr<*>, + val admissibilityGuard: UBoolExpr? = null, +) + +/** Prepares a fresh opaque result; callers must apply [PreparedFreshUnknownCallResult.admissibilityGuard]. */ +internal fun prepareFreshUnknownCallResult( scope: TsStepScope, resultType: EtsType, -): UExpr<*> = scope.calcOnState { - if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() +): PreparedFreshUnknownCallResult { + if (resultType is EtsStringType) { + // The type guard belongs only to the branch using this result. Asserting it before a + // partial model forks could discard satisfiable model successors. + val ref = scope.calcOnState { makeSymbolicRefUntyped() } + val guard = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) } + return PreparedFreshUnknownCallResult(value = ref, admissibilityGuard = guard) + } + + val value = scope.calcOnState { + if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue() - when (val sort = ctx.typeToSort(resultType)) { - is UAddressSort -> makeSymbolicRefUntyped() + when (val sort = ctx.typeToSort(resultType)) { + is UAddressSort -> makeSymbolicRefUntyped() - is TsUnresolvedSort -> mkFakeValue( - scope, - boolValue = makeSymbolicPrimitive(ctx.boolSort), - fpValue = makeSymbolicPrimitive(ctx.fp64Sort), - refValue = makeSymbolicRefUntyped(), - ) + is TsUnresolvedSort -> mkFakeValue( + scope, + boolValue = makeSymbolicPrimitive(ctx.boolSort), + fpValue = makeSymbolicPrimitive(ctx.fp64Sort), + refValue = makeSymbolicRefUntyped(), + ) - else -> makeSymbolicPrimitive(sort) + else -> makeSymbolicPrimitive(sort) + } } + return PreparedFreshUnknownCallResult(value = value) } 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 8f7d262074..420992e640 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod @@ -151,6 +152,16 @@ class TsContext( is EtsNullType -> addressSort is EtsUndefinedType -> addressSort is EtsUnionType -> unresolvedSort + is EtsIntersectionType -> { + val memberSorts = type.types.map(::typeToSort) + val commonSort = memberSorts.firstOrNull() + + if (commonSort != null && memberSorts.all { it == commonSort }) { + commonSort + } else { + unresolvedSort + } + } is EtsRefType -> addressSort is EtsLexicalEnvType -> addressSort is EtsAnyType -> unresolvedSort 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 c643eb3881..2c9777109d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -91,6 +91,12 @@ data class TsRuntimeFeatureLimitationEvent( /** Stable identifiers for bounded runtime features reported by [TsRuntimeFeatureLimitationEvent]. */ enum class TsRuntimeFeatureLimitationReason { ARRAY_ELEMENT_DELETE, + CAUGHT_EXCEPTION_VALUE, + REGULAR_EXPRESSION_LITERAL, + STRING_CONCAT_OPERAND_CONVERSION, + ARRAY_STORAGE_TYPE, + CONDITIONAL_FIELD_RECEIVER, + FAKE_FIELD_RECEIVER_TYPE, ARRAY_NAMED_PROPERTY_READ, ARRAY_NAMED_PROPERTY_WRITE, ARRAY_INDEX_GROWTH, 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 d3bbab1aad..c2acf85443 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 @@ -105,7 +105,9 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher { TsUnknownCallFailureReason.INTERPROCEDURAL_ANALYSIS_DISABLED, TsUnknownCallFailureReason.LOGGING_CALL, -> { - mockMethodCall(scope, call.callee) + if (!mockMethodCall(scope, call.callee)) { + return TsUnknownCallOutcome.PATH_STOPPED + } scope.doWithState { newStmt(call.callSite) } return TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 5ab9ad9772..49623b3319 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -2,8 +2,8 @@ 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.prepareFreshUnknownCallResult import org.usvm.api.setMockMethodCallResult import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.interpreter.TsStepScope @@ -61,7 +61,9 @@ class TsModelUnknownCallDispatcher( } TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { - mockMethodCall(scope, call.callee, call.resultType) + if (!mockMethodCall(scope, call.callee, call.resultType)) { + return TsUnknownCallOutcome.PATH_STOPPED + } scope.doWithState { newStmt(call.callSite) } } } @@ -76,12 +78,12 @@ class TsModelUnknownCallDispatcher( 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. + // Create the value before forking. A string's type guard is applied only to the residual + // branch below, so an infeasible fresh string cannot discard a modeled successor. val freshResidualResult = if ( residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN ) { - makeFreshUnknownCallResult(scope, call.resultType) + prepareFreshUnknownCallResult(scope, call.resultType) } else { null } @@ -112,8 +114,12 @@ class TsModelUnknownCallDispatcher( }.toMutableList() if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { - guardedStateChanges += residualGuard to { - setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) + val prepared = requireNotNull(freshResidualResult) + val guardedResidual = prepared.admissibilityGuard?.let { admissibilityGuard -> + scope.calcOnState { ctx.mkAnd(residualGuard, admissibilityGuard) } + } ?: residualGuard + guardedStateChanges += guardedResidual to { + setMockMethodCallResult(call.callee, prepared.value) newStmt(call.callSite) freshResidualApplied = true } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt index 1a22c04022..6cbe13d1d0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt @@ -5,18 +5,23 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsStringType 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.USymbolicHeapRef import org.usvm.api.makeSymbolicPrimitive +import org.usvm.api.typeStreamOf import org.usvm.isFalse import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.ExprWithTypeConstraint +import org.usvm.types.TypesResult import org.usvm.types.single import org.usvm.util.boolToFp import org.usvm.util.refOrStringTruthy @@ -31,6 +36,20 @@ fun TsContext.checkNotFake(expr: UExpr<*>) { } } +internal fun TsContext.fieldReceiverLimitation( + scope: TsStepScope, + receiver: UHeapRef, +): TsRuntimeFeatureLimitationReason? { + if (receiver !is UConcreteHeapRef && receiver !is USymbolicHeapRef) { + return TsRuntimeFeatureLimitationReason.CONDITIONAL_FIELD_RECEIVER + } + + val types = scope.calcOnState { memory.typeStreamOf(receiver).take(2) } + return TsRuntimeFeatureLimitationReason.FAKE_FIELD_RECEIVER_TYPE.takeIf { + types is TypesResult.SuccessfulTypesResult && types.types.any { it is EtsFakeType } + } +} + fun TsContext.mkTruthyExpr( expr: UExpr, scope: TsStepScope, 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 13f2ddb0aa..a524176d06 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 @@ -62,8 +62,12 @@ internal fun TsExprResolver.handleArrayAccess( if (storageType is EtsStringType) { return readStringIndex(scope, array, index.value, index.isNumeric) } - check(storageType is EtsArrayType) { - "Expected EtsArrayType, got: ${value.array.type}" + if (storageType !is EtsArrayType) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + detail = "indexed read requires supported array storage: static=${value.array.type}, storage=$storageType", + ) + return null } val indexIsSupported = mkAnd( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 91c0c574c3..ee44b0c9b9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -46,9 +46,25 @@ internal fun TsExprResolver.handleInstanceFieldRef( // Check for undefined or null property access. checkUndefinedOrNullPropertyRead(scope, instance, propertyName = value.field.name) ?: return null + val receiverLimitation = fieldReceiverLimitation(scope, instance) + if (receiverLimitation != null) { + reportRuntimeFeatureLimitation( + reason = receiverLimitation, + detail = "Field read requires an unsupported receiver: ${value.field.name}", + ) + scope.assert(falseExpr) + return null + } + // Handle reading "length" property. if (value.field.name == "length") { - return readLengthProperty(scope, instanceLocal, instance, options.maxArraySize) + return readLengthProperty( + scope = scope, + instanceLocal = instanceLocal, + instance = instance, + maxArraySize = options.maxArraySize, + onFeatureLimitation = ::reportRuntimeFeatureLimitation, + ) } // Read the field. 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 b20dc64274..96756abe9f 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 @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType @@ -22,6 +23,7 @@ fun TsContext.readLengthProperty( instanceLocal: EtsLocal, instance: UHeapRef, maxArraySize: Int, + onFeatureLimitation: (TsRuntimeFeatureLimitationReason, String) -> Unit, ): UExpr<*>? { // Determine the array type. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } @@ -46,7 +48,13 @@ fun TsContext.readLengthProperty( EtsArrayType(EtsUnknownType, dimensions = 1) } - else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") + else -> { + onFeatureLimitation( + TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + "length read requires supported array storage: static=${instanceLocal.type}, storage=$type", + ) + return null + } } // Read the length of the array. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index bc388200a6..b04b1f46a8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -3,6 +3,7 @@ package org.usvm.machine.expr import io.ksmt.expr.KFp64Value import io.ksmt.utils.asExpr import io.ksmt.utils.cast +import kotlinx.serialization.json.JsonPrimitive import mu.KotlinLogging import org.jacodb.ets.model.EtsAddExpr import org.jacodb.ets.model.EtsAndExpr @@ -57,6 +58,7 @@ import org.jacodb.ets.model.EtsPostIncExpr import org.jacodb.ets.model.EtsPreDecExpr import org.jacodb.ets.model.EtsPreIncExpr import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsRawEntity import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsRemExpr import org.jacodb.ets.model.EtsRightShiftExpr @@ -578,15 +580,28 @@ class TsExprResolver( } val lhsRef = stringStorageRef(lhs) - ?: error("String concatenation is not supported for left operand: $lhs") + ?: return@resolveAfterResolved stopUnsupportedStringConcatOperand(side = "left", value = lhs) val rhsRef = stringStorageRef(rhs) - ?: error("String concatenation is not supported for right operand: $rhs") + ?: return@resolveAfterResolved stopUnsupportedStringConcatOperand(side = "right", value = rhs) scope.calcOnState { concatStrings(lhsRef, rhsRef) } } } return resolveBinaryOperator(TsBinaryOperator.Add, expr) } + private fun stopUnsupportedStringConcatOperand( + side: String, + value: UExpr<*>, + ): UExpr? = with(ctx) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION, + detail = "Cannot convert $side operand to string: $value", + ) + scope.assert(falseExpr) + + null + } + private fun stringStorageRef(value: UExpr<*>): UHeapRef? = with(ctx) { if (value is UIteExpr<*>) { val trueBranch = stringStorageRef(value.trueBranch) ?: return null @@ -1012,8 +1027,32 @@ class TsExprResolver( override fun visit(value: EtsStaticFieldRef): UExpr<*>? = handleStaticFieldRef(value) override fun visit(value: EtsCaughtExceptionRef): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.CAUGHT_EXCEPTION_VALUE, + detail = "Caught exception value cannot be modeled: $value", + ) + scope.assert(ctx.falseExpr) + + return null + } + + override fun visit(value: EtsRawEntity): UExpr? { + val kindName = when (val raw = value.extra["kindName"]) { + is JsonPrimitive -> raw.content + is String -> raw + else -> null + } + if (value.kind != "UnsupportedValue" || kindName != "RegularExpressionLiteral") { + error("Cannot handle EtsRawEntity: $value") + } + + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, + detail = "Regular expression literal is not modeled: $value", + ) + scope.assert(ctx.falseExpr) + + return null } override fun visit(value: EtsGlobalRef): UExpr? { @@ -1060,8 +1099,10 @@ class TsExprResolver( if (expr.type.typeName == "Number") { val clazz = scene.sdkClasses.filter { it.name == "Number" }.maxByOrNull { it.methods.size } - ?: error("No Number class found in SDK") - return@with scope.calcOnState { memory.allocConcrete(clazz.type) } + // The allocation itself does not execute the Number constructor. If the SDK class is + // absent, retain the IR type and let the following constructor call use the residual + // call policy instead of treating the missing SDK declaration as a tool failure. + return@with scope.calcOnState { memory.allocConcrete(clazz?.type ?: resolvedType) } } scope.calcOnState { memory.allocConcrete(resolvedType) } 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 e315837abb..ddf35e55fc 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 @@ -22,11 +22,18 @@ internal fun TsExprResolver.handleAssignToArrayIndex( expr: UExpr<*>, ): Unit? = with(ctx) { // Resolve the array. - val resolvedArray = resolve(lhv.array) ?: return null - check(resolvedArray.sort == addressSort) { - "Expected address sort for array, got: ${resolvedArray.sort}" + val array = run { + val resolved = resolve(lhv.array) ?: return null + if (resolved.isFakeObject()) { + scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: return null + resolved.extractRef(scope) + } else { + check(resolved.sort == addressSort) { + "Expected address sort for array, got: ${resolved.sort}" + } + resolved.asExpr(addressSort) + } } - val array = resolvedArray.asExpr(addressSort) handleAssignToArrayIndex(lhv, expr, array) } @@ -62,8 +69,12 @@ internal fun TsExprResolver.handleAssignToArrayIndex( val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) val arrayType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } - check(arrayType is EtsArrayType) { - "Expected EtsArrayType, got: ${lhv.array.type}" + if (arrayType !is EtsArrayType) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, + detail = "indexed write requires supported array storage: static=${lhv.array.type}, storage=$arrayType", + ) + return null } return assignToArrayIndex( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 1f5dcb27ff..788724b857 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -51,6 +51,16 @@ internal fun TsExprResolver.handleAssignToInstanceField( // Check for undefined or null field access. checkUndefinedOrNullPropertyRead(scope, instance, field.name) ?: return null + val receiverLimitation = fieldReceiverLimitation(scope, instance) + if (receiverLimitation != null) { + reportRuntimeFeatureLimitation( + reason = receiverLimitation, + detail = "Field write requires an unsupported receiver: ${field.name}", + ) + scope.assert(falseExpr) + return null + } + val arrayType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } as? EtsArrayType if (field.name == "length" && arrayType != null) { return assignToArrayLength( 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 41cab2635b..630dad0cd7 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 @@ -71,6 +71,7 @@ import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt import org.usvm.machine.state.parametersWithThisCount import org.usvm.machine.state.returnValue +import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort @@ -252,6 +253,11 @@ class TsInterpreter( return } + if (possibleTypesSet.any { it is EtsFakeType }) { + unknownCallDispatcher.dispatch(scope, stmt, Reason.UNSUPPORTED_RECEIVER_TYPE, receiver) + return + } + val filteredPossibleTypesSet = possibleTypesSet - EtsAnyType val methodsDeclaringClasses = concreteMethods.mapNotNull { it.enclosingClass } // is it right? diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index cefcc35885..f126ae1423 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -70,6 +70,12 @@ class TsTypeSystem( // "never" is the universal subtype: never can be assigned to any type. if (unwrappedType is EtsNeverType) return true + // A fake type only matches itself. Distinct wrappers do not establish a + // TypeScript subtype relation; callers handle those branches explicitly. + if (unwrappedType is EtsFakeType || unwrappedSupertype is EtsFakeType) { + return unwrappedSupertype === unwrappedType + } + // When "never" is in supertype position, only never <: never. if (unwrappedSupertype is EtsNeverType) return type is EtsNeverType @@ -164,10 +170,6 @@ class TsTypeSystem( // Class and structural types - require(unwrappedType !is EtsFakeType && unwrappedSupertype !is EtsFakeType) { - "Fake types should not occur in type constraints" - } - if (unwrappedSupertype is EtsAuxiliaryType && unwrappedType is EtsAuxiliaryType) { return unwrappedType.properties.all { it in unwrappedSupertype.properties } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index 607a702e42..2fbbe2fa8a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt @@ -24,7 +24,8 @@ fun TsContext.resolveEtsField( if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) { val classes = hierarchy.classesForType(EtsClassType(field.enclosingClass)) if (classes.isEmpty()) { - error("Cannot resolve class ${field.enclosingClass.name}") + logger.warn { "Cannot resolve class ${field.enclosingClass.name} for field ${field.name}" } + return TsResolutionResult.Empty } if (classes.size > 1) { error("Multiple classes with name ${field.enclosingClass.name}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt new file mode 100644 index 0000000000..65b829f429 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsContextTypeToSortTest.kt @@ -0,0 +1,51 @@ +package org.usvm.machine + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnclearRefType +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals + +class TsContextTypeToSortTest { + private val ctx = TsContext( + scene = EtsScene(projectFiles = emptyList()), + components = mockk(), + ) + + @Test + fun `intersection of reference types has reference sort`() { + val window = EtsClassType( + signature = EtsClassSignature( + name = "Window", + file = EtsFileSignature.UNKNOWN, + ), + ) + val globalThis = EtsUnclearRefType( + name = "globalThis", + typeParameters = emptyList(), + ) + val type = EtsIntersectionType(types = listOf(window, globalThis)) + + val sort = ctx.typeToSort(type) + + assertEquals(ctx.addressSort, sort) + } + + @Test + fun `intersection with incompatible sorts remains unresolved`() { + val globalThis = EtsUnclearRefType( + name = "globalThis", + typeParameters = emptyList(), + ) + val type = EtsIntersectionType(types = listOf(EtsNumberType, globalThis)) + + val sort = ctx.typeToSort(type) + + assertEquals(ctx.unresolvedSort, sort) + } +} 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 4abb82bb0b..485ad9884e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -25,6 +25,7 @@ import org.usvm.UBoolSort import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UMachineOptions +import org.usvm.api.evalTypeEquals import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.isTrue @@ -209,6 +210,30 @@ class TsUnknownCallDispatcherTest { ) } + @Test + fun `partial string model keeps modeled and typed fresh successors`() { + val observer = RecordingUnknownCallObserver() + + val states = analyzeAllStates( + methodName = "modeledStringCallForks", + fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + models = catalog(PartialStringModel), + observer = observer, + ) + + assertEquals(2, states.size) + assertEquals( + listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), + observer.events.map { it.outcome }, + ) + states.forEach { state -> + val result = assertIs(state.methodResult).value + val isString = state.memory.types.evalTypeEquals(result.asExpr(state.ctx.addressSort), EtsStringType) + assertTrue(state.models.isNotEmpty()) + assertTrue(state.models.all { model -> model.eval(isString).isTrue }) + } + } + @Test fun `partial model sends residual domain to stop fallback`() { val observer = RecordingUnknownCallObserver() @@ -717,6 +742,25 @@ class TsUnknownCallDispatcherTest { } } + private object PartialStringModel : TestModel( + id = "partial-string-model", + methodName = "convert", + enclosingClassName = "ExternalString", + ) { + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution { + val condition = requireNotNull(call.arguments.single().resolved).asExpr(state.ctx.boolSort) + val successor = TsUnknownCallModelSuccessor( + guard = condition, + completion = TsUnknownCallModelCompletion.Normal { mkInitializedStringConstant("modeled") }, + ) + + 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( @@ -760,8 +804,9 @@ class TsUnknownCallDispatcherTest { private abstract class TestModel( override val id: String, methodName: String, + enclosingClassName: String? = null, ) : TsUnknownCallModel { - override val target = TsUnknownCallTarget(methodName = methodName) + override val target = TsUnknownCallTarget(methodName = methodName, enclosingClassName = enclosingClassName) } private class RecordingUnknownCallObserver : TsInterpreterObserver { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayStorageTypeBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayStorageTypeBoundaryTest.kt new file mode 100644 index 0000000000..e6e44c602f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/ArrayStorageTypeBoundaryTest.kt @@ -0,0 +1,87 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +class ArrayStorageTypeBoundaryTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayStorageTypeBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(sourceFile)) + + @Test + fun `unsupported indexed access and typed array length report limitations`() { + val methods = mapOf( + "readUnknown" to "unknown", + "writeUnknown" to "unknown", + "readUint16" to "Uint16Array", + "lengthUint8" to "Uint8Array", + ) + + methods.forEach { (methodName, expectedType) -> + val observer = RecordingObserver() + val method = scene.projectClasses + .single { it.name == "ArrayStorageTypeBoundary" } + .methods + .single { it.name == methodName } + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + machine.analyze(methods = listOf(method)) + } + + assertTrue(states.none { it.methodResult is TsMethodResult.Success }, methodName) + assertTrue(observer.limitations.isNotEmpty(), methodName) + assertTrue( + observer.limitations.all { it.reason == TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE }, + "$methodName: ${observer.limitations.map { it.reason }}", + ) + assertTrue( + observer.limitations.any { expectedType in it.detail }, + "$methodName: ${observer.limitations.map { it.detail }}", + ) + } + } + + private class RecordingObserver : TsInterpreterObserver { + val limitations = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumberWithoutSdkTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumberWithoutSdkTest.kt new file mode 100644 index 0000000000..9b7a0871f8 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumberWithoutSdkTest.kt @@ -0,0 +1,76 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.call.TsUnknownCallOutcome +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +class NumberWithoutSdkTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/NumberWithoutSdk.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `missing Number SDK class leaves constructor call residual`() { + val clazz = scene.projectClasses.single { it.name == "NumberWithoutSdk" } + val method = clazz.methods.single { it.name == "construct" } + val observer = RecordingObserver() + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + val freshReturnObserved = observer.events.any { event -> + event.callee.name == CONSTRUCTOR_NAME && + event.outcome == TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN + } + + assertTrue(states.isNotEmpty()) + assertTrue(freshReturnObserved) + } + + private class RecordingObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.Z3, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnknownStringConcatTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnknownStringConcatTest.kt new file mode 100644 index 0000000000..772679041b --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnknownStringConcatTest.kt @@ -0,0 +1,98 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.call.TsUnknownCallOutcome +import org.usvm.machine.state.TsState +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration + +class UnknownStringConcatTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/UnknownStringConcat.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `fresh string return can be concatenated`() { + val observer = RecordingObserver() + + val states = analyze(methodName = "concatOpaqueString", observer = observer) + + assertTrue(states.isNotEmpty()) + assertTrue(observer.events.any { it.outcome == TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN }) + assertTrue(observer.limitations.isEmpty()) + } + + @Test + fun `symbolic number to string is an explicit limitation`() { + val observer = RecordingObserver() + + val states = analyze(methodName = "concatOpaqueNumber", observer = observer) + + assertTrue(states.isEmpty()) + assertEquals( + TsRuntimeFeatureLimitationReason.STRING_CONCAT_OPERAND_CONVERSION, + observer.limitations.single().reason, + ) + } + + private fun analyze(methodName: String, observer: RecordingObserver): List { + val clazz = scene.projectClasses.single { it.name == "UnknownStringConcat" } + val method = clazz.methods.single { it.name == methodName } + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions( + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN, + ), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + } + + private class RecordingObserver : TsInterpreterObserver { + val events = mutableListOf() + val limitations = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.Z3, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnsupportedExpressionBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnsupportedExpressionBoundaryTest.kt new file mode 100644 index 0000000000..41beec14b1 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/UnsupportedExpressionBoundaryTest.kt @@ -0,0 +1,78 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.time.Duration + +class UnsupportedExpressionBoundaryTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/UnsupportedExpressionBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `regular expression literal stops with an observed limitation`() { + assertLimitation( + methodName = "regularExpressionLiteral", + reason = TsRuntimeFeatureLimitationReason.REGULAR_EXPRESSION_LITERAL, + ) + } + + @Test + fun `used catch value stops with an observed limitation`() { + assertLimitation( + methodName = "caughtExceptionValue", + reason = TsRuntimeFeatureLimitationReason.CAUGHT_EXCEPTION_VALUE, + ) + } + + private fun assertLimitation(methodName: String, reason: TsRuntimeFeatureLimitationReason) { + val method = scene.projectClasses.flatMap { it.methods }.single { it.name == methodName } + val observer = RecordingObserver() + + TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + assertEquals(listOf(reason), observer.limitations.map { it.reason }) + } + + private class RecordingObserver : TsInterpreterObserver { + val limitations = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.Z3, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt index 2e699edffc..2bed4645b6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -1,5 +1,6 @@ package org.usvm.machine.types +import io.mockk.mockk import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldImpl @@ -9,12 +10,52 @@ import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test +import org.usvm.machine.TsContext +import org.usvm.types.USingleTypeStream import org.usvm.util.EtsHierarchy import org.usvm.util.type +import kotlin.test.assertFalse import kotlin.test.assertTrue import kotlin.time.Duration.Companion.seconds class TsTypeSystemTest { + @Test + fun `synthetic wrapper does not satisfy structural type constraints`() { + val scene = EtsScene(projectFiles = emptyList()) + val context = TsContext(scene = scene, components = mockk()) + val typeSystem = TsTypeSystem( + scene = scene, + typeOperationsTimeout = 1.seconds, + hierarchy = EtsHierarchy(scene), + ) + val fakeType = EtsFakeType.mkRef(context) + val structuralType = EtsAuxiliaryType(properties = setOf("style")) + + val fakeHasProperty = typeSystem.isSupertype(structuralType, fakeType) + val propertyHasFakeType = typeSystem.isSupertype(fakeType, structuralType) + + assertFalse(fakeHasProperty) + assertFalse(propertyHasFakeType) + } + + @Test + fun `fake type remains in a singleton stream after filtering by itself`() { + val scene = EtsScene(projectFiles = emptyList()) + val context = TsContext(scene = scene, components = mockk()) + val typeSystem = TsTypeSystem( + scene = scene, + typeOperationsTimeout = 1.seconds, + hierarchy = EtsHierarchy(scene), + ) + val fakeType = EtsFakeType.mkRef(context) + val stream = USingleTypeStream(typeSystem = typeSystem, singleType = fakeType) + + val filtered = stream.filterBySupertype(fakeType).filterBySubtype(fakeType) + + assertTrue(typeSystem.isSupertype(fakeType, fakeType)) + assertFalse(filtered.isEmpty ?: true) + } + @Test fun `auxiliary type is a subtype of a class containing its properties`() { val fileSignature = EtsFileSignature(projectName = "test", fileName = "types.ts") diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt new file mode 100644 index 0000000000..300ec9c550 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/EtsFieldResolverTest.kt @@ -0,0 +1,40 @@ +package org.usvm.util + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +import org.junit.jupiter.api.Test +import org.usvm.machine.TsContext +import kotlin.test.assertEquals + +class EtsFieldResolverTest { + @Test + fun `missing built-in class leaves its field unresolved`() { + val scene = EtsScene(projectFiles = emptyList()) + val ctx = TsContext(scene = scene, components = mockk()) + val hierarchy = EtsHierarchy(scene) + + for ((className, fieldName) in listOf("RangeError" to "stack", "URL" to "searchParams")) { + val signature = EtsClassSignature( + name = className, + file = EtsFileSignature.UNKNOWN, + ) + val field = EtsFieldSignature( + enclosingClass = signature, + name = fieldName, + type = EtsStringType, + ) + + val result = ctx.resolveEtsField( + instance = null, + field = field, + hierarchy = hierarchy, + ) + + assertEquals(TsResolutionResult.Empty, result) + } + } +} diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts index e37b101722..dd04bbe03a 100644 --- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -18,6 +18,10 @@ declare class ExternalBoolean { static convert(value: boolean): boolean; } +declare class ExternalString { + static convert(value: boolean): string; +} + declare class ExternalAny { static value(): any; } @@ -77,6 +81,10 @@ class CallFallbackBaseline { return ExternalBoolean.convert(value); } + modeledStringCallForks(value: boolean): string { + return ExternalString.convert(value); + } + modeledUnknownCallReturnsAlias(receiver: ExternalReceiver): number { if (ExternalModeledCall.identity(receiver) === receiver) { return 122; diff --git a/usvm-ts/src/test/resources/models/ArrayStorageTypeBoundary.ts b/usvm-ts/src/test/resources/models/ArrayStorageTypeBoundary.ts new file mode 100644 index 0000000000..89ba876a4a --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayStorageTypeBoundary.ts @@ -0,0 +1,20 @@ +// @ts-nocheck + +export class ArrayStorageTypeBoundary { + readUnknown(values: unknown): unknown { + return values[0]; + } + + writeUnknown(values: unknown): number { + values[0] = 7; + return 1; + } + + readUint16(values: Uint16Array): number { + return values[0]; + } + + lengthUint8(values: Uint8Array): number { + return values.length; + } +} diff --git a/usvm-ts/src/test/resources/models/NumberWithoutSdk.ts b/usvm-ts/src/test/resources/models/NumberWithoutSdk.ts new file mode 100644 index 0000000000..a80ebdef44 --- /dev/null +++ b/usvm-ts/src/test/resources/models/NumberWithoutSdk.ts @@ -0,0 +1,9 @@ +// @ts-nocheck + +class NumberWithoutSdk { + construct(value: number): number { + const wrapper = new Number(value); + + return wrapper.valueOf(); + } +} diff --git a/usvm-ts/src/test/resources/models/UnknownStringConcat.ts b/usvm-ts/src/test/resources/models/UnknownStringConcat.ts new file mode 100644 index 0000000000..391c292bd7 --- /dev/null +++ b/usvm-ts/src/test/resources/models/UnknownStringConcat.ts @@ -0,0 +1,16 @@ +// @ts-nocheck + +class UnknownStringConcat { + concatOpaqueString(): number { + const upper = "a".toUpperCase(); + const result = upper + "!"; + + return result.length; + } + + concatOpaqueNumber(value: number): number { + const result = `${value}`; + + return result.length; + } +} diff --git a/usvm-ts/src/test/resources/models/UnsupportedExpressionBoundary.ts b/usvm-ts/src/test/resources/models/UnsupportedExpressionBoundary.ts new file mode 100644 index 0000000000..f0685c379e --- /dev/null +++ b/usvm-ts/src/test/resources/models/UnsupportedExpressionBoundary.ts @@ -0,0 +1,12 @@ +export function regularExpressionLiteral(value: string): string { + const whitespace = /\s+/g; + return value.replaceAll(whitespace, "-"); +} + +export function caughtExceptionValue(): unknown { + try { + return 1; + } catch (error) { + return error; + } +}