From ece65992549730e55547a5e1725414ee263fcf0d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 20 Oct 2026 12:29:33 +0300 Subject: [PATCH] Expose JVM residual call policies with explicit stopped prefixes --- .../kotlin/org/usvm/machine/JcComponents.kt | 9 +- .../org/usvm/machine/JcInterpreterObserver.kt | 6 + .../main/kotlin/org/usvm/machine/JcMachine.kt | 8 +- .../org/usvm/machine/JcMachineOptions.kt | 15 +- .../usvm/machine/interpreter/JcInterpreter.kt | 34 ++++- .../kotlin/org/usvm/machine/state/JcState.kt | 5 + .../samples/invokes/ResidualCallProfiles.java | 61 ++++++++ .../experiments/JavaFourProfileSmokeTest.kt | 142 ++++++++++++++++++ .../usvm/experiments/JavaPilotClasspath.kt | 40 +++++ 9 files changed, 310 insertions(+), 10 deletions(-) create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/invokes/ResidualCallProfiles.java create mode 100644 usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaFourProfileSmokeTest.kt create mode 100644 usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaPilotClasspath.kt diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt index 42344b579e..ea252316b9 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcComponents.kt @@ -13,12 +13,15 @@ import org.usvm.model.ULazyModelDecoder import org.usvm.solver.UExprTranslator import org.usvm.solver.USoftConstraintsProvider import org.usvm.solver.USolverBase +import org.usvm.solver.USolverQueryEvent import org.usvm.solver.UTypeSolver +import org.usvm.solver.observeSolverQueries class JcComponents( private val typeSystem: JcTypeSystem, // TODO specific JcMachineOptions should be here private val options: UMachineOptions, + private val solverQueryObserver: ((USolverQueryEvent) -> Unit)? = null, ) : UComponents { private val closeableResources = mutableListOf() override val useSolverForForks: Boolean get() = options.useSolverForForks @@ -46,7 +49,11 @@ class JcComponents( closeableResources += smtSolver closeableResources += solverFactory - return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout) + val observedSolver = solverQueryObserver?.let { observer -> + observeSolverQueries(solver = smtSolver, observer = observer) + } ?: smtSolver + + return USolverBase(ctx, observedSolver, typeSolver, translator, decoder, options.solverTimeout) } fun close() { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt index 3aea93f0cd..358db50866 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreterObserver.kt @@ -13,9 +13,15 @@ import org.jacodb.api.jvm.cfg.JcSwitchInst import org.jacodb.api.jvm.cfg.JcThrowInst import org.usvm.machine.interpreter.JcSimpleValueResolver import org.usvm.machine.interpreter.JcStepScope +import org.usvm.solver.USolverQueryEvent import org.usvm.statistics.UInterpreterObserver interface JcInterpreterObserver : UInterpreterObserver { + fun onMethodApproximation(call: JcMethodCall, applied: Boolean, elapsedNanos: Long, failure: String?) {} + fun onSolverQuery(event: USolverQueryEvent) {} + fun onAnalysisStopped(reason: String, hasPendingStates: Boolean) {} + fun onResidualCall(call: JcMethodCall, policy: JcResidualCallPolicy, scope: JcStepScope) {} + fun onAssignStatement(simpleValueResolver: JcSimpleValueResolver, stmt: JcAssignInst, stepScope: JcStepScope) {} fun onEntryPoint(simpleValueResolver: JcSimpleValueResolver, stmt: JcMethodEntrypointInst, stepScope: JcStepScope) fun onMethodCallWithUnresolvedArguments(simpleValueResolver: JcSimpleValueResolver, stmt: JcCallExpr, stepScope: JcStepScope) {} diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index a3ea7395bc..9ce2324c95 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt @@ -49,7 +49,7 @@ class JcMachine( private val applicationGraph = JcApplicationGraph(cp) private val typeSystem = JcTypeSystem(cp, options.typeOperationsTimeout) - private val components = JcComponents(typeSystem, options) + private val components = JcComponents(typeSystem, options, interpreterObserver?.let { it::onSolverQuery }) private val ctx = JcContext(cp, components) private val interpreter = JcInterpreter(ctx, applicationGraph, jcMachineOptions, interpreterObserver) @@ -199,6 +199,10 @@ class JcMachine( stopStrategy = stopStrategy, ) + val hasPendingStates = !pathSelector.isEmpty() + val stopReason = if (hasPendingStates) stopStrategy.stopReason() else "QUEUE_EXHAUSTED" + interpreterObserver?.onAnalysisStopped(stopReason, hasPendingStates) + return statesCollector.collectedStates } @@ -221,7 +225,7 @@ class JcMachine( } private fun isStateTerminated(state: JcState): Boolean { - return state.callStack.isEmpty() + return state.callStack.isEmpty() || state.residualCallStop != null } override fun close() { diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt index 623503d786..3075aa50fa 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt @@ -1,8 +1,11 @@ package org.usvm.machine -/** - * JcMachine specific options. - * */ +enum class JcResidualCallPolicy { + STOP, + FRESH, +} + +/** JcMachine specific options. */ data class JcMachineOptions( /** * During virtual call resolution the machine should consider all possible call implementations. @@ -19,4 +22,10 @@ data class JcMachineOptions( * Hard constraint for maximal array size. * */ val arrayMaxSize: Int = 1_500, + + /** Local experiment toggle for the interpreter's built-in method models. */ + val enableMethodApproximations: Boolean = true, + + /** Policy for native, bodyless, and unresolved dynamic calls after model attempts. */ + val residualCallPolicy: JcResidualCallPolicy = JcResidualCallPolicy.FRESH, ) diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt index ca89b045cd..091b14aec8 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt @@ -57,6 +57,7 @@ import org.usvm.machine.JcMethodApproximationResolver import org.usvm.machine.JcMethodCall import org.usvm.machine.JcMethodCallBaseInst import org.usvm.machine.JcMethodEntrypointInst +import org.usvm.machine.JcResidualCallPolicy import org.usvm.machine.JcVirtualMethodCallInst import org.usvm.machine.mocks.mockMethod import org.usvm.machine.state.JcMethodResult @@ -77,6 +78,7 @@ import org.usvm.util.write import org.usvm.utils.ensureSat import org.usvm.utils.logAssertFailure import org.usvm.utils.onStateDeath +import kotlin.time.TimeSource typealias JcStepScope = StepScope @@ -280,7 +282,8 @@ class JcInterpreter( val entryPoint = applicationGraph.entryPoints(method).singleOrNull() if (method.isNative || entryPoint == null) { - mockMethod(scope, stmt, applicationGraph) + val returnType = with(applicationGraph) { method.typed.returnType } + handleResidualCall(scope, stmt, returnType) return } @@ -330,7 +333,7 @@ class JcInterpreter( return } - mockMethod(scope, stmt, stmt.dynamicCall.callSiteReturnType) + handleResidualCall(scope, stmt, stmt.dynamicCall.callSiteReturnType) } } } @@ -737,8 +740,31 @@ class JcInterpreter( private val approximationResolver = JcMethodApproximationResolver(ctx, applicationGraph) + @Suppress("TooGenericExceptionCaught") // Observe and rethrow the original engine error. private fun approximateMethod(scope: JcStepScope, methodCall: JcMethodCall): Boolean { - val exprResolver = exprResolverWithScope(scope) - return approximationResolver.approximate(scope, exprResolver, methodCall) + if (!options.enableMethodApproximations) return false + + val started = TimeSource.Monotonic.markNow() + var applied = false + var failure: String? = null + try { + val exprResolver = exprResolverWithScope(scope) + applied = approximationResolver.approximate(scope, exprResolver, methodCall) + return applied + } catch (error: Throwable) { + failure = error::class.java.name + throw error + } finally { + observer?.onMethodApproximation(methodCall, applied, started.elapsedNow().inWholeNanoseconds, failure) + } + } + + private fun handleResidualCall(scope: JcStepScope, call: JcMethodCall, returnType: JcType) { + observer?.onResidualCall(call, options.residualCallPolicy, scope) + + when (options.residualCallPolicy) { + JcResidualCallPolicy.STOP -> scope.doWithState { residualCallStop = call } + JcResidualCallPolicy.FRESH -> mockMethod(scope, call, returnType) + } } } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt index 24f8290c4a..2b4f01f90b 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt +++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt @@ -10,6 +10,7 @@ import org.usvm.api.targets.JcTarget import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.constraints.UPathConstraints import org.usvm.machine.JcContext +import org.usvm.machine.JcMethodCall import org.usvm.memory.UMemory import org.usvm.merging.MutableMergeGuard import org.usvm.model.UModelBase @@ -27,6 +28,7 @@ class JcState( forkPoints: PathNode> = PathNode.root(), var methodResult: JcMethodResult = JcMethodResult.NoCall, targets: UTargetsSet = UTargetsSet.empty(), + var residualCallStop: JcMethodCall? = null, ) : UState( ctx, ownership, @@ -58,6 +60,7 @@ class JcState( forkPoints, methodResult, targets.clone(), + residualCallStop = residualCallStop, ) } @@ -67,6 +70,8 @@ class JcState( * @return the merged state. TODO: Now it may reuse some of the internal components of the former states. */ override fun mergeWith(other: JcState, by: Unit): JcState? { + if (residualCallStop != null || other.residualCallStop != null) return null + val newThisOwnership = MutabilityOwnership() val newOtherOwnership = MutabilityOwnership() val mergedOwnership = MutabilityOwnership() diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/invokes/ResidualCallProfiles.java b/usvm-jvm/src/samples/java/org/usvm/samples/invokes/ResidualCallProfiles.java new file mode 100644 index 0000000000..2e021d71f7 --- /dev/null +++ b/usvm-jvm/src/samples/java/org/usvm/samples/invokes/ResidualCallProfiles.java @@ -0,0 +1,61 @@ +package org.usvm.samples.invokes; + +public class ResidualCallProfiles { + private static int marker; + + private static native int unknownInt(); + private static native byte unknownByte(); + private static native short unknownShort(); + private static native char unknownChar(); + private static native void unknownVoid(); + + public static int successor() { + unknownInt(); + + return 17; + } + + public static int voidSuccessor() { + marker = 1; + unknownVoid(); + marker = 17; + + return marker; + } + + public static int independentResults() { + int first = unknownInt(); + int second = unknownInt(); + + return first == second ? 1 : 2; + } + + public static int primitiveBounds() { + int narrowByte = unknownByte(); + int narrowShort = unknownShort(); + int narrowChar = unknownChar(); + + boolean byteInRange = narrowByte >= -128 && narrowByte <= 127; + boolean shortInRange = narrowShort >= -32768 && narrowShort <= 32767; + boolean charInRange = narrowChar >= 0 && narrowChar <= 65535; + + return byteInRange && shortInRange && charInRange ? 1 : 0; + } + + public static int modeledNative() { + int[] source = new int[]{17}; + int[] destination = new int[]{0}; + + System.arraycopy(source, 0, destination, 0, 1); + + return destination[0]; + } + + private static int executableBody() { + return 17; + } + + public static int ordinaryBody() { + return executableBody(); + } +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaFourProfileSmokeTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaFourProfileSmokeTest.kt new file mode 100644 index 0000000000..e60ed03736 --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaFourProfileSmokeTest.kt @@ -0,0 +1,142 @@ +package org.usvm.experiments + +import io.ksmt.expr.KBitVec32Value +import kotlinx.coroutines.runBlocking +import org.jacodb.api.jvm.JcClasspath +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.JcInterpreterObserver +import org.usvm.machine.JcMachine +import org.usvm.machine.JcMachineOptions +import org.usvm.machine.JcMethodCall +import org.usvm.machine.JcMethodEntrypointInst +import org.usvm.machine.JcResidualCallPolicy +import org.usvm.machine.interpreter.JcSimpleValueResolver +import org.usvm.machine.interpreter.JcStepScope +import org.usvm.machine.state.JcMethodResult +import org.usvm.machine.state.JcState +import org.usvm.samples.invokes.ResidualCallProfiles +import java.io.File +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class JavaFourProfileSmokeTest { + @Test + fun `all four modes retain prefixes or reach native call successors explicitly`() = runBlocking { + val sampleLocation = ResidualCallProfiles::class.java.protectionDomain.codeSource.location + val samples = File(sampleLocation.toURI()) + + for (modelsEnabled in listOf(false, true)) { + withPilotClasspath(libraries = listOf(samples), approximationsEnabled = modelsEnabled) { classpath -> + val classpathFiles = classpath.locations.map { it.jarOrFolder.canonicalFile }.toSet() + for (name in listOf("usvm.jvm.api.jar.path", "usvm.jvm.approximations.jar.path")) { + val artifact = File(requireNotNull(System.getenv(name))).canonicalFile + assertEquals(modelsEnabled, artifact in classpathFiles, name) + } + + for (policy in JcResidualCallPolicy.entries) { + assertProfile(classpath = classpath, modelsEnabled = modelsEnabled, policy = policy) + } + } + } + } + + private fun assertProfile(classpath: JcClasspath, modelsEnabled: Boolean, policy: JcResidualCallPolicy) { + val owner = requireNotNull(classpath.findClassOrNull(ResidualCallProfiles::class.java.name)) + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + solverType = SolverType.YICES, + timeout = 5.seconds, + throwExceptionOnStepFailure = true, + ) + var approximationAttempts = 0 + var modeledArraycopyApplications = 0 + val observer = object : JcInterpreterObserver { + override fun onEntryPoint( + simpleValueResolver: JcSimpleValueResolver, + stmt: JcMethodEntrypointInst, + stepScope: JcStepScope, + ) = Unit + + override fun onMethodApproximation( + call: JcMethodCall, + applied: Boolean, + elapsedNanos: Long, + failure: String?, + ) { + approximationAttempts++ + val appliedArraycopy = applied && call.method.enclosingClass.name == "java.lang.System" && + call.method.name == "arraycopy" + if (appliedArraycopy) modeledArraycopyApplications++ + } + } + + val methodNames = listOf( + "successor", + "voidSuccessor", + "independentResults", + "primitiveBounds", + "modeledNative", + "ordinaryBody", + ) + for (methodName in methodNames) { + val method = owner.declaredMethods.single { it.name == methodName } + + val states = JcMachine( + cp = classpath, + options = options, + jcMachineOptions = JcMachineOptions( + forkOnImplicitExceptions = false, + enableMethodApproximations = modelsEnabled, + residualCallPolicy = policy, + ), + interpreterObserver = observer, + ).use { machine -> machine.analyze(method) } + + assertTrue(states.isNotEmpty(), "$modelsEnabled/$policy/$methodName") + val ordinaryBody = methodName == "ordinaryBody" + val modeledNative = methodName == "modeledNative" && modelsEnabled + val methodHasNoResidualCalls = ordinaryBody || modeledNative + val stopsAtNativeCall = policy == JcResidualCallPolicy.STOP && !methodHasNoResidualCalls + if (stopsAtNativeCall) { + assertTrue(states.all { it.residualCallStop != null }) + assertTrue(states.all { it.methodResult == JcMethodResult.NoCall }) + assertTrue(states.all { it.callStack.isNotEmpty() }) + assertTrue(states.all { it.clone().residualCallStop == it.residualCallStop }) + continue + } + + assertTrue(states.all { it.methodResult is JcMethodResult.Success }) + assertFalse(states.any { it.residualCallStop != null }) + val values = states.map(::returnValue).toSet() + val expected = when (methodName) { + "independentResults" -> setOf(1, 2) + "primitiveBounds" -> setOf(1) + "modeledNative" -> if (modelsEnabled) setOf(17) else setOf(0) + else -> setOf(17) + } + assertEquals(expected, values, "$modelsEnabled/$policy/$methodName") + } + + if (modelsEnabled) { + assertTrue(approximationAttempts > 0) + assertTrue(modeledArraycopyApplications > 0) + } else { + assertEquals(0, approximationAttempts) + assertEquals(0, modeledArraycopyApplications) + } + } + + private fun returnValue(state: JcState): Int { + val result = state.methodResult as JcMethodResult.Success + val concrete = state.models.first().eval(result.value) as KBitVec32Value + return concrete.intValue + } +} diff --git a/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaPilotClasspath.kt b/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaPilotClasspath.kt new file mode 100644 index 0000000000..5b51fa3056 --- /dev/null +++ b/usvm-jvm/src/test/kotlin/org/usvm/experiments/JavaPilotClasspath.kt @@ -0,0 +1,40 @@ +package org.usvm.experiments + +import org.jacodb.api.jvm.JcClasspath +import org.jacodb.approximation.Approximations +import org.jacodb.impl.features.InMemoryHierarchy +import org.jacodb.impl.jacodb +import org.usvm.machine.interpreter.transformers.JcMultiDimArrayAllocationTransformer +import org.usvm.machine.interpreter.transformers.JcStringConcatTransformer +import org.usvm.util.classpathWithApproximations +import java.io.File + +internal suspend fun withPilotClasspath( + libraries: List, + approximationsEnabled: Boolean, + action: (JcClasspath) -> Unit, +) { + val database = jacodb { + useProcessJavaRuntime() + installFeatures(InMemoryHierarchy) + if (approximationsEnabled) installFeatures(Approximations(emptyList())) + loadByteCode(libraries) + } + database.use { db -> + val features = listOf(JcMultiDimArrayAllocationTransformer, JcStringConcatTransformer) + val cp = if (approximationsEnabled) { + val requiredVariables = listOf("usvm.jvm.api.jar.path", "usvm.jvm.approximations.jar.path") + val artifactsAvailable = requiredVariables.all { name -> System.getenv(name)?.let(::File)?.isFile == true } + require(artifactsAvailable) { + "ON requires both actual approximation/API artifacts; refusing a mislabeled bare classpath" + } + db.classpathWithApproximations(libraries, features) + } else { + db.classpath(libraries, features) + } + cp.use { classpath -> + db.awaitBackgroundJobs() + action(classpath) + } + } +}