Supports Kotlin nullable fields

buildSrc/src/main/kotlin/Dependencies.kt

@@ -11,6 +11,7 @@ object Versions {
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
     const val kotlin_logging = "3.0.5"
+    const val kotlin_metadata = "2.2.21"
     const val kotlinx_collections = "0.3.8"
     const val kotlinx_coroutines = "1.10.0"
     const val kotlinx_serialization = "1.7.3"
@@ -64,6 +65,12 @@ object Libs {
         version = Versions.kotlin_logging
     )
 
+    val kotlin_metadata = dep(
+        group = "org.jetbrains.kotlin",
+        name = "kotlin-metadata-jvm",
+        version = Versions.kotlin_metadata
+    )
+
     // https://github.com/qos-ch/slf4j
     val slf4j_simple = dep(
         group = "org.slf4j",

usvm-jvm-concrete/src/main/kotlin/utils/JcConcreteTestStateResolver.kt

@@ -2,13 +2,10 @@
 
 import machine.state.concreteMemory.JcConcreteMemory
 import org.jacodb.api.jvm.JcClassType
-import org.jacodb.api.jvm.JcField
 import org.jacodb.api.jvm.JcType
 import org.jacodb.api.jvm.JcTypedField
 import org.jacodb.api.jvm.JcTypedMethod
 import org.jacodb.api.jvm.ext.findType
-import org.jacodb.api.jvm.ext.findTypeOrNull
-import org.jacodb.api.jvm.ext.isAssignable
 import org.usvm.UConcreteHeapRef
 import org.usvm.UHeapRef
 import org.usvm.api.util.JcTestStateResolver

usvm-jvm-spring-runner/build.gradle.kts

@@ -339,7 +339,7 @@ tasks.register<JavaExec>("benchmarkKlaw") {
 }
 
 tasks.register<JavaExec>("benchmarkKomga") {
-    fillProperties(loadBenchmark("komga-1.21.2.jar"), this)
+    fillProperties(loadBenchmark("komga-1.21.2.jar", "classpath:application.yml"), this)
     mainClass.set("benchmarking.BenchmarkingKt")
     configureSpringAnalysis(this)
 }

usvm-jvm-spring/src/main/kotlin/machine/JcSpringTestObserver.kt

@@ -13,7 +13,8 @@ class JcSpringTestObserver : UMachineObserver<JcSpringState> {
     override fun onStateTerminated(state: JcSpringState, stateReachable: Boolean) {
         if (!stateReachable || !state.canGenerateTest()) return
         try {
-            tests.add(state.generateTest())
+            state.generateTest()?.let { tests.add(it) }
+                ?: println("Test skipped because of unsat path constraints")
         } catch (e: Throwable) {
             println("generation failed with $e")
             println(e.stackTraceToString())

usvm-jvm-spring/src/main/kotlin/machine/ps/JcSpringWeighters.kt

@@ -15,14 +15,14 @@ import org.usvm.ps.weighters.CombinedStateStableFloatWeighter
 import org.usvm.ps.weighters.ForkTracesHolder
 import org.usvm.statistics.CoverageStatistics
 
-private const val uncoveredStateWeighterNorm = 45f
-private const val forkTracesWeighterNorm = 34.1f
-private const val springPathWeighterNorm = 6.8f
-private const val springEdgeCaseWeighterNorm = 11.6f
+private const val uncoveredStateWeighterNorm = 6.4f
+private const val forkTracesWeighterNorm = 46.1f
+private const val springPathWeighterNorm = 15.1f
+private const val springEdgeCaseWeighterNorm = 29.9f
 
 private const val springRegressionSuiteNorm = 0f // TODO: fine tuning
 
-private const val concreteBacktrackWeighterNorm = 2.4f
+private const val concreteBacktrackWeighterNorm = 2.5f
 
 internal fun createSpringWeighters(
     jcSpringMachineOptions: JcSpringMachineOptions,

usvm-jvm-spring/src/main/kotlin/testGeneration/JcSpringTestStateResolver.kt

@@ -13,15 +13,26 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.api.util.JcTestStateResolver
 import org.usvm.collection.field.UFieldLValue
+import org.usvm.jvm.util.name
+import org.usvm.jvm.util.notNullableKotlinFields
 import org.usvm.machine.JcContext
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.model.UModelBase
 import org.usvm.test.api.UTestAllocateMemoryCall
 import org.usvm.test.api.UTestConstructorCall
 import org.usvm.test.api.UTestExpression
+import org.usvm.test.api.UTestNullExpression
 import org.usvm.test.api.spring.JcSpringTestExecutorDecoderApi
 import utils.JcConcreteTestStateResolver
 
+class NullKotlinFields(
+    val ref: UConcreteHeapRef,
+    classType: JcClassType,
+    val fields: List<JcTypedField>
+): Exception(
+    "${fields.count()} not nullable fields are null of ${ref.address} ${classType.name}"
+)
+
 class JcSpringTestStateResolver(
     ctx: JcContext,
     model: UModelBase<JcType>,
@@ -62,11 +73,22 @@ class JcSpringTestStateResolver(
     override fun allocateAndInitializeObject(ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcClassType): UTestExpression {
         val currentRef = if (resolveMode == ResolveMode.CURRENT) heapRef else ref
 
+        type.checkKotlinNullables(currentRef)?.let { throw NullKotlinFields(ref, type, it) }
+
         val allArgsConstructor = type.allArgsConstructorInvocationOrNull(currentRef)
 
         return allArgsConstructor ?: super.allocateAndInitializeObject(ref, heapRef, type)
     }
 
+    private fun JcClassType.checkKotlinNullables(ref: UExpr<UAddressSort>): List<JcTypedField>? {
+        val problemFields = notNullableKotlinFields().filter { field ->
+            val lvalue = UFieldLValue(ctx.typeToSort(field.type), ref, field.field)
+            resolveLValue(lvalue, field.type) is UTestNullExpression
+        }
+
+        return if (problemFields.isEmpty()) null else problemFields
+    }
+
     private fun JcClassType.allArgsConstructorInvocationOrNull(ref: UExpr<UAddressSort>): UTestExpression? {
         // If this condition removed, think about decoders for parent classes!
         if (superType != classpath.objectType)

usvm-jvm-spring/src/main/kotlin/testGeneration/TestGenerator.kt

@@ -11,13 +11,17 @@ import machine.state.tableContent
 import org.jacodb.api.jvm.JcClassOrInterface
 import org.jacodb.api.jvm.JcClasspath
 import org.jacodb.api.jvm.JcMethod
+import org.jacodb.api.jvm.JcType
 import org.jacodb.api.jvm.ext.findClass
 import org.jacodb.api.jvm.ext.toType
 import org.jacodb.impl.features.classpaths.JcUnknownClass
 import org.usvm.UHeapRef
 import org.usvm.api.readField
 import org.usvm.api.typeStreamOf
+import org.usvm.collection.field.UFieldLValue
 import org.usvm.jvm.util.toTypedMethod
+import org.usvm.model.UModelBase
+import org.usvm.solver.USatResult
 import org.usvm.test.api.UTest
 import org.usvm.test.api.UTestClassExpression
 import org.usvm.test.api.UTestMockObject
@@ -119,8 +123,9 @@ private fun JcSpringState.createSpringTestKind(testClass: JcClassOrInterface): J
     }
 }
 
-internal fun JcSpringState.generateTest(): SpringTestInfo {
-    val model = springMemory.getFixedModel(this)
+internal fun JcSpringState.generateTest() = generateTest(springMemory.getFixedModel(this))
+
+private fun JcSpringState.generateTest(model: UModelBase<JcType>): SpringTestInfo? {
     val resolver = JcSpringTestStateResolver(ctx, model, memory, entrypoint.toTypedMethod)
 
     val reqPath = pinnedValues.getValue(JcPinnedKey.requestPath())
@@ -140,7 +145,22 @@ internal fun JcSpringState.generateTest(): SpringTestInfo {
 
     val testKind = createSpringTestKind(testClass)
     val testBuilder = JcStateSpringTestBuilder(ctx.cp, controller, testKind, testClass, this, resolver)
-    val uTest = testBuilder.build()
+
+    val uTest = try {
+        testBuilder.build()
+    } catch (exception: NullKotlinFields) {
+        val newPs = pathConstraints.clone()
+        exception.fields.forEach { field ->
+            val fieldValue = memory.read(UFieldLValue(ctx.addressSort, exception.ref, field.field))
+            newPs += ctx.mkNot(ctx.mkEq(ctx.mkNullRef(), fieldValue))
+        }
+
+        return when (val result = ctx.solver<JcType>().check(newPs)) {
+            is USatResult<UModelBase<JcType>> -> generateTest(result.model)
+            else -> null
+        }
+    }
+
     return SpringTestInfo(handler, isExceptional, uTest)
 }
 

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

@@ -87,6 +87,7 @@ import org.usvm.collection.field.UFieldLValue
 import org.usvm.getIntValue
 import org.usvm.jvm.util.allInstanceFields
 import org.usvm.jvm.util.javaName
+import org.usvm.jvm.util.notNullableKotlinFields
 import org.usvm.machine.interpreter.JcExprResolver
 import org.usvm.machine.interpreter.JcMethodCallSkipWithEnsureInst
 import org.usvm.machine.interpreter.JcStepScope
@@ -1071,6 +1072,16 @@ open class JcMethodApproximationResolver(
             dispatchMakeCommonSymbolic(Engine::makeNullableSymbolic, JcStepScope::makeNullableSymbolicRefWithSameType)
             dispatchMakeCommonSymbolic(Engine::makeSymbolicSubtype, JcStepScope::makeSymbolicRefSubtype)
             dispatchMakeCommonSymbolic(Engine::makeNullableSymbolicSubtype, JcStepScope::makeNullableSymbolicRefSubtype)
+            dispatchMakeCommonKotlinSymbolic(Engine::makeKotlinSymbolic, JcStepScope::makeSymbolicRefWithSameType)
+            dispatchMakeCommonKotlinSymbolic(
+                Engine::makeNullableKotlinSymbolic,
+                JcStepScope::makeNullableSymbolicRefWithSameType
+            )
+            dispatchMakeCommonKotlinSymbolic(Engine::makeKotlinSymbolicSubtype, JcStepScope::makeSymbolicRefSubtype)
+            dispatchMakeCommonKotlinSymbolic(
+                Engine::makeNullableKotlinSymbolicSubtype,
+                JcStepScope::makeNullableSymbolicRefSubtype
+            )
             dispatchMkRef2(Engine::makeSymbolicArray) {
                 val (elementClassRefExpr, sizeExpr) = it.arguments
                 val elementClassRef = elementClassRefExpr.asExpr(ctx.addressSort)
@@ -1323,7 +1334,7 @@ open class JcMethodApproximationResolver(
         val classRefTypeRepresentative = scope.calcOnState {
             memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
         }
-        val ref = scope.makeMethod(classRefTypeRepresentative) ?: error("Unable to crate ref for makeSymbolic")
+        val ref = scope.makeMethod(classRefTypeRepresentative) ?: error("Unable to create ref for makeSymbolic")
 
         ref as UExpr<*>
         check(classRefTypeRepresentative is UConcreteHeapRef)
@@ -1340,6 +1351,38 @@ open class JcMethodApproximationResolver(
         }
     }
 
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMakeCommonKotlinSymbolic(
+        apiMethod: KFunction1<Nothing, Any>,
+        makeMethod: StepScope<JcState, JcType, JcInst, JcContext>.(UHeapRef) -> UHeapRef?,
+    ) = dispatchUsvmApiMethod(apiMethod) {
+        val classRef = it.arguments.single().asExpr(ctx.addressSort)
+        val classRefTypeRepresentative = scope.calcOnState {
+            memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
+        }
+        check(classRefTypeRepresentative is UConcreteHeapRef)
+        val classType = scope.calcOnState { memory.types.typeOf(classRefTypeRepresentative.address) }
+                as? JcClassType ?: error("Non classType in makeKotlinSymbolic")
+
+        val ref = scope.makeMethod(classRefTypeRepresentative) ?: error("Unable to create ref for makeKotlinSymbolic")
+        assertNotNullableFields(ref, classType)
+        ref
+    }
+
+    private fun assertNotNullableFields(value: UHeapRef, type: JcType) {
+        if (type !is JcClassType) return
+        type.notNullableKotlinFields().forEach { field ->
+            val fieldValue = scope.calcOnState { memory.read(UFieldLValue(ctx.addressSort, value, field.field)) }
+            assertNotNullableFields(fieldValue, field.type)
+            val constant = ctx.mkNot(ctx.mkHeapRefEq(ctx.mkNullRef(), fieldValue))
+            scope.assert(constant)
+        }
+    }
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef(
+        apiMethod: KFunction1<Nothing, Any>,
+        body: (JcMethodCall) -> UExpr<*>?,
+    ) = dispatchUsvmApiMethod(apiMethod, body)
+
     private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef2(
         apiMethod: KFunction2<Nothing, Nothing, Array<Any>>,
         body: (JcMethodCall) -> UExpr<*>?,

usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java

@@ -37,9 +37,20 @@ public static <T> T makeSymbolicSubtype(Class<T> clazz) {
     }
 
     @SuppressWarnings("unused")
-    public static <T> T makeNullableSymbolicSubtype(Class<T> clazz) {
-        return null;
-    }
+    public static <T> T makeNullableSymbolicSubtype(Class<T> clazz) { return null; }
+
+    // Creates symbolic instance of class with assumed nullable fields
+    @SuppressWarnings("unused")
+    public static <T> T makeKotlinSymbolic(Class<T> clazz) { return null; }
+
+    @SuppressWarnings("unused")
+    public static <T> T makeNullableKotlinSymbolic(Class<T> clazz) { return null; }
+
+    @SuppressWarnings("unused")
+    public static <T> T makeKotlinSymbolicSubtype(Class<T> clazz) { return null; }
+
+    @SuppressWarnings("unused")
+    public static <T> T makeNullableKotlinSymbolicSubtype(Class<T> clazz) { return null; }
 
     public static boolean makeSymbolicBoolean() {
         return false;

usvm-jvm/usvm-jvm-util/build.gradle.kts

@@ -6,6 +6,7 @@ dependencies {
     implementation(Libs.jacodb_api_jvm)
     implementation(Libs.jacodb_core)
     implementation(Libs.jacodb_approximations)
+    implementation(Libs.kotlin_metadata)
 }
 
 publishing {