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/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt index a3cb6ddb40..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 @@ -75,6 +75,16 @@ 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 directModel = select(call) val modelCall = if (directModel == null) { 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 536d1c66d1..cfe30da81a 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 @@ -46,6 +46,10 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private val sourceModelIds by lazy { + models.filterIsInstance().map { model -> model.id }.toSet() + } + private val primitiveClassSignature by lazy { baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature } @@ -436,9 +440,14 @@ 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, + helperClassSignature = { primitiveClassSignature }, + sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass }, + owningModelIds = { sourceModelIds }, implementation = implementation, ) @@ -536,30 +545,6 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } - 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.callee.enclosingClass != primitiveClassSignature) return null - - 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 PRIMITIVE_GROW_ID = "ts.array.primitive.grow" private const val PRIMITIVE_ALLOCATE_LIKE_ID = "ts.array.primitive.allocateLike" 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..b4b51067d7 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsPrimitiveUnknownCallModel.kt @@ -0,0 +1,44 @@ +package org.usvm.machine.call.intrinsic + +import org.jacodb.ets.model.EtsClassSignature +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 helperClassSignature: () -> EtsClassSignature, + private val sourceClassSignature: () -> EtsClassSignature, + private val owningModelIds: () -> Set, + 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? { + val helperOwnerMatches = call.callee.enclosingClass == helperClassSignature() + val callerSignature = call.callSite.location.method.signature + val sourceCallerMatches = callerSignature.enclosingClass == sourceClassSignature() + val sourceModelIsActive = owningModelIds().any(state::isUnknownCallModelActive) + if (!helperOwnerMatches || !sourceCallerMatches || !sourceModelIsActive) return null + + 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 77beb6b8ea..b170cb6ebb 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 @@ -10,7 +10,6 @@ import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter -import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallModelCompletion @@ -41,6 +40,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private val sourceModelIds by lazy { + models.filterIsInstance().map { model -> model.id }.toSet() + } + private val primitiveClassSignature by lazy { baseArtifact.file.allClasses.single { it.name == PRIMITIVES_CLASS_NAME }.signature } @@ -328,9 +331,14 @@ 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, + helperClassSignature = { primitiveClassSignature }, + sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass }, + owningModelIds = { sourceModelIds }, implementation = implementation, ) @@ -406,32 +414,6 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } - 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.callee.enclosingClass != primitiveClassSignature) { - return null - } - - 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_CODE_UNIT_AT_ID = "ts.string.primitive.codeUnitAt" private const val PRIMITIVE_FROM_CODE_UNIT_ID = "ts.string.primitive.fromCodeUnit" private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" 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 1bac1289ae..4ad94a9251 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 @@ -24,6 +24,7 @@ import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsRuntimeFeatureLimitationReason 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 @@ -52,24 +53,6 @@ import org.usvm.util.typedArrayBoxedLValue import org.usvm.util.typedArrayOverrideLValue private val logger = KotlinLogging.logger {} -private val modeledArrayMethods = setOf("concat", "fill", "push", "reverse", "slice", "unshift") - -private val modeledStringMethods = setOf( - "substring", - "trim", - "trimStart", - "trimEnd", - "charAt", - "charCodeAt", - "endsWith", - "includes", - "indexOf", - "lastIndexOf", - "slice", - "startsWith", - "toLowerCase", - "toUpperCase", -) internal fun TsExprResolver.tryApproximateGlobalInstanceCall( expr: EtsInstanceCallExpr, @@ -161,6 +144,11 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Mock `.toString()` method calls if (expr.callee.name == "toString") { + if (unknownCallDispatcher is TsUnknownCallModelDispatcher) { + dispatchLegacyInstanceCall(stmt) + return TsExprApproximationResult.ResolveFailure + } + if (expr.args.isNotEmpty()) { logger.warn { "toString() should have no arguments, but got ${expr.args.size}" } } @@ -187,9 +175,15 @@ internal fun TsExprResolver.tryApproximateInstanceCall( .takeIf { it !is TsUnresolvedSort } ?: addressSort - val usesSemanticArrayModel = expr.callee.name in modeledArrayMethods && - unknownCallDispatcher is TsUnknownCallModelDispatcher - if (usesSemanticArrayModel) { + 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 } @@ -250,12 +244,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 + val modeledStringCall = instanceType is EtsStringType && dispatcher is TsUnknownCallModelDispatcher && + TsBuiltInUnknownCallModels.hasPartialApproximationModel( + methodName = expr.callee.name, + enclosingClassName = "String", + ) + if (modeledStringCall) { dispatcher.dispatch( scope = scope, call = stmt.call, @@ -315,6 +310,17 @@ private fun TsExprResolver.dispatchArrayModel(stmt: TsVirtualMethodCallStmt) { ) } +private fun TsExprResolver.dispatchLegacyInstanceCall(stmt: TsVirtualMethodCallStmt) { + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = stmt.instance, + resolvedArguments = stmt.args, + ) +} + private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSignature = copy(enclosingClass = enclosingClass.copy(name = name)) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt index 1820e2bd14..fa2830945d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt @@ -61,11 +61,27 @@ class TsInstanceCallReceiverTest { assertEquals(case.results, results) assertEquals(case.throws, tests.any { it.returnValue is TsTestValue.TsException }) assertTrue(tests.isNotEmpty()) - if (method.parameters.singleOrNull()?.name == "index") { + val modelToStringIsUnsupported = case.method == "primitiveToString" && !case.compatibility + val exploresBothReceiverAlternatives = method.parameters.singleOrNull()?.name == "index" && + !modelToStringIsUnsupported + if (exploresBothReceiverAlternatives) { val indices = tests.map { assertIs(it.before.parameters.single()).number } assertTrue(indices.containsAll(listOf(0.0, 1.0)), "Both receiver alternatives must be explored") } + if (modelToStringIsUnsupported) { + assertTrue(events.isNotEmpty(), "Primitive toString calls must reach the residual policy") + events.forEach { event -> + assertEquals("toString", event.callee.name) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, event.outcome) + assertEquals(TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, event.failureReason) + assertEquals( + TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH), + event.decision, + ) + } + } + if (case.method == "wrappedShift") { assertEquals(TsUnknownCallDecision.ModelApplied("ts.array.shift"), events.single().decision) } @@ -138,6 +154,7 @@ class TsInstanceCallReceiverTest { Case(method = "conditionalEmptyArray", results = setOf(0.0, 1.0)), Case(method = "arrayOrUserMethod", results = setOf(0.0, 1.0)), Case(method = "primitiveValueOf", results = setOf(0.0, 1.0)), + Case(method = "primitiveToString", results = setOf(0.0)), Case(method = "primitiveToString", results = setOf(0.0, 1.0), compatibility = true), Case(method = "constrainedFake", results = setOf(0.0, 1.0, 2.0)), Case(method = "nullableReceiver", results = setOf(0.0, 1.0), throws = true), diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt new file mode 100644 index 0000000000..bf22cda55f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsPrimitiveOwnerBoundaryTest.kt @@ -0,0 +1,75 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.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.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsPrimitiveOwnerBoundaryTest { + private val source = loadEtsFileAutoConvert( + getResourcePath("/models/ForeignPrimitiveHelpers.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(source)) + + @Test + fun `foreign string helper cannot fabricate a code unit with all models enabled`() { + assertForeignHelperResidual("foreignString") + } + + @Test + fun `foreign array helper cannot mutate storage with all models enabled`() { + assertForeignHelperResidual("foreignArray") + } + + private fun assertForeignHelperResidual(methodName: String) { + val method = scene.projectClasses.single { it.name == "ForeignPrimitiveHelpers" } + .methods + .single { it.name == methodName } + val observer = RecordingObserver() + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + + assertTrue(states.isEmpty()) + assertTrue(observer.events.isNotEmpty()) + assertTrue(observer.events.none { event -> event.decision is TsUnknownCallDecision.ModelApplied }) + assertTrue(observer.events.any { event -> event.outcome == TsUnknownCallOutcome.PATH_STOPPED }) + } + + 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.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts new file mode 100644 index 0000000000..06ee55696e --- /dev/null +++ b/usvm-ts/src/test/resources/models/ForeignPrimitiveHelpers.ts @@ -0,0 +1,19 @@ +declare class StringModelPrimitives { + static codeUnitAt(value: string, index: number): number; +} + +declare class ArrayModelPrimitives { + static grow(values: number[], length: number): void; +} + +export class ForeignPrimitiveHelpers { + foreignString(): number { + return StringModelPrimitives.codeUnitAt("ab", 0); + } + + foreignArray(): number { + const values = [1]; + ArrayModelPrimitives.grow(values, 2); + return values.length; + } +}