From f6ba0c81378729941325268f013899ac0fe40dd7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 12 Oct 2018 09:03:51 -0700 Subject: [PATCH] [sledge] Update build system, etc. Reviewed By: jvillard Differential Revision: D9850346 fbshipit-source-id: 16fa35ae2 --- .gitignore | 2 + Makefile | 2 +- sledge/.gitignore | 10 ++-- sledge/.ocamlformat | 3 +- sledge/Makefile | 72 ++++++++++++-------------- sledge/SETUP.org | 88 +++++++++++++++----------------- sledge/bin/sledge.dbg | 1 + sledge/bin/sledge.opt | 1 + sledge/dune-common.in | 48 +++++++++++++++++ sledge/dune-project | 1 + sledge/dune-workspace | 5 ++ sledge/jbuild-common.in | 40 --------------- sledge/jbuild-workspace.in | 2 - sledge/llair.opam | 14 ++--- sledge/sledge.opam | 13 +++-- sledge/src/dune.in | 20 ++++++++ sledge/src/import/dune.in | 15 ++++++ sledge/src/import/jbuild.in | 13 ----- sledge/src/jbuild.in | 12 ----- sledge/src/llair/dune.in | 15 ++++++ sledge/src/llair/jbuild.in | 13 ----- sledge/src/ppx_trace/dune | 5 ++ sledge/src/ppx_trace/jbuild | 5 -- sledge/src/symbheap/dune.in | 15 ++++++ sledge/src/trace/dune.in | 15 ++++++ sledge/src/trace/jbuild.in | 13 ----- sledge/test/Makefile | 51 +++++++++++------- sledge/tools/gen_version.sh | 8 ++- sledge/tools/opam/dev-tools.opam | 12 +++++ 29 files changed, 290 insertions(+), 224 deletions(-) create mode 120000 sledge/bin/sledge.dbg create mode 120000 sledge/bin/sledge.opt create mode 100644 sledge/dune-common.in create mode 100644 sledge/dune-project create mode 100644 sledge/dune-workspace delete mode 100644 sledge/jbuild-common.in delete mode 100644 sledge/jbuild-workspace.in create mode 100644 sledge/src/dune.in create mode 100644 sledge/src/import/dune.in delete mode 100644 sledge/src/import/jbuild.in delete mode 100644 sledge/src/jbuild.in create mode 100644 sledge/src/llair/dune.in delete mode 100644 sledge/src/llair/jbuild.in create mode 100644 sledge/src/ppx_trace/dune delete mode 100644 sledge/src/ppx_trace/jbuild create mode 100644 sledge/src/symbheap/dune.in create mode 100644 sledge/src/trace/dune.in delete mode 100644 sledge/src/trace/jbuild.in create mode 100644 sledge/tools/opam/dev-tools.opam diff --git a/.gitignore b/.gitignore index 2df49dd69..8227ed7e0 100644 --- a/.gitignore +++ b/.gitignore @@ -171,3 +171,5 @@ infer/src/.project /infer/src/deadcode/dune /infer/src/deadcode/*.ml /infer/src/deadcode/*.mli +_opam +_coverage diff --git a/Makefile b/Makefile index e1b6ed822..6f030ca9f 100644 --- a/Makefile +++ b/Makefile @@ -151,7 +151,7 @@ OCAMLFORMAT_EXE?=ocamlformat fmt: parallel $(OCAMLFORMAT_EXE) -i ::: $$(git diff --name-only --diff-filter=ACMRU $$(git merge-base origin/master HEAD) | grep "\.mli\?$$") -DUNE_ML:=$(shell find * -name 'dune*.in' | grep -v workspace | grep -v sledge) +DUNE_ML:=$(shell find * -name 'dune*.in' | grep -v workspace) .PHONY: fmt_dune fmt_dune: diff --git a/sledge/.gitignore b/sledge/.gitignore index da0182c12..962fb543d 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -1,13 +1,13 @@ .merlin /llvm/ /model/cxxabi.bc -/src/import/jbuild -/src/jbuild -/src/llair/jbuild -/src/trace/jbuild +/src/dune +/src/import/dune +/src/llair/dune +/src/symbheap/dune +/src/trace/dune /src/version.ml /test/*/*.bc /test/*/*.bc.err /test/*/*.bc.out _build -jbuild-workspace diff --git a/sledge/.ocamlformat b/sledge/.ocamlformat index 13ba6940f..40b8a92ff 100644 --- a/sledge/.ocamlformat +++ b/sledge/.ocamlformat @@ -1,4 +1,3 @@ -break-cases = fit -break-string-literals = wrap +profile = compact margin = 77 wrap-comments = true diff --git a/sledge/Makefile b/sledge/Makefile index 187c8d5e5..687dbd162 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -3,67 +3,63 @@ # This source code is licensed under the MIT license found in the # LICENSE file in the root directory of this source tree. -SHELL=bash - -OCAMLDOT?=ocamldot OCAMLFORMAT?=ocamlformat .PHONY: default -default: exe - -.PHONY: src/version.ml -src/version.ml: - @tools/gen_version.sh $@ - -.PHONY: version -version: src/version.ml - -jbuild-workspace: jbuild-workspace.in - sed -e "s|@OPAM_SWITCH[@]|$$(opam switch show)|g" $< > $@ +default: dev -JBUILDS=$(patsubst %.in,%,$(shell find * -name jbuild.in)) +DUNES=$(patsubst %.in,%,$(shell find src -name dune.in)) -.PHONY: jbuilds -jbuilds: $(JBUILDS) +.PHONY: dunes +dunes: $(DUNES) -%/jbuild: jbuild-common.in %/jbuild.in +%/dune: dune-common.in %/dune.in @cat $+ > $@ .PHONY: setup -setup: src/version.ml jbuild-workspace jbuilds +setup: dunes -.PHONY: exe -exe: setup - jbuilder build src/sledge.exe +.PHONY: exes +exes: setup + dune build _build/dev/src/sledge.exe _build/release/src/sledge.exe + +.PHONY: watch +watch: setup + dune build --watch _build/dev/src/sledge.exe _build/release/src/sledge.exe .PHONY: bc bc: setup - jbuilder build _build/dbg/src/sledge.bc + dune build _build/dev/src/sledge.bc + +.PHONY: dev +dev: setup + dune build _build/dev/src/sledge.exe -.PHONY: dbg -dbg: setup - jbuilder build _build/dbg/src/sledge.exe +.PHONY: release +release: setup + dune build _build/release/src/sledge.exe -.PHONY: opt -opt: setup - jbuilder build _build/default/src/sledge.exe +.PHONY: test +test: + dune build @_build/dev/runtest --auto-promote -SRCS=$(shell \ls src/{,*/}*.ml{,i}) +BISECT_DIR=$(CURDIR)/_coverage/out -mod_dep.dot: $(SRCS) - ocamldep.opt $(SRCS) | $(OCAMLDOT) -r Sledge -fullgraph > _build/mod_dep.dot +.PHONY: coverage +coverage: setup + @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 clean: - rm -rf _build jbuild-workspace $(JBUILDS) - -.PHONY: cleaner -cleaner: clean - rm -rf src/version.ml + dune clean + rm -rf _coverage $(DUNES) .PHONY: fmt fmt: - $(OCAMLFORMAT) -i $(SRCS) + $(OCAMLFORMAT) -i $(shell find src -name '*.ml' -or -name '*.mli') src/version.ml.in clang-format -i model/llair_intrinsics.h model/cxxabi.cpp # print any variable for Makefile debugging diff --git a/sledge/SETUP.org b/sledge/SETUP.org index b337ec4dc..40b66dc4c 100644 --- a/sledge/SETUP.org +++ b/sledge/SETUP.org @@ -1,55 +1,51 @@ -1. NOTE: These instructions use ~/.local/llvm_$(opam config var switch) as an install root for llvm/clang, but installing elsewhere should be fine. Also note that you probably don't want to use this clang for anything else because it is a default debug build and hence very slow. So some PATH management is likely needed to have ~/.local/llvm_$(opam config var switch) in PATH only when building / running llair. This is done automatically for the targets in test/Makefile. +1. export SLEDGE=$HOME/sat/sledge 2. clone llvm, clang, and libcxxabi - - cd ~/path/to/sledge - - git clone git+ssh://git@github.com/jberdine/llvm.git --branch ocaml_api + - cd $SLEDGE + - git clone https://github.com/jberdine/llvm.git --branch ocaml_api - git clone https://github.com/llvm-mirror/clang.git llvm/tools/clang + - git -C llvm/tools/clang checkout 32f603c58965543e256fdf8c3cb6eaceec2974da + - git clone https://github.com/llvm-mirror/libcxx.git llvm/projects/libcxx - git clone https://github.com/llvm-mirror/libcxxabi.git llvm/projects/libcxxabi -3. build llvm & clang - - brew install cmake ninja - - cd ~/path/to/sledge/llvm +3. export OPAMJOBS=$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1) +4. create opam switches + - for variant in '' '+flambda'; do opam switch --yes create sledge$variant 4.07.1+rc1$variant; done +5. install llvm deps + - install deps + + sudo yum install cmake ninja + + brew install cmake ninja + - for switch in sledge sledge+flambda; do opam install --yes --switch=$switch ctypes; done +6. build llvm & clang + - cd $SLEDGE/llvm - mkdir _build - cd _build - - cmake -G Ninja -DCMAKE_INSTALL_PREFIX=~/.local/llvm_$(opam config var switch) -DLLVM_OCAML_INSTALL_PATH=~/.local/llvm_$(opam config var switch)/lib/ocaml .. - - ninja -j8 - - ninja ocaml_doc - - ninja install -4. install deps - - add ~/.local/llvm_$(opam config var switch)/bin to shell PATH - + because installing the opam package for llvm will look for it - + export PATH=~/.local/llvm_$(opam config var switch)/bin:$PATH - - pin conf-llvm - + opam pin add -n conf-llvm --dev - + opam pin edit conf-llvm - - edit version number to match that of the llvm clone (= 7.0.0) - - pin llvm - + cd ~/path/to/sledge/llvm - + opam pin add -n -k git llvm . - + opam pin edit llvm - - edit llvm and conf-llvm version number to match that of the llvm clone (= 7.0.0) - - when prompted, ok to save new opam file -5. install llair for llvm_sil - - cd ~/path/to/sledge - - opam pin add -n -k git llair . - + when prompted, ok to create new package - - opam install llair -6. hush `ld: warning: directory not found for option '-L/opt/local/lib'` + - for switch in sledge sledge+flambda; do cmake -G Ninja -DCMAKE_INSTALL_PREFIX=../_install/$switch -DLLVM_OCAML_INSTALL_PATH=../_install/$switch -DLLVM_TARGETS_TO_BUILD="X86" .. && ninja && ninja install; done +7. install deps + - cd $SLEDGE/llvm + - for switch in sledge sledge+flambda; do opam pin --switch=$switch add -n -k git llvm .; done + - cd $SLEDGE + - for switch in sledge sledge+flambda; do PATH=$SLEDGE/llvm/_install/$switch/bin:$PATH opam install --yes --switch=$switch ./sledge.opam --deps-only; done +8. hush `ld: warning: directory not found for option '-L/opt/local/lib'` - the zarith package adds a spurious linker option unless you have both brew and macports, so if you see this linker warning when compiling, execute + sudo mkdir -p /opt/local/lib -7. install dev tools - - opam install merlin ocp-indent tuareg user-setup - - install ocamlformat -8. if needed: point new clang to xcode c++ lib - - cd ~/.local/llvm_$(opam config var switch)/include - - ln -s /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++ . -9. llvm dev workflow - - modify llvm sources - - cd ~/path/to/sledge/llvm/_build; ninja -j8 - - iterate - - (optional?) git add -u; git commit -m ... - - ninja -j8 && ninja ocaml_doc && ninja install && opam upgrade llvm - - cd ~/path/to/sledge; make - - it is not uncommon to get "inconsistent assumptions" errors: clean and re-make -10. llvm emacs mode - - (add-to-list 'load-path (expand-file-name "~/path/to/sledge/llvm/utils/emacs")) +9. install dev tools + - opam pin --yes --switch=sledge add tools/opam +10. if needed: point new clang to xcode c++ lib + - cd $SLEDGE/$(opam switch show)/include + - ln -s /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++ . +11. llvm dev workflow + - modify llvm sources + - cd $SLEDGE/llvm/_build; ninja + - iterate + - (optional?) git add -u; git commit -m ... + - ninja && ninja ocaml_doc && ninja install && opam upgrade llvm + - cd $SLEDGE; make + - it is not uncommon to get "inconsistent assumptions" errors: clean and re-make +12. llvm emacs mode + - (add-to-list 'load-path (expand-file-name "$SLEDGE/llvm/utils/emacs")) - (require 'llvm-mode) - (require 'autodisass-llvm-bitcode) +13. install llair for llvm_sil + - cd $SLEDGE + - opam pin add -n -k git llair . + + when prompted, ok to create new package + - opam install llair diff --git a/sledge/bin/sledge.dbg b/sledge/bin/sledge.dbg new file mode 120000 index 000000000..39fb020be --- /dev/null +++ b/sledge/bin/sledge.dbg @@ -0,0 +1 @@ +../_build/dev/src/sledge.exe \ No newline at end of file diff --git a/sledge/bin/sledge.opt b/sledge/bin/sledge.opt new file mode 120000 index 000000000..b65347864 --- /dev/null +++ b/sledge/bin/sledge.opt @@ -0,0 +1 @@ +../_build/release/src/sledge.exe \ No newline at end of file diff --git a/sledge/dune-common.in b/sledge/dune-common.in new file mode 100644 index 000000000..9554bfba3 --- /dev/null +++ b/sledge/dune-common.in @@ -0,0 +1,48 @@ +(* -*- tuareg -*- *) + +let common_flags = + {|(-w +a-4-9-18-40-42-44-48@50 + -strict-formats -strict-sequence + -short-paths -bin-annot -keep-docs + -unboxed-types)|} + +let ocamlc_flags = + match Jbuild_plugin.V1.context with + | "release" -> "-w -26-32 -noassert" + | _ -> "-g" + +let ocamlopt_flags = + match Jbuild_plugin.V1.context with + | "release" -> ocamlc_flags ^ " -w -a -O3" + | _ -> ocamlc_flags + +let coverage_ppx = + match Jbuild_plugin.V1.context with "coverage" -> "bisect_ppx" | _ -> "" + +let ppx_flags = + match Jbuild_plugin.V1.context with "dev" -> "--debug" | _ -> "" + +let flags deps = + Printf.sprintf + {|(flags (%s %s)) + (ocamlc_flags (%s)) + (ocamlopt_flags (%s)) + (preprocess + (pps + ppx_compare + ppx_custom_printf + ppx_expect + ppx_hash + ppx_here + ppx_inline_test + ppx_sexp_conv + ppx_sexp_value + ppx_trace + %s + %s))|} + common_flags + (String.concat " " + (List.map (fun d -> "-open " ^ String.capitalize_ascii d) deps)) + ocamlc_flags ocamlopt_flags ppx_flags coverage_ppx + +let libraries deps = String.concat " " deps diff --git a/sledge/dune-project b/sledge/dune-project new file mode 100644 index 000000000..de4fc2092 --- /dev/null +++ b/sledge/dune-project @@ -0,0 +1 @@ +(lang dune 1.0) diff --git a/sledge/dune-workspace b/sledge/dune-workspace new file mode 100644 index 000000000..4dc9cec0a --- /dev/null +++ b/sledge/dune-workspace @@ -0,0 +1,5 @@ +(lang dune 1.0) + +(context (opam (switch sledge) (name dev) (merlin))) +(context (opam (switch sledge) (name coverage))) +(context (opam (switch sledge+flambda) (name release))) diff --git a/sledge/jbuild-common.in b/sledge/jbuild-common.in deleted file mode 100644 index 6063a6b98..000000000 --- a/sledge/jbuild-common.in +++ /dev/null @@ -1,40 +0,0 @@ -(* -*- tuareg -*- *) - -let common_flags = - {|(-w +a-3-4-9-18-40-42-44-48@50 - -strict-formats -strict-sequence -principal - -short-paths -bin-annot -keep-docs - -unboxed-types)|} - - -let ocamlc_flags = - match Jbuild_plugin.V1.context with - | "dbg" -> "-g -opaque" - | _ -> "-w -26-32 -noassert" - - -let ocamlopt_flags = - match Jbuild_plugin.V1.context with - | "dbg" -> ocamlc_flags - | _ -> ocamlc_flags ^ " -w -a -O3" - - -let ppx_trace_flags = - match Jbuild_plugin.V1.context with - | "dbg" -> "--debug" - | _ -> "" - - -let flags deps = - Printf.sprintf - {|(flags (%s %s)) - (ocamlc_flags (%s)) - (ocamlopt_flags (%s)) - (preprocess (pps ppx_compare ppx_sexp_conv ppx_trace %s ppx_driver.runner))|} - common_flags - (String.concat " " - (List.map (fun d -> "-open " ^ String.capitalize_ascii d) ("core_kernel" :: deps))) - ocamlc_flags ocamlopt_flags ppx_trace_flags - - -let libraries deps = String.concat " " ("core_kernel" :: deps) diff --git a/sledge/jbuild-workspace.in b/sledge/jbuild-workspace.in deleted file mode 100644 index 91dac1867..000000000 --- a/sledge/jbuild-workspace.in +++ /dev/null @@ -1,2 +0,0 @@ -(context ((switch @OPAM_SWITCH@) (name dbg) (merlin))) -(context ((switch @OPAM_SWITCH@) (name default))) diff --git a/sledge/llair.opam b/sledge/llair.opam index 6e6c98821..847a31e1d 100644 --- a/sledge/llair.opam +++ b/sledge/llair.opam @@ -1,16 +1,18 @@ opam-version: "1.2" maintainer: "Josh Berdine " authors: "Josh Berdine " +homepage: "https://github.com/facebook/infer/tree/master/sledge/src/llair" +bug-reports: "https://github.com/facebook/infer/issues" build: [ - ["tools/gen_version.sh" "src/version.ml" version] - [make "jbuilds"] - ["jbuilder" "build" "-p" name "-j" jobs] + [make "dunes"] + ["dune" "build" "-p" name "-j" jobs] ] depends: [ "cmdliner" - "core_kernel" {>= "v0.10.0"} - "jbuilder" {build} + "core_kernel" {>= "v0.11.0"} + "dune" {build} "llvm" {build & = "7.0.0"} - "ppx_compare" {>= "v0.10.0"} + "ppx_compare" {>= "v0.11.0"} + "ppx_hash" {>= "v0.11.0"} "zarith" ] diff --git a/sledge/sledge.opam b/sledge/sledge.opam index e7e88b07c..60e026216 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -1,15 +1,18 @@ opam-version: "1.2" maintainer: "Josh Berdine " authors: "Josh Berdine " +homepage: "https://github.com/facebook/infer/tree/master/sledge" +bug-reports: "https://github.com/facebook/infer/issues" build: [ - ["make setup"] - ["jbuilder" "build" "-p" name "-j" jobs] + [make "setup"] + ["dune" "build" "-p" name "-j" jobs] ] depends: [ "cmdliner" - "core_kernel" {>= "v0.10.0"} - "jbuilder" {build} + "core_kernel" {>= "v0.11.0"} + "dune" {build} "llvm" {build & = "7.0.0"} - "ppx_compare" {>= "v0.10.0"} + "ppx_compare" {>= "v0.11.0"} + "ppx_hash" {>= "v0.11.0"} "zarith" ] diff --git a/sledge/src/dune.in b/sledge/src/dune.in new file mode 100644 index 000000000..bc691d918 --- /dev/null +++ b/sledge/src/dune.in @@ -0,0 +1,20 @@ +(* -*- tuareg -*- *) + +let deps = ["import"; "trace"; "llair_"; "symbheap"] + +;; +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 + (name sledge) + %s + (libraries cmdliner %s)) +|} + (flags deps) (libraries deps) diff --git a/sledge/src/import/dune.in b/sledge/src/import/dune.in new file mode 100644 index 000000000..0fdc31898 --- /dev/null +++ b/sledge/src/import/dune.in @@ -0,0 +1,15 @@ +(* -*- tuareg -*- *) + +let deps = [] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf + {| +(library + (name import) + (public_name llair.import) + %s + (libraries core_kernel zarith %s)) +|} + (flags deps) (libraries deps) diff --git a/sledge/src/import/jbuild.in b/sledge/src/import/jbuild.in deleted file mode 100644 index bcea0faea..000000000 --- a/sledge/src/import/jbuild.in +++ /dev/null @@ -1,13 +0,0 @@ -(* -*- tuareg -*- *) - -let deps = [] - -;; Jbuild_plugin.V1.send @@ Format.sprintf " -(library - ((name import) - (public_name llair.import) - %s - (libraries (zarith %s)))) -" -(flags deps) -(libraries deps) diff --git a/sledge/src/jbuild.in b/sledge/src/jbuild.in deleted file mode 100644 index 21f0e460b..000000000 --- a/sledge/src/jbuild.in +++ /dev/null @@ -1,12 +0,0 @@ -(* -*- tuareg -*- *) - -let deps = ["import"; "trace"; "llair_"] - -;; Jbuild_plugin.V1.send @@ Format.sprintf " -(executable - ((name sledge) - %s - (libraries (cmdliner %s)))) -" -(flags deps) -(libraries deps) diff --git a/sledge/src/llair/dune.in b/sledge/src/llair/dune.in new file mode 100644 index 000000000..8d3080474 --- /dev/null +++ b/sledge/src/llair/dune.in @@ -0,0 +1,15 @@ +(* -*- tuareg -*- *) + +let deps = ["import"; "trace"] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf + {| +(library + (name llair_) + (public_name llair) + %s + (libraries llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target %s)) +|} + (flags deps) (libraries deps) diff --git a/sledge/src/llair/jbuild.in b/sledge/src/llair/jbuild.in deleted file mode 100644 index 48ebe0551..000000000 --- a/sledge/src/llair/jbuild.in +++ /dev/null @@ -1,13 +0,0 @@ -(* -*- tuareg -*- *) - -let deps = ["import"; "trace"] - -;; Jbuild_plugin.V1.send @@ Format.sprintf " -(library - ((name llair_) - (public_name llair) - %s - (libraries (llvm llvm.irreader llvm.analysis llvm.scalar_opts %s)))) -" -(flags deps) -(libraries deps) diff --git a/sledge/src/ppx_trace/dune b/sledge/src/ppx_trace/dune new file mode 100644 index 000000000..dd4d5b14a --- /dev/null +++ b/sledge/src/ppx_trace/dune @@ -0,0 +1,5 @@ +(library + (name ppx_trace) + (kind ppx_rewriter) + (preprocess no_preprocessing) + (libraries ppxlib)) diff --git a/sledge/src/ppx_trace/jbuild b/sledge/src/ppx_trace/jbuild deleted file mode 100644 index b7f37d17f..000000000 --- a/sledge/src/ppx_trace/jbuild +++ /dev/null @@ -1,5 +0,0 @@ -(library - ((name ppx_trace) - (kind ppx_rewriter) - (preprocess no_preprocessing) - (libraries (ppx_core ppx_driver)))) diff --git a/sledge/src/symbheap/dune.in b/sledge/src/symbheap/dune.in new file mode 100644 index 000000000..4cdf53573 --- /dev/null +++ b/sledge/src/symbheap/dune.in @@ -0,0 +1,15 @@ +(* -*- tuareg -*- *) + +let deps = ["import"; "trace"; "llair_"] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf + {| +(library + (name symbheap) + %s + (libraries %s) + (inline_tests)) +|} + (flags deps) (libraries deps) diff --git a/sledge/src/trace/dune.in b/sledge/src/trace/dune.in new file mode 100644 index 000000000..cdb5f4091 --- /dev/null +++ b/sledge/src/trace/dune.in @@ -0,0 +1,15 @@ +(* -*- tuareg -*- *) + +let deps = ["import"] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf + {| +(library + (name trace) + (public_name llair.trace) + %s + (libraries %s)) +|} + (flags deps) (libraries deps) diff --git a/sledge/src/trace/jbuild.in b/sledge/src/trace/jbuild.in deleted file mode 100644 index 2f813edad..000000000 --- a/sledge/src/trace/jbuild.in +++ /dev/null @@ -1,13 +0,0 @@ -(* -*- tuareg -*- *) - -let deps = ["import"] - -;; Jbuild_plugin.V1.send @@ Format.sprintf " -(library - ((name trace) - (public_name llair.trace) - %s - (libraries (%s)))) -" -(flags deps) -(libraries deps) diff --git a/sledge/test/Makefile b/sledge/test/Makefile index 5b048856c..84b9ac310 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -4,7 +4,7 @@ # LICENSE file in the root directory of this source tree. # additional arguments to pass to clang -OPT_ARGS?=-O0 +OPT_ARGS?=-Os CLANG_ARGS?=-g $(OPT_ARGS) # additional arguments to pass to sledge @@ -16,13 +16,12 @@ MEMOUT?=4096 MEMOUTk=$(shell echo $$(( $(MEMOUT) * 1024 ))) # executable to test -SLEDGE_EXE=$(CURDIR)/../_build/dbg/src/sledge.exe +SLEDGE_EXE=$(CURDIR)/../_build/dev/src/sledge.exe MODEL_DIR=$(CURDIR)/../model # configure the non-host llvm and clang -LLVM_PREFIX=$(HOME)/.local/llvm_$(shell opam config var switch) -export PATH := $(LLVM_PREFIX)/bin:$(PATH) +export PATH := $(CURDIR)/../_opam/llvm/bin:$(PATH) # code to test SrcCs:=$(shell find -L * -not -path 'llvm/*' -name '*.c') @@ -31,7 +30,6 @@ SrcLLs:=$(shell find -L * -name '*.ll') SrcBCs:=$(shell find -L * -name '*.bc') GenBCs:=$(patsubst %.c,%.bc,$(SrcCs)) $(patsubst %.cpp,%.bc,$(SrcCPPs)) -GenLLs:=$(patsubst %.bc,%.ll,$(GenBCs) $(SrcBCs)) TestBCs:=$(GenBCs) $(SrcBCs) TestLLs:=$(SrcLLs) @@ -45,11 +43,15 @@ $(MODEL_DIR)/cxxabi.bc: $(MODEL_DIR)/cxxabi.cpp # compile c to llvm bitcode %.bc : %.c $(MODEL_DIR)/cxxabi.bc - @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).c -o - | llvm-link $(MODEL_DIR)/cxxabi.bc - | opt $(OPT_ARGS) -o $(notdir $*).bc) + @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).c -o - | opt $(OPT_ARGS) -o $(notdir $*).bc) + +# @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).c -o - | llvm-link $(MODEL_DIR)/cxxabi.bc - | opt $(OPT_ARGS) -o $(notdir $*).bc) # compile c++ to llvm bitcode %.bc : %.cpp $(MODEL_DIR)/cxxabi.bc - @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).cpp -o - | llvm-link $(MODEL_DIR)/cxxabi.bc - | opt $(OPT_ARGS) -o $(notdir $*).bc) + @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).cpp -o - | opt $(OPT_ARGS) -o $(notdir $*).bc) + +# @(cd $(dir $*) && clang $(CLANG_ARGS) -c -emit-llvm $(notdir $*).cpp -o - | llvm-link $(MODEL_DIR)/cxxabi.bc - | opt $(OPT_ARGS) -o $(notdir $*).bc) # disassemble bitcode to llvm assembly %.ll : %.bc @@ -84,25 +86,42 @@ endef # compile all c to bc compile: $(GenBCs) -# disassemble all bc to ll -disasm: $(GenLLs) - # run all tests test: $(Outs) +# run all tests and generate code coverage information +BISECT_DIR=$(CURDIR)/../_coverage/out +coverage: + @cd ..; dune build _build/coverage/src/sledge.exe + @mkdir -p $(BISECT_DIR) + @-$(MAKE) BISECT_FILE=$(BISECT_DIR)/bisect SLEDGE_EXE=$(CURDIR)/../_build/coverage/src/sledge.exe test -k + @find $(BISECT_DIR) -type f | xargs bisect-ppx-report -I ../_build/coverage/ -text ../_coverage/summary.txt -html ../_coverage/ + @echo "open ../_coverage/index.html" + +# translate all tests +translate: + $(MAKE) SLEDGE_ARGS='$(SLEDGE_ARGS) --compile-only' test + # report all results full-report: @find -L * -name '*.out' \ | xargs grep "RESULT:" \ - | sed 's/.out:/: /' | column -ts$$'\t' | sort -s -k 3 | uniq + | sed 's/.out:/: /' | column -ts$$'\t' | sort | sort -s -t':' -k 3,4 | uniq + +# report all errors +report-errors: + @find -L * -name '*.out' \ + | xargs grep "RESULT:" \ + | grep -E -v "RESULT: (Success|Invalid input)" \ + | sed 's/.out:/: /' | column -ts$$'\t' | sort | sort -s -t':' -k 3,4 | uniq # report errors report: @find -L * -name '*.out' \ | xargs grep "RESULT:" \ - | grep -E -v "RESULT: Unimplemented: (landingpad of type other than {i8\*, i32}|msvc exceptions):" \ + | grep -E -v "RESULT: Unimplemented: (landingpad of type other than {i8\*, i32}|windows exception handling|non-integral pointer types|types with undetermined size):" \ | grep -E -v "RESULT: (Success|Invalid input)" \ - | sed 's/.out:/: /' | column -ts$$'\t' | sort -s -k 3 | uniq + | sed 's/.out:/: /' | column -ts$$'\t' | sort | sort -s -t':' -k 3,4 | uniq # report warnings warnings: @@ -112,10 +131,6 @@ warnings: cleanBC: @rm -f $(GenBCs) -# remove generated assembly files -cleanLL: - @rm -f $(GenLLs) - # remove result files cleanout: @find -L * -name "*.out" -or -name '*.err' \ @@ -139,7 +154,7 @@ cleanIE: | xargs grep -l -E "RESULT: (Internal error|Unimplemented|Unknown error)" \ | xargs rm -f -clean: cleanBC cleanLL cleanout +clean: cleanBC cleanout fmt: clang-format -i $(SrcCs) $(SrcCPPs) diff --git a/sledge/tools/gen_version.sh b/sledge/tools/gen_version.sh index c77f0b468..d4be0788c 100755 --- a/sledge/tools/gen_version.sh +++ b/sledge/tools/gen_version.sh @@ -14,16 +14,14 @@ if [[ ! -z "$2" ]]; then # second arg passed when called from opam VERSION="$2" else - # second arg omitted when called from src/jbuild + # 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 --tags --dirty --always) + VERSION=$(git describe --dirty --always) fi fi -(test -e $FILE || touch $FILE); - -sed -e "s|%%VERSION%[%]|$VERSION|g" $FILE.in | diff $FILE - | patch --silent $FILE +sed -e "s|%%VERSION%[%]|$VERSION|g" $FILE.in > $FILE diff --git a/sledge/tools/opam/dev-tools.opam b/sledge/tools/opam/dev-tools.opam new file mode 100644 index 000000000..35a5394a0 --- /dev/null +++ b/sledge/tools/opam/dev-tools.opam @@ -0,0 +1,12 @@ +opam-version: "1.2" +name: "dev-tools" +version: "0.1" +depends: [ + "bisect_ppx" {>= "1.3.4"} + "merlin" + "ocamlformat" + "ocp-indent" + "patdiff" + "tuareg" + "user-setup" +]