build.gradle

plugins {
    id 'java-test-fixtures'
}

description = "Core functionality (terms, rules, prover, ...) for deductive verification of Java programs"

configurations { antlr4 }

dependencies {
    api project(':key.util')
    api project(':key.ncore')
    api project(':key.ncore.calculus')

    antlr4 "org.antlr:antlr4:4.13.2"
    api "org.antlr:antlr4-runtime:4.13.2"

    api project(':key.util')

    def JP_VERSION = "3.28.0-K13.5"
    api "org.key-project.proofjava:javaparser-core:$JP_VERSION"
    api "org.key-project.proofjava:javaparser-core-serialization:$JP_VERSION"
    api "org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION"

    testImplementation("com.google.truth:truth:1.4.5")
    testImplementation(project(":key.core"))

    // https://mvnrepository.com/artifact/com.fasterxml.jackson.dataformat/jackson-dataformat-yaml
    testImplementation 'com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.4'

    // test fixtures
    testFixturesApi(testFixtures(project(":key.util")))
}

// The target directory for JavaCC (parser generation)
//def javaCCOutputDir = layout.buildDirectory.dir("generated-src/javacc").getOrNull()
//def javaCCOutputDirMain = file("$javaCCOutputDir/main")

sourceSets.main.java.srcDirs("$projectDir/build/generated-src/antlr4/main/")


tasks.register('generateSMTListings') {
    def pack = "de/uka/ilkd/key/smt/newsmt2"
    def resourcesDir = "${project.projectDir}/src/main/resources"
    def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main"
    // ${project.buildDir}
    inputs.files fileTree("$resourcesDir/$pack", {
        exclude "$resourcesDir/$pack/DefinedSymbolsHandler.preamble.xml"
    })
    outputs.files file("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml")
    doLast {
        new File("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml").withWriter { list ->
            list.writeLine '<?xml version="1.0" encoding="UTF-8" standalone="no"?>'
            list.writeLine '<!DOCTYPE properties SYSTEM "http://java.sun.com/dtd/properties.dtd">'
            list.writeLine '<properties>'
            new File("$resourcesDir/$pack").eachFile {
                if (it.name.endsWith('.DefinedSymbolsHandler.preamble.xml')) {
                    // println it.name
                    it.eachLine { list.writeLine it }
                }
            }
            list.writeLine '</properties>'
        }
    }
}

tasks.register('generateSolverPropsList') {
    def pack = "de/uka/ilkd/key/smt/solvertypes"
    def resourcesDir = "${project.projectDir}/src/main/resources"
    def outputDir = resourcesDir // in the future that should be "${project.buildDir}/resources/main"
    // ${project.buildDir}
    inputs.files fileTree("$outputDir/$pack/", {
        exclude "./solvers.txt"
    })
    outputs.files file("$outputDir/$pack/solvers.txt")
    doLast {
        def list = []
        def dir = new File("$outputDir/$pack/")
        dir.eachFileRecurse({ file ->
            if (file.name.endsWith(".props")) {
                list.add(file.name)
            }
        })
        list.sort()
        String files = ''
        for (String propsFile : list) {
            files += propsFile + System.lineSeparator()
        }
        new File("$outputDir/$pack/solvers.txt").withWriter { listSolvers ->
            listSolvers.write files
        }
    }
}

classes.dependsOn << generateSMTListings
classes.dependsOn << generateSolverPropsList


tasks.withType(Test) {
    enableAssertions = true
}


tasks.register('testProveRules', Test) {
    description = 'Proves KeY taclet rules tagged as lemma'
    group = "verification"
    filter { includeTestsMatching "ProveRulesTest" }
    //useJUnitPlatform() {includeTags "testProveRules"    }
}

tasks.register('testRunAllFunProofs', Test) {
    description = 'Prove/reload all keyfiles tagged for regression testing'
    group = "verification"
    filter {
        includeTestsMatching "RunAllProofsFunctional"
    }
}

tasks.register('testProveSMTLemmas', Test) {
    description = 'Prove (or load proofs for) lemmas used in the SMT translation'
    group = "verification"
    filter {
        includeTestsMatching "ProveSMTLemmasTest"
    }
}

// Run the tests for the new smt translation in strict mode
// where "unknown" is less accepted
tasks.register('testStrictSMT', Test) {
    description = 'Run the tests for the new smt translation in strict mode'
    group = 'verification'
    systemProperty("key.newsmt2.stricttests", "true")
    filter {
        includeTestsMatching "MasterHandlerTest"
    }
}

//Generation of the three version files within the resources by executing `git'.
tasks.register('generateVersionFiles') {
    def outputFolder = file("build/resources/main/de/uka/ilkd/key/util")
    def sha1 = new File(outputFolder, "sha1")
    def branch = new File(outputFolder, "branch")
    def versionf = new File(outputFolder, "version")

    inputs.files "$project.rootDir/.git/HEAD"
    outputs.files sha1, branch, versionf

    def gitRevision = gitRevParse('HEAD')
    def gitBranch = gitRevParse('--abbrev-ref HEAD')

    doLast {
        sha1.text = gitRevision
        branch.text = gitBranch
        versionf.text = rootProject.version
    }
}

// Helper function that calls "git rev-parse" to
// find names/SHAs for commits
static def gitRevParse(String args) {
    try {
        return "git rev-parse $args".execute().text.trim()
    } catch (Exception e) {
        return ""
    }
}

// @AW: Say something here. From POV this explain by itself.
processResources.dependsOn generateVersionFiles, generateSolverPropsList, generateSMTListings

def antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser"
tasks.register('runAntlr4Key', JavaExec) {
    //see incremental task api, prevents rerun if nothing has changed.
    inputs.files "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4"
    outputs.dir antlr4OutputKey
    classpath = configurations.antlr4
    mainClass.set("org.antlr.v4.Tool")
    args = ["-visitor",
            "-Xexact-output-dir", "-o", antlr4OutputKey,
            "-package", "de.uka.ilkd.key.nparser",
            "src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4"]
    doFirst {
        file(antlr4OutputKey).mkdirs()
        println("create $antlr4OutputKey")
    }
}
compileJava.dependsOn runAntlr4Key

tasks.register('debugKeyLexer', JavaExec) {
    mainClass.set("de.uka.ilkd.key.nparser.DebugKeyLexer")
    classpath = sourceSets.main.runtimeClasspath
    standardInput = System.in
}

// @AW: Say something here. From POV this explain by itself.
processResources.dependsOn generateVersionFiles

def antlr4OutputJml = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/speclang/njml"
tasks.register('runAntlr4Jml', JavaExec) {
    //see incremental task api, prevents rerun if nothing has changed.
    inputs.files "src/main/antlr4/JmlLexer.g4", "src/main/antlr4/JmlParser.g4"
    outputs.dir antlr4OutputJml
    classpath = configurations.antlr4
    mainClass.set("org.antlr.v4.Tool")
    args = ["-visitor",
            "-Xexact-output-dir", "-o", antlr4OutputJml,
            "-package", "de.uka.ilkd.key.speclang.njml",
            "src/main/antlr4/JmlLexer.g4", "src/main/antlr4/JmlParser.g4"]
    doFirst {
        file(antlr4OutputJml).mkdirs()
        println("create $antlr4OutputJml")
    }
}
compileJava.dependsOn runAntlr4Jml

tasks.register('debugJmlLexer', JavaExec) {
    mainClass.set("de.uka.ilkd.key.speclang.njml.DebugJmlLexer")
    classpath = sourceSets.main.runtimeClasspath
    standardInput = System.in
}

tasks.register('ptest', Test) { group = "verification" }

def rapDir = layout.buildDirectory.dir("generated-src/rap/").getOrNull()

tasks.register('generateRAPUnitTests', JavaExec) {
    classpath = sourceSets.test.runtimeClasspath
    mainClass.set("de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests")
    args(rapDir)
}

tasks.register("testRAP", Test) {
    description = "Testng the generated RAP unit tests"
    group = "verification"
    dependsOn('generateRAPUnitTests', 'testClasses')

    forkEvery = 1
    maxParallelForks = 2
    useJUnitPlatform()
    it.filter {
        it.includeTestsMatching "de.uka.ilkd.key.proof.runallproofs.gen.*"
    }
    // set heap size for the test JVM(s)
    minHeapSize = "1g"
    maxHeapSize = "3g"

    // set JVM arguments for the test JVM(s)
    //jvmArgs('-XX:MaxPermSize=1g')
    failFast=false
    testLogging.showStandardStreams = false
    testLogging.displayGranularity = 1
}

sourceSets.test.java.srcDirs(rapDir)

sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key)