Process runner (#29)

* Runner implementation

* Rewrite test infrastructure on top of process runner

* Fix z3 native library load on Windows

.github/workflows/build-and-run-tests.yml

@@ -37,13 +37,11 @@ jobs:
             build
             --no-daemon
             --continue
-            -Pz3.runBenchmarksBasedTests=false
-            -Pbitwuzla.runBenchmarksBasedTests=false
+            -PrunBenchmarksBasedTests=false
 
-# todo: test report uploading is temporarily disabled (https://github.com/UnitTestBot/ksmt/pull/18)
-#      - name: Upload ksmt test reports
-#        uses: actions/upload-artifact@v3
-#        if: always()
-#        with:
-#          name: ksmt_tests_report
-#          path: ./**/build/reports/tests/test/
+      - name: Upload ksmt test reports
+        uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: ksmt_tests_report
+          path: ./**/build/reports/tests/test/

.github/workflows/run-long-tests.yml

@@ -27,8 +27,7 @@ jobs:
             build
             --no-daemon
             --continue
-            -Pz3.runBenchmarksBasedTests=true
-            -Pbitwuzla.runBenchmarksBasedTests=true
+            -PrunBenchmarksBasedTests=true
 
       - name: Upload ksmt test reports
         uses: actions/upload-artifact@v3

detekt.yml

@@ -125,7 +125,7 @@ complexity:
     ignoreDefaultParameters: false
     ignoreDataClasses: true
     ignoreAnnotatedParameter: []
-    excludes: ['**/test/**', '**/example/**']
+    excludes: ['**/test/**', '**/example/**', '**/generated/**']
   MethodOverloading:
     active: false
     threshold: 6
@@ -187,7 +187,7 @@ empty-blocks:
     active: true
   EmptyFunctionBlock:
     active: true
-    ignoreOverridden: false
+    ignoreOverridden: true
   EmptyIfBlock:
     active: true
   EmptyInitBlock:
@@ -276,6 +276,7 @@ exceptions:
 
 naming:
   active: true
+  excludes: [ '**/test/**', '**/example/**', '**/generated/**' ]
   BooleanPropertyNaming:
     active: false
     allowedPattern: '^(is|has|are)'
@@ -559,6 +560,7 @@ style:
     active: false
   MaxLineLength:
     active: true
+    excludes: [ '**/test/**', '**/example/**', '**/generated/**' ]
     maxLineLength: 120
     excludePackageStatements: true
     excludeImportStatements: true
@@ -675,6 +677,6 @@ style:
     active: true
   WildcardImport:
     active: true
-    excludes: ['**/test/**', '**/example/**']
+    excludes: ['**/test/**', '**/example/**', '**/generated/**']
     excludeImports:
       - 'java.util.*'

ksmt-bitwuzla/build.gradle.kts

@@ -13,12 +13,9 @@ val bitwuzlaNative by configurations.creating
 
 dependencies {
     implementation(project(":ksmt-core"))
-    implementation("net.java.dev.jna:jna:5.12.0")
+    api("net.java.dev.jna:jna:5.12.0")
     implementation("net.java.dev.jna:jna-platform:5.12.0")
 
-    testImplementation(project(":ksmt-z3"))
-    testImplementation(testFixtures(project(":ksmt-z3")))
-
     bitwuzlaNative("bitwuzla", "bitwuzla-native-linux-x86-64", "1.0", ext = "zip")
     bitwuzlaNative("bitwuzla", "bitwuzla-native-win32-x86-64", "1.0", ext = "zip")
 }
@@ -38,32 +35,6 @@ tasks.withType<ProcessResources> {
     }
 }
 
-val runBenchmarksBasedTests = project.booleanProperty("bitwuzla.runBenchmarksBasedTests") ?: false
-
-// skip big benchmarks to achieve faster tests build and run time
-val skipBigBenchmarks = project.booleanProperty("bitwuzla.skipBigBenchmarks") ?: true
-
-val smtLibBenchmarks = listOfNotNull(
-    "QF_UF", // 100M
-    "ABV", // 400K
-    if (!skipBigBenchmarks) "AUFBV" else null, // 1.2G
-    if (!skipBigBenchmarks) "BV" else null, // 847M
-    "QF_ABV", // 253M
-    if (!skipBigBenchmarks) "QF_BV" else null// 12.3G
-)
-
-val smtLibBenchmarkTestData = smtLibBenchmarks.map { mkSmtLibBenchmarkTestData(it) }
-val prepareTestData by tasks.registering {
-    dependsOn.addAll(smtLibBenchmarkTestData)
-}
-
-tasks.withType<Test> {
-    if (runBenchmarksBasedTests) {
-        environment("bitwuzla.benchmarksBasedTests", "enabled")
-        dependsOn.add(prepareTestData)
-    }
-}
-
 publishing {
     publications {
         create<MavenPublication>("maven") {

ksmt-core/build.gradle.kts

@@ -2,11 +2,10 @@ import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
 
 plugins {
     id("org.ksmt.ksmt-base")
-    `java-test-fixtures`
 }
 
 dependencies {
-    testFixturesApi("org.junit.jupiter", "junit-jupiter-params", "5.8.2")
+
 }
 
 tasks.withType<KotlinCompile> {
@@ -16,7 +15,7 @@ tasks.withType<KotlinCompile> {
 publishing {
     publications {
         create<MavenPublication>("maven") {
-            from(components["java"].also { removeTestFixtures(it) })
+            from(components["java"])
             artifact(tasks["kotlinSourcesJar"])
         }
     }

ksmt-core/src/main/kotlin/org/ksmt/utils/NativeLibraryLoader.kt

@@ -38,7 +38,9 @@ object NativeLibraryLoader {
                 continue
             }
 
-            val libFile = Files.createTempFile(libName, libraryExt)
+            // use directory to preserve dll name on Windows
+            val libUnpackDirectory = Files.createTempDirectory("ksmt")
+            val libFile = libUnpackDirectory.resolve(libName + libraryExt)
 
             NativeLibraryLoader::class.java.classLoader
                 .getResourceAsStream(resourceName)
@@ -47,6 +49,9 @@ object NativeLibraryLoader {
                 }
 
             System.load(libFile.toAbsolutePath().toString())
+
+            // tmp files are not removed on Windows
+            libFile.toFile().delete()
         }
     }
 }