diff --git a/.github/actions/docker-deploy/action.yml b/.github/actions/docker-deploy/action.yml index 20a57818f8..7e69cbca6e 100644 --- a/.github/actions/docker-deploy/action.yml +++ b/.github/actions/docker-deploy/action.yml @@ -5,26 +5,45 @@ inputs: required: true version: required: true + user-dockerhub: + required: true + user-ghcr: + required: true + push: + required: true runs: using: "composite" steps: - name: Checkout uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - - name: Extract metadata (tags, labels) for Docker - id: meta + - name: Extract metadata (tags, labels) for DockerHub + id: metaDH + uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e + with: + images: ${{ inputs.user-dockerhub }}/${{ inputs.project }} + tags: type:raw, value=${{ inputs.version }} + - name: Extract metadata (tags, labels) for ghcr.io + id: metaGH uses: docker/metadata-action@c4ee3adeed93b1fa6a762f209fb01608c1a22f1e with: - images: catshark2013/${{ inputs.project }} + images: ghcr.io/${{ inputs.user-ghcr }}/${{ inputs.project }} tags: type:raw, value=${{ inputs.version }} - name: Creating path id: 'path' shell: bash run: | echo "path=./docker/${{ inputs.project }}.Dockerfile" >> $GITHUB_OUTPUT - - name: Build and push + - name: Build and push to DockerHub + uses: docker/build-push-action@2eb1c1961a95fc15694676618e422e8ba1d63825 + with: + context: . + file: ${{ steps.path.outputs.path }} + push: ${{ inputs.push }} + tags: ${{ steps.metaDH.outputs.tags }} + - name: Build and push to ghcr.io uses: docker/build-push-action@2eb1c1961a95fc15694676618e422e8ba1d63825 with: context: . file: ${{ steps.path.outputs.path }} - push: true - tags: ${{ steps.meta.outputs.tags }} \ No newline at end of file + push: ${{ inputs.push }} + tags: ${{ steps.metaGH.outputs.tags }} diff --git a/.github/actions/docker-login/action.yml b/.github/actions/docker-login/action.yml index 5a06160ab1..0d6c82cc5a 100644 --- a/.github/actions/docker-login/action.yml +++ b/.github/actions/docker-login/action.yml @@ -1,18 +1,22 @@ -name: 'Login to DockerHub' -description: 'Login to DockerHub by using the secrets, and use it in reusable-workflow' +name: 'Login to a docker registry' +description: 'Login to a docker registry by using the secrets, and use it in reusable-workflow' inputs: token: required: true username: required: true + registry: + required: false runs: using: "composite" steps: - name: Checkout uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - - name: Login to Docker Hub + - name: Login to the Registry + if: inputs.username != '' uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a with: + registry: ${{ inputs.registry }} username: ${{ inputs.username }} password: ${{ inputs.token }} diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml index bc3843f1bd..8a36b9df12 100644 --- a/.github/workflows/linux-build-test-deploy.yml +++ b/.github/workflows/linux-build-test-deploy.yml @@ -109,8 +109,40 @@ jobs: PGP_KEY_ID: ${{ secrets.PGP_KEY_ID }} PGP_PWD: ${{ secrets.PGP_PWD }} + test-docker: + strategy: + matrix: + dockerprojects: ["theta-cfa-cli", "theta-sts-cli", "theta-xsts-cli", "theta-xta-cli"] + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 + - name: Version + id: version + run: | + echo version=$(./gradlew properties --no-daemon --console=plain -q | grep "^version:" | awk '{printf $2}') >> $GITHUB_OUTPUT + - name: docker-login + uses: ./.github/actions/docker-login + with: + username: ${{secrets.DOCKER_USERNAME}} + token: ${{secrets.DOCKER_TOKEN}} + - name: docker-login-ghcr + uses: ./.github/actions/docker-login + with: + registry: ghcr.io + username: ${{github.repository_owner}} + token: ${{secrets.GITHUB_TOKEN}} + - name: Build and publish docker file + uses: ./.github/actions/docker-deploy + with: + project: ${{ matrix.dockerprojects }} + version: ${{ steps.version.outputs.version }} + user-dockerhub: ftsrg + user-ghcr: ftsrg + push: false + deploy-docker: - needs: test-linux + needs: [test-linux, test-docker] if: "${{ github.event.inputs.message != '' && github.ref == 'refs/heads/master' && github.event_name != 'pull_request' }}" strategy: matrix: @@ -128,11 +160,26 @@ jobs: with: username: ${{secrets.DOCKER_USERNAME}} token: ${{secrets.DOCKER_TOKEN}} + - name: docker-login-ghcr + uses: ./.github/actions/docker-login + with: + registry: ghcr.io + username: ${{github.repository_owner}} + token: ${{secrets.GITHUB_TOKEN}} - name: Build and publish docker file uses: ./.github/actions/docker-deploy with: project: ${{ matrix.dockerprojects }} version: ${{ steps.version.outputs.version }} + user-dockerhub: ftsrg + user-ghcr: ftsrg + push: false + - name: Docker Hub Description update + uses: peter-evans/dockerhub-description@dc67fad7001ef9e8e3c124cb7a64e16d0a63d864 + with: + username: ${{ secrets.DOCKER_USERNAME }} + password: ${{ secrets.DOCKER_TOKEN }} + repository: ftsrg/${{ matrix.dockerprojects }} deploy-docs: runs-on: ubuntu-latest @@ -141,4 +188,4 @@ jobs: - name: Checkout repository uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - name: Deploy docs - uses: ./.github/actions/deploy-docs \ No newline at end of file + uses: ./.github/actions/deploy-docs diff --git a/.github/workflows/reapply_copyright.yml b/.github/workflows/reapply_copyright.yml index 519122bbbf..3acc9e3876 100644 --- a/.github/workflows/reapply_copyright.yml +++ b/.github/workflows/reapply_copyright.yml @@ -15,10 +15,17 @@ on: jobs: copyright_checker: runs-on: ubuntu-latest - steps: - - name: Checkout Repository + - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92 + id: generate-token + with: + app_id: ${{ secrets.APP_ID }} + private_key: ${{ secrets.APP_PRIVATE_KEY }} + + - name: Checkout repository uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 + with: + token: ${{ steps.generate-token.outputs.token }} - name: Run Copyright Checker shell: bash {0} @@ -56,9 +63,15 @@ jobs: commit-message: "Reapplied copyright" branch: "copyright-reapply" title: '[AutoPR] Reaplied copyright' + token: ${{ steps.generate-token.outputs.token }} + committer: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> + author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> - name: Commit changes if: ${{ inputs.direct-commit }} uses: stefanzweifel/git-auto-commit-action@3ea6ae190baf489ba007f7c92608f33ce20ef04a with: - commit_message: "Reapplied copyright" \ No newline at end of file + commit_message: "Reapplied copyright" + commit_user_name: ThetaBotMaintainer[bot] + commit_user_email: 139346997+ThetaBotMaintainer[bot]@users.noreply.github.com + commit_author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> \ No newline at end of file diff --git a/.github/workflows/reformat-code.yml b/.github/workflows/reformat-code.yml index b24baa37ed..d44f9931ba 100644 --- a/.github/workflows/reformat-code.yml +++ b/.github/workflows/reformat-code.yml @@ -16,8 +16,17 @@ jobs: reformat: runs-on: ubuntu-latest steps: + - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92 + id: generate-token + with: + app_id: ${{ secrets.APP_ID }} + private_key: ${{ secrets.APP_PRIVATE_KEY }} + - name: Checkout repository uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 + with: + token: ${{ steps.generate-token.outputs.token }} + - name: Do reformat uses: leventeBajczi/intellij-idea-format@v1.0 with: @@ -31,9 +40,15 @@ jobs: commit-message: "Reformatted code" branch: "code-reformat" title: '[AutoPR] Reformatted code' + token: ${{ steps.generate-token.outputs.token }} + committer: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> + author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> - name: Commit changes if: ${{ inputs.direct-commit }} uses: stefanzweifel/git-auto-commit-action@3ea6ae190baf489ba007f7c92608f33ce20ef04a with: - commit_message: "Reformatted code" \ No newline at end of file + commit_message: "Reformatted code" + commit_user_name: ThetaBotMaintainer[bot] + commit_user_email: 139346997+ThetaBotMaintainer[bot]@users.noreply.github.com + commit_author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> diff --git a/.github/workflows/version-bump.yml b/.github/workflows/version-bump.yml index 3a4062ff3f..ec8cf100e6 100644 --- a/.github/workflows/version-bump.yml +++ b/.github/workflows/version-bump.yml @@ -17,8 +17,16 @@ jobs: version-bump: runs-on: ubuntu-latest steps: + - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92 + id: generate-token + with: + app_id: ${{ secrets.APP_ID }} + private_key: ${{ secrets.APP_PRIVATE_KEY }} + - name: Checkout uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 + with: + token: ${{ steps.generate-token.outputs.token }} - name: Determine new version run: | @@ -42,3 +50,6 @@ jobs: with: commit_message: "Version bump" file_pattern: "build.gradle.kts" + commit_user_name: ThetaBotMaintainer[bot] + commit_user_email: 139346997+ThetaBotMaintainer[bot]@users.noreply.github.com + commit_author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> diff --git a/README.md b/README.md index acea32679a..7f91fd904a 100644 --- a/README.md +++ b/README.md @@ -38,6 +38,13 @@ Currently, the following tools are available (follow the links for more informat * [`theta-xcfa-cli`](subprojects/xcfa/xcfa-cli): Reachability checking of error locations in eXtended Control Flow Automata (XCFA) using CEGAR-based algorithms. The CFA formalism is extended with procedures and processes, able to support multithreaded analysis and also several optimization passes. Right now it is mainly used to check both single and multithreaded C programs. * the [`c-frontend`](subprojects/frontends/c-frontend) module of Theta is capable of parsing C programs and transforming them into a formalism independent, in-memory representation. The `xcfa-cli` is able to convert this representation into an XCFA. +To use Theta as a standalone tool, see the following deployments: + * [DockerHub](https://hub.docker.com/u/ftsrg) and [ghcr.io](https://github.com/orgs/ftsrg/packages) for Docker images based on the `*-cli` subprojects + * Latest [release](https://github.com/ftsrg/theta/releases/latest) for `.jar` files + +To use Theta as a library, see [Maven Central](https://central.sonatype.com/namespace/hu.bme.mit.theta). + + ## Overview of the architecture Theta can be divided into the following four layers. diff --git a/build.gradle.kts b/build.gradle.kts index fad2f7035f..0bfb8d1b81 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "4.4.2" + version = "4.4.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/doc/CI.md b/doc/CI.md index eb0e17835b..792efddecc 100644 --- a/doc/CI.md +++ b/doc/CI.md @@ -16,7 +16,7 @@ The `master` branch is protected, meaning direct pushes to the branch are forbid * SonarCloud check for code quality succeeds (see job `run-sonar` in [linux-build-test-deploy.yml](https://github.com/ftsrg/theta/actions/workflows/linux-build-test-deploy.yml)), including test coverage criteria (at least 60% of the new code) * Building and tests succeed for `ubuntu-latest` ([linux-build-test-deploy.yml](https://github.com/ftsrg/theta/actions/workflows/linux-build-test-deploy.yml)), `windows-latest` ([win-build-test.yml](https://github.com/ftsrg/theta/actions/workflows/win-build-test.yml)) and `macos-latest` ([mac-build-test.yml](https://github.com/ftsrg/theta/actions/workflows/mac-build-test.yml)). * Valid javadoc can be generated (`javadoc` in [linux-build-test-deploy.yml](https://github.com/ftsrg/theta/actions/workflows/linux-build-test-deploy.yml)) - * The version must be different to that of `master` ([check-version.yml](https://github.com/ftsrg/theta/actions/workflows/check-version.yml)). For an automated version bump, see[version-bump.yml](https://github.com/ftsrg/theta/actions/workflows/version-bump.yml). + * The version must be different to that of `master` ([check-version.yml](https://github.com/ftsrg/theta/actions/workflows/check-version.yml)). For an automated version bump, see [version-bump.yml](https://github.com/ftsrg/theta/actions/workflows/version-bump.yml). Administrators are allowed to bypass these rules, but are strongly encouraged _not to do so_. @@ -37,4 +37,4 @@ For a more-or-less stable user experience, binaries are generated at stable mile * DockerHub (docker images) * GitHub pages ([wiki](http://theta.mit.bme.hu/publications/wiki), [javadoc](http://theta.mit.bme.hu/javadoc), [publications](http://theta.mit.bme.hu/publications/)) -These steps are only run after being manually invoked via [linux-build-test-deploy.yml](https://github.com/ftsrg/theta/actions/workflows/linux-build-test-deploy.yml), and only over commits on the master branch. \ No newline at end of file +These steps are only run after being manually invoked via [linux-build-test-deploy.yml](https://github.com/ftsrg/theta/actions/workflows/linux-build-test-deploy.yml), and only over commits on the master branch.