diff --git a/sledge/.gitignore b/sledge/.gitignore index 20c95a932..b903df7ee 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -1,15 +1,13 @@ .merlin -/bin/ /llvm/ /model/dune -/src/dune /src/config/dune +/src/domain/dune +/src/dune /src/import/dune /src/llair/dune /src/symbheap/dune /src/trace/dune -/src/domain/dune -/src/version.ml /test/*/*.bc /test/*/*.bc.err /test/*/*.bc.out diff --git a/sledge/Makefile b/sledge/Makefile index 6dd59783e..3fa2ab8ec 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -11,8 +11,17 @@ INSTALLS = sledge FMTS = @_build/dbg/src/fmt DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS)) _build/dbg/sledge-help.txt -OPT_TARGETS = $(patsubst %,_build/opt/%.exe,$(EXES)) $(patsubst %,_build/opt/%.install,$(INSTALLS)) _build/opt/sledge-help.txt -DBG_OPT_TARGETS = $(patsubst %,_build/dbg-opt/%.exe,$(EXES)) $(patsubst %,_build/dbg-opt/%.install,$(INSTALLS)) _build/dbg-opt/sledge-help.txt + +TARGETS = $(DBG_TARGETS) $(subst dbg,dbg-opt,$(DBG_TARGETS)) $(subst dbg,opt,$(DBG_TARGETS)) + +dune_build_dbg = dune build $(DBG_TARGETS) +dune_install_dbg = dune install --context=dbg --prefix=_build/_install/dbg sledge 2>/dev/null + +dune_build_dbg_opt = $(subst dbg,dbg-opt,$(dune_build_dbg)) +dune_install_dbg_opt = $(subst dbg,dbg-opt,$(dune_install_dbg)) + +dune_build_opt = $(subst dbg,opt,$(dune_build_dbg)) +dune_install_opt = $(subst dbg,opt,$(dune_install_dbg)) DUNEINS = $(shell find src model -name dune.in) DUNES = $(patsubst %.in,%,$(DUNEINS)) @@ -21,7 +30,7 @@ DUNES = $(patsubst %.in,%,$(DUNEINS)) dunes: $(DUNES) %/dune: dune-common.in %/dune.in - @cat $+ > $@ + cat $+ > $@ .PHONY: setup setup: dunes @@ -32,23 +41,29 @@ check: setup .PHONY: exes exes: setup - dune build $(DBG_TARGETS) $(DBG_OPT_TARGETS) $(OPT_TARGETS) + dune build $(TARGETS) + $(dune_install_dbg) + $(dune_install_dbg_opt) + $(dune_install_opt) .PHONY: dbg dbg: setup - dune build $(DBG_TARGETS) + $(dune_build_dbg) + $(dune_install_dbg) .PHONY: do do: setup - dune build $(DBG_OPT_TARGETS) + $(dune_build_dbg_opt) + $(dune_install_dbg_opt) .PHONY: opt opt: setup - dune build $(OPT_TARGETS) + $(dune_build_opt) + $(dune_install_opt) .PHONY: watch watch: setup - dune build --watch $(DBG_TARGETS) $(DBG_OPT_TARGETS) $(OPT_TARGETS) + dune build --watch $(TARGETS) .PHONY: test test: setup @@ -62,10 +77,10 @@ BISECT_DIR = $(CURDIR)/_coverage/out .PHONY: coverage coverage: setup - @rm -rf _coverage - @mkdir -p $(BISECT_DIR) - @BISECT_FILE=$(BISECT_DIR)/bisect dune build --force @_build/coverage/runtest - @find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I _build/coverage/ -text _coverage/summary.txt -html _coverage/ + rm -rf _coverage + mkdir -p $(BISECT_DIR) + BISECT_FILE=$(BISECT_DIR)/bisect dune build --force @_build/coverage/runtest + find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I _build/coverage/ -text _coverage/summary.txt -html _coverage/ @echo "open _coverage/index.html" .PHONY: clean @@ -76,7 +91,7 @@ clean: .PHONY: fmt fmt: dune build $(FMTS) --auto-promote - ocamlformat -i src/version.ml.in $(DUNEINS) + ocamlformat -i $(DUNEINS) clang-format -i model/llair_intrinsics.h model/cxxabi.cpp ${MAKE} -C test fmt diff --git a/sledge/bin/sledge b/sledge/bin/sledge index 09fa49bec..cb339f52e 120000 --- a/sledge/bin/sledge +++ b/sledge/bin/sledge @@ -1 +1 @@ -../_build/install/opt/bin/sledge \ No newline at end of file +../_build/_install/opt/bin/sledge \ No newline at end of file diff --git a/sledge/bin/sledge.dbg b/sledge/bin/sledge.dbg index b2907c46b..a454e906c 120000 --- a/sledge/bin/sledge.dbg +++ b/sledge/bin/sledge.dbg @@ -1 +1 @@ -../_build/install/dbg/bin/sledge \ No newline at end of file +../_build/_install/dbg/bin/sledge \ No newline at end of file diff --git a/sledge/bin/sledge.do b/sledge/bin/sledge.do new file mode 120000 index 000000000..ce505ca35 --- /dev/null +++ b/sledge/bin/sledge.do @@ -0,0 +1 @@ +../_build/_install/dbg-opt/bin/sledge \ No newline at end of file diff --git a/sledge/sledge.opam b/sledge/sledge.opam index fe17804ab..308d3413e 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -16,7 +16,8 @@ depends: [ "crunch" {build} "ctypes" "ctypes-foreign" - "dune" {build} + "dune" {>= "1.11.3" build} + "dune-build-info" "llvm" {= "8.0.0"} "ppx_compare" "ppx_import" diff --git a/sledge/src/dune.in b/sledge/src/dune.in index a2a3ec62e..974ca8491 100644 --- a/sledge/src/dune.in +++ b/sledge/src/dune.in @@ -12,17 +12,11 @@ let deps = ["import"; "llair_"; "symbheap"; "config"; "domain"] Jbuild_plugin.V1.send @@ Format.sprintf {| -(rule - (targets version.ml) - (deps version.ml.in (universe)) - (action (run ../tools/gen_version.sh version.ml)) - (mode promote-until-clean)) - (executable (public_name sledge) (package sledge) %s - (libraries shexp.process %s)) + (libraries dune-build-info shexp.process %s)) |} (flags `exe deps) (libraries deps) diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 7888f957e..8e8d2e34e 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -195,7 +195,7 @@ let readme () = tracing." ;; -Command.run ~version:Version.version ~build_info:"" +Command.run ~version:Version.version ~build_info:Version.build_info (Command.group ~summary ~readme ~preserve_subcommand_order:() [ ("buck", Sledge_buck.main ~command ~analyze:(translate >*> analyze)) ; ("llvm", llvm_grp); ("analyze", analyze_cmd) diff --git a/sledge/src/version.ml b/sledge/src/version.ml new file mode 100644 index 000000000..593a3201a --- /dev/null +++ b/sledge/src/version.ml @@ -0,0 +1,40 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Version information populated by build system *) + +let debug = + let d = ref false in + assert ( + d := true ; + true ) ; + !d + +module B = Build_info.V1 + +let version_to_string v = + Option.value_map ~f:B.Version.to_string v ~default:"dev" + +let version = + version_to_string (B.version ()) ^ if debug then "-dbg" else "" + +let build_info = + let libs = + List.map (B.Statically_linked_libraries.to_list ()) ~f:(fun lib -> + ( B.Statically_linked_library.name lib + , version_to_string (B.Statically_linked_library.version lib) ) ) + |> List.sort ~compare:[%compare: string * string] + in + let max_length = + List.fold_left libs ~init:0 ~f:(fun n (name, _) -> + max n (String.length name) ) + in + String.concat ~sep:"\n" + ( "statically linked libraries:" + :: List.map libs ~f:(fun (name, v) -> + Printf.sprintf "- %-*s %s" max_length name v ) + @ ["version:"] ) diff --git a/sledge/src/version.ml.in b/sledge/src/version.ml.in deleted file mode 100644 index e1cbf5b9f..000000000 --- a/sledge/src/version.ml.in +++ /dev/null @@ -1,11 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -(** Version information populated by build system *) - -let debug = [%debug] -let version = "%%VERSION%%" ^ if debug then "-dbg" else "" diff --git a/sledge/src/version.mli b/sledge/src/version.mli index 6d5973683..6a2a9288f 100644 --- a/sledge/src/version.mli +++ b/sledge/src/version.mli @@ -9,3 +9,4 @@ val debug : bool val version : string +val build_info : string diff --git a/sledge/tools/gen_version.sh b/sledge/tools/gen_version.sh deleted file mode 100755 index 3229af41a..000000000 --- a/sledge/tools/gen_version.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash - -# Copyright (c) Facebook, Inc. and its affiliates. -# -# This source code is licensed under the MIT license found in the -# LICENSE file in the root directory of this source tree. - -# usage: gen_version.sh [] - -FILE="$1" - -if [[ ! -z "$2" ]]; then - # second arg passed when called from opam - VERSION="$2" -else - # second arg omitted when called from src/dune - if [[ ! "%%VERSION%%" == "%%"*"%%" ]]; then - # file has been watermarked when building distrib archive - VERSION="%%VERSION%%" - else - # file has not been watermarked when building in dev git tree - VERSION=$(git describe --dirty --always) - fi -fi - -sed -e "s|%%VERSION%[%]|$VERSION|g" $FILE.in > $FILE