docker: Improve Kani Docker setup

Signed-off-by: Nick Spinale <[email protected]>
seL4 · May 15, 2024 · 53c051a · 53c051a
1 parent 09708cd
commit 53c051a
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 31 deletions.
diff --git a/hacking/kani/docker/Dockerfile b/hacking/kani/docker/Dockerfile
@@ -10,45 +10,39 @@ RUN apt-get update && apt-get install -y \
     build-essential \
     curl \
     python3-pip \
-    sudo \
-    man \
-    procps \
-    vim \
     bash-completion \
+    man \
+    sudo \
     && rm -rf /var/lib/apt/lists/*
 
-RUN echo '%sudo ALL=(ALL) NOPASSWD:ALL' >> /etc/sudoers
-
 ARG UID
 ARG GID
 
 RUN set -eux; \
-    if ! [ $UID = 0 -a $GID = 0 ]; then \
+    if [ $UID -eq 0 ]; then \
+        [ $GID -eq 0 ]; \
+    else \
         ! getent passwd $UID; \
         if ! getent group $GID; then \
-            groupadd -g $GID x; \
+            groupadd --gid $GID x; \
         fi; \
-        useradd -u $UID -g $GID -G sudo -m -p x x; \
-    fi
-
-ENV RUSTUP_HOME=/opt/rustup
-ENV CARGO_HOME=/opt/cargo
+        useradd --uid $UID --gid $GID --groups sudo --create-home x; \
+    fi;
 
-RUN set -eux; \
-    dirs="$RUSTUP_HOME $CARGO_HOME"; \
-    mkdir -p -m 0755 $dirs; \
-    chown $UID:$GID $dirs
+RUN echo '%sudo ALL=(ALL) NOPASSWD:ALL' >> /etc/sudoers
 
 USER $UID
 
-# Optimize by matching rust-toolchain.toml
-ENV DEFAULT_TOOLCHAIN=nightly-2024-05-01
+ARG TOOLCHAIN
 
-RUN curl -sSf -L https://sh.rustup.rs | \
-        bash -s -- -y --no-modify-path --default-toolchain $DEFAULT_TOOLCHAIN
+RUN set -eux; \
+    if [ $UID -ne 0 ]; then \
+        curl -sSf https://sh.rustup.rs | \
+            bash -s -- -y --no-modify-path --default-toolchain $TOOLCHAIN; \
+    fi;
 
-ENV PATH=$CARGO_HOME/bin:$PATH
+ENV PATH=/home/x/.cargo/bin:/root/.cargo/bin:$PATH
 
-RUN cargo install --locked kani-verifier && cargo kani setup
+RUN cargo install --locked kani-verifier@0.51.0 && cargo kani setup
 
-WORKDIR /work
+WORKDIR /work/hacking/kani
diff --git a/hacking/kani/docker/Makefile b/hacking/kani/docker/Makefile
@@ -5,15 +5,11 @@
 #
 
 work_root := ../../..
-here_relative := hacking/kani
 
 id := rust-sel4-kani
 image_tag := $(id)
 container_name := $(id)
 
-uid := $(shell id -u)
-gid := $(shell id -g)
-
 mount_params := type=bind,src=$(abspath $(work_root)),dst=/work
 
 .PHONY: none
@@ -22,7 +18,9 @@ none:
 .PHONY: build
 build:
 	docker build \
-		--build-arg UID=$(uid) --build-arg GID=$(gid) \
+		--build-arg UID=$$(id -u) \
+		--build-arg GID=$$(id -g) \
+		--build-arg TOOLCHAIN=$$(sed -rn 's,channel = "(.*)",\1,p' $(work_root)/rust-toolchain.toml) \
 		-t $(image_tag) .
 
 .PHONY: runi
@@ -44,16 +42,18 @@ exec:
 
 .PHONY: rm-container
 rm-container:
+	set -e; \
 	for id in $$(docker ps -aq -f "name=^$(container_name)$$"); do \
 		docker rm -f $$id; \
 	done
 
 .PHONY: check
 check: build
+	set -e; \
 	if [ -t 0 ]; then \
 		tty_args="-it"; \
-	fi && \
+	fi; \
 	docker run --rm $$tty_args \
 		--mount $(mount_params),readonly \
 		$(image_tag) \
-		make -C $(here_relative) check BUILD=/tmp/build
+		make check BUILD=/tmp/build