Reviewed By: jvillard Differential Revision: D9850346 fbshipit-source-id: 16fa35ae2master
Josh Berdine
6 years ago
committed by
Facebook Github Bot
parent
e1d4aad487
commit
f6ba0c8137
@ -1,4 +1,3 @@
|
|||||||
break-cases = fit
|
profile = compact
|
||||||
break-string-literals = wrap
|
|
||||||
margin = 77
|
margin = 77
|
||||||
wrap-comments = true
|
wrap-comments = true
|
||||||
|
|||||||
@ -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
|
2. clone llvm, clang, and libcxxabi
|
||||||
- cd ~/path/to/sledge
|
- cd $SLEDGE
|
||||||
- git clone git+ssh://git@github.com/jberdine/llvm.git --branch ocaml_api
|
- git clone https://github.com/jberdine/llvm.git --branch ocaml_api
|
||||||
- git clone https://github.com/llvm-mirror/clang.git llvm/tools/clang
|
- 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
|
- git clone https://github.com/llvm-mirror/libcxxabi.git llvm/projects/libcxxabi
|
||||||
3. build llvm & clang
|
3. export OPAMJOBS=$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1)
|
||||||
- brew install cmake ninja
|
4. create opam switches
|
||||||
- cd ~/path/to/sledge/llvm
|
- 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
|
- mkdir _build
|
||||||
- cd _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 ..
|
- 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
|
||||||
- ninja -j8
|
7. install deps
|
||||||
- ninja ocaml_doc
|
- cd $SLEDGE/llvm
|
||||||
- ninja install
|
- for switch in sledge sledge+flambda; do opam pin --switch=$switch add -n -k git llvm .; done
|
||||||
4. install deps
|
- cd $SLEDGE
|
||||||
- add ~/.local/llvm_$(opam config var switch)/bin to shell PATH
|
- for switch in sledge sledge+flambda; do PATH=$SLEDGE/llvm/_install/$switch/bin:$PATH opam install --yes --switch=$switch ./sledge.opam --deps-only; done
|
||||||
+ because installing the opam package for llvm will look for it
|
8. hush `ld: warning: directory not found for option '-L/opt/local/lib'`
|
||||||
+ 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'`
|
|
||||||
- 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
|
- 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
|
+ sudo mkdir -p /opt/local/lib
|
||||||
7. install dev tools
|
9. install dev tools
|
||||||
- opam install merlin ocp-indent tuareg user-setup
|
- opam pin --yes --switch=sledge add tools/opam
|
||||||
- install ocamlformat
|
10. if needed: point new clang to xcode c++ lib
|
||||||
8. if needed: point new clang to xcode c++ lib
|
- cd $SLEDGE/$(opam switch show)/include
|
||||||
- cd ~/.local/llvm_$(opam config var switch)/include
|
|
||||||
- ln -s /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++ .
|
- ln -s /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++ .
|
||||||
9. llvm dev workflow
|
11. llvm dev workflow
|
||||||
- modify llvm sources
|
- modify llvm sources
|
||||||
- cd ~/path/to/sledge/llvm/_build; ninja -j8
|
- cd $SLEDGE/llvm/_build; ninja
|
||||||
- iterate
|
- iterate
|
||||||
- (optional?) git add -u; git commit -m ...
|
- (optional?) git add -u; git commit -m ...
|
||||||
- ninja -j8 && ninja ocaml_doc && ninja install && opam upgrade llvm
|
- ninja && ninja ocaml_doc && ninja install && opam upgrade llvm
|
||||||
- cd ~/path/to/sledge; make
|
- cd $SLEDGE; make
|
||||||
- it is not uncommon to get "inconsistent assumptions" errors: clean and re-make
|
- it is not uncommon to get "inconsistent assumptions" errors: clean and re-make
|
||||||
10. llvm emacs mode
|
12. llvm emacs mode
|
||||||
- (add-to-list 'load-path (expand-file-name "~/path/to/sledge/llvm/utils/emacs"))
|
- (add-to-list 'load-path (expand-file-name "$SLEDGE/llvm/utils/emacs"))
|
||||||
- (require 'llvm-mode)
|
- (require 'llvm-mode)
|
||||||
- (require 'autodisass-llvm-bitcode)
|
- (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
|
||||||
|
|||||||
@ -0,0 +1 @@
|
|||||||
|
../_build/dev/src/sledge.exe
|
||||||
@ -0,0 +1 @@
|
|||||||
|
../_build/release/src/sledge.exe
|
||||||
@ -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
|
||||||
@ -0,0 +1 @@
|
|||||||
|
(lang dune 1.0)
|
||||||
@ -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)))
|
||||||
@ -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)
|
|
||||||
@ -1,2 +0,0 @@
|
|||||||
(context ((switch @OPAM_SWITCH@) (name dbg) (merlin)))
|
|
||||||
(context ((switch @OPAM_SWITCH@) (name default)))
|
|
||||||
@ -1,16 +1,18 @@
|
|||||||
opam-version: "1.2"
|
opam-version: "1.2"
|
||||||
maintainer: "Josh Berdine <jjb@fb.com>"
|
maintainer: "Josh Berdine <jjb@fb.com>"
|
||||||
authors: "Josh Berdine <jjb@fb.com>"
|
authors: "Josh Berdine <jjb@fb.com>"
|
||||||
|
homepage: "https://github.com/facebook/infer/tree/master/sledge/src/llair"
|
||||||
|
bug-reports: "https://github.com/facebook/infer/issues"
|
||||||
build: [
|
build: [
|
||||||
["tools/gen_version.sh" "src/version.ml" version]
|
[make "dunes"]
|
||||||
[make "jbuilds"]
|
["dune" "build" "-p" name "-j" jobs]
|
||||||
["jbuilder" "build" "-p" name "-j" jobs]
|
|
||||||
]
|
]
|
||||||
depends: [
|
depends: [
|
||||||
"cmdliner"
|
"cmdliner"
|
||||||
"core_kernel" {>= "v0.10.0"}
|
"core_kernel" {>= "v0.11.0"}
|
||||||
"jbuilder" {build}
|
"dune" {build}
|
||||||
"llvm" {build & = "7.0.0"}
|
"llvm" {build & = "7.0.0"}
|
||||||
"ppx_compare" {>= "v0.10.0"}
|
"ppx_compare" {>= "v0.11.0"}
|
||||||
|
"ppx_hash" {>= "v0.11.0"}
|
||||||
"zarith"
|
"zarith"
|
||||||
]
|
]
|
||||||
|
|||||||
@ -1,15 +1,18 @@
|
|||||||
opam-version: "1.2"
|
opam-version: "1.2"
|
||||||
maintainer: "Josh Berdine <jjb@fb.com>"
|
maintainer: "Josh Berdine <jjb@fb.com>"
|
||||||
authors: "Josh Berdine <jjb@fb.com>"
|
authors: "Josh Berdine <jjb@fb.com>"
|
||||||
|
homepage: "https://github.com/facebook/infer/tree/master/sledge"
|
||||||
|
bug-reports: "https://github.com/facebook/infer/issues"
|
||||||
build: [
|
build: [
|
||||||
["make setup"]
|
[make "setup"]
|
||||||
["jbuilder" "build" "-p" name "-j" jobs]
|
["dune" "build" "-p" name "-j" jobs]
|
||||||
]
|
]
|
||||||
depends: [
|
depends: [
|
||||||
"cmdliner"
|
"cmdliner"
|
||||||
"core_kernel" {>= "v0.10.0"}
|
"core_kernel" {>= "v0.11.0"}
|
||||||
"jbuilder" {build}
|
"dune" {build}
|
||||||
"llvm" {build & = "7.0.0"}
|
"llvm" {build & = "7.0.0"}
|
||||||
"ppx_compare" {>= "v0.10.0"}
|
"ppx_compare" {>= "v0.11.0"}
|
||||||
|
"ppx_hash" {>= "v0.11.0"}
|
||||||
"zarith"
|
"zarith"
|
||||||
]
|
]
|
||||||
|
|||||||
@ -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)
|
||||||
@ -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)
|
||||||
@ -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)
|
|
||||||
@ -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)
|
|
||||||
@ -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)
|
||||||
@ -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)
|
|
||||||
@ -0,0 +1,5 @@
|
|||||||
|
(library
|
||||||
|
(name ppx_trace)
|
||||||
|
(kind ppx_rewriter)
|
||||||
|
(preprocess no_preprocessing)
|
||||||
|
(libraries ppxlib))
|
||||||
@ -1,5 +0,0 @@
|
|||||||
(library
|
|
||||||
((name ppx_trace)
|
|
||||||
(kind ppx_rewriter)
|
|
||||||
(preprocess no_preprocessing)
|
|
||||||
(libraries (ppx_core ppx_driver))))
|
|
||||||
@ -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)
|
||||||
@ -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)
|
||||||
@ -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)
|
|
||||||
@ -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"
|
||||||
|
]
|
||||||
Loading…
Reference in new issue