Merge pull request #454 from GaloisInc/bd/dockerfile-cleanups

Dockerfile cleanups

.github/workflows/main.yml

@@ -41,9 +41,12 @@ jobs:
             docker pull artifactory.galois.com:5025/pate/pate:refs-heads-master || \
             echo "No latest image found"
 
+      # Docker on our self-hosted runners doesn't populate TARGETPLATFORM so we
+      # set it manually via build-arg. We need this to pass our platform check
+      # in the Dockerfile.
       - name: Build Docker Image
         run: |
-          docker build . \
+          docker build --platform linux/amd64 --build-arg TARGETPLATFORM=linux/amd64 . \
             --cache-from artifactory.galois.com:5025/pate/pate:${GITHUB_REF//\//\-} \
             --cache-from artifactory.galois.com:5025/pate/pate:refs-heads-master \
             -t pate

Dockerfile

@@ -1,5 +1,8 @@
 ## Clone git into image
-FROM --platform=linux/amd64 ubuntu:20.04 as gitbase
+FROM ubuntu:20.04 AS gitbase
+
+ARG TARGETPLATFORM
+RUN if [ "${TARGETPLATFORM}" != "linux/amd64" ]; then echo "TARGETPLATFORM '${TARGETPLATFORM}' is not supported, use '--platform linux/amd64'"; exit 1; fi
 
 RUN apt update && apt install -y ssh
 RUN apt install -y git
@@ -30,7 +33,7 @@ RUN find . -name .gitignore -exec rm {} \;
 
 
 ## Build project in image
-FROM --platform=linux/amd64 ubuntu:20.04
+FROM ubuntu:20.04
 ENV GHC_VERSION=9.6.2
 ENV TZ=America/Los_Angeles
 RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone
@@ -43,13 +46,13 @@ RUN apt-get install -y yices2
 
 RUN curl https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -o /usr/bin/ghcup && chmod +x /usr/bin/ghcup
 RUN mkdir -p /root/.ghcup && ghcup install-cabal
-RUN ghcup install ghc ${GHC_VERSION} && ghcup set ghc ${GHC_VERSION} 
+RUN ghcup install ghc ${GHC_VERSION} && ghcup set ghc ${GHC_VERSION}
 
 RUN apt install locales
 RUN locale-gen en_US.UTF-8
-ENV LANG en_US.UTF-8
-ENV LANGUAGE en_US:en
-ENV LC_ALL en_US.UTF-8
+ENV LANG=en_US.UTF-8
+ENV LANGUAGE=en_US:en
+ENV LC_ALL=en_US.UTF-8
 
 
 ######################################################################
@@ -82,7 +85,7 @@ RUN cabal v2-build what4
 # crucible
 COPY --from=gitbase /home/src/submodules/crucible /home/src/submodules/crucible
 RUN cabal v2-build crucible
- 
+
 # arm-asl-parser
 COPY --from=gitbase /home/src/submodules/arm-asl-parser /home/src/submodules/arm-asl-parser
 RUN cabal v2-build asl-parser
@@ -114,7 +117,7 @@ RUN cabal v2-build binary-symbols flexdis86
 #mutual dependency between these submodules
 # macaw
 COPY --from=gitbase /home/src/submodules/macaw /home/src/submodules/macaw
- 
+
 # macaw-loader
 COPY --from=gitbase /home/src/submodules/macaw-loader /home/src/submodules/macaw-loader
 RUN cabal v2-build macaw-base macaw-loader macaw-semmc

README.rst

@@ -12,7 +12,7 @@ The fastest way to get started is to build the Docker image and use the tool via
 
 First, build the Docker image with the command::
 
-  docker build . -t pate
+  docker build --platform linux/amd64 . -t pate
 
 Next, run the verifier on an example::
 
@@ -87,7 +87,7 @@ The verifier accepts the following command line arguments::
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --assume-stack-scope     Add additional assumptions about stack frame scoping 
+  --assume-stack-scope     Add additional assumptions about stack frame scoping
                            during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
   --always-classify-return Always resolve classifier failures by assuming
@@ -107,13 +107,14 @@ If you have a ``tar`` file of a Docker image of the verifier, you can install it
 
 To run the verifier via Docker after this::
 
-  docker run --rm -it pate --help
+  docker run --rm -it --platform linux/amd64 pate --help
 
 To make use of the verifier with Docker, it is useful to map a directory on your local filesystem into the Docker container to be able to save output files. Assuming that your original and patched binaries are ``original.exe`` and ``patched.exe``, respectively::
 
   mkdir VerifierData
   cp original.exe patched.exe VerifierData/
-  docker run --rm -it -v `pwd`/VerifierData`:/VerifierData pate \
+  docker run --rm -it --platform linux/amd64 \
+             -v `pwd`/VerifierData`:/VerifierData pate \
              --original /VerifierData/original.exe \
              --patched /VerifierData/patched.exe \
              --proof-summary-json /VerifierData/report.json \

docs/user-manual/build.tex

@@ -19,7 +19,7 @@ \subsection{Recommended: Docker Container Image}
   git clone [email protected]:GaloisInc/pate.git
   cd pate
   git submodule update --init
-  docker build . -t pate
+  docker build --platform linux/amd64 . -t pate
 \end{verbatim}
 
 \pate{} may subsequently be used via Docker, such as: