[sledge] Change build system to not generate dune files

Reviewed By: jvillard

Differential Revision: D20322877

fbshipit-source-id: 0034a4163
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent fff3a491bf
commit 0c7249b992

4
sledge/.gitignore vendored

@ -1,9 +1,5 @@
.llvm_build .llvm_build
.llvm_install .llvm_install
.merlin
/bin/dune
/lib/dune
/lib/import/dune
/llvm/ /llvm/
/test/*/*.bc /test/*/*.bc
/test/*/*.bc.err /test/*/*.bc.err

@ -8,11 +8,10 @@ default: exes
EXES = bin/sledge EXES = bin/sledge
INSTALLS = sledge INSTALLS = sledge
FMTS = @_build/dbg/lib/fmt @_build/dbg/bin/fmt
DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS)) _build/dbg/sledge-help.txt DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS))
TARGETS = $(DBG_TARGETS) $(subst dbg,dbg-opt,$(DBG_TARGETS)) $(subst dbg,opt,$(DBG_TARGETS)) TARGETS = $(DBG_TARGETS) $(subst dbg,dbg-opt,$(DBG_TARGETS)) $(subst dbg,opt,$(DBG_TARGETS)) _build/opt/sledge-help.txt
dune_build_dbg = dune build $(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_install_dbg = dune install --context=dbg --prefix=_build/_install/dbg sledge 2>/dev/null
@ -23,76 +22,52 @@ dune_install_dbg_opt = $(subst dbg,dbg-opt,$(dune_install_dbg))
dune_build_opt = $(subst dbg,opt,$(dune_build_dbg)) dune_build_opt = $(subst dbg,opt,$(dune_build_dbg))
dune_install_opt = $(subst dbg,opt,$(dune_install_dbg)) dune_install_opt = $(subst dbg,opt,$(dune_install_dbg))
DUNEINS = $(shell find lib bin model -name dune.in)
DUNES = $(patsubst %.in,%,$(DUNEINS))
.PHONY: dunes
dunes: $(DUNES)
%/dune: dune-common.in %/dune.in
cat $+ > $@
.PHONY: setup
setup: dunes
.PHONY: check .PHONY: check
check: setup check:
dune build @check dune build @check
.PHONY: exes .PHONY: exes
exes: setup exes:
dune build $(TARGETS) dune build $(TARGETS)
$(dune_install_dbg) $(dune_install_dbg)
$(dune_install_dbg_opt) $(dune_install_dbg_opt)
$(dune_install_opt) $(dune_install_opt)
.PHONY: dbg .PHONY: dbg
dbg: setup dbg:
$(dune_build_dbg) $(dune_build_dbg)
$(dune_install_dbg) $(dune_install_dbg)
.PHONY: do .PHONY: do
do: setup do:
$(dune_build_dbg_opt) $(dune_build_dbg_opt)
$(dune_install_dbg_opt) $(dune_install_dbg_opt)
.PHONY: opt .PHONY: opt
opt: setup opt:
$(dune_build_opt) $(dune_build_opt)
$(dune_install_opt) $(dune_install_opt)
.PHONY: watch .PHONY: watch
watch: setup watch:
dune build --watch --terminal-persistence=clear-on-rebuild $(TARGETS) dune build --watch --terminal-persistence=clear-on-rebuild $(TARGETS)
.PHONY: test .PHONY: test
test: setup test:
-dune build @_build/dbg/runtest --auto-promote -dune build @_build/dbg/runtest --auto-promote
dune build $(FMTS) --auto-promote dune build @fmt --auto-promote
.PHONY: ci-test .PHONY: ci-test
ci-test: setup ci-test:
dune build @_build/dbg/runtest dune build @_build/dbg/runtest
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/
@echo "open _coverage/index.html"
.PHONY: clean .PHONY: clean
clean: clean:
dune clean dune clean
rm -rf _coverage $(DUNES)
.PHONY: fmt .PHONY: fmt
fmt: fmt:
dune build @fmt --auto-promote dune build @fmt --auto-promote
ocamlformat -i $(DUNEINS)
clang-format -i model/llair_intrinsics.h model/cxxabi.cpp clang-format -i model/llair_intrinsics.h model/cxxabi.cpp
${MAKE} -C test fmt ${MAKE} -C test fmt

@ -0,0 +1,16 @@
; 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.
(executable
(public_name sledge)
(package sledge)
(libraries dune-build-info llvm llvm.irreader llvm.analysis llvm.scalar_opts
llvm.target llvm.ipo llvm.linker shexp.process yojson trace import
sledgelib model)
(flags
(:standard -open Import -open Sledgelib -open Model))
(preprocess
(pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here
ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace)))

@ -1,22 +0,0 @@
(* -*- tuareg -*- *)
(*
* 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.
*)
let deps = ["import"; "libsledge"; "model"]
;;
Jbuild_plugin.V1.send
@@ Format.sprintf
{|
(executable
(public_name sledge)
(package sledge)
(libraries dune-build-info llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo llvm.linker shexp.process yojson %s)
%s)
|}
(libraries ("trace" :: deps))
(flags `exe deps)

@ -1,59 +0,0 @@
(* -*- tuareg -*- *)
(*
* 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.
*)
let common_flags =
{|(-w +a-4-9-18-40-42-44-48@50-66
-strict-formats -strict-sequence
-short-paths -bin-annot -keep-docs
-unboxed-types)|}
let ocamlc_flags =
match Jbuild_plugin.V1.context with
| "opt" | "dbg-opt" -> "-w -26-32 -noassert"
| _ -> "-g"
let ocamlopt_flags =
match Jbuild_plugin.V1.context with
| "opt" | "dbg-opt" -> 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
| "dbg" | "dbg-opt" -> "--debug"
| _ -> ""
let flags exe_or_lib 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_let
ppx_sexp_conv
ppx_sexp_value
ppx_trace
%s
%s))
%s|}
common_flags
(String.concat " "
(List.map (fun d -> "-open " ^ String.capitalize_ascii d) deps))
ocamlc_flags ocamlopt_flags ppx_flags coverage_ppx
(match exe_or_lib with `lib -> "(inline_tests)" | _ -> "")
let libraries deps = String.concat " " deps

@ -5,7 +5,29 @@
; This source code is licensed under the MIT license found in the ; This source code is licensed under the MIT license found in the
; LICENSE file in the root directory of this source tree. ; LICENSE file in the root directory of this source tree.
(context (opam (switch sledge) (name dbg) (merlin))) (env
(context (opam (switch sledge) (name dbg-opt))) (dbg
(context (opam (switch sledge) (name opt))) (flags
(context (opam (switch sledge) (name coverage))) (-w +a-4-9-18-40-42-44-48@50-66 -strict-formats -strict-sequence
-short-paths -bin-annot -keep-locs -keep-docs -opaque))
(env-vars
(PPX_TRACE_ENABLED 1))
(inline_tests enabled))
(opt
(flags
(-w -a -noassert -unboxed-types))
(ocamlopt_flags (-O3))
(env-vars
(PPX_TRACE_ENABLED 0))
(inline_tests disabled))
(dbg-opt
(flags
(-w -a -noassert -unboxed-types))
(ocamlopt_flags (-O3))
(env-vars
(PPX_TRACE_ENABLED 1))
(inline_tests disabled)))
(context (opam (switch sledge) (name dbg) (profile dbg) (merlin)))
(context (opam (switch sledge) (name opt) (profile opt)))
(context (opam (switch sledge) (name dbg-opt) (profile dbg-opt)))

@ -0,0 +1,14 @@
; 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.
(library
(name sledgelib)
(libraries apron apron.boxMPQ ctypes ctypes.foreign trace import)
(flags
(:standard -open Import))
(preprocess
(pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here
ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace))
(inline_tests))

@ -1,21 +0,0 @@
(* -*- tuareg -*- *)
(*
* 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.
*)
let deps = ["import"]
;;
Jbuild_plugin.V1.send
@@ Format.sprintf
{|
(library
(name libsledge)
(libraries apron apron.boxMPQ ctypes ctypes.foreign %s)
%s)
|}
(libraries ("trace" :: deps))
(flags `lib deps)

@ -0,0 +1,14 @@
; 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.
(library
(name import)
(public_name sledge.import)
(libraries core core_kernel.fheap zarith trace)
(flags (:standard))
(preprocess
(pps ppx_compare ppx_custom_printf ppx_expect ppx_hash ppx_here
ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_trace))
(inline_tests))

@ -1,22 +0,0 @@
(* -*- tuareg -*- *)
(*
* 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.
*)
let deps = []
;;
Jbuild_plugin.V1.send
@@ Format.sprintf
{|
(library
(name import)
(public_name sledge.import)
(libraries core core_kernel.fheap zarith %s)
%s)
|}
(libraries ("trace" :: deps))
(flags `lib deps)

@ -1,3 +1,8 @@
; 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.
(library (library
(name ppx_trace) (name ppx_trace)
(kind ppx_rewriter) (kind ppx_rewriter)

@ -6,8 +6,8 @@ bug-reports: "https://github.com/facebook/infer/issues/new?template=sledge_issue
dev-repo: "git://github.com/facebook/infer.git" dev-repo: "git://github.com/facebook/infer.git"
license: "MIT" license: "MIT"
build: [ build: [
[make "setup"] ["dune" "build" "_build/opt/bin/sledge.exe" "-j" jobs]
["dune" "build" "-p" name "--profile" "opt" "-j" jobs] ["dune" "install" "--context=opt" "sledge"]
] ]
depends: [ depends: [
"ocaml" "ocaml"

@ -2,7 +2,6 @@ opam-version: "1.2"
name: "dev-tools" name: "dev-tools"
version: "0.1" version: "0.1"
depends: [ depends: [
"bisect_ppx" {>= "1.3.4"}
"merlin" "merlin"
"ocp-indent" "ocp-indent"
"patdiff" "patdiff"

Loading…
Cancel
Save