Merge pull request #137 from GaloisInc/135-post-release-polishing

post-release polishing

.github/workflows/main.yml

@@ -23,10 +23,7 @@ jobs:
       - name: Prove specs
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make -C saw
@@ -49,7 +46,7 @@ jobs:
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             cp -r /HARDENS/ /tmp
-            make -C /tmp/HARDENS/src -f frama_c.mk
+            make -C /tmp/HARDENS/src -f frama_c.mk proofs
 
   rts_posix_scenarios:
     runs-on: ubuntu-latest
@@ -61,18 +58,15 @@ jobs:
       - name: Build RTS and run test scenarios
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make rts
             cd tests && 
             pip3 install -r requirements.txt &&
             RTS_DEBUG=1 QUICK=1 python3 ./run_all.py
 
-  rts_riscv_scenarios:
+  rts_riscv_build_verilator:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository and submodules
@@ -82,12 +76,25 @@ jobs:
       - name: Build RTS and run test scenarios
         uses: addnab/docker-run-action@v3
         with:
-          username: ${{ secrets.ARTIFACTORY_USERNAME }}
-          password: ${{ secrets.ARTIFACTORY_PASSWORD }}
-          registry: artifactory.galois.com:5015
-          image: artifactory.galois.com:5015/hardens
+          image: galoisinc/hardens
           options: -v ${{ github.workspace }}:/HARDENS
           run: |
             make rts
             PLATFORM=RV32_bare_metal make rts
-# TODO: run scenarios
+# NOTE: there is currently no way to run RISCV scenarios
+
+  rts_riscv_build_fpga:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Build RTS and run test scenarios
+        uses: addnab/docker-run-action@v3
+        with:
+          image: galoisinc/hardens
+          options: -v ${{ github.workspace }}:/HARDENS
+          run: |
+            make rts
+            PLATFORM=RV32_bare_metal DEV_BOARD=LFE5UM5G_85F_EVN make rts

Dockerfile

@@ -32,13 +32,12 @@ RUN apt-get install -y wget git python3 pip \
     autoconf automake autotools-dev curl libmpc-dev \
     libmpfr-dev libgmp-dev texinfo gperf \
     libtool patchutils bc zlib1g-dev libexpat-dev \
-    libftdi-dev unzip \
-    cabal-install libffi7 \
+    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
+    texlive-full pandoc
 
 # Builder
 FROM base as builder
@@ -178,6 +177,14 @@ RUN \
 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 2.11
@@ -186,6 +193,9 @@ ARG TAG=dfae4580e322584185235f301bc8a03b6bc19a65
 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 \
@@ -252,24 +262,6 @@ RUN cp build/bin/btor* /usr/local/bin/
 RUN cp deps/btor2tools/bin/btorsim /usr/local/bin/
 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}"
-
 # NuSMV
 # wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz
 # tar xzf NuSMV-2.6.0-linux64.tar.gz
@@ -319,14 +311,32 @@ RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG}
 # RDE Refinement Finder (aka the DocumentationEnricher)
 ARG TOOL=der
 ARG TAG=0.1.5
-ARG REPO=https://github.com/GaloisInc/RDE_RF/releases/tag/v.0.1.5
+ARG REPO=https://github.com/GaloisInc/RDE_RF
 WORKDIR /tmp
-RUN wget ${REPO}/${TOOL}-${TAG}.zip
+RUN wget ${REPO}/releases/download/v.${TAG}/${TOOL}-${TAG}.zip
 RUN unzip ${TOOL}-${TAG}.zip
-RUN    mv ${TOOL}-${TAG} /tools/${TOOL}
-ENV PATH="/tools/${TOOL}/bin:${PATH}"
+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/

Makefile

@@ -60,7 +60,7 @@ rts:
 	SENSORS=$(SENSORS) SELF_TEST=Disabled make -C src rts
 	mv src/rts src/rts.no_self_test
 
-clean:
+src_clean:
 	make -C src clean
 
 else # Not PLATFORM=posix
@@ -76,7 +76,7 @@ fw_only:
 fw_clean:
 	PROG=main make -C hardware/SoC/firmware clean
 
-clean:
+src_clean:
 	PROG=main make -C hardware/SoC/ clean
 
 $(info Choosing dev board $(DEV_BOARD))
@@ -92,7 +92,7 @@ ifeq ($(DEV_BOARD),LFE5UM5G_85F_EVN)
 CORE_FREQ=2400000
 
 rts:
-	CORE_FREQ=$(CORE_FREQ) PROG=main make -C hardware/SoC/ prog
+	CORE_FREQ=$(CORE_FREQ) PROG=main make -C hardware/SoC/ design.svf
 
 else
 $(info Unsupported dev board!)
@@ -105,7 +105,27 @@ $(info Unsupported platform!)
 endif # PLATFORM=RV32_bare_metal ?
 endif # PLATFORM=posix ?
 
-.PHONY: rts all clean
+#
+# Documentation
+#
+
+docs: README.pdf Assurance.pdf Toolchain.pdf
+
+README.pdf: README.md
+	pandoc -o README.pdf README.md
+
+Assurance.pdf: Assurance.md
+	pandoc -o Assurance.pdf Assurance.md
+
+Toolchain.pdf: Toolchain.md
+	pandoc -o Toolchain.pdf Toolchain.md
+
+clean: src_clean doc_clean
+
+doc_clean:
+	rm -f README.pdf Assurance.pdf Toolchain.pdf
+
+.PHONY: rts all clean src_clean fw_clean doc_clean docs
 
 check:
 	make -C models