scala.yml

# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
#
# Copyright (c) 2011-2020 ETH Zurich.

name: Build, Test, and Publish

on:
  push: # run this workflow on every push
  pull_request: # run this workflow on every pull_request
  workflow_dispatch: # allow to manually trigger this workflow
    inputs:
      type:
        description: 'Specifies whether a stable or nightly release should be triggered. Note that "stable" can only be used on branch "release".'
        required: true
        default: 'nightly'
        options: 
          - stable
          - nightly
      tag_name:
        description: 'Tag name for stable release. Ignored if a nightly release will be created.'
        required: true
        default: '-'
      release_name:
        description: 'Release title for stable release. Ignored if a nightly release will be created.'
        required: true
        default: '-'
  schedule:
    - cron: '0 7 * * *' # run every day at 07:00 UTC


# some remarks about the high-level structure of this CI script:
# - build
# `build` builds and tests ViperServer using sbt.
# - test
# `test` takes both ViperServer JARs that include tests and executes them on Ubuntu, macOS, and Windows.
# - create-nightly-release
# takes the fat and skinny JARs produced by configuration `latest` during `build` job and creates a nightly release with
# them. This job automatically runs every night.
# - create-stable-release
# takes the fat and skinny JARs produced by configuration `release` during `build` job and creates a draft release with
# them. This only works on branch `release`.

env:
  Z3_VERSION: "4.8.7"

jobs:
  build:
    # build is the base job on which all other jobs depend
    # we enforce here that the nightly build job only runs in the main repo:
    if: (github.event_name == 'schedule' && github.repository == 'viperproject/viperserver') || (github.event_name != 'schedule')
    runs-on: ubuntu-latest
    container: viperproject/viperserver:v4_z3_4.8.7
    steps:
      - name: Checkout ViperServer
        uses: actions/checkout@v3
        with:
          path: viperserver
          submodules: recursive

      - name: Java Version
        run: java --version
      - name: Z3 Version
        run: z3 -version
      - name: Boogie Version
        run: boogie /version

      - name: Get Silver commits referenced by Silicon and Carbon
        run: |
          echo "SILICON_SILVER_REF=$(git -C viperserver/silicon/silver rev-parse HEAD)" >> $GITHUB_ENV
          echo "CARBON_SILVER_REF=$(git -C viperserver/carbon/silver rev-parse HEAD)" >> $GITHUB_ENV

      - name: Silicon and Carbon reference different Silver commits
        if: env.SILICON_SILVER_REF != env.CARBON_SILVER_REF
        run: |
          echo "::error file=.github/workflows/scala.yml::Silicon and Carbon reference different Silver commits (${{ env.SILICON_SILVER_REF }} and ${{ env.CARBON_SILVER_REF }})"
          # terminate this job:
          exit 1

      - name: Create version file
        run: |
          echo "ViperServer: commit $(git -C viperserver rev-parse HEAD)" >> versions.txt
          echo "Silicon: commit $(git -C viperserver/silicon rev-parse HEAD)" >> versions.txt
          echo "Carbon: commit $(git -C viperserver/carbon rev-parse HEAD)" >> versions.txt
          echo "Silver: commit ${{ env.SILICON_SILVER_REF }}" >> versions.txt
        # first line overwrites versions.txt in case it already exists, all other append to the file
      - name: Upload version file
        uses: actions/upload-artifact@v3
        with:
          name: versions.txt
          path: versions.txt

      - name: Set sbt cache variables
        run: echo "SBT_OPTS=-Dsbt.global.base=sbt-cache/.sbtboot -Dsbt.boot.directory=sbt-cache/.boot -Dsbt.ivy.home=sbt-cache/.ivy" >> $GITHUB_ENV
        # note that the cache path is relative to the directory in which sbt is invoked.

      - name: Cache SBT
        uses: actions/cache@v3
        with:
          path: |
            viperserver/sbt-cache/.sbtboot
            viperserver/sbt-cache/.boot
            viperserver/sbt-cache/.ivy/cache
          # <x>/project/target and <x>/target, where <x> is e.g. 'viperserver', are intentionally not
          # included as several occurrences of NoSuchMethodError exceptions have been observed during CI runs. It seems
          # like sbt is unable to correctly compute source files that require a recompilation. Therefore, we have
          # disabled caching of compiled source files altogether
          key: ${{ runner.os }}-sbt-no-precompiled-sources-${{ hashFiles('**/build.sbt') }}

      - name: Test ViperServer
        run: sbt test
        working-directory: viperserver

      - name: Upload log files
        if: ${{ failure() }}
        uses: actions/upload-artifact@v3
        with:
          name: TestLogs
          path: viperserver/logs

      - name: Assemble ViperServer skinny JARs
        run: sbt stage
        working-directory: viperserver

      - name: Zip skinny JARs
        run: zip -r ../../../../viperserver-skinny-jars.zip ./*
        working-directory: viperserver/target/universal/stage/lib

      - name: Upload ViperServer skinny JARs
        uses: actions/upload-artifact@v3
        with:
          name: viperserver-skinny-jars
          path: viperserver/viperserver-skinny-jars.zip

      - name: Assemble ViperServer fat JAR
        run: sbt "set test in assembly := {}" clean assembly
        working-directory: viperserver

      - name: Upload ViperServer fat JAR
        uses: actions/upload-artifact@v3
        with:
          name: viperserver-fat-jar
          path: viperserver/target/scala-2.13/viperserver.jar

      - name: Assemble ViperServer test fat JAR
        run: sbt clean test:assembly
        working-directory: viperserver

      - name: Upload ViperServer test fat JAR
        uses: actions/upload-artifact@v3
        with:
          name: viperserver-test-fat-jar
          path: viperserver/target/scala-2.13/viperserver-test.jar


  test:
    name: test - ${{ matrix.os }}
    needs: build
    strategy:
      # tests should not be stopped when they fail on one of the OSes:
      fail-fast: false
      matrix:
        os: [macos-latest, ubuntu-latest, windows-latest]
    runs-on: ${{ matrix.os }}
    env:
      WIN_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-win.zip'
      LINUX_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-linux.zip'
      MAC_BOOGIE_URL: 'https://github.com/viperproject/boogie-builder/releases/latest/download/boogie-osx.zip'
    steps:
      # we need to checkout the repo to have access to the test files
      - name: Checkout ViperServer
        uses: actions/checkout@v3
        with:
          path: viperserver

      # we need to checkout the silicon repo to have access to the logback configuration file
      # as we do not use anything else except the logback config, we simply take the latest master branch (in all configurations)
      - name: Checkout Silicon
        uses: actions/checkout@v3
        with:
          repository: viperproject/silicon
          path: silicon

      - name: Download ViperServer test fat JAR
        uses: actions/download-artifact@v3
        with:
          name: viperserver-test-fat-jar
          path: viperserver

      - name: Download Z3 (Ubuntu)
        if: startsWith(matrix.os, 'ubuntu')
        run: |
          curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04.zip --output z3.zip
          unzip z3.zip -d z3/
          echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04/bin" >> $GITHUB_PATH
          echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-ubuntu-16.04/bin/z3" >> $GITHUB_ENV
        shell: bash

      - name: Download Z3 (macOS)
        if: startsWith(matrix.os, 'macos')
        run: |
          curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6.zip --output z3.zip
          unzip z3.zip -d z3/
          echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6/bin" >> $GITHUB_PATH
          echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-osx-10.14.6/bin/z3" >> $GITHUB_ENV
        shell: bash

      - name: Download Z3 (Windows)
        if: startsWith(matrix.os, 'windows')
        run: |
          curl -L --silent --show-error --fail https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-win.zip --output z3.zip
          unzip z3.zip -d z3/
          echo "$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-win/bin" >> $GITHUB_PATH
          echo "Z3_EXE=$GITHUB_WORKSPACE/z3/z3-${{ env.Z3_VERSION }}-x64-win/bin/z3.exe" >> $GITHUB_ENV
        shell: bash

      - name: Download Boogie (Ubuntu)
        if: startsWith(matrix.os, 'ubuntu')
        run: |
          curl -L --silent --show-error --fail ${{ env.LINUX_BOOGIE_URL }} --output boogie-linux.zip
          unzip boogie-linux.zip -d boogie-linux
          echo "$GITHUB_WORKSPACE/boogie-linux/binaries-linux" >> $GITHUB_PATH
          echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-linux/binaries-linux/Boogie" >> $GITHUB_ENV
        shell: bash

      - name: Download Boogie (macOS)
        if: startsWith(matrix.os, 'macos')
        run: |
          curl -L --silent --show-error --fail ${{ env.MAC_BOOGIE_URL }} --output boogie-mac.zip
          unzip boogie-mac.zip -d boogie-mac
          echo "$GITHUB_WORKSPACE/boogie-mac/binaries-osx" >> $GITHUB_PATH
          echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-mac/binaries-osx/Boogie" >> $GITHUB_ENV
        shell: bash

      - name: Download Boogie (Windows)
        if: startsWith(matrix.os, 'windows')
        run: |
          curl -L --silent --show-error --fail ${{ env.WIN_BOOGIE_URL }} --output boogie-win.zip
          unzip boogie-win.zip -d boogie-win
          echo "$GITHUB_WORKSPACE/boogie-win/binaries-win" >> $GITHUB_PATH
          echo "BOOGIE_EXE=$GITHUB_WORKSPACE/boogie-win/binaries-win/Boogie.exe" >> $GITHUB_ENV
        shell: bash

      - name: Setup Java JDK
        uses: actions/setup-java@v3
        with:
          java-version: '11'
          distribution: 'temurin'

      - name: Java Version
        run: java --version
      - name: Z3 Version
        run: z3 -version
      - name: Boogie Version
        run: Boogie /version

      # unfortunately, the JAR seems to be broken and discovering test suites (e.g. using `-w viper.server`) fails.
      # thus, the test suites have to be explicitly mentioned
      - name: Test ViperServer
        run: java -Xss128m -Dlogback.configurationFile=$GITHUB_WORKSPACE/silicon/src/main/resources/logback.xml -cp viperserver-test.jar org.scalatest.tools.Runner -R viperserver-test.jar -o -s viper.server.core.AstGenerationTests -s viper.server.core.CoreServerSpec -s viper.server.core.ViperServerHttpSpec
        shell: bash
        working-directory: viperserver

      - name: Upload log files
        if: ${{ failure() }}
        uses: actions/upload-artifact@v3
        with:
          name: TestLogs-${{ runner.os }}
          path: viperserver/logs


  create-nightly-release:
    needs: test
    # this job creates a new nightly pre-release, set viperserver.jar as artifacts, and deletes old releases
    if: github.ref != 'refs/heads/release' && ((github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'nightly') || github.event_name == 'schedule')
    runs-on: ubuntu-latest
    steps:
      - name: Install prerequisites
        run: sudo apt-get install curl

      - name: Download ViperServer skinny JARs
        uses: actions/download-artifact@v3
        with:
          name: viperserver-skinny-jars
          path: deploy

      - name: Download ViperServer fat JAR
        uses: actions/download-artifact@v3
        with:
          name: viperserver-fat-jar
          path: deploy

      - name: Download version file
        uses: actions/download-artifact@v3
        with:
          name: versions.txt

      - name: Check whether commits have changed
          # the following command queries all releases (as JSON) and passes it to `jq` that performs the following
          # filtering:
          # 1. only consider prereleases (instead of stable releases)
          # 2. extract body
          # 3. check if $VERSIONS is contained in the release's body. $VERSIONS stores the file content of versions.txt
          # 4. return 'true" if at least one release satisfies the criterion
          # MATCHING_RELEASE is 'true' if a matching release has been found and thus no new release should be created
        run: |
          MATCHING_RELEASE=$( \
            curl --fail --silent \
              --header 'Accept: application/vnd.github.v3+json' \
              --header 'Authorization: token ${{ secrets.GITHUB_TOKEN }}' \
              --url 'https://api.github.com/repos/viperproject/viperserver/releases' \
            | \
            jq --rawfile VERSIONS versions.txt \
              'map(select(.prerelease == true) | .body | contains($VERSIONS)) | any')
          echo "MATCHING_RELEASE=$MATCHING_RELEASE" >> $GITHUB_ENV

      - name: Create release tag
        if: env.MATCHING_RELEASE != 'true'
        shell: bash
        run: echo "TAG_NAME=$(date +v-%Y-%m-%d-%H%M)" >> $GITHUB_ENV

      - name: Create nightly release
        if: env.MATCHING_RELEASE != 'true'
        id: create_release
        uses: viperproject/create-nightly-release@v1
        env:
          # This token is provided by Actions, you do not need to create your own token
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          tag_name: ${{ env.TAG_NAME }}
          release_name: Nightly Release ${{ env.TAG_NAME }}
          body_path: versions.txt
          keep_num: 1 # keep the previous nightly release such that there are always two

      - name: Upload ViperServer skinny jars
        if: env.MATCHING_RELEASE != 'true'
        uses: actions/upload-release-asset@v1.0.2
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          upload_url: ${{ steps.create_release.outputs.upload_url }}
          asset_path: deploy/viperserver-skinny-jars.zip
          asset_name: viperserver-skinny-jars.zip
          asset_content_type: application/zip

      - name: Upload ViperServer fat jar artifact
        if: env.MATCHING_RELEASE != 'true'
        uses: actions/upload-release-asset@v1.0.2
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          upload_url: ${{ steps.create_release.outputs.upload_url }}
          asset_path: deploy/viperserver.jar
          asset_name: viperserver.jar
          asset_content_type: application/octet-stream

      - name: Trigger Viper-IDE CI
        if: env.MATCHING_RELEASE != 'true'
        run: |
          curl --fail --request POST \
          --user 'viper-admin:${{ secrets.VIPER_ADMIN_TOKEN }}' \
          --header 'Accept: application/vnd.github.v3+json' \
          --url 'https://api.github.com/repos/viperproject/viper-ide/actions/workflows/test.yml/dispatches' \
          --data "{ \
            \"ref\":\"master\", \
            \"inputs\":{ \
              \"type\":\"nightly\", \
              \"viperserver_tag_name\":\"${{ env.TAG_NAME }}\", \
              \"boogie_tag_name\":\"latest\", \
              \"z3_version\":\"${{ env.Z3_VERSION }}\", \
              \"tag_name\":\"${{ env.TAG_NAME }}\", \
              \"release_name\":\"Nightly Release ${{ env.TAG_NAME }}\" \
            } \
          }"


  create-stable-release:
    needs: test
    # this job creates a stable draft-release and set viperserver.jar as artifacts
    if: github.ref == 'refs/heads/release' && github.event_name == 'workflow_dispatch' && github.event.inputs.type == 'stable'
    runs-on: ubuntu-latest
    steps:
      - name: Download ViperServer skinny JARs
        uses: actions/download-artifact@v3
        with:
          name: viperserver-skinny-jars
          path: deploy

      - name: Download ViperServer fat JAR
        uses: actions/download-artifact@v3
        with:
          name: viperserver-fat-jar
          path: deploy

      - name: Download version file
        uses: actions/download-artifact@v3
        with:
          name: versions.txt

      - name: Create stable draft-release
        id: create_release
        uses: actions/create-release@v1
        env:
          # This token is provided by Actions, you do not need to create your own token
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          tag_name: ${{ github.event.inputs.tag_name }}
          release_name: ${{ github.event.inputs.release_name }}
          body_path: versions.txt
          draft: true
          prerelease: false

      - name: Upload ViperServer skinny jars
        uses: actions/upload-release-asset@v1.0.2
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          upload_url: ${{ steps.create_release.outputs.upload_url }}
          asset_path: deploy/viperserver-skinny-jars.zip
          asset_name: viperserver-skinny-jars.zip
          asset_content_type: application/zip

      - name: Upload ViperServer fat jar
        uses: actions/upload-release-asset@v1.0.2
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          upload_url: ${{ steps.create_release.outputs.upload_url }}
          asset_path: deploy/viperserver.jar
          asset_name: viperserver.jar
          asset_content_type: application/octet-stream