[JVM] Expose residual call policies and model observation

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<JcType, USizeSort> {
     private val closeableResources = mutableListOf<AutoCloseable>()
     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() {

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) {}

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() {

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,
 )

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<JcState, JcType, JcInst, JcContext>
 
@@ -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)
+        }
     }
 }

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<JcInst>> = PathNode.root(),
     var methodResult: JcMethodResult = JcMethodResult.NoCall,
     targets: UTargetsSet<JcTarget, JcInst> = UTargetsSet.empty(),
+    var residualCallStop: JcMethodCall? = null,
 ) : UState<JcType, JcMethod, JcInst, JcContext, JcTarget, JcState>(
     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()

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();
+    }
+}