diff --git a/sledge/.gitignore b/sledge/.gitignore index eafd1b195..b680501ce 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -1,6 +1,3 @@ -.llvm_build -.llvm_install -/llvm/ /model/cxxabi.bc /model/lib_fuzzer_main.bc /test/**/*.bc @@ -11,4 +8,7 @@ /test/*.sexp /test/extra /test/local +/vendor/llvm-dune/llvm-project/llvm/test +/vendor/llvm-dune/llvm_*.opam +/vendor/llvm-dune/src _build diff --git a/sledge/Makefile b/sledge/Makefile index 586b0676e..6b1cd5609 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -20,38 +20,59 @@ dune_install_trace = $(subst release,trace,$(dune_install_release)) dune_build_debug = $(subst release,debug,$(dune_build_release)) dune_install_debug = $(subst release,debug,$(dune_install_release)) +LLVM_OCAML_SRC = $(shell git ls-files -- vendor/llvm-dune) + +# file to use as a sentinel indicating llvm ocaml bindings are up-to-date +LLVM_OCAML_SENTINEL=vendor/llvm-dune/src/llvm/common/dune + +# Note that this does not correctly detect llvm shared libraries on +# macos since llvm-config is broken. A filthy workaround seems to be +# to create the libLLVM-11.dylib file llvm-config looks for as a +# symbolic link to libLLVM.dylib: +# LLVMROOT=$(dirname $(dirname $(opam config var conf-llvm:config))) \ +# ln -s $LLVMROOT/lib/libLLVM.dylib $LLVMROOT/lib/libLLVM-11.dylib + +$(LLVM_OCAML_SENTINEL): $(LLVM_OCAML_SRC) + cd vendor/llvm-dune; ./setup.sh $$(opam config var conf-llvm:config) &>/dev/null + +clean_llvm: + rm -rf vendor/llvm-dune/{src,llvm_*.opam} + +.PHONY: setup +setup: $(LLVM_OCAML_SENTINEL) + .PHONY: check -check: +check: setup dune build @check .PHONY: exes -exes: +exes: setup dune build $(TARGETS) $(dune_install_debug) $(dune_install_trace) $(dune_install_release) .PHONY: debug -debug: +debug: setup $(dune_build_debug) $(dune_install_debug) .PHONY: trace -trace: +trace: setup $(dune_build_trace) $(dune_install_trace) .PHONY: release -release: +release: setup $(dune_build_release) $(dune_install_release) .PHONY: report -report: +report: setup dune build $(REPORT_TARGETS) .PHONY: watch -watch: +watch: setup dune build --watch --terminal-persistence=clear-on-rebuild $(TARGETS) .PHONY: test diff --git a/sledge/dune b/sledge/dune index d4db12f9b..1ceb87a65 100644 --- a/sledge/dune +++ b/sledge/dune @@ -107,7 +107,7 @@ (preprocess (pps ppx_sledge ppx_trace)))) -(dirs :standard \ llvm test) +(dirs :standard \ test) (vendored_dirs vendor) diff --git a/sledge/ppx_trace/ppx_trace.ml b/sledge/ppx_trace/ppx_trace.ml index 969a3bddf..808b7e3f6 100644 --- a/sledge/ppx_trace/ppx_trace.ml +++ b/sledge/ppx_trace/ppx_trace.ml @@ -61,7 +61,8 @@ let debug = ref false ;; Driver.Cookies.add_simple_handler "ppx_trace_enabled" Ast_pattern.__ ~f:(function - | Some {pexp_desc= Pexp_constant (Pconst_string (("1" | "true"), _))} -> + | Some {pexp_desc= Pexp_constant (Pconst_string (("1" | "true"), _, _))} + -> debug := true | _ -> () ) diff --git a/sledge/sledge.opam b/sledge/sledge.opam index 153d9c9ec..3d824e4ad 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -14,6 +14,7 @@ depends: [ "base" "containers" "containers-data" + "conf-llvm" {= "11.0.0"} "core" {>= "v0.14"} "ctypes" "ctypes-foreign" @@ -21,11 +22,10 @@ depends: [ "dune-build-info" {build} "fpath" "iter" - "llvm" {= "8.0.0"} "mtime" "ppx_compare" "ppx_hash" - "ppxlib" {< "0.16.0"} + "ppxlib" {>= "0.21.0"} "shexp" "smtlib-utils" "yojson" diff --git a/sledge/test/Makefile b/sledge/test/Makefile index d9446d99d..10f049293 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -33,8 +33,8 @@ sledge_report_exe: # which utilities to use diff?=patdiff -# configure the non-host llvm and clang -export PATH := $(CURDIR)/../.llvm_install/sledge/bin:$(PATH) +# select llvm and clang used by opam +export PATH := $(shell $$(opam config var conf-llvm:config) --bindir):$(PATH) # configure sort export LANG := C diff --git a/sledge/test/llvm b/sledge/test/llvm index 4405e5249..775c3b20e 120000 --- a/sledge/test/llvm +++ b/sledge/test/llvm @@ -1 +1 @@ -../llvm/test \ No newline at end of file +../vendor/llvm-dune/llvm-project/llvm/test \ No newline at end of file diff --git a/sledge/vendor/llvm-dune/setup.sh b/sledge/vendor/llvm-dune/setup.sh index 9ca855559..c793efc01 100755 --- a/sledge/vendor/llvm-dune/setup.sh +++ b/sledge/vendor/llvm-dune/setup.sh @@ -1,4 +1,4 @@ -#!/bin/sh -ex +#!/bin/sh -e if test "$(dirname $0)" != '.'; then echo "The script must be executed from its current directory." @@ -19,12 +19,12 @@ llvm_config() { "$llvm_config" $@ } -if llvm_config --link-static --libs; then +if llvm_config --link-static; then default_mode=static support_static_mode=true fi -if llvm_config --link-shared --libs; then +if llvm_config --link-shared; then default_mode=shared support_shared_mode=true fi