From 0c45c6b52095668188d7eedb9a6949162993c595 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=D0=A1=D1=82=D0=B0=D1=80=D1=86=D0=B5=D0=B2=20=D0=9C=D0=B0?= =?UTF-8?q?=D1=82=D0=B2=D0=B5=D0=B9?= Date: Tue, 18 Nov 2025 17:08:37 +0300 Subject: [PATCH] Supports Kotlin nullable fields MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Старцев Матвей --- buildSrc/src/main/kotlin/Dependencies.kt | 7 +++ .../utils/JcConcreteTestStateResolver.kt | 3 -- usvm-jvm-spring-runner/build.gradle.kts | 2 +- .../kotlin/machine/JcSpringTestObserver.kt | 3 +- .../kotlin/machine/ps/JcSpringWeighters.kt | 10 ++--- .../JcSpringTestStateResolver.kt | 22 +++++++++ .../kotlin/testGeneration/TestGenerator.kt | 26 +++++++++-- .../org/usvm/machine/JcApproximations.kt | 45 ++++++++++++++++++- .../src/main/java/org/usvm/api/Engine.java | 17 +++++-- usvm-jvm/usvm-jvm-util/build.gradle.kts | 1 + 10 files changed, 119 insertions(+), 17 deletions(-) diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 1e312d34fe..de7d7f3e04 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/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", diff --git a/usvm-jvm-concrete/src/main/kotlin/utils/JcConcreteTestStateResolver.kt b/usvm-jvm-concrete/src/main/kotlin/utils/JcConcreteTestStateResolver.kt index 9dfb9f11a9..be297c6ebe 100644 --- a/usvm-jvm-concrete/src/main/kotlin/utils/JcConcreteTestStateResolver.kt +++ b/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 diff --git a/usvm-jvm-spring-runner/build.gradle.kts b/usvm-jvm-spring-runner/build.gradle.kts index c5d055d5e9..92ba56691c 100644 --- a/usvm-jvm-spring-runner/build.gradle.kts +++ b/usvm-jvm-spring-runner/build.gradle.kts @@ -339,7 +339,7 @@ tasks.register("benchmarkKlaw") { } tasks.register("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) } diff --git a/usvm-jvm-spring/src/main/kotlin/machine/JcSpringTestObserver.kt b/usvm-jvm-spring/src/main/kotlin/machine/JcSpringTestObserver.kt index 28d2c6695c..31038d3f48 100644 --- a/usvm-jvm-spring/src/main/kotlin/machine/JcSpringTestObserver.kt +++ b/usvm-jvm-spring/src/main/kotlin/machine/JcSpringTestObserver.kt @@ -13,7 +13,8 @@ class JcSpringTestObserver : UMachineObserver { 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()) diff --git a/usvm-jvm-spring/src/main/kotlin/machine/ps/JcSpringWeighters.kt b/usvm-jvm-spring/src/main/kotlin/machine/ps/JcSpringWeighters.kt index 9538757b2f..af5ac3c582 100644 --- a/usvm-jvm-spring/src/main/kotlin/machine/ps/JcSpringWeighters.kt +++ b/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, diff --git a/usvm-jvm-spring/src/main/kotlin/testGeneration/JcSpringTestStateResolver.kt b/usvm-jvm-spring/src/main/kotlin/testGeneration/JcSpringTestStateResolver.kt index 2930adb859..973fdce23f 100644 --- a/usvm-jvm-spring/src/main/kotlin/testGeneration/JcSpringTestStateResolver.kt +++ b/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 +): Exception( + "${fields.count()} not nullable fields are null of ${ref.address} ${classType.name}" +) + class JcSpringTestStateResolver( ctx: JcContext, model: UModelBase, @@ -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): List? { + 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): UTestExpression? { // If this condition removed, think about decoders for parent classes! if (superType != classpath.objectType) diff --git a/usvm-jvm-spring/src/main/kotlin/testGeneration/TestGenerator.kt b/usvm-jvm-spring/src/main/kotlin/testGeneration/TestGenerator.kt index c41a852bb1..f9e101975a 100644 --- a/usvm-jvm-spring/src/main/kotlin/testGeneration/TestGenerator.kt +++ b/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): 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().check(newPs)) { + is USatResult> -> generateTest(result.model) + else -> null + } + } + return SpringTestInfo(handler, isExceptional, uTest) } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt index d9b3a85b95..3642f96d19 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt +++ b/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 UExpr<*>?>.dispatchMakeCommonKotlinSymbolic( + apiMethod: KFunction1, + makeMethod: StepScope.(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 UExpr<*>?>.dispatchMkRef( + apiMethod: KFunction1, + body: (JcMethodCall) -> UExpr<*>?, + ) = dispatchUsvmApiMethod(apiMethod, body) + private fun MutableMap UExpr<*>?>.dispatchMkRef2( apiMethod: KFunction2>, body: (JcMethodCall) -> UExpr<*>?, diff --git a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java index 4407ca8988..99014a5f53 100644 --- a/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java +++ b/usvm-jvm/usvm-jvm-api/src/main/java/org/usvm/api/Engine.java @@ -37,9 +37,20 @@ public static T makeSymbolicSubtype(Class clazz) { } @SuppressWarnings("unused") - public static T makeNullableSymbolicSubtype(Class clazz) { - return null; - } + public static T makeNullableSymbolicSubtype(Class clazz) { return null; } + + // Creates symbolic instance of class with assumed nullable fields + @SuppressWarnings("unused") + public static T makeKotlinSymbolic(Class clazz) { return null; } + + @SuppressWarnings("unused") + public static T makeNullableKotlinSymbolic(Class clazz) { return null; } + + @SuppressWarnings("unused") + public static T makeKotlinSymbolicSubtype(Class clazz) { return null; } + + @SuppressWarnings("unused") + public static T makeNullableKotlinSymbolicSubtype(Class clazz) { return null; } public static boolean makeSymbolicBoolean() { return false; diff --git a/usvm-jvm/usvm-jvm-util/build.gradle.kts b/usvm-jvm/usvm-jvm-util/build.gradle.kts index 70bc670f08..8c58013c9a 100644 --- a/usvm-jvm/usvm-jvm-util/build.gradle.kts +++ b/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 {