Skip to content

Fix purity classification of composite literals #4623

Fix purity classification of composite literals

Fix purity classification of composite literals #4623

Workflow file for this run

# 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 }}