Experimental updates for Oct 2024.

GaloisInc · Oct 17, 2024 · 96cf4d1 · 96cf4d1
1 parent e24bfdb
commit 96cf4d1
Showing 1 changed file with 361 additions and 0 deletions.
diff --git a/Dockerfile-2024 b/Dockerfile-2024
@@ -0,0 +1,361 @@
+#    Copyright 2021, 2022, 2023 Galois, Inc.
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+
+# Base
+FROM ubuntu:22.04 as base
+ARG DEBIAN_FRONTEND=noninteractive
+RUN mkdir /tools
+WORKDIR /
+
+RUN apt-get update && apt-get upgrade -y
+RUN apt-get install -y wget git python3 pip \
+    python3-dev software-properties-common \
+    iproute2 usbutils srecord \
+    build-essential clang bison flex \
+    libreadline-dev gawk tcl-dev libffi-dev git \
+    graphviz xdot pkg-config python3 libboost-system-dev \
+    libboost-python-dev libboost-filesystem-dev zlib1g-dev \
+    libboost-all-dev python3-pip \
+    cmake openocd \
+    libeigen3-dev qtbase5-dev qtchooser qt5-qmake qtbase5-dev-tools \
+    autoconf automake autotools-dev curl libmpc-dev \
+    libmpfr-dev libgmp-dev texinfo gperf \
+    libtool patchutils bc zlib1g-dev libexpat-dev \
+    libftdi-dev unzip libffi7 \
+    libftdi1-2 libftdi1-dev libhidapi-libusb0 libhidapi-dev libudev-dev make g++ \
+    libc++-dev libc++abi-dev nodejs python2 npm \
+    iverilog verilator \
+    vim mercurial libboost-program-options-dev \
+    texlive-full pandoc
+
+# Builder
+FROM base as builder
+ARG VERSION_LOG=/tools/log.txt
+RUN echo "Installed tools:" >> ${VERSION_LOG}
+
+# Yosys
+ARG TOOL=yosys
+ARG TAG=yosys-0.46
+ARG REPO=https://github.com/YosysHQ/yosys.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    git checkout ${TAG} \
+    && make -j$(nproc) \
+    && make install PREFIX=/opt
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Trellis
+ARG TOOL=prjtrellis
+ARG TAG=1.4
+ARG REPO=https://github.com/YosysHQ/prjtrellis.git
+RUN git clone --recursive ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}/libtrellis
+RUN \
+    git checkout ${TAG} \
+    && cmake -DCMAKE_INSTALL_PREFIX=/opt . \
+    && make -j$(nproc) \
+    && make install
+ENV TRELLIS="/opt/share/trellis"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# nextpnr
+ARG TOOL=nextpnr
+ARG TAG=nextpnr-0.7
+ARG REPO=https://github.com/YosysHQ/nextpnr.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    git checkout ${TAG} \
+    && cmake . -DARCH=ecp5 -DTRELLIS_INSTALL_PREFIX=/opt \
+    && make -j$(nproc) \
+    && make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# RISCV toolchain
+ARG TOOL=riscv-gnu-toolchain
+ARG TAG=2024.09.03
+ARG REPO=https://github.com/riscv/riscv-gnu-toolchain
+RUN git clone --recursive ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    git checkout ${TAG} \
+    &&  ./configure --prefix=/opt/riscv --enable-multilib \
+    && export MAKEFLAGS="-j$(nproc)" \
+    && make \
+    && make linux
+ENV PATH="/opt/riscv/bin:/opt/bin:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# ecpprog
+ARG TOOL=ecpprog
+ARG TAG=8af8863855599f4b8ef8f46a336408b1aba60e9d
+ARG REPO=https://github.com/gregdavill/ecpprog
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}/ecpprog
+RUN \
+    git checkout ${TAG} \
+    && make -j$(nproc) \
+    && make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Iverilog
+RUN echo "`iverilog -v | head -1`" >> ${VERSION_LOG}
+
+# Bluespec compiler
+ARG TOOL=bsc
+ARG TAG=2024.07
+ARG REPO=https://github.com/B-Lang-org/bsc
+WORKDIR /tmp
+# https://github.com/B-Lang-org/bsc/releases/download/2024.07/bsc-2024.07-ubuntu-22.04.tar.gz
+RUN \
+    wget ${REPO}/releases/download/${TAG}/${TOOL}-${TAG}-ubuntu-22.04.tar.gz \
+    && tar xvzf ${TOOL}-${TAG}-ubuntu-22.04.tar.gz \
+    && mv ${TAG} /tools/${TAG} \
+    && rm ${TAG}.tar.gz
+ENV PATH="/tools/${TAG}/bin:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Verilator
+RUN echo "`verilator --version`" >> ${VERSION_LOG}
+
+# OpenFPGAloader
+ARG TOOL=openFPGALoader
+ARG TAG=v0.12.1
+ARG REPO=https://github.com/trabucayre/openFPGALoader.git
+RUN \
+    git clone ${REPO} /tmp/${TOOL} \
+    && cd /tmp/${TOOL} \
+    && git checkout ${TAG}
+RUN mkdir /tmp/${TOOL}/build
+WORKDIR /tmp/${TOOL}/build
+RUN \
+    cmake ../ \
+    && cmake --build . \
+    && make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# NOTE: these might be necessary for properly connecting USB devices
+#WORKDIR /tools/${TOOL}
+#RUN cp 99-openfpgaloader.rules /etc/udev/rules.d/
+#RUN udevadm control --reload-rules && sudo udevadm trigger
+#RUN usermod -a $USER -G plugdev
+
+# elf2hex
+ARG TOOL=elf2hex
+ARG TAG=v20.08.00.00
+ARG REPO=https://github.com/sifive/elf2hex.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    git checkout ${TAG} \
+    && autoreconf -i \
+    && ./configure --target=riscv64-unknown-elf \
+    && make \
+    && make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Bluespec libraries
+ARG TOOL=bsc-contrib
+ARG TAG=2024.07
+ARG REPO=https://github.com/B-Lang-org/bsc-contrib.git
+RUN git clone ${REPO} /tools/${TOOL}
+WORKDIR /tools/${TOOL}
+RUN \
+    git checkout ${TAG} \
+    && make PREFIX=/tools/bsc-2024.07-ubuntu-22.04/
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# GHC and Cabal
+RUN \
+    wget https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -O /usr/local/bin/ghcup \
+    && chmod +x /usr/local/bin/ghcup
+ENV PATH="/root/.ghcup/bin:${PATH}"
+RUN \
+    ghcup install ghc 8.10.7 \
+    && ghcup set ghc 8.10.7 \
+    && ghcup install cabal
+RUN cabal update
+
+# Cryptol 3.2.0
+# Why build Cryptol?
+ARG TOOL=cryptol
+ARG TAG=3.2.0
+ARG REPO=https://github.com/GaloisInc/cryptol.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+# Build fix
+#RUN echo "constraints:" > cabal.project.local
+#RUN echo "  parameterized-utils < 2.1.6" >> cabal.project.local
+RUN \
+    git checkout ${TAG} \
+    && git submodule update --init \
+    && ./cry build \
+    && cabal v2-install --installdir=/tools
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Z3 solver
+ARG TOOL=z3
+ARG TAG=z3-4.13.3
+# z3-4.13.3-x64-glibc-2.35.zip
+# https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip
+ARG REPO=https://github.com/Z3Prover/z3/releases/download/${TAG}/${TAG}-x64-glibc-2.35.zip
+WORKDIR /tmp
+RUN wget ${REPO}/${TOOL}-${TAG}.zip
+RUN unzip ${TOOL}-${TAG}.zip
+RUN    mv ${TOOL}-${TAG} /tools/${TOOL}
+ENV PATH="/tools/${TOOL}/bin:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# SAW
+# Why build SAW?
+ARG TOOL=saw
+ARG TAG=v1.2
+ARG REPO=https://github.com/GaloisInc/saw-script.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN git checkout ${TAG} \
+    && git submodule update --init \
+    && ./build.sh \
+    && cp bin/saw /usr/local/bin
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+########################################
+# Riscv-formal
+#######################################
+ARG TOOL=SymbiYosys
+ARG TAG=yosys-0.46
+ARG REPO=https://github.com/YosysHQ/SymbiYosys.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Why build Yices?
+ARG TOOL=yices2
+ARG TAG=Yices-2.6.5
+ARG REPO=https://github.com/SRI-CSL/yices2.git
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN autoconf
+RUN ./configure
+RUN make -j$(nproc)
+RUN make install
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Why build Boolector?
+ARG TOOL=boolector
+ARG TAG=3.2.4
+ARG REPO=https://github.com/boolector/boolectorhttps://github.com/boolector/boolector
+RUN git clone ${REPO} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN ./contrib/setup-btor2tools.sh
+RUN ./contrib/setup-lingeling.sh
+RUN ./configure.sh
+RUN make -C build -j$(nproc)
+RUN cp build/bin/boolector /usr/local/bin/
+RUN cp build/bin/btor* /usr/local/bin/
+RUN cp deps/btor2tools/bin/btorsim /usr/local/bin/
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# NuSMV
+# wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz
+# tar xzf NuSMV-2.6.0-linux64.tar.gz
+# cp NuSMV-2.6.0-Linux/bin/* /usr/local/bin/
+
+# JKind-1
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.2/jkind
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.2/jkind.jar
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.2/jlustre2kind
+# wget https://github.com/andreaskatis/jkind-1/releases/download/v2.2/jrealizability
+# chmod 755 jkind jlustre2kind jrealizability
+# cp * /usr/local/bin/
+
+# Kind 2
+# wget https://github.com/kind2-mc/kind2/releases/download/v2.2.0/kind2-v2.2.0-linux-x86_64.tar.gz
+# tar xzf kind2-v2.2.0-linux-x86_64.tar.gz
+# mv kind2 /usr/local/bin/
+
+# FRET
+# Why build FRET?
+# ARG TOOL=fret
+# ARG TAG=v2.9.0
+# ARG REPO=https://github.com/NASA-SW-VnV/fret.git
+# RUN git clone ${REPO} /tools/${TOOL}
+# WORKDIR /tools/${TOOL}
+# RUN git checkout ${TAG} \
+#     && git submodule update --init
+# WORKDIR /tools/${TOOL}/fret-electron
+# # Change https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/package.json#L249 to "redux-thunk": "^2.4.1" and
+# # https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/package.json#L248 to "redux": :^4"
+# RUN npm run fret-install
+# # NOTE: npm run start still fails, likely because it requires X server which is not availale in Docker
+# RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# Lando/Lobot
+ARG TOOL=lando
+ARG TAG=besspin-v1.0
+ARG REPO=https://github.com/GaloisInc/BESSPIN-Lando.git
+RUN git clone ${REPO} /tools/${TOOL}
+WORKDIR /tools/${TOOL}
+RUN apt-get install -y maven
+RUN ./lando.sh -r
+RUN cd /tools/${TOOL}/source/lobot/ && cabal v2-build
+ENV PATH="/tools/${TOOL}:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# RDE Refinement Finder (aka the DocumentationEnricher)
+ARG TOOL=der
+ARG TAG=0.1.7
+ARG REPO=https://github.com/GaloisInc/RDE_RF
+WORKDIR /tmp
+RUN wget ${REPO}/releases/download/v.${TAG}/${TOOL}-${TAG}.zip
+RUN unzip ${TOOL}-${TAG}.zip
+RUN mv ${TOOL}-${TAG} /tools/${TOOL} && rm ${TOOL}-${TAG}.zip
+ENV PATH="/tools/${TOOL}:${PATH}"
+RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
+
+# cryptol-verilog
+ARG TOOL=cryptol-verilog
+COPY ${TOOL} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    cabal v2-build \
+    && cabal v2-install --installdir=/tools
+
+# Crymp
+ARG TOOL=cryptol-codegen
+COPY ${TOOL} /tmp/${TOOL}
+WORKDIR /tmp/${TOOL}
+RUN \
+    cabal build \
+    && cabal install --installdir=/tools
+
+ENV PATH="/tools/:${PATH}"
+
+# Runner
+FROM base as runner
+COPY --from=builder /opt/ /opt/
+COPY --from=builder /tools/ /tools/
+COPY --from=builder /root/.cabal/ /root/.cabal/
+COPY --from=builder /usr/local/bin/ /usr/local/bin/
+COPY --from=builder /usr/local/lib/python2.7/dist-packages/ /usr/local/lib/python2.7/dist-packages/
+COPY --from=builder /usr/local/share/ /usr/local/share/
+RUN cat ${VERSION_LOG}
+WORKDIR /HARDENS
+
+# Install java so we can run lando
+RUN apt-get install -y default-jre
+
+ENV PATH="/tools/der/bin:/tools/lando:/tools:/tools/z3/bin:/tools/bsc-2021.07-ubuntu-20.04/bin:/opt/riscv/bin:/opt/bin:${PATH}"