From aacfff0710b31537b5aeeca5968a4d59adcc559b Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 15:53:21 -0800 Subject: [PATCH 01/17] Update generated files (code line numbers have changed because the added license) --- src/Makefile | 2 +- .../SystemVerilog/actuation_unit_impl.sv | 32 +++++++++---------- src/generated/SystemVerilog/actuator_impl.sv | 2 +- .../SystemVerilog/instrumentation_impl.sv | 12 +++---- 4 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/Makefile b/src/Makefile index 549b202..ea06595 100644 --- a/src/Makefile +++ b/src/Makefile @@ -162,7 +162,7 @@ BUILD_MSG = BUILD CC=$(CC) PLATFORM=$(PLATFORM) EXECUTION=$(EXECUTION) SELF_TEST .PHONY: all rts clean linux macos proof generate_sources generate_c generate_sv self_test_data/tests.inc.c core.c -all: rts rts_no_self_test +all: rts rts: $(SRC:.c=.o) $(EXTRA_SRC) $(CC) $(CFLAGS) $(LIBS) -o $@ $^ diff --git a/src/generated/SystemVerilog/actuation_unit_impl.sv b/src/generated/SystemVerilog/actuation_unit_impl.sv index 6920b64..c18bb93 100644 --- a/src/generated/SystemVerilog/actuation_unit_impl.sv +++ b/src/generated/SystemVerilog/actuation_unit_impl.sv @@ -6,22 +6,22 @@ module Coincidence_2_4 logic b; logic c; logic d; - // ../models/RTS/ActuationUnit.cry:60:7--60:8 + // ../models/RTS/ActuationUnit.cry:74:7--74:8 assign a = x[31:24] != 8'h0; - // ../models/RTS/ActuationUnit.cry:61:7--61:8 + // ../models/RTS/ActuationUnit.cry:75:7--75:8 assign b = x[23:16] != 8'h0; - // ../models/RTS/ActuationUnit.cry:62:7--62:8 + // ../models/RTS/ActuationUnit.cry:76:7--76:8 assign c = x[15:8] != 8'h0; - // ../models/RTS/ActuationUnit.cry:63:7--63:8 + // ../models/RTS/ActuationUnit.cry:77:7--77:8 assign d = x[7:0] != 8'h0; - // ../models/RTS/ActuationUnit.cry:57:3--57:18 + // ../models/RTS/ActuationUnit.cry:71:3--71:18 assign out = a & b | ((a | b) & (c | d) | c & d); endmodule module TemperatureLogic ( input logic [31:0] ts, output logic out ); - // ../models/RTS/ActuationUnit.cry:44:1--44:17 + // ../models/RTS/ActuationUnit.cry:58:1--58:17 Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts), .out(out)); endmodule @@ -29,7 +29,7 @@ module PressureLogic ( input logic [31:0] ts, output logic out ); - // ../models/RTS/ActuationUnit.cry:47:1--47:14 + // ../models/RTS/ActuationUnit.cry:61:1--61:14 Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts), .out(out)); endmodule @@ -37,7 +37,7 @@ module TempPressureTripOut ( input logic [1:0] ts, output logic out ); - // ../models/RTS/ActuationUnit.cry:53:1--53:20 + // ../models/RTS/ActuationUnit.cry:67:1--67:20 assign out = ts[1] | ts[0]; endmodule module Actuate_D0 @@ -48,11 +48,11 @@ module Actuate_D0 logic [31:0] temperatureTrips; logic [31:0] pressureTrips; logic d0; - // ../models/RTS/ActuationUnit.cry:34:5--34:21 + // ../models/RTS/ActuationUnit.cry:48:5--48:21 assign temperatureTrips[31:0] = trips[95:64]; - // ../models/RTS/ActuationUnit.cry:35:5--35:18 + // ../models/RTS/ActuationUnit.cry:49:5--49:18 assign pressureTrips[31:0] = trips[63:32]; - // ../models/RTS/ActuationUnit.cry:32:5--32:7 + // ../models/RTS/ActuationUnit.cry:46:5--46:7 logic TemperatureLogic_out; TemperatureLogic TemperatureLogic_inst1 (.ts(temperatureTrips), .out(TemperatureLogic_out)); @@ -61,14 +61,14 @@ module Actuate_D0 .out(PressureLogic_out)); TempPressureTripOut TempPressureTripOut_inst1 (.ts({TemperatureLogic_out, PressureLogic_out}), .out(d0)); - // ../models/RTS/ActuationUnit.cry:30:1--30:11 + // ../models/RTS/ActuationUnit.cry:44:1--44:11 assign out = d0 | old; endmodule module SaturationLogic ( input logic [31:0] ts, output logic out ); - // ../models/RTS/ActuationUnit.cry:50:1--50:16 + // ../models/RTS/ActuationUnit.cry:64:1--64:16 Coincidence_2_4 Coincidence_2_4_inst1 (.x(ts), .out(out)); endmodule @@ -79,11 +79,11 @@ module Actuate_D1 ); logic [31:0] saturationTrips; logic d1; - // ../models/RTS/ActuationUnit.cry:41:5--41:20 + // ../models/RTS/ActuationUnit.cry:55:5--55:20 assign saturationTrips[31:0] = trips[31:0]; - // ../models/RTS/ActuationUnit.cry:40:5--40:7 + // ../models/RTS/ActuationUnit.cry:54:5--54:7 SaturationLogic SaturationLogic_inst1 (.ts(saturationTrips), .out(d1)); - // ../models/RTS/ActuationUnit.cry:38:1--38:11 + // ../models/RTS/ActuationUnit.cry:52:1--52:11 assign out = d1 | old; endmodule diff --git a/src/generated/SystemVerilog/actuator_impl.sv b/src/generated/SystemVerilog/actuator_impl.sv index 6949c59..c571d15 100644 --- a/src/generated/SystemVerilog/actuator_impl.sv +++ b/src/generated/SystemVerilog/actuator_impl.sv @@ -2,6 +2,6 @@ module ActuateActuator ( input logic [1:0] inputs, output logic out ); - // ../models/RTS/Actuator.cry:31:1--31:16 + // ../models/RTS/Actuator.cry:45:1--45:16 assign out = inputs[1] | inputs[0]; endmodule diff --git a/src/generated/SystemVerilog/instrumentation_impl.sv b/src/generated/SystemVerilog/instrumentation_impl.sv index f11217a..50dee6e 100644 --- a/src/generated/SystemVerilog/instrumentation_impl.sv +++ b/src/generated/SystemVerilog/instrumentation_impl.sv @@ -4,7 +4,7 @@ module Is_Ch_Tripped input logic sensor_tripped, output logic out ); - // ../models/RTS/InstrumentationUnit.cry:139:1--139:14 + // ../models/RTS/InstrumentationUnit.cry:153:1--153:14 assign out = (mode == 2'h2) | (mode == 2'h1) & sensor_tripped; endmodule module Trip @@ -17,11 +17,11 @@ module Trip ); logic [31:0] v; logic [31:0] sp; - // ../models/RTS/InstrumentationUnit.cry:228:9--228:10 + // ../models/RTS/InstrumentationUnit.cry:242:9--242:10 assign v[31:0] = vals[32 * (NChannels - ch - 1) + 31-:32]; - // ../models/RTS/InstrumentationUnit.cry:229:9--229:11 + // ../models/RTS/InstrumentationUnit.cry:243:9--243:11 assign sp[31:0] = setpoints[32 * (NChannels - ch - 1) + 31-:32]; - // ../models/RTS/InstrumentationUnit.cry:227:1--227:5 + // ../models/RTS/InstrumentationUnit.cry:241:1--241:5 assign out = ch == 2'h2 ? $signed(v) < $signed(sp) : sp < v; endmodule module Generate_Sensor_Trips @@ -30,8 +30,8 @@ module Generate_Sensor_Trips input logic [NChannels * 32 - 1:0] setpoints, output logic [NChannels - 1:0] out ); - // ../models/RTS/InstrumentationUnit.cry:221:1--221:22 - // ../models/RTS/InstrumentationUnit.cry:224:5--224:76 + // ../models/RTS/InstrumentationUnit.cry:235:1--235:22 + // ../models/RTS/InstrumentationUnit.cry:238:5--238:76 Trip Trip_inst1 (.vals(vals), .setpoints(setpoints), .ch(2'h0), From 383dc7acb273ee0335ee81b24c7f69c67d0cf645 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 15:57:38 -0800 Subject: [PATCH 02/17] Update dockerfile, based on #123 --- Dockerfile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Dockerfile b/Dockerfile index 8c5bdfa..87e7a7b 100644 --- a/Dockerfile +++ b/Dockerfile @@ -319,12 +319,12 @@ 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} # Runner From d4efba030a68b9935e183b9cec48c5695a04c824 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 16:04:06 -0800 Subject: [PATCH 03/17] Update docker build script for dockerhub --- build_docker.sh | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/build_docker.sh b/build_docker.sh index e1ad318..7a0928a 100755 --- a/build_docker.sh +++ b/build_docker.sh @@ -20,8 +20,7 @@ while [[ $# -gt 0 ]]; do done # Env and settings -DOCKER_JFROG_PATH=artifactory.galois.com:5015 -IMAGE_TAG=${DOCKER_JFROG_PATH}/hardens:latest +IMAGE_TAG=galoisinc/hardens:latest # clone cryptol-verilog and update its submodules prior to building the docker image if [ -d "cryptol-verilog" ]; @@ -62,9 +61,7 @@ DOCKER_BUILDKIT=1 sudo docker build \ if [ $doPush -eq 1 ]; then echo "Logging in to the docker repository" - docker login ${DOCKER_JFROG_PATH} + docker login echo "INFO: Pushing the image..." - docker push ${IMAGE_TAG} - echo "INFO: Logout from the docker repo" - docker logout ${DOCKER_JFROG_PATH} + docker push IMAGE_TAG fi From f125883656b54a7ad726a1ecb0b5ea805703c96b Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 16:09:27 -0800 Subject: [PATCH 04/17] Make DMEMORY_SIZE size match dmemory_size in NervSOC.bsv TODO: figure out how to pass variables to Bluespec --- hardware/SoC/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hardware/SoC/Makefile b/hardware/SoC/Makefile index 56ff7e5..e536985 100644 --- a/hardware/SoC/Makefile +++ b/hardware/SoC/Makefile @@ -39,7 +39,7 @@ else endif IMEMORY_SIZE ?= 0x07000 -DMEMORY_SIZE ?= 0x03000 +DMEMORY_SIZE ?= 0x07000 # ================================================================ From e26d0f8a8226b7b18dde62adc582d156966cba17 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 16:37:06 -0800 Subject: [PATCH 05/17] Update CI to use Dockerhub --- .github/workflows/main.yml | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 9139c2b..1b7649a 100644 --- a/.github/workflows/main.yml +++ b/.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 @@ -61,10 +58,7 @@ 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 @@ -72,7 +66,7 @@ jobs: pip3 install -r requirements.txt && RTS_DEBUG=1 QUICK=1 python3 ./run_all.py - rts_riscv_scenarios: + rts_riscv_build: runs-on: ubuntu-latest steps: - name: Checkout repository and submodules @@ -82,12 +76,9 @@ 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 From 6b9dd979f2f5abe5d06529d4a623a0326f3658ce Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 16:37:20 -0800 Subject: [PATCH 06/17] Fix Makefile and add explanatory comments --- hardware/SoC/Makefile | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/hardware/SoC/Makefile b/hardware/SoC/Makefile index e536985..0083a12 100644 --- a/hardware/SoC/Makefile +++ b/hardware/SoC/Makefile @@ -38,6 +38,10 @@ else $(info INFO: BLUESPEC_HOME is $(BLUESPEC_HOME)) endif +# NOTE: make sure that these values match what is in +# https://github.com/GaloisInc/HARDENS/blob/develop/hardware/SoC/src_BSV/NervSoC.bsv#L151 +# +# NOTE: if this much memory doesn't fit into the FPGA, you will need to adjust it downwards IMEMORY_SIZE ?= 0x07000 DMEMORY_SIZE ?= 0x07000 @@ -82,6 +86,11 @@ BSCDIRS_V = -vdir $(VERILOG_DIR) -bdir $(BUILD_V_DIR) -info-dir $(BUILD_V_DIR) FIRMWARE_DIR = firmware PROG ?= demo +# NOTE: this value might have to be updated for the simulated target, +# depending on the host computer +# 1333333 Hz *should* be OK for the FPGA target +# See https://github.com/GaloisInc/HARDENS/blob/develop/hardware/SoC/firmware/bsp.c#L43 +# for details CORE_FREQ ?= 1333333 dmem_contents.memhex32: From 5678612687963e9707f4469c070845e70d559eb8 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 16:47:00 -0800 Subject: [PATCH 07/17] Add pandoc to generate documentation, clean up doc make target: --- Dockerfile | 2 +- Makefile | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Dockerfile b/Dockerfile index 87e7a7b..fa742b7 100644 --- a/Dockerfile +++ b/Dockerfile @@ -38,7 +38,7 @@ RUN apt-get install -y wget git python3 pip \ 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 diff --git a/Makefile b/Makefile index bb5e4a1..b6be7d7 100644 --- a/Makefile +++ b/Makefile @@ -109,7 +109,7 @@ endif # PLATFORM=posix ? # Documentation # -docs: README.pdf +docs: README.pdf Assurance.pdf Toolchain.pdf README.pdf: README.md pandoc -o README.pdf README.md @@ -123,7 +123,7 @@ Toolchain.pdf: Toolchain.md clean: src_clean doc_clean doc_clean: - rm -f README.pdf Assurance.pdf Toolchain.md + rm -f README.pdf Assurance.pdf Toolchain.pdf .PHONY: rts all clean src_clean fw_clean doc_clean docs From 8942d2f6d3f49b5dffccf16f8e1d8f849e0d580d Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 9 Feb 2023 17:18:55 -0800 Subject: [PATCH 08/17] Add FPGA build target --- .github/workflows/main.yml | 18 +++++++++++++++++- Makefile | 2 +- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 1b7649a..b0257eb 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -66,7 +66,7 @@ jobs: pip3 install -r requirements.txt && RTS_DEBUG=1 QUICK=1 python3 ./run_all.py - rts_riscv_build: + rts_riscv_build_verilator: runs-on: ubuntu-latest steps: - name: Checkout repository and submodules @@ -82,3 +82,19 @@ jobs: make rts PLATFORM=RV32_bare_metal make rts # 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 \ No newline at end of file diff --git a/Makefile b/Makefile index b6be7d7..4ad0caf 100644 --- a/Makefile +++ b/Makefile @@ -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!) From 9c898693c0317978047110cfff4b7d8474119d16 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Fri, 10 Feb 2023 11:12:46 -0800 Subject: [PATCH 09/17] Build fixes for cryptol --- Dockerfile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Dockerfile b/Dockerfile index fa742b7..f3588b3 100644 --- a/Dockerfile +++ b/Dockerfile @@ -186,6 +186,11 @@ ARG TAG=dfae4580e322584185235f301bc8a03b6bc19a65 ARG REPO=https://github.com/GaloisInc/cryptol.git RUN git clone ${REPO} /tmp/${TOOL} WORKDIR /tmp/${TOOL} +# Build fix +COPY < Date: Fri, 10 Feb 2023 12:14:08 -0800 Subject: [PATCH 10/17] Move cryptol based builds towards the end of the image --- Dockerfile | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/Dockerfile b/Dockerfile index f3588b3..e4b692f 100644 --- a/Dockerfile +++ b/Dockerfile @@ -257,24 +257,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 @@ -332,6 +314,24 @@ 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/ From 90b24db46411efac05859f1b0af3c0718a3bbcfc Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Fri, 10 Feb 2023 13:31:11 -0800 Subject: [PATCH 11/17] Switch to ubuntu 20.04 to avoid cryptol related build errors --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e4b692f..32698d5 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,7 @@ # limitations under the License. # Base -FROM ubuntu:22.04 as base +FROM ubuntu:20.04 as base ARG DEBIAN_FRONTEND=noninteractive RUN mkdir /tools WORKDIR / From 02fbf62891f5daf43696d2b3a9d351c87adc3a43 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Fri, 10 Feb 2023 16:46:27 -0800 Subject: [PATCH 12/17] Upgrade Ubuntu so we have a new-enough cabal --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 32698d5..38fd3e4 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,7 @@ # limitations under the License. # Base -FROM ubuntu:20.04 as base +FROM ubuntu:21.04 as base ARG DEBIAN_FRONTEND=noninteractive RUN mkdir /tools WORKDIR / From 1472eb589229edaeeda01cb33ae74e405c196ce0 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Mon, 13 Feb 2023 10:29:22 -0800 Subject: [PATCH 13/17] Manually specify GHC version so cryptol 2.11 build properly --- Dockerfile | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Dockerfile b/Dockerfile index 38fd3e4..e7be09a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -32,8 +32,7 @@ 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 \ @@ -178,7 +177,14 @@ RUN \ RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG} # GHC and Cabal -RUN cabal update +RUN \ + wget https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -O /usr/local/bin/ghcup \ + && chmod +x /usr/local/bin/ghcup +ENV PATH="${HOME}/.cabal/bin:${HOME}/.ghcup/bin:${PATH}" +RUN \ + ghcup install ghc 8.8.4 \ + && ghcup set ghc 8.8.4 \ + && ghcup install cabal # cryptol 2.11 ARG TOOL=cryptol From 722b4eba180df036797aea6d2c3d5449c72cc29a Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Mon, 13 Feb 2023 13:29:13 -0800 Subject: [PATCH 14/17] Cabal build fixes --- Dockerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e7be09a..6627c84 100644 --- a/Dockerfile +++ b/Dockerfile @@ -180,11 +180,12 @@ RUN echo "${TOOL} ${REPO} ${TAG}" >> ${VERSION_LOG} RUN \ wget https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup -O /usr/local/bin/ghcup \ && chmod +x /usr/local/bin/ghcup -ENV PATH="${HOME}/.cabal/bin:${HOME}/.ghcup/bin:${PATH}" +ENV PATH="/root/.ghcup/bin:${PATH}" RUN \ ghcup install ghc 8.8.4 \ && ghcup set ghc 8.8.4 \ && ghcup install cabal +RUN cabal update # cryptol 2.11 ARG TOOL=cryptol From 81c461fb619c8e6f488e27f61329543b546450b0 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Mon, 13 Feb 2023 13:30:11 -0800 Subject: [PATCH 15/17] Ubuntu version fix --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 6627c84..7fc3158 100644 --- a/Dockerfile +++ b/Dockerfile @@ -13,7 +13,7 @@ # limitations under the License. # Base -FROM ubuntu:21.04 as base +FROM ubuntu:22.04 as base ARG DEBIAN_FRONTEND=noninteractive RUN mkdir /tools WORKDIR / From b86f58f171c68018849bd572bb3b3e940fab1633 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Thu, 16 Feb 2023 09:42:56 -0800 Subject: [PATCH 16/17] more readable cabal setup --- Dockerfile | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Dockerfile b/Dockerfile index 7fc3158..1b2761f 100644 --- a/Dockerfile +++ b/Dockerfile @@ -182,8 +182,8 @@ RUN \ && chmod +x /usr/local/bin/ghcup ENV PATH="/root/.ghcup/bin:${PATH}" RUN \ - ghcup install ghc 8.8.4 \ - && ghcup set ghc 8.8.4 \ + ghcup install ghc 8.10.7 \ + && ghcup set ghc 8.10.7 \ && ghcup install cabal RUN cabal update @@ -194,10 +194,8 @@ ARG REPO=https://github.com/GaloisInc/cryptol.git RUN git clone ${REPO} /tmp/${TOOL} WORKDIR /tmp/${TOOL} # Build fix -COPY < cabal.project.local +RUN echo " parameterized-utils < 2.1.6" >> cabal.project.local RUN \ git checkout ${TAG} \ && git submodule update --init \ From b8fe55047215f9bddd0079de01e66516cd066988 Mon Sep 17 00:00:00 2001 From: Michal Podhradsky Date: Fri, 5 Apr 2024 10:24:07 -0700 Subject: [PATCH 17/17] Warn about docker image build, switch to the existing public HARDENS image --- README.md | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index 249d0ab..9e080d6 100644 --- a/README.md +++ b/README.md @@ -285,13 +285,11 @@ tools to this container as necessary during project execution. #### HARDENS Container -To build and run the core HARDENS Docker image, use the -`build_docker.sh` script and then `docker run` commands. +To build and run the core HARDENS Docker image, use the prebuild `galoisinc/hardens:latest` image. Note that `build_docker.sh` currently does not work, as `cryptol-codegen` no longer builds. Best if you use the following command: ``` -$ ./build_docker.sh $ docker run --network host --privileged -v $PWD:/HARDENS -it \ - hardens:latest + galoisinc/hardens:latest ``` In order to run a long-lived Docker container for reuse, use a `docker @@ -300,7 +298,7 @@ directory in order to bind your sandbox properly into the container. ``` $ docker run -d -it --name HARDENS --network host --privileged \ - -v $PWD:/HARDENS hardens:latest + -v $PWD:/HARDENS galoisinc/hardens:latest ``` If you have stopped a container running and it lists as "exited" when @@ -317,15 +315,6 @@ use by running a command like: $ docker exec -it HARDENS bash -l ``` -If you are *within Galois network* and *you have access rights*, you -can download the docker image from artifactory: - -```bash -$ docker pull artifactory.galois.com:5015/hardens:latest -$ docker run --network host --privileged -v $PWD:/HARDENS -it \ - artifactory.galois.com:5015/hardens:latest -``` - The helper script `run_docker.sh` executed the above detached run command, using Galois's public docker HARDENS image. The helper script `docker_shell.sh` runs a shell in the spawned container.