Add workflows from evm-semantics

.github/actions/with-docker/action.yml

@@ -3,33 +3,85 @@ description: 'Run a given stage with Docker Image'
 inputs:
   container-name:
     description: 'Docker container name to use'
+    type: string
     required: true
+  tag-name:
+    description: 'Docker image tag to use'
+    type: string
+    required: false
+    default: runtimeverificationinc/kontrol
+  subdir:
+    description: 'Subdirectory where code is cloned.'
+    required: false
+    type: string
+    default: './'
+  os:
+    description: 'OS to setup Docker for.'
+    required: false
+    type: string
+    default: 'ubuntu'
+  distro:
+    description: 'Distribution to setup Docker for.'
+    required: false
+    type: string
+    default: 'jammy'
+  llvm:
+    description: 'LLVM version to use.'
+    required: false
+    type: number
+    default: 14
+  dockerfile:
+    description: 'Hardcode the path of the dockerfile to use.'
+    required: false
+    type: string
+    default: '.github/workflows/Dockerfile'
 runs:
   using: 'composite'
   steps:
   - name: 'Set up Docker'
     shell: bash {0}
-    env:
-      CONTAINER_NAME: ${{ inputs.container-name }}
     run: |
       set -euxo pipefail
 
+      CONTAINER_NAME=${{ inputs.container-name }}
+      SUBDIR=${{ inputs.subdir }}
+      BASE_OS=${{ inputs.os }}
+      BASE_DISTRO=${{ inputs.distro }}
+      DOCKERFILE=${{ inputs.dockerfile }}
+      LLVM_VERSION=${{ inputs.llvm }}
+      TAG_NAME=${{ inputs.tag-name }}
+
+      USER=github-user
+      GROUP=${USER}
+      Z3_VERSION=4.12.1
       K_VERSION=$(cat deps/k_release)
+      USER_ID=1000
+      GROUP_ID=${USER_ID}
+
+      docker build .                           \
+        --file .github/workflows/Dockerfile.z3 \
+        --tag z3:${Z3_VERSION}                 \
 
-      docker build .                                \
-        --file ./Dockerfile                         \
-        --tag runtimeverification/${CONTAINER_NAME} \
-        --build-arg K_VERSION=${K_VERSION}
+      docker build . --file ${DOCKERFILE}        \
+        --tag ${TAG_NAME}                        \
+        --build-arg USER_ID=${USER_ID}           \
+        --build-arg GROUP_ID=${GROUP_ID}         \
+        --build-arg USER=${USER}                 \
+        --build-arg GROUP=${GROUP}               \
+        --build-arg BASE_DISTRO=${BASE_DISTRO}   \
+        --build-arg K_VERSION=${K_VERSION}       \
+        --build-arg Z3_VERSION=${Z3_VERSION}     \
+        --build-arg LLVM_VERSION=${LLVM_VERSION}
 
-      docker run                       \
-        --name ${CONTAINER_NAME}       \
-        --rm                           \
-        --interactive                  \
-        --tty                          \
-        --detach                       \
-        --user root                    \
-        --workdir /home/user/workspace \
-        runtimeverification/${CONTAINER_NAME}
+      docker run                          \
+        --name ${CONTAINER_NAME}          \
+        --rm                              \
+        --interactive                     \
+        --tty                             \
+        --detach                          \
+        --user root                       \
+        --workdir /home/${USER}/workspace \
+        ${TAG_NAME}
 
-      docker cp . ${CONTAINER_NAME}:/home/user/workspace
-      docker exec ${CONTAINER_NAME} chown -R user:user /home/user
+      docker cp . ${CONTAINER_NAME}:/home/${USER}/workspace
+      docker exec ${CONTAINER_NAME} chown -R ${USER}:${GROUP} /home/${USER}

.github/workflows/Dockerfile

@@ -0,0 +1,58 @@
+ARG Z3_VERSION
+ARG K_VERSION
+ARG BASE_DISTRO
+ARG LLVM_VERSION
+
+FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
+
+ARG Z3_VERSION
+FROM z3:${Z3_VERSION} as Z3
+
+ARG K_VERSION
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
+
+COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
+COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
+COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
+
+COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+
+ARG LLVM_VERSION
+
+RUN    apt-get update                  \
+    && apt-get upgrade --yes           \
+    && apt-get install --yes           \
+            cargo                      \
+            clang-${LLVM_VERSION}      \
+            cmake                      \
+            curl                       \
+            debhelper                  \
+            libboost-test-dev          \
+            libcrypto++-dev            \
+            libprocps-dev              \
+            libssl-dev                 \
+            libyaml-dev                \
+            llvm-${LLVM_VERSION}-dev   \
+            llvm-${LLVM_VERSION}-tools \
+            maven                      \
+            python3                    \
+            python3-pip
+
+ARG USER=user
+ARG GROUP
+ARG USER_ID
+ARG GROUP_ID
+RUN groupadd -g ${GROUP_ID} ${GROUP} && useradd -m -u ${USER_ID} -s /bin/sh -g ${GROUP} ${USER}
+
+USER ${USER}:${GROUP}
+RUN mkdir /home/${USER}/workspace
+WORKDIR /home/${USER}/workspace
+
+ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PATH}
+
+RUN    curl -sSL https://install.python-poetry.org | python3 - \
+    && poetry --version
+
+RUN    cargo install svm-rs --version 0.3.0 --locked \
+    && svm install 0.8.13                            \
+    && solc --version

.github/workflows/Dockerfile.z3

@@ -0,0 +1,22 @@
+FROM ubuntu:jammy
+
+ENV TZ=America/Chicago
+RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
+
+RUN    apt-get update        \
+    && apt-get upgrade --yes \
+    && apt-get install --yes \
+            clang            \
+            cmake            \
+            git              \
+            python3
+
+ARG Z3_VERSION=4.12.1
+RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \
+    && cd z3                                                                \
+    && python3 scripts/mk_make.py                                           \
+    && cd build                                                             \
+    && make -j8                                                             \
+    && make install                                                         \
+    && cd ../..                                                             \
+    && rm -rf z3

.github/workflows/test-pr.yml

@@ -58,19 +58,67 @@ jobs:
       - name: 'Run unit tests'
         run: make cov-unit
 
+  profile:
+    needs: code-quality-checks
+    name: 'Profiling'
+    runs-on: [self-hosted, linux, normal]
+    strategy:
+      matrix:
+        backend: ['legacy', 'booster']
+    timeout-minutes: 15
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          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 kevm-dist --verbose build -j`nproc` plugin foundry'
+      - name: 'Run profiling'
+        run: |
+          PROF_ARGS=
+          [ ${{ matrix.backend }} == 'booster' ] && PROF_ARGS=--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]
+    strategy:
+      matrix:
+        backend: ['legacy', 'booster']
+    timeout-minutes: 150
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          fetch-depth: 0
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
-          container-name: kontrol-ci-${{ github.sha }}
+          container-name: control-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 kevm-dist --verbose build -j`nproc` plugin foundry'
       - name: 'Run integration tests'
-        run: docker exec --user user kontrol-ci-${GITHUB_SHA} make cov-integration
+        run: |
+          TEST_ARGS=
+          [ ${{ matrix.backend }} == 'booster' ] && TEST_ARGS=--use-booster
+          docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS=${TEST_ARGS}
+        run: |
       - name: 'Tear down Docker'
         if: always()
-        run: docker stop --time 0 kontrol-ci-${GITHUB_SHA}
+        run: |
+          docker stop --time=0 kontrol-ci-integration-${GITHUB_SHA}

Makefile

@@ -54,6 +54,15 @@ cov-integration: TEST_ARGS += --cov-report=html:cov-integration-html $(COV_ARGS)
 cov-integration: test-integration
 
 
+# Profiling
+
+PROF_ARGS :=
+
+profile: poetry-install
+	$(POETRY_RUN) pytest src/tests/profiling --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(PROF_ARGS)
+	find /tmp/pytest-of-$$(whoami)/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
+
+
 # Checks and formatting
 
 format: autoflake isort black

deps/k_release

@@ -1 +1 @@
-6.0.27
+6.0.69