From 3d9a7b64adef359a5aab8131445ae4eee647bb82 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Mon, 4 Nov 2024 19:56:53 -0800 Subject: [PATCH 1/9] Simplify the docker build, and properly build a multiplatform image with docker build actions --- .github/workflows/docker.yml | 20 ++++++++++---------- Dockerfile.deps => Dockerfile | 10 ++++++++-- Dockerfile.dev-env | 15 --------------- Dockerfile.release | 7 ------- Makefile_docker | 22 ---------------------- 5 files changed, 18 insertions(+), 56 deletions(-) rename Dockerfile.deps => Dockerfile (61%) delete mode 100644 Dockerfile.dev-env delete mode 100644 Dockerfile.release delete mode 100644 Makefile_docker diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index b8c8fd90e..e578a2c6b 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -15,12 +15,10 @@ concurrency: group: docker-${{ github.workflow }}-${{ github.ref }} cancel-in-progress: false +# Instructions from https://depot.dev/blog/multi-platform-docker-images-in-github-actions jobs: deploy-docker: runs-on: ubuntu-latest - strategy: - matrix: - platform: [linux/amd64, linux/arm64] permissions: packages: write contents: read @@ -40,11 +38,13 @@ jobs: uses: docker/setup-qemu-action@v3 - name: Set up Docker Buildx uses: docker/setup-buildx-action@v3 - - name: Build the Docker image - run: | - echo "Building ${{env.CERBERUS_IMAGE_ID}}" - PLATFORM=${{ matrix.platform }} make -f Makefile_docker release_cn - docker tag cn:release ${{env.CERBERUS_IMAGE_ID}} - - name: Push the Docker image - run: docker push ${{env.CERBERUS_IMAGE_ID}} + - name: Build multi-platform image + uses: docker/build-push-action@v5 + with: + context: . + platforms: linux/amd64,linux/arm64 + push: true + tags: ${{env.CERBERUS_IMAGE_ID}} + cache-from: type=gha + cache-to: type=gha,mode=max diff --git a/Dockerfile.deps b/Dockerfile similarity index 61% rename from Dockerfile.deps rename to Dockerfile index 3cf30851c..0df15e1cd 100644 --- a/Dockerfile.deps +++ b/Dockerfile @@ -1,4 +1,5 @@ -FROM ubuntu:22.04 +# Build image with all dependencies +FROM ubuntu:22.04 as deps RUN apt-get update RUN apt-get upgrade -y @@ -15,4 +16,9 @@ RUN eval `opam env` \ && make install \ && make install_cn -WORKDIR /opt \ No newline at end of file +WORKDIR /opt + +COPY docker_entry_point.sh /opt/docker_entry_point.sh +RUN chmod +x /opt/docker_entry_point.sh +WORKDIR /data +ENTRYPOINT ["/opt/docker_entry_point.sh"] diff --git a/Dockerfile.dev-env b/Dockerfile.dev-env deleted file mode 100644 index 3b240c135..000000000 --- a/Dockerfile.dev-env +++ /dev/null @@ -1,15 +0,0 @@ -FROM cerberus:deps - -#COPY --chown=user1 . /home/opam/cerberus/ -#RUN eval `opam env` && \ -# cd /home/opam/cerberus/ && \ -# make && \ -# make install -#COPY --chown=user1 docker_entry_point.sh /home/user1/ -#RUN chmod +x docker_entry_point.sh -#WORKDIR /data - -RUN echo 'export PS1="[\u@docker] \W # "' >> /home/user1/.bashrc -RUN echo 'eval $(opam env)' >> /home/user1/.bashrc - -ENTRYPOINT ["bash"] diff --git a/Dockerfile.release b/Dockerfile.release deleted file mode 100644 index 9645a6309..000000000 --- a/Dockerfile.release +++ /dev/null @@ -1,7 +0,0 @@ -FROM cerberus:deps - -RUN rm -rf /opt/cerberus -COPY docker_entry_point.sh /opt/docker_entry_point.sh -RUN chmod +x /opt/docker_entry_point.sh -WORKDIR /data -ENTRYPOINT ["/opt/docker_entry_point.sh"] diff --git a/Makefile_docker b/Makefile_docker deleted file mode 100644 index f809b44a2..000000000 --- a/Makefile_docker +++ /dev/null @@ -1,22 +0,0 @@ -.PHONY: all release dev-env deps - -PLATFORM ?= linux/amd64 -$(info Building for platform $(PLATFORM)) - -all: - @echo 'targets: deps|release|dev-env' - -deps : - docker build --platform $(PLATFORM) --tag cerberus:deps -f Dockerfile.deps . - -release: deps - docker build --platform $(PLATFORM) --tag cerberus:release -f Dockerfile.release . - @echo 'for example: docker run --volume `PWD`:/data/ cerberus:release cerberus tests/tcc/00_assignment.c --pp=core' - -release_cn: deps - docker build --platform $(PLATFORM) --tag cn:release -f Dockerfile.release . - @echo 'for example: docker run --volume `PWD`:/data/ cn:release cerberus tests/tcc/00_assignment.c --pp=core' - -dev-env: deps - docker build --platform $(PLATFORM) --tag cerberus:dev-env -f Dockerfile.dev-env . - @echo 'for example: docker run -ti --volume `PWD`:/home/user1/cerberus/ cerberus:dev-env' From 5afd2805a0367d50c4986943f2c505688d7c6de3 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 11:43:39 -0800 Subject: [PATCH 2/9] Temporarily disable scheduled docker build for faster testing --- .github/workflows/docker.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index e578a2c6b..719861b1c 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -1,8 +1,9 @@ name: docker on: - schedule: - - cron: '30 18 * * *' + pull_request: + # schedule: + # - cron: '30 18 * * *' env: CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release From 31f2e19395eb57b3ea53ec25444013d5928c42e2 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 14:45:22 -0800 Subject: [PATCH 3/9] Clean up the release docker image --- Dockerfile => Dockerfile.ubuntu | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) rename Dockerfile => Dockerfile.ubuntu (89%) diff --git a/Dockerfile b/Dockerfile.ubuntu similarity index 89% rename from Dockerfile rename to Dockerfile.ubuntu index 0df15e1cd..4fb0204e4 100644 --- a/Dockerfile +++ b/Dockerfile.ubuntu @@ -1,5 +1,5 @@ -# Build image with all dependencies -FROM ubuntu:22.04 as deps +# Build a minimal release image +FROM ubuntu:22.04 RUN apt-get update RUN apt-get upgrade -y @@ -12,6 +12,7 @@ RUN opam install dune lem ADD . /opt/cerberus WORKDIR /opt/cerberus RUN opam install --deps-only ./cerberus-lib.opam ./cn.opam + RUN eval `opam env` \ && make install \ && make install_cn From 45da802268991171ea5db6f080097e8b87a18d42 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 14:45:46 -0800 Subject: [PATCH 4/9] Add a separate job for RedHat docker image --- .github/workflows/docker.yml | 42 +++++++++++++++++++++++++++++++----- 1 file changed, 37 insertions(+), 5 deletions(-) diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index 719861b1c..d3b199f15 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -6,7 +6,7 @@ on: # - cron: '30 18 * * *' env: - CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn:release + CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn # Cancelling an in-progress job when a new push is performed causes the CI to # show up as failed: https://github.com/orgs/community/discussions/8336 @@ -18,7 +18,7 @@ concurrency: # Instructions from https://depot.dev/blog/multi-platform-docker-images-in-github-actions jobs: - deploy-docker: + docker-release-ubuntu: runs-on: ubuntu-latest permissions: packages: write @@ -46,6 +46,38 @@ jobs: context: . platforms: linux/amd64,linux/arm64 push: true - tags: ${{env.CERBERUS_IMAGE_ID}} - cache-from: type=gha - cache-to: type=gha,mode=max + tags: ${{env.CERBERUS_IMAGE_ID}}:release + file: Dockerfile.ubuntu + + docker-release-redhat: + runs-on: ubuntu-latest + permissions: + packages: write + contents: read + attestations: write + id-token: write + steps: + - uses: actions/checkout@v4 + + - name: Login to GitHub Container Registry + uses: docker/login-action@v3 + with: + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + + - name: Set up QEMU + uses: docker/setup-qemu-action@v3 + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v3 + + - name: Build multi-platform image + uses: docker/build-push-action@v5 + with: + context: . + platforms: linux/amd64,linux/arm64 + push: true + tags: ${{env.CERBERUS_IMAGE_ID}}:release-redhat + file: Dockerfile.redhat + attests: type=sbom + provenance: mode=max From 3f676919d0bdbf06d45765a735ac8836ee20456c Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 14:54:23 -0800 Subject: [PATCH 5/9] Added RedHat dockerfile --- Dockerfile.redhat | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 Dockerfile.redhat diff --git a/Dockerfile.redhat b/Dockerfile.redhat new file mode 100644 index 000000000..a621726aa --- /dev/null +++ b/Dockerfile.redhat @@ -0,0 +1,40 @@ +FROM redhat/ubi9:latest + +# Install basic dependencies +RUN yum update -y && \ + yum install -y xz sudo gcc unzip \ + diffutils patch pkgconfig bzip2 \ + git perl wget ca-certificates \ + mpfr-devel gmp-devel m4 + +# Install additional FEDORA packages +# from https://www.cyberciti.biz/faq/install-epel-repo-on-an-rhel-8-x/ +# Currently the FEDORA packages are needed only for Z3 +# NOTE: we might have to eventually use *only* RedHat packages +# which would mean installing Z3 directly from the release page +RUN yum install -y https://dl.fedoraproject.org/pub/epel/epel-release-latest-9.noarch.rpm && \ + yum update -y && \ + yum install -y z3 + +# Install OPAM +# See https://opam.ocaml.org/doc/1.2/Install.html +RUN curl -fsSL https://opam.ocaml.org/install.sh | sh + +ENV OPAMCONFIRMLEVEL=unsafe-yes +RUN opam init --disable-sandboxing +RUN opam install dune lem + +ADD . /opt/cerberus +WORKDIR /opt/cerberus +RUN opam install --deps-only ./cerberus-lib.opam ./cn.opam + +RUN eval `opam env` \ + && make install \ + && make install_cn + +WORKDIR /opt + +COPY docker_entry_point.sh /opt/docker_entry_point.sh +RUN chmod +x /opt/docker_entry_point.sh +WORKDIR /data +ENTRYPOINT ["/opt/docker_entry_point.sh"] From 7bf0f994eb31221d65d6cd84812d158ee94af23d Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 16:41:12 -0800 Subject: [PATCH 6/9] Revert "Temporarily disable scheduled docker build for faster testing" This reverts commit 5afd2805a0367d50c4986943f2c505688d7c6de3. --- .github/workflows/docker.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index d3b199f15..ee73c202d 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -1,9 +1,8 @@ name: docker on: - pull_request: - # schedule: - # - cron: '30 18 * * *' + schedule: + - cron: '30 18 * * *' env: CERBERUS_IMAGE_ID: ghcr.io/rems-project/cerberus/cn From 12c844f91b1ac17edfecf419ef077ba840f4b32c Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 17:06:33 -0800 Subject: [PATCH 7/9] Try to specify github tokens --- .github/workflows/docker.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index ee73c202d..f872e0a3c 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -47,6 +47,7 @@ jobs: push: true tags: ${{env.CERBERUS_IMAGE_ID}}:release file: Dockerfile.ubuntu + github-token: ${{ secrets.GITHUB_TOKEN }} docker-release-redhat: runs-on: ubuntu-latest @@ -80,3 +81,4 @@ jobs: file: Dockerfile.redhat attests: type=sbom provenance: mode=max + github-token: ${{ secrets.GITHUB_TOKEN }} From 72a5c6e01a97d9d3313e1cccab52264dba93ab95 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Wed, 6 Nov 2024 17:06:42 -0800 Subject: [PATCH 8/9] Add CI badges: --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2c3c1bb1e..ab6ccfde2 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Cerberus C semantics -[![CI](https://github.com/rems-project/cerberus/actions/workflows/ci.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci.yml) +[![CI](https://github.com/rems-project/cerberus/actions/workflows/ci.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci.yml) [![CI-CN](https://github.com/rems-project/cerberus/actions/workflows/ci-cn.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn.yml) [![CI-CN-specs-testing](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-spec-testing.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-spec-testing.yml) [![CI-CN-becnhmarks](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-bench.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cn-bench.yml) [![CI-CHERI](https://github.com/rems-project/cerberus/actions/workflows/ci-cheri.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/ci-cheri.yml) [![Docker](https://github.com/rems-project/cerberus/actions/workflows/docker.yml/badge.svg)](https://github.com/rems-project/cerberus/actions/workflows/docker.yml) Web interfaces, papers, and web page From a584f509395753cb4a5a1bec54e5a6aedf82f99c Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 7 Nov 2024 08:18:56 -0800 Subject: [PATCH 9/9] Remove un-needed lines per @dc-mak 's suggestions --- Dockerfile.redhat | 2 -- Dockerfile.ubuntu | 2 -- 2 files changed, 4 deletions(-) diff --git a/Dockerfile.redhat b/Dockerfile.redhat index a621726aa..0c526a306 100644 --- a/Dockerfile.redhat +++ b/Dockerfile.redhat @@ -22,14 +22,12 @@ RUN curl -fsSL https://opam.ocaml.org/install.sh | sh ENV OPAMCONFIRMLEVEL=unsafe-yes RUN opam init --disable-sandboxing -RUN opam install dune lem ADD . /opt/cerberus WORKDIR /opt/cerberus RUN opam install --deps-only ./cerberus-lib.opam ./cn.opam RUN eval `opam env` \ - && make install \ && make install_cn WORKDIR /opt diff --git a/Dockerfile.ubuntu b/Dockerfile.ubuntu index 4fb0204e4..4fe361313 100644 --- a/Dockerfile.ubuntu +++ b/Dockerfile.ubuntu @@ -7,14 +7,12 @@ RUN apt-get install -y opam libgmp-dev libmpfr-dev ENV OPAMCONFIRMLEVEL=unsafe-yes RUN opam init --disable-sandboxing -RUN opam install dune lem ADD . /opt/cerberus WORKDIR /opt/cerberus RUN opam install --deps-only ./cerberus-lib.opam ./cn.opam RUN eval `opam env` \ - && make install \ && make install_cn WORKDIR /opt