Bump Kotlin to 2.2.0

buildSrc/build.gradle.kts

@@ -2,7 +2,7 @@ plugins {
     `kotlin-dsl`
 }
 
-val kotlinVersion = "2.1.0"
+val kotlinVersion = "2.2.0"
 val detektVersion = "1.23.5"
 val gjavahVersion = "0.3.1"
 

buildSrc/src/main/kotlin/Dependencies.kt

@@ -9,7 +9,7 @@ object Versions {
     const val jacodb = "4ff7243d3a"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
-    const val kotlin = "2.1.0"
+    const val kotlin = "2.2.0"
     const val kotlin_logging = "3.0.5"
     const val kotlinx_collections = "0.3.8"
     const val kotlinx_coroutines = "1.10.0"

buildSrc/src/main/kotlin/DetektConfiguration.kt

@@ -1,5 +1,5 @@
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.detekt
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.detektPlugins
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.detekt
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.detektPlugins
 import io.gitlab.arturbosch.detekt.Detekt
 import io.gitlab.arturbosch.detekt.DetektCreateBaselineTask
 import io.gitlab.arturbosch.detekt.report.ReportMergeTask

buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts

@@ -1,3 +1,4 @@
+import org.jetbrains.kotlin.gradle.dsl.JvmTarget
 import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
 
 plugins {
@@ -36,10 +37,10 @@ tasks {
         options.compilerArgs.add("-Werror")
     }
     withType<KotlinCompile> {
-        kotlinOptions {
-            jvmTarget = JavaVersion.VERSION_1_8.toString()
-            freeCompilerArgs += "-Xsam-conversions=class"
+        compilerOptions {
+            jvmTarget = JvmTarget.JVM_1_8
             allWarningsAsErrors = true
+            freeCompilerArgs.add("-Xsam-conversions=class")
         }
     }
 }

buildSrc/src/main/kotlin/usvmpython/tasks/JNIHeaderTask.kt

@@ -1,13 +1,12 @@
 package usvmpython.tasks
 
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.main
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.sourceSets
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.main
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.sourceSets
 import org.glavo.javah.JavahTask
 import org.gradle.api.Project
 import usvmpython.getGeneratedHeadersPath
 import usvmpython.CPYTHON_ADAPTER_CLASS
 
-
 fun Project.generateJNIForCPythonAdapterTask() {
     val task = JavahTask()
     task.outputDir = getGeneratedHeadersPath().toPath()

buildSrc/src/main/kotlin/usvmpython/tasks/PythonSamplesTasks.kt

@@ -1,7 +1,7 @@
 package usvmpython.tasks
 
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.sourceSets
-import gradle.kotlin.dsl.accessors._466a692754d3da37fc853e1c7ad8ae1e.test
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.sourceSets
+import gradle.kotlin.dsl.accessors._ed4eee7f6ae7e6c7746c5b956eb7e0be.test
 import org.gradle.api.Project
 import org.gradle.api.tasks.Exec
 import org.gradle.api.tasks.JavaExec

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -63,8 +63,8 @@ private fun <Method, Statement, Target, State> createPathSelector(
             PathSelectionStrategy.DEPTH -> createDepthPathSelector()
             PathSelectionStrategy.DEPTH_RANDOM -> createDepthPathSelector(random)
 
-            PathSelectionStrategy.FORK_DEPTH -> createForkDepthPathSelector()
-            PathSelectionStrategy.FORK_DEPTH_RANDOM -> createForkDepthPathSelector(random)
+            PathSelectionStrategy.FORK_DEPTH -> createForkDepthPathSelector<Method, Statement, State>()
+            PathSelectionStrategy.FORK_DEPTH_RANDOM -> createForkDepthPathSelector<Method, Statement, State>(random)
 
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" },
@@ -106,7 +106,8 @@ private fun <Method, Statement, Target, State> createPathSelector(
     }
 
     selectors.singleOrNull()?.let { selector ->
-        val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory)
+        @Suppress("UNCHECKED_CAST")
+        val mergingSelector = createMergingPathSelector(initialStates, selector as UPathSelector<State>, options, cfgStatisticsFactory)
         val resultSelector = mergingSelector.wrapIfRequired(options, loopStatisticFactory)
         resultSelector.add(initialStates.toList())
         return resultSelector
@@ -117,7 +118,8 @@ private fun <Method, Statement, Target, State> createPathSelector(
     val selector = when (options.pathSelectorCombinationStrategy) {
         PathSelectorCombinationStrategy.INTERLEAVED -> {
             // Since all selectors here work as one, we can wrap an interleaved selector only.
-            val selector = InterleavedPathSelector(selectors)
+            @Suppress("UNCHECKED_CAST")
+            val selector = InterleavedPathSelector(selectors as UPathSelector<State>)
 
             val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory)
             val resultSelector = mergingSelector.wrapIfRequired(options, loopStatisticFactory)
@@ -128,8 +130,9 @@ private fun <Method, Statement, Target, State> createPathSelector(
 
         PathSelectorCombinationStrategy.PARALLEL -> {
             // Here we should wrap all selectors independently since they work in parallel.
+            @Suppress("UNCHECKED_CAST")
             val wrappedSelectors = selectors.map { selector ->
-                val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory)
+                val mergingSelector = createMergingPathSelector(initialStates, selector as UPathSelector<State>, options, cfgStatisticsFactory)
                 mergingSelector.wrapIfRequired(options, loopStatisticFactory)
             }
 

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

@@ -27,6 +27,7 @@ import org.usvm.statistics.TransitiveCoverageZoneObserver
 import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
+import org.usvm.statistics.collectors.StatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatistics
@@ -107,9 +108,9 @@ class JcMachine(
             { loopTracker }
         )
 
-        val statesCollector =
+        val statesCollector: StatesCollector<JcState> =
             when (options.stateCollectionStrategy) {
-                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<JcState>(coverageStatistics) {
+                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) {
                     it.methodResult is JcMethodResult.JcException
                 }
 

usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt

@@ -18,6 +18,7 @@ import org.usvm.statistics.TimeStatistics
 import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
+import org.usvm.statistics.collectors.StatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CallGraphStatisticsImpl
@@ -77,9 +78,9 @@ class SampleMachine(
             { callGraphStatistics }
         )
 
-        val statesCollector =
+        val statesCollector: StatesCollector<SampleState> =
             when (options.stateCollectionStrategy) {
-                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<SampleState>(coverageStatistics) {
+                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) {
                     it.exceptionRegister != null
                 }
                 StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector()

usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt

@@ -22,6 +22,7 @@ import org.usvm.statistics.TimeStatistics
 import org.usvm.statistics.UMachineObserver
 import org.usvm.statistics.collectors.AllStatesCollector
 import org.usvm.statistics.collectors.CoveredNewStatesCollector
+import org.usvm.statistics.collectors.StatesCollector
 import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatisticsImpl
@@ -82,9 +83,9 @@ class TsMachine(
             callGraphStatisticsFactory = { callGraphStatistics },
         )
 
-        val statesCollector =
+        val statesCollector: StatesCollector<TsState> =
             when (options.stateCollectionStrategy) {
-                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector<TsState>(coverageStatistics) {
+                StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) {
                     it.methodResult is TsMethodResult.TsException
                 }
 

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -1004,23 +1004,23 @@ class TsSimpleValueResolver(
         }
     }
 
-    override fun visit(local: EtsLocal): UExpr<out USort> {
-        if (local.name == "NaN") {
+    override fun visit(value: EtsLocal): UExpr<out USort> {
+        if (value.name == "NaN") {
             return ctx.mkFp64NaN()
         }
-        if (local.name == "Infinity") {
+        if (value.name == "Infinity") {
             return ctx.mkFpInf(false, ctx.fp64Sort)
         }
 
         val currentMethod = scope.calcOnState { lastEnteredMethod }
-        if (local !in currentMethod.getDeclaredLocals()) {
-            if (local.type is EtsFunctionType) {
+        if (value !in currentMethod.getDeclaredLocals()) {
+            if (value.type is EtsFunctionType) {
                 // TODO: function pointers should be "singletons"
-                return scope.calcOnState { memory.allocConcrete(local.type) }
+                return scope.calcOnState { memory.allocConcrete(value.type) }
             }
         }
 
-        val lValue = resolveLocal(local)
+        val lValue = resolveLocal(value)
         return scope.calcOnState { memory.read(lValue) }
     }