diff --git a/.github/old_workflows/deletecache.yml b/.github/old_workflows/deletecache.yml deleted file mode 100644 index 8376a396fc9..00000000000 --- a/.github/old_workflows/deletecache.yml +++ /dev/null @@ -1,34 +0,0 @@ -name: cleanup caches by a branch -on: - pull_request: - types: - - closed - workflow_dispatch: - -jobs: - cleanup: - runs-on: ubuntu-latest - steps: - - name: Check out code - uses: actions/checkout@v3 - - - name: Cleanup - run: | - gh extension install actions/gh-actions-cache - - REPO=$ - BRANCH=$ - - echo "Fetching list of cache key" - cacheKeysForPR=$(gh actions-cache list -R $REPO -B $BRANCH | cut -f 1 ) - - ## Setting this to not fail the workflow while deleting cache keys. - set +e - echo "Deleting caches..." - for cacheKey in $cacheKeysForPR - do - gh actions-cache delete $cacheKey -R $REPO -B $BRANCH --confirm - done - echo "Done" - env: - GH_TOKEN: $ diff --git a/.github/old_workflows/labeler.yml b/.github/old_workflows/labeler.yml deleted file mode 100644 index 41134d5a18f..00000000000 --- a/.github/old_workflows/labeler.yml +++ /dev/null @@ -1,14 +0,0 @@ -name: "Pull Request Labeler" -on: [pull_request, pull_request_target] - -jobs: - triage: - permissions: - contents: read - pull-requests: write - runs-on: ubuntu-latest - steps: - - uses: actions/labeler@v4 - with: - sync-labels: true - repo-token: "${{ secrets.GITHUB_TOKEN }}" diff --git a/.github/old_workflows/mega-lint.yml b/.github/old_workflows/mega-lint.yml deleted file mode 100644 index 93a3b2f001d..00000000000 --- a/.github/old_workflows/mega-lint.yml +++ /dev/null @@ -1,80 +0,0 @@ -name: MegaLinter - -on: - # Trigger mega-linter at every push. Action will also be visible from Pull Requests to main - push: # Comment this line to trigger action only on pull-requests (not recommended if you don't pay for GH Actions) - pull_request: - branches: [master, main] - -env: # Comment env block if you do not want to apply fixes - # Apply linter fixes configuration - APPLY_FIXES: all # When active, APPLY_FIXES must also be defined as environment variable (in github/workflows/mega-linter.yml or other CI tool) - APPLY_FIXES_EVENT: pull_request # Decide which event triggers application of fixes in a commit or a PR (pull_request, push, all) - APPLY_FIXES_MODE: commit # If APPLY_FIXES is used, defines if the fixes are directly committed (commit) or posted in a PR (pull_request) - -concurrency: - group: ${{ github.ref }}-${{ github.workflow }} - cancel-in-progress: true - -jobs: - build: - name: MegaLinter - runs-on: ubuntu-latest - steps: - # Git Checkout - - name: Checkout Code - uses: actions/checkout@v3 - with: - token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} - fetch-depth: 0 # If you use VALIDATE_ALL_CODEBASE = true, you can remove this line to improve performances - - # MegaLinter - - name: MegaLinter - id: ml - # You can override MegaLinter flavor used to have faster performances - # More info at https://megalinter.github.io/flavors/ - uses: oxsecurity/megalinter@v6 - env: - # All available variables are described in documentation - # https://megalinter.github.io/configuration/ - VALIDATE_ALL_CODEBASE: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }} # Validates all source when push on main, else just the git diff with main. Override with true if you always want to lint all sources - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - # ADD YOUR CUSTOM ENV VARIABLES HERE OR DEFINE THEM IN A FILE .mega-linter.yml AT THE ROOT OF YOUR REPOSITORY - # DISABLE: COPYPASTE,SPELL # Uncomment to disable copy-paste and spell checks - - # Upload MegaLinter artifacts - - name: Archive production artifacts - if: ${{ success() }} || ${{ failure() }} - uses: actions/upload-artifact@v3 - with: - name: MegaLinter reports - path: | - megalinter-reports - mega-linter.log - - # Create pull request if applicable (for now works only on PR from same repository, not from forks) - - name: Create Pull Request with applied fixes - id: cpr - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - uses: peter-evans/create-pull-request@v4 - with: - token: ${{ secrets.PAT || secrets.GITHUB_TOKEN }} - commit-message: "[MegaLinter] Apply linters automatic fixes" - title: "[MegaLinter] Apply linters automatic fixes" - labels: bot - - name: Create PR output - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'pull_request' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - run: | - echo "Pull Request Number - ${{ steps.cpr.outputs.pull-request-number }}" - echo "Pull Request URL - ${{ steps.cpr.outputs.pull-request-url }}" - - # Push new commit if applicable (for now works only on PR from same repository, not from forks) - - name: Prepare commit - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - run: sudo chown -Rc $UID .git/ - - name: Commit and push applied linter fixes - if: steps.ml.outputs.has_updated_sources == 1 && (env.APPLY_FIXES_EVENT == 'all' || env.APPLY_FIXES_EVENT == github.event_name) && env.APPLY_FIXES_MODE == 'commit' && github.ref != 'refs/heads/main' && (github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository) && !contains(github.event.head_commit.message, 'skip fix') - uses: stefanzweifel/git-auto-commit-action@v4 - with: - branch: ${{ github.event.pull_request.head.ref || github.head_ref || github.ref }} - commit_message: "[MegaLinter] Apply linters fixes" diff --git a/.github/old_workflows/test-report.yml b/.github/old_workflows/test-report.yml deleted file mode 100644 index 4fc333c65f9..00000000000 --- a/.github/old_workflows/test-report.yml +++ /dev/null @@ -1,16 +0,0 @@ -name: 'Test Report' -on: - workflow_run: - workflows: ['CI'] # runs after CI workflow - types: - - completed -jobs: - report: - runs-on: ubuntu-latest - steps: - - uses: dorny/test-reporter@v1 - with: - artifact: test-results # artifact name - name: JUnit Tests # Name of the check run which will be created - path: '*.xml' # Path to test results (inside artifact .zip) - reporter: java-junit # Format of test results diff --git a/.github/old_workflows/update_symbex_oracles.yml b/.github/old_workflows/update_symbex_oracles.yml deleted file mode 100644 index 405127c3c27..00000000000 --- a/.github/old_workflows/update_symbex_oracles.yml +++ /dev/null @@ -1,44 +0,0 @@ -name: Update Symbex Oracles - -on: - workflow_dispatch: - push: - branches: [ "main" ] - -permissions: - contents: write - issues: write - pull-requests: write - id-token: write - -jobs: - optional-tests: - runs-on: ubuntu-latest - continue-on-error: true - steps: - - uses: actions/checkout@v4 - - name: Set up JDK 21 - uses: actions/setup-java@v4 - with: - java-version: '21' - distribution: 'corretto' - cache: 'gradle' - - - name: Build with Gradle - uses: gradle/gradle-build-action@v3 - with: - arguments: --continue -D UPDATE_TEST_ORACLE=true -D ORACLE_DIRECTORY=key.core.symbolic_execution/src/test/resources/testcase :key.core.symbolic_execution:test - - - name: Make new branch - uses: EndBug/add-and-commit@v9 - with: - add: 'key.core.symbolic_execution/src/test/resources/testcase' - author_name: Kiki - author_email: support@kit.edu - default_author: github_actions - message: 'Auto-Commit: update of the symbex oracle' - pull: '--rebase --autostash' - new_branch: update_oracle_${GITHUB_RUN_ID}_${GITHUB_RUN_NUMBER} - - - name: Create Pull-Request - run: gh pr create --title "Update of the symbex oracle" --body "This is an automated Pull Request" -a "unp1" -B "main" -l "automatic" -H update_oracle_${GITHUB_RUN_ID}_${GITHUB_RUN_NUMBER} diff --git a/.github/qodana.starter.full.xml b/.github/qodana.starter.full.xml deleted file mode 100644 index 1b7e1c7dc30..00000000000 --- a/.github/qodana.starter.full.xml +++ /dev/null @@ -1,7016 +0,0 @@ - - - - \ No newline at end of file diff --git a/build.gradle b/build.gradle deleted file mode 100644 index 866bca5019a..00000000000 --- a/build.gradle +++ /dev/null @@ -1,455 +0,0 @@ -plugins { - //Support for IntelliJ IDEA - //https://docs.gradle.org/current/userguide/idea_plugin.html - id("idea") - - //Support for Eclipse - //https://docs.gradle.org/current/userguide/eclipse_plugin.html - id("eclipse") //support for Eclipse - - // Code formatting - id "com.diffplug.spotless" version "8.3.0" - - // EISOP Checker Framework - id "org.checkerframework" version "0.6.61" - - id("org.sonarqube") version "7.2.3.7755" - - // Plugin for publishing via the new Nexus API - id "io.github.gradle-nexus.publish-plugin" version "2.0.0" -} - - -// Configure this project for use inside IntelliJ: -idea { - module { - downloadJavadoc = false - downloadSources = true - } -} - -static def getDate() { - return new Date().format('yyyyMMdd') -} - -// The $BUILD_NUMBER is an environment variable set by Jenkins. -def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMBER}" - -group = "org.key-project" -version = "2.13.0$build" - -subprojects { - apply plugin: "java" - apply plugin: "java-library" - apply plugin: "maven-publish" - apply plugin: "signing" // GPG signing of artifacts, required by maven central - apply plugin: "idea" - apply plugin: "eclipse" - - apply plugin: "com.diffplug.spotless" - apply plugin: "org.checkerframework" - - group = rootProject.group - version = rootProject.version - - java { - sourceCompatibility = 21 - targetCompatibility = 21 - } - - repositories { - mavenCentral() - } - - dependencies { - implementation("org.slf4j:slf4j-api:2.0.17") - implementation("org.slf4j:slf4j-api:2.0.17") - testImplementation("ch.qos.logback:logback-classic:1.5.32") - - - compileOnly("org.jspecify:jspecify:1.0.0") - testCompileOnly("org.jspecify:jspecify:1.0.0") - def eisop_version = "3.49.3-eisop1" - compileOnly "io.github.eisop:checker-qual:$eisop_version" - compileOnly "io.github.eisop:checker-util:$eisop_version" - testCompileOnly "io.github.eisop:checker-qual:$eisop_version" - checkerFramework "io.github.eisop:checker-qual:$eisop_version" - checkerFramework "io.github.eisop:checker:$eisop_version" - - testImplementation("ch.qos.logback:logback-classic:1.5.32") - testImplementation("org.assertj:assertj-core:3.27.7") - testImplementation("ch.qos.logback:logback-classic:1.5.32") - - testImplementation(platform("org.junit:junit-bom:5.14.3")) - testImplementation ("org.junit.jupiter:junit-jupiter-api") - testImplementation ("org.junit.jupiter:junit-jupiter-params") - testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine") - testRuntimeOnly ("org.junit.platform:junit-platform-launcher") - testImplementation ("org.assertj:assertj-core:3.27.7") - testImplementation project(':key.util') - - // test fixtures - testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.1") - testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.1") - - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine' - } - - tasks.withType(JavaCompile).configureEach { - // Setting UTF-8 as the java source encoding. - options.encoding = "UTF-8" - // Setting the release to Java 21 - options.release = 21 - } - - tasks.withType(Javadoc).configureEach { - failOnError = false - options.addBooleanOption 'Xdoclint:none', true - //options.verbose() - options.encoding = 'UTF-8' - options.addBooleanOption('html5', true) - } - - tasks.withType(Test).configureEach {//Configure all tests - def examplesDir = rootProject.layout.projectDirectory.dir("key.ui/examples").getAsFile() - def runAllProofsReportDir = layout.buildDirectory.dir("report/runallproves/").get().getAsFile() - systemProperty "test-resources", "src/test/resources" - systemProperty "testcases", "src/test/resources/testcase" - systemProperty "TACLET_PROOFS", "tacletProofs" - systemProperty "EXAMPLES_DIR", file("$rootProject/key.ui/examples") - systemProperty "RUNALLPROOFS_DIR", layout.buildDirectory.dir("report/runallproves").get().toString() - - systemProperty "key.disregardSettings", "true" - maxHeapSize = "4g" - - forkEvery = 0 //default - maxParallelForks = 1 // weigl: test on master - - useJUnitPlatform { - includeEngines 'junit-jupiter' - } - - // these seems to be missing starting with Gradle 9 - testClassesDirs = sourceSets.test.output.classesDirs - classpath = sourceSets.test.runtimeClasspath - - // Fail on empty test suites - afterSuite { suite, result -> - assert result.testCount > 0, "There are no executed test. This is unexpected and should be investigated!" - } - } - - - test { - // Before we switched to JUnit 5, we used JUnit 4 with a customized discovery of test class. - // This discovery called AutoSuite and searched in the compiled classes. AutoSuite was - // necessary due to bugs caused in some execution order. - // AutoSuites made the test order deterministic. A last known commit to find AutoSuite (for the case), - // is 980294d04008f6b3798986bce218bac2753b4783. - - useJUnitPlatform { - excludeTags "owntest", "interactive", "performance" - } - - afterTest { desc, result -> logger.error "${result.resultType}: ${desc.className}#${desc.name}" } - beforeTest { desc -> logger.error "> ${desc.className}#${desc.name}" } - - testLogging { - outputs.upToDateWhen { false } - showStandardStreams = true - } - } - - tasks.register('testFast', Test) { - group = "verification" - useJUnitPlatform { - excludeTags "slow", "performance", "interactive" - } - - testLogging { - // set options for log level LIFECYCLE - events = ["failed"] - exceptionFormat = "short" - - // set options for log level DEBUG - debug { - events "started", "skipped", "failed" - exceptionFormat = "full" - } - - // remove standard output/error logging from --info builds - // by assigning only 'failed' and 'skipped' events - info.events = ["failed", "skipped"] - } - } - - // The following two tasks can be used to execute main methods from the project - // The main class is set via "gradle -DmainClass=... execute --args ..." - // see https://stackoverflow.com/questions/21358466/gradle-to-execute-java-class-without-modifying-build-gradle - tasks.register('execute', JavaExec) { - description = 'Execute main method from the project. Set main class via "gradle -DmainClass=... execute --args ..."' - group = "application" - mainClass.set(System.getProperty('mainClass')) - classpath = sourceSets.main.runtimeClasspath - } - - tasks.register('executeInTests', JavaExec) { - description = 'Execute main method from the project (tests loaded). Set main class via "gradle -DmainClass=... execute --args ..."' - group = "application" - mainClass.set(System.getProperty('mainClass')) - classpath = sourceSets.test.runtimeClasspath - } - - tasks.register('sourcesJar', Jar) { - description = 'Create a jar file with the sources from this project' - from sourceSets.main.allJava - archiveClassifier = 'sources' - } - - tasks.register('javadocJar', Jar) { - description = 'Create a jar file with the javadocs from this project' - from javadoc - archiveClassifier = 'javadoc' - } - - eclipse { //configures the generated .project and .classpath files. - classpath { - file { - whenMerged { // This adds the exclude entry for every resource and antlr folder. - //As eclipse is so stupid, that it does not distuinguish between resource and java folder correctly. - entries.findAll { it.path.endsWith('src/test/antlr') }.each { it.excludes = ["**/*.java"] } - entries.findAll { it.path.endsWith('/resources') }.each { it.excludes = ["**/*.java"] } - } - } - } - } - - spotless { - // see https://github.com/diffplug/spotless/tree/main/plugin-gradle - - // optional: limit format enforcement to just the files changed by this feature branch - // ratchetFrom 'origin/master' - - format('Key') { - // define the files to apply `misc` to - //target '*.gradle', '*.md', '.gitignore' - target 'src/main/resources/**/*.key' - trimTrailingWhitespace() - //indentWithSpaces(4) // this does not really work - endWithNewline() - // TODO: license headers are problematic at the moment, - // see https://git.key-project.org/key/key/-/wikis/KaKeY%202022-09-30 - //licenseHeaderFile("$rootDir/gradle/header", '\\s*\\\\\\w+') - } - - antlr4 { - target 'src/*/antlr4/**/*.g4' // default value, you can change if you want - //licenseHeaderFile "$rootDir/gradle/header" - } - - java { - //target("*.java") - // don't need to set target, it is inferred from java - - // We ignore the build folder to avoid double checks and checks of generated code. - targetExclude 'build/**' - - // allows us to use spotless:off / spotless:on to keep pre-formatted sections - // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on" - // that must be used instead. - toggleOffOn() - - removeUnusedImports() - - /* When new options are added in new versions of the Eclipse formatter, the easiest way is to export the new - * style file from the Eclipse GUI and then use the CodeStyleMerger tool in - * "$rootDir/scripts/tools/checkstyle/CodeStyleMerger.java" to merge the old and the new style files, - * i.e. "java CodeStyleMerger.java keyCodeStyle.xml". The tool adds all - * entries with keys that were not present in the old file and optionally overwrites the old entries. The - * file is output with ordered keys, such that the file can easily be diffed using git. - */ - eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") - trimTrailingWhitespace() // not sure how to set this in the xml file ... - //googleJavaFormat().aosp().reflowLongStrings() - - // note: you can use an empty string for all the imports you didn't specify explicitly, - // '|' to join group without blank line, and '\\#` prefix for static imports - importOrder('java|javax', 'de.uka', 'org.key_project', '', '\\#') - - // specific delimiter: normally just 'package', but spotless crashes for files in default package - // (see https://github.com/diffplug/spotless/issues/30), therefore 'import' is needed. '//' is for files - // with completely commented out code (which would probably better just be removed in future). - if (project.name == 'recoder') { - licenseHeaderFile("$rootDir/gradle/header-recoder", '(package|import|//)') - } else { - licenseHeaderFile("$rootDir/gradle/header", '(package|import|//)') - } - } - } - - afterEvaluate { // required so project.description is non-null as set by sub build.gradle - publishing { - publications { - mavenJava(MavenPublication) { - from components.java - artifact sourcesJar - artifact javadocJar - pom { - name = projects.name - description = project.description - url = 'https://key-project.org/' - - licenses { - license { - name = "GNU General Public License (GPL), Version 2" - url = "https://www.gnu.org/licenses/old-licenses/gpl-2.0.html" - } - } - - developers { - developer { - id = 'key' - name = 'KeY Developers' - email = 'support@key-project.org' - url = "https://www.key-project.org/about/people/" - } - } - scm { - connection = 'scm:git:git://github.com/keyproject/key.git' - developerConnection = 'scm:git:git://github.com/keyproject/key.git' - url = 'https://github.com/keyproject/key/' - } - } - } - } - repositories { - maven { - name = "LOCAL" - url= uri("$rootDir/local") - } - - maven { // deployment to git.key-project.org/key-public/key - name = "KEYLAB" - url = uri("https://git.key-project.org/api/v4/projects/35/packages/maven") - credentials(HttpHeaderCredentials) { - def userToken = envOrPropertyValue("GITLAB_USER_TOKEN") - def deployToken = envOrPropertyValue("GITLAB_DEPLOY_TOKEN") - def ciToken = envOrPropertyValue("GITLAB_CIJOB_TOKEN") - - if (userToken != "") { - name = 'Private-Token' - value = userToken - } else if(deployToken != "") { - name = 'Deploy-Token' - value = deployToken - } else { - name = 'Job-Token' - value = ciToken - } - } - authentication { - header(HttpHeaderAuthentication) - } - } - } - } - - signing { - useGpgCmd() // works better than the Java implementation, which requires PGP keyrings. - sign publishing.publications.mavenJava - } - } -} - - -nexusPublishing { - repositories { - central { - nexusUrl = uri("https://ossrh-staging-api.central.sonatype.com/service/local/") - snapshotRepositoryUrl = uri("https://central.sonatype.com/repository/maven-snapshots/") - - stagingProfileId.set("org.key-project") - - /** - * To be able to publish things on Maven Central, you need two things: - * - * (1) a JIRA account with permission on group-id `org.key-project` - * (2) a keyserver-published GPG (w/o sub-keys) - * - * Your `$HOME/.gradle/gradle.properties` should like this: - * ``` - * signing.keyId=YourKeyId - * signing.password=YourPublicKeyPassword - * ossrhUsername=your-jira-id - * ossrhPassword=your-jira-password - * ``` - * - * You can test signing with `gradle sign`, and publish with `gradle publish`. - * https://central.sonatype.org/publish/publish-guide/ - */ - username = envOrPropertyValue("ossrhUsername") - password = envOrPropertyValue("ossrhPassword") - } - } -} - -tasks.register('start'){ - description = "Use :key.ui:run instead" - doFirst { - println "Use :key.ui:run instead" - } -} - -// Generation of a JavaDoc across sub projects. -tasks.register('alldoc', Javadoc){ - group = "documentation" - description = "Generate a JavaDoc across sub projects" - def projects = subprojects - //key.ui javadoc is broken - source projects.collect { it.sourceSets.main.allJava } - classpath = files(projects.collect { it.sourceSets.main.compileClasspath }) - destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile() - - if (JavaVersion.current().isJava9Compatible()) { - options.addBooleanOption('html5', true) - } - - configure(options) { - //showFromPrivate() - encoding = 'UTF-8' - addBooleanOption 'Xdoclint:none', true - // overview = new File( projectDir, 'src/javadoc/package.html' ) - //stylesheetFile = new File( projectDir, 'src/javadoc/stylesheet.css' ) - windowTitle = 'KeY API Documentation' - docTitle = "KeY JavaDoc ($project.version) -- ${getDate()}" - bottom = "Copyright © 2003-2026 The KeY-Project." - use = true - links += "https://docs.oracle.com/en/java/javase/21/docs/api/" - links += "https://www.antlr.org/api/Java/" - } -} - -// Creates a jar file with the javadoc over all sub projects. -tasks.register('alldocJar', Zip){ - dependsOn alldoc - description = 'Create a jar file with the javadoc over all sub projects' - from alldoc - archiveFileName = "key-api-doc-${project.version}.zip" - destinationDirectory = layout.buildDirectory.dir("distribution").getOrNull() -} - -//conditionally enable jacoco coverage when `-DjacocoEnabled=true` is given on CLI. -def jacocoEnabled = System.properties.getProperty("jacocoEnabled") ?: "false" -if (jacocoEnabled.toBoolean()) { - project.logger.lifecycle("Jacoco enabled. Test performance will be slower.") - apply from: rootProject.file("scripts/jacocokey.gradle") -} - - -def envOrPropertyValue(String key) { - if(key in System.getenv()) { - return System.getenv(key) - }else{ - return project.properties.getOrDefault(key, "") - } -} \ No newline at end of file diff --git a/build.gradle.kts b/build.gradle.kts new file mode 100644 index 00000000000..53dabcff5c8 --- /dev/null +++ b/build.gradle.kts @@ -0,0 +1,71 @@ +import java.util.Date + +plugins { + //Support for IntelliJ IDEA + //https://docs.gradle.org/current/userguide/idea_plugin.html + id("idea") + + //Support for Eclipse + //https://docs.gradle.org/current/userguide/eclipse_plugin.html + id("eclipse") //support for Eclipse + + // Gives `gradle dependencyUpdate` to show which dependency has a newer version + // id "com.github.ben-manes.versions" version "0.39.0" + + // Code formatting + id("com.diffplug.spotless") + + id("com.github.ben-manes.versions") +} + +// Configure this project for use inside IntelliJ: +idea { + module { + isDownloadJavadoc = false + isDownloadSources = true + } +} + +// The $BUILD_NUMBER is an environment variable set by Jenkins. +val build = System.getenv("BUILD_NUMBER")?.let { "-$it" } ?: "-dev" + +group = "org.key-project" +version = "2.12.4$build" + +// Generation of a JavaDoc across sub projects. +val alldoc = tasks.register("alldoc") { + group = "documentation" + description = "Generate a JavaDoc across sub projects" + + subprojects.forEach { subproject -> + if (subproject.plugins.hasPlugin("java")) { + val sourceSets = subproject.extensions.getByName("sourceSets") as SourceSetContainer + val main = sourceSets.getByName("main") + source(main.allJava) + classpath += main.compileClasspath + } + } + destinationDir = layout.buildDirectory.dir("docs/javadoc").get().asFile + + with(options as StandardJavadocDocletOptions) { + //showFromPrivate() + encoding = "UTF-8" + addBooleanOption("Xdoclint:none", true) + // overview = new File( projectDir, 'src/javadoc/package.html' ) + //stylesheetFile = new File( projectDir, 'src/javadoc/stylesheet.css' ) + windowTitle = "KeY API Documentation" + docTitle = "KeY JavaDoc ($project.version) -- ${Date()}" + bottom = "Copyright © 2003-2023 The KeY-Project." + isUse=true + links = listOf("https://docs.oracle.com/en/java/javase/21/docs/api/", "https://www.antlr.org/api/Java/") + } +} + +// Creates a jar file with the javadoc over all sub projects. +tasks.register("alldocJar") { + dependsOn(alldoc.get()) + description = "Create a jar file with the javadoc over all sub projects" + from(alldoc.get()) + archiveFileName = "key-api-doc-${project.version}.zip" + destinationDirectory = layout.buildDirectory.dir("distribution").get() +} diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts new file mode 100644 index 00000000000..73d2077c30b --- /dev/null +++ b/buildSrc/build.gradle.kts @@ -0,0 +1,24 @@ +import org.gradle.kotlin.dsl.plugins + +plugins { + `kotlin-dsl` + `kotlin-dsl-precompiled-script-plugins` +} + +repositories { + mavenCentral() + gradlePluginPortal() +} + +kotlin { + jvmToolchain(21) +} + +dependencies { + implementation("com.diffplug.spotless:com.diffplug.spotless.gradle.plugin:7.2.1") + implementation("org.checkerframework:org.checkerframework.gradle.plugin:0.6.56") + implementation("com.gradleup.shadow:com.gradleup.shadow.gradle.plugin:9.0.2") + implementation("com.github.ben-manes:gradle-versions-plugin:0.38.0") + + implementation(libs.kotlinGradlePlugin) +} \ No newline at end of file diff --git a/buildSrc/settings.gradle.kts b/buildSrc/settings.gradle.kts new file mode 100644 index 00000000000..54c2b363d87 --- /dev/null +++ b/buildSrc/settings.gradle.kts @@ -0,0 +1,18 @@ +dependencyResolutionManagement { + + // Use Maven Central and the Gradle Plugin Portal for resolving dependencies in the shared build logic (`buildSrc`) project. + @Suppress("UnstableApiUsage") + repositories { + mavenCentral() + gradlePluginPortal() + } + + // Reuse the version catalog from the main build. + versionCatalogs { + create("libs") { + from(files("../gradle/libs.versions.toml")) + } + } +} + +rootProject.name = "buildSrc" \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/java-convention.gradle.kts b/buildSrc/src/main/kotlin/java-convention.gradle.kts new file mode 100644 index 00000000000..bd7b19b0a28 --- /dev/null +++ b/buildSrc/src/main/kotlin/java-convention.gradle.kts @@ -0,0 +1,375 @@ +import org.gradle.api.tasks.testing.logging.TestExceptionFormat +import org.gradle.api.tasks.testing.logging.TestLogEvent +import org.gradle.plugins.ide.eclipse.model.Classpath +import org.gradle.plugins.ide.eclipse.model.SourceFolder + +plugins { + java + `java-library` + `maven-publish` + signing // GPG signing of artifacts, required by maven central + idea + eclipse + + id("com.diffplug.spotless") + id("org.checkerframework") +} + +//conditionally enable jacoco coverage when `-DjacocoEnabled=true` is given on CLI. +val jacocoEnabled = System.getProperty("jacocoEnabled", "false").toBoolean() +if (jacocoEnabled) { + project.logger.lifecycle("Jacoco enabled. Test performance will be slower.") +} + +java { + toolchain { + languageVersion = JavaLanguageVersion.of(21) + } + + withJavadocJar() + withSourcesJar() +} + +repositories { + mavenCentral() + maven { + url = uri("https://git.key-project.org/api/v4/projects/35/packages/maven") + } +} + +internal val Project.libs: VersionCatalog + get() = project.extensions.getByType().named("libs") + +dependencies { + implementation(libs.findLibrary("slf4j").get()) + api(libs.findLibrary("jspecify").get()) + + val checkerQual = libs.findLibrary("eisopCheckerQual").get() + val eisopUtil = libs.findLibrary("eisopUtil").get() + + compileOnly(checkerQual) + compileOnly(eisopUtil) + checkerFramework(checkerQual) + checkerFramework(eisopUtil) + checkerFramework(libs.findLibrary("eisopChecker").get()) + + // Testing + testCompileOnly(checkerQual) + + testImplementation(platform(libs.findLibrary("junit-bom").get())) + testImplementation(libs.findBundle("testing").get()) + + testRuntimeOnly(libs.findLibrary("junit.engine").get()) + testRuntimeOnly(libs.findLibrary("junit.platform").get()) + + testImplementation(project(":key.util")) +} + +tasks.withType().configureEach { + // Setting UTF-8 as the java source encoding. + options.encoding = "UTF-8" +} + +tasks.withType { + isFailOnError = false + val o = options as CoreJavadocOptions + o.addBooleanOption("Xdoclint:none", true) + //options.verbose() + o.encoding = "UTF-8" + o.addBooleanOption("html5", true) +} + +tasks.withType().configureEach { + val examplesDir = rootProject.layout.projectDirectory.dir("key.ui/examples").asFile + val runAllProofsReportDir = layout.buildDirectory.dir("report/runallproves/").get().asFile + + systemProperty("test-resources", "src/test/resources") + systemProperty("testcases", "src/test/resources/testcase") + systemProperty("TACLET_PROOFS", "tacletProofs") + systemProperty("EXAMPLES_DIR", "$examplesDir") + systemProperty("RUNALLPROOFS_DIR", "$runAllProofsReportDir") + systemProperty("key.disregardSettings", "true") + + maxHeapSize = "4g" + + forkEvery = 0 //default + maxParallelForks = 1 // weigl: test on master + + useJUnitPlatform { + includeEngines("junit-jupiter") + } + + // these seems to be missing starting with Gradle 9 + testClassesDirs = sourceSets["test"].output.classesDirs + classpath = sourceSets["test"].runtimeClasspath + + // Fail on empty test suites + addTestListener(object : TestListener { + override fun beforeSuite(suite: TestDescriptor) {} + override fun beforeTest(testDescriptor: TestDescriptor) {} + override fun afterTest(testDescriptor: TestDescriptor, result: TestResult) {} + override fun afterSuite(suite: TestDescriptor, result: TestResult) { + require(result.testCount > 0) { + "There are no executed test. This is unexpected and should be investigated!" + } + } + }) +} + +tasks.test { + // Before we switched to JUnit 5, we used JUnit 4 with a customized discovery of test class. + // This discovery called AutoSuite and searched in the compiled classes. AutoSuite was + // necessary due to bugs caused in some execution order. + // AutoSuites made the test order deterministic. A last known commit to find AutoSuite (for the case), + // is 980294d04008f6b3798986bce218bac2753b4783. + + useJUnitPlatform { + excludeTags("owntest", "interactive", "performance") + } + + testLogging { + outputs.upToDateWhen { false } + showStandardStreams = false + + // set options for log level LIFECYCLE + events = setOf(TestLogEvent.FAILED) + exceptionFormat = TestExceptionFormat.SHORT + + // set options for log level DEBUG + info { + // remove standard output/error logging from --info builds + // by assigning only 'failed' and 'skipped' events + events = setOf(TestLogEvent.FAILED, TestLogEvent.SKIPPED) + exceptionFormat = TestExceptionFormat.SHORT + showStandardStreams = true + showStackTraces = true + } + + // set options for log level DEBUG + debug { + events = setOf( + TestLogEvent.STARTED, TestLogEvent.SKIPPED, TestLogEvent.FAILED, TestLogEvent.PASSED + ) + exceptionFormat = TestExceptionFormat.FULL + showStackTraces = true + showStandardStreams = true + } + } +} + + +// The following two tasks can be used to execute main methods from the project +// The main class is set via "gradle -DmainClass=... execute --args ..." +// see https://stackoverflow.com/questions/21358466/gradle-to-execute-java-class-without-modifying-build-gradle +tasks.register("execute") { + description = + "Execute main method from the project. Set main class via \"gradle -DmainClass=... execute --args ...\"" + group = "application" + mainClass.set(System.getProperty("mainClass")) + classpath = sourceSets["main"].runtimeClasspath +} + +tasks.register("executeInTests") { + description = + "Execute main method from the project (tests loaded). Set main class via \"gradle -DmainClass=... execute --args ...\"" + group = "application" + mainClass.set(System.getProperty("mainClass")) + classpath = sourceSets["test"].runtimeClasspath +} + +eclipse.classpath.file { + whenMerged(Action { -> + // This adds the exclude entry for every resource and antlr folder. + //As eclipse is so stupid, that it does not distuinguish between resource and java folder correctly. + entries.filterIsInstance().filter { it -> it.path.endsWith("src/test/antlr") } + .forEach { it.excludes = listOf("**/*.java") } + + entries.filterIsInstance().filter { it.path.endsWith("/resources") } + .forEach { it.excludes = listOf("**/*.java") } + }) +} + +spotless { + // see https://github.com/diffplug/spotless/tree/main/plugin-gradle + + // optional: limit format enforcement to just the files changed by this feature branch + // ratchetFrom 'origin/master' + + format("Key") { + // define the files to apply `misc` to + //target '*.gradle', '*.md', '.gitignore' + target("src/main/resources/**/*.key") + trimTrailingWhitespace() + //indentWithSpaces(4) // this does not really work + endWithNewline() + // TODO: license headers are problematic at the moment, + // see https://git.key-project.org/key/key/-/wikis/KaKeY%202022-09-30 + //licenseHeaderFile("$rootDir/gradle/header", '\\s*\\\\\\w+') + } + + antlr4 { + target("src/*/antlr4/**/*.g4") // default value, you can change if you want + //licenseHeaderFile "$rootDir/gradle/header" + } + + java { + //target("*.java") + // don't need to set target, it is inferred from java + + // We ignore the build folder to avoid double checks and checks of generated code. + targetExclude("build/**") + + // allows us to use spotless:off / spotless:on to keep pre-formatted sections + // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on" + // that must be used instead. + toggleOffOn() + + removeUnusedImports() + + /* When new options are added in new versions of the Eclipse formatter, the easiest way is to export the new + * style file from the Eclipse GUI and then use the CodeStyleMerger tool in + * "$rootDir/scripts/tools/checkstyle/CodeStyleMerger.java" to merge the old and the new style files, + * i.e. "java CodeStyleMerger.java keyCodeStyle.xml". The tool adds all + * entries with keys that were not present in the old file and optionally overwrites the old entries. The + * file is output with ordered keys, such that the file can easily be diffed using git. + */ + eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") + trimTrailingWhitespace() // not sure how to set this in the xml file ... + //googleJavaFormat().aosp().reflowLongStrings() + + // note: you can use an empty string for all the imports you didn't specify explicitly, + // '|' to join group without blank line, and '\\#` prefix for static imports + importOrder("java|javax", "de.uka", "org.key_project", "", "\\#") + + // specific delimiter: normally just 'package', but spotless crashes for files in default package + // (see https://github.com/diffplug/spotless/issues/30), therefore 'import' is needed. '//' is for files + // with completely commented out code (which would probably better just be removed in future). + if (project.name == "recoder") { + licenseHeaderFile("$rootDir/gradle/header-recoder", "(package|import|//)") + } else { + licenseHeaderFile("$rootDir/gradle/header", "(package|import|//)") + } + } +} + +publishing { + publications { + create("mavenJava") { + from(components["java"]) + pom { + name = project.name + description = project.description + url = "https://key-project.org/" + + licenses { + license { + name = "GNU General Public License (GPL), Version 2" + url = "https://www.gnu.org/licenses/old-licenses/gpl-2.0.html" + } + } + + developers { + developer { + id = "key" + name = "KeY Developers" + email = "support@key-project.org" + url = "https://www.key-project.org/about/people/" + } + } + scm { + connection = "scm:git:git://github.com/keyproject/key.git" + developerConnection = "scm:git:git://github.com/keyproject/key.git" + url = "https://github.com/keyproject/key/" + } + } + } + } + repositories { + maven { + name = "Maven Central" + /** + * To be able to publish things on Maven Central, you need two things: + * + * (1) a JIRA account with permission on group-id `org.key-project` + * (2) a keyserver-published GPG (w/o sub-keys) + * + * Your `$HOME/.gradle/gradle.properties` should like this: + * ``` + * signing.keyId=YourKeyId + * signing.password=YourPublicKeyPassword + * ossrhUsername=your-jira-id + * ossrhPassword=your-jira-password + * ``` + * + * You can test signing with `gradle sign`, and publish with `gradle publish`. + * https://central.sonatype.org/publish/publish-guide/ + */ + val ossrhUsername = project.properties.getOrDefault("ossrhUsername", "").toString() + val ossrhPassword = project.properties.getOrDefault("ossrhPassword", "").toString() + + if (project.version.toString().endsWith("-SNAPSHOT")) { + name = "mavenSnapshot" + url = uri("https://s01.oss.sonatype.org/content/repositories/snapshots/") + credentials { + username = ossrhUsername + password = ossrhPassword + } + } else { + name = "mavenStaging" + url = uri("https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/") + credentials { + username = ossrhUsername + password = ossrhPassword + } + } + } + + maven { + // deployment to git.key-project.org + name = "Keylab" + url = uri("https://git.key-project.org/api/v4/projects/35/packages/maven") + credentials(HttpHeaderCredentials::class) { + if (System.getenv("TOKEN") != null) { + name = "Private-Token" // for private pushing + value = findProperty("keylab.token") as String? + ?: System.getenv("keylab.token").toString() + } else { + name = "Job-Token" // for gitlab CI + value = System.getenv("CI_JOB_TOKEN") + } + } + authentication { + create("header", HttpHeaderAuthentication::class) + } + } + } +} + +signing { + useGpgCmd() // works better than the Java implementation, which requires PGP keyrings. + sign(publishing.publications.getByName("mavenJava")) +} + + +extra["CHECKER_FRAMEWORK_PACKAGES_REGEX"] = "^org\\.key_project" + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS").toBoolean()) { + checkers = listOf("org.checkerframework.checker.nullness.NullnessChecker") + val stubsEntries = listOf( + "$rootDir/key.util/src/main/checkerframework", + "permit-nullness-assertion-exception.astub", + "checker.jar/junit-assertions.astub" + ) + val stubs = stubsEntries.joinToString(File.pathSeparator) + + extraJavacArgs = listOf( + extra["CHECKER_FRAMEWORK_PACKAGES_REGEX"]?.let { "-AonlyDefs=$it" } ?: "", + "-Xmaxerrs", "10000", + "-Astubs=$stubs", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ) + } +} diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml new file mode 100644 index 00000000000..e4c64c18128 --- /dev/null +++ b/gradle/libs.versions.toml @@ -0,0 +1,54 @@ +[versions] +jspecify = "1.0.0" +eisop = "3.42.0-eisop5" +kotlin = "2.2.0" +junit = "5.13.4" +retrotranslator = "1.2.9" + +[libraries] +kotlinGradlePlugin = { module = "org.jetbrains.kotlin:kotlin-gradle-plugin", version.ref = "kotlin" } + +jspecify = { module = "org.jspecify:jspecify", version.ref = "jspecify" } +slf4j = { module = "org.slf4j:slf4j-api", version = "2.0.16" } + +eisopCheckerQual = { module = "io.github.eisop:checker-qual", version.ref = "eisop" } +eisopUtil = { module = "io.github.eisop:checker-util", version.ref = "eisop" } +eisopChecker = { module = "io.github.eisop:checker", version.ref = "eisop" } + +assertj = { module = "org.assertj:assertj-core", version = "3.27.3" } +logback = { module = "ch.qos.logback:logback-classic", version = "1.5.15" } + + +yaml = { module = "com.fasterxml.jackson.dataformat:jackson-dataformat-yaml", version = "2.18.2" } +yamljsr = { module = "com.fasterxml.jackson.datatype:jackson-datatype-jsr310", version = "2.18.2" } + +junit-bom = { module = "org.junit:junit-bom", version.ref = "junit" } +junit-api = { module = "org.junit.jupiter:junit-jupiter-api" } +junit-params = { module = "org.junit.jupiter:junit-jupiter-params" } +junit-engine = { module = "org.junit.jupiter:junit-jupiter-engine" } +junit-platform = { module = "org.junit.platform:junit-platform-launcher" } + +javacc = { module = "net.java.dev.javacc:javacc", version = "4.0" } +antlr = { module = "org.antlr:antlr4", version = "4.13.2" } +antlrRuntime = { module = "org.antlr:antlr4-runtime", version = "4.13.2" } +miglayout = { module = "com.miglayout:miglayout-swing", version = "11.4.2" } + +dockingFramesCommon = { module = "org.key-project:docking-frames-common", version = "1.1.3p1" } +dockingFramesCore = { module = "org.key-project:docking-frames-core", version = "1.1.3p1" } + +stringtemplate = { module = "org.antlr:ST4", version = "4.3.4" } + +## recoder stuff +asm = { module = "org.ow2.asm:asm", version = "9.8" } +beanshell = { module = "org.apache-extras.beanshell:bsh", version = "2.0b6" } +retrotranslator-runtime = { module = "net.sf.retrotranslator:retrotranslator-runtime", version.ref = "retrotranslator" } +retrotranslator-transformer = { module = "net.sf.retrotranslator:retrotranslator-transformer", version.ref = "retrotranslator" } + +[bundles] +testing = ["junit-api", "junit-params", "assertj", "logback", "yaml", "yamljsr"] + +recoder = ["asm", "beanshell", "retrotranslator-runtime", "retrotranslator-transformer"] + + +[plugins] +shadowjar = { id = "com.gradleup.shadow", version = "9.0.1" } \ No newline at end of file diff --git a/key.core.example/build.gradle b/key.core.example/build.gradle.kts similarity index 53% rename from key.core.example/build.gradle rename to key.core.example/build.gradle.kts index c96f606393f..6ceb3880225 100644 --- a/key.core.example/build.gradle +++ b/key.core.example/build.gradle.kts @@ -1,5 +1,6 @@ plugins { - id 'application' + id("java-convention") + application } description = "Example project to use KeY's APIs" @@ -9,6 +10,6 @@ application { } dependencies { - implementation project(":key.core") - implementation 'ch.qos.logback:logback-classic:1.5.32' + implementation(project(":key.core")) + implementation(libs.logback) } \ No newline at end of file diff --git a/key.core.infflow/build.gradle b/key.core.infflow/build.gradle deleted file mode 100644 index 9edc6360b73..00000000000 --- a/key.core.infflow/build.gradle +++ /dev/null @@ -1,25 +0,0 @@ - - -dependencies { - api(project(":key.core")) - testImplementation(project(":key.core").sourceSets.test.output) -} - - -tasks.register('testRunAllInfProofs', Test) { - description = 'Prove/reload all keyfiles tagged for regression testing' - group = "verification" - filter { - includeTestsMatching "RunAllProofsInfFlow" - } -} - - -def rapDir = layout.buildDirectory.dir("generated-src/rap/").getOrNull() -sourceSets.test.java.srcDirs(rapDir) - -tasks.register('generateRAPUnitTests', JavaExec) { - classpath = sourceSets.test.runtimeClasspath - mainClass.set("de.uka.ilkd.key.informationflow.GenerateUnitTests") - args(rapDir) -} diff --git a/key.core.infflow/build.gradle.kts b/key.core.infflow/build.gradle.kts new file mode 100644 index 00000000000..61aa03493f2 --- /dev/null +++ b/key.core.infflow/build.gradle.kts @@ -0,0 +1,28 @@ +plugins { + id("java-convention") +} + + +dependencies { + api(project(":key.core")) + testImplementation(testFixtures(project(":key.core"))) +} + + +tasks.register("testRunAllInfProofs") { + description = "Prove/reload all keyfiles tagged for regression testing" + group = "verification" + filter { + includeTestsMatching("RunAllProofsInfFlow") + } +} + + +val rapDir = layout.buildDirectory.dir("generated-src/rap/").get() +sourceSets["test"].java.srcDirs(rapDir) + +tasks.register("generateRAPUnitTests") { + classpath = sourceSets["test"].runtimeClasspath + mainClass.set("de.uka.ilkd.key.wd.GenerateUnitTests") + args(rapDir) +} diff --git a/key.core.proof_references/build.gradle b/key.core.proof_references/build.gradle.kts similarity index 56% rename from key.core.proof_references/build.gradle rename to key.core.proof_references/build.gradle.kts index 3c857464238..9f0db05cf39 100644 --- a/key.core.proof_references/build.gradle +++ b/key.core.proof_references/build.gradle.kts @@ -1,5 +1,9 @@ +plugins { + id("java-convention") +} + description = "API for using KeY for maintaining references between objects in proofs" dependencies { - implementation project(":key.core") + implementation(project(":key.core")) } diff --git a/key.core.rifl/build.gradle b/key.core.rifl/build.gradle.kts similarity index 51% rename from key.core.rifl/build.gradle rename to key.core.rifl/build.gradle.kts index 5d5aa84bf64..653ec0df73c 100644 --- a/key.core.rifl/build.gradle +++ b/key.core.rifl/build.gradle.kts @@ -1,4 +1,9 @@ +plugins { + id("java-convention") +} + description = "Support for the RS3 Information Flow Language (RIFL)" + dependencies { - implementation project (":key.core") + implementation(project(":key.core")) } \ No newline at end of file diff --git a/key.core.symbolic_execution.example/build.gradle b/key.core.symbolic_execution.example/build.gradle deleted file mode 100644 index 4f5dc697988..00000000000 --- a/key.core.symbolic_execution.example/build.gradle +++ /dev/null @@ -1,6 +0,0 @@ -description = "Example project to use KeY's APIs" - -dependencies { - implementation project(":key.core") - implementation project(":key.core.symbolic_execution") -} \ No newline at end of file diff --git a/key.core.symbolic_execution.example/build.gradle.kts b/key.core.symbolic_execution.example/build.gradle.kts new file mode 100644 index 00000000000..90dd69fac63 --- /dev/null +++ b/key.core.symbolic_execution.example/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-convention") +} + +description = "Example project to use KeY's APIs" + +dependencies { + implementation (project(":key.core")) + implementation (project(":key.core.symbolic_execution")) +} \ No newline at end of file diff --git a/key.core.symbolic_execution/build.gradle b/key.core.symbolic_execution/build.gradle deleted file mode 100644 index 697c8045706..00000000000 --- a/key.core.symbolic_execution/build.gradle +++ /dev/null @@ -1,12 +0,0 @@ -description = "API for using KeY as a symbolic execution engine for Java programs" - -dependencies { - implementation project(":key.core") - testImplementation project(":key.core").sourceSets.test.output -} - -test { - maxHeapSize = "4g" - systemProperty "UPDATE_TEST_ORACLE", System.getProperty("UPDATE_TEST_ORACLE") - systemProperty "ORACLE_DIRECTORY", System.getProperty("ORACLE_DIRECTORY") -} diff --git a/key.core.symbolic_execution/build.gradle.kts b/key.core.symbolic_execution/build.gradle.kts new file mode 100644 index 00000000000..c1c4a9ba7f9 --- /dev/null +++ b/key.core.symbolic_execution/build.gradle.kts @@ -0,0 +1,16 @@ +plugins { + id("java-convention") +} + +description = "API for using KeY as a symbolic execution engine for Java programs" + +dependencies { + implementation(project(":key.core")) + testImplementation(project(":key.core", configuration = "testArtifacts")) +} + +tasks.test { + maxHeapSize = "4g" + systemProperty("UPDATE_TEST_ORACLE", System.getProperty("UPDATE_TEST_ORACLE")) + systemProperty("ORACLE_DIRECTORY", System.getProperty("ORACLE_DIRECTORY")) +} diff --git a/key.core.testgen/build.gradle b/key.core.testgen/build.gradle deleted file mode 100644 index 7a81dad8962..00000000000 --- a/key.core.testgen/build.gradle +++ /dev/null @@ -1,9 +0,0 @@ -description = "Test Case Generation based on proof attempts." - -dependencies { - implementation project(":key.core") - implementation("com.squareup:javapoet:1.13.0") - - implementation "info.picocli:picocli:4.7.7" -} - diff --git a/key.core.testgen/build.gradle.kts b/key.core.testgen/build.gradle.kts new file mode 100644 index 00000000000..1898fc32875 --- /dev/null +++ b/key.core.testgen/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-convention") +} + +description = "Test Case Generation based on proof attempts." + +dependencies { + implementation (project(":key.core")) +} diff --git a/key.core.wd/build.gradle b/key.core.wd/build.gradle deleted file mode 100644 index cbf92d09e6a..00000000000 --- a/key.core.wd/build.gradle +++ /dev/null @@ -1,22 +0,0 @@ -dependencies { - api(project(":key.core")) - testImplementation(project(":key.core").sourceSets.test.output) -} - -tasks.register('testRunAllWdProofs', Test) { - description = 'Prove/reload all keyfiles tagged for regression testing' - group = "verification" - filter { - includeTestsMatching "RunAllProofsWd" - } -} - - -def rapDir = layout.buildDirectory.dir("generated-src/rap/").getOrNull() -sourceSets.test.java.srcDirs(rapDir) - -tasks.register('generateRAPUnitTests', JavaExec) { - classpath = sourceSets.test.runtimeClasspath - mainClass.set("de.uka.ilkd.key.wd.GenerateUnitTests") - args(rapDir) -} diff --git a/key.core.wd/build.gradle.kts b/key.core.wd/build.gradle.kts new file mode 100644 index 00000000000..db4b44e0927 --- /dev/null +++ b/key.core.wd/build.gradle.kts @@ -0,0 +1,26 @@ +plugins { + id("java-convention") +} + +dependencies { + api(project(":key.core")) + testImplementation(testFixtures(project(":key.core"))) +} + +tasks.register("testRunAllWdProofs") { + description = "Prove/reload all keyfiles tagged for regression testing" + group = "verification" + filter { + includeTestsMatching ("RunAllProofsWd") + } +} + + +val rapDir = layout.buildDirectory.dir("generated-src/rap/").get() +sourceSets["test"].java.srcDirs(rapDir) + +tasks.register("generateRAPUnitTests") { + classpath = sourceSets["test"].runtimeClasspath + mainClass.set("de.uka.ilkd.key.wd.GenerateUnitTests") + args(rapDir) +} diff --git a/key.core/build.gradle b/key.core/build.gradle deleted file mode 100644 index 2645553ba50..00000000000 --- a/key.core/build.gradle +++ /dev/null @@ -1,247 +0,0 @@ -plugins { - id 'org.javacc.javacc' version '4.0.3' -} - -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') - //api group: group, name: 'recoderkey', version: '1.0' - api project(':recoder') - - // JavaCC - implementation group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' - javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' - - antlr4 "org.antlr:antlr4:4.13.2" - api "org.antlr:antlr4-runtime:4.13.2" -} - -// 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(javaCCOutputDirMain, "$projectDir/build/generated-src/antlr4/main/") - -// Generate code from JavaCC grammars. -compileJavacc { - outputDirectory = javaCCOutputDirMain - inputDirectory = file("src/main/javacc") - doLast { - // Some manual overwriting of Token files needed - copy { - from("src/main/javacc/de/uka/ilkd/key/parser/schemajava/Token.java") - into "$javaCCOutputDirMain/de/uka/ilkd/key/parser/schemajava/" - } - copy { - from("src/main/javacc/de/uka/ilkd/key/parser/proofjava/Token.java") - into "$javaCCOutputDirMain/de/uka/ilkd/key/parser/proofjava/" - } - copy { - from("src/main/javacc/de/uka/ilkd/key/parser/schemajava/JavaCharStream.java") - into "$javaCCOutputDirMain/de/uka/ilkd/key/parser/schemajava/" - } - copy { - from("src/main/javacc/de/uka/ilkd/key/parser/proofjava/JavaCharStream.java") - into "$javaCCOutputDirMain/de/uka/ilkd/key/parser/proofjava/" - } - } -} - -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 '' - list.writeLine '' - list.writeLine '' - new File("$resourcesDir/$pack").eachFile { - if (it.name.endsWith('.DefinedSymbolsHandler.preamble.xml')) { - // println it.name - it.eachLine { list.writeLine it } - } - } - list.writeLine '' - } - } -} - -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) -} - -sourceSets.test.java.srcDirs(rapDir) - -sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key, compileJavacc) diff --git a/key.core/build.gradle.kts b/key.core/build.gradle.kts new file mode 100644 index 00000000000..c79e69fc22f --- /dev/null +++ b/key.core/build.gradle.kts @@ -0,0 +1,277 @@ +import org.eclipse.jgit.lib.Repository +import org.eclipse.jgit.storage.file.FileRepositoryBuilder +import org.javacc.plugin.gradle.javacc.CompileJavaccTask +import java.nio.file.Files +import java.nio.file.StandardCopyOption + +plugins { + id("java-convention") + id("org.javacc.javacc") version "4.0.1" +} + +description = "Core functionality (terms, rules, prover, ...) for deductive verification of Java programs" + +val antlr4 by configurations.creating + + +// region Exposing TEST artifact +// This is not good. Normally there is a Gradle way for exposing text fixtures. +// This is the lightweight variant to expose test classes to key.core.symbolic_execution. +// This dependency should be resolved in the future. +val testJar by tasks.registering(Jar::class) { + archiveClassifier.set("test") + from(sourceSets["test"].output) +} +artifacts { + val testArtifacts by configurations.creating + add("testArtifacts", testJar) +} +//endregion + + +dependencies { + api(project(":key.util")) + api(project(":key.ncore")) + api(project(":key.ncore.calculus")) + api(project(":recoder")) + + implementation(libs.javacc) + javacc(libs.javacc) + antlr4(libs.antlr) + api(libs.antlrRuntime) +} + +val javaCCOutputDir = layout.buildDirectory.dir("generated-src/javacc") +val javaCCOutputDirMain = javaCCOutputDir.map { it.dir("main") } + +sourceSets["main"].java.srcDirs( + javaCCOutputDirMain.get().asFile, + file("$projectDir/build/generated-src/antlr4/main/") +) + + +tasks.named("compileJavacc") { + outputDirectory = javaCCOutputDirMain.get().asFile + inputDirectory = file("src/main/javacc") + doLast { + // Some manual overwriting of Token files needed + for (folder in listOf("schemajava", "proofjava")) { + for (fil in listOf( + "de/uka/ilkd/key/parser/$folder/Token.java", + "de/uka/ilkd/key/parser/$folder/JavaCharStream.java" + )) { + Files.copy( + projectDir.toPath().resolve("src/main/javacc/$fil"), + javaCCOutputDirMain.get().asFile.toPath().resolve(fil), + StandardCopyOption.REPLACE_EXISTING + ) + } + } + } +} + +tasks.register("generateSMTListings") { + val pack = "de/uka/ilkd/key/smt/newsmt2" + val resourcesDir = file("src/main/resources") + val outputDir = resourcesDir + + inputs.files(fileTree("$resourcesDir/$pack") { + exclude("$resourcesDir/$pack/DefinedSymbolsHandler.preamble.xml") + }) + outputs.file(file("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml")) + + doLast { + val outputFile = file("$outputDir/$pack/DefinedSymbolsHandler.preamble.xml") + outputFile.bufferedWriter().use { writer -> + writer.write( + """ + + + + """.trimIndent() + ) + file("$resourcesDir/$pack").listFiles()?.forEach { + if (it.name.endsWith(".DefinedSymbolsHandler.preamble.xml")) { + it.forEachLine { line -> writer.write(line) } + } + } + writer.write("") + } + } +} + +tasks.register("generateSolverPropsList") { + val pack = "de/uka/ilkd/key/smt/solvertypes" + val resourcesDir = file("src/main/resources") + val outputDir = resourcesDir + + inputs.files(fileTree("$outputDir/$pack") { + exclude("solvers.txt") + }) + outputs.file(file("$outputDir/$pack/solvers.txt")) + + doLast { + val list = mutableListOf() + file("$outputDir/$pack").walkTopDown().forEach { + if (it.name.endsWith(".props")) list.add(it.name) + } + list.sort() + file("$outputDir/$pack/solvers.txt").writeText(list.joinToString(System.lineSeparator())) + } +} + +tasks.named("classes") { + dependsOn("generateSMTListings", "generateSolverPropsList") +} + +tasks.register("testProveRules") { + description = "Proves KeY taclet rules tagged as lemma" + group = "verification" + filter { + includeTestsMatching("ProveRulesTest") + } +} + +tasks.register("testRunAllFunProofs") { + description = "Prove/reload all keyfiles tagged for regression testing" + group = "verification" + filter { + includeTestsMatching("RunAllProofsFunctional") + } +} + +tasks.register("testRunAllInfProofs") { + description = "Prove/reload all keyfiles tagged for regression testing" + group = "verification" + filter { + includeTestsMatching("RunAllProofsInfFlow") + } +} + +tasks.register("testProveSMTLemmas") { + description = "Prove (or load proofs for) lemmas used in the SMT translation" + group = "verification" + filter { + includeTestsMatching("ProveSMTLemmasTest") + } +} + +tasks.register("testStrictSMT") { + description = "Run the tests for the new smt translation in strict mode" + group = "verification" + systemProperty("key.newsmt2.stricttests", "true") + filter { + includeTestsMatching("MasterHandlerTest") + } +} + + +tasks.register("generateVersionFiles") { + val outputFolder = file("build/resources/main/de/uka/ilkd/key/util") + val sha1 = File(outputFolder, "sha1") + val branch = File(outputFolder, "branch") + val versionf = File(outputFolder, "version") + + inputs.file("${project.rootDir}/.git/HEAD") + outputs.files(sha1, branch, versionf) + + doLast { + val builder = FileRepositoryBuilder() + val repository: Repository = builder.setGitDir(File(rootDir, ".git")) + .readEnvironment() + .findGitDir() + .build() + + repository.use { + val ref = it.resolve("HEAD") + val version = ref?.name() ?: "" + val short = ref?.abbreviate(8)?.name() ?: "" + sha1.writeText(version) + branch.writeText(short) + versionf.writeText(rootProject.version.toString()) + } + } +} + +tasks.named("processResources") { + dependsOn("generateVersionFiles", "generateSolverPropsList", "generateSMTListings") +} + +val antlr4OutputKey = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/nparser" + +tasks.register("runAntlr4Key") { + inputs.files("src/main/antlr4/KeYLexer.g4", "src/main/antlr4/KeYParser.g4") + outputs.dir(antlr4OutputKey) + classpath = antlr4 + mainClass.set("org.antlr.v4.Tool") + args = listOf( + "-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") + } +} + +tasks.named("compileJava") { + dependsOn("runAntlr4Key") +} + +tasks.register("debugKeyLexer") { + mainClass.set("de.uka.ilkd.key.nparser.DebugKeyLexer") + classpath = sourceSets["main"].runtimeClasspath + standardInput = System.`in` +} + +tasks.named("processResources") { + dependsOn("generateVersionFiles") +} + +val antlr4OutputJml = "$projectDir/build/generated-src/antlr4/main/de/uka/ilkd/key/speclang/njml" + +tasks.register("runAntlr4Jml") { + 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 = listOf( + "-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") + } +} + +tasks.named("compileJava") { + dependsOn("runAntlr4Jml") +} + +tasks.register("debugJmlLexer") { + mainClass.set("de.uka.ilkd.key.speclang.njml.DebugJmlLexer") + classpath = sourceSets["main"].runtimeClasspath + standardInput = System.`in` +} + +tasks.register("ptest") { + group = "verification" +} + +val rapDir = layout.buildDirectory.dir("generated-src/rap") + +tasks.register("generateRAPUnitTests") { + classpath = sourceSets["test"].runtimeClasspath + mainClass.set("de.uka.ilkd.key.proof.runallproofs.GenerateUnitTests") + args = listOf(rapDir.get().asFile.absolutePath) +} + +sourceSets["test"].java.srcDirs(rapDir.get().asFile) + +tasks.named("sourcesJar") { + dependsOn("runAntlr4Jml", "runAntlr4Key", "compileJavacc") +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 167aff7270c..3e437adb6ca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -478,7 +478,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { .map(e -> Paths.get(e.getName())).toList(); if (!proofs.isEmpty()) { // load first proof found in file - proofFilename = proofs.get(0); + proofFilename = proofs.getFirst(); } else { // no proof found in bundle! throw new IOException("The bundle contains no proof to load!"); diff --git a/key.ncore.calculus/build.gradle b/key.ncore.calculus/build.gradle deleted file mode 100644 index 05e0fe5994d..00000000000 --- a/key.ncore.calculus/build.gradle +++ /dev/null @@ -1,25 +0,0 @@ -repositories { - mavenCentral() -} - -dependencies { - api project(':key.util') - api project(':key.ncore') - implementation('org.jspecify:jspecify:1.0.0') -} - -checkerFramework { - if (System.getProperty("ENABLE_NULLNESS")) { - checkers = [ - "org.checkerframework.checker.nullness.NullnessChecker", - ] - extraJavacArgs = [ - //"-AonlyDefs=^org\\.key_project\\.prover", - "-Xmaxerrs", "10000", - "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub", - "-AstubNoWarnIfNotFound", - "-Werror", - "-Aversion", - ] - } -} \ No newline at end of file diff --git a/key.ncore.calculus/build.gradle.kts b/key.ncore.calculus/build.gradle.kts new file mode 100644 index 00000000000..43cdff45c6c --- /dev/null +++ b/key.ncore.calculus/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-convention") + +} + +dependencies { + api(project(":key.util")) + api(project(":key.ncore")) +} \ No newline at end of file diff --git a/key.ncore/build.gradle b/key.ncore/build.gradle deleted file mode 100644 index ea2fee5167f..00000000000 --- a/key.ncore/build.gradle +++ /dev/null @@ -1,32 +0,0 @@ -plugins { -} - -description = "Generic data strutures for terms and formulas without dependencies to a specific target programming language" - -configurations { } - -dependencies { - api project(':key.util') - implementation 'org.jspecify:jspecify:1.0.0' -} - -tasks.withType(Test) { - enableAssertions = true -} - - -checkerFramework { - if(System.getProperty("ENABLE_NULLNESS")) { - checkers = [ - "org.checkerframework.checker.nullness.NullnessChecker", - ] - extraJavacArgs = [ - "-AonlyDefs=^org\\.key_project\\.logic", - "-Xmaxerrs", "10000", - "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub", - "-AstubNoWarnIfNotFound", - "-Werror", - "-Aversion", - ] - } -} diff --git a/key.ncore/build.gradle.kts b/key.ncore/build.gradle.kts new file mode 100644 index 00000000000..602855cd567 --- /dev/null +++ b/key.ncore/build.gradle.kts @@ -0,0 +1,12 @@ +plugins { + id("java-convention") +} + +description = "Generic data structures for terms and formulas without " + + "dependencies to a specific target programming language" + +dependencies { + api(project(":key.util")) +} + +//extra = "org\\.key_project\\.logic" diff --git a/key.removegenerics/build.gradle b/key.removegenerics/build.gradle.kts similarity index 65% rename from key.removegenerics/build.gradle rename to key.removegenerics/build.gradle.kts index 607cac04ecd..8a594d9c5ce 100644 --- a/key.removegenerics/build.gradle +++ b/key.removegenerics/build.gradle.kts @@ -1,19 +1,20 @@ plugins { - id 'application' - id 'com.gradleup.shadow' version "9.3.2" + id("java-convention") + application + id("com.gradleup.shadow") } description = "Helper to remove generics from Java source code" dependencies { - implementation project(":key.core") + implementation (project(":key.core")) } application { mainClass.set("de.uka.ilkd.key.util.removegenerics.Main") } -shadowJar { +tasks.shadowJar { archiveClassifier = "exe" archiveBaseName = "key.removegenerics" } diff --git a/key.ui/build.gradle b/key.ui/build.gradle deleted file mode 100644 index ed237374e59..00000000000 --- a/key.ui/build.gradle +++ /dev/null @@ -1,153 +0,0 @@ -import java.nio.file.Files -import java.nio.file.Paths - - -plugins { - id 'application' - - // Used to create a single executable jar file with all dependencies - // see task "shadowJar" below - // https://github.com/GradleUp/shadow - id 'com.gradleup.shadow' version "9.3.2" -} - -description = "User interface for the deductive verification of Java programs" - -dependencies { - implementation project(":key.core") - implementation project(":key.core.rifl") - - implementation("com.formdev:flatlaf:3.7") - - implementation project(":key.core.infflow") - implementation project(":key.core.wd") - - implementation project(":key.core.proof_references") - implementation project(":key.core.symbolic_execution") - implementation project(":key.removegenerics") - - api 'com.miglayout:miglayout-swing:11.4.3' - - implementation("info.picocli:picocli:4.7.7") - - //logging implementation used by the slf4j - implementation 'ch.qos.logback:logback-classic:1.5.32' - - api 'org.key-project:docking-frames-common:1.1.3p1' - api 'org.key-project:docking-frames-core:1.1.3p1' - - runtimeOnly project(":keyext.ui.testgen") - runtimeOnly project(":keyext.caching") - runtimeOnly project(":keyext.exploration") - runtimeOnly project(":keyext.slicing") - runtimeOnly project(":keyext.proofmanagement") - runtimeOnly project(":keyext.isabelletranslation") -} - -tasks.register('createExamplesZip', Zip) { - description = 'Create "examples.zip" containing all KeY examples' - destinationDirectory = layout.buildDirectory.dir("resources/main/").getOrNull() - archiveFileName = "examples.zip" - from "examples" - include scanReadmeFiles() // see end of file -} - -processResources.dependsOn << createExamplesZip - - -shadowJar { - archiveClassifier.set("exe") - archiveBaseName.set("key") - filesMatching("META-INF/services/**") { - duplicatesStrategy = DuplicatesStrategy.INCLUDE // needed for mergeServices - } - mergeServiceFiles() -} - -distZip { - archiveBaseName.set("key") -} - -application { - mainClass.set("de.uka.ilkd.key.core.Main") -} - -run { - systemProperties["key.examples.dir"] = "$projectDir/examples" - //systemProperties["slf4j.detectLoggerNameMismatch"] = true - //systemProperties["KeyDebugFlag"] = "on" - //args "--experimental" - - // enable assertion - jvmArgs += "-ea" - - // this can be used to solve a problem where the OS hangs during debugging of popup menus - // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425) - jvmArgs += "-Dsun.awt.disablegrab=true" -} - -tasks.register('runWithProfiler', JavaExec) { - group = "application" - description = """Run key.ui with flight recoder enabled. - See https://www.baeldung.com/java-flight-recorder-monitoring for a how to.""" - - classpath = sourceSets.main.runtimeClasspath - mainClass.set("de.uka.ilkd.key.core.Main") - jvmArgs = ["-XX:+FlightRecorder", - "-XX:StartFlightRecording=duration=30s,filename=key_profile.jfr", - "-XX:FlightRecorderOptions=stackdepth=256"] - doLast { - println "A file key_profile.jfr has been created in folder 'key.ui' by JRE (FlightRecoder)." - println "You can open key_profile.jfr in IntelliJ to inspect the performance measurement." - } -} - -tasks.register('runInExperimentalMode', JavaExec) { - group = "application" - classpath = sourceSets.main.runtimeClasspath - mainClass.set("de.uka.ilkd.key.core.Main") - args("--experimental") -} - -/** - * Go and scan all registered README.txt files for files that need to be - * included into examples.zip. Thus only those files that can actually be - * accessed from the example browser are added to examples.zip. - * - * The file size is reduced considerably. - * - * @return a list of filenames to be added to examples.zip. Each line - * is relative to the examples directory. - */ -List scanReadmeFiles() { - def examplesIndex = Paths.get(projectDir.toString(), - "examples", "index", "samplesIndex.txt") - List result = new ArrayList<>() - result.add("index/samplesIndex.txt") - for (String line : Files.readAllLines(examplesIndex)) { - line = line.trim() - if (line.isEmpty() || line.startsWith("#")) { - continue - } - - def readme = Paths.get(projectDir.toString(), "examples", - line.replace("/", File.separator)) - def dir = line.substring(0, line.lastIndexOf('/') + 1) - result.add(line) - // The project file is not always project.key, but better include the - // default file. - result.add(dir + "project.key") - for (String rmLine : Files.readAllLines(readme)) { - if(rmLine.startsWith("#")) continue - def parts = rmLine.split("=", 2) - if (parts.length < 2) break - def key = parts[0].trim() - if(key.containsIgnoreCase("file")) { - def filename = parts[1].trim() - result.add(dir + filename) - } - } - } - // println(result) - return result -} diff --git a/key.ui/build.gradle.kts b/key.ui/build.gradle.kts new file mode 100644 index 00000000000..7438c3a4cc3 --- /dev/null +++ b/key.ui/build.gradle.kts @@ -0,0 +1,136 @@ +import java.nio.file.Paths +import kotlin.io.path.readLines + +plugins { + id("java-convention") + application + // Used to create a single executable jar file with all dependencies + // see task "shadowJar" below + // https://github.com/GradleUp/shadow + id("com.gradleup.shadow") +} + +description = "User interface for the deductive verification of Java programs" + +dependencies { + implementation(project(":key.core")) + implementation(project(":key.core.rifl")) + + implementation("com.formdev:flatlaf:3.6.1") + + implementation(project(":key.core.proof_references")) + implementation(project(":key.core.symbolic_execution")) + implementation(project(":key.removegenerics")) + + api(libs.miglayout) + + //logging implementation used by the slf4j + implementation(libs.logback) + + api(libs.dockingFramesCommon) + api(libs.dockingFramesCore) + + runtimeOnly(project(":keyext.ui.testgen")) + runtimeOnly(project(":keyext.caching")) + runtimeOnly(project(":keyext.exploration")) + runtimeOnly(project(":keyext.slicing")) + runtimeOnly(project(":keyext.proofmanagement")) + runtimeOnly(project(":keyext.isabelletranslation")) +} + +val createExamplesZip by tasks.registering(Zip::class) { + description = "Create \"examples.zip\" containing all KeY examples" + destinationDirectory = layout.buildDirectory.dir("resources/main/").getOrNull() + archiveFileName = "examples.zip" + from("examples") + include(scanReadmeFiles()) // see end of file +} + +tasks.processResources.get().dependsOn(createExamplesZip) + +tasks.shadowJar { + archiveClassifier.set("exe") + archiveBaseName.set("key") + mergeServiceFiles() +} + +tasks.distZip { + archiveBaseName.set("key") +} + +application { + mainClass.set("de.uka.ilkd.key.core.Main") +} + +tasks.run { + systemProperties["key.examples.dir"] = "$projectDir/examples" + //systemProperties["slf4j.detectLoggerNameMismatch"] = true + //systemProperties["KeyDebugFlag"] = "on" + //args "--experimental" + + // this can be used to solve a problem where the OS hangs during debugging of popup menus + // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425) + jvmArgs.add("-Dsun.awt.disablegrab=true") +} + +tasks.register("runWithProfiler") { + group = "application" + description = """Run key.ui with flight recoder enabled. + See https://www.baeldung.com/java-flight-recorder-monitoring for a how to.""" + + classpath = sourceSets["main"].runtimeClasspath + mainClass.set("de.uka.ilkd.key.core.Main") + jvmArgs = listOf( + "-XX:+FlightRecorder", + "-XX:StartFlightRecording=duration=30s,filename=key_profile.jfr", + "-XX:FlightRecorderOptions=stackdepth=256" + ) + doLast { + println("A file key_profile.jfr has been created in folder 'key.ui' by JRE (FlightRecoder).") + println("You can open key_profile.jfr in IntelliJ to inspect the performance measurement.") + } +} + +/** + * Go and scan all registered README.txt files for files that need to be + * included into examples.zip. Thus only those files that can actually be + * accessed from the example browser are added to examples.zip. + * + * The file size is reduced considerably. + * + * @return a list of filenames to be added to examples.zip. Each line + * is relative to the examples directory. + */ +fun scanReadmeFiles(): List { + val REGEX_FILE = "file".toRegex(RegexOption.IGNORE_CASE) + val REGEX_EQ = "=".toRegex() + + val exampleDir = projectDir.toPath().resolve("examples") + val examplesIndex = exampleDir.resolve("index").resolve("samplesIndex.txt") + + val result = mutableListOf("index/samplesIndex.txt") + + for (line in examplesIndex.readLines()) { + val line = line.trim() + if (line.isEmpty() || line.startsWith("#")) { + continue + } + val entry = Paths.get(line.replace("/", File.separator)) + val readme = exampleDir.resolve(entry) + val dir = entry.parent + result.add(line) + + // The project file is not always project.key, but better include the default file. + result.add("$dir/project.key") + + for (rmLine in readme.readLines()) { + if (rmLine.startsWith("#") || "=" !in rmLine) continue + val (key, value) = rmLine.split(REGEX_EQ, 2) + if (key.trim().contains(REGEX_FILE)) { + val filename = value.trim() + result.add("$dir/$filename") + } + } + } + return result +} diff --git a/key.util/build.gradle b/key.util/build.gradle deleted file mode 100644 index cd0a45de4ae..00000000000 --- a/key.util/build.gradle +++ /dev/null @@ -1,21 +0,0 @@ -description = "Utility library of the key-project" - -dependencies { - implementation("org.jspecify:jspecify:1.0.0") -} - -checkerFramework { - if(System.getProperty("ENABLE_NULLNESS")) { - checkers = [ - "org.checkerframework.checker.nullness.NullnessChecker", - ] - extraJavacArgs = [ - "-AonlyDefs=^org\\.key_project\\.util", - "-Xmaxerrs", "10000", - "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub:checker.jar/junit-assertions.astub", - "-AstubNoWarnIfNotFound", - "-Werror", - "-Aversion", - ] - } -} diff --git a/key.util/build.gradle.kts b/key.util/build.gradle.kts new file mode 100644 index 00000000000..533442dbd7c --- /dev/null +++ b/key.util/build.gradle.kts @@ -0,0 +1,9 @@ +plugins { + id("java-convention") +} + +description = "Utility library of the key-project" + +dependencies {} + +extra["CHECKER_FRAMEWORK_PACKAGES_REGEX"] = "^org\\.key_project\\.util" diff --git a/keyext.caching/build.gradle b/keyext.caching/build.gradle deleted file mode 100644 index fc751b22881..00000000000 --- a/keyext.caching/build.gradle +++ /dev/null @@ -1,8 +0,0 @@ -description = "Caching of provable nodes to make proving with KeY faster." - -dependencies { - implementation project(":key.core") - implementation project(":key.ui") - - implementation project(":keyext.slicing") -} \ No newline at end of file diff --git a/keyext.caching/build.gradle.kts b/keyext.caching/build.gradle.kts new file mode 100644 index 00000000000..a11a506498f --- /dev/null +++ b/keyext.caching/build.gradle.kts @@ -0,0 +1,12 @@ +plugins { + id("java-convention") +} + +description = "Caching of provable nodes to make proving with KeY faster." + +dependencies { + implementation( project(":key.core")) + implementation (project(":key.ui")) + + implementation (project(":keyext.slicing")) +} \ No newline at end of file diff --git a/keyext.exploration/build.gradle b/keyext.exploration/build.gradle deleted file mode 100644 index aa1ba0d0641..00000000000 --- a/keyext.exploration/build.gradle +++ /dev/null @@ -1,6 +0,0 @@ -description = "Proof exploration capabilities for key.ui" - -dependencies { - implementation project(":key.core") - implementation project(":key.ui") -} \ No newline at end of file diff --git a/keyext.exploration/build.gradle.kts b/keyext.exploration/build.gradle.kts new file mode 100644 index 00000000000..56c870ed9d4 --- /dev/null +++ b/keyext.exploration/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-convention") +} + +description = "Proof exploration capabilities for key.ui" + +dependencies { + implementation( project(":key.core")) + implementation (project(":key.ui")) +} \ No newline at end of file diff --git a/keyext.isabelletranslation/build.gradle b/keyext.isabelletranslation/build.gradle deleted file mode 100644 index 42c2a1156c6..00000000000 --- a/keyext.isabelletranslation/build.gradle +++ /dev/null @@ -1,17 +0,0 @@ -description = "Translation of Sequents to Isabelle" - -dependencies { - implementation project(':key.core') - implementation project(':key.ui') - implementation("de.unruh:scala-isabelle_2.13:0.4.5") -} - -/* - scala-isabelle uses slf4j-simple. As KeY is currently using logback, this would result in two slf4j providers. - The code below excludes this module, thereby causing a fallback to logback. - - ! If KeY switches to slf4j-simple, this code needs to be removed ! - */ -configurations.configureEach { - exclude group: 'org.slf4j', module: 'slf4j-simple' -} \ No newline at end of file diff --git a/keyext.isabelletranslation/build.gradle.kts b/keyext.isabelletranslation/build.gradle.kts new file mode 100644 index 00000000000..787485ce3ff --- /dev/null +++ b/keyext.isabelletranslation/build.gradle.kts @@ -0,0 +1,18 @@ +plugins { + id("java-convention") +} + +description = "Translation of Sequents to Isabelle" + +dependencies { + implementation(project(":key.core")) + implementation(project(":key.ui")) + implementation("de.unruh:scala-isabelle_2.13:0.4.3") { + /* + scala-isabelle uses slf4j-simple. As KeY is currently using logback, this would result in two slf4j providers. + The code below excludes this module, thereby causing a fallback to logback. + */ + exclude("org.slf4j:slf4j-simple") + } +} + diff --git a/keyext.proofmanagement/build.gradle b/keyext.proofmanagement/build.gradle.kts similarity index 73% rename from keyext.proofmanagement/build.gradle rename to keyext.proofmanagement/build.gradle.kts index 2b1cbd3ce07..4d32cff80ff 100644 --- a/keyext.proofmanagement/build.gradle +++ b/keyext.proofmanagement/build.gradle.kts @@ -1,16 +1,16 @@ plugins { - id 'application' - id 'com.gradleup.shadow' version "9.3.2" + id("java-convention") + application + id("com.gradleup.shadow") } description = "Management of larger verification with KeY." dependencies { - implementation project(':key.core') - implementation project(':key.ui') + implementation(project(":key.core")) + implementation(project(":key.ui")) - implementation group: 'org.antlr', name: 'ST4', version: '4.3.4' - implementation("info.picocli:picocli:4.7.7") + implementation(libs.stringtemplate) } application { @@ -19,7 +19,7 @@ application { applicationName = "pm" } -run { +tasks.run { // for debugging, something like this can be used: //args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency', 'pmexample2') //args('merge', 'bundle1', 'bundle2.zip', 'output.zproof') @@ -29,7 +29,7 @@ run { // jvmArgs += ['--add-opens', 'java.base/java.util=ALL-UNNAMED'] } -shadowJar { +tasks.shadowJar { archiveClassifier = "exe" archiveBaseName = "keyext.proofmanagement" } diff --git a/keyext.slicing/build.gradle b/keyext.slicing/build.gradle deleted file mode 100644 index 00b33e93830..00000000000 --- a/keyext.slicing/build.gradle +++ /dev/null @@ -1,8 +0,0 @@ -description = "Proof slicing (removing of unnecessary nodes) for the KeY system." - - -dependencies { - implementation project(":key.core") - implementation project(":key.ui") - implementation("info.picocli:picocli:4.7.7") -} \ No newline at end of file diff --git a/keyext.slicing/build.gradle.kts b/keyext.slicing/build.gradle.kts new file mode 100644 index 00000000000..07e618aa363 --- /dev/null +++ b/keyext.slicing/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-convention") +} + +description = "Proof slicing (removing of unnecessary nodes) for the KeY system." + +dependencies { + implementation (project(":key.core")) + implementation (project(":key.ui")) +} \ No newline at end of file diff --git a/keyext.ui.testgen/build.gradle b/keyext.ui.testgen/build.gradle deleted file mode 100644 index 3412fe69f59..00000000000 --- a/keyext.ui.testgen/build.gradle +++ /dev/null @@ -1,7 +0,0 @@ -description = "Extension for key.ui to access the Test Case Generation graphically" - -dependencies { - implementation project(":key.ui") - implementation project(":key.core") - implementation project(":key.core.testgen") -} \ No newline at end of file diff --git a/keyext.ui.testgen/build.gradle.kts b/keyext.ui.testgen/build.gradle.kts new file mode 100644 index 00000000000..26bcdde9e9d --- /dev/null +++ b/keyext.ui.testgen/build.gradle.kts @@ -0,0 +1,11 @@ +plugins { + id("java-convention") +} + +description = "Extension for key.ui to access the Test Case Generation graphically" + +dependencies { + implementation (project(":key.ui")) + implementation (project(":key.core")) + implementation (project(":key.core.testgen")) +} \ No newline at end of file diff --git a/recoder/build.gradle b/recoder/build.gradle deleted file mode 100644 index 5f96e9b0f9e..00000000000 --- a/recoder/build.gradle +++ /dev/null @@ -1,12 +0,0 @@ -description = "Fork of the Recoder -- a parser/ast for Java with extensions for KeY-Java dialects." - -def headerFile = "$rootDir/gradle/header-recoder" -repositories { - mavenCentral() -} -dependencies { - implementation 'org.ow2.asm:asm:9.9.1' - implementation 'org.apache-extras.beanshell:bsh:2.0b6' - implementation 'net.sf.retrotranslator:retrotranslator-runtime:1.2.9' - implementation 'net.sf.retrotranslator:retrotranslator-transformer:1.2.9' -} \ No newline at end of file diff --git a/recoder/build.gradle.kts b/recoder/build.gradle.kts new file mode 100644 index 00000000000..a94289a2b25 --- /dev/null +++ b/recoder/build.gradle.kts @@ -0,0 +1,10 @@ +plugins { + id("java-convention") +} + +description = "Fork of the Recoder -- a parser/ast for Java with extensions for KeY-Java dialects." + + +dependencies { + implementation (libs.bundles.recoder) +} \ No newline at end of file diff --git a/settings.gradle b/settings.gradle deleted file mode 100644 index b1ff8b8011b..00000000000 --- a/settings.gradle +++ /dev/null @@ -1,36 +0,0 @@ -plugins { - id("org.gradle.toolchains.foojay-resolver-convention").version("1.0.0") -} - -include "recoder" - -include "key.util" -include "key.ncore" -include 'key.ncore.calculus' - -include "key.core" -include "key.core.rifl" -include "key.core.infflow" -include "key.core.wd" -include "key.core.symbolic_execution" -include "key.core.testgen" -include "key.core.proof_references" - -include "key.core.example" -include "key.core.symbolic_execution.example" - -include "key.ui" - -include "key.removegenerics" - -include "keyext.ui.testgen" -include "keyext.proofmanagement" -include "keyext.exploration" -include "keyext.slicing" -include "keyext.caching" -include "keyext.isabelletranslation" - -// ENABLE NULLNESS here or on the CLI -// This flag is activated to enable the checker framework. -// System.setProperty("ENABLE_NULLNESS", "true") - diff --git a/settings.gradle.kts b/settings.gradle.kts new file mode 100644 index 00000000000..edfc8aaad12 --- /dev/null +++ b/settings.gradle.kts @@ -0,0 +1,37 @@ +plugins { + id("org.gradle.toolchains.foojay-resolver-convention").version("1.0.0") + //id("com.gradle.develocity").version("4.1") +} + +include("key.util") +include("recoder") + +include("key.ncore") +include("key.ncore.calculus") + +include("key.core") +include("key.core.rifl") +include("key.core.infflow") +include("key.core.wd") +include("key.core.symbolic_execution") +include("key.core.testgen") +include("key.removegenerics") +include("key.core.proof_references") + +include("key.core.example") +include("key.core.symbolic_execution.example") + + +include("key.ui") + +include("keyext.ui.testgen") +include("keyext.proofmanagement") +include("keyext.exploration") +include("keyext.slicing") +include("keyext.caching") +include("keyext.isabelletranslation") + +// ENABLE NULLNESS here or on the CLI +// This flag is activated to enable the checker framework. +// System.setProperty("ENABLE_NULLNESS", "true") +