diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 307df8f9b20..a21df76293a 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -35,3 +35,46 @@ jobs: cache: 'gradle' - name: Build with Gradle run: ./gradlew --parallel --continue spotlessCheck + + checkstyle: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + ref: ${{ github.event.pull_request.head.sha }} + + - uses: actions/setup-java@v4 + with: + distribution: 'corretto' + java-version: '21' + cache: 'gradle' + + - run: git merge-base HEAD origin/main + - run: git diff -U0 $(git merge-base HEAD origin/main) + + - name: Build with Gradle + run: ./gradlew --parallel --continue checkstyleMain + + - name: Merge sarif files into single file. + run: | + ./gradlew --parallel --continue sarifCopy + ls build/sarif-results/* + if: (success() || failure()) + + - name: "Job summary" + run: "cat */build/reports/checkstyle/main.md >> $GITHUB_STEP_SUMMARY" + if: (success() || failure()) + + - name: Upload checkstyle report + uses: actions/upload-artifact@v4 + if: (success() || failure()) + with: + name: checkstyle-report + path: "**/build/reports/checkstyle/main.html" + + - name: "Publish in Github code scanning" + uses: github/codeql-action/upload-sarif@v3 + if: (success() || failure()) + with: + sarif_file: "build/sarif-results/checkstyle.sarif" diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 554a2a61109..e773eef05df 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -72,6 +72,12 @@ jobs: - name: Upload coverage reports to Codecov uses: codecov/codecov-action@v5 + if: (success() || failure()) + + - name: JUnit into Github Annotations + run: ./gradlew junitAsAnnotations + if: (success() || failure()) + integration-tests: env: @@ -110,3 +116,9 @@ jobs: **/build/test-results/*/*.xml key.core/build/reports/runallproofs/* **/build/reports/ + + - name: JUnit into Github Annotations + run: ./gradlew junitAsAnnotations + if: (success() || failure()) + + diff --git a/build.gradle b/build.gradle index d7745aa8613..52611b07e0f 100644 --- a/build.gradle +++ b/build.gradle @@ -1,5 +1,3 @@ -import groovy.transform.Memoized - plugins { //Support for IntelliJ IDEA //https://docs.gradle.org/current/userguide/idea_plugin.html @@ -19,14 +17,8 @@ plugins { id "org.checkerframework" version "0.6.60" id("org.sonarqube") version "7.0.1.6134" -} -sonar { - properties { - property "sonar.projectKey", "KeYProject_key" - property "sonar.organization", "keyproject" - property "sonar.host.url", "https://sonarcloud.io" - } + id("checkstyle") } @@ -48,6 +40,11 @@ def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMB group = "org.key-project" version = "2.12.4$build" + +repositories { + mavenCentral() +} + subprojects { apply plugin: "java" apply plugin: "java-library" @@ -59,11 +56,15 @@ subprojects { apply plugin: "com.diffplug.spotless" apply plugin: "checkstyle" apply plugin: "pmd" + apply plugin: 'jacoco' apply plugin: "org.checkerframework" group = rootProject.group version = rootProject.version + //conditionally enable jacoco coverage when `-DjacocoEnabled=true` is given on CLI. + def jacocoEnabled = (System.properties.getProperty("jacocoEnabled") ?: "false") == "true" + java { sourceCompatibility = 21 targetCompatibility = 21 @@ -72,7 +73,8 @@ subprojects { repositories { mavenCentral() maven { - url = 'https://git.key-project.org/api/v4/projects/35/packages/maven' + url = "https://git.key-project.org/api/v4/projects/35/packages/maven" + allowInsecureProtocol=true } } @@ -96,11 +98,11 @@ subprojects { testImplementation("ch.qos.logback:logback-classic:1.5.20") testImplementation(platform("org.junit:junit-bom:5.14.1")) - testImplementation ("org.junit.jupiter:junit-jupiter-api") - 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.junit.jupiter:junit-jupiter-api") + 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.6") testImplementation project(':key.util') @@ -109,16 +111,23 @@ subprojects { testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.20.1") testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.14.1' + + //checkstyle extensions + checkstyle("org.key-project.devel:checkstyle-key-extensions:1.17-SNAPSHOT") + checkstyle("com.puppycrawl.tools:checkstyle:10.26.1") + + //def checkstyle = configurations.getByName("checkstyle") + //println(checkstyle.resolve()) } - tasks.withType(JavaCompile) { + 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) { + tasks.withType(Javadoc).configureEach { failOnError = false options.addBooleanOption 'Xdoclint:none', true //options.verbose() @@ -130,7 +139,6 @@ subprojects { 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" @@ -176,6 +184,10 @@ subprojects { outputs.upToDateWhen { false } showStandardStreams = true } + + jacoco { + enabled = jacocoEnabled + } } tasks.register('testFast', Test) { @@ -199,6 +211,10 @@ subprojects { // by assigning only 'failed' and 'skipped' events info.events = ["failed", "skipped"] } + + jacoco { + enabled = jacocoEnabled + } } // The following two tasks can be used to execute main methods from the project @@ -218,74 +234,31 @@ subprojects { classpath = sourceSets.test.runtimeClasspath } - // findbugs { findbugsTest.enabled = false; ignoreFailures = true } - pmd { - pmdTest.enabled = false - ignoreFailures = true - toolVersion = "7.10.0" - consoleOutput = false - rulesMinimumPriority = 5 - ruleSets = ["category/java/errorprone.xml", "category/java/bestpractices.xml"] - } - - tasks.register('pmdMainChanged', Pmd) { - // Specify all files that should be checked - def changedFiles = getChangedFiles() - source pmdMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles } - classpath = checkstyleMain.classpath - reports { - html { - required = true - outputLocation = file("build/reports/pmd/main_diff.html") - } - xml { - required = true - outputLocation = file("build/reports/pmd/main_diff.xml") - } - } - } - - checkstyle { toolVersion = "10.26.0" ignoreFailures = true configFile = file("$rootDir/gradle/key_checks.xml") - showViolations = false // disable console output + showViolations = true // disable console output + configProperties.put("home.dir", rootDir.absoluteFile) + configProperties.put("GitDiff.debug", "true") } + tasks.withType(Checkstyle).configureEach { + ignoreFailures = false + maxWarnings = 0 - tasks.register('checkstyleMainChanged', Checkstyle) { - // Specify all files that should be checked - def changedFiles = getChangedFiles() - source checkstyleMain.source.filter { f -> f.getAbsoluteFile().toString() in changedFiles } - classpath = checkstyleMain.classpath - - //println(source.getFiles()) - - // Define the output folder of the generated reports reports { - html { - required = true - outputLocation = file("build/reports/checkstyle/main_diff.html") - } - xml { - required = true - outputLocation = file("build/reports/checkstyle/main_diff.xml") - } + xml.required = true + html.required = true + //html.stylesheet = resources.text.fromFile('gradle/checkstyle-custom.xsl') + sarif.required = true } - } - - // tasks.withType(FindBugs) { - // reports { - // xml.enabled = false - // html.enabled = true - // } - // } - tasks.withType(Pmd) { - reports { - xml.getRequired().set(true) - html.getRequired().set(true) + finalizedBy { + def inputXml = layout.buildDirectory.dir("reports/checkstyle/main.xml").get().asFile.toPath() + def outputMd = layout.buildDirectory.dir("reports/checkstyle/main.md").get().asFile.toPath() + CheckstyleMarkdownReport.report(inputXml, outputMd, projectDir.toPath()) + logger.lifecycle("Create checkstyle markdown report: $outputMd") } } @@ -313,6 +286,23 @@ subprojects { } } + jacoco { + toolVersion = '0.8.12' + } + + jacocoTestReport { + reports { + html.required = true + html.outputLocation = layout.buildDirectory.dir('jacocoHtml') + xml.required = true + csv.required = false + } + } + + test.finalizedBy jacocoTestReport + testFast.finalizedBy jacocoTestReport + + spotless { // see https://github.com/diffplug/spotless/tree/main/plugin-gradle @@ -376,19 +366,6 @@ subprojects { } } -// checkerFramework { -// checkers = [ -// "org.checkerframework.checker.nullness.NullnessChecker", -// ] -// extraJavacArgs = [ -// "-AonlyDefs=^org\\.key_project\\.util", -// "-Xmaxerrs", "10000", -// "-Astubs=$projectDir/src/main/checkerframework", -// "-Werror", -// "-Aversion", -// ] -// } - afterEvaluate { // required so project.description is non-null as set by sub build.gradle publishing { publications { @@ -495,6 +472,13 @@ tasks.register('start'){ } } +checkstyle { + toolVersion = "10.21.1" // will be ignored + ignoreFailures = true + configFile file("$rootDir/gradle/key_checks.xml") + showViolations = false +} + // Generation of a JavaDoc across sub projects. tasks.register('alldoc', Javadoc){ group = "documentation" @@ -521,8 +505,6 @@ tasks.register('alldoc', Javadoc){ bottom = "Copyright © 2003-2023 The KeY-Project." use = true links += "https://docs.oracle.com/en/java/javase/17/docs/api/" - links += "http://www.antlr2.org/javadoc/" - links += "http://www.antlr3.org/api/Java/" links += "https://www.antlr.org/api/Java/" } } @@ -536,33 +518,23 @@ tasks.register('alldocJar', 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") -} - -@Memoized -def getChangedFiles() { - // Get the target and source branch - def anchor = "git merge-base HEAD origin/main".execute().getText() +tasks.register('sarifCopy', SarifJoiner) { + def source = + files(fileTree(dir: '.').matching { include "*/build/reports/checkstyle/main.sarif" }) + sarifFiles = source + outputFile.set(layout.buildDirectory.file("sarif-results/checkstyle.sarif")) +} - // Get list of all changed files including status - def allFiles = "git diff --name-status --diff-filter=dr $anchor".execute().getText().split("\n") - //println("Found ${allFiles.length} changed files") +tasks.register("junitAsAnnotations") { + def source = files(fileTree(dir: '.').matching { + include "*/build/test-results/test/TEST-*xml" } + ) + inputs.files(source) - // Remove the status prefix - def files = new TreeSet() - for (file in allFiles) { - if (file.length() > 1) { - def a = file.substring(1).trim() - if (!a.isBlank()) { - files.add(("$rootDir/" + a).toString()) - } + doLast { + source.asList().forEach { + JUnitGithubAnnotations.readAndPrint(it.toPath()) } } - // Return the list of touched files - files -} +} \ No newline at end of file diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts new file mode 100644 index 00000000000..a8fa1777d33 --- /dev/null +++ b/buildSrc/build.gradle.kts @@ -0,0 +1,18 @@ +import org.gradle.kotlin.dsl.plugins + +plugins { + `kotlin-dsl` +} + +repositories { + mavenCentral() + gradlePluginPortal() +} + +kotlin { + //jvmToolchain(21) +} + +dependencies { + implementation("org.jetbrains.kotlin:kotlin-gradle-plugin:2.2.0") +} \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/CheckstyleMarkdownReport.kt b/buildSrc/src/main/kotlin/CheckstyleMarkdownReport.kt new file mode 100644 index 00000000000..7589f07f982 --- /dev/null +++ b/buildSrc/src/main/kotlin/CheckstyleMarkdownReport.kt @@ -0,0 +1,49 @@ +import org.w3c.dom.Element +import java.io.PrintWriter +import java.nio.file.Path +import java.nio.file.Paths +import javax.xml.parsers.DocumentBuilderFactory +import kotlin.io.path.exists + +object CheckstyleMarkdownReport { + @JvmStatic + fun report(xmlFile: Path, targetFile: Path, projectDir: Path) { + if (!xmlFile.exists()) return + + // get variables either from the environment + val sha = System.getenv("GITHUB_SHA") ?: "main" + val host = System.getenv("GITHUB_SERVER_URL") ?: "https://github.com" + val repo = System.getenv("GITHUB_REPOSITORY") ?: "keyproject/key" + val baseUrl = "$host/$repo/blob/$sha" + + val docBuilder = DocumentBuilderFactory.newInstance().newDocumentBuilder() + val doc = docBuilder.parse(xmlFile.toFile()) + doc.documentElement.normalize() + + PrintWriter(targetFile.toFile()).use { out -> + out.write("\n\n") + + val files = doc.getElementsByTagName("file") + for (i in 0 until files.length) { + val fileNode = files.item(i) as Element + val filePath = Paths.get(fileNode.getAttribute("name")) + //val relativePath = projectDir.relativize(filePath).toString() + val url = "$baseUrl/$filePath".replace("\\", "/") + + out.write("#### $filePath\n\n") + + val errors = fileNode.getElementsByTagName("error") + for (j in 0 until errors.length) { + val error = errors.item(j) as Element + val severity = error.getAttribute("severity") + val message = error.getAttribute("message") + val line = error.getAttribute("line") + val column = error.getAttribute("column") + out.write("\n* $severity `$message` [@$line:$column]($url#L$line)") + } + + out.write("\n\nGenerated by buildSrc/src/main/kotlin/CheckstyleMarkdownReport.kt") + } + } + } +} \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/JUnitGithubAnnotations.kt b/buildSrc/src/main/kotlin/JUnitGithubAnnotations.kt new file mode 100644 index 00000000000..5d6c883a719 --- /dev/null +++ b/buildSrc/src/main/kotlin/JUnitGithubAnnotations.kt @@ -0,0 +1,65 @@ +import org.w3c.dom.NodeList +import java.nio.file.Path +import javax.xml.parsers.DocumentBuilderFactory +import javax.xml.xpath.XPathConstants +import javax.xml.xpath.XPathFactory +import kotlin.io.path.extension +import kotlin.io.path.name +import kotlin.io.path.walk + + +/** + * Provides utility functions to parse JUnit XML test reports and print annotations understood by GitHub Actions + * workflow for failed test cases. This helps surface test failures directly + * in the GitHub Actions UI by generating error annotations with relevant file and test information. + */ +@kotlin.io.path.ExperimentalPathApi +object JUnitGithubAnnotations { + private val xqryTestcase by lazy { + val xPath = XPathFactory.newInstance().newXPath() + val expression = "/testsuite/testcase[./failure]" + xPath.compile(expression) + } + + private val xqryFailureMessage by lazy { + val xPath = XPathFactory.newInstance().newXPath() + val expression = "./failure/@message" + xPath.compile(expression) + } + + @JvmStatic + fun readAndPrint(f: Path) { + val builder = DocumentBuilderFactory.newInstance().newDocumentBuilder() + val doc = builder.parse(f.toFile()) + val nodeList = xqryTestcase.evaluate(doc, XPathConstants.NODESET) as NodeList + + if (nodeList.length <= 0) { + return + } + + + // module name assuming /build/test-results/test/.xml + val base = f.parent.parent.parent.parent.name + for (i in 0 until nodeList.length) { + val node = nodeList.item(i) + // failure in test case + val failure = xqryFailureMessage.evaluate(node, XPathConstants.STRING) as String? + val attributes = node.attributes + val caseName = attributes.getNamedItem("name").textContent + val classname = attributes.getNamedItem("classname").textContent + val filename = "$base/${classname.replace(".", "/")}.java" + val message = failure?.take(80) ?: "" + // ::error file={name},line={line},endLine={endLine}, ={title}::{message} + print("::error title=Testcase-missed,file=$filename::Test error in '$caseName' with '$message'") + } + } + + @JvmStatic + fun readAndPrintAll(root: Path) { + val reports = root.fileSystem.getPathMatcher("glob:TEST-*xml") + root.walk() + .filter { it.extension == "xml" } + .filter { reports.matches(it) } + .forEach { readAndPrint(it) } + } +} \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/SarifCombiner.kt b/buildSrc/src/main/kotlin/SarifCombiner.kt new file mode 100644 index 00000000000..011f89d7cbc --- /dev/null +++ b/buildSrc/src/main/kotlin/SarifCombiner.kt @@ -0,0 +1,63 @@ +import org.gradle.api.DefaultTask +import org.gradle.api.file.FileCollection +import org.gradle.api.file.RegularFileProperty +import org.gradle.api.provider.Property +import org.gradle.api.tasks.InputFiles +import org.gradle.api.tasks.OutputFile +import org.gradle.api.tasks.TaskAction +import org.jetbrains.kotlin.com.google.gson.Gson +import org.jetbrains.kotlin.com.google.gson.GsonBuilder +import org.jetbrains.kotlin.com.google.gson.JsonElement +import java.io.File + +/** + * Utility class for combining multiple SARIF (Static Analysis Results Interchange Format) files. + * + * This class provides a method to merge SARIF reports, which are commonly used for aggregating + * static analysis results from different tools or runs into a single report. + * + * The implementation has no deep understanding of the SARIF format and simply merges the `results` field. + * Not applicable for multiple `run` or `tool` entries. + * + * @see SARIF Specification + */ +/** */ +private val JsonElement.getResultsOfFirstRun + get() = asJsonObject.get("runs").asJsonArray.get(0).asJsonObject.get("results").asJsonArray + +abstract class SarifJoiner : DefaultTask() { + @get:InputFiles + abstract val sarifFiles: Property + + @get:OutputFile + abstract val outputFile: RegularFileProperty + + @TaskAction + fun run() { + val inputs = sarifFiles.get().files.toList() + if (inputs.isEmpty()) return + + val first = readSarif(inputs.first()) + val others = inputs.subList(1, inputs.size).map { readSarif(it) } + + for (map in others) { + first.getResultsOfFirstRun.addAll(map.getResultsOfFirstRun) + } + + writeSarif(outputFile.get().asFile, first) + } + + private fun writeSarif(out: File, first: JsonElement) { + out.bufferedWriter(Charsets.UTF_8).use { + gson.toJson(first, it) + } + } + + + private fun readSarif(first: File): JsonElement { + first.reader().use { + return gson.fromJson(it, JsonElement::class.java)!! + } + } +} +val gson: Gson = GsonBuilder().setPrettyPrinting().create() diff --git a/gradle/key_checks.xml b/gradle/key_checks.xml index 856de55ec15..fb9328b9cf6 100644 --- a/gradle/key_checks.xml +++ b/gradle/key_checks.xml @@ -1,7 +1,7 @@ + "-//Puppy Crawl//DTD Check Configuration 1.3//EN" + "http://www.puppycrawl.com/dtds/configuration_1_3.dtd"> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 2a84e188b85..2e1113280ef 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,6 +1,6 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-9.0.0-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-9.1.0-bin.zip networkTimeout=10000 validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME diff --git a/key.core/build.gradle b/key.core/build.gradle index df2ba408900..6a6e2842c77 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -107,9 +107,9 @@ tasks.register('generateSolverPropsList') { classes.dependsOn << generateSMTListings classes.dependsOn << generateSolverPropsList +spotlessJava.dependsOn(compileJavacc) - -tasks.withType(Test) { +tasks.withType(Test).configureEach { enableAssertions = true } @@ -118,7 +118,7 @@ tasks.register('testProveRules', Test) { description = 'Proves KeY taclet rules tagged as lemma' group = "verification" filter { includeTestsMatching "ProveRulesTest" } - //useJUnitPlatform() {includeTags "testProveRules" } + jacoco { enabled = false } } tasks.register('testRunAllFunProofs', Test) { @@ -127,6 +127,7 @@ tasks.register('testRunAllFunProofs', Test) { filter { includeTestsMatching "RunAllProofsFunctional" } + jacoco { enabled = false } } tasks.register('testRunAllInfProofs', Test) { @@ -135,6 +136,7 @@ tasks.register('testRunAllInfProofs', Test) { filter { includeTestsMatching "RunAllProofsInfFlow" } + jacoco { enabled = false } } @@ -144,6 +146,7 @@ tasks.register('testProveSMTLemmas', Test) { filter { includeTestsMatching "ProveSMTLemmasTest" } + jacoco { enabled = false } } // Run the tests for the new smt translation in strict mode @@ -155,6 +158,7 @@ tasks.register('testStrictSMT', Test) { filter { includeTestsMatching "MasterHandlerTest" } + jacoco { enabled = false } } //Generation of the three version files within the resources by executing `git'. @@ -182,7 +186,7 @@ tasks.register('generateVersionFiles') { static def gitRevParse(String args) { try { return "git rev-parse $args".execute().text.trim() - } catch (Exception e) { + } catch (Exception ignored) { return "" } } diff --git a/key.util/src/main/java/org/key_project/util/Filenames.java b/key.util/src/main/java/org/key_project/util/Filenames.java index bfbc5a340b8..b948191d5f4 100644 --- a/key.util/src/main/java/org/key_project/util/Filenames.java +++ b/key.util/src/main/java/org/key_project/util/Filenames.java @@ -8,6 +8,13 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl +// This class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImplThis class is only used by FunctionalOperationContractImpl /** * @author Alexander Weigl diff --git a/key.util/src/test/java/org/key_project/util/StringsTest.java b/key.util/src/test/java/org/key_project/util/StringsTest.java index 66e1a2260d8..5345c6b4785 100644 --- a/key.util/src/test/java/org/key_project/util/StringsTest.java +++ b/key.util/src/test/java/org/key_project/util/StringsTest.java @@ -14,6 +14,7 @@ class StringsTest { @Test void containsWholeWord() { + assert false; String[] sentences = { "asfKeY;prover", "KeY prover", diff --git a/scripts/jacocokey.gradle b/scripts/jacocokey.gradle deleted file mode 100644 index 8d33e46b844..00000000000 --- a/scripts/jacocokey.gradle +++ /dev/null @@ -1,29 +0,0 @@ -apply plugin: 'jacoco' - -jacoco { - toolVersion = '0.8.8' -} - -subprojects { - apply plugin: 'jacoco' - - jacocoTestReport { - reports { - html.required = false - xml.required = true - csv.required = false - } - } - - test { - finalizedBy jacocoTestReport - } - - - testFast { - finalizedBy jacocoTestReport - jacoco { - destinationFile = layout.buildDirectory.dir("jacoco/test.exec").get().getAsFile() - } - } -} diff --git a/scripts/tools/checkstyle/GitDiffFilter.java b/scripts/tools/checkstyle/GitDiffFilter.java deleted file mode 100644 index e35b009a93f..00000000000 --- a/scripts/tools/checkstyle/GitDiffFilter.java +++ /dev/null @@ -1,184 +0,0 @@ -import java.io.BufferedReader; -import java.io.File; -import java.io.FileReader; -import java.io.IOException; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import java.util.regex.Matcher; -import java.util.regex.Pattern; - -import com.puppycrawl.tools.checkstyle.api.AuditEvent; -import com.puppycrawl.tools.checkstyle.api.AutomaticBean; -import com.puppycrawl.tools.checkstyle.api.Filter; - -/** - * This class implements a checkstyle filter which filters all messages - * which correspond to lines which have been recently changed according - * to a git-diff file provided to the filter. - * - *

Diff file

- * The git-diff file must be provided and is not produced by the filter. - * You may create it using - * - *
git diff -U0 $MERGE_BASE > diffFile
- * - * For MERGE_BASE the assignment - * - *
MERGE_BASE=`git merge-base HEAD origin/main`
- * - * proved sensible if merging against the main branch. - * The diffFile can then be provided to the filter as - *
 <module name="GitDiffFilter">
- *   <property name="diffFilename" value="diffFile" />
- * </module>
- * - * @author Mattias Ulbrich - * @version 1 - * @since Mar 2017 - */ -public final class GitDiffFilter extends AutomaticBean implements Filter { - - private static class Interval { - private final int from; - private final int to; - private Interval(int from, int to) { - assert from > 0 && to >= from: from + "-" + to; - this.from = from; - this.to = to; - } - - public int compareTo(int val) { - if(val < from) { - return -1; - } else if(val > to) { - return +1; - } else { - return 0; - } - } - - @Override - public String toString() { - return "[" + from + ", " + to + "]"; - } - } - - private final Pattern FILENAME_PATTERN = Pattern.compile("\\+\\+\\+ b/(.*)"); - private final Pattern CHANGE_PATTERN = Pattern.compile("@@ -[^ ]+ \\+(\\d+)(?:,(\\d+))? @@.*"); - - private String diffFilename = null; - private String filenamePrefix = null; - private Map> changedLines = null; - - - public void setDiffFilename(String filename) { - this.diffFilename = filename; - } - - public void setFilenamePrefix(String prefix) { - this.filenamePrefix = prefix; - } - - @Override - public boolean accept(AuditEvent event) { - if(changedLines == null) { - computeChangedLines(); - } - - String filename; - filename = event.getFileName(); - // try { - // filename = new File(event.getFileName()).getAbsoluteFile().getCanonicalPath(); - // } catch (IOException e) { - // throw new RuntimeException(e); - // } - List intervals = changedLines.get(filename); - - if(intervals == null) { - return false; - } - - assert find(intervals, event.getLine()) == findSimple(intervals, event.getLine()); - - return find(intervals, event.getLine()); - } - - private void computeChangedLines() { - - Map> result = new HashMap>(); - - try(BufferedReader br = new BufferedReader(new FileReader(diffFilename))) { - - String filename = null; - String line; - while((line = br.readLine()) != null) { - Matcher m = FILENAME_PATTERN.matcher(line); - if(m.matches()) { - filename = m.group(1); - if(filenamePrefix != null) - filename = filenamePrefix + File.separator + filename; - // filename = new File(filename).getAbsoluteFile().getCanonicalPath(); - result.put(filename, new ArrayList()); - continue; - } - - m = CHANGE_PATTERN.matcher(line); - if(m.matches()) { - int from = Integer.parseInt(m.group(1)); - String toString = m.group(2); - int len = toString != null ? Integer.parseInt(toString) : 1; - - // store this interval only if it is not a deletion. - if(len > 0) { - if(filename == null) { - throw new RuntimeException(); - } - - List list = result.get(filename); - - list.add(new Interval(from, from+len-1)); - } - } - } - - } catch(IOException ioex) { - throw new RuntimeException(ioex); - } - - this.changedLines = result; - } - - private boolean find(List intervals, int value) { - int lo = 0; - int hi = intervals.size() - 1; - - while(lo <= hi) { - int mid = (lo+hi) >>> 1; - Interval midInterval = intervals.get(mid); - switch(midInterval.compareTo(value)) { - case -1: hi = mid-1; break; - case +1: lo = mid+1; break; - case 0: return true; - } - } - - return false; -// return intervals.get(lo).compareTo(value) == 0; - } - - // A comparison implementation to ensure binsearch works correctly - private boolean findSimple(List intervals, int value) { - for (Interval interval : intervals) { - if(interval.compareTo(value) == 0) { - return true; - } - } - return false; - } - - @Override - public void finishLocalSetup() { - } -} diff --git a/scripts/tools/checkstyle/NoEmbeddedPlusPlusCheck.java b/scripts/tools/checkstyle/NoEmbeddedPlusPlusCheck.java deleted file mode 100644 index 9860618b209..00000000000 --- a/scripts/tools/checkstyle/NoEmbeddedPlusPlusCheck.java +++ /dev/null @@ -1,146 +0,0 @@ -import java.util.BitSet; - -import com.puppycrawl.tools.checkstyle.api.AbstractCheck; -import com.puppycrawl.tools.checkstyle.api.DetailAST; -import com.puppycrawl.tools.checkstyle.api.TokenTypes; -import com.puppycrawl.tools.checkstyle.utils.TokenUtil; - -import static com.puppycrawl.tools.checkstyle.api.TokenTypes.*; - -/** - * This class implements a checkstyle rule which asserts that increment and - * decrement expressions do only occur as individual commands. - * - * This is meant to avoid rather unreadable code like - * - *
- *   for (int k = left; ++left <= right; k = ++left)
- * 
- * - * (taken from JDK's DualPivotQuicksort.java). - * - *

Check

- * - * The check scans all occurrences of pre- and postincrements and checks their - * parents and grandparents in the AST. First parent is checked (see - * "admissibleParents" in configuration below). If the parent is EXPR, then - * the grandparent AST type is also checked. - * - *

Configuration

- * - * The check can be configured from the style file as follows: - * - *
- *   <module name="NoEmbeddedPlusPlus">
- *     <property name="admissibleParents" value="EXPR"/>
- *     <property name="admissibleGrandParents"
- *                  value="SLIST, ELIST, LITERAL_WHILE,
- *                         LITERAL_FOR, LITERAL_IF"/>
- *     <message key="parent"
- *                 value="Unallowed increment/decrement operation."/>
- *     <message key="grandParent"
- *                 value="Unallowed increment/decrement operation."/>
- *   </module>
- * 
- * - * This lists also the default values. - * - * @author Mattias Ulbrich - * @version 1 - * @since May 2017 - */ -public class NoEmbeddedPlusPlusCheck extends AbstractCheck { - - private static final int[] DEFAULT_TOKENS = - { DEC, INC, POST_DEC, POST_INC }; - - private static final int[] ADMISSIBLE_PARENTS = - { EXPR }; - - private static final int[] ADMISSIBLE_GRAND_PARENTS = - { SLIST, ELIST, LITERAL_WHILE, LITERAL_FOR, LITERAL_IF }; - - private static final String DEFAULT_PARENT_MESSAGE = - "Unallowed increment/decrement operation."; - - private static final String DEFAULT_GRAND_PARENT_MESSAGE = - "Unallowed increment/decrement operation."; - - private BitSet admissibleParents = new BitSet(); - private BitSet admissibleGrandParents = new BitSet(); - private String parentMessage = DEFAULT_PARENT_MESSAGE; - private String grandParentMessage = DEFAULT_GRAND_PARENT_MESSAGE; - - public NoEmbeddedPlusPlusCheck() { - setBits(this.admissibleParents, ADMISSIBLE_PARENTS); - setBits(this.admissibleGrandParents, ADMISSIBLE_GRAND_PARENTS); - } - - private void setBits(BitSet bitset, int[] bits) { - for (int bit : bits) { - bitset.set(bit); - } - } - - @Override - public void visitToken(DetailAST ast) { - - DetailAST parent = ast.getParent(); - - if(parent != null) { - int id = parent.getType(); - if(!admissibleParents.get(id)) { - log(ast.getLineNo(), ast.getColumnNo(), - parentMessage); - } - - if(id == TokenTypes.EXPR) { - int gid = parent.getParent().getType(); - if(!admissibleGrandParents.get(gid)) { - log(ast.getLineNo(), ast.getColumnNo(), - grandParentMessage); - } - } - } - - } - - @Override - public int[] getDefaultTokens() { - return DEFAULT_TOKENS; - } - - public void setAdmissibleParents(String... parentTokens) { - admissibleParents.clear(); - for (int i = 0; i < parentTokens.length; i++) { - admissibleParents.set(TokenUtil.getTokenId(parentTokens[i])); - } - } - - public void setParentMessage(String parentMessage) { - this.parentMessage = parentMessage; - } - - public void setGrandAdmissibleParents(String... parentTokens) { - admissibleGrandParents.clear(); - for (int i = 0; i < parentTokens.length; i++) { - admissibleGrandParents.set(TokenUtil.getTokenId(parentTokens[i])); - } - } - - - public void setGrandParentMessage(String grandParentMessage) { - this.grandParentMessage = grandParentMessage; - } - - @Override - public int[] getRequiredTokens() { - return getDefaultTokens(); - } - - @Override - public int[] getAcceptableTokens() { - return getDefaultTokens(); - } - -} diff --git a/scripts/tools/checkstyle/checkstyle-10.6.0-all.jar b/scripts/tools/checkstyle/checkstyle-10.6.0-all.jar deleted file mode 100644 index 22bb2171aa1..00000000000 Binary files a/scripts/tools/checkstyle/checkstyle-10.6.0-all.jar and /dev/null differ diff --git a/scripts/tools/checkstyle/publishAudit.pl b/scripts/tools/checkstyle/publishAudit.pl deleted file mode 100755 index 52ae2eb952b..00000000000 --- a/scripts/tools/checkstyle/publishAudit.pl +++ /dev/null @@ -1,77 +0,0 @@ -#!/usr/bin/perl -w - - -# -# THIS PROGRAM IS OUTDATED. -# -# Please refer to the python program publishAudit.py -# composed by Alexander Weigl. -# -# - - - -# workflow: -# - runIncrementalCheckstyle.sh | tee report.txt -# - publishAudit.pl report.txt - -use LWP::UserAgent; -use Data::Dumper; -use HTTP::Request::Common; - -$rawReport = shift @ARGV; -$server = "https://git.key-project.org/"; -$url = $ENV{"CI_PROJECT_URL"}; -$pid = $ENV{"CI_PROJECT_ID"}; -$token = $ENV{"CI_COMMENT_TOKEN"}; -$sha = $ENV{"CI_COMMIT_SHA"}; -$bid = $ENV{"CI_BUILD_ID"}; - -open(my $raw, "<", $rawReport); -my $URL = "hhh"; -my %report = (); -while(<$raw>) { - - if(/\[(.*?)\] (.*\/(.*?)):(\d+)(?::\d+)?: (.*)/) { - $report{$1} .= "* [$3:$4](../blob/$sha/$2#L$4): $5\n"; - } -} -close($raw); - -sub report { - (my $type, my $msg) = @_; - - my $result = ""; - if($msg) { - $result .= "#" unless $type eq "ERROR"; # Errors have a larger heading ... - $result .= "## $type messages\n\n"; - $result .= $msg . "\n"; - } - return $result; -} - -my $note = "Checkstyle has been run on this commit in [job $bid]($url/builds/$bid). "; -$note .= "Here is its report:\n\n"; -if(%report) { - $note .= "
"; - $note .= &report("ERROR", $report{"ERROR"}); - $note .= &report("WARNING", $report{"WARN"}); - $note .= &report("INFO", $report{"INFO"}); - $note .= "
"; -} else { - $note .= "*No issues. Good.*"; -} - -my $ua = LWP::UserAgent->new(); -my $response = $ua->post( - "$server/api/v4/projects/$pid/repository/commits/$sha/comments", - { private_token => $token, note => $note }); -my $content = $response->as_string(); - -print Dumper($content); - -if($report{"ERROR"}) { - exit 1; -} else { - exit 0; -} diff --git a/scripts/tools/checkstyle/publishAudit.py b/scripts/tools/checkstyle/publishAudit.py deleted file mode 100755 index 3054bf2a9ac..00000000000 --- a/scripts/tools/checkstyle/publishAudit.py +++ /dev/null @@ -1,79 +0,0 @@ -#!/usr/bin/python3 - -import sys, os, re, urllib - -# workflow: -# - runIncrementalCheckstyle.sh | tee report.txt -# - publishAudit.py report.txt - -# The original was written in perl and is available under publishAudit.pl - -# Written by Alexander Weigl -# Refactored in May 2018, by Mattias Ulbrich - -def getenv(*args): - "relaxed access to environment" - return map(lambda x: os.environ.get(x, ""), args) - -rawReport = sys.argv[1] -SERVER = "https://git.key-project.org/" -URL, PID, TOKEN, SHA, BID, JID, MR_IID = getenv("CI_PROJECT_URL", "CI_PROJECT_ID", - "CI_COMMENT_TOKEN", "CI_COMMIT_SHA", - "CI_BUILD_ID", "CI_JOB_ID", "CI_MERGE_REQUEST_IID") - -everythingIsFine = True - -with open(rawReport) as raw: - report = {'ERROR':0, 'WARN':0, 'INFO':0} - - regex = re.compile(r'\[(?P.*?)\] (?P.*\/(?P.*?)):(?P\d+)(:\d+)?: (?P.*)') - - for line in raw: - m = regex.match(line) - if m: - everythingIsFine = False - old = report[m.group('level')] - report[m.group('level')] = old + 1 - -def r2s(header, count, red=False): - "report to string" - if count > 0: - markup = "**" if red else "" - return "- " + markup + str(count) + " " + header + markup + "\n" - else: - return "" - -if everythingIsFine: - note = """Checkstyle has been run on this commit in [job %s](%s/builds/%s). - *No issues. Good job* - """ % (BID, URL, BID) -else: - note = """Checkstyle has been run on this commit in [job %s](%s/builds/%s). - -It found the following issues: -%s - -Its report can be [downloaded here](%s/-/jobs/%s/artifacts/raw/report.txt). -*Please* resolve as many issues as possible before merging the code back into the master branch. -You can produce a report locally by executing `key/key/scripts/tools/checkstyle/runIncrementalCheckstyle.sh` in your local repository -""" % (BID, URL, BID, - r2s("ERROR messages", report['ERROR'], red=True) + - r2s("warning messages", report['WARN']) + - r2s("info messages", report['INFO']), - URL, BID) - -print(note) - -import requests -commitReportUrl = "%s/api/v4/projects/%s/repository/commits/%s/comments" % (SERVER,PID,SHA) -mergeRequestReportUrl = "%s/api/v4/projects/%s/merge_requests/%s/notes" %(SERVER, PID, MR_IID) - -if MR_IID != "": - reportUrl = mergeRequestReportUrl -else: - reportUrl = commitReportUrl - -print("Send report to", reportUrl) -resp = requests.post(reportUrl, data={ b'private_token': TOKEN, b'note':note }) -print(note) -sys.exit(int(bool(report["ERROR"]))) diff --git a/scripts/tools/checkstyle/runIncrementalCheckstyle.sh b/scripts/tools/checkstyle/runIncrementalCheckstyle.sh deleted file mode 100755 index 7047b2854cc..00000000000 --- a/scripts/tools/checkstyle/runIncrementalCheckstyle.sh +++ /dev/null @@ -1,43 +0,0 @@ -#!/usr/bin/env bash - -cd `dirname $0` - -HOME_DIR=`readlink -f ../../..` -DIFF_FILE=$HOME_DIR/checkstyle-diff.txt - -MERGE_BASE=`git merge-base HEAD origin/main` -OPTIONS="" - -javac -cp checkstyle-10.6.0-all.jar -d . -sourcepath $HOME_DIR \ - GitDiffFilter.java \ - NoEmbeddedPlusPlusCheck.java - -for arg in "$@" -do - case $arg in - --xml) - OPTIONS="-f xml " - ;; - - --base=*) - MERGE_BASE=${arg#*=} - ;; - - --out=*) - OPTIONS="-o ${arg#*=}" - esac -done - -git diff -U0 $MERGE_BASE > $DIFF_FILE - -# Uncomment the incremental check in the checkstyle configuration -sed -e 's//\1/' key_checks.xml > key_checks_incremental.xml - -java -ea -cp .:checkstyle-10.6.0-all.jar \ - -Dhome.dir=$HOME_DIR/ \ - -Ddiff.file=$DIFF_FILE \ - com.puppycrawl.tools.checkstyle.Main \ - -c key_checks_incremental.xml \ - $OPTIONS \ - $HOME_DIR/*/*/src/main/java \ - $HOME_DIR/*/src/main/java diff --git a/scripts/tools/checkstyle/translateAudit.py b/scripts/tools/checkstyle/translateAudit.py deleted file mode 100755 index cf4964e5978..00000000000 --- a/scripts/tools/checkstyle/translateAudit.py +++ /dev/null @@ -1,68 +0,0 @@ -#!/usr/bin/python3 - -import sys -import os -import re -import json - -from hashlib import sha224 - -# workflow: -# - runIncrementalCheckstyle.sh | tee report.txt -# - publishAudit.py report.txt - -# The original was written in perl and is available under publishAudit.pl - -# Written by Alexander Weigl -# Refactored in May 2018, by Mattias Ulbrich - -def getenv(*args): - "relaxed access to environment" - return map(lambda x: os.environ.get(x, ""), args) - - - -REGEX = re.compile(r'\[(?P.*?)\] (?P.*\/(?P.*?)):(?P\d+)(:\d+)?: (?P.*)') - -#info, minor, major, blocker,critical -LEVEL_TO_SEVERITY = { - 'INFO': 'info', - 'WARN': 'minor', - 'ERROR': 'major' -} - -def main(filename): - with open(filename) as raw: - statistics = {'ERROR':0, 'WARN':0, 'INFO':0} - reports = list() - - for line in raw: - m = REGEX.match(line) - if m: - old = statistics[m.group('level')] - statistics[m.group('level')] = old + 1 - - fingerprint = sha224(line.encode()).hexdigest() - - #see https://docs.gitlab.com/ee/user/project/merge_requests/code_quality.html#implementing-a-custom-tool - entry = { - 'description': m.group('msg'), - 'fingerprint': fingerprint, - 'severity': LEVEL_TO_SEVERITY[m.group('level')], - 'location.path': os.path.join(m.group('path'),m.group('file')), - 'location.lines.begin': m.group('line') - } - reports.append(entry) - - json.dump(reports, sys.stdout, indent=4) - - everythingIsFine = statistics['ERROR'] > 0 or statistics['WARN'] > 0 - - sys.exit(statistics["ERROR"]) - -###################################################### -if __name__=='__main__': - main(sys.argv[1]) - - -