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/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/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 768a3663e41..52b60ee2bf2 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -7,13 +7,13 @@ on: jobs: optional-tests: - continue-on-error: true + continue-on-error: false strategy: fail-fast: false matrix: os: [ubuntu-latest, windows-latest] java: [21] - tests: [":key.core.proof_references:test", ":key.core.symbolic_execution:test"] + name: ["proof_references", "symbolic_execution"] runs-on: ${{matrix.os}} steps: - uses: actions/checkout@v6 @@ -27,13 +27,13 @@ jobs: - name: Setup Gradle uses: gradle/actions/setup-gradle@v5 - name: Test with Gradle - run: ./gradlew --continue ${{ matrix.tests }} + run: ./gradlew --continue :key.core.${{ matrix.name }}:test - name: Upload test results uses: actions/upload-artifact@v6 if: success() || failure() with: - name: test-results-${{ matrix.tests }} + name: test-results-${{ matrix.os }}-${{ matrix.name }} path: | **/build/test-results/*/*.xml **/build/reports/ diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml new file mode 100644 index 00000000000..8b354e32090 --- /dev/null +++ b/.github/workflows/release-tests.yml @@ -0,0 +1,160 @@ +name: Broad Release Tests + +on: + workflow_dispatch: + schedule: + - cron: '0 5 5 * *' # every monday morning + +env: + z3: '4.13.4' # default z3 version + cvc5: '1.3.2' # default cvc5 version + +jobs: + unit-tests: + strategy: + fail-fast: false + matrix: + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21, 25 ] + continue-on-error: false + runs-on: ${{ matrix.os }} + env: + GH_TOKEN: ${{ github.token }} + steps: + - uses: actions/checkout@v6 + + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0 + with: + cvc5Version: ${{ env.cvc5 }} + z3Version: ${{ env.z3 }} + + - name: z3 version + run: z3 --version + + - name: cvc5 version + run: cvc5 --version + + - name: Setup Gradle + uses: + gradle/actions/setup-gradle@v5 + + - name: Assemble + run: ./gradlew --parallel assemble + + - name: Test mandatory modules with Gradle + run: ./gradlew test --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test + + - name: Test optional modules with Gradle + run: ./gradlew :key.core.symbolic_execution:test -x :key.core.proof_references:test + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() + with: + name: unit-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} + path: | + **/build/test-results/*/*.xml + **/build/reports/ + !**/jacocoTestReport.xml + + + integration-tests: + env: + GH_TOKEN: ${{ github.token }} + continue-on-error: false + strategy: + fail-fast: false + matrix: + test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testProveSMTLemmas ] + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21, 25 ] + z3: [ '4.15.4' ] + cvc5: [ '1.3.2' ] + + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0 + with: + cvc5Version: ${{ env.cvc5 }} + z3Version: ${{ env.z3 }} + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v5 + + - name: "Running tests: ${{ matrix.test }}" + run: ./gradlew --continue ${{ matrix.test }} + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() # run this step even if a previous step failed + with: + name: integration-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} + path: | + **/build/test-results/*/*.xml + key.core/build/reports/runallproofs/* + **/build/reports/ + !**/jacocoTestReport.xml + + + smt-tests: + env: + GH_TOKEN: ${{ github.token }} + continue-on-error: false + strategy: + fail-fast: false + matrix: + test: [ testProveSMTLemmas, testStrictSMT ] + os: [ macos-latest, ubuntu-latest, windows-latest ] + java: [ 21 ] + z3: [ '4.13.4', '4.14.1', '4.15.4' ] + cvc5: [ '1.3.2', '1.2.1' ] + runs-on: ${{ matrix.os }} + steps: + - uses: actions/checkout@v6 + - name: Set up JDK ${{matrix.java}} + uses: actions/setup-java@v5 + with: + java-version: ${{ matrix.java }} + distribution: 'temurin' + cache: 'gradle' + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0.3.0 + with: + cvc5Version: ${{ matrix.cvc5 }} + z3Version: ${{ matrix.z3 }} + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v5 + + - name: "Running tests" + run: ./gradlew :key.core:test --continue --tests 'de.uka.ilkd.key.smt.*' + + - name: Upload test results + uses: actions/upload-artifact@v6 + if: success() || failure() # run this step even if a previous step failed + with: + name: smt-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }}-${{matrix.z3}}-${{matrix.cvc5}} + path: | + **/build/test-results/*/*.xml + key.core/build/reports/runallproofs/* + **/build/reports/ + !**/jacocoTestReport.xml + diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 77c1268452f..4c70985f045 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -8,6 +8,7 @@ on: branches: - "main" - "KeY-*" + - "releases/*" merge_group: permissions: diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml deleted file mode 100644 index 497019b40e9..00000000000 --- a/.github/workflows/tests_winmac.yml +++ /dev/null @@ -1,98 +0,0 @@ -name: Broad Release Tests - -on: - workflow_dispatch: - schedule: - - cron: '0 5 * * 1' # every monday morning - -permissions: - checks: write - -jobs: - unit-tests: - strategy: - fail-fast: false - matrix: - os: [macos-latest, ubuntu-latest, windows-latest] - java: [21,23] - continue-on-error: true - runs-on: ${{ matrix.os }} - env: - GH_TOKEN: ${{ github.token }} - steps: - - uses: actions/checkout@v6 - - - name: Setup SMT solvers - uses: keyproject/setup-smt@v0 - - - name: z3 version - run: z3 --version - - - name: cvc5 version - run: cvc5 --version - - - - name: Set up JDK ${{matrix.java}} - uses: actions/setup-java@v5 - with: - java-version: ${{ matrix.java }} - distribution: 'corretto' - cache: 'gradle' - - - name: Setup Gradle - uses: - gradle/actions/setup-gradle@v5 - - name: Test with Gradle - run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test - - - name: Upload test results - uses: actions/upload-artifact@v6 - if: success() || failure() - with: - name: unit-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} - path: | - **/build/test-results/*/*.xml - **/build/reports/ - !**/jacocoTestReport.xml - - - integration-tests: - env: - GH_TOKEN: ${{ github.token }} - continue-on-error: true - strategy: - fail-fast: false - matrix: - test: [testProveRules, testRunAllFunProofs, testRunAllInfProofs] - os: [ macos-latest, ubuntu-latest, windows-latest ] - java: [21] - runs-on: ${{ matrix.os }} - steps: - - uses: actions/checkout@v6 - - - name: Setup SMT solvers - uses: keyproject/setup-smt@v0 - - - name: Set up JDK 21 - uses: actions/setup-java@v5 - with: - java-version: ${{ matrix.java }} - distribution: 'corretto' - cache: 'gradle' - - - name: Setup Gradle - uses: gradle/actions/setup-gradle@v5 - - name: "Running tests: ${{ matrix.test }}" - run: ./gradlew --continue ${{ matrix.test }} - - - name: Upload test results - uses: actions/upload-artifact@v6 - if: success() || failure() # run this step even if a previous step failed - with: - name: integration-test-results-${{matrix.test}}-${{ matrix.os }}-${{ matrix.java }} - path: | - **/build/test-results/*/*.xml - key.core/build/reports/runallproofs/* - **/build/reports/ - !**/jacocoTestReport.xml - diff --git a/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java b/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java index 0dd249414a0..d722ddd6765 100644 --- a/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java +++ b/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java @@ -312,6 +312,9 @@ protected void doProofFunctionTest(@Nullable Path baseDir, String javaPathInBase // representations ProofIndependentSettings.setUsePrettyPrinting(false); // Make sure that required files exists + if (javaPathInBaseDir.startsWith("/")) { + javaPathInBaseDir = javaPathInBaseDir.substring(1); + } Path javaFile = baseDir.resolve(javaPathInBaseDir); assertTrue(Files.exists(javaFile)); // Make sure that the correct taclet options are defined. @@ -385,6 +388,9 @@ protected void doProofMethodTest(@Nullable Path baseDir, String javaPathInBaseDi // representations ProofIndependentSettings.setUsePrettyPrinting(false); // Make sure that required files exists + if (javaPathInBaseDir.startsWith("/")) { + javaPathInBaseDir = javaPathInBaseDir.substring(1); + } Path javaFile = baseDir.resolve(javaPathInBaseDir); assertTrue(Files.exists(javaFile)); // Make sure that the correct taclet options are defined. diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java index 56933b36ff7..a0ca0e7f44f 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java @@ -1458,6 +1458,9 @@ protected static SymbolicExecutionEnvironment creat boolean usePrettyPrinting, boolean variablesAreOnlyComputedFromUpdates, boolean simplifyConditions) throws ProblemLoaderException, ProofInputException { // Make sure that required files exists + if (javaPathInBaseDir.startsWith("/")) { + javaPathInBaseDir = javaPathInBaseDir.substring(1); + } Path javaFile = baseDir.resolve(javaPathInBaseDir); assertTrue(Files.exists(javaFile)); // Load java file @@ -2049,6 +2052,9 @@ protected SymbolicExecutionEnvironment doSETTest(Pa assertNotNull(containerTypeName); assertNotNull(methodFullName); assertNotNull(oraclePathInBaseDirFile); + if (oraclePathInBaseDirFile.startsWith("/")) { + oraclePathInBaseDirFile = oraclePathInBaseDirFile.substring(1); + } var oracleFile = baseDir.resolve(oraclePathInBaseDirFile); if (!CREATE_NEW_ORACLE_FILES_IN_TEMP_DIRECTORY) { assertTrue(Files.exists(oracleFile), diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java index 52e96bf5b6f..588c875dc29 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java @@ -18,6 +18,7 @@ import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooser; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment; +import org.jspecify.annotations.NonNull; import org.junit.jupiter.api.*; import static org.junit.jupiter.api.Assertions.*; @@ -648,6 +649,9 @@ public void testAllNodeTypesTest_JavaProfile() throws Exception { */ protected void doJavaProfileTest(String proofFilePathInBaseDir, String oraclePathInBaseDirFile) throws Exception { + proofFilePathInBaseDir = cleanStartSlash(proofFilePathInBaseDir); + oraclePathInBaseDirFile = cleanStartSlash(oraclePathInBaseDirFile); + // Ensure that JavaProfile was used before KeYEnvironment env = KeYEnvironment.load(JavaProfile.getDefaultInstance(), testCaseDirectory.resolve(proofFilePathInBaseDir), null, null, null, true); @@ -662,6 +666,13 @@ protected void doJavaProfileTest(String proofFilePathInBaseDir, String oraclePat false); } + private static @NonNull String cleanStartSlash(String proofFilePathInBaseDir) { + if (proofFilePathInBaseDir.startsWith("/")) { + proofFilePathInBaseDir = proofFilePathInBaseDir.substring(1); + } + return proofFilePathInBaseDir; + } + /** * Tests example: /set/allNodeTypesTest in the Symbolic Execution Profile */ diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index b232446aea3..61bf4e12065 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -43,7 +43,7 @@ public class TestSymbolicExecutionUtil extends AbstractSymbolicExecutionTestCase @Test public void test1ImproveReadability() throws ProblemLoaderException { Path location = testCaseDirectory.resolve( - "/readability/InnerAndAnonymousTypeTest/InnerAndAnonymousTypeTest.java") + "readability/InnerAndAnonymousTypeTest/InnerAndAnonymousTypeTest.java") .toAbsolutePath(); assertTrue(Files.exists(location), "Could not find required resource: " + location);