test.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-2021 ETH Zurich.

name: test

on:
  push: # run this workflow on every push
  pull_request: # run this workflow on every pull_request

jobs:
  # there is a single job to avoid copying the built docker image from one job to the other
  build-test-deploy-container:
    runs-on: ubuntu-latest
    env:
      IMAGE_ID: ghcr.io/${{ github.repository_owner }}/gobra
      # image labels are new-line separated key value pairs (according to https://specs.opencontainers.org/image-spec/annotations/):
      IMAGE_LABELS: |
        org.opencontainers.image.authors=Viper Project <https://viper.ethz.ch>
        org.opencontainers.image.url=https://github.com/viperproject/gobra/pkgs/container/gobra
        org.opencontainers.image.source=${{ github.server_url }}/${{ github.repository }}
        org.opencontainers.image.revision=${{ github.sha }}
        org.opencontainers.image.licenses=MPL-2.0
        org.opencontainers.image.description=Gobra image for revision ${{ github.sha }} built by workflow run ${{ github.run_id }}
      CONCLUSION_SUCCESS: "success"
      CONCLUSION_FAILURE: "failure"
      # Output levels according to severity.
      # They identify the kinds of annotations to be printed by Github.
      NOTICE_LEVEL: "info"
      WARNING_LEVEL: "warning"
      FAILURE_LEVEL: "error"
    steps:
      - name: Checkout Gobra
        uses: actions/checkout@v4
        with:
          submodules: 'recursive'
      - name: Check that silicon & carbon reference same silver commit
        run: |
          SILICON_SILVER_REF=$(git -C viperserver/silicon/silver rev-parse HEAD) && \
          CARBON_SILVER_REF=$(git -C viperserver/carbon/silver rev-parse HEAD) && \
          if [ "$SILICON_SILVER_REF" != "$CARBON_SILVER_REF" ]; then echo "Silicon and Carbon reference different Silver commits ($SILICON_SILVER_REF and $CARBON_SILVER_REF)" && exit 1 ; fi

      # used to enable Docker caching (see https://github.com/docker/build-push-action)
      - name: Set up Docker Buildx
        uses: docker/setup-buildx-action@v3

      - name: Create image creation label
        run: |
          CREATED_LABEL="org.opencontainers.image.created=$(date --rfc-3339=seconds)"
          echo "CREATED_LABEL=$CREATED_LABEL" >> $GITHUB_ENV

      - name: Create image metadata
        id: image-metadata
        uses: docker/metadata-action@v5
        with:
          images: ${{ env.IMAGE_ID }}
          labels: |
            ${{ env.IMAGE_LABELS }}
            ${{ env.CREATED_LABEL }}
          tags: |
            # the first 4 tags correspond to the default options
            type=schedule
            type=ref,event=branch
            type=ref,event=tag
            type=ref,event=pr
            # use (short) commit hash as tag:
            type=sha
            # use latest tag for default branch and with highest priority (1000 is the highest default priority for the other types):
            type=raw,value=latest,priority=1100,enable={{is_default_branch}}

      - name: Get first tag
        run: echo "IMAGE_TAG=$(echo "${{ steps.image-metadata.outputs.tags }}" | head -1)" >> $GITHUB_ENV

      - name: Build image up to including stage 'build'
        id: image-build
        # note that the action's name is misleading: this step does NOT push
        uses: docker/build-push-action@v5
        with:
          context: .
          load: true # make the built image available in docker (locally)
          target: build # only build up to and including stage 'build'
          file: workflow-container/Dockerfile
          tags: ${{ steps.image-metadata.outputs.tags }}
          labels: ${{ steps.image-metadata.outputs.labels }}
          push: false
          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
          # use GitHub cache:
          cache-from: type=gha, scope=${{ github.workflow }}
          cache-to: type=gha, scope=${{ github.workflow }}

      - name: Execute all tests
        run: |
          # create a directory to sync with the docker container and to store the created pidstats
          mkdir -p $PWD/sync
          docker run \
            --mount type=volume,dst=/build/gobra/sync,volume-driver=local,volume-opt=type=none,volume-opt=o=bind,volume-opt=device=$PWD/sync \
            ${{ env.IMAGE_TAG }} \
            /bin/sh -c "$(cat .github/test-and-measure-ram.sh)"

      - name: Get max RAM usage by Java and Z3
        if: ${{ always() }}
        shell: bash
        env:
          JAVA_WARNING_THRESHOLD_GB: 4.5
          JAVA_FAILURE_THRESHOLD_GB: 5.5
          Z3_WARNING_THRESHOLD_GB: 0.5
          Z3_FAILURE_THRESHOLD_GB: 1
        # awk is used to perform the computations such that the computations are performed with floating point precision
        # we transform bash variables into awk variables to not cause problems with bash's variable substitution
        # after computing the memory usage (in KB) a few more computations are performed. At the very end, all (local)
        # environment variables are exported to `$GITHUB_ENV` such that they will be available in the next step as well.
        run: |
          function getMaxMemOfProcessInKb {
            # $1 is the regex used to filter lines by the 9th column
            # - we use variable `max` to keep track of the maximum
            # - `curCount` stores the sum of all processes with the given name for a particular timestamp
            # - note that looking at the timestamp is only an approximation: pidstat might report different timestamps in the
            #   same "block" of outputs (i.e. the report every second)
            # - `NR>=2` specifies that the file's first line (NR=1) is ignored
            # - `$7` refers to the 7th column in the file which corresponds to the column storing RAM (in kb)
            # - `java$` matches only lines that end in the string 'java'
            # - variable `max` is printed after processing the entire file
            local result=$(awk -v processName=$1 -v max=0 -v curCount=0 -v curTimestamp=0 'processName~$9 {if(NR>=2){if(curTimestamp==$1){curCount=curCount+$7}else{curTimestamp=$1; curCount=$7}}; if(curCount>max){max=curCount}}END{print max}' sync/pidstat.txt)
            echo $result
          }
          function convertKbToGb {
            # $1 is the value [KB] that should be converted
            local result=$(awk -v value=$1 'BEGIN {print value / 1000 / 1000}')
            echo $result
          }
          function getLevel {
            # $1 is the value that should be comparing against the thresholds
            # $2 is the threshold causing a warning
            # $3 is the threshold causing an error
            # writes ${{ env.NOTICE_LEVEL }}, ${{ env.WARNING_LEVEL}} or ${{ env.FAILURE_LEVEL }} to standard output
            local result=$(awk -v value=$1 -v warnThres=$2 -v errThres=$3 'BEGIN { print (value>errThres) ? "${{ env.FAILURE_LEVEL }}" : (value>warnThres) ? "${{ env.WARNING_LEVEL }}" : "${{ env.NOTICE_LEVEL}}" }')
            echo $result
          }
          MAX_JAVA_KB=$(getMaxMemOfProcessInKb 'java$')
          MAX_Z3_KB=$(getMaxMemOfProcessInKb 'z3$')
          MAX_JAVA_GB=$(convertKbToGb $MAX_JAVA_KB)
          MAX_Z3_GB=$(convertKbToGb $MAX_Z3_KB)
          JAVA_LEVEL=$(getLevel $MAX_JAVA_GB ${{ env.JAVA_WARNING_THRESHOLD_GB }} ${{ env.JAVA_FAILURE_THRESHOLD_GB }})
          Z3_LEVEL=$(getLevel $MAX_Z3_GB ${{ env.Z3_WARNING_THRESHOLD_GB }} ${{ env.Z3_FAILURE_THRESHOLD_GB }})
          if [[ "$JAVA_LEVEL" = "${{ env.FAILURE_LEVEL }}" || "$Z3_LEVEL" = "${{ env.FAILURE_LEVEL }}" ]]
          then
            CONCLUSION="${{ env.CONCLUSION_FAILURE }}"
          else
            CONCLUSION="${{ env.CONCLUSION_SUCCESS }}"
          fi
          echo "MAX_JAVA_GB=$MAX_JAVA_GB" >> $GITHUB_ENV
          echo "MAX_Z3_GB=$MAX_Z3_GB" >> $GITHUB_ENV
          echo "JAVA_LEVEL=$JAVA_LEVEL" >> $GITHUB_ENV
          echo "Z3_LEVEL=$Z3_LEVEL" >> $GITHUB_ENV
          echo "CONCLUSION=$CONCLUSION" >> $GITHUB_ENV

      - name: Create annotations
        if: ${{ always() }}
        # Outputs the memory consumption of JAVA and Z3. The message format is described in
        # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions .
        run: |
          JAVA_MESSAGE="Java used up to ${{ env.MAX_JAVA_GB }}GB of RAM"
          if [ "${{ env.JAVA_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ]
          then
            echo "$JAVA_MESSAGE"
          else
            echo "::${{ env.JAVA_LEVEL }} file=.github/workflows/test.yml,line=1::$JAVA_MESSAGE"
          fi 

          Z3_MESSAGE="Z3 used up to ${{ env.MAX_Z3_GB }}GB of RAM"
          if [ "${{ env.Z3_LEVEL }}" = "${{ env.NOTICE_LEVEL }}" ]
          then
            echo "$Z3_MESSAGE"
          else
            echo "::${{ env.Z3_LEVEL }} file=.github/workflows/test.yml,line=1::$Z3_MESSAGE"
          fi 

          if [ $CONCLUSION = "${{ env.CONCLUSION_FAILURE }}" ]
          then
            # the whole step fails when this comparison fails
            exit 1
          fi

      - name: Upload RAM usage
        if: ${{ always() }}
        uses: actions/upload-artifact@v4
        with:
          name: pidstat.txt
          path: sync/pidstat.txt

      - name: Build entire image
        uses: docker/build-push-action@v5
        with:
          context: .
          load: true # make the built image available in docker (locally)
          file: workflow-container/Dockerfile
          tags: ${{ steps.image-metadata.outputs.tags }}
          labels: ${{ steps.image-metadata.outputs.labels }}
          push: false
          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
          # use GitHub cache:
          cache-from: type=gha, scope=${{ github.workflow }}
          cache-to: type=gha, scope=${{ github.workflow }}

      - name: Test final container by verifying a file
        run: |
          docker run \
            ${{ env.IMAGE_TAG }} \
            -i tutorial-examples/basicAnnotations.gobra

      - name: Decide whether image should be deployed or not
        run: |
          # note that these GitHub expressions return the value '1' for 'true' (as opposed to bash)
          IS_GOBRA_REPO=${{ github.repository == 'viperproject/gobra' }}
          IS_MASTER=${{ github.ref == 'refs/heads/master' }}
          IS_VERIFIED_SCION=${{ github.ref == 'refs/heads/verified-scion-preview-without-selective' }}
          IS_PROPER_TAG=${{ startsWith(github.ref, 'refs/tags/v') }}
          # we use `${{ true }}` to be able to compare against GitHub's truth value:
          if [[ "$IS_GOBRA_REPO" == ${{ true }} && ("$IS_MASTER" == ${{ true }} || "$IS_VERIFIED_SCION" == ${{ true }} || "$IS_PROPER_TAG" == ${{ true }}) ]]
          then
            SHOULD_DEPLOY='true'
          else
            SHOULD_DEPLOY='false'
          fi
          echo "SHOULD_DEPLOY=$SHOULD_DEPLOY" >> $GITHUB_ENV

      - name: Login to Github Packages
        if: env.SHOULD_DEPLOY == 'true'
        uses: docker/login-action@v3
        with:
          registry: ghcr.io
          username: ${{ github.actor }}
          password: ${{ secrets.GITHUB_TOKEN }}

      - name: Push entire image
        if: env.SHOULD_DEPLOY == 'true'
        uses: docker/build-push-action@v5
        with:
          context: .
          file: workflow-container/Dockerfile
          tags: ${{ steps.image-metadata.outputs.tags }}
          labels: ${{ steps.image-metadata.outputs.labels }}
          push: true
          provenance: false # without this, GH displays 2 architecture (unknown/unknown) and omits labels
          # use GitHub cache:
          cache-from: type=gha, scope=${{ github.workflow }}
          cache-to: type=gha, scope=${{ github.workflow }}