diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts index 5075d846cd..f44bbb67a0 100644 --- a/buildSrc/build.gradle.kts +++ b/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" diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 03474c51d5..74cae65670 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/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" diff --git a/buildSrc/src/main/kotlin/DetektConfiguration.kt b/buildSrc/src/main/kotlin/DetektConfiguration.kt index b1fa87b9b9..6856f8f9ad 100644 --- a/buildSrc/src/main/kotlin/DetektConfiguration.kt +++ b/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 diff --git a/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts b/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts index 1ae09d4c0e..f0337b7388 100644 --- a/buildSrc/src/main/kotlin/usvm.kotlin-conventions.gradle.kts +++ b/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 { - kotlinOptions { - jvmTarget = JavaVersion.VERSION_1_8.toString() - freeCompilerArgs += "-Xsam-conversions=class" + compilerOptions { + jvmTarget = JvmTarget.JVM_1_8 allWarningsAsErrors = true + freeCompilerArgs.add("-Xsam-conversions=class") } } } diff --git a/buildSrc/src/main/kotlin/usvmpython/tasks/JNIHeaderTask.kt b/buildSrc/src/main/kotlin/usvmpython/tasks/JNIHeaderTask.kt index 847d463911..2dcd365322 100644 --- a/buildSrc/src/main/kotlin/usvmpython/tasks/JNIHeaderTask.kt +++ b/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() diff --git a/buildSrc/src/main/kotlin/usvmpython/tasks/PythonSamplesTasks.kt b/buildSrc/src/main/kotlin/usvmpython/tasks/PythonSamplesTasks.kt index a486687aec..e2e2e9e3c2 100644 --- a/buildSrc/src/main/kotlin/usvmpython/tasks/PythonSamplesTasks.kt +++ b/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 diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index 2f4c528063..4d32e6d26f 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -63,8 +63,8 @@ private fun createPathSelector( PathSelectionStrategy.DEPTH -> createDepthPathSelector() PathSelectionStrategy.DEPTH_RANDOM -> createDepthPathSelector(random) - PathSelectionStrategy.FORK_DEPTH -> createForkDepthPathSelector() - PathSelectionStrategy.FORK_DEPTH_RANDOM -> createForkDepthPathSelector(random) + PathSelectionStrategy.FORK_DEPTH -> createForkDepthPathSelector() + PathSelectionStrategy.FORK_DEPTH_RANDOM -> createForkDepthPathSelector(random) PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector( requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" }, @@ -106,7 +106,8 @@ private fun createPathSelector( } selectors.singleOrNull()?.let { selector -> - val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory) + @Suppress("UNCHECKED_CAST") + val mergingSelector = createMergingPathSelector(initialStates, selector as UPathSelector, options, cfgStatisticsFactory) val resultSelector = mergingSelector.wrapIfRequired(options, loopStatisticFactory) resultSelector.add(initialStates.toList()) return resultSelector @@ -117,7 +118,8 @@ private fun 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) val mergingSelector = createMergingPathSelector(initialStates, selector, options, cfgStatisticsFactory) val resultSelector = mergingSelector.wrapIfRequired(options, loopStatisticFactory) @@ -128,8 +130,9 @@ private fun 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, options, cfgStatisticsFactory) mergingSelector.wrapIfRequired(options, loopStatisticFactory) } diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt index 6138db8534..f707488800 100644 --- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt +++ b/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 = when (options.stateCollectionStrategy) { - StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { + StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { it.methodResult is JcMethodResult.JcException } diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt index 3741d29245..74f848ba3e 100644 --- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleMachine.kt +++ b/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 = when (options.stateCollectionStrategy) { - StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { + StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { it.exceptionRegister != null } StateCollectionStrategy.REACHED_TARGET -> TargetsReachedStatesCollector() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index d82ac0ab88..67a14bf965 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/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 = when (options.stateCollectionStrategy) { - StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { + StateCollectionStrategy.COVERED_NEW -> CoveredNewStatesCollector(coverageStatistics) { it.methodResult is TsMethodResult.TsException } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 082324130d..fbfb946859 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1004,23 +1004,23 @@ class TsSimpleValueResolver( } } - override fun visit(local: EtsLocal): UExpr { - if (local.name == "NaN") { + override fun visit(value: EtsLocal): UExpr { + 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) } }