Convert to Gradle.kts

Split projects for easier assembly of jars with the application and shadow plugins.

TODO:
* Add z3 libs to application distributions.
* Set up the jacocoRootReport task.
* Copy jars to the dest directory.
* Set up maven-publish and bintray
* Modularize the project for Java 11 compatibility
* Set up cross-os builds for OpenJFX

build.gradle.kts

@@ -0,0 +1,13 @@
+plugins {
+    base
+}
+
+allprojects {
+    group = "hu.bme.mit.inf.theta"
+    version = "0.0.1-SNAPSHOT"
+
+    apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
+}
+
+val libPath: String by extra { rootProject.rootDir.resolve("lib").path }
+val execPath by extra { "$libPath${File.pathSeparator}${System.getenv("PATH")}" }

buildSrc/build.gradle.kts

@@ -0,0 +1,91 @@
+import java.io.FileOutputStream
+import org.jetbrains.kotlin.gradle.plugin.KotlinSourceSet
+import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
+
+plugins {
+    `java-gradle-plugin`
+    `kotlin-dsl`
+    `kotlin-dsl-precompiled-script-plugins`
+}
+
+repositories {
+    gradlePluginPortal()
+}
+
+apply(from = rootDir.resolve("../gradle/shared-with-buildSrc/mirrors.gradle.kts"))
+
+kotlinDslPluginOptions {
+    experimentalWarning.set(false)
+}
+
+val kotlinVersion: String by project
+val shadowVersion: String by project
+
+// https://github.com/gradle/kotlin-dsl/issues/430#issuecomment-414768887
+fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$version"
+
+dependencies {
+    compileOnly(gradleKotlinDsl())
+    compile(kotlin("gradle-plugin", kotlinVersion))
+    compile(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion))
+}
+
+// Force the embeddable Kotlin compiler version to be the selected kotlinVersion.
+// https://github.com/gradle/kotlin-dsl/issues/1207
+configurations.all {
+    val isKotlinCompiler = name == "embeddedKotlin" || name.startsWith("kotlin") || name.startsWith("kapt")
+    if (!isKotlinCompiler) {
+        resolutionStrategy.eachDependency {
+            if (requested.group == "org.jetbrains.kotlin" && requested.module.name == "kotlin-compiler-embeddable") {
+                useVersion(kotlinVersion)
+            }
+        }
+    }
+}
+
+val versionsClassName = "Versions"
+val generatedVersionsKotlinSrcDir = buildDir.resolve("generated-sources/versions/kotlin")
+val generatedVersionsFile = generatedVersionsKotlinSrcDir.resolve("$versionsClassName.kt")
+
+sourceSets {
+    named("main") {
+        withConvention(KotlinSourceSet::class) {
+            kotlin.srcDir(generatedVersionsKotlinSrcDir)
+        }
+    }
+}
+
+fun generateVersionsSource(): String {
+    val text = StringBuilder()
+
+    text.appendln("object $versionsClassName {")
+
+    for (property in project.properties) {
+        if (property.key.endsWith("Version")) {
+            val keyWithoutVersion = property.key.substringBefore("Version")
+            text.appendln("   const val `$keyWithoutVersion` = \"${property.value}\"")
+        }
+    }
+
+    text.appendln("}")
+
+    return text.toString()
+}
+
+tasks {
+    val generateVersions by creating {
+        description = "Updates Versions.kt from project properties."
+        group = "build"
+        outputs.dirs(generatedVersionsKotlinSrcDir)
+
+        doLast {
+            val versionsSource = generateVersionsSource()
+            generatedVersionsKotlinSrcDir.mkdirs()
+            generatedVersionsFile.writeText(versionsSource)
+        }
+    }
+
+    named("compileKotlin", KotlinCompile::class) {
+        dependsOn(generateVersions)
+    }
+}

buildSrc/gradle.properties

@@ -0,0 +1,10 @@
+javaVersion=11
+kotlinVersion=1.3.0
+shadowVersion=4.0.2
+antlrVersion=4.5.3
+guavaVersion=23.6-jre
+jcommanderVersion=1.72
+z3Version=4.5.0
+junitVersion=4.12
+jacocoVersion=0.8.2
+mockitoVersion=2.2.11

buildSrc/src/main/kotlin/Deps.kt

@@ -0,0 +1,18 @@
+object Deps {
+    val guava = "com.google.guava:guava:${Versions.guava}"
+
+    object Antlr {
+        val antlr = "org.antlr:antlr4:${Versions.antlr}"
+        val runtime = "org.antlr:antlr4-runtime:${Versions.antlr}"
+    }
+
+    val z3 = "z3:com.microsoft.z3:${Versions.z3}"
+
+    val jcommander = "com.beust:jcommander:${Versions.jcommander}"
+
+    val junit4 = "junit:junit:${Versions.junit}"
+
+    object Mockito {
+        val core = "org.mockito:mockito-core:${Versions.mockito}"
+    }
+}

buildSrc/src/main/kotlin/GenerateGrammarExtension.kt

@@ -0,0 +1,3 @@
+import org.gradle.api.Project
+import org.gradle.kotlin.dsl.property
+

buildSrc/src/main/kotlin/antlr-grammar.gradle.kts

@@ -0,0 +1,28 @@
+import java.nio.file.Files
+
+apply<AntlrPlugin>()
+
+dependencies {
+    val antlr: Configuration by configurations
+    val implementation: Configuration by configurations
+
+    antlr(Deps.Antlr.antlr)
+    implementation(Deps.Antlr.runtime)
+}
+
+open class GenerateGrammarExtension(project: Project) {
+    var packageName: String = "hu.bme.mit.${project.name.replace("-",".")}.dsl.gen"
+}
+
+tasks {
+    val grammar = extensions.create<GenerateGrammarExtension>("grammar", project)
+
+    named("generateGrammarSource", AntlrTask::class) {
+        val packageName = grammar.packageName
+        val directoryName = packageName.replace(".", File.separator)
+        val pacakgeQualifiedOutputDirectory = outputDirectory.resolve(directoryName)
+        outputDirectory = pacakgeQualifiedOutputDirectory
+
+        arguments.addAll(listOf("-package", packageName, "-Werror", "-visitor"))
+    }
+}

buildSrc/src/main/kotlin/cli-tool.gradle.kts

@@ -0,0 +1,8 @@
+apply(plugin = "tool-common")
+
+dependencies {
+    val implementation: Configuration by configurations
+
+    implementation(Deps.jcommander)
+}
+

buildSrc/src/main/kotlin/java-common.gradle.kts

@@ -0,0 +1,30 @@
+apply<JavaPlugin>()
+apply<JacocoPlugin>()
+
+dependencies {
+    val implementation: Configuration by configurations
+    val testImplementation: Configuration by configurations
+
+    implementation(Deps.guava)
+    testImplementation(Deps.junit4)
+    testImplementation(Deps.Mockito.core)
+}
+
+tasks {
+    withType<JavaCompile>() {
+        sourceCompatibility = Versions.java
+        targetCompatibility = Versions.java
+    }
+
+    val libPath: String by rootProject.extra
+    val execPath: String by rootProject.extra
+
+    withType<Test>() {
+        environment["PATH"] = execPath
+        environment["LD_LIBRARY_PATH"] = libPath
+    }
+}
+
+extensions.configure<JacocoPluginExtension> {
+    toolVersion = Versions.jacoco
+}

buildSrc/src/main/kotlin/tool-common.gradle.kts

@@ -0,0 +1,17 @@
+import com.github.jengelman.gradle.plugins.shadow.ShadowPlugin
+
+apply<ApplicationPlugin>()
+apply<ShadowPlugin>()
+
+tasks {
+    val libPath: String by rootProject.extra
+    val execPath: String by rootProject.extra
+
+    fun JavaExec.setupEnvironment() {
+        environment["PATH"] = execPath
+        environment["LD_LIBRARY_PATH"] = libPath
+    }
+
+    named("run", JavaExec::class).configure { setupEnvironment() }
+    named("runShadow", JavaExec::class).configure { setupEnvironment() }
+}

gradle/shared-with-buildSrc/mirrors.gradle.kts

@@ -0,0 +1,6 @@
+repositories {
+    mavenCentral()
+    maven {
+        setUrl("https://dl.bintray.com/ftsrg/maven")
+    }
+}

settings.gradle.kts

@@ -0,0 +1,26 @@
+rootProject.name = "theta"
+
+include(
+        "analysis",
+        "cfa",
+        "cfa2dot",
+        "cfa-analysis",
+        "cfa-cli",
+        "cfa-metrics",
+        "common",
+        "core",
+        "solver",
+        "solver-z3",
+        "sts",
+        "sts-analysis",
+        "sts-cli",
+        "xta",
+        "xta-analysis",
+        "xta-cli"
+)
+
+for (project in rootProject.children) {
+    val projectName = project.name
+    project.projectDir = file("subprojects/$projectName")
+    project.name = "${rootProject.name}-$projectName"
+}

subprojects/analysis/build.gradle.kts

@@ -0,0 +1,10 @@
+plugins {
+    id("java-common")
+}
+
+dependencies {
+    compile(project(":theta-common"))
+    compile(project(":theta-core"))
+    compile(project(":theta-solver"))
+    testImplementation(project(":theta-solver-z3"))
+}

subprojects/cfa-analysis/build.gradle.kts

@@ -0,0 +1,11 @@
+plugins {
+    id("java-common")
+}
+
+dependencies {
+    compile(project(":theta-analysis"))
+    compile(project(":theta-cfa"))
+    compile(project(":theta-common"))
+    compile(project(":theta-core"))
+    testImplementation(project(":theta-solver-z3"))
+}

subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java → subprojects/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaTraceConcretizer.java

@@ -29,16 +29,17 @@
 import hu.bme.mit.theta.analysis.expr.refinement.ItpRefutation;
 import hu.bme.mit.theta.core.model.Valuation;
 import hu.bme.mit.theta.core.type.booltype.BoolExprs;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.*;
 
 public final class CfaTraceConcretizer {
 
 	private CfaTraceConcretizer() {
 	}
 
-	public static Trace<CfaState<ExplState>, CfaAction> concretize(final Trace<CfaState<?>, CfaAction> trace) {
+	public static Trace<CfaState<ExplState>, CfaAction> concretize(
+	        final Trace<CfaState<?>, CfaAction> trace, SolverFactory solverFactory) {
 		final ExprTraceChecker<ItpRefutation> checker = ExprTraceFwBinItpChecker.create(BoolExprs.True(),
-				BoolExprs.True(), Z3SolverFactory.getInstace().createItpSolver());
+				BoolExprs.True(), solverFactory.createItpSolver());
 		final ExprTraceStatus<ItpRefutation> status = checker.check(trace);
 		checkArgument(status.isFeasible(), "Infeasible trace.");
 		final Trace<Valuation, ? extends Action> valuations = status.asFeasible().getValuations();