Merge pull request #80 from FStarLang/_taramana_ci_rust_bindings

DPE: Generate Rust bindings as part of CI
FStarLang · May 22, 2024 · e946344 · e946344
2 parents 5d99ee0 + 8a0d624
commit e946344
Show file tree

Hide file tree

Showing 8 changed files with 85 additions and 28 deletions.
diff --git a/pulse2rust/dpe/c.Makefile b/pulse2rust/dpe/c.Makefile
@@ -4,9 +4,6 @@
 #
 # It is invoked by the gen-rust-bindings.sh script
 #
-# This is not run as part of CI,
-#   rather we check-in the generated bindings
-#
 
 PULSE_HOME ?= ../..
 OUTPUT_DIRECTORY=_output

diff --git a/pulse2rust/dpe/gen-external-h.sh b/pulse2rust/dpe/gen-external-h.sh
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+#
+# The script generates .h files for external dependencies,
+#   evercrypt and l0core (from DICE*) so far
+# The generated .h files are used to generate Rust bindings
+#   using the rust bindgen tool
+#
+
+set -e
+set -x
+
+# chdir to the current directory
+unset CDPATH
+cd "$( dirname "${BASH_SOURCE[0]}" )"
+
+if  [[ -z "$PULSE_HOME" ]] ; then
+    PULSE_HOME=$(realpath $(pwd)/../../)
+fi
+
+# regenerate EverCrypt*.h and L0Core.h
+make -j -f c.Makefile
+cp $PULSE_HOME/share/pulse/examples/dice/external/c/hacl/EverCrypt_Base.h _output/
+echo "// This file is generated by gen-rust-bindings.sh" > _output/bindings.h
+for f in _output/EverCrypt_*.h ; do echo '#include "'$(basename $f)'"' ; done >> _output/bindings.h
+echo '#include "L0Core.h"' >> _output/bindings.h
diff --git a/pulse2rust/dpe/gen-rust-bindings-docker.sh b/pulse2rust/dpe/gen-rust-bindings-docker.sh
@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+
+#
+# Creates rust bindings for external dependencies of DPE
+#   using docker
+#
+
+set -e
+set -x
+
+# chdir to the current directory
+unset CDPATH
+cd "$( dirname "${BASH_SOURCE[0]}" )"
+
+if  [[ -z "$PULSE_HOME" ]] ; then
+    PULSE_HOME=$(realpath $(pwd)/../../)
+fi
+
+# regenerate EverCrypt*.h and L0Core.h
+./gen-external-h.sh
+
+# generate evercrypt_gen.rs and l0core_gen in a Docker image
+DOCKER_IMAGE_NAME=haclrustbindingsimg"$$"
+echo $DOCKER_IMAGE_NAME
+docker build -t $DOCKER_IMAGE_NAME -f rust.Dockerfile .
+
+DPE_OUTPUT_DIR=$PULSE_HOME/pulse2rust/dpe/src/generated
+
+# copy evercrypt_gen.rs and l0core_gen.rs from the Docker image
+DOCKER_CONTAINER_NAME=haclrustbindingscont"$$"
+docker create --name $DOCKER_CONTAINER_NAME $DOCKER_IMAGE_NAME
+docker cp $DOCKER_CONTAINER_NAME:/usr/src/hacl/evercrypt_gen.rs $DPE_OUTPUT_DIR/
+docker cp $DOCKER_CONTAINER_NAME:/usr/src/hacl/l0core_gen.rs $DPE_OUTPUT_DIR/
+docker rm $DOCKER_CONTAINER_NAME
diff --git a/pulse2rust/dpe/gen-rust-bindings.sh b/pulse2rust/dpe/gen-rust-bindings.sh
@@ -1,4 +1,12 @@
 #!/usr/bin/env bash
+
+#
+# Generates rust bindings for external dependencies of DPE
+# It first invokes gen-external-h.sh to create .h files for
+#   the dependencies
+# And then uses the Rust bindgen tool to create their rust bindings
+#
+
 set -e
 set -x
 
@@ -7,27 +15,13 @@ unset CDPATH
 cd "$( dirname "${BASH_SOURCE[0]}" )"
 
 if  [[ -z "$PULSE_HOME" ]] ; then
-    # assume share/pulse/examples/dice/common/hacl-rust
     PULSE_HOME=$(realpath $(pwd)/../../)
 fi
 
-# regenerate EverCrypt*.h
-make -j -f c.Makefile
-cp $PULSE_HOME/share/pulse/examples/dice/external/c/hacl/EverCrypt_Base.h _output/
-echo "// This file is generated by gen-rust-bindings.sh" > _output/bindings.h
-for f in _output/EverCrypt_*.h ; do echo '#include "'$(basename $f)'"' ; done >> _output/bindings.h
-echo '#include "L0Core.h"' >> _output/bindings.h
-
-# generate EverCrypt*.rs in a Docker image
-DOCKER_IMAGE_NAME=haclrustbindingsimg"$$"
-echo $DOCKER_IMAGE_NAME
-docker build -t $DOCKER_IMAGE_NAME -f rust.Dockerfile .
+# regenerate EverCrypt*.h and L0Core.h
+./gen-external-h.sh
 
+# generate evercrypt_gen.rs and l0core_gen.rs
 DPE_OUTPUT_DIR=$PULSE_HOME/pulse2rust/dpe/src/generated
-
-# copy everCrypt.rs from the Docker image
-DOCKER_CONTAINER_NAME=haclrustbindingscont"$$"
-docker create --name $DOCKER_CONTAINER_NAME $DOCKER_IMAGE_NAME
-docker cp $DOCKER_CONTAINER_NAME:/usr/src/hacl/evercrypt_gen.rs $DPE_OUTPUT_DIR/
-docker cp $DOCKER_CONTAINER_NAME:/usr/src/hacl/l0core_gen.rs $DPE_OUTPUT_DIR/
-docker rm $DOCKER_CONTAINER_NAME
+bindgen -o $DPE_OUTPUT_DIR/evercrypt_gen.rs --allowlist-file '.*EverCrypt.*' _output/bindings.h --dynamic-loading "evercrypt" --dynamic-link-require-all -- -I _output -I .
+bindgen -o $DPE_OUTPUT_DIR/l0core_gen.rs --allowlist-file '.*L0Core.*' _output/bindings.h --dynamic-loading "l0" --dynamic-link-require-all -- -I _output -I .
diff --git a/pulse2rust/tests/Makefile b/pulse2rust/tests/Makefile
@@ -92,7 +92,11 @@ all-rs: pulsetutorial-loops.rs pulsetutorial-algorithms.rs
 test: all-rs
 	cargo test
 
-dpe: dpe.rs
+.PHONY: external
+external:
+	../dpe/gen-rust-bindings.sh
+
+dpe: dpe.rs external
 	cd ../dpe && cargo build && cd -
 	$(MAKE) -C ../dpe -f c.Makefile
 

diff --git a/share/pulse/Makefile b/share/pulse/Makefile
@@ -12,4 +12,4 @@ $(TARGETS): %:
 %.install: %
 	$(INSTALL) -m 644 -D $< $(PREFIX)/share/pulse/$<
 
-install: $(addsuffix .install,Makefile.locate-fstar,Makefile.include-base,Makefile.include)
+install: $(addsuffix .install,Makefile.locate-fstar Makefile.include-base Makefile.include)
diff --git a/src/ci/hierarchic.Dockerfile b/src/ci/hierarchic.Dockerfile
@@ -9,7 +9,8 @@ RUN sudo apt-get install -y --no-install-recommends nodejs
 
 # install rust
 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-RUN . "$HOME/.cargo/env"
+RUN sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang
+RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
 
 ADD --chown=opam:opam ./ $HOME/pulse
 WORKDIR $HOME/pulse
@@ -24,6 +25,6 @@ RUN mkdir -p $HOME/pulse_tools && \
 # Pulse CI proper
 ARG PULSE_NIGHTLY_CI
 ARG OTHERFLAGS=--use_hints
-RUN eval $(opam env) && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/pulse/src ci
+RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C $HOME/pulse/src ci
 
 ENV PULSE_HOME $HOME/pulse
diff --git a/src/ci/no-fstar-home.Dockerfile b/src/ci/no-fstar-home.Dockerfile
@@ -11,11 +11,12 @@ ARG opamthreads=24
 # https://github.com/nodesource/distributions/issues/1593
 # Remove when they are solved
 RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sed 's,https://deb.nodesource.com,http://deb.nodesource.com,' | sudo -E bash -
+RUN sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang
 RUN sudo apt-get install -y --no-install-recommends nodejs
 
 # install rust
 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
-RUN . "$HOME/.cargo/env"
+RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
 
 ADD --chown=opam:opam ./ pulse/
 
@@ -39,4 +40,4 @@ ENV PATH=$HOME/FStar/bin:$PATH
 # Pulse CI proper
 ARG PULSE_NIGHTLY_CI
 ARG OTHERFLAGS=--use_hints
-RUN eval $(opam env) && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse test
+RUN eval $(opam env) && . "$HOME/.cargo/env" && env PULSE_NIGHTLY_CI="$PULSE_NIGHTLY_CI" make -k -j $opamthreads -C pulse/src ci