Added hack for non-null value field in strings (#165)

Author: Damtev

usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt

@@ -51,6 +51,7 @@ import org.usvm.api.targets.JcTarget
 import org.usvm.collection.array.UArrayIndexLValue
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.forkblacklists.UForkBlackList
+import org.usvm.isStaticHeapRef
 import org.usvm.machine.JcApplicationGraph
 import org.usvm.machine.JcConcreteMethodCallInst
 import org.usvm.machine.JcContext
@@ -295,6 +296,12 @@ class JcInterpreter(
                     },
                 )
 
+                // TODO usvm-sbft-merge: hack to prevent NPE for the `value` field in strings
+                handleStringValueField(
+                    scope,
+                    method,
+                ) { stmt.arguments.first().asExpr(ctx.addressSort) }
+
                 scope.doWithState {
                     addNewMethodCall(stmt, entryPoint)
                 }
@@ -322,6 +329,32 @@ class JcInterpreter(
         }
     }
 
+    private fun handleStringValueField(scope: JcStepScope, method: JcMethod, stringRefBlock: () -> UHeapRef) {
+        with(ctx) {
+            if (method.isStatic || method.isConstructor) {
+                return
+            }
+
+            val type = method.enclosingClass.toType()
+            if (type != stringType) {
+                return
+            }
+
+            val stringThisRef = stringRefBlock()
+            if (isStaticHeapRef(stringThisRef)) {
+                // For string literals we set `value` explicitly
+                return
+            }
+
+            val stringValueLValue = UFieldLValue(addressSort, stringThisRef, stringValueField.field)
+            val stringValue = scope.calcOnState { memory.read(stringValueLValue) }
+
+            val notNullValueConstraint = mkEq(stringValue, nullRef).not()
+            scope.assert(notNullValueConstraint)
+                ?: error("Cannot make `java.lang.String#value` not-null for string $stringThisRef")
+        }
+    }
+
     private inline fun handleInnerClassMethodCall(
         scope: JcStepScope,
         enclosingType: JcClassType,

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

@@ -519,4 +519,12 @@ public String equalsIgnoreCase(String s) {
     public String listToString() {
         return Arrays.asList("a", "b", "c").toString();
     }
+
+    public int getSymbolicLength(String s) {
+        if (s == null) {
+            return -1;
+        }
+
+        return s.length();
+    }
 }

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

@@ -695,4 +695,14 @@ internal class StringExamplesTest : JavaMethodTestRunner() {
             { _, r -> r == "[a, b, c]" },
         )
     }
+
+    @Test
+    fun testGetSymbolicLength() {
+        checkDiscoveredProperties(
+            StringExamples::getSymbolicLength,
+            eq(2),
+            { _, s, r -> s == null && r == -1 },
+            { _, s, r -> s != null && r == s.length },
+        )
+    }
 }