[JVM] Make the pinned model string length bound configurable

usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt

@@ -108,6 +108,7 @@ import kotlin.reflect.KFunction2
 class JcMethodApproximationResolver(
     private val ctx: JcContext,
     private val applicationGraph: JcApplicationGraph,
+    private val options: JcMachineOptions,
 ) {
     private var currentScope: JcStepScope? = null
     private val scope: JcStepScope
@@ -1068,6 +1069,15 @@ class JcMethodApproximationResolver(
                 scope.assert(arg)?.let { ctx.voidValue }
             }
             dispatchUsvmApiMethod(Engine::assumeSymbolic) {
+                val skipStringModelBound = !options.enforceModelStringLengthBound && scope.calcOnState {
+                    val caller = lastEnteredMethod
+                    caller.enclosingClass.name == "java.lang.String" && caller.name == "_assumeInvariants" &&
+                        caller.parameters.singleOrNull()?.type?.typeName == "java.lang.String"
+                }
+                // aa9e358446 has one assumeSymbolic call in this private helper: logical length <= 50.
+                // Its coder, non-null backing and nonnegative-length Engine.assume calls still execute.
+                if (skipStringModelBound) return@dispatchUsvmApiMethod ctx.voidValue
+
                 val instance = it.arguments[0].asExpr(ctx.addressSort)
                 val condition = it.arguments[1].asExpr(ctx.booleanSort)
                 val assumptionConstraint = foldHeapRefWithStaticAsConcrete<UBoolExpr>(

usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachineOptions.kt

@@ -26,6 +26,9 @@ data class JcMachineOptions(
     /** Local experiment toggle for the interpreter's built-in method models. */
     val enableMethodApproximations: Boolean = true,
 
+    /** Retain the pinned stdlib model's lazy length <= 50 restriction on symbolic Strings. */
+    val enforceModelStringLengthBound: 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

@@ -738,7 +738,7 @@ class JcInterpreter(
         scope: JcStepScope,
     ): Unit = resolveVirtualInvoke(ctx, methodCall, scope, typeSelector, options.forkOnRemainingTypes)
 
-    private val approximationResolver = JcMethodApproximationResolver(ctx, applicationGraph)
+    private val approximationResolver = JcMethodApproximationResolver(ctx, applicationGraph, options)
 
     @Suppress("TooGenericExceptionCaught") // Observe and rethrow the original engine error.
     private fun approximateMethod(scope: JcStepScope, methodCall: JcMethodCall): Boolean {

usvm-jvm/src/samples/java/org/usvm/samples/strings/ModelStringDomain.java

@@ -0,0 +1,33 @@
+package org.usvm.samples.strings;
+
+import org.usvm.api.Engine;
+
+public class ModelStringDomain {
+    public static int lengthBoundary(String value) {
+        if (value == null) {
+            return -1;
+        }
+
+        return value.length() == 51 ? 1 : 0;
+    }
+
+    public static int userAssumption(String value) {
+        if (value == null) {
+            return -1;
+        }
+
+        Engine.assumeSymbolic(value, value.length() <= 2);
+        return value.length() <= 2 ? 1 : -2;
+    }
+
+    public static int characterBeyondBoundary(String value) {
+        if (value == null) {
+            return -1;
+        }
+        if (value.length() != 51) {
+            return 0;
+        }
+
+        return value.charAt(50) == 'A' ? 1 : 2;
+    }
+}

usvm-jvm/src/test/kotlin/org/usvm/samples/strings/ModelStringDomainTest.kt

@@ -0,0 +1,91 @@
+package org.usvm.samples.strings
+
+import org.jacodb.api.jvm.JcClasspath
+import org.junit.jupiter.api.Test
+import org.usvm.UMachineOptions
+import org.usvm.machine.JcInterpreterObserver
+import org.usvm.machine.JcMachine
+import org.usvm.machine.JcMachineOptions
+import org.usvm.samples.approximations.ApproximationsTestRunner
+import org.usvm.test.util.checkers.eq
+import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
+
+class ModelStringDomainTest : ApproximationsTestRunner() {
+    private var enforceBound = true
+
+    init {
+        options = options.copy(throwExceptionOnStepFailure = true)
+    }
+
+    override fun createMachine(
+        cp: JcClasspath,
+        options: UMachineOptions,
+        interpreterObserver: JcInterpreterObserver?,
+    ): JcMachine = JcMachine(
+        cp = cp,
+        options = options,
+        jcMachineOptions = JcMachineOptions(enforceModelStringLengthBound = enforceBound),
+        interpreterObserver = interpreterObserver,
+    )
+
+    @Test
+    fun `default preserves the explicit legacy model bound`() {
+        enforceBound = true
+
+        checkDiscoveredProperties(
+            ModelStringDomain::lengthBoundary,
+            eq(count = 2),
+            { value, result -> value == null && result == -1 },
+            { value, result -> value != null && value.length <= 50 && result == 0 },
+        )
+    }
+
+    @Test
+    fun `disabling only the model bound admits symbolic strings longer than fifty`() {
+        enforceBound = false
+
+        checkDiscoveredProperties(
+            ModelStringDomain::lengthBoundary,
+            eq(count = 3),
+            { value, result -> value == null && result == -1 },
+            { value, result -> value != null && value.length == 51 && result == 1 },
+            { value, result -> value != null && value.length != 51 && result == 0 },
+        )
+    }
+
+    @Test
+    fun `user symbolic assumptions are still enforced with the model bound disabled`() {
+        enforceBound = false
+
+        checkDiscoveredProperties(
+            ModelStringDomain::userAssumption,
+            eq(count = 2),
+            { value, result -> value == null && result == -1 },
+            { value, result -> value != null && value.length <= 2 && result == 1 },
+            invariants = arrayOf({ value, _ -> value == null || value.length <= 2 }),
+        )
+    }
+
+    @Test
+    fun `character model retains meaningful data past the legacy boundary`() {
+        enforceBound = false
+
+        checkDiscoveredProperties(
+            ModelStringDomain::characterBeyondBoundary,
+            ignoreNumberOfAnalysisResults,
+            { value, result -> value == null && result == -1 },
+            { value, result -> value != null && value.length != 51 && result == 0 },
+            { value, result -> value != null && value.length == 51 && value[50] == 'A' && result == 1 },
+            { value, result -> value != null && value.length == 51 && value[50] != 'A' && result == 2 },
+            invariants = arrayOf({ value, result ->
+                val expected = when {
+                    value == null -> -1
+                    value.length != 51 -> 0
+                    value[50] == 'A' -> 1
+                    else -> 2
+                }
+                result == expected
+            }),
+        )
+    }
+}