-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Showing
2 changed files
with
120 additions
and
117 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,7 +2,6 @@ dist-newstyle/ | |
dist/ | ||
Dockerfile* | ||
cabal.project.local* | ||
.git/ | ||
.github/ | ||
.gitmodules | ||
.tags | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,196 +1,200 @@ | ||
FROM --platform=linux/amd64 ubuntu:20.04 | ||
## Clone git into image | ||
FROM --platform=linux/amd64 ubuntu:20.04 as gitbase | ||
|
||
RUN apt update && apt install -y ssh | ||
RUN apt install -y git | ||
|
||
RUN mkdir /home/src-git | ||
COPY ./.git /home/src-git/.git | ||
|
||
WORKDIR /home/src-git | ||
RUN git rev-parse HEAD > /tmp/git-rev | ||
RUN git clone --depth=1 /home/src-git /home/src | ||
WORKDIR /home/src | ||
RUN git checkout $(cat /tmp/git-rev) | ||
|
||
RUN git config --global protocol.file.allow always | ||
|
||
RUN sed -i "s/url = https:\/\/github.com\/.*\/\(.*\)\.git/url = \/home\/src-git\/.git\/modules\/submodules\/\1/g" .gitmodules | ||
RUN sed -i "s/url = [email protected]:.*\/\(.*\)\.git/url = \/home\/src-git\/.git\/modules\/submodules\/\1/g" .gitmodules | ||
|
||
RUN mv /home/src-git/.git/modules/tools/pate/static/* /home/src-git/.git/modules/submodules/ | ||
# RUN git config --global url."https://github.com/".insteadOf "[email protected]:" | ||
RUN git submodule update --init | ||
|
||
# delete all git files, since we don't want to copy them | ||
RUN find . -name .git -exec rm {} \; | ||
RUN find . -name .gitmodules -exec rm {} \; | ||
RUN find . -name .gitignore -exec rm {} \; | ||
|
||
FROM --platform=linux/amd64 ubuntu:20.04 as solver-base | ||
|
||
ENV TZ=America/Los_Angeles | ||
RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone | ||
RUN apt update && apt install -y software-properties-common apt-transport-https ca-certificates wget | ||
RUN apt install -y curl zlibc zlib1g zlib1g-dev git zip \ | ||
libgmp3-dev build-essential libtinfo-dev autoconf automake gperf cmake locales \ | ||
python3-distutils python-setuptools antlr3 libantlr3c-dev libtool libtool-bin libboost-all-dev python3-pip \ | ||
libfftw3-dev && \ | ||
locale-gen en_US.UTF-8 && \ | ||
pip3 install toml | ||
|
||
RUN apt update && apt install -y zlibc zlib1g libgmp10 libantlr3c-3.4-0 locales && locale-gen en_US.UTF-8 | ||
RUN apt update && \ | ||
apt install -y software-properties-common curl zlibc zlib1g zlib1g-dev git libgmp3-dev build-essential # Version 1 | ||
|
||
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 | ||
|
||
###################################################################### | ||
# Sorry, Docker uses Debian, but SRI builds for Ubuntu, so these won't work: | ||
# RUN add-apt-repository ppa:sri-csl/formal-methods | ||
# RUN apt-get update | ||
# RUN apt-get install -y yices2 | ||
|
||
RUN apt install autoconf gperf --yes | ||
RUN mkdir -p /home/yices2/src; \ | ||
git clone https://github.com/SRI-CSL/yices2.git /home/yices2/src && \ | ||
(cd /home/yices2/src; \ | ||
git checkout Yices-2.6.2 && \ | ||
git checkout Yices-2.6.1 && \ | ||
autoconf && \ | ||
./configure && \ | ||
make -j4 && \ | ||
make -j && \ | ||
make install) | ||
|
||
###################################################################### | ||
# Similarly, this won't work for Z3: | ||
# RUN apt-get install -y z3 | ||
|
||
RUN apt install -y cmake python3-distutils python-setuptools | ||
RUN mkdir -p /home/z3/src; \ | ||
git clone https://github.com/Z3Prover/z3.git /home/z3/src && \ | ||
cd /home/z3/src && \ | ||
git checkout z3-4.8.10 && \ | ||
git checkout z3-4.8.3 && \ | ||
mkdir -p /home/z3/bld && \ | ||
(cd /home/z3/bld; \ | ||
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release -DUSE_OPENMP=ON /home/z3/src -DUSE_LIB_GMP=FALSE -DBUILD_LIBZ3_SHARED=OFF /home/z3/src && \ | ||
make -j4 && \ | ||
make && \ | ||
make install) | ||
|
||
RUN apt update && apt install -y antlr3 libantlr3c-dev libtool libtool-bin libboost-dev | ||
RUN mkdir -p /home/cvc4/src; \ | ||
git clone https://github.com/CVC4/CVC4.git /home/cvc4/src && \ | ||
cd /home/cvc4/src && \ | ||
git checkout 1.8 && \ | ||
bash contrib/get-antlr-3.4 && \ | ||
bash contrib/get-cadical && \ | ||
bash contrib/get-kissat && \ | ||
(./configure.sh --cadical --kissat --static --static-binary && \ | ||
cd build && \ | ||
make -j4 && \ | ||
make install) | ||
git checkout 1.6 && \ | ||
(./autogen.sh && \ | ||
./configure && \ | ||
make && \ | ||
make install) | ||
|
||
## Build project in image | ||
FROM --platform=linux/amd64 ubuntu:20.04 | ||
ENV GHC_VERSION=9.2.8 | ||
ENV TZ=America/Los_Angeles | ||
RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone | ||
RUN apt update && \ | ||
apt install -y software-properties-common curl zlibc zlib1g zlib1g-dev git libgmp3-dev build-essential # Version 1 | ||
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 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 | ||
|
||
RUN curl -L https://downloads.haskell.org/~ghcup/0.1.16/x86_64-linux-ghcup-0.1.16 -o /usr/bin/ghcup && chmod +x /usr/bin/ghcup | ||
RUN mkdir -p /root/.ghcup && ghcup --version && ghcup install cabal && ghcup install ghc 8.10.7 && ghcup set ghc 8.10.7 | ||
|
||
###################################################################### | ||
ENV PATH="/root/.ghcup/bin:${PATH}" | ||
RUN cabal update | ||
|
||
# Ensure that submodule remotes use https instead of ssh so we can pull | ||
# them without setting up ssh credentials | ||
RUN git config --global url."https://github.com/".insteadOf "[email protected]:" | ||
RUN git config --global url."https://".insteadOf "git://" | ||
# Get a fresh repo clone to avoid local changes | ||
# This ADD is to ensure the cache updates if this repo changes | ||
|
||
RUN git clone --depth=1 https://github.com/GaloisInc/pate.git /home/src | ||
RUN cabal v2-update | ||
RUN mkdir -p /home/src | ||
RUN mkdir -p /home/src/submodules | ||
|
||
COPY --from=gitbase /home/src/cabal.project.dist /home/src/cabal.GHC-${GHC_VERSION}.freeze /home/src/ | ||
WORKDIR /home/src | ||
|
||
RUN cp cabal.GHC-${GHC_VERSION}.freeze cabal.project.freeze | ||
RUN cp cabal.project.dist cabal.project | ||
RUN cp cabal.GHC-8.10.7.freeze cabal.project.freeze | ||
RUN sed -i "1s/.*/optional-packages:/" cabal.project | ||
RUN cabal v2-configure --ghc-options="-fno-safe-haskell" | ||
|
||
# The pattern below allows us to incrementally build the submodules | ||
# for this project, where each individual step only depends on the | ||
# specific revision on the master branch for pate. | ||
# In particular, this allows us to cache the builds for the | ||
# revisions of these submodules. | ||
RUN cabal --version ; ghc --version | ||
|
||
# We don't need to cache all submodule builds, this step is | ||
# optional and intended to avoid re-building large packages | ||
# (e.g. macaw-aarch32). After these cached steps, the full set | ||
# of submodules is checked out in order to finish the build. | ||
RUN sed -i "1s/.*/optional-packages:/" cabal.project | ||
|
||
# Notably, these cached steps can be safely deleted as they are purely | ||
# an optimization. | ||
# llvm-pretty | ||
COPY --from=gitbase /home/src/submodules/llvm-pretty /home/src/submodules/llvm-pretty | ||
RUN cabal v2-build llvm-pretty | ||
|
||
# parameterized-utils | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/parameterized-utils parameterized-utils.json | ||
RUN git submodule update --init -- submodules/parameterized-utils | ||
COPY --from=gitbase /home/src/submodules/parameterized-utils /home/src/submodules/parameterized-utils | ||
RUN cabal v2-build parameterized-utils | ||
|
||
# what4 | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/what4 what4.json | ||
RUN git submodule update --init -- submodules/what4 | ||
COPY --from=gitbase /home/src/submodules/what4 /home/src/submodules/what4 | ||
RUN cabal v2-build what4 | ||
|
||
# llvm-pretty | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/llvm-pretty llvm-pretty.json | ||
RUN git submodule update --init -- submodules/llvm-pretty | ||
RUN cabal v2-build llvm-pretty | ||
|
||
# crucible | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/crucible crucible.json | ||
RUN git submodule update --init -- submodules/crucible | ||
COPY --from=gitbase /home/src/submodules/crucible /home/src/submodules/crucible | ||
RUN cabal v2-build crucible | ||
|
||
# what4-serialize | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/what4-serialize what4-serialize.json | ||
RUN git submodule update --init -- submodules/what4-serialize | ||
RUN cabal v2-build what4-serialize | ||
|
||
|
||
# arm-asl-parser | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/arm-asl-parser arm-asl-parser.json | ||
RUN git submodule update --init -- submodules/arm-asl-parser | ||
COPY --from=gitbase /home/src/submodules/arm-asl-parser /home/src/submodules/arm-asl-parser | ||
RUN cabal v2-build asl-parser | ||
|
||
# dismantle | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/dismantle dismantle.json | ||
RUN git submodule update --init -- submodules/dismantle | ||
COPY --from=gitbase /home/src/submodules/dismantle /home/src/submodules/dismantle | ||
RUN cabal v2-build dismantle-tablegen dismantle-arm-xml dismantle-ppc | ||
|
||
# what4-serialize | ||
COPY --from=gitbase /home/src/submodules/what4-serialize /home/src/submodules/what4-serialize | ||
RUN cabal v2-build what4-serialize | ||
|
||
# asl-translator | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/asl-translator asl-translator.json | ||
RUN git submodule update --init -- submodules/asl-translator | ||
COPY --from=gitbase /home/src/submodules/asl-translator /home/src/submodules/asl-translator | ||
RUN cabal v2-build asl-translator | ||
|
||
# elf-edit | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/elf-edit elf-edit.json | ||
RUN git submodule update --init -- submodules/elf-edit | ||
COPY --from=gitbase /home/src/submodules/elf-edit /home/src/submodules/elf-edit | ||
RUN cabal v2-build elf-edit | ||
|
||
# semmc | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/semmc semmc.json | ||
RUN git submodule update --init -- submodules/semmc | ||
RUN cabal v2-build semmc semmc-aarch32 semmc-ppc | ||
COPY --from=gitbase /home/src/submodules/semmc /home/src/submodules/semmc | ||
RUN cabal v2-build semmc semmc-aarch32 semmc-ppc semmc-synthesis semmc-learning | ||
|
||
# dwarf | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/dwarf dwarf.json | ||
RUN git submodule update --init -- submodules/dwarf | ||
# galois-dwarf | ||
COPY --from=gitbase /home/src/submodules/dwarf /home/src/submodules/dwarf | ||
RUN cabal v2-build galois-dwarf | ||
|
||
# flexdis86 | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/flexdis86 flexdis86.json | ||
RUN git submodule update --init -- submodules/flexdis86 | ||
RUN cabal v2-build binary-symbols | ||
COPY --from=gitbase /home/src/submodules/flexdis86 /home/src/submodules/flexdis86 | ||
RUN cabal v2-build binary-symbols flexdis86 | ||
|
||
#mutual dependency between these submodules | ||
# macaw | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/macaw macaw.json | ||
RUN git submodule update --init -- submodules/macaw | ||
|
||
COPY --from=gitbase /home/src/submodules/macaw /home/src/submodules/macaw | ||
|
||
# macaw-loader | ||
ADD https://api.github.com/repos/GaloisInc/pate/contents/submodules/macaw-loader macaw-loader.json | ||
RUN git submodule update --init -- submodules/macaw-loader | ||
RUN cabal v2-build macaw-base 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 | ||
|
||
RUN cabal v2-build macaw-ppc macaw-loader-ppc | ||
RUN cabal v2-build macaw-x86 macaw-loader-x86 | ||
RUN cabal v2-build macaw-aarch32 macaw-loader-aarch32 | ||
|
||
# This step is a catch-all that builds the rest of the project | ||
# dependencies. | ||
# Notably these submodules may be stale in the cache, but | ||
# the next step ensures everything is brought up to date. | ||
RUN git submodule update --init | ||
RUN cp cabal.project.dist cabal.project | ||
RUN cabal v2-build lib:pate --only-dependencies | ||
|
||
# After the cached submodule steps, we now add the dependency on the current pate revision, so | ||
# any changes to non-cached submodules (or pate itself) are captured. | ||
ADD https://api.github.com/repos/GaloisInc/pate/git/refs/heads/master version.json | ||
# Notably our previous 'git clone' was not guarded with the above, and so the | ||
# cache may be stale. We run 'git pull' to ensure the repository is up to date. | ||
RUN git pull | ||
RUN git submodule update --init | ||
RUN cp cabal.project.dist cabal.project | ||
RUN cabal v2-build pate-repl-base | ||
|
||
FROM --platform=linux/amd64 ubuntu:20.04 | ||
COPY --from=gitbase /home/src/pate.cabal /home/src/pate.cabal | ||
|
||
RUN apt update && apt install -y build-essential libgmp3-dev libtinfo-dev zlib1g-dev zlibc zlib1g libgmp10 libantlr3c-3.4-0 locales && locale-gen en_US.UTF-8 | ||
ENV LANG en_US.UTF-8 | ||
ENV LANGUAGE en_US:en | ||
ENV LC_ALL en_US.UTF-8 | ||
RUN cp cabal.project.dist cabal.project | ||
RUN cabal v2-build pkg:pate --only-dependencies | ||
|
||
COPY --from=0 /usr/local/bin/cvc4 \ | ||
/usr/local/bin/z3 \ | ||
/usr/local/bin/yices \ | ||
/usr/local/bin/yices-smt2 \ | ||
/usr/local/bin/ | ||
COPY --from=gitbase /home/src/src /home/src/src | ||
COPY --from=gitbase /home/src/arch /home/src/arch | ||
COPY --from=gitbase /home/src/tools /home/src/tools | ||
COPY --from=gitbase /home/src/tests /home/src/tests | ||
COPY --from=gitbase /home/src/pate.sh /home/src/pate.sh | ||
|
||
COPY --from=0 /root/.ghcup /root/.ghcup | ||
COPY --from=0 /root/.cabal /root/.cabal | ||
COPY --from=0 /home/src /home/src | ||
RUN cabal v2-build pate-repl-base | ||
|
||
ENV PATH="/home/src/:/root/.ghcup/bin:${PATH}" | ||
|
||
COPY --from=gitbase /home/src/loadrepl.ghci /home/src/loadrepl.ghci | ||
RUN apt install -y libtinfo5 libtinfo-dev | ||
ENTRYPOINT ["/home/src/pate.sh"] | ||
|
||
|