Skip to content

Extend library refs processing, fix in error messages for setUp #4936

Extend library refs processing, fix in error messages for setUp

Extend library refs processing, fix in error messages for setUp #4936

Workflow file for this run

---
name: 'Test PR'
on:
pull_request:
branches:
- 'master'
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
code-quality-checks:
name: 'Code Quality Checks'
runs-on: ubuntu-latest
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Install Poetry'
uses: Gr1N/setup-poetry@v8
- name: 'Run code quality checks'
run: make check
- name: 'Run pyupgrade'
run: make pyupgrade
unit-tests:
needs: code-quality-checks
name: 'Unit Tests'
runs-on: ubuntu-latest
steps:
- name: 'Check out code'
uses: actions/checkout@v4
- name: 'Install Poetry'
uses: Gr1N/setup-poetry@v8
- name: 'Run unit tests'
run: make cov-unit
profile:
needs: code-quality-checks
name: 'Profiling'
runs-on: [self-hosted, linux, normal]
strategy:
fail-fast: false
matrix:
backend: ['legacy', 'booster']
timeout-minutes: 30
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: kontrol-ci-profile-${{ github.sha }}
- name: 'Build KEVM'
run: |
docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install'
docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.foundry'
- name: 'Run profiling'
run: |
PROF_ARGS=--numprocesses=8
[ ${{ matrix.backend }} == 'legacy' ] && PROF_ARGS+=' --no-use-booster'
docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kontrol-ci-profile-${GITHUB_SHA}
integration-tests:
needs: code-quality-checks
name: 'Integration Tests'
runs-on: [self-hosted, linux, normal, fast]
strategy:
fail-fast: false
matrix:
backend: ['legacy', 'booster']
timeout-minutes: 120
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: kontrol-ci-integration-${{ github.sha }}
- name: 'Build KEVM'
run: |
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
- name: 'Run integration tests'
run: |
TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)"'
if [ ${{ matrix.backend }} == 'legacy' ]; then
TEST_ARGS+=' --no-use-booster --numprocesses=6'
else
TEST_ARGS+=' --numprocesses=4'
fi
docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
cse-tests:
needs: code-quality-checks
name: 'CSE Tests'
runs-on: [self-hosted, linux, normal, fast]
timeout-minutes: 120
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: kontrol-ci-integration-${{ github.sha }}
- name: 'Build KEVM'
run: |
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
- name: 'Run CSE and Minimize tests'
run: |
TEST_ARGS='--numprocesses=8 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
end-to-end-tests:
needs: code-quality-checks
name: 'End to End Sanity Tests'
runs-on: [self-hosted, linux, normal, fast]
timeout-minutes: 35
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: kontrol-ci-integration-${{ github.sha }}
- name: 'Build KEVM'
run: |
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
- name: 'Run end-to-end tests'
run: |
TEST_ARGS='--numprocesses=8 -vv -k "test_kontrol_end_to_end"'
docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}
docker:
needs: code-quality-checks
name: 'Docker Tests'
runs-on: [self-hosted, linux, normal]
timeout-minutes: 30
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Set environment'
run: |
echo "IMAGE_TAG=runtimeverificationinc/kontrol-${GITHUB_SHA}" >> ${GITHUB_ENV}
echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV}
echo "DOCKER_USER=user" >> ${GITHUB_ENV}
echo "DOCKER_GROUP=user" >> ${GITHUB_ENV}
echo "FOUNDRY_ROOT=/home/user/foundry" >> ${GITHUB_ENV}
- name: 'Build Docker image'
run: |
K_VERSION=$(cat deps/k_release)
Z3_VERSION=$(cat deps/z3)
docker build . --tag ${IMAGE_TAG} --build-arg K_VERSION=${K_VERSION} --build-arg Z3_VERSION=${Z3_VERSION}
- name: 'Start Docker container'
run: |
docker run \
--name ${CONTAINER_NAME} \
--rm \
--interactive \
--tty \
--detach \
--user root \
${IMAGE_TAG}
docker cp src/tests/integration/test-data/foundry ${CONTAINER_NAME}:${FOUNDRY_ROOT}
docker exec ${CONTAINER_NAME} chown -R ${DOCKER_USER}:${DOCKER_GROUP} ${FOUNDRY_ROOT}
- name: 'Run forge build'
run: |
docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git foundry-rs/forge-std@75f1746
docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge install --no-git runtimeverification/kontrol-cheatcodes@a5dd4b0
docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} forge build
- name: 'Run kontrol build'
run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build -O2
- name: 'Run kontrol prove'
run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()'
- name: 'Run kontrol show'
run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()'
- name: 'Tear down Docker'
if: always()
run: |
docker stop --time=0 ${CONTAINER_NAME}
nix:
needs: code-quality-checks
name: 'Nix Tests'
strategy:
fail-fast: false
matrix:
runner: [ubuntu-latest, macos-13, MacM1] # MacM1 is self-hosted
runs-on: ${{ matrix.runner }}
timeout-minutes: 60
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Install Nix'
if: ${{ matrix.runner != 'MacM1' }}
uses: cachix/install-nix-action@v22
with:
install_url: https://releases.nixos.org/nix/nix-2.13.3/install
extra_nix_config: |
substituters = http://cache.nixos.org https://cache.iog.io
trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
- name: 'Install Cachix'
if: ${{ matrix.runner != 'MacM1' }}
uses: cachix/cachix-action@v12
with:
name: k-framework
- name: 'Build Kontrol'
env:
NIX_PATH: 'nixpkgs=http://nixos.org/channels/nixos-22.05/nixexprs.tar.xz'
GC_DONT_GC: '1'
run: |
set -euxo pipefail
nix --version
JQ=$(nix-build '<nixpkgs>' -A jq --no-link)/bin/jq
KONTROL_BIN=$(nix build .#kontrol.solc_0_8_13 --print-build-logs --json | $JQ -r '.[].outputs | to_entries[].value')/bin
echo $KONTROL_BIN >> $GITHUB_PATH
- name: 'Run smoke test'
run: cd package && ./test-package.sh