SAWScript #2526
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Overall configuration notes: | |
| # - Artifact uploads for binaries are from GHC 8.10.7 | |
| # - Builds for Ubuntu happen on 22.04. We also include a single configuration | |
| # for 20.04 to increase our Linux coverage. | |
| # - Docker builds happen nightly, on manual invocation, and on release branch commits | |
| # Please update this comment as those details change. | |
| name: SAWScript | |
| on: | |
| push: | |
| tags: ["v?[0-9]+.[0-9]+(.[0-9]+)?"] | |
| branches: [master, "release-**"] | |
| pull_request: | |
| schedule: | |
| - cron: "0 10 * * *" # 10am UTC -> 2/3am PST | |
| workflow_dispatch: | |
| env: | |
| CACHE_VERSION: 1 | |
| DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc" | |
| # Solver package snapshot date - also update in the following locations: | |
| # ./saw/Dockerfile | |
| # ./saw-remote-api/Dockerfile | |
| # ./s2nTests/scripts/blst-entrypoint.sh | |
| # ./s2nTests/docker/saw.dockerfile | |
| SOLVER_PKG_VERSION: "snapshot-20221212" | |
| OCAML_VERSION: 4.09.x | |
| jobs: | |
| config: | |
| runs-on: ubuntu-22.04 | |
| outputs: | |
| name: ${{ steps.config.outputs.name }} | |
| version: ${{ steps.config.outputs.version }} | |
| event-tag: ${{ steps.config.outputs.tag }} | |
| event-schedule: ${{ steps.config.outputs.schedule }} | |
| publish: ${{ steps.config.outputs.publish }} | |
| release: ${{ steps.config.outputs.release }} | |
| retention-days: ${{ steps.config.outputs.retention-days }} | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| fetch-depth: 0 | |
| - name: config | |
| id: config | |
| env: | |
| EVENT_TAG: ${{ startsWith(github.event.ref, 'refs/tags/') }} | |
| EVENT_SCHEDULE: ${{ github.event_name == 'schedule' }} | |
| EVENT_DISPATCH: ${{ github.event_name == 'workflow_dispatch' }} | |
| RELEASE: ${{ startsWith(github.event.ref, 'refs/heads/release-') }} | |
| run: | | |
| set -x | |
| .github/ci.sh output name saw-$(.github/ci.sh ver) | |
| .github/ci.sh output version $(.github/ci.sh ver) | |
| .github/ci.sh output tag $EVENT_TAG | |
| .github/ci.sh output schedule $EVENT_SCHEDULE | |
| .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false) | |
| .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) | |
| .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5) | |
| build: | |
| runs-on: ${{ matrix.os }} | |
| needs: [config] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-22.04, macos-12, windows-latest] | |
| cabal: ["3.10.1.0"] | |
| ghc: ["8.8.4", "8.10.7", "9.2.7"] | |
| run-tests: [true] | |
| include: | |
| # We include one job from an older Ubuntu LTS release to increase our | |
| # coverage of possible Linux configurations. Since we already run the | |
| # tests with the newest LTS release, we won't bother testing this one. | |
| - os: ubuntu-20.04 | |
| ghc: "8.10.7" | |
| cabal: "3.10.1.0" | |
| run-tests: false | |
| exclude: | |
| # Exclude 8.8 on macOS 12 due to | |
| # https://gitlab.haskell.org/ghc/ghc/-/issues/18446 | |
| - os: macos-12 | |
| ghc: "8.8.4" | |
| cabal: "3.10.1.0" | |
| run-tests: true | |
| - os: windows-latest | |
| ghc: "8.8.4" | |
| cabal: "3.10.1.0" | |
| run-tests: true | |
| outputs: | |
| cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }} | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - run: | | |
| git submodule update --init | |
| - id: config | |
| shell: bash | |
| run: | | |
| NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64" | |
| .github/ci.sh output name $NAME | |
| echo "NAME=${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64" >> $GITHUB_ENV | |
| - uses: haskell/actions/setup@v1 | |
| id: setup-haskell | |
| with: | |
| ghc-version: ${{ matrix.ghc }} | |
| cabal-version: ${{ matrix.cabal }} | |
| - name: Post-GHC installation fixups on Windows | |
| shell: bash | |
| if: runner.os == 'Windows' | |
| run: | | |
| # A workaround for https://github.com/Mistuke/CabalChoco/issues/5 | |
| cabal user-config update -a "extra-include-dirs: \"\"" | |
| cabal user-config update -a "extra-lib-dirs: \"\"" | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| - uses: actions/cache/restore@v3 | |
| name: Restore cabal store cache | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} | |
| restore-keys: | | |
| ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- | |
| - if: needs.config.outputs.release == 'true' | |
| shell: bash | |
| run: | | |
| sed -i.bak \ | |
| -e 's/^hashText = .*$/hashText = ""/' \ | |
| -e '/import GitRev.*$/d' \ | |
| saw/SAWScript/Version.hs | |
| rm -f saw/SAWScript/Version.hs.bak | |
| - shell: bash | |
| run: .github/ci.sh build | |
| - shell: bash | |
| env: | |
| RELEASE: ${{ needs.config.outputs.release }} | |
| run: .github/ci.sh build_cryptol | |
| - uses: GaloisInc/.github/actions/cabal-collect-bins@v1.1.1 | |
| id: cabal-test-suites | |
| with: | |
| targets: | | |
| integration_tests | |
| test-sawcore | |
| cryptol-saw-core-tc-test | |
| prover_tests | |
| dest: dist-tests | |
| - uses: actions/upload-artifact@v2 | |
| if: "matrix.ghc == '8.10.7'" | |
| with: | |
| path: dist-tests | |
| name: dist-tests-${{ matrix.os }} | |
| - shell: bash | |
| run: .github/ci.sh setup_dist_bins | |
| - shell: bash | |
| run: .github/ci.sh bundle_files | |
| - shell: bash | |
| run: .github/ci.sh zip_dist $NAME | |
| - shell: bash | |
| run: .github/ci.sh zip_dist_with_solvers $NAME-with-solvers | |
| - if: matrix.ghc == '8.10.7' && github.event.pull_request.head.repo.fork == false | |
| shell: bash | |
| env: | |
| SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} | |
| SIGNING_KEY: ${{ secrets.SIGNING_KEY }} | |
| run: .github/ci.sh sign $NAME.tar.gz | |
| - if: matrix.ghc == '8.10.7' && github.event.pull_request.head.repo.fork == false | |
| shell: bash | |
| env: | |
| SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} | |
| SIGNING_KEY: ${{ secrets.SIGNING_KEY }} | |
| run: .github/ci.sh sign $NAME-with-solvers.tar.gz | |
| - if: matrix.ghc == '8.10.7' | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) | |
| path: "${{ steps.config.outputs.name }}.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - if: matrix.ghc == '8.10.7' | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) | |
| path: "${{ steps.config.outputs.name }}-with-solvers.tar.gz*" | |
| if-no-files-found: error | |
| retention-days: ${{ needs.config.outputs.retention-days }} | |
| - if: matrix.ghc == '8.10.7' && matrix.run-tests | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| path: dist/bin | |
| name: ${{ runner.os }}-bins | |
| - uses: actions/cache/save@v3 | |
| name: Save cabal store cache | |
| if: always() | |
| with: | |
| path: | | |
| ${{ steps.setup-haskell.outputs.cabal-store }} | |
| dist-newstyle | |
| key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} | |
| ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- | |
| mr-solver-tests: | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-22.04, macos-12] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: dist/bin | |
| - name: Update PATH to include SAW | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH | |
| - working-directory: examples/mr_solver | |
| shell: bash | |
| run: | | |
| saw monadify.saw | |
| saw mr_solver_unit_tests.saw | |
| heapster-tests: | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-22.04, macos-12] | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: dist/bin | |
| - name: Update PATH to include SAW | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH | |
| - uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: 4.14.x | |
| - run: opam repo add coq-released https://coq.inria.fr/opam/released | |
| - run: opam install -y coq=8.15.2 coq-bits=1.1.0 | |
| # If you change the entree-specs commit below, make sure you update the | |
| # documentation in saw-core-coq/README.md accordingly. | |
| - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb | |
| # FIXME: the following steps generate Coq libraries for the SAW core to | |
| # Coq translator and builds them; if we do other Coq tests, these steps | |
| # should become their own build artifact, to avoid re-compiling the Coq | |
| # libraries | |
| - working-directory: saw-core-coq/coq | |
| shell: bash | |
| run: opam exec -- make -j | |
| - working-directory: heapster-saw/examples | |
| shell: bash | |
| run: opam exec -- make -j | |
| saw-remote-api-tests: | |
| runs-on: ${{ matrix.os }} | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: Install and test | |
| test: saw-remote-api/scripts/run_rpc_tests.sh | |
| os: ubuntu-22.04 | |
| # TODO: saw-remote-api unit tests are disabled pending a fix for #1699 | |
| - name: Install on MacOS | |
| test: | | |
| cd saw-remote-api/python/ | |
| poetry update | |
| poetry install | |
| poetry run mypy --install-types --non-interactive saw_client/ || true | |
| poetry run mypy --install-types --non-interactive saw_client/ | |
| os: macos-12 | |
| - name: Check docs | |
| test: saw-remote-api/scripts/check_docs.sh | |
| os: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: dist/bin | |
| - uses: actions/setup-python@v2 | |
| with: | |
| python-version: '3.11' | |
| - uses: abatilo/actions-poetry@v2.0.0 | |
| with: | |
| poetry-version: 1.1.5 | |
| - name: ${{ matrix.name }} | |
| shell: bash | |
| run: | | |
| chmod +x dist/bin/* | |
| export PATH="$PWD/dist/bin:$PATH" | |
| echo "$PWD/dist/bin" >> "$GITHUB_PATH" | |
| abc -h || true | |
| yices --version | |
| yices-smt2 --version | |
| saw --version | |
| saw-remote-api --help | |
| ${{ matrix.test }} | |
| cabal-test: | |
| runs-on: ${{ matrix.os }} | |
| needs: [build] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| suite: ${{ fromJson(needs.build.outputs.cabal-test-suites-json) }} | |
| os: [ubuntu-22.04] | |
| continue-on-error: [false] | |
| include: | |
| - suite: integration_tests | |
| os: macos-12 | |
| continue-on-error: true # https://github.com/GaloisInc/saw-script/issues/1135 | |
| - suite: integration_tests | |
| os: windows-latest | |
| timeout-minutes: 60 | |
| continue-on-error: true # https://github.com/GaloisInc/saw-script/issues/1135 | |
| exclude: | |
| - suite: integration_tests | |
| os: macos-12 | |
| continue-on-error: false | |
| - suite: integration_tests | |
| os: windows-latest | |
| continue-on-error: false | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - shell: bash | |
| run: .github/ci.sh install_system_deps | |
| env: | |
| BUILD_TARGET_OS: ${{ matrix.os }} | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: dist/bin | |
| - shell: bash | |
| if: "runner.os != 'Windows'" | |
| run: chmod +x dist/bin/* | |
| - shell: bash | |
| if: runner.os != 'Windows' | |
| run: chmod +x bin/* | |
| - uses: actions/download-artifact@v2 | |
| with: | |
| name: dist-tests-${{ matrix.os }} | |
| path: dist-tests | |
| - shell: bash | |
| if: runner.os != 'Windows' | |
| run: chmod +x dist-tests/* | |
| - uses: actions/setup-java@v1 | |
| if: "matrix.suite == 'integration_tests'" | |
| with: | |
| java-version: "8" | |
| java-package: jdk | |
| architecture: x64 | |
| - name: ${{ matrix.suite }} | |
| continue-on-error: ${{ matrix.continue-on-error }} | |
| shell: bash | |
| run: | | |
| export PATH="$PWD/bin:$PWD/dist/bin:$PATH" | |
| dist-tests/${{ matrix.suite }} | |
| build-push-image: | |
| runs-on: ubuntu-22.04 | |
| needs: [config] | |
| if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - file: saw/Dockerfile | |
| image: ghcr.io/galoisinc/saw | |
| cache: ghcr.io/galoisinc/cache-saw | |
| - file: saw-remote-api/Dockerfile | |
| image: ghcr.io/galoisinc/saw-remote-api | |
| cache: ghcr.io/galoisinc/cache-saw-remote-api | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - uses: rlespinasse/github-slug-action@v3.x | |
| - id: common-tag | |
| run: | | |
| echo "::set-output name=common-tag::$GITHUB_REF_SLUG" | |
| echo "COMMON_TAG=$GITHUB_REF_SLUG" >> $GITHUB_ENV | |
| - uses: docker/setup-buildx-action@v1 | |
| - uses: crazy-max/ghaction-docker-meta@v1 | |
| name: Labels | |
| id: labels | |
| with: | |
| images: ${{ matrix.image }} | |
| - uses: docker/login-action@v1 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.actor }} | |
| password: ${{ secrets.GITHUB_TOKEN }} | |
| - if: needs.config.outputs.release == 'true' | |
| shell: bash | |
| run: | | |
| sed -i.bak \ | |
| -e 's/^hashText = .*$/hashText = ""/' \ | |
| -e '/import GitRev.*$/d' \ | |
| saw/SAWScript/Version.hs | |
| rm -f saw/SAWScript/Version.hs.bak | |
| - uses: docker/build-push-action@v2 | |
| with: | |
| context: . | |
| tags: ${{ matrix.image }}:${{ steps.common-tag.outputs.common-tag }} | |
| labels: ${{ steps.labels.outputs.labels }} | |
| load: true | |
| push: false | |
| file: ${{ matrix.file }} | |
| build-args: ${{ matrix.build-args }} | |
| cache-from: | | |
| type=registry,ref=${{ matrix.cache }}:${{ steps.prefix.outputs.prefix }}master | |
| type=registry,ref=${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }} | |
| - name: Cache image build | |
| uses: docker/build-push-action@v2 | |
| continue-on-error: true # Tolerate cache upload failures - this should be handled better | |
| with: | |
| context: . | |
| file: ${{ matrix.file }} | |
| build-args: ${{ matrix.build-args }} | |
| cache-to: type=registry,ref=${{ matrix.cache }}:${{ steps.common-tag.outputs.common-tag }},mode=max | |
| - if: matrix.image == 'ghcr.io/galoisinc/saw-remote-api' | |
| uses: actions/setup-python@v2 | |
| with: | |
| python-version: '3.9' | |
| - if: matrix.image == 'ghcr.io/galoisinc/saw-remote-api' | |
| uses: abatilo/actions-poetry@v2.0.0 | |
| with: | |
| poetry-version: 1.1.5 | |
| - if: matrix.image == 'ghcr.io/galoisinc/saw-remote-api' | |
| name: Test saw-remote-api | |
| run: ./saw-remote-api/scripts/test_docker.sh ${{ matrix.image }}:$COMMON_TAG | |
| - if: needs.config.outputs.event-schedule == 'true' | |
| name: ${{ matrix.image }}:nightly | |
| run: | | |
| docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:nightly | |
| docker push ${{ matrix.image }}:nightly | |
| - if: needs.config.outputs.release == 'true' | |
| name: ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| run: | | |
| docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| docker push ${{ matrix.image }}:${{ needs.config.outputs.version }} | |
| docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest | |
| docker push ${{ matrix.image }}:latest | |
| s2n-tests: | |
| name: "Test s2n proofs" | |
| timeout-minutes: 120 | |
| needs: build | |
| runs-on: ubuntu-22.04 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| s2n-target: | |
| - hmac | |
| - drbg | |
| - sike | |
| - bike | |
| - tls | |
| - hmac-failure | |
| - awslc | |
| - blst | |
| ghc: ["8.10.7"] | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - run: | | |
| mkdir -p s2nTests/bin | |
| - name: Download previously-built SAW | |
| uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: ./s2nTests/bin | |
| - shell: bash | |
| working-directory: s2nTests | |
| run: | | |
| docker-compose pull | |
| grep -h '^FROM' docker/*.dockerfile | sort -u | awk '{print $2}' | xargs -n1 -P8 docker pull | |
| - shell: bash | |
| name: "make s2n" | |
| working-directory: s2nTests | |
| run: docker-compose build s2n | |
| - shell: bash | |
| name: "s2n tests: ${{ matrix.s2n-target }}" | |
| working-directory: s2nTests | |
| run: | | |
| chmod +x bin/* | |
| make ${{ matrix.s2n-target }} | |
| exercises: | |
| name: "Test SAW exercises" | |
| needs: build | |
| runs-on: ubuntu-22.04 | |
| strategy: | |
| matrix: | |
| ghc: ["8.10.7"] | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - run: | | |
| mkdir -p exercises/bin | |
| - name: Download previously-built SAW | |
| uses: actions/download-artifact@v2 | |
| with: | |
| name: "${{ runner.os }}-bins" | |
| path: ./exercises/bin | |
| - shell: bash | |
| name: "make exercises container" | |
| working-directory: exercises | |
| run: docker build -t exercises . | |
| - shell: bash | |
| name: "run exercises" | |
| working-directory: exercises | |
| run: | | |
| chmod +x bin/* | |
| docker run -v $PWD/bin:/saw-bin exercises | |
| # Indicates sufficient CI success for the purposes of mergify merging the pull | |
| # request, see .github/mergify.yml. This is done instead of enumerating each | |
| # instance of each job in the mergify configuration for a number of reasons: | |
| # - continue-on-error is respected, won't block merge | |
| # - changes to jobs or job instances don't require a mergify config update | |
| # - dependencies through `needs:` are validated, CI will fail if it's invalid | |
| mergify: | |
| runs-on: ubuntu-22.04 | |
| needs: | |
| - build | |
| - heapster-tests | |
| - saw-remote-api-tests | |
| - cabal-test | |
| - s2n-tests | |
| - exercises | |
| steps: | |
| - run: "true" |