diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0887d628..c478880f 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/Dockerfile b/Dockerfile index b18e5503..8d222441 100644 --- a/Dockerfile +++ b/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 diff --git a/README.rst b/README.rst index baf10a9b..91b84991 100644 --- a/README.rst +++ b/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 \ diff --git a/docs/user-manual/build.tex b/docs/user-manual/build.tex index 9ff237d9..5c5f5bf7 100644 --- a/docs/user-manual/build.tex +++ b/docs/user-manual/build.tex @@ -19,7 +19,7 @@ \subsection{Recommended: Docker Container Image} git clone git@github.com: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: diff --git a/docs/user-manual/user-manual.pdf b/docs/user-manual/user-manual.pdf index 5e135aa2..0bd7cea5 100644 Binary files a/docs/user-manual/user-manual.pdf and b/docs/user-manual/user-manual.pdf differ