diff --git a/sledge/bin/dune b/sledge/bin/dune deleted file mode 100644 index b8ed12df3..000000000 --- a/sledge/bin/dune +++ /dev/null @@ -1,16 +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. - -(executable - (name sledge_cli) - (public_name sledge) - (package sledge) - (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm - llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo - llvm.linker shexp.process yojson trace import sledge model) - (flags - (:standard -w -58 -open Import -open Sledge -open Model)) - (preprocess - (pps ppx_sledge))) diff --git a/sledge/dune b/sledge/dune index 8867d990f..6bf4fcf64 100644 --- a/sledge/dune +++ b/sledge/dune @@ -18,7 +18,7 @@ (env-vars (PPX_TRACE_ENABLED 1)) (inline_tests disabled)) - (_ + (_ ; release, dev, default,... (flags (-w -a -noassert -unboxed-types)) (ocamlopt_flags (-O3)) @@ -26,6 +26,71 @@ (PPX_TRACE_ENABLED 0)) (inline_tests disabled))) +(library + (name ppx_sledge) + (kind ppx_rewriter) + (libraries ppx_compare ppx_expect ppx_hash ppx_here ppx_inline_test ppx_let + ppx_sexp_conv ppx_sexp_value) + (preprocess no_preprocessing)) + +(subdir + src/import + (library + (name import) + (public_name sledge.import) + (libraries core core_kernel.fheap zarith trace) + (flags (:standard)) + (preprocess + (pps ppx_sledge ppx_trace)) + (inline_tests))) + +(subdir + src + (library + (name sledge) + (public_name sledge) + (libraries import) + (flags + (:standard -open Import)) + (preprocess + (pps ppx_sledge ppx_trace)) + (inline_tests))) + +(subdir + model + (rule + (targets cxxabi.bc) + (deps cxxabi.cpp Makefile llair_intrinsics.h) + (action + (run make ROOT=../../.. cxxabi.bc))) + (rule + (targets lib_fuzzer_main.bc) + (deps lib_fuzzer_main.c Makefile) + (action + (run make ROOT=../../.. lib_fuzzer_main.bc))) + (rule + (targets model.ml) + (deps cxxabi.bc lib_fuzzer_main.bc) + (action + (run ocaml-crunch -m plain -e bc -o model.ml .))) + (library + (name model) + (public_name sledge.model))) + +(subdir + bin + (executable + (name sledge_cli) + (public_name sledge) + (package sledge) + (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm + llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo + llvm.linker shexp.process yojson trace import sledge model) + (flags + (:standard -w -58 -open Import -open Sledge -open Model)) + (preprocess + (pps ppx_sledge ppx_trace)))) + (dirs :standard \ llvm test) (rule diff --git a/sledge/dune-project b/sledge/dune-project index 929c696e5..a0727d625 100644 --- a/sledge/dune-project +++ b/sledge/dune-project @@ -1 +1,7 @@ -(lang dune 2.0) +(lang dune 2.5) + +(package + (name ppx_trace)) + +(package + (name sledge)) diff --git a/sledge/model/dune b/sledge/model/dune deleted file mode 100644 index e520fe1b7..000000000 --- a/sledge/model/dune +++ /dev/null @@ -1,26 +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. - -(rule - (targets cxxabi.bc) - (deps cxxabi.cpp Makefile llair_intrinsics.h) - (action - (run make ROOT=../../.. cxxabi.bc))) - -(rule - (targets lib_fuzzer_main.bc) - (deps lib_fuzzer_main.c Makefile) - (action - (run make ROOT=../../.. lib_fuzzer_main.bc))) - -(rule - (targets model.ml) - (deps cxxabi.bc lib_fuzzer_main.bc) - (action - (run ocaml-crunch -m plain -e bc -o model.ml .))) - -(library - (name model) - (public_name sledge.model)) diff --git a/sledge/ppx_sledge/dune b/sledge/ppx_sledge/dune deleted file mode 100644 index 901c3454d..000000000 --- a/sledge/ppx_sledge/dune +++ /dev/null @@ -1,14 +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. - -(library - (name ppx_sledge) - (kind - (ppx_rewriter - (cookies - (ppx_trace_enabled %{env:PPX_TRACE_ENABLED=0})))) - (libraries ppx_compare ppx_expect ppx_hash ppx_here ppx_inline_test ppx_let - ppx_sexp_conv ppx_sexp_value ppx_trace) - (preprocess no_preprocessing)) diff --git a/sledge/ppx_trace.opam b/sledge/ppx_trace.opam deleted file mode 100644 index fec12fd55..000000000 --- a/sledge/ppx_trace.opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "2.0" -maintainer: "Josh Berdine " -authors: "Josh Berdine " -homepage: "https://github.com/facebook/infer/tree/master/sledge/ppx_trace" -bug-reports: "https://github.com/facebook/infer/issues/new?template=sledge_issue_template.md" -dev-repo: "git://github.com/facebook/infer.git" -license: "MIT" -build: [ - ["dune" "build" "-p" name "-j" jobs] -] -depends: [ - "ocaml" - "dune" {>= "2.0.0"} - "ppxlib" -] -synopsis: "Conditionally compiled debug tracing" -description: "Conditionally compiled debug tracing" diff --git a/sledge/ppx_trace/dune b/sledge/ppx_trace/dune index 45c1c7126..4545a7069 100644 --- a/sledge/ppx_trace/dune +++ b/sledge/ppx_trace/dune @@ -3,8 +3,17 @@ ; This source code is licensed under the MIT license found in the ; LICENSE file in the root directory of this source tree. +(subdir + trace + (library + (name trace) + (public_name ppx_trace.trace))) + (library - (name ppx_trace) - (kind ppx_rewriter) + (public_name ppx_trace) + (kind + (ppx_rewriter + (cookies + (ppx_trace_enabled %{env:PPX_TRACE_ENABLED=0})))) (preprocess no_preprocessing) (libraries ppxlib)) diff --git a/sledge/ppx_trace/trace/dune b/sledge/ppx_trace/trace/dune deleted file mode 100644 index df18ccc4d..000000000 --- a/sledge/ppx_trace/trace/dune +++ /dev/null @@ -1,8 +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. - -(library - (name trace) - (public_name ppx_trace.trace)) diff --git a/sledge/sledge.opam b/sledge/sledge.opam index 7d0e5eb3a..ab3e3b93a 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -6,19 +6,18 @@ bug-reports: "https://github.com/facebook/infer/issues/new?template=sledge_issue dev-repo: "git://github.com/facebook/infer.git" license: "MIT" build: [ - ["dune" "build" "_build/opt/bin/sledge.exe" "-j" jobs] - ["dune" "install" "--context=opt" "sledge"] + [make "release"] ] depends: [ "ocaml" "apron" - "base" {>= "v0.12.0"} - "core" + "base" + "core" {>= "v0.14"} "crunch" {build} "ctypes" "ctypes-foreign" - "dune" {>= "2.0" build} - "dune-build-info" + "dune" {build & >= "2.5"} + "dune-build-info" {build} "llvm" {= "8.0.0"} "ppx_compare" "ppx_hash" diff --git a/sledge/src/dune b/sledge/src/dune deleted file mode 100644 index 9723fbd88..000000000 --- a/sledge/src/dune +++ /dev/null @@ -1,14 +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. - -(library - (name sledge) - (public_name sledge) - (libraries trace import) - (flags - (:standard -open Import)) - (preprocess - (pps ppx_sledge)) - (inline_tests)) diff --git a/sledge/src/import/dune b/sledge/src/import/dune deleted file mode 100644 index 00ec926ad..000000000 --- a/sledge/src/import/dune +++ /dev/null @@ -1,13 +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. - -(library - (name import) - (public_name sledge.import) - (libraries core core_kernel.fheap zarith trace) - (flags (:standard)) - (preprocess - (pps ppx_sledge)) - (inline_tests))