From 3190103f0e5c6a3c795e75b6615cc637d75d7c27 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 20 Mar 2023 17:52:21 +0100 Subject: [PATCH] Migrate compiler build from ocamlbuild to dune --- .gitlab-ci.yml | 8 +-- MANIFEST | 8 +-- compiler/MANIFEST | 7 ++- compiler/Makefile | 45 +++++---------- compiler/_tags | 29 ---------- compiler/default.nix | 4 +- compiler/dune | 31 ++++++++++ compiler/dune-project | 5 ++ compiler/examples/gimli/x86-64/Makefile | 2 +- compiler/examples/siphash/x86-64/makefile | 2 +- compiler/jasmin.mlpack.in | 69 ----------------------- compiler/{opam => jasmin.opam} | 4 +- compiler/myocamlbuild.ml | 50 ---------------- compiler/scripts/check-arm-m4 | 2 +- compiler/scripts/check-cct | 2 +- compiler/scripts/check-safety | 2 +- compiler/scripts/check-x86-64 | 2 +- compiler/scripts/extract-and-check | 4 +- compiler/scripts/parse-print-parse | 6 +- compiler/src/dune | 6 ++ default.nix | 2 +- scripts/test-libjade.sh | 2 +- 22 files changed, 84 insertions(+), 208 deletions(-) delete mode 100644 compiler/_tags create mode 100644 compiler/dune create mode 100644 compiler/dune-project delete mode 100644 compiler/jasmin.mlpack.in rename compiler/{opam => jasmin.opam} (85%) delete mode 100644 compiler/myocamlbuild.ml create mode 100644 compiler/src/dune diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ad5ea756c..2959b07a3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -79,8 +79,8 @@ ocaml: artifacts: paths: - compiler/_build/ - - compiler/jasminc.native - - compiler/jazz2tex.native + - compiler/jasminc + - compiler/jazz2tex eclib: stage: prove @@ -143,7 +143,7 @@ opam-compiler: nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'eval $(opam env) && make -C compiler -j$NIX_BUILD_CORES && - (cd compiler && mkdir -p bin && cp _build/entry/jasminc.native bin/jasminc)' + (cd compiler && mkdir -p bin && cp _build/default/jasminc.exe bin/jasminc)' artifacts: paths: - compiler/bin/jasminc @@ -182,7 +182,7 @@ check: - coq-program - ocaml script: - - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc.native -version' + - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc -version' - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler check-ci $EXTRA_MAKE_ARGUMENTS' libjade-compile-to-asm: diff --git a/MANIFEST b/MANIFEST index c2b8e84c2..c64031325 100644 --- a/MANIFEST +++ b/MANIFEST @@ -19,10 +19,10 @@ compiler/entry/jasminc.ml compiler/src/LICENSE.puf compiler/scripts/runtest compiler/Makefile -compiler/jasmin.mlpack.in -compiler/myocamlbuild.ml -compiler/_tags -compiler/opam +compiler/dune +compiler/dune-project +compiler/src/dune +compiler/jasmin.opam compiler/CIL/.keep compiler/config/tests.config diff --git a/compiler/MANIFEST b/compiler/MANIFEST index 8c6790ffb..1fe9d777c 100644 --- a/compiler/MANIFEST +++ b/compiler/MANIFEST @@ -4,10 +4,11 @@ README.md default.nix Makefile -jasmin.mlpack.in -_tags -myocamlbuild.ml +dune +dune-project +src/dune .merlin +jasmin.opam find:CIL:*.ml find:CIL:*.mli diff --git a/compiler/Makefile b/compiler/Makefile index 6d4188a31..9873dd3ff 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -1,19 +1,5 @@ # -*- Makefile -*- -# -------------------------------------------------------------------- -OCAMLBUILD_JOBS ?= 2 -OCAMLBUILD_BIN ?= ocamlbuild -OCAMLBUILD_EXTRA ?= -OCAMLBUILD_OPTS := -use-ocamlfind -j $(OCAMLBUILD_JOBS) - -# In Emacs, use classic display to enable error jumping. -ifeq ($(shell echo $$TERM), dumb) - OCAMLBUILD_OPTS += -classic-display -endif -OCAMLBUILD_OPTS += $(OCAMLBUILD_EXTRA) - -OCAMLBUILD := $(OCAMLBUILD_BIN) $(OCAMLBUILD_OPTS) - # -------------------------------------------------------------------- JSJOBS ?= 2 CHECKPY ?= @@ -45,26 +31,21 @@ OBELISK ?= obelisk all: build @true -build: jasmin.mlpack native +build: native define do-build $(RM) jasminc jazz2tex - $(OCAMLBUILD) "entry/jasminc.$(1)" "entry/jazz2tex.$(1)" - ln -sf "_build/entry/jasminc.$(1)" jasminc - ln -sf "_build/entry/jazz2tex.$(1)" jazz2tex + dune build jasminc.$(1) + dune build jazz2tex.$(1) + ln -sf "_build/default/jasminc.$(1)" jasminc + ln -sf "_build/default/jazz2tex.$(1)" jazz2tex endef byte: - $(call do-build,byte) + $(call do-build,bc) native: - $(call do-build,native) - -jasmin.mlpack: __force__ - ( echo '# GENERATED - EDIT jasmin.mlpack.in'; \ - cat jasmin.mlpack.in; \ - echo "$(wildcard CIL/*.ml*)" | tr ' ' '\n' | sed 's/\..*$$//' | sort -u ) \ - > jasmin.mlpack + $(call do-build,exe) CIL: rm -f CIL/*.ml CIL/*.mli ../proofs/extraction.vo @@ -79,14 +60,14 @@ check-ci: $(CHECK) --report=- $(CHECKCATS) clean: - $(OCAMLBUILD) -clean -classic-display + dune clean rm -rf _c_build - rm -f jasminc.native jasminc.byte lib*.a + rm -f jasminc jazz2tex lib*.a install: $(INSTALL) -m 0755 -d $(DESTDIR)$(BINDIR) - $(INSTALL) -m 0755 -T jasminc.native $(DESTDIR)$(BINDIR)/jasminc - $(INSTALL) -m 0755 -T jazz2tex.native $(DESTDIR)$(BINDIR)/jazz2tex + $(INSTALL) -m 0755 -T jasminc $(DESTDIR)$(BINDIR)/jasminc + $(INSTALL) -m 0755 -T jazz2tex $(DESTDIR)$(BINDIR)/jazz2tex uninstall: $(RM) $(DESTDIR)$(BINDIR)/jasminc @@ -111,8 +92,8 @@ lib%.a: _c_build/%.o _c_build/%.o: _c_build/%.s gcc -c -o $@ $< -_c_build/%.s: examples/%.jazz _c_build jasminc.native - ./jasminc.native $< -o $@ +_c_build/%.s: examples/%.jazz _c_build jasminc + ./jasminc $< -o $@ # -------------------------------------------------------------------- %.inferred.mli: diff --git a/compiler/_tags b/compiler/_tags deleted file mode 100644 index 9d4bbf433..000000000 --- a/compiler/_tags +++ /dev/null @@ -1,29 +0,0 @@ -# -------------------------------------------------------------------- -true : use_menhir, menhir_explain, menhir_table -true : debug -true : warn_Z, warn_Y, warn_+28, warn_-23, warn_+32, warn_+33, warn_+34, warn_-58, warn_error(+8) -true : -traverse -true : bin_annot - -# -------------------------------------------------------------------- -<.> : include - : include - : include - : include - : include - : traverse - : traverse - : traverse - -# -------------------------------------------------------------------- -: package(batteries, menhirLib, zarith, apron.octMPQ, apron.ppl, apron.boxMPQ, yojson) - : for-pack(Jasmin) -: warn_-32 -: for-pack(Jasmin) - -: for-pack(Jasmin) -: warn_-20, warn_-32, warn_-33, warn_-34 - -# -------------------------------------------------------------------- -: package(batteries, menhirLib, zarith, apron.octMPQ, apron.ppl, apron.boxMPQ, yojson) -: package(batteries, cmdliner, menhirLib, zarith, apron.ppl, apron.boxMPQ, apron.octMPQ, yojson) diff --git a/compiler/default.nix b/compiler/default.nix index 34cf17112..d8c35ec59 100644 --- a/compiler/default.nix +++ b/compiler/default.nix @@ -4,14 +4,14 @@ stdenv.mkDerivation { name = "jasmin-0"; src = ./.; buildInputs = [ mpfr ppl ] - ++ (with ocamlPackages; [ ocaml findlib ocamlbuild apron batteries camlidl cmdliner menhir menhirLib zarith yojson]) + ++ (with ocamlPackages; [ ocaml findlib dune_3 apron batteries camlidl cmdliner menhir menhirLib zarith yojson]) ; installPhase = '' mkdir -p $out/bin for p in jasminc jazz2tex do - cp _build/entry/$p.native $out/bin/$p + cp _build/default/$p.exe $out/bin/$p done ''; } diff --git a/compiler/dune b/compiler/dune new file mode 100644 index 000000000..e38bb3ca8 --- /dev/null +++ b/compiler/dune @@ -0,0 +1,31 @@ +(env + (dev + (flags (:standard -w +Z+Y+28-23+32+33+34-58@8))) + (release + (flags (:standard -w +Z+Y+28-23+32+33+34-58@8)))) + +(dirs src CIL entry) +(include_subdirs unqualified) + +(executable + (public_name jasminc) + (name jasminc) + (modules jasminc) + (flags -rectypes) + (modes byte exe) + (libraries jasmin)) + +(executable + (public_name jazz2tex) + (name jazz2tex) + (modules jazz2tex) + (flags -rectypes) + (modes byte exe) + (libraries cmdliner jasmin)) + +(library + (name jasmin) + (public_name jasmin.jasmin) + (modules :standard \ jasminc jazz2tex) + (flags -rectypes) + (libraries batteries zarith menhirLib yojson apron.octMPQ apron.ppl apron.boxMPQ)) diff --git a/compiler/dune-project b/compiler/dune-project new file mode 100644 index 000000000..ea5821a82 --- /dev/null +++ b/compiler/dune-project @@ -0,0 +1,5 @@ +(lang dune 3.2) +(name jasmin) +(license MIT) +(authors "The Jasmin development team") +(using menhir 2.1) diff --git a/compiler/examples/gimli/x86-64/Makefile b/compiler/examples/gimli/x86-64/Makefile index 991434424..6f00042e6 100644 --- a/compiler/examples/gimli/x86-64/Makefile +++ b/compiler/examples/gimli/x86-64/Makefile @@ -1,4 +1,4 @@ -JASMINC?=../../jasminc.native +JASMINC?=../../jasminc .SUFFIXES: .s .o .jazz .jinc diff --git a/compiler/examples/siphash/x86-64/makefile b/compiler/examples/siphash/x86-64/makefile index 49864ab1b..ac5317128 100644 --- a/compiler/examples/siphash/x86-64/makefile +++ b/compiler/examples/siphash/x86-64/makefile @@ -1,4 +1,4 @@ -JASMINC?=../../jasminc.native +JASMINC?=../../jasminc all: run ./run diff --git a/compiler/jasmin.mlpack.in b/compiler/jasmin.mlpack.in deleted file mode 100644 index f711243f9..000000000 --- a/compiler/jasmin.mlpack.in +++ /dev/null @@ -1,69 +0,0 @@ -src/Alias -src/Annotations -src/Arch -src/Arch_full -src/Array_expand -src/CheckAnnot -src/CLI_errors -src/Compile -src/Conv -src/CoreArchFactory -src/CoreConv -src/Ct_checker_forward -src/Evaluator -src/FInfo -src/Help -src/IInfo -src/Insert_copy_and_fix_length -src/Interval -src/IntervalGraphColoring -src/Latex_printer -src/Lexer -src/Liveness -src/Location -src/Glob_options -src/Main_compiler -src/Parseio -src/Parser -src/Ppasm -src/Pp_arm_m4 -src/Pretyping -src/Printer -src/PrintFexpr -src/PrintLinear -src/PrintCommon -src/Prog -src/Puf -src/Regalloc -src/RemoveUnusedResults -src/Ssa -src/StackAlloc -src/Subst -src/Syntax -src/Syscall_ocaml -src/Syscall_t -src/ToEC -src/safety/safetyAbsExpr -src/safety/safetyConfig -src/safety/safetyConstr -src/safety/safetyExpr -src/safety/safetyInterpreter -src/safety/safetyPreanalysis -src/safety/safetyUtils -src/safety/safetyVar -src/safety/domains/safetyBoolean -src/safety/domains/safetyCongr -src/safety/domains/safetyDisjunctive -src/safety/domains/safetyInterfaces -src/safety/domains/safetyNum -src/safety/domains/safetyPointsTo -src/safety/domains/safetyProduct -src/safety/domains/safetyProf -src/safety/domains/safetySymEq -src/Tt_arm_m4 -src/Typing -src/Utils -src/Varalloc -src/X86_arch_full -src/X86_safety -src/Arm_arch_full diff --git a/compiler/opam b/compiler/jasmin.opam similarity index 85% rename from compiler/opam rename to compiler/jasmin.opam index 91eb3ba01..95f03b592 100644 --- a/compiler/opam +++ b/compiler/jasmin.opam @@ -13,8 +13,8 @@ build: [ ] install: [ mkdir -p "%{prefix}%/bin" - cp "_build/entry/jasminc.native" "%{prefix}%/bin/jasminc" - cp "_build/entry/jazz2tex.native" "%{prefix}%/bin/jazz2tex" + cp "_build/default/jasminc.exe" "%{prefix}%/bin/jasminc" + cp "_build/default/jazz2tex.exe" "%{prefix}%/bin/jazz2tex" ] depends: [ "ocaml" { >= "4.10" & build } diff --git a/compiler/myocamlbuild.ml b/compiler/myocamlbuild.ml deleted file mode 100644 index 8ad0ba6aa..000000000 --- a/compiler/myocamlbuild.ml +++ /dev/null @@ -1,50 +0,0 @@ -open Ocamlbuild_plugin - -let _ = dispatch begin function - | After_options -> - Options.ocamlc := S[!Options.ocamlc ; A"-rectypes"]; - Options.ocamlopt := S[!Options.ocamlopt; A"-rectypes"]; - - | After_rules -> - (* Numerical warnings *) - begin - let wflag error mode wid = - let mode = match mode with - | `Enable -> "+" - | `Disable -> "-" - | `Mark -> "@" - in - match error with - | false -> S[A"-w"; A(Printf.sprintf "%s%d" mode wid)] - | true -> S[A"-warn-error"; A(Printf.sprintf "%s%d" mode wid)] - in - for i = 1 to 59 do - flag ["ocaml"; "compile"; Printf.sprintf "warn_+%d" i] & (wflag false `Enable i); - flag ["ocaml"; "compile"; Printf.sprintf "warn_-%d" i] & (wflag false `Disable i); - flag ["ocaml"; "compile"; Printf.sprintf "warn_@%d" i] & (wflag false `Mark i); - flag ["ocaml"; "compile"; Printf.sprintf "werr_+%d" i] & (wflag true `Enable i); - flag ["ocaml"; "compile"; Printf.sprintf "werr_-%d" i] & (wflag true `Disable i); - flag ["ocaml"; "compile"; Printf.sprintf "werr_@%d" i] & (wflag true `Mark i) - done - end; - - (* menhir & --explain/--trace/--table *) - flag ["ocaml"; "parser"; "menhir"; "menhir_explain"] & A"--explain"; - flag ["ocaml"; "parser"; "menhir"; "menhir_trace" ] & A"--trace"; - flag ["ocaml"; "parser"; "menhir"; "menhir_table" ] & A"--table"; - flag ["ocaml"; "parser"; "menhir"; "menhir_utokens"] & A"--unused-tokens"; - - flag ["ocaml"; "menhir_ocamldep"; "menhir_utokens"] & A"--unused-tokens"; - - (* Threads switches *) - flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]); - flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]); - - (* libs <-> src *) - Pathname.define_context "entry" ["."]; - Pathname.define_context "src" ["CIL"]; - Pathname.define_context "src/safety" ["CIL"]; - Pathname.define_context "src/safety/domains" ["CIL"] - - | _ -> () -end diff --git a/compiler/scripts/check-arm-m4 b/compiler/scripts/check-arm-m4 index 1c5b22fb2..a9611b084 100755 --- a/compiler/scripts/check-arm-m4 +++ b/compiler/scripts/check-arm-m4 @@ -10,6 +10,6 @@ trap "rm -r ${DIR}" EXIT set -x -$(dirname $0)/../jasminc.native -arch arm-m4 -o ${ASM} "$@" +$(dirname $0)/../jasminc -arch arm-m4 -o ${ASM} "$@" llvm-mc --triple=armv7m --mcpu=cortex-m4 --filetype=obj -o ${OBJ} ${ASM} diff --git a/compiler/scripts/check-cct b/compiler/scripts/check-cct index 46d6012af..c9e5e2330 100755 --- a/compiler/scripts/check-cct +++ b/compiler/scripts/check-cct @@ -2,4 +2,4 @@ set -ex -exec $(dirname $0)/../jasminc.native -checkCT "$@" +exec $(dirname $0)/../jasminc -checkCT "$@" diff --git a/compiler/scripts/check-safety b/compiler/scripts/check-safety index 1a752443b..632bdc964 100755 --- a/compiler/scripts/check-safety +++ b/compiler/scripts/check-safety @@ -2,4 +2,4 @@ set -ex -exec $(dirname $0)/../jasminc.native -checksafety "$@" +exec $(dirname $0)/../jasminc -checksafety "$@" diff --git a/compiler/scripts/check-x86-64 b/compiler/scripts/check-x86-64 index 622a8325f..697d71924 100755 --- a/compiler/scripts/check-x86-64 +++ b/compiler/scripts/check-x86-64 @@ -11,7 +11,7 @@ trap "rm -r ${DIR}" EXIT set -x -$(dirname $0)/../jasminc.native -o ${ASM} "$@" +$(dirname $0)/../jasminc -o ${ASM} "$@" # Negative test cases should have failed by now # Succeed early if it’s not the case (i.e., do not try to assemble the result) (echo $@ | grep -q fail) && exit 0 diff --git a/compiler/scripts/extract-and-check b/compiler/scripts/extract-and-check index 58c9f5548..9ad6b19c3 100755 --- a/compiler/scripts/extract-and-check +++ b/compiler/scripts/extract-and-check @@ -10,8 +10,8 @@ trap "rm -r ${DIR}" EXIT set -x -$(dirname $0)/../jasminc.native -oecarray ${DIR} -oec ${EC} "$@" -$(dirname $0)/../jasminc.native -oecarray ${DIR} -CT -oec ${CT} "$@" +$(dirname $0)/../jasminc -oecarray ${DIR} -oec ${EC} "$@" +$(dirname $0)/../jasminc -oecarray ${DIR} -CT -oec ${CT} "$@" easycrypt ${ECARGS} ${EC} easycrypt ${ECARGS} ${CT} diff --git a/compiler/scripts/parse-print-parse b/compiler/scripts/parse-print-parse index 4fd82a344..9e7fa083a 100755 --- a/compiler/scripts/parse-print-parse +++ b/compiler/scripts/parse-print-parse @@ -10,8 +10,8 @@ trap "rm -r ${DIR}" EXIT set -x # Check that no printer crashes -$(dirname $0)/../jasminc.native -pall "$@" >/dev/null +$(dirname $0)/../jasminc -pall "$@" >/dev/null # Pretty-print the program before compilation -$(dirname $0)/../jasminc.native -ptyping "$@" > ${OUT} +$(dirname $0)/../jasminc -ptyping "$@" > ${OUT} # Try to parse it and type-check it again -$(dirname $0)/../jasminc.native -until_typing ${OUT} +$(dirname $0)/../jasminc -until_typing ${OUT} diff --git a/compiler/src/dune b/compiler/src/dune new file mode 100644 index 000000000..89be43cf6 --- /dev/null +++ b/compiler/src/dune @@ -0,0 +1,6 @@ +(ocamllex + (modules lexer)) + +(menhir + (flags "--table" "--explain") + (modules parser)) diff --git a/default.nix b/default.nix index 2a2b03660..1f7508ea8 100644 --- a/default.nix +++ b/default.nix @@ -54,7 +54,7 @@ stdenv.mkDerivation { ++ optionals coqDeps [ coqPackages.coq mathcomp-word ] ++ optionals testDeps ([ curl.bin oP.apron.out libllvm ] ++ (with python3Packages; [ python pyyaml ])) ++ optionals ocamlDeps ([ mpfr ppl ] ++ (with oP; [ - ocaml findlib ocamlbuild + ocaml findlib dune_3 cmdliner (batteries.overrideAttrs (o: { doCheck = false; })) menhir (oP.menhirLib or null) zarith camlidl apron yojson ])) diff --git a/scripts/test-libjade.sh b/scripts/test-libjade.sh index 5aaeb54b0..7bc6ee520 100755 --- a/scripts/test-libjade.sh +++ b/scripts/test-libjade.sh @@ -12,7 +12,7 @@ OUT="results" DIR="$ROOT/$1" -MAKELINE="-C $DIR CI=1 JASMIN=$PWD/compiler/jasminc.native" +MAKELINE="-C $DIR CI=1 JASMIN=$PWD/compiler/jasminc" # Exclude primitives that are known not to build export EXCLUDE=""